src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 60758 d8d85a8172b5 parent 60585 48fdff264eb2 child 61799 4cf66f21b764
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Jul 18 21:44:18 2015 +0200
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Sat Jul 18 22:58:50 2015 +0200
1.3 @@ -5,13 +5,13 @@
1.4  Cardinal-order relations as needed by bounded natural functors.
1.5  *)
1.6
1.7 -section {* Cardinal-Order Relations as Needed by Bounded Natural Functors *}
1.8 +section \<open>Cardinal-Order Relations as Needed by Bounded Natural Functors\<close>
1.9
1.10  theory BNF_Cardinal_Order_Relation
1.11  imports Zorn BNF_Wellorder_Constructions
1.12  begin
1.13
1.14 -text{* In this section, we define cardinal-order relations to be minim well-orders
1.15 +text\<open>In this section, we define cardinal-order relations to be minim well-orders
1.16  on their field.  Then we define the cardinal of a set to be {\em some} cardinal-order
1.17  relation on that set, which will be unique up to order isomorphism.  Then we study
1.18  the connection between cardinals and:
1.19 @@ -31,14 +31,14 @@
1.20  most of the standard set-theoretic constructions (except for the powerset)
1.21  {\em do not increase cardinality}.  In particular, e.g., the set of words/lists over
1.22  any infinite set has the same cardinality (hence, is in bijection) with that set.
1.23 -*}
1.24 +\<close>
1.25
1.26
1.27 -subsection {* Cardinal orders *}
1.28 +subsection \<open>Cardinal orders\<close>
1.29
1.30 -text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.31 +text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.32  order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
1.33 -strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
1.34 +strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.\<close>
1.35
1.36  definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.37  where
1.38 @@ -56,7 +56,7 @@
1.39  "card_order_on A r \<Longrightarrow> A = Field r \<and> Card_order r"
1.40  unfolding card_order_on_def using well_order_on_Field by blast
1.41
1.42 -text{* The existence of a cardinal relation on any given set (which will mean
1.43 +text\<open>The existence of a cardinal relation on any given set (which will mean
1.44  that any set has a cardinal) follows from two facts:
1.45  \begin{itemize}
1.46  \item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
1.47 @@ -64,7 +64,7 @@
1.48  \item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
1.49  such well-order, i.e., a cardinal order.
1.50  \end{itemize}
1.51 -*}
1.52 +\<close>
1.53
1.54  theorem card_order_on: "\<exists>r. card_order_on A r"
1.55  proof-
1.56 @@ -111,11 +111,11 @@
1.57  using assms Card_order_ordIso ordIso_symmetric by blast
1.58
1.59
1.60 -subsection {* Cardinal of a set *}
1.61 +subsection \<open>Cardinal of a set\<close>
1.62
1.63 -text{* We define the cardinal of set to be {\em some} cardinal order on that set.
1.64 +text\<open>We define the cardinal of set to be {\em some} cardinal order on that set.
1.65  We shall prove that this notion is unique up to order isomorphism, meaning
1.66 -that order isomorphism shall be the true identity of cardinals. *}
1.67 +that order isomorphism shall be the true identity of cardinals.\<close>
1.68
1.69  definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
1.70  where "card_of A = (SOME r. card_order_on A r)"
1.71 @@ -343,13 +343,13 @@
1.72  using internalize_card_of_ordLeq[of "A" "|C|"] Field_card_of[of C] by auto
1.73
1.74
1.75 -subsection {* Cardinals versus set operations on arbitrary sets *}
1.76 +subsection \<open>Cardinals versus set operations on arbitrary sets\<close>
1.77
1.78 -text{* Here we embark in a long journey of simple results showing
1.79 +text\<open>Here we embark in a long journey of simple results showing
1.80  that the standard set-theoretic operations are well-behaved w.r.t. the notion of
1.81  cardinal -- essentially, this means that they preserve the cardinal identity"
1.82  @{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
1.83 -*}
1.84 +\<close>
1.85
1.86  lemma card_of_empty: "|{}| \<le>o |A|"
1.87  using card_of_ordLeq inj_on_id by blast
1.88 @@ -819,21 +819,21 @@
1.89  using assms card_of_Field_ordIso card_of_ordIso_finite ordIso_equivalence by blast
1.90
1.91
1.92 -subsection {* Cardinals versus set operations involving infinite sets *}
1.93 +subsection \<open>Cardinals versus set operations involving infinite sets\<close>
1.94
1.95 -text{* Here we show that, for infinite sets, most set-theoretic constructions
1.96 +text\<open>Here we show that, for infinite sets, most set-theoretic constructions
1.97  do not increase the cardinality.  The cornerstone for this is
1.98  theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
1.99  does not increase cardinality -- the proof of this fact adapts a standard
1.100  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
1.101 -at page 47 in @{cite "card-book"}. Then everything else follows fairly easily. *}
1.102 +at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
1.103
1.104  lemma infinite_iff_card_of_nat:
1.105  "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
1.106  unfolding infinite_iff_countable_subset card_of_ordLeq ..
1.107
1.108 -text{* The next two results correspond to the ZF fact that all infinite cardinals are
1.109 -limit ordinals: *}
1.110 +text\<open>The next two results correspond to the ZF fact that all infinite cardinals are
1.111 +limit ordinals:\<close>
1.112
1.113  lemma Card_order_infinite_not_under:
1.114  assumes CARD: "Card_order r" and INF: "\<not>finite (Field r)"
1.115 @@ -1140,13 +1140,13 @@
1.116  qed
1.117
1.118
1.119 -subsection {* The cardinal $\omega$ and the finite cardinals *}
1.120 +subsection \<open>The cardinal $\omega$ and the finite cardinals\<close>
1.121
1.122 -text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.123 +text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.124  order relation on
1.125  @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
1.126  shall be the restrictions of these relations to the numbers smaller than
1.127 -fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
1.128 +fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.\<close>
1.129
1.130  definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.131  definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.132 @@ -1160,12 +1160,12 @@
1.133  proof
1.134    assume "finite (A \<times> B)"
1.135    from assms(1) have "A \<noteq> {}" by auto
1.136 -  with finite (A \<times> B) have "finite B" using finite_cartesian_productD2 by auto
1.137 +  with \<open>finite (A \<times> B)\<close> have "finite B" using finite_cartesian_productD2 by auto
1.138    with assms(2) show False by simp
1.139  qed
1.140
1.141
1.142 -subsubsection {* First as well-orders *}
1.143 +subsubsection \<open>First as well-orders\<close>
1.144
1.145  lemma Field_natLeq: "Field natLeq = (UNIV::nat set)"
1.146  by(unfold Field_def natLeq_def, auto)
1.147 @@ -1225,7 +1225,7 @@
1.148  unfolding wo_rel_def using natLeq_on_Well_order .
1.149
1.150
1.151 -subsubsection {* Then as cardinals *}
1.152 +subsubsection \<open>Then as cardinals\<close>
1.153
1.154  lemma natLeq_Card_order: "Card_order natLeq"
1.156 @@ -1258,11 +1258,11 @@
1.157        card_of_Well_order natLeq_Well_order by blast
1.158
1.159
1.160 -subsection {* The successor of a cardinal *}
1.161 +subsection \<open>The successor of a cardinal\<close>
1.162
1.163 -text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.164 +text\<open>First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.165  being a successor cardinal of @{text "r"}. Although the definition does
1.166 -not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
1.167 +not require @{text "r"} to be a cardinal, only this case will be meaningful.\<close>
1.168
1.169  definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1.170  where
1.171 @@ -1270,9 +1270,9 @@
1.172   Card_order r' \<and> r <o r' \<and>
1.173   (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
1.174
1.175 -text{* Now we introduce the cardinal-successor operator @{text "cardSuc"},
1.176 +text\<open>Now we introduce the cardinal-successor operator @{text "cardSuc"},
1.177  by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
1.178 -Again, the picked item shall be proved unique up to order-isomorphism. *}
1.179 +Again, the picked item shall be proved unique up to order-isomorphism.\<close>
1.180
1.181  definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
1.182  where
1.183 @@ -1312,14 +1312,14 @@
1.184  "Card_order r \<Longrightarrow> r \<le>o cardSuc r"
1.185  using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1.186
1.187 -text{* The minimality property of @{text "cardSuc"} originally present in its definition
1.188 -is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
1.189 +text\<open>The minimality property of @{text "cardSuc"} originally present in its definition
1.190 +is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:\<close>
1.191
1.192  lemma cardSuc_least_aux:
1.193  "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"
1.194  using cardSuc_isCardSuc unfolding isCardSuc_def by blast
1.195
1.196 -text{* But from this we can infer general minimality: *}
1.197 +text\<open>But from this we can infer general minimality:\<close>
1.198
1.199  lemma cardSuc_least:
1.200  assumes CARD: "Card_order r" and CARD': "Card_order r'" and LESS: "r <o r'"
1.201 @@ -1497,7 +1497,7 @@
1.202  ordLeq_transitive by fast
1.203
1.204
1.205 -subsection {* Regular cardinals *}
1.206 +subsection \<open>Regular cardinals\<close>
1.207
1.208  definition cofinal where
1.209  "cofinal A r \<equiv>
1.210 @@ -1616,7 +1616,7 @@
1.211  qed
1.212
1.213
1.214 -subsection {* Others *}
1.215 +subsection \<open>Others\<close>
1.216
1.217  lemma card_of_Func_Times:
1.218  "|Func (A <*> B) C| =o |Func A (Func B C)|"