53 by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
53 by (etac (cons_absorb RS ssubst) 3 THEN assume_tac 3); (*backtracking!*) |
54 by (REPEAT (ares_tac prems 1)); |
54 by (REPEAT (ares_tac prems 1)); |
55 val Fin_induct = result(); |
55 val Fin_induct = result(); |
56 |
56 |
57 (** Simplification for Fin **) |
57 (** Simplification for Fin **) |
58 val Fin_ss = arith_ss addcongs mk_congs Fin.thy ["Fin"] addrews Fin.intrs; |
58 val Fin_ss = arith_ss addsimps Fin.intrs; |
59 |
59 |
60 (*The union of two finite sets is fin*) |
60 (*The union of two finite sets is fin*) |
61 val major::prems = goal Fin.thy |
61 val major::prems = goal Fin.thy |
62 "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; |
62 "[| b: Fin(A); c: Fin(A) |] ==> b Un c : Fin(A)"; |
63 by (rtac (major RS Fin_induct) 1); |
63 by (rtac (major RS Fin_induct) 1); |
64 by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Un_0, Un_cons])))); |
64 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Un_0, Un_cons])))); |
65 val Fin_UnI = result(); |
65 val Fin_UnI = result(); |
66 |
66 |
67 (*The union of a set of finite sets is fin*) |
67 (*The union of a set of finite sets is fin*) |
68 val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; |
68 val [major] = goal Fin.thy "C : Fin(Fin(A)) ==> Union(C) : Fin(A)"; |
69 by (rtac (major RS Fin_induct) 1); |
69 by (rtac (major RS Fin_induct) 1); |
70 by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews [Union_0, Union_cons, Fin_UnI]))); |
70 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps [Union_0, Union_cons, Fin_UnI]))); |
71 val Fin_UnionI = result(); |
71 val Fin_UnionI = result(); |
72 |
72 |
73 (*Every subset of a finite set is fin*) |
73 (*Every subset of a finite set is fin*) |
74 val [subs,fin] = goal Fin.thy "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"; |
74 val [subs,fin] = goal Fin.thy "[| c<=b; b: Fin(A) |] ==> c: Fin(A)"; |
75 by (EVERY1 [subgoal_tac "(ALL z. z<=b --> z: Fin(A))", |
75 by (EVERY1 [subgoal_tac "(ALL z. z<=b --> z: Fin(A))", |
76 etac (spec RS mp), |
76 etac (spec RS mp), |
77 rtac subs]); |
77 rtac subs]); |
78 by (rtac (fin RS Fin_induct) 1); |
78 by (rtac (fin RS Fin_induct) 1); |
79 by (SIMP_TAC (Fin_ss addrews [subset_empty_iff]) 1); |
79 by (simp_tac (Fin_ss addsimps [subset_empty_iff]) 1); |
80 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1])); |
80 by (safe_tac (ZF_cs addSDs [subset_cons_iff RS iffD1])); |
81 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2); |
81 by (eres_inst_tac [("b","z")] (cons_Diff RS subst) 2); |
82 by (ALLGOALS (ASM_SIMP_TAC Fin_ss)); |
82 by (ALLGOALS (asm_simp_tac Fin_ss)); |
83 val Fin_subset = result(); |
83 val Fin_subset = result(); |
84 |
84 |
85 val major::prems = goal Fin.thy |
85 val major::prems = goal Fin.thy |
86 "[| c: Fin(A); b: Fin(A); \ |
86 "[| c: Fin(A); b: Fin(A); \ |
87 \ P(b); \ |
87 \ P(b); \ |
88 \ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
88 \ !!x y. [| x: A; y: Fin(A); x:y; P(y) |] ==> P(y-{x}) \ |
89 \ |] ==> c<=b --> P(b-c)"; |
89 \ |] ==> c<=b --> P(b-c)"; |
90 by (rtac (major RS Fin_induct) 1); |
90 by (rtac (major RS Fin_induct) 1); |
91 by (rtac (Diff_cons RS ssubst) 2); |
91 by (rtac (Diff_cons RS ssubst) 2); |
92 by (ALLGOALS (ASM_SIMP_TAC (Fin_ss addrews (prems@[Diff_0, cons_subset_iff, |
92 by (ALLGOALS (asm_simp_tac (Fin_ss addsimps (prems@[Diff_0, cons_subset_iff, |
93 Diff_subset RS Fin_subset])))); |
93 Diff_subset RS Fin_subset])))); |
94 val Fin_0_induct_lemma = result(); |
94 val Fin_0_induct_lemma = result(); |
95 |
95 |
96 val prems = goal Fin.thy |
96 val prems = goal Fin.thy |
97 "[| b: Fin(A); \ |
97 "[| b: Fin(A); \ |