author  paulson 
Fri, 16 Feb 1996 18:00:47 +0100  
changeset 1512  ce37c64244c0 
parent 1461  6bcb44e4d6e5 
child 1609  5324067d993f 
permissions  rwrr 
1461  1 
(* Title: ZF/Cardinal.ML 
435  2 
ID: $Id$ 
1461  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
435  4 
Copyright 1994 University of Cambridge 
5 

6 
Cardinals in ZermeloFraenkel Set Theory 

7 

8 
This theory does NOT assume the Axiom of Choice 

9 
*) 

10 

11 
open Cardinal; 

12 

13 
(*** The SchroederBernstein Theorem  see Davey & Priestly, page 106 ***) 

14 

15 
(** Lemma: Banach's Decomposition Theorem **) 

16 

17 
goal Cardinal.thy "bnd_mono(X, %W. X  g``(Y  f``W))"; 

18 
by (rtac bnd_monoI 1); 

19 
by (REPEAT (ares_tac [Diff_subset, subset_refl, Diff_mono, image_mono] 1)); 

760  20 
qed "decomp_bnd_mono"; 
435  21 

22 
val [gfun] = goal Cardinal.thy 

1461  23 
"g: Y>X ==> \ 
24 
\ g``(Y  f`` lfp(X, %W. X  g``(Y  f``W))) = \ 

435  25 
\ X  lfp(X, %W. X  g``(Y  f``W)) "; 
26 
by (res_inst_tac [("P", "%u. ?v = Xu")] 

27 
(decomp_bnd_mono RS lfp_Tarski RS ssubst) 1); 

28 
by (simp_tac (ZF_ss addsimps [subset_refl, double_complement, 

1461  29 
gfun RS fun_is_rel RS image_subset]) 1); 
760  30 
qed "Banach_last_equation"; 
435  31 

32 
val prems = goal Cardinal.thy 

33 
"[ f: X>Y; g: Y>X ] ==> \ 

34 
\ EX XA XB YA YB. (XA Int XB = 0) & (XA Un XB = X) & \ 

35 
\ (YA Int YB = 0) & (YA Un YB = Y) & \ 

36 
\ f``XA=YA & g``YB=XB"; 

37 
by (REPEAT 

38 
(FIRSTGOAL 

39 
(resolve_tac [refl, exI, conjI, Diff_disjoint, Diff_partition]))); 

40 
by (rtac Banach_last_equation 3); 

41 
by (REPEAT (resolve_tac (prems@[fun_is_rel, image_subset, lfp_subset]) 1)); 

760  42 
qed "decomposition"; 
435  43 

44 
val prems = goal Cardinal.thy 

45 
"[ f: inj(X,Y); g: inj(Y,X) ] ==> EX h. h: bij(X,Y)"; 

46 
by (cut_facts_tac prems 1); 

47 
by (cut_facts_tac [(prems RL [inj_is_fun]) MRS decomposition] 1); 

48 
by (fast_tac (ZF_cs addSIs [restrict_bij,bij_disjoint_Un] 

49 
addIs [bij_converse_bij]) 1); 

50 
(* The instantiation of exI to "restrict(f,XA) Un converse(restrict(g,YB))" 

51 
is forced by the context!! *) 

760  52 
qed "schroeder_bernstein"; 
435  53 

54 

55 
(** Equipollence is an equivalence relation **) 

56 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

57 
goalw Cardinal.thy [eqpoll_def] "!!f A B. f: bij(A,B) ==> A eqpoll B"; 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

58 
by (etac exI 1); 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

59 
qed "bij_imp_eqpoll"; 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

60 

825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

61 
(*A eqpoll A*) 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

62 
bind_thm ("eqpoll_refl", id_bij RS bij_imp_eqpoll); 
435  63 

64 
goalw Cardinal.thy [eqpoll_def] "!!X Y. X eqpoll Y ==> Y eqpoll X"; 

65 
by (fast_tac (ZF_cs addIs [bij_converse_bij]) 1); 

760  66 
qed "eqpoll_sym"; 
435  67 

68 
goalw Cardinal.thy [eqpoll_def] 

69 
"!!X Y. [ X eqpoll Y; Y eqpoll Z ] ==> X eqpoll Z"; 

70 
by (fast_tac (ZF_cs addIs [comp_bij]) 1); 

760  71 
qed "eqpoll_trans"; 
435  72 

73 
(** Lepollence is a partial ordering **) 

74 

75 
goalw Cardinal.thy [lepoll_def] "!!X Y. X<=Y ==> X lepoll Y"; 

437  76 
by (rtac exI 1); 
77 
by (etac id_subset_inj 1); 

760  78 
qed "subset_imp_lepoll"; 
435  79 

80 
val lepoll_refl = subset_refl RS subset_imp_lepoll; 

81 

82 
goalw Cardinal.thy [eqpoll_def, bij_def, lepoll_def] 

83 
"!!X Y. X eqpoll Y ==> X lepoll Y"; 

84 
by (fast_tac ZF_cs 1); 

760  85 
qed "eqpoll_imp_lepoll"; 
435  86 

87 
goalw Cardinal.thy [lepoll_def] 

88 
"!!X Y. [ X lepoll Y; Y lepoll Z ] ==> X lepoll Z"; 

89 
by (fast_tac (ZF_cs addIs [comp_inj]) 1); 

760  90 
qed "lepoll_trans"; 
435  91 

92 
(*Asymmetry law*) 

93 
goalw Cardinal.thy [lepoll_def,eqpoll_def] 

94 
"!!X Y. [ X lepoll Y; Y lepoll X ] ==> X eqpoll Y"; 

95 
by (REPEAT (etac exE 1)); 

96 
by (rtac schroeder_bernstein 1); 

97 
by (REPEAT (assume_tac 1)); 

760  98 
qed "eqpollI"; 
435  99 

100 
val [major,minor] = goal Cardinal.thy 

101 
"[ X eqpoll Y; [ X lepoll Y; Y lepoll X ] ==> P ] ==> P"; 

437  102 
by (rtac minor 1); 
435  103 
by (REPEAT (resolve_tac [major, eqpoll_imp_lepoll, eqpoll_sym] 1)); 
760  104 
qed "eqpollE"; 
435  105 

106 
goal Cardinal.thy "X eqpoll Y <> X lepoll Y & Y lepoll X"; 

107 
by (fast_tac (ZF_cs addIs [eqpollI] addSEs [eqpollE]) 1); 

760  108 
qed "eqpoll_iff"; 
435  109 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

110 
goalw Cardinal.thy [lepoll_def, inj_def] "!!A. A lepoll 0 ==> A = 0"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

111 
by (fast_tac (eq_cs addDs [apply_type]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

112 
qed "lepoll_0_is_0"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

113 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

114 
(*0 lepoll Y*) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

115 
bind_thm ("empty_lepollI", empty_subsetI RS subset_imp_lepoll); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

116 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

117 
(*A eqpoll 0 ==> A=0*) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

118 
bind_thm ("eqpoll_0_is_0", eqpoll_imp_lepoll RS lepoll_0_is_0); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

119 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

120 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

121 
(*** lesspoll: contributions by Krzysztof Grabczewski ***) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

122 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

123 
goalw Cardinal.thy [inj_def, surj_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

124 
"!!f. [ f : inj(A, succ(m)); f ~: surj(A, succ(m)) ] ==> EX f. f:inj(A,m)"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

125 
by (safe_tac lemmas_cs); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

126 
by (swap_res_tac [exI] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

127 
by (res_inst_tac [("a", "lam z:A. if(f`z=m, y, f`z)")] CollectI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

128 
by (fast_tac (ZF_cs addSIs [if_type RS lam_type] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

129 
addEs [apply_funtype RS succE]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

130 
(*Proving it's injective*) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

131 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

132 
by (fast_tac ZF_cs 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

133 
qed "inj_not_surj_succ"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

134 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

135 
(** Variations on transitivity **) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

136 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

137 
goalw Cardinal.thy [lesspoll_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

138 
"!!X. [ X lesspoll Y; Y lesspoll Z ] ==> X lesspoll Z"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

139 
by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

140 
qed "lesspoll_trans"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

141 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

142 
goalw Cardinal.thy [lesspoll_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

143 
"!!X. [ X lesspoll Y; Y lepoll Z ] ==> X lesspoll Z"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

144 
by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

145 
qed "lesspoll_lepoll_lesspoll"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

146 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

147 
goalw Cardinal.thy [lesspoll_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

148 
"!!X. [ X lesspoll Y; Z lepoll X ] ==> Z lesspoll Y"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

149 
by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] addIs [lepoll_trans]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

150 
qed "lepoll_lesspoll_lesspoll"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

151 

435  152 

153 
(** LEAST  the least number operator [from HOL/Univ.ML] **) 

154 

155 
val [premP,premOrd,premNot] = goalw Cardinal.thy [Least_def] 

156 
"[ P(i); Ord(i); !!x. x<i ==> ~P(x) ] ==> (LEAST x.P(x)) = i"; 

157 
by (rtac the_equality 1); 

158 
by (fast_tac (ZF_cs addSIs [premP,premOrd,premNot]) 1); 

159 
by (REPEAT (etac conjE 1)); 

437  160 
by (etac (premOrd RS Ord_linear_lt) 1); 
435  161 
by (ALLGOALS (fast_tac (ZF_cs addSIs [premP] addSDs [premNot]))); 
760  162 
qed "Least_equality"; 
435  163 

164 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> P(LEAST x.P(x))"; 

165 
by (etac rev_mp 1); 

166 
by (trans_ind_tac "i" [] 1); 

167 
by (rtac impI 1); 

168 
by (rtac classical 1); 

169 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); 

170 
by (assume_tac 2); 

171 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

760  172 
qed "LeastI"; 
435  173 

174 
(*Proof is almost identical to the one above!*) 

175 
goal Cardinal.thy "!!i. [ P(i); Ord(i) ] ==> (LEAST x.P(x)) le i"; 

176 
by (etac rev_mp 1); 

177 
by (trans_ind_tac "i" [] 1); 

178 
by (rtac impI 1); 

179 
by (rtac classical 1); 

180 
by (EVERY1 [rtac (Least_equality RS ssubst), assume_tac, assume_tac]); 

181 
by (etac le_refl 2); 

182 
by (fast_tac (ZF_cs addEs [ltE, lt_trans1] addIs [leI, ltI]) 1); 

760  183 
qed "Least_le"; 
435  184 

185 
(*LEAST really is the smallest*) 

186 
goal Cardinal.thy "!!i. [ P(i); i < (LEAST x.P(x)) ] ==> Q"; 

437  187 
by (rtac (Least_le RSN (2,lt_trans2) RS lt_irrefl) 1); 
435  188 
by (REPEAT (eresolve_tac [asm_rl, ltE] 1)); 
760  189 
qed "less_LeastE"; 
435  190 

1031  191 
(*Easier to apply than LeastI: conclusion has only one occurrence of P*) 
845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

192 
qed_goal "LeastI2" Cardinal.thy 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

193 
"[ P(i); Ord(i); !!j. P(j) ==> Q(j) ] ==> Q(LEAST j. P(j))" 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

194 
(fn prems => [ resolve_tac prems 1, 
1461  195 
rtac LeastI 1, 
196 
resolve_tac prems 1, 

197 
resolve_tac prems 1 ]); 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

198 

437  199 
(*If there is no such P then LEAST is vacuously 0*) 
200 
goalw Cardinal.thy [Least_def] 

201 
"!!P. [ ~ (EX i. Ord(i) & P(i)) ] ==> (LEAST x.P(x)) = 0"; 

202 
by (rtac the_0 1); 

203 
by (fast_tac ZF_cs 1); 

760  204 
qed "Least_0"; 
437  205 

435  206 
goal Cardinal.thy "Ord(LEAST x.P(x))"; 
437  207 
by (excluded_middle_tac "EX i. Ord(i) & P(i)" 1); 
435  208 
by (safe_tac ZF_cs); 
437  209 
by (rtac (Least_le RS ltE) 2); 
435  210 
by (REPEAT_SOME assume_tac); 
437  211 
by (etac (Least_0 RS ssubst) 1); 
212 
by (rtac Ord_0 1); 

760  213 
qed "Ord_Least"; 
435  214 

215 

216 
(** Basic properties of cardinals **) 

217 

218 
(*Not needed for simplification, but helpful below*) 

219 
val prems = goal Cardinal.thy 

220 
"[ !!y. P(y) <> Q(y) ] ==> (LEAST x.P(x)) = (LEAST x.Q(x))"; 

221 
by (simp_tac (FOL_ss addsimps prems) 1); 

760  222 
qed "Least_cong"; 
435  223 

765  224 
(*Need AC to prove X lepoll Y ==> X le Y ; 
225 
see well_ord_lepoll_imp_Card_le *) 

435  226 
goalw Cardinal.thy [eqpoll_def,cardinal_def] "!!X Y. X eqpoll Y ==> X = Y"; 
437  227 
by (rtac Least_cong 1); 
435  228 
by (fast_tac (ZF_cs addEs [comp_bij,bij_converse_bij]) 1); 
760  229 
qed "cardinal_cong"; 
435  230 

231 
(*Under AC, the premise becomes trivial; one consequence is A = A*) 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

232 
goalw Cardinal.thy [cardinal_def] 
435  233 
"!!A. well_ord(A,r) ==> A eqpoll A"; 
437  234 
by (rtac LeastI 1); 
235 
by (etac Ord_ordertype 2); 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

236 
by (etac (ordermap_bij RS bij_converse_bij RS bij_imp_eqpoll) 1); 
760  237 
qed "well_ord_cardinal_eqpoll"; 
435  238 

803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
792
diff
changeset

239 
bind_thm ("Ord_cardinal_eqpoll", well_ord_Memrel RS well_ord_cardinal_eqpoll); 
435  240 

241 
goal Cardinal.thy 

242 
"!!X Y. [ well_ord(X,r); well_ord(Y,s); X = Y ] ==> X eqpoll Y"; 

437  243 
by (rtac (eqpoll_sym RS eqpoll_trans) 1); 
244 
by (etac well_ord_cardinal_eqpoll 1); 

435  245 
by (asm_simp_tac (ZF_ss addsimps [well_ord_cardinal_eqpoll]) 1); 
760  246 
qed "well_ord_cardinal_eqE"; 
435  247 

248 

249 
(** Observations from Kunen, page 28 **) 

250 

251 
goalw Cardinal.thy [cardinal_def] "!!i. Ord(i) ==> i le i"; 

437  252 
by (etac (eqpoll_refl RS Least_le) 1); 
760  253 
qed "Ord_cardinal_le"; 
435  254 

484  255 
goalw Cardinal.thy [Card_def] "!!K. Card(K) ==> K = K"; 
437  256 
by (etac sym 1); 
760  257 
qed "Card_cardinal_eq"; 
435  258 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

259 
(* Could replace the ~(j eqpoll i) by ~(i lepoll j) *) 
435  260 
val prems = goalw Cardinal.thy [Card_def,cardinal_def] 
261 
"[ Ord(i); !!j. j<i ==> ~(j eqpoll i) ] ==> Card(i)"; 

437  262 
by (rtac (Least_equality RS ssubst) 1); 
435  263 
by (REPEAT (ares_tac ([refl,eqpoll_refl]@prems) 1)); 
760  264 
qed "CardI"; 
435  265 

266 
goalw Cardinal.thy [Card_def, cardinal_def] "!!i. Card(i) ==> Ord(i)"; 

437  267 
by (etac ssubst 1); 
268 
by (rtac Ord_Least 1); 

760  269 
qed "Card_is_Ord"; 
435  270 

765  271 
goal Cardinal.thy "!!K. Card(K) ==> K le K"; 
272 
by (asm_simp_tac (ZF_ss addsimps [le_refl, Card_is_Ord, Card_cardinal_eq]) 1); 

782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
765
diff
changeset

273 
qed "Card_cardinal_le"; 
765  274 

484  275 
goalw Cardinal.thy [cardinal_def] "Ord(A)"; 
437  276 
by (rtac Ord_Least 1); 
760  277 
qed "Ord_cardinal"; 
435  278 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

279 
(*The cardinals are the initial ordinals*) 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

280 
goal Cardinal.thy "Card(K) <> Ord(K) & (ALL j. j<K > ~ j eqpoll K)"; 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

281 
by (safe_tac (ZF_cs addSIs [CardI, Card_is_Ord])); 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

282 
by (fast_tac ZF_cs 2); 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

283 
by (rewrite_goals_tac [Card_def, cardinal_def]); 
1461  284 
by (rtac less_LeastE 1); 
285 
by (etac subst 2); 

845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

286 
by (ALLGOALS assume_tac); 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

287 
qed "Card_iff_initial"; 
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

288 

437  289 
goal Cardinal.thy "Card(0)"; 
290 
by (rtac (Ord_0 RS CardI) 1); 

291 
by (fast_tac (ZF_cs addSEs [ltE]) 1); 

760  292 
qed "Card_0"; 
437  293 

522  294 
val [premK,premL] = goal Cardinal.thy 
295 
"[ Card(K); Card(L) ] ==> Card(K Un L)"; 

296 
by (rtac ([premK RS Card_is_Ord, premL RS Card_is_Ord] MRS Ord_linear_le) 1); 

297 
by (asm_simp_tac 

298 
(ZF_ss addsimps [premL, le_imp_subset, subset_Un_iff RS iffD1]) 1); 

299 
by (asm_simp_tac 

300 
(ZF_ss addsimps [premK, le_imp_subset, subset_Un_iff2 RS iffD1]) 1); 

760  301 
qed "Card_Un"; 
522  302 

303 
(*Infinite unions of cardinals? See Devlin, Lemma 6.7, page 98*) 

304 

484  305 
goalw Cardinal.thy [cardinal_def] "Card(A)"; 
437  306 
by (excluded_middle_tac "EX i. Ord(i) & i eqpoll A" 1); 
307 
by (etac (Least_0 RS ssubst) 1 THEN rtac Card_0 1); 

308 
by (rtac (Ord_Least RS CardI) 1); 

309 
by (safe_tac ZF_cs); 

310 
by (rtac less_LeastE 1); 

311 
by (assume_tac 2); 

312 
by (etac eqpoll_trans 1); 

313 
by (REPEAT (ares_tac [LeastI] 1)); 

760  314 
qed "Card_cardinal"; 
437  315 

435  316 
(*Kunen's Lemma 10.5*) 
317 
goal Cardinal.thy "!!i j. [ i le j; j le i ] ==> j = i"; 

437  318 
by (rtac (eqpollI RS cardinal_cong) 1); 
319 
by (etac (le_imp_subset RS subset_imp_lepoll) 1); 

320 
by (rtac lepoll_trans 1); 

321 
by (etac (le_imp_subset RS subset_imp_lepoll) 2); 

322 
by (rtac (eqpoll_sym RS eqpoll_imp_lepoll) 1); 

323 
by (rtac Ord_cardinal_eqpoll 1); 

435  324 
by (REPEAT (eresolve_tac [ltE, Ord_succD] 1)); 
760  325 
qed "cardinal_eq_lemma"; 
435  326 

327 
goal Cardinal.thy "!!i j. i le j ==> i le j"; 

328 
by (res_inst_tac [("i","i"),("j","j")] Ord_linear_le 1); 

329 
by (REPEAT_FIRST (ares_tac [Ord_cardinal, le_eqI])); 

437  330 
by (rtac cardinal_eq_lemma 1); 
331 
by (assume_tac 2); 

332 
by (etac le_trans 1); 

333 
by (etac ltE 1); 

334 
by (etac Ord_cardinal_le 1); 

760  335 
qed "cardinal_mono"; 
435  336 

337 
(*Since we have succ(nat) le nat, the converse of cardinal_mono fails!*) 

338 
goal Cardinal.thy "!!i j. [ i < j; Ord(i); Ord(j) ] ==> i < j"; 

437  339 
by (rtac Ord_linear2 1); 
435  340 
by (REPEAT_SOME assume_tac); 
437  341 
by (etac (lt_trans2 RS lt_irrefl) 1); 
342 
by (etac cardinal_mono 1); 

760  343 
qed "cardinal_lt_imp_lt"; 
435  344 

484  345 
goal Cardinal.thy "!!i j. [ i < K; Ord(i); Card(K) ] ==> i < K"; 
435  346 
by (asm_simp_tac (ZF_ss addsimps 
1461  347 
[cardinal_lt_imp_lt, Card_is_Ord, Card_cardinal_eq]) 1); 
760  348 
qed "Card_lt_imp_lt"; 
435  349 

484  350 
goal Cardinal.thy "!!i j. [ Ord(i); Card(K) ] ==> (i < K) <> (i < K)"; 
351 
by (fast_tac (ZF_cs addEs [Card_lt_imp_lt, Ord_cardinal_le RS lt_trans1]) 1); 

760  352 
qed "Card_lt_iff"; 
484  353 

354 
goal Cardinal.thy "!!i j. [ Ord(i); Card(K) ] ==> (K le i) <> (K le i)"; 

355 
by (asm_simp_tac (ZF_ss addsimps 

1461  356 
[Card_lt_iff, Card_is_Ord, Ord_cardinal, 
357 
not_lt_iff_le RS iff_sym]) 1); 

760  358 
qed "Card_le_iff"; 
484  359 

435  360 

361 
(*** The finite cardinals ***) 

362 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

363 
goalw Cardinal.thy [lepoll_def, inj_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

364 
"!!A B. [ cons(u,A) lepoll cons(v,B); u~:A; v~:B ] ==> A lepoll B"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

365 
by (safe_tac ZF_cs); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

366 
by (res_inst_tac [("x", "lam x:A. if(f`x=v, f`u, f`x)")] exI 1); 
437  367 
by (rtac CollectI 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

368 
(*Proving it's in the function space A>B*) 
437  369 
by (rtac (if_type RS lam_type) 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

370 
by (fast_tac (ZF_cs addEs [apply_funtype RS consE]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

371 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1); 
435  372 
(*Proving it's injective*) 
373 
by (asm_simp_tac (ZF_ss setloop split_tac [expand_if]) 1); 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

374 
by (fast_tac ZF_cs 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

375 
qed "cons_lepoll_consD"; 
435  376 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

377 
goal Cardinal.thy 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

378 
"!!A B. [ cons(u,A) eqpoll cons(v,B); u~:A; v~:B ] ==> A eqpoll B"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

379 
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

380 
by (fast_tac (ZF_cs addIs [cons_lepoll_consD]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

381 
qed "cons_eqpoll_consD"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

382 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

383 
(*Lemma suggested by Mike Fourman*) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

384 
goalw Cardinal.thy [succ_def] "!!m n. succ(m) lepoll succ(n) ==> m lepoll n"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

385 
by (etac cons_lepoll_consD 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

386 
by (REPEAT (rtac mem_not_refl 1)); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

387 
qed "succ_lepoll_succD"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

388 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

389 
val [prem] = goal Cardinal.thy 
435  390 
"m:nat ==> ALL n: nat. m lepoll n > m le n"; 
391 
by (nat_ind_tac "m" [prem] 1); 

392 
by (fast_tac (ZF_cs addSIs [nat_0_le]) 1); 

437  393 
by (rtac ballI 1); 
435  394 
by (eres_inst_tac [("n","n")] natE 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

395 
by (asm_simp_tac (ZF_ss addsimps [lepoll_def, inj_def, 
1461  396 
succI1 RS Pi_empty2]) 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

397 
by (fast_tac (ZF_cs addSIs [succ_leI] addSDs [succ_lepoll_succD]) 1); 
803
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
792
diff
changeset

398 
val nat_lepoll_imp_le_lemma = result(); 
4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
792
diff
changeset

399 

4c8333ab3eae
changed useless "qed" calls for lemmas back to uses of "result",
lcp
parents:
792
diff
changeset

400 
bind_thm ("nat_lepoll_imp_le", nat_lepoll_imp_le_lemma RS bspec RS mp); 
435  401 

402 
goal Cardinal.thy 

403 
"!!m n. [ m:nat; n: nat ] ==> m eqpoll n <> m = n"; 

437  404 
by (rtac iffI 1); 
435  405 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
437  406 
by (fast_tac (ZF_cs addIs [nat_lepoll_imp_le, le_anti_sym] 
407 
addSEs [eqpollE]) 1); 

760  408 
qed "nat_eqpoll_iff"; 
435  409 

410 
goalw Cardinal.thy [Card_def,cardinal_def] 

411 
"!!n. n: nat ==> Card(n)"; 

437  412 
by (rtac (Least_equality RS ssubst) 1); 
435  413 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, nat_into_Ord, refl])); 
414 
by (asm_simp_tac (ZF_ss addsimps [lt_nat_in_nat RS nat_eqpoll_iff]) 1); 

437  415 
by (fast_tac (ZF_cs addSEs [lt_irrefl]) 1); 
760  416 
qed "nat_into_Card"; 
435  417 

418 
(*Part of Kunen's Lemma 10.6*) 

419 
goal Cardinal.thy "!!n. [ succ(n) lepoll n; n:nat ] ==> P"; 

437  420 
by (rtac (nat_lepoll_imp_le RS lt_irrefl) 1); 
435  421 
by (REPEAT (ares_tac [nat_succI] 1)); 
760  422 
qed "succ_lepoll_natE"; 
435  423 

424 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

425 
(** lepoll, lesspoll and natural numbers **) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

426 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

427 
goalw Cardinal.thy [lesspoll_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

428 
"!!m. [ A lepoll m; m:nat ] ==> A lesspoll succ(m)"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

429 
by (rtac conjI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

430 
by (fast_tac (ZF_cs addIs [subset_imp_lepoll RSN (2,lepoll_trans)]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

431 
by (rtac notI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

432 
by (dresolve_tac [eqpoll_sym RS eqpoll_imp_lepoll] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

433 
by (dtac lepoll_trans 1 THEN assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

434 
by (etac succ_lepoll_natE 1 THEN assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

435 
qed "lepoll_imp_lesspoll_succ"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

436 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

437 
goalw Cardinal.thy [lesspoll_def, lepoll_def, eqpoll_def, bij_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

438 
"!!m. [ A lesspoll succ(m); m:nat ] ==> A lepoll m"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

439 
by (step_tac ZF_cs 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

440 
by (fast_tac (ZF_cs addSIs [inj_not_surj_succ]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

441 
qed "lesspoll_succ_imp_lepoll"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

442 

1031  443 
goal Cardinal.thy "!!m. m:nat ==> A lesspoll succ(m) <> A lepoll m"; 
444 
by (fast_tac (ZF_cs addSIs [lepoll_imp_lesspoll_succ, 

1461  445 
lesspoll_succ_imp_lepoll]) 1); 
1031  446 
qed "lesspoll_succ_iff"; 
447 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

448 
goal Cardinal.thy "!!A m. [ A lepoll succ(m); m:nat ] ==> \ 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

449 
\ A lepoll m  A eqpoll succ(m)"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

450 
by (rtac disjCI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

451 
by (rtac lesspoll_succ_imp_lepoll 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

452 
by (assume_tac 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

453 
by (asm_simp_tac (ZF_ss addsimps [lesspoll_def]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

454 
qed "lepoll_succ_disj"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

455 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

456 

435  457 
(*** The first infinite cardinal: Omega, or nat ***) 
458 

459 
(*This implies Kunen's Lemma 10.6*) 

460 
goal Cardinal.thy "!!n. [ n<i; n:nat ] ==> ~ i lepoll n"; 

437  461 
by (rtac notI 1); 
435  462 
by (rtac succ_lepoll_natE 1 THEN assume_tac 2); 
463 
by (rtac lepoll_trans 1 THEN assume_tac 2); 

437  464 
by (etac ltE 1); 
435  465 
by (REPEAT (ares_tac [Ord_succ_subsetI RS subset_imp_lepoll] 1)); 
760  466 
qed "lt_not_lepoll"; 
435  467 

468 
goal Cardinal.thy "!!i n. [ Ord(i); n:nat ] ==> i eqpoll n <> i=n"; 

437  469 
by (rtac iffI 1); 
435  470 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_refl]) 2); 
471 
by (rtac Ord_linear_lt 1); 

472 
by (REPEAT_SOME (eresolve_tac [asm_rl, nat_into_Ord])); 

473 
by (etac (lt_nat_in_nat RS nat_eqpoll_iff RS iffD1) 1 THEN 

474 
REPEAT (assume_tac 1)); 

475 
by (rtac (lt_not_lepoll RS notE) 1 THEN (REPEAT (assume_tac 1))); 

437  476 
by (etac eqpoll_imp_lepoll 1); 
760  477 
qed "Ord_nat_eqpoll_iff"; 
435  478 

437  479 
goalw Cardinal.thy [Card_def,cardinal_def] "Card(nat)"; 
480 
by (rtac (Least_equality RS ssubst) 1); 

481 
by (REPEAT_FIRST (ares_tac [eqpoll_refl, Ord_nat, refl])); 

482 
by (etac ltE 1); 

483 
by (asm_simp_tac (ZF_ss addsimps [eqpoll_iff, lt_not_lepoll, ltI]) 1); 

760  484 
qed "Card_nat"; 
435  485 

437  486 
(*Allows showing that i is a limit cardinal*) 
487 
goal Cardinal.thy "!!i. nat le i ==> nat le i"; 

488 
by (rtac (Card_nat RS Card_cardinal_eq RS subst) 1); 

489 
by (etac cardinal_mono 1); 

760  490 
qed "nat_le_cardinal"; 
437  491 

571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

492 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

493 
(*** Towards Cardinal Arithmetic ***) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

494 
(** Congruence laws for successor, cardinal addition and multiplication **) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

495 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

496 
(*Congruence law for cons under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

497 
goalw Cardinal.thy [lepoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

498 
"!!A B. [ A lepoll B; b ~: B ] ==> cons(a,A) lepoll cons(b,B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

499 
by (safe_tac ZF_cs); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

500 
by (res_inst_tac [("x", "lam y: cons(a,A).if(y=a, b, f`y)")] exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

501 
by (res_inst_tac [("d","%z.if(z:B, converse(f)`z, a)")] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

502 
lam_injective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

503 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, cons_iff] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

504 
setloop etac consE') 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

505 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_type, left_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

506 
setloop etac consE') 1); 
760  507 
qed "cons_lepoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

508 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

509 
goal Cardinal.thy 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

510 
"!!A B. [ A eqpoll B; a ~: A; b ~: B ] ==> cons(a,A) eqpoll cons(b,B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

511 
by (asm_full_simp_tac (ZF_ss addsimps [eqpoll_iff, cons_lepoll_cong]) 1); 
760  512 
qed "cons_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

513 

833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

514 
goal Cardinal.thy 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

515 
"!!A B. [ a ~: A; b ~: B ] ==> \ 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

516 
\ cons(a,A) lepoll cons(b,B) <> A lepoll B"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

517 
by (fast_tac (ZF_cs addIs [cons_lepoll_cong, cons_lepoll_consD]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

518 
qed "cons_lepoll_cons_iff"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

519 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

520 
goal Cardinal.thy 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

521 
"!!A B. [ a ~: A; b ~: B ] ==> \ 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

522 
\ cons(a,A) eqpoll cons(b,B) <> A eqpoll B"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

523 
by (fast_tac (ZF_cs addIs [cons_eqpoll_cong, cons_eqpoll_consD]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

524 
qed "cons_eqpoll_cons_iff"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

525 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

526 
goalw Cardinal.thy [succ_def] "{a} eqpoll 1"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

527 
by (fast_tac (ZF_cs addSIs [eqpoll_refl RS cons_eqpoll_cong]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

528 
qed "singleton_eqpoll_1"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

529 

571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

530 
(*Congruence law for succ under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

531 
goalw Cardinal.thy [succ_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

532 
"!!A B. A eqpoll B ==> succ(A) eqpoll succ(B)"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

533 
by (REPEAT (ares_tac [cons_eqpoll_cong, mem_not_refl] 1)); 
760  534 
qed "succ_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

535 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

536 
(*Congruence law for + under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

537 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

538 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A+B eqpoll C+D"; 
845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

539 
by (fast_tac (ZF_cs addSIs [sum_bij]) 1); 
760  540 
qed "sum_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

541 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

542 
(*Congruence law for * under equipollence*) 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

543 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

544 
"!!A B C D. [ A eqpoll C; B eqpoll D ] ==> A*B eqpoll C*D"; 
845
825e96b87ef7
Added Krzysztof's theorem LeastI2. Proof of sum_eqpoll_cong
lcp
parents:
833
diff
changeset

545 
by (fast_tac (ZF_cs addSIs [prod_bij]) 1); 
760  546 
qed "prod_eqpoll_cong"; 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

547 

0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

548 
goalw Cardinal.thy [eqpoll_def] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

549 
"!!f. [ f: inj(A,B); A Int B = 0 ] ==> A Un (B  range(f)) eqpoll B"; 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

550 
by (rtac exI 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

551 
by (res_inst_tac [("c", "%x. if(x:A, f`x, x)"), 
1461  552 
("d", "%y. if(y: range(f), converse(f)`y, y)")] 
571
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

553 
lam_bijective 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

554 
by (fast_tac (ZF_cs addSIs [if_type, apply_type] addIs [inj_is_fun]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

555 
by (asm_simp_tac 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

556 
(ZF_ss addsimps [inj_converse_fun RS apply_funtype] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

557 
setloop split_tac [expand_if]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

558 
by (asm_simp_tac (ZF_ss addsimps [inj_is_fun RS apply_rangeI, left_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

559 
setloop etac UnE') 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

560 
by (asm_simp_tac 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

561 
(ZF_ss addsimps [inj_converse_fun RS apply_funtype, right_inverse] 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

562 
setloop split_tac [expand_if]) 1); 
0b03ce5b62f7
ZF/Cardinal: some results moved here from CardinalArith
lcp
parents:
522
diff
changeset

563 
by (fast_tac (ZF_cs addEs [equals0D]) 1); 
760  564 
qed "inj_disjoint_eqpoll"; 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

565 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

566 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

567 
(*** Lemmas by Krzysztof Grabczewski. New proofs using cons_lepoll_cons. 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

568 
Could easily generalise from succ to cons. ***) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

569 

1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

570 
(*If A has at most n+1 elements and a:A then A{a} has at most n.*) 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

571 
goalw Cardinal.thy [succ_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

572 
"!!A a n. [ a:A; A lepoll succ(n) ] ==> A  {a} lepoll n"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

573 
by (rtac cons_lepoll_consD 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

574 
by (rtac mem_not_refl 3); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

575 
by (eresolve_tac [cons_Diff RS ssubst] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

576 
by (safe_tac ZF_cs); 
1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

577 
qed "Diff_sing_lepoll"; 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

578 

1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

579 
(*If A has at least n+1 elements then A{a} has at least n.*) 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

580 
goalw Cardinal.thy [succ_def] 
1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

581 
"!!A a n. [ succ(n) lepoll A ] ==> n lepoll A  {a}"; 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

582 
by (rtac cons_lepoll_consD 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

583 
by (rtac mem_not_refl 2); 
1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

584 
by (fast_tac ZF_cs 2); 
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

585 
by (fast_tac (ZF_cs addSEs [subset_imp_lepoll RSN (2, lepoll_trans)]) 1); 
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

586 
qed "lepoll_Diff_sing"; 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

587 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

588 
goal Cardinal.thy "!!A a n. [ a:A; A eqpoll succ(n) ] ==> A  {a} eqpoll n"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

589 
by (fast_tac (ZF_cs addSIs [eqpollI] addSEs [eqpollE] 
1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

590 
addIs [Diff_sing_lepoll,lepoll_Diff_sing]) 1); 
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

591 
qed "Diff_sing_eqpoll"; 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

592 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

593 
goal Cardinal.thy "!!A. [ A lepoll 1; a:A ] ==> A = {a}"; 
1055
67f5344605b7
Renamed diff_sing_lepoll, lepoll_diff_sing and diff_sing_eqpoll
lcp
parents:
1031
diff
changeset

594 
by (forward_tac [Diff_sing_lepoll] 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

595 
by (assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

596 
by (dtac lepoll_0_is_0 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

597 
by (fast_tac (eq_cs addEs [equalityE]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

598 
qed "lepoll_1_is_sing"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

599 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

600 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

601 
(*** Finite and infinite sets ***) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

602 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

603 
goalw Cardinal.thy [Finite_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

604 
"!!A. [ A lepoll n; n:nat ] ==> Finite(A)"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

605 
by (etac rev_mp 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

606 
by (etac nat_induct 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

607 
by (fast_tac (ZF_cs addSDs [lepoll_0_is_0] addSIs [eqpoll_refl,nat_0I]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

608 
by (fast_tac (ZF_cs addSDs [lepoll_succ_disj] addSIs [nat_succI]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

609 
qed "lepoll_nat_imp_Finite"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

610 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

611 
goalw Cardinal.thy [Finite_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

612 
"!!X. [ Y lepoll X; Finite(X) ] ==> Finite(Y)"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

613 
by (fast_tac (ZF_cs addSEs [eqpollE] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

614 
addEs [lepoll_trans RS 
1461  615 
rewrite_rule [Finite_def] lepoll_nat_imp_Finite]) 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

616 
qed "lepoll_Finite"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

617 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

618 
goalw Cardinal.thy [Finite_def] "!!x. Finite(x) ==> Finite(cons(y,x))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

619 
by (excluded_middle_tac "y:x" 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

620 
by (asm_simp_tac (ZF_ss addsimps [cons_absorb]) 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

621 
by (etac bexE 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

622 
by (rtac bexI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

623 
by (etac nat_succI 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

624 
by (asm_simp_tac 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

625 
(ZF_ss addsimps [succ_def, cons_eqpoll_cong, mem_not_refl]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

626 
qed "Finite_imp_cons_Finite"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

627 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

628 
goalw Cardinal.thy [succ_def] "!!x. Finite(x) ==> Finite(succ(x))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

629 
by (etac Finite_imp_cons_Finite 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

630 
qed "Finite_imp_succ_Finite"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

631 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

632 
goalw Cardinal.thy [Finite_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

633 
"!!i. [ Ord(i); ~ Finite(i) ] ==> nat le i"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

634 
by (eresolve_tac [Ord_nat RSN (2,Ord_linear2)] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

635 
by (assume_tac 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

636 
by (fast_tac (ZF_cs addSIs [eqpoll_refl] addSEs [ltE]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

637 
qed "nat_le_infinite_Ord"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

638 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

639 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

640 
(*Krzysztof Grabczewski's proof that the converse of a finite, wellordered 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

641 
set is wellordered. Proofs simplified by lcp. *) 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

642 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

643 
goal Nat.thy "!!n. n:nat ==> wf[n](converse(Memrel(n)))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

644 
by (etac nat_induct 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

645 
by (fast_tac (ZF_cs addIs [wf_onI]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

646 
by (rtac wf_onI 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

647 
by (asm_full_simp_tac 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

648 
(ZF_ss addsimps [wf_on_def, wf_def, converse_iff, Memrel_iff]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

649 
by (excluded_middle_tac "x:Z" 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

650 
by (dres_inst_tac [("x", "x")] bspec 2 THEN assume_tac 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

651 
by (fast_tac (ZF_cs addSEs [mem_irrefl] addEs [mem_asym]) 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

652 
by (dres_inst_tac [("x", "Z")] spec 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

653 
by (safe_tac ZF_cs); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

654 
by (dres_inst_tac [("x", "xa")] bspec 1 THEN assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

655 
by (fast_tac ZF_cs 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

656 
qed "nat_wf_on_converse_Memrel"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

657 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

658 
goal Cardinal.thy "!!n. n:nat ==> well_ord(n,converse(Memrel(n)))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

659 
by (forward_tac [Ord_nat RS Ord_in_Ord RS well_ord_Memrel] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

660 
by (rewtac well_ord_def); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

661 
by (fast_tac (ZF_cs addSIs [tot_ord_converse, nat_wf_on_converse_Memrel]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

662 
qed "nat_well_ord_converse_Memrel"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

663 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

664 
goal Cardinal.thy 
1461  665 
"!!A. [ well_ord(A,r); \ 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

666 
\ well_ord(ordertype(A,r), converse(Memrel(ordertype(A, r)))) \ 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

667 
\ ] ==> well_ord(A,converse(r))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

668 
by (resolve_tac [well_ord_Int_iff RS iffD1] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

669 
by (forward_tac [ordermap_bij RS bij_is_inj RS well_ord_rvimage] 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

670 
by (assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

671 
by (asm_full_simp_tac 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

672 
(ZF_ss addsimps [rvimage_converse, converse_Int, converse_prod, 
1461  673 
ordertype_ord_iso RS ord_iso_rvimage_eq]) 1); 
833
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

674 
qed "well_ord_converse"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

675 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

676 
goal Cardinal.thy 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

677 
"!!A. [ well_ord(A,r); A eqpoll n; n:nat ] ==> ordertype(A,r)=n"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

678 
by (rtac (Ord_ordertype RS Ord_nat_eqpoll_iff RS iffD1) 1 THEN 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

679 
REPEAT (assume_tac 1)); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

680 
by (rtac eqpoll_trans 1 THEN assume_tac 2); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

681 
by (rewtac eqpoll_def); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

682 
by (fast_tac (ZF_cs addSIs [ordermap_bij RS bij_converse_bij]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

683 
qed "ordertype_eq_n"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

684 

ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

685 
goalw Cardinal.thy [Finite_def] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

686 
"!!A. [ Finite(A); well_ord(A,r) ] ==> well_ord(A,converse(r))"; 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

687 
by (rtac well_ord_converse 1 THEN assume_tac 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

688 
by (fast_tac (ZF_cs addDs [ordertype_eq_n] 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

689 
addSIs [nat_well_ord_converse_Memrel]) 1); 
ba386650df2c
Proved cons_lepoll_consD, succ_lepoll_succD, cons_eqpoll_consD,
lcp
parents:
803
diff
changeset

690 
qed "Finite_well_ord_converse"; 