author  wenzelm 
Sat, 18 Jul 2015 22:58:50 +0200  
changeset 60758  d8d85a8172b5 
parent 58889  5b7a9633cfa8 
child 61943  7fba644ed827 
permissions  rwrr 
55056  1 
(* Title: HOL/BNF_Cardinal_Arithmetic.thy 
54474  2 
Author: Dmitriy Traytel, TU Muenchen 
3 
Copyright 2012 

4 

55059  5 
Cardinal arithmetic as needed by bounded natural functors. 
54474  6 
*) 
7 

60758  8 
section \<open>Cardinal Arithmetic as Needed by Bounded Natural Functors\<close> 
54474  9 

55056  10 
theory BNF_Cardinal_Arithmetic 
11 
imports BNF_Cardinal_Order_Relation 

54474  12 
begin 
13 

14 
lemma dir_image: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); Card_order r\<rbrakk> \<Longrightarrow> r =o dir_image r f" 

15 
by (rule dir_image_ordIso) (auto simp add: inj_on_def card_order_on_def) 

16 

17 
lemma card_order_dir_image: 

18 
assumes bij: "bij f" and co: "card_order r" 

19 
shows "card_order (dir_image r f)" 

20 
proof  

21 
from assms have "Field (dir_image r f) = UNIV" 

22 
using card_order_on_Card_order[of UNIV r] unfolding bij_def dir_image_Field by auto 

23 
moreover from bij have "\<And>x y. (f x = f y) = (x = y)" unfolding bij_def inj_on_def by auto 

24 
with co have "Card_order (dir_image r f)" 

25 
using card_order_on_Card_order[of UNIV r] Card_order_ordIso2[OF _ dir_image] by blast 

26 
ultimately show ?thesis by auto 

27 
qed 

28 

29 
lemma ordIso_refl: "Card_order r \<Longrightarrow> r =o r" 

30 
by (rule card_order_on_ordIso) 

31 

32 
lemma ordLeq_refl: "Card_order r \<Longrightarrow> r \<le>o r" 

33 
by (rule ordIso_imp_ordLeq, rule card_order_on_ordIso) 

34 

35 
lemma card_of_ordIso_subst: "A = B \<Longrightarrow> A =o B" 

36 
by (simp only: ordIso_refl card_of_Card_order) 

37 

38 
lemma Field_card_order: "card_order r \<Longrightarrow> Field r = UNIV" 

39 
using card_order_on_Card_order[of UNIV r] by simp 

40 

41 

60758  42 
subsection \<open>Zero\<close> 
54474  43 

44 
definition czero where 

45 
"czero = card_of {}" 

46 

47 
lemma czero_ordIso: 

48 
"czero =o czero" 

49 
using card_of_empty_ordIso by (simp add: czero_def) 

50 

51 
lemma card_of_ordIso_czero_iff_empty: 

52 
"A =o (czero :: 'b rel) \<longleftrightarrow> A = ({} :: 'a set)" 

53 
unfolding czero_def by (rule iffI[OF card_of_empty2]) (auto simp: card_of_refl card_of_empty_ordIso) 

54 

55 
(* A "not czero" Cardinal predicate *) 

56 
abbreviation Cnotzero where 

57 
"Cnotzero (r :: 'a rel) \<equiv> \<not>(r =o (czero :: 'a rel)) \<and> Card_order r" 

58 

59 
(*helper*) 

60 
lemma Cnotzero_imp_not_empty: "Cnotzero r \<Longrightarrow> Field r \<noteq> {}" 

55811  61 
unfolding Card_order_iff_ordIso_card_of czero_def by force 
54474  62 

63 
lemma czeroI: 

64 
"\<lbrakk>Card_order r; Field r = {}\<rbrakk> \<Longrightarrow> r =o czero" 

65 
using Cnotzero_imp_not_empty ordIso_transitive[OF _ czero_ordIso] by blast 

66 

67 
lemma czeroE: 

68 
"r =o czero \<Longrightarrow> Field r = {}" 

69 
unfolding czero_def 

70 
by (drule card_of_cong) (simp only: Field_card_of card_of_empty2) 

71 

72 
lemma Cnotzero_mono: 

73 
"\<lbrakk>Cnotzero r; Card_order q; r \<le>o q\<rbrakk> \<Longrightarrow> Cnotzero q" 

74 
apply (rule ccontr) 

75 
apply auto 

76 
apply (drule czeroE) 

77 
apply (erule notE) 

78 
apply (erule czeroI) 

79 
apply (drule card_of_mono2) 

80 
apply (simp only: card_of_empty3) 

81 
done 

82 

60758  83 
subsection \<open>(In)finite cardinals\<close> 
54474  84 

85 
definition cinfinite where 

54578
9387251b6a46
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
traytel
parents:
54482
diff
changeset

86 
"cinfinite r = (\<not> finite (Field r))" 
54474  87 

88 
abbreviation Cinfinite where 

89 
"Cinfinite r \<equiv> cinfinite r \<and> Card_order r" 

90 

91 
definition cfinite where 

92 
"cfinite r = finite (Field r)" 

93 

94 
abbreviation Cfinite where 

95 
"Cfinite r \<equiv> cfinite r \<and> Card_order r" 

96 

97 
lemma Cfinite_ordLess_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r <o s" 

98 
unfolding cfinite_def cinfinite_def 

55811  99 
by (blast intro: finite_ordLess_infinite card_order_on_well_order_on) 
54474  100 

54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

101 
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq] 
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

