author | wenzelm |
Tue, 20 Oct 1998 16:26:20 +0200 | |
changeset 5686 | 1f053d05f571 |
parent 5268 | 59ef39008514 |
child 7499 | 23e090051cb8 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/HH.ML |
1123 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1123 | 4 |
|
5 |
Some properties of the recursive definition of HH used in the proofs of |
|
6 |
AC17 ==> AC1 |
|
7 |
AC1 ==> WO2 |
|
8 |
AC15 ==> WO6 |
|
9 |
*) |
|
10 |
||
11 |
open HH; |
|
12 |
||
13 |
(* ********************************************************************** *) |
|
1461 | 14 |
(* Lemmas useful in each of the three proofs *) |
1123 | 15 |
(* ********************************************************************** *) |
16 |
||
5068 | 17 |
Goal "HH(f,x,a) = \ |
1461 | 18 |
\ (let z = x - (UN b:a. HH(f,x,b)) \ |
19 |
\ in if(f`z:Pow(z)-{0}, f`z, {x}))"; |
|
1123 | 20 |
by (resolve_tac [HH_def RS def_transrec RS trans] 1); |
2469 | 21 |
by (Simp_tac 1); |
3731 | 22 |
qed "HH_def_satisfies_eq"; |
1123 | 23 |
|
5068 | 24 |
Goal "HH(f,x,a) : Pow(x)-{0} | HH(f,x,a)={x}"; |
1123 | 25 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
5137 | 26 |
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1); |
2469 | 27 |
by (Fast_tac 1); |
3731 | 28 |
qed "HH_values"; |
1123 | 29 |
|
5137 | 30 |
Goal "B<=A ==> X-(UN a:A. P(a)) = X-(UN a:A-B. P(a))-(UN b:B. P(b))"; |
2496 | 31 |
by (Fast_tac 1); |
3731 | 32 |
qed "subset_imp_Diff_eq"; |
1123 | 33 |
|
5137 | 34 |
Goal "[| c:a-b; b<a |] ==> c=b | b<c & c<a"; |
1207 | 35 |
by (etac ltE 1); |
3731 | 36 |
by (dtac Ord_linear 1); |
4091 | 37 |
by (fast_tac (claset() addSIs [ltI] addIs [Ord_in_Ord]) 2); |
38 |
by (fast_tac (claset() addEs [Ord_in_Ord]) 1); |
|
3731 | 39 |
qed "Ord_DiffE"; |
1123 | 40 |
|
41 |
val prems = goal thy "(!!y. y:A ==> P(y) = {x}) ==> x - (UN y:A. P(y)) = x"; |
|
4091 | 42 |
by (asm_full_simp_tac (simpset() addsimps prems) 1); |
43 |
by (fast_tac (claset() addSDs [prem] addSEs [mem_irrefl]) 1); |
|
3731 | 44 |
qed "Diff_UN_eq_self"; |
1123 | 45 |
|
5137 | 46 |
Goal "x - (UN b:a. HH(f,x,b)) = x - (UN b:a1. HH(f,x,b)) \ |
1461 | 47 |
\ ==> HH(f,x,a) = HH(f,x,a1)"; |
1123 | 48 |
by (resolve_tac [HH_def_satisfies_eq RS |
1461 | 49 |
(HH_def_satisfies_eq RS sym RSN (3, trans RS trans))] 1); |
1207 | 50 |
by (etac subst_context 1); |
3731 | 51 |
qed "HH_eq"; |
1123 | 52 |
|
5137 | 53 |
Goal "[| HH(f,x,b)={x}; b<a |] ==> HH(f,x,a)={x}"; |
1123 | 54 |
by (res_inst_tac [("P","b<a")] impE 1 THEN REPEAT (assume_tac 2)); |
55 |
by (eresolve_tac [lt_Ord2 RS trans_induct] 1); |
|
1207 | 56 |
by (rtac impI 1); |
1123 | 57 |
by (resolve_tac [HH_eq RS trans] 1 THEN (assume_tac 2)); |
58 |
by (resolve_tac [leI RS le_imp_subset RS subset_imp_Diff_eq RS ssubst] 1 |
|
1461 | 59 |
THEN (assume_tac 1)); |
1123 | 60 |
by (res_inst_tac [("t","%z. z-?X")] subst_context 1); |
1207 | 61 |
by (rtac Diff_UN_eq_self 1); |
62 |
by (dtac Ord_DiffE 1 THEN (assume_tac 1)); |
|
4091 | 63 |
by (fast_tac (claset() addEs [ltE]) 1); |
3731 | 64 |
qed "HH_is_x_gt_too"; |
1123 | 65 |
|
5137 | 66 |
Goal "[| HH(f,x,a) : Pow(x)-{0}; b<a |] ==> HH(f,x,b) : Pow(x)-{0}"; |
1123 | 67 |
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
1207 | 68 |
by (dtac HH_is_x_gt_too 1 THEN (assume_tac 1)); |
69 |
by (dtac subst 1 THEN (assume_tac 1)); |
|
4091 | 70 |
by (fast_tac (claset() addSEs [mem_irrefl]) 1); |
3731 | 71 |
qed "HH_subset_x_lt_too"; |
1123 | 72 |
|
5137 | 73 |
Goal "HH(f,x,a) : Pow(x)-{0} \ |
1461 | 74 |
\ ==> HH(f,x,a) : Pow(x - (UN b:a. HH(f,x,b)))-{0}"; |
1123 | 75 |
by (dresolve_tac [HH_def_satisfies_eq RS subst] 1); |
76 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
|
4091 | 77 |
by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1); |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
5068
diff
changeset
|
78 |
by (dresolve_tac [split_if RS iffD1] 1); |
5137 | 79 |
by (Simp_tac 1); |
1200 | 80 |
by (fast_tac (subset_cs addSEs [mem_irrefl]) 1); |
3731 | 81 |
qed "HH_subset_x_imp_subset_Diff_UN"; |
1123 | 82 |
|
5137 | 83 |
Goal "[| HH(f,x,v)=HH(f,x,w); HH(f,x,v): Pow(x)-{0}; v:w |] ==> P"; |
1123 | 84 |
by (forw_inst_tac [("P","%y. y: Pow(x)-{0}")] subst 1 THEN (assume_tac 1)); |
85 |
by (dres_inst_tac [("a","w")] HH_subset_x_imp_subset_Diff_UN 1); |
|
1207 | 86 |
by (dtac subst_elem 1 THEN (assume_tac 1)); |
4091 | 87 |
by (fast_tac (claset() addSIs [singleton_iff RS iffD2, equals0I]) 1); |
3731 | 88 |
qed "HH_eq_arg_lt"; |
1123 | 89 |
|
5137 | 90 |
Goal "[| HH(f,x,v)=HH(f,x,w); HH(f,x,w): Pow(x)-{0}; \ |
1461 | 91 |
\ Ord(v); Ord(w) |] ==> v=w"; |
1123 | 92 |
by (res_inst_tac [("j","w")] Ord_linear_lt 1 THEN TRYALL assume_tac); |
93 |
by (resolve_tac [sym RS (ltD RSN (3, HH_eq_arg_lt))] 2 |
|
1461 | 94 |
THEN REPEAT (assume_tac 2)); |
1207 | 95 |
by (dtac subst_elem 1 THEN (assume_tac 1)); |
1123 | 96 |
by (fast_tac (FOL_cs addDs [ltD] addSEs [HH_eq_arg_lt]) 1); |
3731 | 97 |
qed "HH_eq_imp_arg_eq"; |
1123 | 98 |
|
5068 | 99 |
Goalw [lepoll_def, inj_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
100 |
"[| HH(f, x, i) : Pow(x)-{0}; Ord(i) |] ==> i lepoll Pow(x)-{0}"; |
1123 | 101 |
by (res_inst_tac [("x","lam j:i. HH(f, x, j)")] exI 1); |
2469 | 102 |
by (Asm_simp_tac 1); |
1123 | 103 |
by (fast_tac (FOL_cs addSEs [HH_eq_imp_arg_eq, Ord_in_Ord, HH_subset_x_lt_too] |
1461 | 104 |
addSIs [lam_type, ballI, ltI] addIs [bexI]) 1); |
3731 | 105 |
qed "HH_subset_x_imp_lepoll"; |
1123 | 106 |
|
5068 | 107 |
Goal "HH(f, x, Hartog(Pow(x)-{0})) = {x}"; |
1123 | 108 |
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 2)); |
109 |
by (fast_tac (FOL_cs addSDs [HH_subset_x_imp_lepoll] |
|
1461 | 110 |
addSIs [Ord_Hartog] addSEs [HartogE]) 1); |
3731 | 111 |
qed "HH_Hartog_is_x"; |
1123 | 112 |
|
5068 | 113 |
Goal "HH(f, x, LEAST i. HH(f, x, i) = {x}) = {x}"; |
4091 | 114 |
by (fast_tac (claset() addSIs [Ord_Hartog, HH_Hartog_is_x, LeastI]) 1); |
3731 | 115 |
qed "HH_Least_eq_x"; |
1123 | 116 |
|
5137 | 117 |
Goal "a:(LEAST i. HH(f,x,i)={x}) ==> HH(f,x,a) : Pow(x)-{0}"; |
1123 | 118 |
by (resolve_tac [HH_values RS disjE] 1 THEN (assume_tac 1)); |
1207 | 119 |
by (rtac less_LeastE 1); |
1123 | 120 |
by (eresolve_tac [Ord_Least RSN (2, ltI)] 2); |
121 |
by (assume_tac 1); |
|
3731 | 122 |
qed "less_Least_subset_x"; |
1123 | 123 |
|
124 |
(* ********************************************************************** *) |
|
1461 | 125 |
(* Lemmas used in the proofs of AC1 ==> WO2 and AC17 ==> AC1 *) |
1123 | 126 |
(* ********************************************************************** *) |
127 |
||
5068 | 128 |
Goalw [inj_def] |
1461 | 129 |
"(lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) : \ |
130 |
\ inj(LEAST i. HH(f,x,i)={x}, Pow(x)-{0})"; |
|
2469 | 131 |
by (Asm_full_simp_tac 1); |
4091 | 132 |
by (fast_tac (claset() addSIs [lam_type] addDs [less_Least_subset_x] |
1461 | 133 |
addSEs [HH_eq_imp_arg_eq, Ord_Least RS Ord_in_Ord]) 1); |
3731 | 134 |
qed "lam_Least_HH_inj_Pow"; |
1123 | 135 |
|
5137 | 136 |
Goal "ALL a:(LEAST i. HH(f,x,i)={x}). EX z:x. HH(f,x,a) = {z} \ |
1461 | 137 |
\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
138 |
\ : inj(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
|
1123 | 139 |
by (resolve_tac [lam_Least_HH_inj_Pow RS inj_strengthen_type] 1); |
2469 | 140 |
by (Asm_full_simp_tac 1); |
3731 | 141 |
qed "lam_Least_HH_inj"; |
1123 | 142 |
|
5068 | 143 |
Goalw [surj_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
144 |
"[| x - (UN a:A. F(a)) = 0; \ |
1461 | 145 |
\ ALL a:A. EX z:x. F(a) = {z} |] \ |
146 |
\ ==> (lam a:A. F(a)) : surj(A, {{y}. y:x})"; |
|
4091 | 147 |
by (asm_full_simp_tac (simpset() addsimps [lam_type, Diff_eq_0_iff]) 1); |
3731 | 148 |
by Safe_tac; |
2469 | 149 |
by (set_mp_tac 1); |
4091 | 150 |
by (deepen_tac (claset() addSIs [bexI] addSEs [equalityE]) 4 1); |
3731 | 151 |
qed "lam_surj_sing"; |
1123 | 152 |
|
5137 | 153 |
Goal "y:Pow(x)-{0} ==> x ~= 0"; |
5241 | 154 |
by Auto_tac; |
3731 | 155 |
qed "not_emptyI2"; |
1123 | 156 |
|
5137 | 157 |
Goal "f`(x - (UN j:i. HH(f,x,j))): Pow(x - (UN j:i. HH(f,x,j)))-{0} \ |
1461 | 158 |
\ ==> HH(f, x, i) : Pow(x) - {0}"; |
1123 | 159 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
4091 | 160 |
by (asm_full_simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI, |
1461 | 161 |
not_emptyI2 RS if_P]) 1); |
2469 | 162 |
by (Fast_tac 1); |
3731 | 163 |
qed "f_subset_imp_HH_subset"; |
1123 | 164 |
|
165 |
val [prem] = goal thy "(!!z. z:Pow(x)-{0} ==> f`z : Pow(z)-{0}) ==> \ |
|
1461 | 166 |
\ x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0"; |
1123 | 167 |
by (excluded_middle_tac "?P : {0}" 1); |
2469 | 168 |
by (Fast_tac 2); |
1123 | 169 |
by (dresolve_tac [Diff_subset RS PowI RS DiffI RS prem RS |
1461 | 170 |
f_subset_imp_HH_subset] 1); |
4091 | 171 |
by (fast_tac (claset() addSDs [HH_Least_eq_x RS sym RSN (2, subst_elem)] |
1461 | 172 |
addSEs [mem_irrefl]) 1); |
3731 | 173 |
qed "f_subsets_imp_UN_HH_eq_x"; |
1123 | 174 |
|
5068 | 175 |
Goal "HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j))) | HH(f,x,i)={x}"; |
1123 | 176 |
by (resolve_tac [HH_def_satisfies_eq RS ssubst] 1); |
5137 | 177 |
by (simp_tac (simpset() addsimps [Let_def, Diff_subset RS PowI]) 1); |
3731 | 178 |
qed "HH_values2"; |
1123 | 179 |
|
5268 | 180 |
Goal "HH(f,x,i): Pow(x)-{0} ==> HH(f,x,i)=f`(x - (UN j:i. HH(f,x,j)))"; |
1123 | 181 |
by (resolve_tac [HH_values2 RS disjE] 1 THEN (assume_tac 1)); |
4091 | 182 |
by (fast_tac (claset() addSEs [equalityE, mem_irrefl] |
1461 | 183 |
addSDs [singleton_subsetD]) 1); |
3731 | 184 |
qed "HH_subset_imp_eq"; |
1123 | 185 |
|
5137 | 186 |
Goal "[| f : (Pow(x)-{0}) -> {{z}. z:x}; \ |
1461 | 187 |
\ a:(LEAST i. HH(f,x,i)={x}) |] ==> EX z:x. HH(f,x,a) = {z}"; |
1207 | 188 |
by (dtac less_Least_subset_x 1); |
1123 | 189 |
by (forward_tac [HH_subset_imp_eq] 1); |
1207 | 190 |
by (dtac apply_type 1); |
1123 | 191 |
by (resolve_tac [Diff_subset RS PowI RS DiffI] 1); |
2493 | 192 |
by (fast_tac |
4091 | 193 |
(claset() addSDs [HH_subset_x_imp_subset_Diff_UN RS not_emptyI2]) 1); |
194 |
by (fast_tac (claset() addss (simpset())) 1); |
|
3731 | 195 |
qed "f_sing_imp_HH_sing"; |
1123 | 196 |
|
5068 | 197 |
Goalw [bij_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
198 |
"[| x - (UN j: (LEAST i. HH(f,x,i)={x}). HH(f,x,j)) = 0; \ |
2493 | 199 |
\ f : (Pow(x)-{0}) -> {{z}. z:x} |] \ |
1461 | 200 |
\ ==> (lam a:(LEAST i. HH(f,x,i)={x}). HH(f,x,a)) \ |
201 |
\ : bij(LEAST i. HH(f,x,i)={x}, {{y}. y:x})"; |
|
4091 | 202 |
by (fast_tac (claset() addSIs [lam_Least_HH_inj, lam_surj_sing, |
2493 | 203 |
f_sing_imp_HH_sing]) 1); |
3731 | 204 |
qed "f_sing_lam_bij"; |
1123 | 205 |
|
5137 | 206 |
Goal "f: (PROD X: Pow(x)-{0}. F(X)) \ |
1461 | 207 |
\ ==> (lam X:Pow(x)-{0}. {f`X}) : (PROD X: Pow(x)-{0}. {{z}. z:F(X)})"; |
1123 | 208 |
by (fast_tac (FOL_cs addSIs [lam_type, RepFun_eqI, singleton_eq_iff RS iffD2] |
2493 | 209 |
addDs [apply_type]) 1); |
3731 | 210 |
qed "lam_singI"; |
1123 | 211 |
|
2493 | 212 |
val bij_Least_HH_x = |
213 |
(lam_singI RSN (2, [f_sing_lam_bij, lam_sing_bij RS bij_converse_bij] |
|
214 |
MRS comp_bij)) |> standard; |