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