33 qed "subset_imp_Diff_eq"; |
33 qed "subset_imp_Diff_eq"; |
34 |
34 |
35 goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a"; |
35 goal thy "!!c. [| c:a-b; b<a |] ==> c=b | b<c & c<a"; |
36 by (etac ltE 1); |
36 by (etac ltE 1); |
37 by (dtac Ord_linear 1); |
37 by (dtac Ord_linear 1); |
38 by (fast_tac (!claset addSIs [ltI] addIs [Ord_in_Ord]) 2); |
38 by (fast_tac (claset() addSIs [ltI] addIs [Ord_in_Ord]) 2); |
39 by (fast_tac (!claset addEs [Ord_in_Ord]) 1); |
39 by (fast_tac (claset() addEs [Ord_in_Ord]) 1); |
40 qed "Ord_DiffE"; |
40 qed "Ord_DiffE"; |
41 |
41 |
42 val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x"; |
42 val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x"; |
43 by (asm_full_simp_tac (!simpset addsimps prems) 1); |
43 by (asm_full_simp_tac (simpset() addsimps prems) 1); |
44 by (fast_tac (!claset addSDs [prem] addSEs [mem_irrefl]) 1); |
44 by (fast_tac (claset() addSDs [prem] addSEs [mem_irrefl]) 1); |
45 qed "Diff_UN_eq_self"; |
45 qed "Diff_UN_eq_self"; |
46 |
46 |
47 goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \ |
47 goal thy "!!a. x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \ |
48 \ ==> HH(f,x,a) = HH(f,x,a1)"; |
48 \ ==> HH(f,x,a) = HH(f,x,a1)"; |
49 by (resolve_tac [HH_def_satisfies_eq RS |
49 by (resolve_tac [HH_def_satisfies_eq RS |
59 by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1 |
59 by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1 |
60 THEN (assume_tac 1)); |
60 THEN (assume_tac 1)); |
61 by (res_inst_tac [("t","%z. z-?X")] subst_context 1); |
61 by (res_inst_tac [("t","%z. z-?X")] subst_context 1); |
62 by (rtac Diff_UN_eq_self 1); |
62 by (rtac Diff_UN_eq_self 1); |
63 by (dtac Ord_DiffE 1 THEN (assume_tac 1)); |
63 by (dtac Ord_DiffE 1 THEN (assume_tac 1)); |
64 by (fast_tac (!claset addEs [ltE]) 1); |
64 by (fast_tac (claset() addEs [ltE]) 1); |
65 qed "HH_is_x_gt_too"; |
65 qed "HH_is_x_gt_too"; |
66 |
66 |
67 goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}"; |
67 goal thy "!!a. [| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}"; |
68 by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
68 by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
69 by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1)); |
69 by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1)); |
70 by (dtac subst 1 THEN (assume_tac 1)); |
70 by (dtac subst 1 THEN (assume_tac 1)); |
71 by (fast_tac (!claset addSEs [mem_irrefl]) 1); |
71 by (fast_tac (claset() addSEs [mem_irrefl]) 1); |
72 qed "HH_subset_x_lt_too"; |
72 qed "HH_subset_x_lt_too"; |
73 |
73 |
74 goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \ |
74 goal thy "!!a. HH(f,x,a) : Pow(x)-{0} \ |
75 \ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}"; |
75 \ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}"; |
76 by (dresolve_tac [HH_def_satisfies_eq RS subst] 1); |
76 by (dresolve_tac [HH_def_satisfies_eq RS subst] 1); |
77 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
77 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
78 by (asm_full_simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI]) 1); |
78 by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1); |
79 by (dresolve_tac [expand_if RS iffD1] 1); |
79 by (dresolve_tac [expand_if RS iffD1] 1); |
80 by (simp_tac (!simpset setloop split_tac [expand_if] ) 1); |
80 by (simp_tac (simpset() setloop split_tac [expand_if] ) 1); |
81 by (fast_tac (subset_cs addSEs [mem_irrefl]) 1); |
81 by (fast_tac (subset_cs addSEs [mem_irrefl]) 1); |
82 qed "HH_subset_x_imp_subset_Diff_UN"; |
82 qed "HH_subset_x_imp_subset_Diff_UN"; |
83 |
83 |
84 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; |
84 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; |
85 by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); |
85 by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); |
86 by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); |
86 by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); |
87 by (dtac subst_elem 1 THEN (assume_tac 1)); |
87 by (dtac subst_elem 1 THEN (assume_tac 1)); |
88 by (fast_tac (!claset addSIs [singleton_iff RS iffD2, equals0I]) 1); |
88 by (fast_tac (claset() addSIs [singleton_iff RS iffD2, equals0I]) 1); |
89 qed "HH_eq_arg_lt"; |
89 qed "HH_eq_arg_lt"; |
90 |
90 |
91 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \ |
91 goal thy "!!x. [| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \ |
92 \ Ord(v); Ord(w) |] ==> v=w"; |
92 \ Ord(v); Ord(w) |] ==> v=w"; |
93 by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); |
93 by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); |
128 |
128 |
129 goalw thy [inj_def] |
129 goalw thy [inj_def] |
130 "(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \ |
130 "(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \ |
131 \ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"; |
131 \ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"; |
132 by (Asm_full_simp_tac 1); |
132 by (Asm_full_simp_tac 1); |
133 by (fast_tac (!claset addSIs [lam_type] addDs [less_Least_subset_x] |
133 by (fast_tac (claset() addSIs [lam_type] addDs [less_Least_subset_x] |
134 addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1); |
134 addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1); |
135 qed "lam_Least_HH_inj_Pow"; |
135 qed "lam_Least_HH_inj_Pow"; |
136 |
136 |
137 goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \ |
137 goal thy "!!x. ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \ |
138 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
138 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
143 |
143 |
144 goalw thy [surj_def] |
144 goalw thy [surj_def] |
145 "!!x. [| x - (UN a:A. F(a)) = 0; \ |
145 "!!x. [| x - (UN a:A. F(a)) = 0; \ |
146 \ ALL a:A. EX z:x. F(a) = {z} |] \ |
146 \ ALL a:A. EX z:x. F(a) = {z} |] \ |
147 \ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; |
147 \ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; |
148 by (asm_full_simp_tac (!simpset addsimps [lam_type, Diff_eq_0_iff]) 1); |
148 by (asm_full_simp_tac (simpset() addsimps [lam_type, Diff_eq_0_iff]) 1); |
149 by Safe_tac; |
149 by Safe_tac; |
150 by (set_mp_tac 1); |
150 by (set_mp_tac 1); |
151 by (deepen_tac (!claset addSIs [bexI] addSEs [equalityE]) 4 1); |
151 by (deepen_tac (claset() addSIs [bexI] addSEs [equalityE]) 4 1); |
152 qed "lam_surj_sing"; |
152 qed "lam_surj_sing"; |
153 |
153 |
154 goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0"; |
154 goal thy "!!x. y:Pow(x)-{0} ==> x ~= 0"; |
155 by (fast_tac (!claset addSIs [equals0I, singletonI RS subst_elem] |
155 by (fast_tac (claset() addSIs [equals0I, singletonI RS subst_elem] |
156 addSDs [equals0D]) 1); |
156 addSDs [equals0D]) 1); |
157 qed "not_emptyI2"; |
157 qed "not_emptyI2"; |
158 |
158 |
159 goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \ |
159 goal thy "!!f. f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \ |
160 \ ==> HH(f, x, i) : Pow(x) - {0}"; |
160 \ ==> HH(f, x, i) : Pow(x) - {0}"; |
161 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
161 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
162 by (asm_full_simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI, |
162 by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI, |
163 not_emptyI2 RS if_P]) 1); |
163 not_emptyI2 RS if_P]) 1); |
164 by (Fast_tac 1); |
164 by (Fast_tac 1); |
165 qed "f_subset_imp_HH_subset"; |
165 qed "f_subset_imp_HH_subset"; |
166 |
166 |
167 val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \ |
167 val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \ |
168 \ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"; |
168 \ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"; |
169 by (excluded_middle_tac "?P : {0}" 1); |
169 by (excluded_middle_tac "?P : {0}" 1); |
170 by (Fast_tac 2); |
170 by (Fast_tac 2); |
171 by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS |
171 by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS |
172 f_subset_imp_HH_subset] 1); |
172 f_subset_imp_HH_subset] 1); |
173 by (fast_tac (!claset addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)] |
173 by (fast_tac (claset() addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)] |
174 addSEs [mem_irrefl]) 1); |
174 addSEs [mem_irrefl]) 1); |
175 qed "f_subsets_imp_UN_HH_eq_x"; |
175 qed "f_subsets_imp_UN_HH_eq_x"; |
176 |
176 |
177 goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; |
177 goal thy "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; |
178 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
178 by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
179 by (simp_tac (!simpset addsimps [Let_def, Diff_subset RS PowI] |
179 by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI] |
180 setloop split_tac [expand_if]) 1); |
180 setloop split_tac [expand_if]) 1); |
181 qed "HH_values2"; |
181 qed "HH_values2"; |
182 |
182 |
183 goal thy |
183 goal thy |
184 "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; |
184 "!!f. HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; |
185 by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); |
185 by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); |
186 by (fast_tac (!claset addSEs [equalityE, mem_irrefl] |
186 by (fast_tac (claset() addSEs [equalityE, mem_irrefl] |
187 addSDs [singleton_subsetD]) 1); |
187 addSDs [singleton_subsetD]) 1); |
188 qed "HH_subset_imp_eq"; |
188 qed "HH_subset_imp_eq"; |
189 |
189 |
190 goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x}; \ |
190 goal thy "!!f. [| f : (Pow(x)-{0}) -> {{z}. z:x}; \ |
191 \ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; |
191 \ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; |
192 by (dtac less_Least_subset_x 1); |
192 by (dtac less_Least_subset_x 1); |
193 by (forward_tac [HH_subset_imp_eq] 1); |
193 by (forward_tac [HH_subset_imp_eq] 1); |
194 by (dtac apply_type 1); |
194 by (dtac apply_type 1); |
195 by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); |
195 by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); |
196 by (fast_tac |
196 by (fast_tac |
197 (!claset addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
197 (claset() addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
198 by (fast_tac (!claset addss (!simpset)) 1); |
198 by (fast_tac (claset() addss (simpset())) 1); |
199 qed "f_sing_imp_HH_sing"; |
199 qed "f_sing_imp_HH_sing"; |
200 |
200 |
201 goalw thy [bij_def] |
201 goalw thy [bij_def] |
202 "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ |
202 "!!f. [| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ |
203 \ f : (Pow(x)-{0}) -> {{z}. z:x} |] \ |
203 \ f : (Pow(x)-{0}) -> {{z}. z:x} |] \ |
204 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
204 \ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
205 \ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
205 \ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
206 by (fast_tac (!claset addSIs [lam_Least_HH_inj, lam_surj_sing, |
206 by (fast_tac (claset() addSIs [lam_Least_HH_inj, lam_surj_sing, |
207 f_sing_imp_HH_sing]) 1); |
207 f_sing_imp_HH_sing]) 1); |
208 qed "f_sing_lam_bij"; |
208 qed "f_sing_lam_bij"; |
209 |
209 |
210 goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \ |
210 goal thy "!!f. f: (PROD X: Pow(x)-{0}. F(X)) \ |
211 \ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})"; |
211 \ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})"; |