102 

1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

103 
lemma natLeq_cinfinite: "cinfinite natLeq" 
55811  104 
unfolding cinfinite_def Field_natLeq by (rule infinite_UNIV_nat) 
54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

105 

54474  106 
lemma natLeq_ordLeq_cinfinite: 
107 
assumes inf: "Cinfinite r" 

108 
shows "natLeq \<le>o r" 

109 
proof  

55811  110 
from inf have "natLeq \<le>o Field r" unfolding cinfinite_def 
111 
using infinite_iff_natLeq_ordLeq by blast 

54474  112 
also from inf have "Field r =o r" by (simp add: card_of_unique ordIso_symmetric) 
113 
finally show ?thesis . 

114 
qed 

115 

116 
lemma cinfinite_not_czero: "cinfinite r \<Longrightarrow> \<not> (r =o (czero :: 'a rel))" 

55811  117 
unfolding cinfinite_def by (cases "Field r = {}") (auto dest: czeroE) 
54474  118 

119 
lemma Cinfinite_Cnotzero: "Cinfinite r \<Longrightarrow> Cnotzero r" 

55811  120 
by (rule conjI[OF cinfinite_not_czero]) simp_all 
54474  121 

122 
lemma Cinfinite_cong: "\<lbrakk>r1 =o r2; Cinfinite r1\<rbrakk> \<Longrightarrow> Cinfinite r2" 

55811  123 
using Card_order_ordIso2[of r1 r2] unfolding cinfinite_def ordIso_iff_ordLeq 
124 
by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2]) 

54474  125 

126 
lemma cinfinite_mono: "\<lbrakk>r1 \<le>o r2; cinfinite r1\<rbrakk> \<Longrightarrow> cinfinite r2" 

55811  127 
unfolding cinfinite_def by (auto dest: card_of_ordLeq_infinite[OF card_of_mono2]) 
54474  128 

129 

60758  130 
subsection \<open>Binary sum\<close> 
54474  131 

132 
definition csum (infixr "+c" 65) where 

133 
"r1 +c r2 \<equiv> Field r1 <+> Field r2" 

134 

135 
lemma Field_csum: "Field (r +c s) = Inl ` Field r \<union> Inr ` Field s" 

136 
unfolding csum_def Field_card_of by auto 

137 

138 
lemma Card_order_csum: 

139 
"Card_order (r1 +c r2)" 

140 
unfolding csum_def by (simp add: card_of_Card_order) 

141 

142 
lemma csum_Cnotzero1: 

143 
"Cnotzero r1 \<Longrightarrow> Cnotzero (r1 +c r2)" 

55811  144 
unfolding csum_def using Cnotzero_imp_not_empty[of r1] Plus_eq_empty_conv[of "Field r1" "Field r2"] 
145 
card_of_ordIso_czero_iff_empty[of "Field r1 <+> Field r2"] by (auto intro: card_of_Card_order) 

54474  146 

147 
lemma card_order_csum: 

148 
assumes "card_order r1" "card_order r2" 

149 
shows "card_order (r1 +c r2)" 

150 
proof  

151 
have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto 

152 
thus ?thesis unfolding csum_def by (auto simp: card_of_card_order_on) 

153 
qed 

154 

155 
lemma cinfinite_csum: 

156 
"cinfinite r1 \<or> cinfinite r2 \<Longrightarrow> cinfinite (r1 +c r2)" 

157 
unfolding cinfinite_def csum_def by (auto simp: Field_card_of) 

158 

159 
lemma Cinfinite_csum1: 

160 
"Cinfinite r1 \<Longrightarrow> Cinfinite (r1 +c r2)" 

55811  161 
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of) 
54474  162 

54480
57e781b711b5
no need for 3way split with GFP for a handful of theorems
blanchet
parents:
54474
diff
changeset

163 
lemma Cinfinite_csum: 
57e781b711b5
no need for 3way split with GFP for a handful of theorems
blanchet
parents:
54474
diff
changeset

164 
"Cinfinite r1 \<or> Cinfinite r2 \<Longrightarrow> Cinfinite (r1 +c r2)" 
55811  165 
unfolding cinfinite_def csum_def by (rule conjI[OF _ card_of_Card_order]) (auto simp: Field_card_of) 
54480
57e781b711b5
no need for 3way split with GFP for a handful of theorems
blanchet
parents:
54474
diff
changeset

166 

55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

167 
lemma Cinfinite_csum_weak: 
54480
57e781b711b5
no need for 3way split with GFP for a handful of theorems
blanchet
parents:
54474
diff
changeset

168 
"\<lbrakk>Cinfinite r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 +c r2)" 
55811  169 
by (erule Cinfinite_csum1) 
54480
57e781b711b5
no need for 3way split with GFP for a handful of theorems
blanchet
parents:
54474
diff
changeset

170 

54474  171 
lemma csum_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 +c p2 =o r1 +c r2" 
172 
by (simp only: csum_def ordIso_Plus_cong) 

173 

174 
lemma csum_cong1: "p1 =o r1 \<Longrightarrow> p1 +c q =o r1 +c q" 

175 
by (simp only: csum_def ordIso_Plus_cong1) 

176 

177 
lemma csum_cong2: "p2 =o r2 \<Longrightarrow> q +c p2 =o q +c r2" 

178 
by (simp only: csum_def ordIso_Plus_cong2) 

179 

180 
lemma csum_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 +c p2 \<le>o r1 +c r2" 

