author | paulson |
Thu, 10 Sep 1998 17:42:44 +0200 | |
changeset 5470 | 855654b691db |
parent 5314 | c061e6f9d546 |
child 6021 | 4a3fc834288e |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/AC16_WO4.ML |
1200 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Krzysztof Grabczewski |
1200 | 4 |
|
5 |
The proof of AC16(n, k) ==> WO4(n-k) |
|
6 |
*) |
|
1196 | 7 |
|
8 |
open AC16_WO4; |
|
9 |
||
10 |
(* ********************************************************************** *) |
|
1461 | 11 |
(* The case of finite set *) |
1196 | 12 |
(* ********************************************************************** *) |
13 |
||
5137 | 14 |
Goalw [Finite_def] "[| Finite(A); 0<m; m:nat |] ==> \ |
1461 | 15 |
\ EX a f. Ord(a) & domain(f) = a & \ |
16 |
\ (UN b<a. f`b) = A & (ALL b<a. f`b lepoll m)"; |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
17 |
by (etac bexE 1); |
1196 | 18 |
by (dresolve_tac [eqpoll_sym RS (eqpoll_def RS def_imp_iff RS iffD1)] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
19 |
by (etac exE 1); |
1196 | 20 |
by (res_inst_tac [("x","n")] exI 1); |
21 |
by (res_inst_tac [("x","lam i:n. {f`i}")] exI 1); |
|
2469 | 22 |
by (Asm_full_simp_tac 1); |
1196 | 23 |
by (rewrite_goals_tac [bij_def, surj_def]); |
4091 | 24 |
by (fast_tac (claset() addSIs [ltI, nat_into_Ord, lam_funtype RS domain_of_fun, |
1461 | 25 |
equalityI, singleton_eqpoll_1 RS eqpoll_imp_lepoll RS lepoll_trans, |
26 |
nat_1_lepoll_iff RS iffD2] |
|
1932
cc9f1ba8f29a
Tidying: removing redundant args in classical reasoner calls
paulson
parents:
1924
diff
changeset
|
27 |
addSEs [apply_type, ltE]) 1); |
1196 | 28 |
val lemma1 = result(); |
29 |
||
30 |
(* ********************************************************************** *) |
|
1461 | 31 |
(* The case of infinite set *) |
1196 | 32 |
(* ********************************************************************** *) |
33 |
||
2167 | 34 |
(* well_ord(x,r) ==> well_ord({{y,z}. y:x}, Something(x,z)) **) |
3731 | 35 |
bind_thm ("well_ord_paired", (paired_bij RS bij_is_inj RS well_ord_rvimage)); |
1196 | 36 |
|
5137 | 37 |
Goal "[| A lepoll B; ~ A lepoll C |] ==> ~ B lepoll C"; |
4091 | 38 |
by (fast_tac (claset() addEs [notE, lepoll_trans]) 1); |
3731 | 39 |
qed "lepoll_trans1"; |
1196 | 40 |
|
41 |
(* ********************************************************************** *) |
|
1461 | 42 |
(* There exists a well ordered set y such that ... *) |
1196 | 43 |
(* ********************************************************************** *) |
44 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
45 |
val lepoll_paired = paired_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
46 |
|
5068 | 47 |
Goal "EX y R. well_ord(y,R) & x Int y = 0 & ~y lepoll z & ~Finite(y)"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
48 |
by (res_inst_tac [("x","{{a,x}. a:nat Un Hartog(z)}")] exI 1); |
3891 | 49 |
by (resolve_tac [transfer thy Ord_nat RS well_ord_Memrel RS (Ord_Hartog RS |
1461 | 50 |
well_ord_Memrel RSN (2, well_ord_Un)) RS exE] 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
51 |
by (fast_tac |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
52 |
(claset() addSIs [Ord_Hartog, well_ord_Memrel, well_ord_paired, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
53 |
HartogI RSN (2, lepoll_trans1), |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
54 |
subset_imp_lepoll RS (lepoll_paired RSN (2, lepoll_trans))] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
55 |
addSEs [nat_not_Finite RS notE] addEs [mem_asym] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
56 |
addSDs [Un_upper1 RS subset_imp_lepoll RS lepoll_Finite, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
57 |
lepoll_paired RS lepoll_Finite]) 1); |
1196 | 58 |
val lemma2 = result(); |
59 |
||
60 |
val [prem] = goal thy "~Finite(B) ==> ~Finite(A Un B)"; |
|
4091 | 61 |
by (fast_tac (claset() |
1461 | 62 |
addSIs [subset_imp_lepoll RS (prem RSN (2, lepoll_infinite))]) 1); |
3731 | 63 |
qed "infinite_Un"; |
1196 | 64 |
|
65 |
(* ********************************************************************** *) |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
66 |
(* There is a v : s(u) such that k lepoll x Int y (in our case succ(k)) *) |
1461 | 67 |
(* The idea of the proof is the following : *) |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
68 |
(* Suppose not, i.e. every element of s(u) has exactly k-1 elements of y *) |
1461 | 69 |
(* Thence y is less than or equipollent to {v:Pow(x). v eqpoll n#-k} *) |
70 |
(* We have obtained this result in two steps : *) |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
71 |
(* 1. y is less than or equipollent to {v:s(u). a <= v} *) |
1461 | 72 |
(* where a is certain k-2 element subset of y *) |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
73 |
(* 2. {v:s(u). a <= v} is less than or equipollent *) |
1461 | 74 |
(* to {v:Pow(x). v eqpoll n-k} *) |
1196 | 75 |
(* ********************************************************************** *) |
76 |
||
1710 | 77 |
(*Proof simplified by LCP*) |
5137 | 78 |
Goal "[| ~(EX x:A. f`x=y); f : inj(A, B); y:B |] \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
79 |
\ ==> (lam a:succ(A). if(a=A, y, f`a)) : inj(succ(A), B)"; |
1196 | 80 |
by (res_inst_tac [("d","%z. if(z=y, A, converse(f)`z)")] lam_injective 1); |
1710 | 81 |
by (ALLGOALS |
82 |
(asm_simp_tac |
|
4091 | 83 |
(simpset() addsimps [inj_is_fun RS apply_type, left_inverse] |
5116
8eb343ab5748
Renamed expand_if to split_if and setloop split_tac to addsplits,
paulson
parents:
5068
diff
changeset
|
84 |
setloop (split_tac [split_if] ORELSE' Step_tac)))); |
3731 | 85 |
qed "succ_not_lepoll_lemma"; |
1196 | 86 |
|
5068 | 87 |
Goalw [lepoll_def, eqpoll_def, bij_def, surj_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
88 |
"[| ~A eqpoll B; A lepoll B |] ==> succ(A) lepoll B"; |
4091 | 89 |
by (fast_tac (claset() addSEs [succ_not_lepoll_lemma, inj_is_fun]) 1); |
3731 | 90 |
qed "succ_not_lepoll_imp_eqpoll"; |
1196 | 91 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
92 |
|
1196 | 93 |
(* ********************************************************************** *) |
1461 | 94 |
(* There is a k-2 element subset of y *) |
1196 | 95 |
(* ********************************************************************** *) |
96 |
||
5068 | 97 |
Goalw [lepoll_def, eqpoll_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
98 |
"[| n:nat; nat lepoll X |] ==> EX Y. Y<=X & n eqpoll Y"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
99 |
by (fast_tac (subset_cs addSDs [Ord_nat RSN (2, OrdmemD) RSN (2, restrict_inj)] |
1461 | 100 |
addSEs [restrict_bij, inj_is_fun RS fun_is_rel RS image_subset]) 1); |
3731 | 101 |
qed "nat_lepoll_imp_ex_eqpoll_n"; |
1196 | 102 |
|
103 |
val ordertype_eqpoll = |
|
1461 | 104 |
ordermap_bij RS (exI RS (eqpoll_def RS def_imp_iff RS iffD2)); |
1196 | 105 |
|
5137 | 106 |
Goalw [lesspoll_def] "n: nat ==> n lesspoll nat"; |
4091 | 107 |
by (fast_tac (claset() addSEs [Ord_nat RSN (2, ltI) RS leI RS le_imp_lepoll, |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
108 |
eqpoll_sym RS eqpoll_imp_lepoll] |
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
109 |
addIs [Ord_nat RSN (2, nat_succI RS ltI) RS leI |
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
110 |
RS le_imp_lepoll RS lepoll_trans RS succ_lepoll_natE]) 1); |
3731 | 111 |
qed "n_lesspoll_nat"; |
1196 | 112 |
|
5137 | 113 |
Goal "[| a<=y; b:y-a; u:x |] ==> cons(b, cons(u, a)) : Pow(x Un y)"; |
2469 | 114 |
by (Fast_tac 1); |
3731 | 115 |
qed "cons_cons_subset"; |
1196 | 116 |
|
5137 | 117 |
Goal "[| a eqpoll k; a<=y; b:y-a; u:x; x Int y = 0 \ |
1461 | 118 |
\ |] ==> cons(b, cons(u, a)) eqpoll succ(succ(k))"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
119 |
by (fast_tac (claset() addSIs [cons_eqpoll_succ]) 1); |
3731 | 120 |
qed "cons_cons_eqpoll"; |
1196 | 121 |
|
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
122 |
Goal "[| succ(k) eqpoll A; k eqpoll B; B <= A; a : A-B; k:nat \ |
1461 | 123 |
\ |] ==> A = cons(a, B)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
124 |
by (rtac equalityI 1); |
2469 | 125 |
by (Fast_tac 2); |
1196 | 126 |
by (resolve_tac [Diff_eq_0_iff RS iffD1] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
127 |
by (rtac equals0I 1); |
1196 | 128 |
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); |
129 |
by (dresolve_tac [eqpoll_sym RS cons_eqpoll_succ] 1); |
|
2469 | 130 |
by (Fast_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
131 |
by (dtac cons_eqpoll_succ 1); |
2469 | 132 |
by (Fast_tac 1); |
5137 | 133 |
by (fast_tac |
134 |
(claset() |
|
1461 | 135 |
addSEs [[eqpoll_sym RS eqpoll_imp_lepoll, subset_imp_lepoll] MRS |
136 |
(lepoll_trans RS lepoll_trans) RS succ_lepoll_natE]) 1); |
|
3731 | 137 |
qed "set_eq_cons"; |
1196 | 138 |
|
5137 | 139 |
Goal "[| cons(x,a) = cons(y,a); x~: a |] ==> x = y "; |
4091 | 140 |
by (fast_tac (claset() addSEs [equalityE]) 1); |
3731 | 141 |
qed "cons_eqE"; |
1196 | 142 |
|
5137 | 143 |
Goal "A = B ==> A Int C = B Int C"; |
2469 | 144 |
by (Asm_simp_tac 1); |
3731 | 145 |
qed "eq_imp_Int_eq"; |
1196 | 146 |
|
147 |
(* ********************************************************************** *) |
|
1461 | 148 |
(* some arithmetic *) |
1196 | 149 |
(* ********************************************************************** *) |
150 |
||
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
151 |
Goal "[| k:nat; m:nat |] ==> \ |
1461 | 152 |
\ ALL A B. A eqpoll k #+ m & k lepoll B & B<=A --> A-B lepoll m"; |
1196 | 153 |
by (eres_inst_tac [("n","k")] nat_induct 1); |
4091 | 154 |
by (simp_tac (simpset() addsimps [add_0]) 1); |
155 |
by (fast_tac (claset() addIs [eqpoll_imp_lepoll RS |
|
1461 | 156 |
(Diff_subset RS subset_imp_lepoll RS lepoll_trans)]) 1); |
1196 | 157 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
158 |
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
2469 | 159 |
by (Fast_tac 1); |
1196 | 160 |
by (eres_inst_tac [("x","A - {xa}")] allE 1); |
161 |
by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
162 |
by (etac impE 1); |
4091 | 163 |
by (asm_full_simp_tac (simpset() addsimps [add_succ]) 1); |
164 |
by (fast_tac (claset() addSIs [Diff_sing_eqpoll, lepoll_Diff_sing]) 1); |
|
1196 | 165 |
by (res_inst_tac [("P","%z. z lepoll m")] subst 1 THEN (assume_tac 2)); |
2496 | 166 |
by (Fast_tac 1); |
3731 | 167 |
qed "eqpoll_sum_imp_Diff_lepoll_lemma"; |
1196 | 168 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
169 |
Goal "[| A eqpoll succ(k #+ m); B<=A; succ(k) lepoll B; k:nat; m:nat |] \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
170 |
\ ==> A-B lepoll m"; |
1196 | 171 |
by (dresolve_tac [add_succ RS ssubst] 1); |
172 |
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_lepoll_lemma] 1 |
|
1461 | 173 |
THEN (REPEAT (assume_tac 1))); |
2469 | 174 |
by (Fast_tac 1); |
3731 | 175 |
qed "eqpoll_sum_imp_Diff_lepoll"; |
1196 | 176 |
|
177 |
(* ********************************************************************** *) |
|
1461 | 178 |
(* similar properties for eqpoll *) |
1196 | 179 |
(* ********************************************************************** *) |
180 |
||
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
181 |
Goal "[| k:nat; m:nat |] ==> \ |
1461 | 182 |
\ ALL A B. A eqpoll k #+ m & k eqpoll B & B<=A --> A-B eqpoll m"; |
1196 | 183 |
by (eres_inst_tac [("n","k")] nat_induct 1); |
4091 | 184 |
by (fast_tac (claset() addSDs [eqpoll_sym RS eqpoll_imp_lepoll RS lepoll_0_is_0] |
185 |
addss (simpset() addsimps [add_0])) 1); |
|
1196 | 186 |
by (REPEAT (resolve_tac [allI,impI] 1)); |
187 |
by (resolve_tac [succ_lepoll_imp_not_empty RS not_emptyE] 1); |
|
4091 | 188 |
by (fast_tac (claset() addSEs [eqpoll_imp_lepoll]) 1); |
1196 | 189 |
by (eres_inst_tac [("x","A - {xa}")] allE 1); |
190 |
by (eres_inst_tac [("x","B - {xa}")] allE 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
191 |
by (etac impE 1); |
4091 | 192 |
by (fast_tac (claset() addSIs [Diff_sing_eqpoll, |
1461 | 193 |
eqpoll_sym RSN (2, Diff_sing_eqpoll) RS eqpoll_sym] |
4091 | 194 |
addss (simpset() addsimps [add_succ])) 1); |
1196 | 195 |
by (res_inst_tac [("P","%z. z eqpoll m")] subst 1 THEN (assume_tac 2)); |
2496 | 196 |
by (Fast_tac 1); |
3731 | 197 |
qed "eqpoll_sum_imp_Diff_eqpoll_lemma"; |
1196 | 198 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
199 |
Goal "[| A eqpoll succ(k #+ m); B<=A; succ(k) eqpoll B; k:nat; m:nat |] \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
200 |
\ ==> A-B eqpoll m"; |
1196 | 201 |
by (dresolve_tac [add_succ RS ssubst] 1); |
202 |
by (dresolve_tac [nat_succI RS eqpoll_sum_imp_Diff_eqpoll_lemma] 1 |
|
1461 | 203 |
THEN (REPEAT (assume_tac 1))); |
2469 | 204 |
by (Fast_tac 1); |
3731 | 205 |
qed "eqpoll_sum_imp_Diff_eqpoll"; |
1196 | 206 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
207 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
208 |
(* ********************************************************************** *) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
209 |
(* LL can be well ordered *) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
210 |
(* ********************************************************************** *) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
211 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
212 |
Goal "{x:Pow(X). x lepoll 0} = {0}"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
213 |
by (fast_tac (claset() addSDs [lepoll_0_is_0] addSIs [lepoll_refl]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
214 |
qed "subsets_lepoll_0_eq_unit"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
215 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
216 |
Goal "n:nat ==> {z:Pow(y). z lepoll succ(n)} = \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
217 |
\ {z:Pow(y). z lepoll n} Un {z:Pow(y). z eqpoll succ(n)}"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
218 |
by (fast_tac (claset() addIs [le_refl, leI, le_imp_lepoll] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
219 |
addSDs [lepoll_succ_disj] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
220 |
addSEs [nat_into_Ord, lepoll_trans, eqpoll_imp_lepoll]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
221 |
qed "subsets_lepoll_succ"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
222 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
223 |
Goal "n:nat ==> {z:Pow(y). z lepoll n} Int {z:Pow(y). z eqpoll succ(n)} = 0"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
224 |
by (fast_tac (claset() addSEs [eqpoll_sym RS eqpoll_imp_lepoll |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
225 |
RS lepoll_trans RS succ_lepoll_natE] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
226 |
addSIs [equals0I]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
227 |
qed "Int_empty"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
228 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
229 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
230 |
Open_locale "AC16"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
231 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
232 |
val all_ex = thm "all_ex"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
233 |
val disjoint = thm "disjoint"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
234 |
val includes = thm "includes"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
235 |
val WO_R = thm "WO_R"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
236 |
val k_def = thm "k_def"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
237 |
val lnat = thm "lnat"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
238 |
val mnat = thm "mnat"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
239 |
val mpos = thm "mpos"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
240 |
val Infinite = thm "Infinite"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
241 |
val noLepoll = thm "noLepoll"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
242 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
243 |
val LL_def = thm "LL_def"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
244 |
val MM_def = thm "MM_def"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
245 |
val GG_def = thm "GG_def"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
246 |
val s_def = thm "s_def"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
247 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
248 |
Addsimps [disjoint, WO_R, lnat, mnat, mpos, Infinite]; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
249 |
AddSIs [disjoint, WO_R, lnat, mnat, mpos]; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
250 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
251 |
Goalw [k_def] "k: nat"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
252 |
by Auto_tac; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
253 |
qed "knat"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
254 |
Addsimps [knat]; AddSIs [knat]; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
255 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
256 |
AddSIs [Infinite]; (*if notI is removed!*) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
257 |
AddSEs [Infinite RS notE]; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
258 |
|
5470 | 259 |
AddEs [[disjoint, IntI] MRS (equals0D RS notE)]; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
260 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
261 |
(*use k = succ(l) *) |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
262 |
val includes_l = simplify (FOL_ss addsimps [k_def]) includes; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
263 |
val all_ex_l = simplify (FOL_ss addsimps [k_def]) all_ex; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
264 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
265 |
(* ********************************************************************** *) |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
266 |
(* 1. y is less than or equipollent to {v:s(u). a <= v} *) |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
267 |
(* where a is certain k-2 element subset of y *) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
268 |
(* ********************************************************************** *) |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
269 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
270 |
Goal "[| l eqpoll a; a <= y |] ==> y - a eqpoll y"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
271 |
by (cut_facts_tac [WO_R, Infinite, lnat] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
272 |
by (fast_tac (empty_cs addIs [lepoll_lesspoll_lesspoll] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
273 |
addSIs [Card_cardinal, Diff_lesspoll_eqpoll_Card RS eqpoll_trans, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
274 |
Card_cardinal RS Card_is_Ord RS nat_le_infinite_Ord |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
275 |
RS le_imp_lepoll] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
276 |
addSEs [well_ord_cardinal_eqpoll, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
277 |
well_ord_cardinal_eqpoll RS eqpoll_sym, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
278 |
eqpoll_sym RS eqpoll_imp_lepoll, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
279 |
n_lesspoll_nat RS lesspoll_lepoll_lesspoll, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
280 |
well_ord_cardinal_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
281 |
RS lepoll_infinite]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
282 |
qed "Diff_Finite_eqpoll"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
283 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
284 |
Goalw [s_def] "s(u) <= t_n"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
285 |
by (Fast_tac 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
286 |
qed "s_subset"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
287 |
|
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
288 |
Goalw [s_def, succ_def, k_def] |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
289 |
"[| w:t_n; cons(b,cons(u,a)) <= w; a <= y; b : y-a; l eqpoll a \ |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
290 |
\ |] ==> w: s(u)"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
291 |
by (fast_tac (claset() addDs [eqpoll_imp_lepoll RS cons_lepoll_cong] |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
292 |
addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
293 |
qed "sI"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
294 |
|
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
295 |
Goalw [s_def] "v : s(u) ==> u : v"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
296 |
by (Fast_tac 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
297 |
qed "in_s_imp_u_in"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
298 |
|
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
299 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
300 |
Goal "[| l eqpoll a; a <= y; b : y - a; u : x |] \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
301 |
\ ==> EX! c. c: s(u) & a <= c & b:c"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
302 |
by (rtac (all_ex_l RS ballE) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
303 |
by (blast_tac (claset() delrules [PowI] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
304 |
addSIs [cons_cons_subset, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
305 |
eqpoll_sym RS cons_cons_eqpoll]) 2); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
306 |
by (etac ex1E 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
307 |
by (res_inst_tac [("a","w")] ex1I 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
308 |
by (blast_tac (claset() addIs [sI]) 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
309 |
by (etac allE 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
310 |
by (etac impE 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
311 |
by (assume_tac 2); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
312 |
by (fast_tac (claset() addSEs [s_subset RS subsetD, in_s_imp_u_in]) 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
313 |
qed "ex1_superset_a"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
314 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
315 |
Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
316 |
\ l eqpoll a; a <= y; b : y - a; u : x |] \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
317 |
\ ==> (THE c. c: s(u) & a <= c & b:c) \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
318 |
\ Int y = cons(b, a)"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
319 |
by (forward_tac [ex1_superset_a RS theI] 1 THEN REPEAT (assume_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
320 |
by (rtac set_eq_cons 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
321 |
by (REPEAT (Fast_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
322 |
qed "the_eq_cons"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
323 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
324 |
Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
325 |
\ l eqpoll a; a <= y; u:x |] \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
326 |
\ ==> y lepoll {v:s(u). a <= v}"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
327 |
by (resolve_tac [Diff_Finite_eqpoll RS eqpoll_sym RS |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
328 |
eqpoll_imp_lepoll RS lepoll_trans] 1 |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
329 |
THEN REPEAT (Fast_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
330 |
by (res_inst_tac |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
331 |
[("f3", "lam b:y-a. THE c. c: s(u) & a <= c & b:c")] |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
332 |
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
333 |
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
334 |
by (rtac CollectI 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
335 |
by (rtac lam_type 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
336 |
by (forward_tac [ex1_superset_a RS theI] 1 |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
337 |
THEN REPEAT (Fast_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
338 |
by (Asm_simp_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
339 |
by (Clarify_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
340 |
by (rtac cons_eqE 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
341 |
by (Fast_tac 2); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
342 |
by (dres_inst_tac [("A","THE c. ?P(c)"), ("C","y")] eq_imp_Int_eq 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
343 |
by (asm_full_simp_tac (simpset() addsimps [the_eq_cons]) 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
344 |
qed "y_lepoll_subset_s"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
345 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
346 |
|
1196 | 347 |
(* ********************************************************************** *) |
1461 | 348 |
(* back to the second part *) |
1196 | 349 |
(* ********************************************************************** *) |
350 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
351 |
Goal "w <= x Un y ==> w Int (x - {u}) = w - cons(u, w Int y)"; |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
352 |
by (Fast_tac 1); |
3731 | 353 |
qed "w_Int_eq_w_Diff"; |
1196 | 354 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
355 |
Goal "[| w:{v:s(u). a <= v}; \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
356 |
\ l eqpoll a; u : x; \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
357 |
\ ALL v:s(u). succ(l) eqpoll v Int y \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
358 |
\ |] ==> w Int (x - {u}) eqpoll m"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
359 |
by (etac CollectE 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
360 |
by (stac w_Int_eq_w_Diff 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
361 |
by (fast_tac (claset() addSDs [s_subset RS subsetD, |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
362 |
includes_l RS subsetD]) 1); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
363 |
by (fast_tac (claset() addSDs [bspec] |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
364 |
addDs [s_subset RS subsetD, includes_l RS subsetD] |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
365 |
addSEs [eqpoll_sym RS cons_eqpoll_succ RS eqpoll_sym, in_s_imp_u_in] |
5137 | 366 |
addSIs [eqpoll_sum_imp_Diff_eqpoll]) 1); |
3731 | 367 |
qed "w_Int_eqpoll_m"; |
1196 | 368 |
|
369 |
(* ********************************************************************** *) |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
370 |
(* 2. {v:s(u). a <= v} is less than or equipollent *) |
1461 | 371 |
(* to {v:Pow(x). v eqpoll n-k} *) |
1196 | 372 |
(* ********************************************************************** *) |
373 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
374 |
Goal "x eqpoll m ==> x ~= 0"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
375 |
by (cut_facts_tac [mpos] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
376 |
by (fast_tac (claset() addSEs [zero_lt_natE] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
377 |
addSDs [eqpoll_succ_imp_not_empty]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
378 |
qed "eqpoll_m_not_empty"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
379 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
380 |
Goal "[| z : xa Int (x - {u}); l eqpoll a; a <= y; u:x |] \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
381 |
\ ==> EX! w. w : t_n & cons(z, cons(u, a)) <= w"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
382 |
by (rtac (all_ex RS bspec) 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
383 |
by (rewtac k_def); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
384 |
by (fast_tac (claset() addSIs [cons_eqpoll_succ] addEs [eqpoll_sym]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
385 |
qed "cons_cons_in"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
386 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
387 |
Goal "[| ALL v:s(u). succ(l) eqpoll v Int y; \ |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
388 |
\ a <= y; l eqpoll a; u : x |] \ |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
389 |
\ ==> {v:s(u). a <= v} lepoll {v:Pow(x). v eqpoll m}"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
390 |
by (res_inst_tac [("f3","lam w:{v:s(u). a <= v}. w Int (x - {u})")] |
1461 | 391 |
(exI RS (lepoll_def RS def_imp_iff RS iffD2)) 1); |
1196 | 392 |
by (resolve_tac [inj_def RS def_imp_eq RS ssubst] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
393 |
by (rtac CollectI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
394 |
by (rtac lam_type 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
395 |
by (rtac CollectI 1); |
2469 | 396 |
by (Fast_tac 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
397 |
by (rtac w_Int_eqpoll_m 1 THEN REPEAT (assume_tac 1)); |
4091 | 398 |
by (simp_tac (simpset() delsimps ball_simps) 1); |
1196 | 399 |
by (REPEAT (resolve_tac [ballI, impI] 1)); |
2483
95c2f9c0930a
Default rewrite rules for quantification over Collect(A,P)
paulson
parents:
2469
diff
changeset
|
400 |
(** LEVEL 9 **) |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
401 |
by (resolve_tac [w_Int_eqpoll_m RS eqpoll_m_not_empty RS not_emptyE] 1 |
1461 | 402 |
THEN REPEAT (assume_tac 1)); |
1196 | 403 |
by (dresolve_tac [equalityD1 RS subsetD] 1 THEN (assume_tac 1)); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
404 |
by (forward_tac [cons_cons_in] 1 THEN REPEAT (assume_tac 1)); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
405 |
by (etac ex1_two_eq 1); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
406 |
by (REPEAT (blast_tac |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
407 |
(claset() addDs [s_subset RS subsetD, in_s_imp_u_in]) 1)); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
408 |
qed "subset_s_lepoll_w"; |
1196 | 409 |
|
410 |
||
411 |
(* ********************************************************************** *) |
|
1461 | 412 |
(* well_ord_subsets_lepoll_n *) |
1196 | 413 |
(* ********************************************************************** *) |
414 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
415 |
Goal "n:nat ==> EX S. well_ord({z: Pow(y) . z eqpoll succ(n)}, S)"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
416 |
by (resolve_tac [WO_R RS well_ord_infinite_subsets_eqpoll_X |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
417 |
RS (eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
418 |
by (REPEAT (fast_tac (claset() addIs [bij_is_inj RS well_ord_rvimage]) 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
419 |
qed "well_ord_subsets_eqpoll_n"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
420 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
421 |
Goal "n:nat ==> EX R. well_ord({z:Pow(y). z lepoll n}, R)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
422 |
by (etac nat_induct 1); |
4091 | 423 |
by (fast_tac (claset() addSIs [well_ord_unit] |
424 |
addss (simpset() addsimps [subsets_lepoll_0_eq_unit])) 1); |
|
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
425 |
by (etac exE 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
426 |
by (resolve_tac [well_ord_subsets_eqpoll_n RS exE] 1 THEN assume_tac 1); |
4091 | 427 |
by (asm_simp_tac (simpset() addsimps [subsets_lepoll_succ]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
428 |
by (dtac well_ord_radd 1 THEN (assume_tac 1)); |
1196 | 429 |
by (eresolve_tac [Int_empty RS disj_Un_eqpoll_sum RS |
1461 | 430 |
(eqpoll_def RS def_imp_iff RS iffD1) RS exE] 1); |
4091 | 431 |
by (fast_tac (claset() addSEs [bij_is_inj RS well_ord_rvimage]) 1); |
3731 | 432 |
qed "well_ord_subsets_lepoll_n"; |
1196 | 433 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
434 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
435 |
Goalw [LL_def, MM_def] "LL <= {z:Pow(y). z lepoll succ(k #+ m)}"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
436 |
by (cut_facts_tac [includes] 1); |
5241 | 437 |
by (fast_tac (claset() addIs [subset_imp_lepoll |
438 |
RS (eqpoll_imp_lepoll |
|
439 |
RSN (2, lepoll_trans))]) 1); |
|
3731 | 440 |
qed "LL_subset"; |
1196 | 441 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
442 |
Goal "EX S. well_ord(LL,S)"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
443 |
by (rtac (well_ord_subsets_lepoll_n RS exE) 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
444 |
by (blast_tac (claset() addIs [LL_subset RSN (2, well_ord_subset)]) 2); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
445 |
by Auto_tac; |
3731 | 446 |
qed "well_ord_LL"; |
1196 | 447 |
|
448 |
(* ********************************************************************** *) |
|
1461 | 449 |
(* every element of LL is a contained in exactly one element of MM *) |
1196 | 450 |
(* ********************************************************************** *) |
451 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
452 |
Goalw [MM_def, LL_def] "v:LL ==> EX! w. w:MM & v<=w"; |
5241 | 453 |
by Safe_tac; |
2845 | 454 |
by (Fast_tac 1); |
1196 | 455 |
by (resolve_tac [lepoll_imp_eqpoll_subset RS exE] 1 THEN (assume_tac 1)); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
456 |
by (res_inst_tac [("x","x")] (all_ex RS ballE) 1); |
4091 | 457 |
by (fast_tac (claset() addSEs [eqpoll_sym]) 2); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
458 |
by (Blast_tac 1); |
3731 | 459 |
qed "unique_superset_in_MM"; |
1196 | 460 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
461 |
val unique_superset1 = unique_superset_in_MM RS theI RS conjunct1; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
462 |
val unique_superset2 = unique_superset_in_MM RS the_equality2; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
463 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
464 |
|
1196 | 465 |
(* ********************************************************************** *) |
1461 | 466 |
(* The function GG satisfies the conditions of WO4 *) |
1196 | 467 |
(* ********************************************************************** *) |
468 |
||
469 |
(* ********************************************************************** *) |
|
1461 | 470 |
(* The union of appropriate values is the whole x *) |
1196 | 471 |
(* ********************************************************************** *) |
472 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
473 |
Goalw [LL_def] "w : MM ==> w Int y : LL"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
474 |
by (Fast_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
475 |
qed "Int_in_LL"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
476 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
477 |
Goalw [LL_def] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
478 |
"v : LL ==> v = (THE x. x : MM & v <= x) Int y"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
479 |
by (Clarify_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
480 |
by (stac unique_superset2 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
481 |
by (auto_tac (claset(), simpset() addsimps [Int_in_LL])); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
482 |
qed "in_LL_eq_Int"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
483 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
484 |
Goal "v : LL ==> (THE x. x : MM & v <= x) <= x Un y"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
485 |
by (dtac unique_superset1 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
486 |
by (rewtac MM_def); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
487 |
by (fast_tac (claset() addSDs [unique_superset1, includes RS subsetD]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
488 |
qed "the_in_MM_subset"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
489 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
490 |
Goalw [GG_def] "v : LL ==> GG ` v <= x"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
491 |
by (forward_tac [the_in_MM_subset] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
492 |
by (forward_tac [in_LL_eq_Int] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
493 |
by (force_tac (claset() addEs [equalityE], simpset()) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
494 |
qed "GG_subset"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
495 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
496 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
497 |
Goal "n:nat ==> EX z. z<=y & n eqpoll z"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
498 |
by (etac nat_lepoll_imp_ex_eqpoll_n 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
499 |
by (resolve_tac [ordertype_eqpoll RS eqpoll_sym RS eqpoll_imp_lepoll |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
500 |
RSN (2, lepoll_trans)] 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
501 |
by (rtac WO_R 2); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
502 |
by (fast_tac |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
503 |
(claset() delrules [notI] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
504 |
addSIs [nat_le_infinite_Ord RS le_imp_lepoll] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
505 |
addIs [Ord_ordertype, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
506 |
ordertype_eqpoll RS eqpoll_imp_lepoll |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
507 |
RS lepoll_infinite]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
508 |
qed "ex_subset_eqpoll_n"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
509 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
510 |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
511 |
Goal "u:x ==> EX v : s(u). succ(k) lepoll v Int y"; |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
512 |
by (rtac ccontr 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
513 |
by (subgoal_tac "ALL v:s(u). k eqpoll v Int y" 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
514 |
by (full_simp_tac (simpset() addsimps [s_def]) 2); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
515 |
by (blast_tac (claset() addIs [succ_not_lepoll_imp_eqpoll]) 2); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
516 |
by (rewtac k_def); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
517 |
by (cut_facts_tac [all_ex, includes, lnat] 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
518 |
by (rtac (ex_subset_eqpoll_n RS exE) 1 THEN assume_tac 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
519 |
by (rtac (noLepoll RS notE) 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
520 |
by (blast_tac (claset() addIs |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
521 |
[[y_lepoll_subset_s, subset_s_lepoll_w] MRS lepoll_trans]) 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
522 |
qed "exists_proper_in_s"; |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
523 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
524 |
Goal "u:x ==> EX w:MM. u:w"; |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
525 |
by (eresolve_tac [exists_proper_in_s RS bexE] 1); |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
526 |
by (rewrite_goals_tac [MM_def, s_def]); |
2469 | 527 |
by (Fast_tac 1); |
3731 | 528 |
qed "exists_in_MM"; |
1196 | 529 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
530 |
Goal "u:x ==> EX w:LL. u:GG`w"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
531 |
by (rtac (exists_in_MM RS bexE) 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
532 |
by (assume_tac 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
533 |
by (rtac bexI 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
534 |
by (etac Int_in_LL 2); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
535 |
by (rewtac GG_def); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
536 |
by (asm_simp_tac (simpset() addsimps [Int_in_LL]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
537 |
by (stac unique_superset2 1); |
5265
9d1d4c43c76d
Disjointness reasoning by AddEs [equals0E, sym RS equals0E]
paulson
parents:
5241
diff
changeset
|
538 |
by (REPEAT (fast_tac (claset() addSEs [Int_in_LL]) 1)); |
3731 | 539 |
qed "exists_in_LL"; |
1196 | 540 |
|
541 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
542 |
Goal "well_ord(LL,S) ==> \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
543 |
\ (UN b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)) = x"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
544 |
by (rtac equalityI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
545 |
by (rtac subsetI 1); |
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
546 |
by (etac OUN_E 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
547 |
by (resolve_tac [GG_subset RS subsetD] 1); |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
548 |
by (assume_tac 2); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
549 |
by (blast_tac (claset() addIs [ordermap_bij RS bij_converse_bij RS |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
550 |
bij_is_fun RS apply_type, ltD]) 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
551 |
by (rtac subsetI 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
552 |
by (eresolve_tac [exists_in_LL RS bexE] 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
553 |
by (force_tac (claset() addIs [Ord_ordertype RSN (2, ltI), |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
554 |
ordermap_type RS apply_type], |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
555 |
simpset() addsimps [ordermap_bij RS bij_is_inj RS left_inverse]) 1); |
3731 | 556 |
qed "OUN_eq_x"; |
1196 | 557 |
|
558 |
(* ********************************************************************** *) |
|
1461 | 559 |
(* Every element of the family is less than or equipollent to n-k (m) *) |
1196 | 560 |
(* ********************************************************************** *) |
561 |
||
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
562 |
Goalw [MM_def] "w : MM ==> w eqpoll succ(k #+ m)"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
563 |
by (fast_tac (claset() addDs [includes RS subsetD]) 1); |
3731 | 564 |
qed "in_MM_eqpoll_n"; |
1196 | 565 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
566 |
Goalw [LL_def, MM_def] "w : LL ==> succ(k) lepoll w"; |
2469 | 567 |
by (Fast_tac 1); |
3731 | 568 |
qed "in_LL_eqpoll_n"; |
1196 | 569 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
570 |
val in_LL = in_LL_eq_Int RS equalityD1 RS (Int_lower1 RSN (2, subset_trans)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
571 |
|
5068 | 572 |
Goalw [GG_def] |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
573 |
"well_ord(LL,S) ==> \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
574 |
\ ALL b<ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b) lepoll m"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
575 |
by (rtac oallI 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
576 |
by (asm_simp_tac |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
577 |
(simpset() addsimps [ltD, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
578 |
ordermap_bij RS bij_converse_bij RS |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
579 |
bij_is_fun RS apply_type]) 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
580 |
by (cut_facts_tac [includes] 1); |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
581 |
by (rtac eqpoll_sum_imp_Diff_lepoll 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
582 |
by (REPEAT |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
583 |
(fast_tac (claset() delrules [subsetI] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
584 |
addSDs [ltD] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
585 |
addSIs [eqpoll_sum_imp_Diff_lepoll, in_LL_eqpoll_n] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
586 |
addIs [unique_superset1 RS in_MM_eqpoll_n, in_LL, |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
587 |
ordermap_bij RS bij_converse_bij RS |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
588 |
bij_is_fun RS apply_type]) 1 )); |
3731 | 589 |
qed "all_in_lepoll_m"; |
1196 | 590 |
|
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
591 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
592 |
Goal "EX a f. Ord(a) & domain(f) = a & \ |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
593 |
\ (UN b<a. f ` b) = x & (ALL b<a. f ` b lepoll m)"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
594 |
by (resolve_tac [well_ord_LL RS exE] 1 THEN REPEAT (assume_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
595 |
by (rename_tac "S" 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
596 |
by (res_inst_tac [("x","ordertype(LL,S)")] exI 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
597 |
by (res_inst_tac [("x", |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
598 |
"lam b:ordertype(LL,S). GG ` (converse(ordermap(LL,S)) ` b)")] |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
599 |
exI 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
600 |
by (Simp_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
601 |
by (REPEAT (ares_tac [conjI, lam_funtype RS domain_of_fun, |
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
602 |
Ord_ordertype, |
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
603 |
all_in_lepoll_m, OUN_eq_x] 1)); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
604 |
qed "conclusion"; |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
605 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
606 |
Close_locale (); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
607 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
608 |
|
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
609 |
|
1196 | 610 |
(* ********************************************************************** *) |
1461 | 611 |
(* The main theorem AC16(n, k) ==> WO4(n-k) *) |
1196 | 612 |
(* ********************************************************************** *) |
613 |
||
5068 | 614 |
Goalw [AC16_def,WO4_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
615 |
"[| AC16(k #+ m, k); 0 < k; 0 < m; k:nat; m:nat |] ==> WO4(m)"; |
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1200
diff
changeset
|
616 |
by (rtac allI 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
617 |
by (case_tac "Finite(A)" 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
618 |
by (rtac lemma1 1 THEN REPEAT (assume_tac 1)); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
619 |
by (cut_facts_tac [lemma2] 1); |
1196 | 620 |
by (REPEAT (eresolve_tac [exE, conjE] 1)); |
621 |
by (eres_inst_tac [("x","A Un y")] allE 1); |
|
622 |
by (forward_tac [infinite_Un] 1 THEN (mp_tac 1)); |
|
5314
c061e6f9d546
Moved the definition of s_u (as s) into the locale
paulson
parents:
5284
diff
changeset
|
623 |
by (etac zero_lt_natE 1); by (assume_tac 1); |
5284
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
624 |
by (Clarify_tac 1); |
c77e9dd9bafc
Tidying of AC, especially of AC16_WO4 using a locale
paulson
parents:
5265
diff
changeset
|
625 |
by (DEPTH_SOLVE (ares_tac [export conclusion] 1)); |
1196 | 626 |
qed "AC16_WO4"; |