52 by (Blast_tac 1); |
52 by (Blast_tac 1); |
53 qed "finite_subset"; |
53 qed "finite_subset"; |
54 |
54 |
55 Goal "finite(F Un G) = (finite F & finite G)"; |
55 Goal "finite(F Un G) = (finite F & finite G)"; |
56 by (blast_tac (claset() |
56 by (blast_tac (claset() |
57 addIs [read_instantiate [("B", "?X Un ?Y")] finite_subset, |
57 addIs [inst "B" "?X Un ?Y" finite_subset, finite_UnI]) 1); |
58 finite_UnI]) 1); |
|
59 qed "finite_Un"; |
58 qed "finite_Un"; |
60 AddIffs[finite_Un]; |
59 AddIffs[finite_Un]; |
61 |
60 |
62 Goal "finite F ==> finite(F Int G)"; |
61 (*The converse obviously fails*) |
|
62 Goal "finite F | finite G ==> finite(F Int G)"; |
63 by (blast_tac (claset() addIs [finite_subset]) 1); |
63 by (blast_tac (claset() addIs [finite_subset]) 1); |
64 qed "finite_Int1"; |
64 qed "finite_Int"; |
65 |
65 |
66 Goal "finite G ==> finite(F Int G)"; |
66 Addsimps [finite_Int]; |
67 by (blast_tac (claset() addIs [finite_subset]) 1); |
67 AddIs [finite_Int]; |
68 qed "finite_Int2"; |
|
69 |
|
70 Addsimps[finite_Int1, finite_Int2]; |
|
71 AddIs[finite_Int1, finite_Int2]; |
|
72 |
|
73 |
68 |
74 Goal "finite(insert a A) = finite A"; |
69 Goal "finite(insert a A) = finite A"; |
75 by (stac insert_is_Un 1); |
70 by (stac insert_is_Un 1); |
76 by (simp_tac (HOL_ss addsimps [finite_Un]) 1); |
71 by (simp_tac (HOL_ss addsimps [finite_Un]) 1); |
77 by (Blast_tac 1); |
72 by (Blast_tac 1); |
123 by (stac insert_Diff 1); |
118 by (stac insert_Diff 1); |
124 by (ALLGOALS Asm_full_simp_tac); |
119 by (ALLGOALS Asm_full_simp_tac); |
125 qed "finite_Diff_insert"; |
120 qed "finite_Diff_insert"; |
126 AddIffs [finite_Diff_insert]; |
121 AddIffs [finite_Diff_insert]; |
127 |
122 |
128 (* lemma merely for classical reasoner *) |
123 (*lemma merely for classical reasoner in the proof below: force_tac can't |
|
124 prove it.*) |
129 Goal "finite(A-{}) = finite A"; |
125 Goal "finite(A-{}) = finite A"; |
130 by (Simp_tac 1); |
126 by (Simp_tac 1); |
131 val lemma = result(); |
127 val lemma = result(); |
132 AddSIs [lemma RS iffD2]; |
|
133 AddSDs [lemma RS iffD1]; |
|
134 |
128 |
135 (*Lemma for proving finite_imageD*) |
129 (*Lemma for proving finite_imageD*) |
136 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
130 Goal "finite B ==> !A. f``A = B --> inj_on f A --> finite A"; |
137 by (etac finite_induct 1); |
131 by (etac finite_induct 1); |
138 by (ALLGOALS Asm_simp_tac); |
132 by (ALLGOALS Asm_simp_tac); |
139 by (Clarify_tac 1); |
133 by (Clarify_tac 1); |
140 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); |
134 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1); |
141 by (Clarify_tac 1); |
135 by (Clarify_tac 1); |
142 by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); |
136 by (full_simp_tac (simpset() addsimps [inj_on_def]) 1); |
143 by (Blast_tac 1); |
137 by (blast_tac (claset() addSDs [lemma RS iffD1]) 1); |
144 by (thin_tac "ALL A. ?PP(A)" 1); |
138 by (thin_tac "ALL A. ?PP(A)" 1); |
145 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); |
139 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1); |
146 by (Clarify_tac 1); |
140 by (Clarify_tac 1); |
147 by (res_inst_tac [("x","xa")] bexI 1); |
141 by (res_inst_tac [("x","xa")] bexI 1); |
148 by (ALLGOALS |
142 by (ALLGOALS |