src/HOL/BNF_Cardinal_Order_Relation.thy
 changeset 55101 57c875e488bd parent 55087 252c7fec4119 child 55206 f7358e55018f
     1.1 --- a/src/HOL/BNF_Cardinal_Order_Relation.thy	Tue Jan 21 16:56:34 2014 +0100
1.2 +++ b/src/HOL/BNF_Cardinal_Order_Relation.thy	Wed Jan 22 09:45:30 2014 +0100
1.3 @@ -38,7 +38,7 @@
1.4
1.5  text{* A cardinal order in our setting shall be a well-order {\em minim} w.r.t. the
1.6  order-embedding relation, @{text "\<le>o"} (which is the same as being {\em minimal} w.r.t. the
1.7 -strict order-embedding relation, @{text "<o"}), among all the well-orders on its field.  *}
1.8 +strict order-embedding relation, @{text "<o"}), among all the well-orders on its field. *}
1.9
1.10  definition card_order_on :: "'a set \<Rightarrow> 'a rel \<Rightarrow> bool"
1.11  where
1.12 @@ -115,7 +115,7 @@
1.13
1.14  text{* We define the cardinal of set to be {\em some} cardinal order on that set.
1.15  We shall prove that this notion is unique up to order isomorphism, meaning
1.16 -that order isomorphism shall be the true identity of cardinals.  *}
1.17 +that order isomorphism shall be the true identity of cardinals. *}
1.18
1.19  definition card_of :: "'a set \<Rightarrow> 'a rel" ("|_|" )
1.20  where "card_of A = (SOME r. card_order_on A r)"
1.21 @@ -827,7 +827,7 @@
1.22  theorem @{text "Card_order_Times_same_infinite"}, which states that self-product
1.23  does not increase cardinality -- the proof of this fact adapts a standard
1.24  set-theoretic argument, as presented, e.g., in the proof of theorem 1.5.11
1.25 -at page 47 in \cite{card-book}. Then everything else follows fairly easily.  *}
1.26 +at page 47 in \cite{card-book}. Then everything else follows fairly easily. *}
1.27
1.28  lemma infinite_iff_card_of_nat:
1.29  "\<not> finite A \<longleftrightarrow> ( |UNIV::nat set| \<le>o |A| )"
1.30 @@ -1141,13 +1141,13 @@
1.31  qed
1.32
1.33
1.34 -subsection {* The cardinal $\omega$ and the finite cardinals  *}
1.35 +subsection {* The cardinal $\omega$ and the finite cardinals *}
1.36
1.37  text{* The cardinal $\omega$, of natural numbers, shall be the standard non-strict
1.38  order relation on
1.39  @{text "nat"}, that we abbreviate by @{text "natLeq"}.  The finite cardinals
1.40  shall be the restrictions of these relations to the numbers smaller than
1.41 -fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}.  *}
1.42 +fixed numbers @{text "n"}, that we abbreviate by @{text "natLeq_on n"}. *}
1.43
1.44  abbreviation "(natLeq::(nat * nat) set) \<equiv> {(x,y). x \<le> y}"
1.45  abbreviation "(natLess::(nat * nat) set) \<equiv> {(x,y). x < y}"
1.46 @@ -1263,7 +1263,7 @@
1.47
1.48  text{* First we define @{text "isCardSuc r r'"}, the notion of @{text "r'"}
1.49  being a successor cardinal of @{text "r"}. Although the definition does
1.50 -not require @{text "r"} to be a cardinal, only this case will be meaningful.  *}
1.51 +not require @{text "r"} to be a cardinal, only this case will be meaningful. *}
1.52
1.53  definition isCardSuc :: "'a rel \<Rightarrow> 'a set rel \<Rightarrow> bool"
1.54  where
1.55 @@ -1314,7 +1314,7 @@
1.56  using cardSuc_greater ordLeq_iff_ordLess_or_ordIso by blast
1.57
1.58  text{* The minimality property of @{text "cardSuc"} originally present in its definition
1.59 -is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}:  *}
1.60 +is local to the type @{text "'a set rel"}, i.e., that of @{text "cardSuc r"}: *}
1.61
1.62  lemma cardSuc_least_aux:
1.63  "\<lbrakk>Card_order (r::'a rel); Card_order (r'::'a set rel); r <o r'\<rbrakk> \<Longrightarrow> cardSuc r \<le>o r'"