27 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
27 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
28 by (rtac ballI 1); |
28 by (rtac ballI 1); |
29 by (eres_inst_tac [("n","n")] natE 1); |
29 by (eres_inst_tac [("n","n")] natE 1); |
30 by (asm_simp_tac (!simpset addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
30 by (asm_simp_tac (!simpset addsimps [inj_def, succI1 RS Pi_empty2]) 1); |
31 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
31 by (fast_tac (!claset addSIs [le_imp_subset RS id_subset_inj]) 1); |
32 val nat_le_imp_lepoll_lemma = result(); |
32 qed "nat_le_imp_lepoll_lemma"; |
33 |
33 |
34 (* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*) |
34 (* used in : AC10-AC15.ML WO1-WO6.ML WO6WO1.ML*) |
35 val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard; |
35 val nat_le_imp_lepoll = nat_le_imp_lepoll_lemma RS bspec RS mp |> standard; |
36 |
36 |
37 (* ********************************************************************** *) |
37 (* ********************************************************************** *) |
38 (* lemmas concerning FOL and pure ZF theory *) |
38 (* lemmas concerning FOL and pure ZF theory *) |
39 (* ********************************************************************** *) |
39 (* ********************************************************************** *) |
40 |
40 |
41 goal thy "!!X. (A->X)=0 ==> X=0"; |
41 goal thy "!!X. (A->X)=0 ==> X=0"; |
42 by (fast_tac (!claset addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1); |
42 by (fast_tac (!claset addSIs [equals0I] addEs [lam_type RSN (2, equals0D)]) 1); |
43 val fun_space_emptyD = result(); |
43 qed "fun_space_emptyD"; |
44 |
44 |
45 (* used only in WO1_DC.ML *) |
45 (* used only in WO1_DC.ML *) |
46 (*Note simpler proof*) |
46 (*Note simpler proof*) |
47 goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \ |
47 goal ZF.thy "!!A f g. [| ALL x:A. f`x=g`x; f:Df->Cf; g:Dg->Cg; \ |
48 \ A<=Df; A<=Dg |] ==> f``A=g``A"; |
48 \ A<=Df; A<=Dg |] ==> f``A=g``A"; |
49 by (asm_simp_tac (!simpset addsimps [image_fun]) 1); |
49 by (asm_simp_tac (!simpset addsimps [image_fun]) 1); |
50 val images_eq = result(); |
50 qed "images_eq"; |
51 |
51 |
52 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
52 (* used in : AC10-AC15.ML AC16WO4.ML WO6WO1.ML *) |
53 (*I don't know where to put this one.*) |
53 (*I don't know where to put this one.*) |
54 goal Cardinal.thy |
54 goal Cardinal.thy |
55 "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
55 "!!m A B. [| A lepoll succ(m); B<=A; B~=0 |] ==> A-B lepoll m"; |
71 (* ********************************************************************** *) |
71 (* ********************************************************************** *) |
72 |
72 |
73 (* lemma for ordertype_Int *) |
73 (* lemma for ordertype_Int *) |
74 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
74 goalw Cardinal.thy [rvimage_def] "rvimage(A,id(A),r) = r Int A*A"; |
75 by (rtac equalityI 1); |
75 by (rtac equalityI 1); |
76 by (Step_tac 1); |
76 by Safe_tac; |
77 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
77 by (dres_inst_tac [("P","%a. <id(A)`xb,a>:r")] (id_conv RS subst) 1 |
78 THEN (assume_tac 1)); |
78 THEN (assume_tac 1)); |
79 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
79 by (dres_inst_tac [("P","%a. <a,ya>:r")] (id_conv RS subst) 1 |
80 THEN (REPEAT (assume_tac 1))); |
80 THEN (REPEAT (assume_tac 1))); |
81 by (fast_tac (!claset addIs [id_conv RS ssubst]) 1); |
81 by (fast_tac (!claset addIs [id_conv RS ssubst]) 1); |
82 val rvimage_id = result(); |
82 qed "rvimage_id"; |
83 |
83 |
84 (* used only in Hartog.ML *) |
84 (* used only in Hartog.ML *) |
85 goal Cardinal.thy |
85 goal Cardinal.thy |
86 "!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
86 "!!A r. well_ord(A,r) ==> ordertype(A, r Int A*A) = ordertype(A,r)"; |
87 by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] |
87 by (res_inst_tac [("P","%a. ordertype(A,a)=ordertype(A,r)")] |
88 (rvimage_id RS subst) 1); |
88 (rvimage_id RS subst) 1); |
89 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
89 by (eresolve_tac [id_bij RS bij_ordertype_vimage] 1); |
90 val ordertype_Int = result(); |
90 qed "ordertype_Int"; |
91 |
91 |
92 (* used only in AC16_lemmas.ML *) |
92 (* used only in AC16_lemmas.ML *) |
93 goalw CardinalArith.thy [InfCard_def] |
93 goalw CardinalArith.thy [InfCard_def] |
94 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
94 "!!i. [| ~Finite(i); Card(i) |] ==> InfCard(i)"; |
95 by (asm_simp_tac (!simpset addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
95 by (asm_simp_tac (!simpset addsimps [Card_is_Ord RS nat_le_infinite_Ord]) 1); |
96 val Inf_Card_is_InfCard = result(); |
96 qed "Inf_Card_is_InfCard"; |
97 |
97 |
98 goal thy "(THE z. {x}={z}) = x"; |
98 goal thy "(THE z. {x}={z}) = x"; |
99 by (fast_tac (!claset addSIs [the_equality] |
99 by (fast_tac (!claset addSIs [the_equality] |
100 addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
100 addSEs [singleton_eq_iff RS iffD1 RS sym]) 1); |
101 val the_element = result(); |
101 qed "the_element"; |
102 |
102 |
103 goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
103 goal thy "(lam x:A. {x}) : bij(A, {{x}. x:A})"; |
104 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
104 by (res_inst_tac [("d","%z. THE x. z={x}")] lam_bijective 1); |
105 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
105 by (TRYALL (eresolve_tac [RepFunI, RepFunE])); |
106 by (REPEAT (asm_full_simp_tac (!simpset addsimps [the_element]) 1)); |
106 by (REPEAT (asm_full_simp_tac (!simpset addsimps [the_element]) 1)); |
107 val lam_sing_bij = result(); |
107 qed "lam_sing_bij"; |
108 |
108 |
109 val [major,minor] = goal thy |
109 val [major,minor] = goal thy |
110 "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
110 "[| f : Pi(A,B); (!!x. x:A ==> B(x)<=C(x)) |] ==> f : Pi(A,C)"; |
111 by (fast_tac (!claset addSIs [major RS Pi_type, minor RS subsetD, |
111 by (fast_tac (!claset addSIs [major RS Pi_type, minor RS subsetD, |
112 major RS apply_type]) 1); |
112 major RS apply_type]) 1); |
113 val Pi_weaken_type = result(); |
113 qed "Pi_weaken_type"; |
114 |
114 |
115 val [major, minor] = goalw thy [inj_def] |
115 val [major, minor] = goalw thy [inj_def] |
116 "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
116 "[| f:inj(A, B); (!!a. a:A ==> f`a : C) |] ==> f:inj(A,C)"; |
117 by (fast_tac (!claset addSEs [minor] |
117 by (fast_tac (!claset addSEs [minor] |
118 addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
118 addSIs [major RS CollectD1 RS Pi_type, major RS CollectD2]) 1); |
119 val inj_strengthen_type = result(); |
119 qed "inj_strengthen_type"; |
120 |
120 |
121 goal thy "A*B=0 <-> A=0 | B=0"; |
121 goal thy "A*B=0 <-> A=0 | B=0"; |
122 by (fast_tac (!claset addSIs [equals0I] addEs [equals0D]) 1); |
122 by (fast_tac (!claset addSIs [equals0I] addEs [equals0D]) 1); |
123 val Sigma_empty_iff = result(); |
123 qed "Sigma_empty_iff"; |
124 |
124 |
125 goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; |
125 goalw thy [Finite_def] "!!n. n:nat ==> Finite(n)"; |
126 by (fast_tac (!claset addSIs [eqpoll_refl]) 1); |
126 by (fast_tac (!claset addSIs [eqpoll_refl]) 1); |
127 val nat_into_Finite = result(); |
127 qed "nat_into_Finite"; |
128 |
128 |
129 goalw thy [Finite_def] "~Finite(nat)"; |
129 goalw thy [Finite_def] "~Finite(nat)"; |
130 by (fast_tac (!claset addSDs [eqpoll_imp_lepoll] |
130 by (fast_tac (!claset addSDs [eqpoll_imp_lepoll] |
131 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
131 addIs [Ord_nat RSN (2, ltI) RS lt_not_lepoll RS notE]) 1); |
132 val nat_not_Finite = result(); |
132 qed "nat_not_Finite"; |
133 |
133 |
134 val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
134 val le_imp_lepoll = le_imp_subset RS subset_imp_lepoll; |
135 |
135 |
136 (* ********************************************************************** *) |
136 (* ********************************************************************** *) |
137 (* Another elimination rule for EX! *) |
137 (* Another elimination rule for EX! *) |
140 goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
140 goal thy "!!x. [| EX! x. P(x); P(x); P(y) |] ==> x=y"; |
141 by (etac ex1E 1); |
141 by (etac ex1E 1); |
142 by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
142 by (res_inst_tac [("b","xa")] (sym RSN (2, trans)) 1); |
143 by (Fast_tac 1); |
143 by (Fast_tac 1); |
144 by (Fast_tac 1); |
144 by (Fast_tac 1); |
145 val ex1_two_eq = result(); |
145 qed "ex1_two_eq"; |
146 |
146 |
147 (* ********************************************************************** *) |
147 (* ********************************************************************** *) |
148 (* image of a surjection *) |
148 (* image of a surjection *) |
149 (* ********************************************************************** *) |
149 (* ********************************************************************** *) |
150 |
150 |
151 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; |
151 goalw thy [surj_def] "!!f. f : surj(A, B) ==> f``A = B"; |
152 by (etac CollectE 1); |
152 by (etac CollectE 1); |
153 by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 |
153 by (resolve_tac [subset_refl RSN (2, image_fun) RS ssubst] 1 |
154 THEN (assume_tac 1)); |
154 THEN (assume_tac 1)); |
155 by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1); |
155 by (fast_tac (!claset addSEs [apply_type] addIs [equalityI]) 1); |
156 val surj_image_eq = result(); |
156 qed "surj_image_eq"; |
157 |
157 |
158 |
158 |
159 goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; |
159 goal thy "!!y. succ(x) lepoll y ==> y ~= 0"; |
160 by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1); |
160 by (fast_tac (!claset addSDs [lepoll_0_is_0]) 1); |
161 val succ_lepoll_imp_not_empty = result(); |
161 qed "succ_lepoll_imp_not_empty"; |
162 |
162 |
163 goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; |
163 goal thy "!!x. x eqpoll succ(n) ==> x ~= 0"; |
164 by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
164 by (fast_tac (!claset addSEs [eqpoll_sym RS eqpoll_0_is_0 RS succ_neq_0]) 1); |
165 val eqpoll_succ_imp_not_empty = result(); |
165 qed "eqpoll_succ_imp_not_empty"; |
166 |
166 |