Goalw [is_Matroid_def] "is_Matroid S F ==> finite(S)"; by (etac conjE 1); by (assume_tac 1); qed "is_MatroidD1"; Goalw [is_Matroid_def] "is_Matroid S F ==> F <= Pow S"; by (etac conjE 1); by (etac conjE 1); by (assume_tac 1); qed "is_MatroidD2"; Goalw [is_Matroid_def] "is_Matroid S F ==> {} : F"; by (etac conjE 1); by (etac conjE 1); by (etac conjE 1); by (assume_tac 1); qed "is_MatroidD3"; Goalw [is_Matroid_def] "is_Matroid S F ==> \ \ ALL X Y. X:F & Y <= X --> Y:F"; by (REPEAT(etac conjE 1)); by (assume_tac 1); qed "is_MatroidD4"; Goalw [is_Matroid_def] "is_Matroid S F ==> \ \ (ALL X Y. X:F --> Y:F --> (card(Y) < card(X)) \ \ --> (EX x. x : X-Y & insert x Y : F )) " ; by (REPEAT(etac conjE 1)); by (assume_tac 1); qed "is_MatroidD5"; Goalw [Matroid_def] "is_Matroid S F ==> F : Matroid S"; by (Blast_tac 1); qed "mem_MatroidsetI"; Goalw [Matroid_def] "F : Matroid S ==> is_Matroid S F"; by (Blast_tac 1); qed "mem_MatroidsetD"; Goalw [Matroid_def,is_Matroid_def] "F : Matroid S ==> finite(F)"; by (dtac CollectD 1); by (REPEAT(etac conjE 1)); by (dtac (finite_Pow_iff RS iffD2) 1); by (rotate_tac ~1 1); by (etac (rotate_prems 1 finite_subset) 1); by (assume_tac 1); qed "matroid_finite"; (* Trying using Larry's advice Goalw [Matroid_def,is_Matroid_def] "F : Matroid S ==> finite(F)"; by (Clarify_tac 1); by (dtac (finite_Pow_iff RS iffD2) 1); by (blast_tac (claset() addIs [finite_subset]) 1); *) Goalw [Bases_def] "X : Bases S F ==> is_Matroid S F"; by (dtac CollectD 1); by (etac conjE 1); by (assume_tac 1); qed "BasesD1"; Goalw [Bases_def] "X : Bases S F ==> F : Matroid S"; by (dtac CollectD 1); by (rtac mem_MatroidsetI 1); by (Clarify_tac 1); qed "BasesD1b"; Goalw [Bases_def] "X : Bases S F ==> X : F"; by (dtac CollectD 1); by (REPEAT(etac conjE 1)); by (assume_tac 1); qed "BasesD2"; Goalw [Bases_def] "X : Bases S F ==> ~(EX X' . X < X' & X' : F)" ; by (dtac CollectD 1); by (REPEAT(etac conjE 1)); by (assume_tac 1); qed "BasesD3"; Goalw [Bases_def] "[| F : Matroid S ; X : F ; (EX X' . X < X' & X' : F) |] ==> X ~: Bases S F"; by (Blast_tac 1); qed "nonMaxNonBase"; Goal "~P ==> ~R ==> (P|Q|R) ==> Q"; by (Best_tac 1); qed "ex2imp3"; Goal "~((m::nat) < n) & ~(n < m) ==> n=m"; by (Clarify_tac 1); by (dres_inst_tac [("P","m EX X'. X < X' & X' : F "; by (Blast_tac 1); qed "xprimeD"; Goal " [| X : F; Y : Bases S F; card(X) < card(Y) |] ==> X ~: Bases S F" ; by (rtac nonMaxNonBase 1); by (blast_tac (claset() addIs [BasesD1 RS mem_MatroidsetI]) 1); by (Clarify_tac 1); by (res_inst_tac [("Y","Y")] xprimeD 1); by (rotate_tac 1 1); by (ftac BasesD1 1); by (dtac BasesD2 1); by (blast_tac (claset() addDs [is_MatroidD5]) 1); qed "XlessYnotBase"; Goal " [| X : Bases S F ; Y : Bases S F |] ==> card(X) = card(Y)"; (* Goal "( Q&R --> ~P ) --> P&Q --> ~R " ; by (Clarify_tac 1); qed "exc3rd"; Goal "P&Q --> ~R " ; by (eres_inst_tac [("P","P"),("Q","Q"),("R","R")] exc3rd 1); Goal " Goal "ALL X Y. (X : Bases S F & Y : Bases S F --> card(X) = card(Y))"; by (strip_tac 1); by (Clarify_tac 1); by (rtac notless_impeq 1); by (rtac conjI 1); by (dtac exc3rd 1); Goal "X : F & Y : Bases S F & card(X) < card(Y) --> X ~: Bases S F" ; by (rtac impI 1); by (rtac nonMaxNonBase 1); by (Clarify_tac 1); by (ftac (BasesD1 RS mem_MatroidsetI) 1); by (assume_tac 1); *)