summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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