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'"