181 
by (simp only: csum_def ordLeq_Plus_mono) 

182 

183 
lemma csum_mono1: "p1 \<le>o r1 \<Longrightarrow> p1 +c q \<le>o r1 +c q" 

184 
by (simp only: csum_def ordLeq_Plus_mono1) 

185 

186 
lemma csum_mono2: "p2 \<le>o r2 \<Longrightarrow> q +c p2 \<le>o q +c r2" 

187 
by (simp only: csum_def ordLeq_Plus_mono2) 

188 

189 
lemma ordLeq_csum1: "Card_order p1 \<Longrightarrow> p1 \<le>o p1 +c p2" 

190 
by (simp only: csum_def Card_order_Plus1) 

191 

192 
lemma ordLeq_csum2: "Card_order p2 \<Longrightarrow> p2 \<le>o p1 +c p2" 

193 
by (simp only: csum_def Card_order_Plus2) 

194 

195 
lemma csum_com: "p1 +c p2 =o p2 +c p1" 

196 
by (simp only: csum_def card_of_Plus_commute) 

197 

198 
lemma csum_assoc: "(p1 +c p2) +c p3 =o p1 +c p2 +c p3" 

199 
by (simp only: csum_def Field_card_of card_of_Plus_assoc) 

200 

201 
lemma Cfinite_csum: "\<lbrakk>Cfinite r; Cfinite s\<rbrakk> \<Longrightarrow> Cfinite (r +c s)" 

202 
unfolding cfinite_def csum_def Field_card_of using card_of_card_order_on by simp 

203 

204 
lemma csum_csum: "(r1 +c r2) +c (r3 +c r4) =o (r1 +c r3) +c (r2 +c r4)" 

205 
proof  

206 
have "(r1 +c r2) +c (r3 +c r4) =o r1 +c r2 +c (r3 +c r4)" 

55811  207 
by (rule csum_assoc) 
54474  208 
also have "r1 +c r2 +c (r3 +c r4) =o r1 +c (r2 +c r3) +c r4" 
55811  209 
by (intro csum_assoc csum_cong2 ordIso_symmetric) 
54474  210 
also have "r1 +c (r2 +c r3) +c r4 =o r1 +c (r3 +c r2) +c r4" 
55811  211 
by (intro csum_com csum_cong1 csum_cong2) 
54474  212 
also have "r1 +c (r3 +c r2) +c r4 =o r1 +c r3 +c r2 +c r4" 
55811  213 
by (intro csum_assoc csum_cong2 ordIso_symmetric) 
54474  214 
also have "r1 +c r3 +c r2 +c r4 =o (r1 +c r3) +c (r2 +c r4)" 
55811  215 
by (intro csum_assoc ordIso_symmetric) 
54474  216 
finally show ?thesis . 
217 
qed 

218 

219 
lemma Plus_csum: "A <+> B =o A +c B" 

220 
by (simp only: csum_def Field_card_of card_of_refl) 

221 

222 
lemma Un_csum: "A \<union> B \<le>o A +c B" 

223 
using ordLeq_ordIso_trans[OF card_of_Un_Plus_ordLeq Plus_csum] by blast 

224 

225 

60758  226 
subsection \<open>One\<close> 
54474  227 

228 
definition cone where 

229 
"cone = card_of {()}" 

230 

231 
lemma Card_order_cone: "Card_order cone" 

232 
unfolding cone_def by (rule card_of_Card_order) 

233 

234 
lemma Cfinite_cone: "Cfinite cone" 

235 
unfolding cfinite_def by (simp add: Card_order_cone) 

236 

237 
lemma cone_not_czero: "\<not> (cone =o czero)" 

55811  238 
unfolding czero_def cone_def ordIso_iff_ordLeq using card_of_empty3 empty_not_insert by blast 
54474  239 

240 
lemma cone_ordLeq_Cnotzero: "Cnotzero r \<Longrightarrow> cone \<le>o r" 

55811  241 
unfolding cone_def by (rule Card_order_singl_ordLeq) (auto intro: czeroI) 
54474  242 

243 

60758  244 
subsection \<open>Two\<close> 
54474  245 

246 
definition ctwo where 

247 
"ctwo = UNIV :: bool set" 

248 

249 
lemma Card_order_ctwo: "Card_order ctwo" 

250 
unfolding ctwo_def by (rule card_of_Card_order) 

251 

252 
lemma ctwo_not_czero: "\<not> (ctwo =o czero)" 

253 
using card_of_empty3[of "UNIV :: bool set"] ordIso_iff_ordLeq 

55811  254 
unfolding czero_def ctwo_def using UNIV_not_empty by auto 
54474  255 

256 
lemma ctwo_Cnotzero: "Cnotzero ctwo" 

257 
by (simp add: ctwo_not_czero Card_order_ctwo) 

258 

259 

60758  260 
subsection \<open>Family sum\<close> 
54474  261 

262 
definition Csum where 

263 
"Csum r rs \<equiv> SIGMA i : Field r. Field (rs i)" 

264 

265 
(* Similar setup to the one for SIGMA from theory Big_Operators: *) 

266 
syntax "_Csum" :: 

267 
"pttrn => ('a * 'a) set => 'b * 'b set => (('a * 'b) * ('a * 'b)) set" 

268 
("(3CSUM _:_. _)" [0, 51, 10] 10) 

269 

270 
translations 

271 
"CSUM i:r. rs" == "CONST Csum r (%i. rs)" 

272 

