matroids[T: TYPE]: THEORY
%------------------------------------------------------------------------------
%
% Experimental Theory
%
% Author: Jon Sjogren, Rick Butler
%
%------------------------------------------------------------------------------

BEGIN

 IMPORTING  finite_sets@finite_sets_eq[T,T]

  pre_matroid: TYPE = [# elem: finite_set[T],
                         indep: [finite_set[T] -> bool]  #]

  indep_in_elem(M: pre_matroid): bool = (FORALL (A:finite_set[T]): 
                                         indep(M)(A) IMPLIES subset?(A,elem(M)))

  indep_subset(M: pre_matroid): bool = (FORALL (A,B:finite_set[T]): 
                    indep(M)(A) and subset?(B,A) IMPLIES indep(M)(B))

  indep_card(M: pre_matroid): bool = (FORALL (A,B:finite_set[T]):
             indep(M)(A) AND indep(M)(B) AND card(A) < card(B)
                 IMPLIES (Exists (x: T): elem(M)(x) AND A(x) AND NOT B(x)
                                         AND indep(M)(add(x,B))))
 
  Matroid: TYPE = {M: pre_matroid | indep_in_elem(M) AND
                                    indep_subset(M) AND 
                                    indep_card(M)}

  x,y: VAR T

  single(x): finite_set[T] = {t: T | t = x}

  double(x,y): finite_set[T] = {t: T | t = x OR t = y}

  simple?(M: Matroid): bool = (FORALL x: elem(M)(x) IMPLIES
                                         (indep(M)(single(x)) AND 
                                          (FORALL y: x /=y IMPLIES 
                                                  indep(M)(double(x,y)))))
                               
  Simple_matroid: TYPE = {M: Matroid | simple?(M)}

  A,B: VAR finite_set[T]
  Subsets(A): TYPE = {B: finite_set[T] | subset?(B,A)}

  M1,M2: VAR Matroid

  extend(M1,M2,(f:[(elem(M1)) -> (elem(M2))])):
                          [Subsets(elem(M1)) -> finite_set[T]] =
           (LAMBDA (A: Subsets(elem(M1))): {t: T | (EXISTS (a: (A)): f(a) = t)})

  isomorph(M1,M2): TYPE = {f: [(elem(M1)) -> (elem(M2))] | 
                         bijective?(f) AND
                         (FORALL (A: Subsets(elem(M1))): indep(M1)(A) IFF
                                              indep(M2)(extend(M1,M2,f)(A)))}


% A circuit is a non-independent set such that when you remove any element,
% it becomes independent.

  circuit?(M: Matroid, A: finite_set[T]): bool = subset?(A,elem(M))
                                                 AND NOT indep(M)(A) AND 
                                                 (FORALL (x: (elem(M))): A(x) 
                                                    IMPLIES indep(M)(remove(x,A)))

  M: VAR Matroid

  circuit_test: LEMMA circuit?(M,A) IMPLIES (subset?(A,elem(M)) AND
                      NOT indep(M)(A) AND (subset?(B,A) and B /= A 
                  IMPLIES indep(M)(B)))

circuit_test2: LEMMA  (subset?(A,elem(M)) AND
                      NOT indep(M)(A) AND 
                      FORALL B: (subset?(B,A) AND B /= A IMPLIES indep(M)(B))) 
                         IMPLIES circuit?(M,A)



End matroids