src/HOL/BNF_Cardinal_Order_Relation.thy
changeset 61799 4cf66f21b764
parent 60758 d8d85a8172b5
child 61943 7fba644ed827
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  \item standard set-theoretic constructions: products,
     1.5  sums, unions, lists, powersets, set-of finite sets operator;
     1.6  \item finiteness and infiniteness (in particular, with the numeric cardinal operator
     1.7 -for finite sets, @{text "card"}, from the theory @{text "Finite_Sets.thy"}).
     1.8 +for finite sets, \<open>card\<close>, from the theory \<open>Finite_Sets.thy\<close>).
     1.9  \end{itemize}
    1.10  %
    1.11  On the way, we define the canonical $\omega$ cardinal and finite cardinals.  We also
    1.12 @@ -37,8 +37,8 @@
    1.13  subsection \<open>Cardinal orders\<close>
    1.14  
    1.15  text\<open>A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
    1.16 -order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
    1.17 -strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.\<close>
    1.18 +order-embedding relation, \<open>\<le>o\<close> (which is the same as being {\em minimal} w.r.t. the
    1.19 +strict order-embedding relation, \<open><o\<close>), among all the well-orders on its field.\<close>
    1.20  
    1.21  definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
    1.22  where
    1.23 @@ -59,9 +59,9 @@
    1.24  text\<open>The existence of a cardinal relation on any given set (which will mean
    1.25  that any set has a cardinal) follows from two facts:
    1.26  \begin{itemize}
    1.27 -\item Zermelo's theorem (proved in @{text "Zorn.thy"} as theorem @{text "well_order_on"}),
    1.28 +\item Zermelo's theorem (proved in \<open>Zorn.thy\<close> as theorem \<open>well_order_on\<close>),
    1.29  which states that on any given set there exists a well-order;
    1.30 -\item The well-founded-ness of @{text "<o"}, ensuring that then there exists a minimal
    1.31 +\item The well-founded-ness of \<open><o\<close>, ensuring that then there exists a minimal
    1.32  such well-order, i.e., a cardinal order.
    1.33  \end{itemize}
    1.34  \<close>
    1.35 @@ -348,7 +348,7 @@
    1.36  text\<open>Here we embark in a long journey of simple results showing
    1.37  that the standard set-theoretic operations are well-behaved w.r.t. the notion of
    1.38  cardinal -- essentially, this means that they preserve the ``cardinal identity"
    1.39 -@{text "=o"} and are monotonic w.r.t. @{text "\<le>o"}.
    1.40 +\<open>=o\<close> and are monotonic w.r.t. \<open>\<le>o\<close>.
    1.41  \<close>
    1.42  
    1.43  lemma card_of_empty: "|{}| \<le>o |A|"
    1.44 @@ -823,7 +823,7 @@
    1.45  
    1.46  text\<open>Here we show that, for infinite sets, most set-theoretic constructions
    1.47  do not increase the cardinality.  The cornerstone for this is
    1.48 -theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
    1.49 +theorem \<open>Card_order_Times_same_infinite\<close>, which states that self-product
    1.50  does not increase cardinality -- the proof of this fact adapts a standard
    1.51  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
    1.52  at page 47 in @{cite "card-book"}. Then everything else follows fairly easily.\<close>
    1.53 @@ -1144,9 +1144,9 @@
    1.54  
    1.55  text\<open>The cardinal $\omega$, of natural numbers, shall be the standard non-strict
    1.56  order relation on
    1.57 -@{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
    1.58 +\<open>nat\<close>, that we abbreviate by \<open>natLeq\<close>.  The finite cardinals
    1.59  shall be the restrictions of these relations to the numbers smaller than
    1.60 -fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.\<close>
    1.61 +fixed numbers \<open>n\<close>, that we abbreviate by \<open>natLeq_on n\<close>.\<close>
    1.62  
    1.63  definition "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
    1.64  definition "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
    1.65 @@ -1260,9 +1260,9 @@
    1.66  
    1.67  subsection \<open>The successor of a cardinal\<close>
    1.68  
    1.69 -text\<open>First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
    1.70 -being a successor cardinal of @{text "r"}. Although the definition does
    1.71 -not require @{text "r"} to be a cardinal, only this case will be meaningful.\<close>
    1.72 +text\<open>First we define \<open>isCardSuc r r'\<close>, the notion of \<open>r'\<close>
    1.73 +being a successor cardinal of \<open>r\<close>. Although the definition does
    1.74 +not require \<open>r\<close> to be a cardinal, only this case will be meaningful.\<close>
    1.75  
    1.76  definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
    1.77  where
    1.78 @@ -1270,8 +1270,8 @@
    1.79   Card_order r' \<and> r <o r' \<and>
    1.80   (\<forall>(r''::'a set rel). Card_order r'' \<and> r <o r'' \<longrightarrow> r' \<le>o r'')"
    1.81  
    1.82 -text\<open>Now we introduce the cardinal-successor operator @{text "cardSuc"},
    1.83 -by picking {\em some} cardinal-order relation fulfilling @{text "isCardSuc"}.
    1.84 +text\<open>Now we introduce the cardinal-successor operator \<open>cardSuc\<close>,
    1.85 +by picking {\em some} cardinal-order relation fulfilling \<open>isCardSuc\<close>.
    1.86  Again, the picked item shall be proved unique up to order-isomorphism.\<close>
    1.87  
    1.88  definition cardSuc :: "'a rel \<Rightarrow> 'a set rel"
    1.89 @@ -1312,8 +1312,8 @@
    1.90  "Card_order r \<Longrightarrow> r \<le>o cardSuc r"
    1.91  using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
    1.92  
    1.93 -text\<open>The minimality property of @{text "cardSuc"} originally present in its definition
    1.94 -is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:\<close>
    1.95 +text\<open>The minimality property of \<open>cardSuc\<close> originally present in its definition
    1.96 +is local to the type \<open>'a set rel\<close>, i.e., that of \<open>cardSuc r\<close>:\<close>
    1.97  
    1.98  lemma cardSuc_least_aux:
    1.99  "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"