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.155  proof(auto simp add: natLeq_Well_order
   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)|"