equal
deleted
inserted
replaced
72 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); |
72 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); |
73 val Fin_UnionI = result(); |
73 val Fin_UnionI = result(); |
74 |
74 |
75 (*Every subset of a finite set is finite.*) |
75 (*Every subset of a finite set is finite.*) |
76 goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)"; |
76 goal Fin.thy "!!b A. b: Fin(A) ==> ALL z. z<=b --> z: Fin(A)"; |
77 be Fin_induct 1; |
77 by (etac Fin_induct 1); |
78 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1); |
78 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1); |
79 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1])); |
79 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1])); |
80 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2); |
80 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2); |
81 by (ALLGOALS (asm_simp_tac Fin_ss)); |
81 by (ALLGOALS (asm_simp_tac Fin_ss)); |
82 val Fin_subset_lemma = result(); |
82 val Fin_subset_lemma = result(); |