author | hoelzl |
Wed, 18 Jun 2014 07:31:12 +0200 | |
changeset 57275 | 0ddb5b755cdc |
parent 55851 | 3d40cf74726c |
child 58127 | b7cab82f488e |
permissions | -rw-r--r-- |
49310 | 1 |
(* Title: HOL/Cardinals/Cardinal_Arithmetic.thy |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
2 |
Author: Dmitriy Traytel, TU Muenchen |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
3 |
Copyright 2012 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
4 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
5 |
Cardinal arithmetic. |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
6 |
*) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
7 |
|
55102 | 8 |
header {* Cardinal Arithmetic *} |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
9 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
10 |
theory Cardinal_Arithmetic |
55056 | 11 |
imports BNF_Cardinal_Arithmetic Cardinal_Order_Relation |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
12 |
begin |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
13 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
14 |
subsection {* Binary sum *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
15 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
16 |
lemma csum_Cnotzero2: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
17 |
"Cnotzero r2 \<Longrightarrow> Cnotzero (r1 +c r2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
18 |
unfolding csum_def |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
19 |
by (metis Cnotzero_imp_not_empty Field_card_of Plus_eq_empty_conv card_of_card_order_on czeroE) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
20 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
21 |
lemma single_cone: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
22 |
"|{x}| =o cone" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
23 |
proof - |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
24 |
let ?f = "\<lambda>x. ()" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
25 |
have "bij_betw ?f {x} {()}" unfolding bij_betw_def by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
26 |
thus ?thesis unfolding cone_def using card_of_ordIso by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
27 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
28 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
29 |
lemma cone_Cnotzero: "Cnotzero cone" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
30 |
by (simp add: cone_not_czero Card_order_cone) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
31 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
32 |
lemma cone_ordLeq_ctwo: "cone \<le>o ctwo" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
33 |
unfolding cone_def ctwo_def card_of_ordLeq[symmetric] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
34 |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
35 |
lemma csum_czero1: "Card_order r \<Longrightarrow> r +c czero =o r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
36 |
unfolding czero_def csum_def Field_card_of |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
37 |
by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty1] card_of_Field_ordIso]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
38 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
39 |
lemma csum_czero2: "Card_order r \<Longrightarrow> czero +c r =o r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
40 |
unfolding czero_def csum_def Field_card_of |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
41 |
by (rule ordIso_transitive[OF ordIso_symmetric[OF card_of_Plus_empty2] card_of_Field_ordIso]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
42 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
43 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
44 |
subsection {* Product *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
45 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
46 |
lemma Times_cprod: "|A \<times> B| =o |A| *c |B|" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
47 |
by (simp only: cprod_def Field_card_of card_of_refl) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
48 |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
49 |
lemma card_of_Times_singleton: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
50 |
fixes A :: "'a set" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
51 |
shows "|A \<times> {x}| =o |A|" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
52 |
proof - |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
53 |
def f \<equiv> "\<lambda>(a::'a,b::'b). (a)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
54 |
have "A \<subseteq> f ` (A <*> {x})" unfolding f_def by (auto simp: image_iff) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
55 |
hence "bij_betw f (A <*> {x}) A" unfolding bij_betw_def inj_on_def f_def by fastforce |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
56 |
thus ?thesis using card_of_ordIso by blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
57 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
58 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
59 |
lemma cprod_assoc: "(r *c s) *c t =o r *c s *c t" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
60 |
unfolding cprod_def Field_card_of by (rule card_of_Times_assoc) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
61 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
62 |
lemma cprod_czero: "r *c czero =o czero" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
63 |
unfolding cprod_def czero_def Field_card_of by (simp add: card_of_empty_ordIso) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
64 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
65 |
lemma cprod_cone: "Card_order r \<Longrightarrow> r *c cone =o r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
66 |
unfolding cprod_def cone_def Field_card_of |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
67 |
by (drule card_of_Field_ordIso) (erule ordIso_transitive[OF card_of_Times_singleton]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
68 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
69 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
70 |
lemma ordLeq_cprod1: "\<lbrakk>Card_order p1; Cnotzero p2\<rbrakk> \<Longrightarrow> p1 \<le>o p1 *c p2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
71 |
unfolding cprod_def by (metis Card_order_Times1 czeroI) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
72 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
73 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
74 |
subsection {* Exponentiation *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
75 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
76 |
lemma cexp_czero: "r ^c czero =o cone" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
77 |
unfolding cexp_def czero_def Field_card_of Func_empty by (rule single_cone) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
78 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
79 |
lemma Pow_cexp_ctwo: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
80 |
"|Pow A| =o ctwo ^c |A|" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
81 |
unfolding ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
82 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
83 |
lemma Cnotzero_cexp: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
84 |
assumes "Cnotzero q" "Card_order r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
85 |
shows "Cnotzero (q ^c r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
86 |
proof (cases "r =o czero") |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
87 |
case False thus ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
88 |
apply - |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
89 |
apply (rule Cnotzero_mono) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
90 |
apply (rule assms(1)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
91 |
apply (rule Card_order_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
92 |
apply (rule ordLeq_cexp1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
93 |
apply (rule conjI) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
94 |
apply (rule notI) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
95 |
apply (erule notE) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
96 |
apply (rule ordIso_transitive) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
97 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
98 |
apply (rule czero_ordIso) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
99 |
apply (rule assms(2)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
100 |
apply (rule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
101 |
apply (rule assms(1)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
102 |
done |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
103 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
104 |
case True thus ?thesis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
105 |
apply - |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
106 |
apply (rule Cnotzero_mono) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
107 |
apply (rule cone_Cnotzero) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
108 |
apply (rule Card_order_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
109 |
apply (rule ordIso_imp_ordLeq) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
110 |
apply (rule ordIso_symmetric) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
111 |
apply (rule ordIso_transitive) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
112 |
apply (rule cexp_cong2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
113 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
114 |
apply (rule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
115 |
apply (rule assms(1)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
116 |
apply (rule assms(2)) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
117 |
apply (rule cexp_czero) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
118 |
done |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
119 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
120 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
121 |
lemma Cinfinite_ctwo_cexp: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
122 |
"Cinfinite r \<Longrightarrow> Cinfinite (ctwo ^c r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
123 |
unfolding ctwo_def cexp_def cinfinite_def Field_card_of |
54475 | 124 |
by (rule conjI, rule infinite_Func, auto) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
125 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
126 |
lemma cone_ordLeq_iff_Field: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
127 |
assumes "cone \<le>o r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
128 |
shows "Field r \<noteq> {}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
129 |
proof (rule ccontr) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
130 |
assume "\<not> Field r \<noteq> {}" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
131 |
hence "Field r = {}" by simp |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
132 |
thus False using card_of_empty3 |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
133 |
card_of_mono2[OF assms] Cnotzero_imp_not_empty[OF cone_Cnotzero] by auto |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
134 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
135 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
136 |
lemma cone_ordLeq_cexp: "cone \<le>o r1 \<Longrightarrow> cone \<le>o r1 ^c r2" |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
137 |
by (simp add: cexp_def cone_def Func_non_emp cone_ordLeq_iff_Field) |
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
138 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
139 |
lemma Card_order_czero: "Card_order czero" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
140 |
by (simp only: card_of_Card_order czero_def) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
141 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
142 |
lemma cexp_mono2'': |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
143 |
assumes 2: "p2 \<le>o r2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
144 |
and n1: "Cnotzero q" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
145 |
and n2: "Card_order p2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
146 |
shows "q ^c p2 \<le>o q ^c r2" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
147 |
proof (cases "p2 =o (czero :: 'a rel)") |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
148 |
case True |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
149 |
hence "q ^c p2 =o q ^c (czero :: 'a rel)" using n1 n2 cexp_cong2 Card_order_czero by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
150 |
also have "q ^c (czero :: 'a rel) =o cone" using cexp_czero by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
151 |
also have "cone \<le>o q ^c r2" using cone_ordLeq_cexp cone_ordLeq_Cnotzero n1 by blast |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
152 |
finally show ?thesis . |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
153 |
next |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
154 |
case False thus ?thesis using assms cexp_mono2' czeroI by metis |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
155 |
qed |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
156 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
157 |
lemma csum_cexp: "\<lbrakk>Cinfinite r1; Cinfinite r2; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow> |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
158 |
q ^c r1 +c q ^c r2 \<le>o q ^c (r1 +c r2)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
159 |
apply (rule csum_cinfinite_bound) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
160 |
apply (rule cexp_mono2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
161 |
apply (rule ordLeq_csum1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
162 |
apply (erule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
163 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
164 |
apply (rule notE) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
165 |
apply (rule cinfinite_not_czero[of r1]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
166 |
apply (erule conjunct1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
167 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
168 |
apply (erule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
169 |
apply (rule cexp_mono2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
170 |
apply (rule ordLeq_csum2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
171 |
apply (erule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
172 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
173 |
apply (rule notE) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
174 |
apply (rule cinfinite_not_czero[of r2]) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
175 |
apply (erule conjunct1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
176 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
177 |
apply (erule conjunct2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
178 |
apply (rule Card_order_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
179 |
apply (rule Card_order_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
180 |
apply (rule Cinfinite_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
181 |
apply assumption |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
182 |
apply (rule Cinfinite_csum) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
183 |
by (rule disjI1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
184 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
185 |
lemma csum_cexp': "\<lbrakk>Cinfinite r; Card_order q; ctwo \<le>o q\<rbrakk> \<Longrightarrow> q +c r \<le>o q ^c r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
186 |
apply (rule csum_cinfinite_bound) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
187 |
apply (metis Cinfinite_Cnotzero ordLeq_cexp1) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
188 |
apply (metis ordLeq_cexp2) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
189 |
apply blast+ |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
190 |
by (metis Cinfinite_cexp) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
191 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
192 |
lemma card_of_Sigma_ordLeq_Cinfinite: |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
193 |
"\<lbrakk>Cinfinite r; |I| \<le>o r; \<forall>i \<in> I. |A i| \<le>o r\<rbrakk> \<Longrightarrow> |SIGMA i : I. A i| \<le>o r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
194 |
unfolding cinfinite_def by (blast intro: card_of_Sigma_ordLeq_infinite_Field) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
195 |
|
54794 | 196 |
lemma card_order_cexp: |
197 |
assumes "card_order r1" "card_order r2" |
|
198 |
shows "card_order (r1 ^c r2)" |
|
199 |
proof - |
|
200 |
have "Field r1 = UNIV" "Field r2 = UNIV" using assms card_order_on_Card_order by auto |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
201 |
thus ?thesis unfolding cexp_def Func_def by simp |
54794 | 202 |
qed |
203 |
||
204 |
lemma Cinfinite_ordLess_cexp: |
|
205 |
assumes r: "Cinfinite r" |
|
206 |
shows "r <o r ^c r" |
|
207 |
proof - |
|
208 |
have "r <o ctwo ^c r" using r by (simp only: ordLess_ctwo_cexp) |
|
209 |
also have "ctwo ^c r \<le>o r ^c r" |
|
210 |
by (rule cexp_mono1[OF ctwo_ordLeq_Cinfinite]) (auto simp: r ctwo_not_czero Card_order_ctwo) |
|
211 |
finally show ?thesis . |
|
212 |
qed |
|
213 |
||
214 |
lemma infinite_ordLeq_cexp: |
|
215 |
assumes "Cinfinite r" |
|
216 |
shows "r \<le>o r ^c r" |
|
217 |
by (rule ordLess_imp_ordLeq[OF Cinfinite_ordLess_cexp[OF assms]]) |
|
218 |
||
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
219 |
lemma czero_cexp: "Cnotzero r \<Longrightarrow> czero ^c r =o czero" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
220 |
by (drule Cnotzero_imp_not_empty) (simp add: cexp_def czero_def card_of_empty_ordIso) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
221 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
222 |
lemma Func_singleton: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
223 |
fixes x :: 'b and A :: "'a set" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
224 |
shows "|Func A {x}| =o |{x}|" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
225 |
proof (rule ordIso_symmetric) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
226 |
def f \<equiv> "\<lambda>y a. if y = x \<and> a \<in> A then x else undefined" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
227 |
have "Func A {x} \<subseteq> f ` {x}" unfolding f_def Func_def by (force simp: fun_eq_iff) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
228 |
hence "bij_betw f {x} (Func A {x})" unfolding bij_betw_def inj_on_def f_def Func_def |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
229 |
by (auto split: split_if_asm) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
230 |
thus "|{x}| =o |Func A {x}|" using card_of_ordIso by blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
231 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
232 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
233 |
lemma cone_cexp: "cone ^c r =o cone" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
234 |
unfolding cexp_def cone_def Field_card_of by (rule Func_singleton) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
235 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
236 |
lemma card_of_Func_squared: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
237 |
fixes A :: "'a set" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
238 |
shows "|Func (UNIV :: bool set) A| =o |A \<times> A|" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
239 |
proof (rule ordIso_symmetric) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
240 |
def f \<equiv> "\<lambda>(x::'a,y) b. if A = {} then undefined else if b then x else y" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
241 |
have "Func (UNIV :: bool set) A \<subseteq> f ` (A \<times> A)" unfolding f_def Func_def |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
242 |
by (auto simp: image_iff fun_eq_iff split: option.splits split_if_asm) blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
243 |
hence "bij_betw f (A \<times> A) (Func (UNIV :: bool set) A)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
244 |
unfolding bij_betw_def inj_on_def f_def Func_def by (auto simp: fun_eq_iff) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
245 |
thus "|A \<times> A| =o |Func (UNIV :: bool set) A|" using card_of_ordIso by blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
246 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
247 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
248 |
lemma cexp_ctwo: "r ^c ctwo =o r *c r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
249 |
unfolding cexp_def ctwo_def cprod_def Field_card_of by (rule card_of_Func_squared) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
250 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
251 |
lemma card_of_Func_Plus: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
252 |
fixes A :: "'a set" and B :: "'b set" and C :: "'c set" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
253 |
shows "|Func (A <+> B) C| =o |Func A C \<times> Func B C|" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
254 |
proof (rule ordIso_symmetric) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
255 |
def f \<equiv> "\<lambda>(g :: 'a => 'c, h::'b \<Rightarrow> 'c) ab. case ab of Inl a \<Rightarrow> g a | Inr b \<Rightarrow> h b" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
256 |
def f' \<equiv> "\<lambda>(f :: ('a + 'b) \<Rightarrow> 'c). (\<lambda>a. f (Inl a), \<lambda>b. f (Inr b))" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
257 |
have "f ` (Func A C \<times> Func B C) \<subseteq> Func (A <+> B) C" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
258 |
unfolding Func_def f_def by (force split: sum.splits) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
259 |
moreover have "f' ` Func (A <+> B) C \<subseteq> Func A C \<times> Func B C" unfolding Func_def f'_def by force |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
260 |
moreover have "\<forall>a \<in> Func A C \<times> Func B C. f' (f a) = a" unfolding f'_def f_def Func_def by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
261 |
moreover have "\<forall>a' \<in> Func (A <+> B) C. f (f' a') = a'" unfolding f'_def f_def Func_def |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
262 |
by (auto split: sum.splits) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
263 |
ultimately have "bij_betw f (Func A C \<times> Func B C) (Func (A <+> B) C)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
264 |
by (intro bij_betw_byWitness[of _ f' f]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
265 |
thus "|Func A C \<times> Func B C| =o |Func (A <+> B) C|" using card_of_ordIso by blast |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
266 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
267 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
268 |
lemma cexp_csum: "r ^c (s +c t) =o r ^c s *c r ^c t" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
269 |
unfolding cexp_def cprod_def csum_def Field_card_of by (rule card_of_Func_Plus) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
270 |
|
54794 | 271 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
272 |
subsection {* Powerset *} |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
273 |
|
54794 | 274 |
definition cpow where "cpow r = |Pow (Field r)|" |
275 |
||
276 |
lemma card_order_cpow: "card_order r \<Longrightarrow> card_order (cpow r)" |
|
277 |
by (simp only: cpow_def Field_card_order Pow_UNIV card_of_card_order_on) |
|
278 |
||
279 |
lemma cpow_greater_eq: "Card_order r \<Longrightarrow> r \<le>o cpow r" |
|
280 |
by (rule ordLess_imp_ordLeq) (simp only: cpow_def Card_order_Pow) |
|
281 |
||
282 |
lemma Cinfinite_cpow: "Cinfinite r \<Longrightarrow> Cinfinite (cpow r)" |
|
283 |
unfolding cpow_def cinfinite_def by (metis Field_card_of card_of_Card_order infinite_Pow) |
|
284 |
||
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
285 |
lemma Card_order_cpow: "Card_order (cpow r)" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
286 |
unfolding cpow_def by (rule card_of_Card_order) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
287 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
288 |
lemma cardSuc_ordLeq_cpow: "Card_order r \<Longrightarrow> cardSuc r \<le>o cpow r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
289 |
unfolding cpow_def by (metis Card_order_Pow cardSuc_ordLess_ordLeq card_of_Card_order) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
290 |
|
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
291 |
lemma cpow_cexp_ctwo: "cpow r =o ctwo ^c r" |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
292 |
unfolding cpow_def ctwo_def cexp_def Field_card_of by (rule card_of_Pow_Func) |
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
293 |
|
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
294 |
subsection {* Inverse image *} |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
295 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
296 |
lemma vimage_ordLeq: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
297 |
assumes "|A| \<le>o k" and "\<forall> a \<in> A. |vimage f {a}| \<le>o k" and "Cinfinite k" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
298 |
shows "|vimage f A| \<le>o k" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
299 |
proof- |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
300 |
have "vimage f A = (\<Union> a \<in> A. vimage f {a})" by auto |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
301 |
also have "|\<Union> a \<in> A. vimage f {a}| \<le>o k" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
302 |
using UNION_Cinfinite_bound[OF assms] . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
303 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
304 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
305 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
306 |
subsection {* Maximum *} |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
307 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
308 |
definition cmax where |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
309 |
"cmax r s = |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
310 |
(if cinfinite r \<or> cinfinite s then czero +c r +c s |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
311 |
else natLeq_on (max (card (Field r)) (card (Field s))) +c czero)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
312 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
313 |
lemma cmax_com: "cmax r s =o cmax s r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
314 |
unfolding cmax_def |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
315 |
by (auto simp: max.commute intro: csum_cong2[OF csum_com] csum_cong2[OF czero_ordIso]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
316 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
317 |
lemma cmax1: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
318 |
assumes "Card_order r" "Card_order s" "s \<le>o r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
319 |
shows "cmax r s =o r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
320 |
unfolding cmax_def proof (split if_splits, intro conjI impI) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
321 |
assume "cinfinite r \<or> cinfinite s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
322 |
hence Cinf: "Cinfinite r" using assms(1,3) by (metis cinfinite_mono) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
323 |
have "czero +c r +c s =o r +c s" by (rule csum_czero2[OF Card_order_csum]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
324 |
also have "r +c s =o r" by (rule csum_absorb1[OF Cinf assms(3)]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
325 |
finally show "czero +c r +c s =o r" . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
326 |
next |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
327 |
assume "\<not> (cinfinite r \<or> cinfinite s)" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
328 |
hence fin: "finite (Field r)" and "finite (Field s)" unfolding cinfinite_def by simp_all |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
329 |
moreover |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
330 |
{ from assms(2) have "|Field s| =o s" by (rule card_of_Field_ordIso) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
331 |
also from assms(3) have "s \<le>o r" . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
332 |
also from assms(1) have "r =o |Field r|" by (rule ordIso_symmetric[OF card_of_Field_ordIso]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
333 |
finally have "|Field s| \<le>o |Field r|" . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
334 |
} |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
335 |
ultimately have "card (Field s) \<le> card (Field r)" by (subst sym[OF finite_card_of_iff_card2]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
336 |
hence "max (card (Field r)) (card (Field s)) = card (Field r)" by (rule max_absorb1) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
337 |
hence "natLeq_on (max (card (Field r)) (card (Field s))) +c czero = |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
338 |
natLeq_on (card (Field r)) +c czero" by simp |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
339 |
also have "\<dots> =o natLeq_on (card (Field r))" by (rule csum_czero1[OF natLeq_on_Card_order]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
340 |
also have "natLeq_on (card (Field r)) =o |Field r|" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
341 |
by (rule ordIso_symmetric[OF finite_imp_card_of_natLeq_on[OF fin]]) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
342 |
also from assms(1) have "|Field r| =o r" by (rule card_of_Field_ordIso) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
343 |
finally show "natLeq_on (max (card (Field r)) (card (Field s))) +c czero =o r" . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
344 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
345 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
346 |
lemma cmax2: |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
347 |
assumes "Card_order r" "Card_order s" "r \<le>o s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
348 |
shows "cmax r s =o s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
349 |
by (metis assms cmax1 cmax_com ordIso_transitive) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
350 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
351 |
lemma csum_absorb2: "Cinfinite r2 \<Longrightarrow> r1 \<le>o r2 \<Longrightarrow> r1 +c r2 =o r2" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
352 |
by (metis csum_absorb2') |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
353 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
354 |
lemma cprod_infinite2': "\<lbrakk>Cnotzero r1; Cinfinite r2; r1 \<le>o r2\<rbrakk> \<Longrightarrow> r1 *c r2 =o r2" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
355 |
unfolding ordIso_iff_ordLeq |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
356 |
by (intro conjI cprod_cinfinite_bound ordLeq_cprod2 ordLeq_refl) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
357 |
(auto dest!: ordIso_imp_ordLeq not_ordLeq_ordLess simp: czero_def Card_order_empty) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
358 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
359 |
context |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
360 |
fixes r s |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
361 |
assumes r: "Cinfinite r" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
362 |
and s: "Cinfinite s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
363 |
begin |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
364 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
365 |
lemma cmax_csum: "cmax r s =o r +c s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
366 |
proof (cases "r \<le>o s") |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
367 |
case True |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
368 |
hence "cmax r s =o s" by (metis cmax2 r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
369 |
also have "s =o r +c s" by (metis True csum_absorb2 ordIso_symmetric s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
370 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
371 |
next |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
372 |
case False |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
373 |
hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
374 |
hence "cmax r s =o r" by (metis cmax1 r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
375 |
also have "r =o r +c s" by (metis `s \<le>o r` csum_absorb1 ordIso_symmetric r) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
376 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
377 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
378 |
|
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
379 |
lemma cmax_cprod: "cmax r s =o r *c s" |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
380 |
proof (cases "r \<le>o s") |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
381 |
case True |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
382 |
hence "cmax r s =o s" by (metis cmax2 r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
383 |
also have "s =o r *c s" by (metis Cinfinite_Cnotzero True cprod_infinite2' ordIso_symmetric r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
384 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
385 |
next |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
386 |
case False |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
387 |
hence "s \<le>o r" by (metis ordLeq_total r s card_order_on_def) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
388 |
hence "cmax r s =o r" by (metis cmax1 r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
389 |
also have "r =o r *c s" by (metis Cinfinite_Cnotzero `s \<le>o r` cprod_infinite1' ordIso_symmetric r s) |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
390 |
finally show ?thesis . |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
391 |
qed |
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
392 |
|
48975
7f79f94a432c
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet
parents:
diff
changeset
|
393 |
end |
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
394 |
|
55174 | 395 |
lemma Card_order_cmax: |
396 |
assumes r: "Card_order r" and s: "Card_order s" |
|
397 |
shows "Card_order (cmax r s)" |
|
398 |
unfolding cmax_def by (auto simp: Card_order_csum) |
|
399 |
||
400 |
lemma ordLeq_cmax: |
|
401 |
assumes r: "Card_order r" and s: "Card_order s" |
|
402 |
shows "r \<le>o cmax r s \<and> s \<le>o cmax r s" |
|
403 |
proof- |
|
404 |
{assume "r \<le>o s" |
|
405 |
hence ?thesis by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) |
|
406 |
} |
|
407 |
moreover |
|
408 |
{assume "s \<le>o r" |
|
409 |
hence ?thesis using cmax_com by (metis cmax2 ordIso_iff_ordLeq ordLeq_transitive r s) |
|
410 |
} |
|
411 |
ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto |
|
412 |
qed |
|
413 |
||
414 |
lemmas ordLeq_cmax1 = ordLeq_cmax[THEN conjunct1] and |
|
415 |
ordLeq_cmax2 = ordLeq_cmax[THEN conjunct2] |
|
416 |
||
417 |
lemma finite_cmax: |
|
418 |
assumes r: "Card_order r" and s: "Card_order s" |
|
419 |
shows "finite (Field (cmax r s)) \<longleftrightarrow> finite (Field r) \<and> finite (Field s)" |
|
420 |
proof- |
|
421 |
{assume "r \<le>o s" |
|
422 |
hence ?thesis by (metis cmax2 ordIso_finite_Field ordLeq_finite_Field r s) |
|
423 |
} |
|
424 |
moreover |
|
425 |
{assume "s \<le>o r" |
|
426 |
hence ?thesis by (metis cmax1 ordIso_finite_Field ordLeq_finite_Field r s) |
|
427 |
} |
|
428 |
ultimately show ?thesis using r s ordLeq_total unfolding card_order_on_def by auto |
|
429 |
qed |
|
430 |
||
54980
7e0573a490ee
basic ordinal arithmetic and cardinals library extension (not relevant for BNFs)
traytel
parents:
54794
diff
changeset
|
431 |
end |