273 
lemma SIGMA_CSUM: "SIGMA i : I. As i = (CSUM i : I. As i )" 

274 
by (auto simp: Csum_def Field_card_of) 

275 

276 
(* NB: Always, under the cardinal operator, 

277 
operations on sets are reduced automatically to operations on cardinals. 

278 
This should make cardinal reasoning more direct and natural. *) 

279 

280 

60758  281 
subsection \<open>Product\<close> 
54474  282 

283 
definition cprod (infixr "*c" 80) where 

284 
"r1 *c r2 = Field r1 <*> Field r2" 

285 

286 
lemma card_order_cprod: 

287 
assumes "card_order r1" "card_order r2" 

288 
shows "card_order (r1 *c r2)" 

289 
proof  

290 
have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto 

291 
thus ?thesis by (auto simp: cprod_def card_of_card_order_on) 

292 
qed 

293 

294 
lemma Card_order_cprod: "Card_order (r1 *c r2)" 

295 
by (simp only: cprod_def Field_card_of card_of_card_order_on) 

296 

297 
lemma cprod_mono1: "p1 \<le>o r1 \<Longrightarrow> p1 *c q \<le>o r1 *c q" 

298 
by (simp only: cprod_def ordLeq_Times_mono1) 

299 

300 
lemma cprod_mono2: "p2 \<le>o r2 \<Longrightarrow> q *c p2 \<le>o q *c r2" 

301 
by (simp only: cprod_def ordLeq_Times_mono2) 

302 

55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

303 
lemma cprod_mono: "\<lbrakk>p1 \<le>o r1; p2 \<le>o r2\<rbrakk> \<Longrightarrow> p1 *c p2 \<le>o r1 *c r2" 
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

304 
by (rule ordLeq_transitive[OF cprod_mono1 cprod_mono2]) 
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

305 

54474  306 
lemma ordLeq_cprod2: "\<lbrakk>Cnotzero p1; Card_order p2\<rbrakk> \<Longrightarrow> p2 \<le>o p1 *c p2" 
55811  307 
unfolding cprod_def by (rule Card_order_Times2) (auto intro: czeroI) 
54474  308 

309 
lemma cinfinite_cprod: "\<lbrakk>cinfinite r1; cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)" 

310 
by (simp add: cinfinite_def cprod_def Field_card_of infinite_cartesian_product) 

311 

312 
lemma cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> cinfinite (r1 *c r2)" 

55811  313 
by (rule cinfinite_mono) (auto intro: ordLeq_cprod2) 
54474  314 

315 
lemma Cinfinite_cprod2: "\<lbrakk>Cnotzero r1; Cinfinite r2\<rbrakk> \<Longrightarrow> Cinfinite (r1 *c r2)" 

316 
by (blast intro: cinfinite_cprod2 Card_order_cprod) 

317 

55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

318 
lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2" 
55866  319 
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono) 
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

320 

3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

321 
lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2" 
55866  322 
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1) 
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

323 

3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

324 
lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2" 
55866  325 
unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2) 
55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

326 

54474  327 
lemma cprod_com: "p1 *c p2 =o p2 *c p1" 
328 
by (simp only: cprod_def card_of_Times_commute) 

329 

330 
lemma card_of_Csum_Times: 

331 
"\<forall>i \<in> I. A i \<le>o B \<Longrightarrow> (CSUM i : I. A i ) \<le>o I *c B" 

56191  332 
by (simp only: Csum_def cprod_def Field_card_of card_of_Sigma_mono1) 
54474  333 

334 
lemma card_of_Csum_Times': 

335 
assumes "Card_order r" "\<forall>i \<in> I. A i \<le>o r" 

336 
shows "(CSUM i : I. A i ) \<le>o I *c r" 

337 
proof  

338 
from assms(1) have *: "r =o Field r" by (simp add: card_of_unique) 

339 
with assms(2) have "\<forall>i \<in> I. A i \<le>o Field r" by (blast intro: ordLeq_ordIso_trans) 

340 
hence "(CSUM i : I. A i ) \<le>o I *c Field r" by (simp only: card_of_Csum_Times) 

341 
also from * have "I *c Field r \<le>o I *c r" 

342 
by (simp only: Field_card_of card_of_refl cprod_def ordIso_imp_ordLeq) 

343 
finally show ?thesis . 

344 
qed 

345 

346 
lemma cprod_csum_distrib1: "r1 *c r2 +c r1 *c r3 =o r1 *c (r2 +c r3)" 

347 
unfolding csum_def cprod_def by (simp add: Field_card_of card_of_Times_Plus_distrib ordIso_symmetric) 

348 

349 
lemma csum_absorb2': "\<lbrakk>Card_order r2; r1 \<le>o r2; cinfinite r1 \<or> cinfinite r2\<rbrakk> \<Longrightarrow> r1 +c r2 =o r2" 

55811  350 
unfolding csum_def by (rule conjunct2[OF Card_order_Plus_infinite]) 
351 
(auto simp: cinfinite_def dest: cinfinite_mono) 

54474  352 

353 
lemma csum_absorb1': 

354 
assumes card: "Card_order r2" 

355 
and r12: "r1 \<le>o r2" and cr12: "cinfinite r1 \<or> cinfinite r2" 

356 
shows "r2 +c r1 =o r2" 

