author  paulson 
Thu, 10 Sep 1998 17:42:44 +0200  
changeset 5470  855654b691db 
parent 5314  c061e6f9d546 
child 6021  4a3fc834288e 
permissions  rwrr 
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(nk) 

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 k1 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 k2 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 nk} *) 
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 k2 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:ya; 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:ya; 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 : AB; 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 > AB 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 
\ ==> AB 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 > AB 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 
\ ==> AB 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 k2 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 : ya; 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:ya. 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 nk} *) 
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 nk (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(nk) *) 
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"; 