357 
by (rule ordIso_transitive, rule csum_com, rule csum_absorb2', (simp only: assms)+) 

358 

359 
lemma csum_absorb1: "\<lbrakk>Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r2 +c r1 =o r2" 

360 
by (rule csum_absorb1') auto 

361 

362 

60758  363 
subsection \<open>Exponentiation\<close> 
54474  364 

365 
definition cexp (infixr "^c" 90) where 

366 
"r1 ^c r2 \<equiv> Func (Field r2) (Field r1)" 

367 

368 
lemma Card_order_cexp: "Card_order (r1 ^c r2)" 

369 
unfolding cexp_def by (rule card_of_Card_order) 

370 

371 
lemma cexp_mono': 

372 
assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2" 

373 
and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}" 

374 
shows "p1 ^c p2 \<le>o r1 ^c r2" 

375 
proof(cases "Field p1 = {}") 

376 
case True 

55811  377 
hence "Field p2 \<noteq> {} \<Longrightarrow> Func (Field p2) {} = {}" unfolding Func_is_emp by simp 
378 
with True have "Field Func (Field p2) (Field p1) \<le>o cone" 

54474  379 
unfolding cone_def Field_card_of 
55811  380 
by (cases "Field p2 = {}", auto intro: surj_imp_ordLeq simp: Func_empty) 
54474  381 
hence "Func (Field p2) (Field p1) \<le>o cone" by (simp add: Field_card_of cexp_def) 
382 
hence "p1 ^c p2 \<le>o cone" unfolding cexp_def . 

383 
thus ?thesis 

384 
proof (cases "Field p2 = {}") 

385 
case True 

386 
with n have "Field r2 = {}" . 

55604  387 
hence "cone \<le>o r1 ^c r2" unfolding cone_def cexp_def Func_def 
388 
by (auto intro: card_of_ordLeqI[where f="\<lambda>_ _. undefined"]) 

60758  389 
thus ?thesis using \<open>p1 ^c p2 \<le>o cone\<close> ordLeq_transitive by auto 
54474  390 
next 
391 
case False with True have "Field (p1 ^c p2) =o czero" 

392 
unfolding card_of_ordIso_czero_iff_empty cexp_def Field_card_of Func_def by auto 

393 
thus ?thesis unfolding cexp_def card_of_ordIso_czero_iff_empty Field_card_of 

394 
by (simp add: card_of_empty) 

395 
qed 

396 
next 

397 
case False 

398 
have 1: "Field p1 \<le>o Field r1" and 2: "Field p2 \<le>o Field r2" 

399 
using 1 2 by (auto simp: card_of_mono2) 

400 
obtain f1 where f1: "f1 ` Field r1 = Field p1" 

401 
using 1 unfolding card_of_ordLeq2[OF False, symmetric] by auto 

402 
obtain f2 where f2: "inj_on f2 (Field p2)" "f2 ` Field p2 \<subseteq> Field r2" 

403 
using 2 unfolding card_of_ordLeq[symmetric] by blast 

404 
have 0: "Func_map (Field p2) f1 f2 ` (Field (r1 ^c r2)) = Field (p1 ^c p2)" 

405 
unfolding cexp_def Field_card_of using Func_map_surj[OF f1 f2 n, symmetric] . 

406 
have 00: "Field (p1 ^c p2) \<noteq> {}" unfolding cexp_def Field_card_of Func_is_emp 

407 
using False by simp 

408 
show ?thesis 

409 
using 0 card_of_ordLeq2[OF 00] unfolding cexp_def Field_card_of by blast 

410 
qed 

411 

412 
lemma cexp_mono: 

413 
assumes 1: "p1 \<le>o r1" and 2: "p2 \<le>o r2" 

414 
and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2" 

415 
shows "p1 ^c p2 \<le>o r1 ^c r2" 

55811  416 
by (rule cexp_mono'[OF 1 2 czeroE[OF n[OF czeroI[OF card]]]]) 
54474  417 

418 
lemma cexp_mono1: 

419 
assumes 1: "p1 \<le>o r1" and q: "Card_order q" 

420 
shows "p1 ^c q \<le>o r1 ^c q" 

421 
using ordLeq_refl[OF q] by (rule cexp_mono[OF 1]) (auto simp: q) 

422 

423 
lemma cexp_mono2': 

424 
assumes 2: "p2 \<le>o r2" and q: "Card_order q" 

425 
and n: "Field p2 = {} \<Longrightarrow> Field r2 = {}" 

426 
shows "q ^c p2 \<le>o q ^c r2" 

427 
using ordLeq_refl[OF q] by (rule cexp_mono'[OF _ 2 n]) auto 

428 

429 
lemma cexp_mono2: 

430 
assumes 2: "p2 \<le>o r2" and q: "Card_order q" 

431 
and n: "p2 =o czero \<Longrightarrow> r2 =o czero" and card: "Card_order p2" 

432 
shows "q ^c p2 \<le>o q ^c r2" 

433 
using ordLeq_refl[OF q] by (rule cexp_mono[OF _ 2 n card]) auto 

434 

435 
lemma cexp_mono2_Cnotzero: 

436 
assumes "p2 \<le>o r2" "Card_order q" "Cnotzero p2" 

437 
shows "q ^c p2 \<le>o q ^c r2" 

55811  438 
using assms(3) czeroI by (blast intro: cexp_mono2'[OF assms(1,2)]) 
54474  439 

440 
lemma cexp_cong: 

441 
assumes 1: "p1 =o r1" and 2: "p2 =o r2" 

442 
and Cr: "Card_order r2" 

443 
and Cp: "Card_order p2" 

444 
shows "p1 ^c p2 =o r1 ^c r2" 

445 
proof  

446 
obtain f where "bij_betw f (Field p2) (Field r2)" 

447 
using 2 card_of_ordIso[of "Field p2" "Field r2"] card_of_cong by auto 

448 
hence 0: "Field p2 = {} \<longleftrightarrow> Field r2 = {}" unfolding bij_betw_def by auto 

449 
have r: "p2 =o czero \<Longrightarrow> r2 =o czero" 

450 
and p: "r2 =o czero \<Longrightarrow> p2 =o czero" 

451 
using 0 Cr Cp czeroE czeroI by auto 

452 
show ?thesis using 0 1 2 unfolding ordIso_iff_ordLeq 

55811  453 
using r p cexp_mono[OF _ _ _ Cp] cexp_mono[OF _ _ _ Cr] by blast 
54474  454 
qed 
455 

456 
lemma cexp_cong1: 

457 
assumes 1: "p1 =o r1" and q: "Card_order q" 

458 
shows "p1 ^c q =o r1 ^c q" 

459 
by (rule cexp_cong[OF 1 _ q q]) (rule ordIso_refl[OF q]) 

460 

461 
lemma cexp_cong2: 

462 
assumes 2: "p2 =o r2" and q: "Card_order q" and p: "Card_order p2" 

463 
shows "q ^c p2 =o q ^c r2" 

464 
by (rule cexp_cong[OF _ 2]) (auto simp only: ordIso_refl Card_order_ordIso2[OF p 2] q p) 

465 

466 
lemma cexp_cone: 

467 
assumes "Card_order r" 

468 
shows "r ^c cone =o r" 

469 
proof  

470 
have "r ^c cone =o Field r" 

471 
unfolding cexp_def cone_def Field_card_of Func_empty 

472 
card_of_ordIso[symmetric] bij_betw_def Func_def inj_on_def image_def 

473 
by (rule exI[of _ "\<lambda>f. f ()"]) auto 

474 
also have "Field r =o r" by (rule card_of_Field_ordIso[OF assms]) 

475 
finally show ?thesis . 

476 
qed 

477 

478 
lemma cexp_cprod: 

479 
assumes r1: "Card_order r1" 

480 
shows "(r1 ^c r2) ^c r3 =o r1 ^c (r2 *c r3)" (is "?L =o ?R") 

481 
proof  

482 
have "?L =o r1 ^c (r3 *c r2)" 

483 
unfolding cprod_def cexp_def Field_card_of 

484 
using card_of_Func_Times by(rule ordIso_symmetric) 

485 
also have "r1 ^c (r3 *c r2) =o ?R" 

486 
apply(rule cexp_cong2) using cprod_com r1 by (auto simp: Card_order_cprod) 

487 
finally show ?thesis . 

488 
qed 

489 

490 
lemma cprod_infinite1': "\<lbrakk>Cinfinite r; Cnotzero p; p \<le>o r\<rbrakk> \<Longrightarrow> r *c p =o r" 

491 
unfolding cinfinite_def cprod_def 

492 
by (rule Card_order_Times_infinite[THEN conjunct1]) (blast intro: czeroI)+ 

493 

55851
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

494 
lemma cprod_infinite: "Cinfinite r \<Longrightarrow> r *c r =o r" 
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

495 
using cprod_infinite1' Cinfinite_Cnotzero ordLeq_refl by blast 
3d40cf74726c
optimize cardinal bounds involving natLeq (omega)
blanchet
parents:
55811
diff
changeset

496 

54474  497 
lemma cexp_cprod_ordLeq: 
498 
assumes r1: "Card_order r1" and r2: "Cinfinite r2" 

499 
and r3: "Cnotzero r3" "r3 \<le>o r2" 

500 
shows "(r1 ^c r2) ^c r3 =o r1 ^c r2" (is "?L =o ?R") 

501 
proof 

502 
have "?L =o r1 ^c (r2 *c r3)" using cexp_cprod[OF r1] . 

503 
also have "r1 ^c (r2 *c r3) =o ?R" 

504 
apply(rule cexp_cong2) 

505 
apply(rule cprod_infinite1'[OF r2 r3]) using r1 r2 by (fastforce simp: Card_order_cprod)+ 

506 
finally show ?thesis . 

507 
qed 

508 

509 
lemma Cnotzero_UNIV: "Cnotzero UNIV" 

510 
by (auto simp: card_of_Card_order card_of_ordIso_czero_iff_empty) 

511 

512 
lemma ordLess_ctwo_cexp: 

513 
assumes "Card_order r" 

514 
shows "r <o ctwo ^c r" 

515 
proof  

516 
have "r <o Pow (Field r)" using assms by (rule Card_order_Pow) 

517 
also have "Pow (Field r) =o ctwo ^c r" 

518 
unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) 

519 
finally show ?thesis . 

520 
qed 

521 

522 
lemma ordLeq_cexp1: 

523 
assumes "Cnotzero r" "Card_order q" 

524 
shows "q \<le>o q ^c r" 

525 
proof (cases "q =o (czero :: 'a rel)") 

526 
case True thus ?thesis by (simp only: card_of_empty cexp_def czero_def ordIso_ordLeq_trans) 

527 
next 

528 
case False 

529 
thus ?thesis 

530 
apply  

531 
apply (rule ordIso_ordLeq_trans) 

532 
apply (rule ordIso_symmetric) 

533 
apply (rule cexp_cone) 

534 
apply (rule assms(2)) 

535 
apply (rule cexp_mono2) 

536 
apply (rule cone_ordLeq_Cnotzero) 

537 
apply (rule assms(1)) 

538 
apply (rule assms(2)) 

539 
apply (rule notE) 

540 
apply (rule cone_not_czero) 

541 
apply assumption 

542 
apply (rule Card_order_cone) 

543 
done 

544 
qed 

545 

546 
lemma ordLeq_cexp2: 

547 
assumes "ctwo \<le>o q" "Card_order r" 

548 
shows "r \<le>o q ^c r" 

549 
proof (cases "r =o (czero :: 'a rel)") 

550 
case True thus ?thesis by (simp only: card_of_empty cexp_def czero_def ordIso_ordLeq_trans) 

551 
next 

552 
case False thus ?thesis 

553 
apply  

554 
apply (rule ordLess_imp_ordLeq) 

555 
apply (rule ordLess_ordLeq_trans) 

556 
apply (rule ordLess_ctwo_cexp) 

557 
apply (rule assms(2)) 

558 
apply (rule cexp_mono1) 

559 
apply (rule assms(1)) 

560 
apply (rule assms(2)) 

561 
done 

562 
qed 

563 

564 
lemma cinfinite_cexp: "\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> cinfinite (q ^c r)" 

55811  565 
by (rule cinfinite_mono[OF ordLeq_cexp2]) simp_all 
54474  566 

567 
lemma Cinfinite_cexp: 

568 
"\<lbrakk>ctwo \<le>o q; Cinfinite r\<rbrakk> \<Longrightarrow> Cinfinite (q ^c r)" 

569 
by (simp add: cinfinite_cexp Card_order_cexp) 

570 

571 
lemma ctwo_ordLess_natLeq: "ctwo <o natLeq" 

54581
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

572 
unfolding ctwo_def using finite_UNIV natLeq_cinfinite natLeq_Card_order 
1502a1f707d9
eliminated dependence of Cardinals_FP on Set_Intervals, more precise imports
traytel
parents:
54578
diff
changeset

573 
by (intro Cfinite_ordLess_Cinfinite) (auto simp: cfinite_def card_of_Card_order) 
54474  574 

575 
lemma ctwo_ordLess_Cinfinite: "Cinfinite r \<Longrightarrow> ctwo <o r" 

55811  576 
by (rule ordLess_ordLeq_trans[OF ctwo_ordLess_natLeq natLeq_ordLeq_cinfinite]) 
54474  577 

578 
lemma ctwo_ordLeq_Cinfinite: 

579 
assumes "Cinfinite r" 

580 
shows "ctwo \<le>o r" 

581 
by (rule ordLess_imp_ordLeq[OF ctwo_ordLess_Cinfinite[OF assms]]) 

582 

583 
lemma Un_Cinfinite_bound: "\<lbrakk>A \<le>o r; B \<le>o r; Cinfinite r\<rbrakk> \<Longrightarrow> A \<union> B \<le>o r" 

584 
by (auto simp add: cinfinite_def card_of_Un_ordLeq_infinite_Field) 

585 

586 
lemma UNION_Cinfinite_bound: "\<lbrakk>I \<le>o r; \<forall>i \<in> I. A i \<le>o r; Cinfinite r\<rbrakk> \<Longrightarrow> \<Union>i \<in> I. A i \<le>o r" 

587 
by (auto simp add: card_of_UNION_ordLeq_infinite_Field cinfinite_def) 

588 

589 
lemma csum_cinfinite_bound: 

590 
assumes "p \<le>o r" "q \<le>o r" "Card_order p" "Card_order q" "Cinfinite r" 

591 
shows "p +c q \<le>o r" 

592 
proof  

593 
from assms(14) have "Field p \<le>o r" "Field q \<le>o r" 

594 
unfolding card_order_on_def using card_of_least ordLeq_transitive by blast+ 

595 
with assms show ?thesis unfolding cinfinite_def csum_def 

596 
by (blast intro: card_of_Plus_ordLeq_infinite_Field) 

597 
qed 

598 

599 
lemma cprod_cinfinite_bound: 

600 
assumes "p \<le>o r" "q \<le>o r" "Card_order p" "Card_order q" "Cinfinite r" 

601 
shows "p *c q \<le>o r" 

602 
proof  

603 
from assms(14) have "Field p \<le>o r" "Field q \<le>o r" 

604 
unfolding card_order_on_def using card_of_least ordLeq_transitive by blast+ 

605 
with assms show ?thesis unfolding cinfinite_def cprod_def 

606 
by (blast intro: card_of_Times_ordLeq_infinite_Field) 

607 
qed 

608 

609 
lemma cprod_csum_cexp: 

610 
"r1 *c r2 \<le>o (r1 +c r2) ^c ctwo" 

611 
unfolding cprod_def csum_def cexp_def ctwo_def Field_card_of 

612 
proof  

613 
let ?f = "\<lambda>(a, b). %x. if x then Inl a else Inr b" 

614 
have "inj_on ?f (Field r1 \<times> Field r2)" (is "inj_on _ ?LHS") 

615 
by (auto simp: inj_on_def fun_eq_iff split: bool.split) 

616 
moreover 

617 
have "?f ` ?LHS \<subseteq> Func (UNIV :: bool set) (Field r1 <+> Field r2)" (is "_ \<subseteq> ?RHS") 

618 
by (auto simp: Func_def) 

619 
ultimately show "?LHS \<le>o ?RHS" using card_of_ordLeq by blast 

620 
qed 

621 

622 
lemma Cfinite_cprod_Cinfinite: "\<lbrakk>Cfinite r; Cinfinite s\<rbrakk> \<Longrightarrow> r *c s \<le>o s" 

623 
by (intro cprod_cinfinite_bound) 

624 
(auto intro: ordLeq_refl ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite]) 

625 

626 
lemma cprod_cexp: "(r *c s) ^c t =o r ^c t *c s ^c t" 

627 
unfolding cprod_def cexp_def Field_card_of by (rule Func_Times_Range) 

628 

629 
lemma cprod_cexp_csum_cexp_Cinfinite: 

630 
assumes t: "Cinfinite t" 

631 
shows "(r *c s) ^c t \<le>o (r +c s) ^c t" 

632 
proof  

633 
have "(r *c s) ^c t \<le>o ((r +c s) ^c ctwo) ^c t" 

634 
by (rule cexp_mono1[OF cprod_csum_cexp conjunct2[OF t]]) 

635 
also have "((r +c s) ^c ctwo) ^c t =o (r +c s) ^c (ctwo *c t)" 

636 
by (rule cexp_cprod[OF Card_order_csum]) 

637 
also have "(r +c s) ^c (ctwo *c t) =o (r +c s) ^c (t *c ctwo)" 

638 
by (rule cexp_cong2[OF cprod_com Card_order_csum Card_order_cprod]) 

639 
also have "(r +c s) ^c (t *c ctwo) =o ((r +c s) ^c t) ^c ctwo" 

640 
by (rule ordIso_symmetric[OF cexp_cprod[OF Card_order_csum]]) 

641 
also have "((r +c s) ^c t) ^c ctwo =o (r +c s) ^c t" 

642 
by (rule cexp_cprod_ordLeq[OF Card_order_csum t ctwo_Cnotzero ctwo_ordLeq_Cinfinite[OF t]]) 

643 
finally show ?thesis . 

644 
qed 

645 

646 
lemma Cfinite_cexp_Cinfinite: 

647 
assumes s: "Cfinite s" and t: "Cinfinite t" 

648 
shows "s ^c t \<le>o ctwo ^c t" 

649 
proof (cases "s \<le>o ctwo") 

650 
case True thus ?thesis using t by (blast intro: cexp_mono1) 

651 
next 

652 
case False 

55811  653 
hence "ctwo \<le>o s" using ordLeq_total[of s ctwo] Card_order_ctwo s 
654 
by (auto intro: card_order_on_well_order_on) 

655 
hence "Cnotzero s" using Cnotzero_mono[OF ctwo_Cnotzero] s by blast 

656 
hence st: "Cnotzero (s *c t)" by (intro Cinfinite_Cnotzero[OF Cinfinite_cprod2]) (auto simp: t) 

54474  657 
have "s ^c t \<le>o (ctwo ^c s) ^c t" 
658 
using assms by (blast intro: cexp_mono1 ordLess_imp_ordLeq[OF ordLess_ctwo_cexp]) 

659 
also have "(ctwo ^c s) ^c t =o ctwo ^c (s *c t)" 

660 
by (blast intro: Card_order_ctwo cexp_cprod) 

661 
also have "ctwo ^c (s *c t) \<le>o ctwo ^c t" 

662 
using assms st by (intro cexp_mono2_Cnotzero Cfinite_cprod_Cinfinite Card_order_ctwo) 

663 
finally show ?thesis . 

664 
qed 

665 

666 
lemma csum_Cfinite_cexp_Cinfinite: 

667 
assumes r: "Card_order r" and s: "Cfinite s" and t: "Cinfinite t" 

668 
shows "(r +c s) ^c t \<le>o (r +c ctwo) ^c t" 

669 
proof (cases "Cinfinite r") 

670 
case True 

671 
hence "r +c s =o r" by (intro csum_absorb1 ordLess_imp_ordLeq[OF Cfinite_ordLess_Cinfinite] s) 

672 
hence "(r +c s) ^c t =o r ^c t" using t by (blast intro: cexp_cong1) 

673 
also have "r ^c t \<le>o (r +c ctwo) ^c t" using t by (blast intro: cexp_mono1 ordLeq_csum1 r) 

674 
finally show ?thesis . 

675 
next 

676 
case False 

677 
with r have "Cfinite r" unfolding cinfinite_def cfinite_def by auto 

678 
hence "Cfinite (r +c s)" by (intro Cfinite_csum s) 

679 
hence "(r +c s) ^c t \<le>o ctwo ^c t" by (intro Cfinite_cexp_Cinfinite t) 

680 
also have "ctwo ^c t \<le>o (r +c ctwo) ^c t" using t 

681 
by (blast intro: cexp_mono1 ordLeq_csum2 Card_order_ctwo) 

682 
finally show ?thesis . 

683 
qed 

684 

685 
(* cardSuc *) 

686 

687 
lemma Cinfinite_cardSuc: "Cinfinite r \<Longrightarrow> Cinfinite (cardSuc r)" 

688 
by (simp add: cinfinite_def cardSuc_Card_order cardSuc_finite) 

689 

690 
lemma cardSuc_UNION_Cinfinite: 

691 
assumes "Cinfinite r" "relChain (cardSuc r) As" "B \<le> (UN i : Field (cardSuc r). As i)" "B <=o r" 

692 
shows "EX i : Field (cardSuc r). B \<le> As i" 

693 
using cardSuc_UNION assms unfolding cinfinite_def by blast 

694 

695 
end 