src/HOL/BNF_Wellorder_Constructions.thy
changeset 61799 4cf66f21b764
parent 60758 d8d85a8172b5
child 61943 7fba644ed827
     1.1 --- a/src/HOL/BNF_Wellorder_Constructions.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/BNF_Wellorder_Constructions.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -14,11 +14,11 @@
     1.4  text \<open>In this section, we study basic constructions on well-orders, such as restriction to
     1.5  a set/order filter, copy via direct images, ordinal-like sum of disjoint well-orders,
     1.6  and bounded square.  We also define between well-orders
     1.7 -the relations @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"}),
     1.8 -@{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"}), and
     1.9 -@{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).  We study the
    1.10 +the relations \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>),
    1.11 +\<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>), and
    1.12 +\<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).  We study the
    1.13  connections between these relations, order filters, and the aforementioned constructions.
    1.14 -A main result of this section is that @{text "<o"} is well-founded.\<close>
    1.15 +A main result of this section is that \<open><o\<close> is well-founded.\<close>
    1.16  
    1.17  
    1.18  subsection \<open>Restriction to a set\<close>
    1.19 @@ -306,14 +306,14 @@
    1.20  
    1.21  text \<open>We define three relations between well-orders:
    1.22  \begin{itemize}
    1.23 -\item @{text "ordLeq"}, of being embedded (abbreviated @{text "\<le>o"});
    1.24 -\item @{text "ordLess"}, of being strictly embedded (abbreviated @{text "<o"});
    1.25 -\item @{text "ordIso"}, of being isomorphic (abbreviated @{text "=o"}).
    1.26 +\item \<open>ordLeq\<close>, of being embedded (abbreviated \<open>\<le>o\<close>);
    1.27 +\item \<open>ordLess\<close>, of being strictly embedded (abbreviated \<open><o\<close>);
    1.28 +\item \<open>ordIso\<close>, of being isomorphic (abbreviated \<open>=o\<close>).
    1.29  \end{itemize}
    1.30  %
    1.31  The prefix "ord" and the index "o" in these names stand for "ordinal-like".
    1.32  These relations shall be proved to be inter-connected in a similar fashion as the trio
    1.33 -@{text "\<le>"}, @{text "<"}, @{text "="} associated to a total order on a set.
    1.34 +\<open>\<le>\<close>, \<open><\<close>, \<open>=\<close> associated to a total order on a set.
    1.35  \<close>
    1.36  
    1.37  definition ordLeq :: "('a rel * 'a' rel) set"
    1.38 @@ -347,10 +347,10 @@
    1.39  shows "Well_order r \<and> Well_order r'"
    1.40  using assms unfolding ordLeq_def by simp
    1.41  
    1.42 -text\<open>Notice that the relations @{text "\<le>o"}, @{text "<o"}, @{text "=o"} connect well-orders
    1.43 +text\<open>Notice that the relations \<open>\<le>o\<close>, \<open><o\<close>, \<open>=o\<close> connect well-orders
    1.44  on potentially {\em distinct} types. However, some of the lemmas below, including the next one,
    1.45 -restrict implicitly the type of these relations to @{text "(('a rel) * ('a rel)) set"} , i.e.,
    1.46 -to @{text "'a rel rel"}.\<close>
    1.47 +restrict implicitly the type of these relations to \<open>(('a rel) * ('a rel)) set\<close> , i.e.,
    1.48 +to \<open>'a rel rel\<close>.\<close>
    1.49  
    1.50  lemma ordLeq_reflexive:
    1.51  "Well_order r \<Longrightarrow> r \<le>o r"
    1.52 @@ -822,12 +822,12 @@
    1.53    ultimately show ?thesis using assms ordLeq_total ordIso_symmetric by blast
    1.54  qed
    1.55  
    1.56 -subsection\<open>@{text "<o"} is well-founded\<close>
    1.57 +subsection\<open>\<open><o\<close> is well-founded\<close>
    1.58  
    1.59 -text \<open>Of course, it only makes sense to state that the @{text "<o"} is well-founded
    1.60 -on the restricted type @{text "'a rel rel"}.  We prove this by first showing that, for any set
    1.61 +text \<open>Of course, it only makes sense to state that the \<open><o\<close> is well-founded
    1.62 +on the restricted type \<open>'a rel rel\<close>.  We prove this by first showing that, for any set
    1.63  of well-orders all embedded in a fixed well-order, the function mapping each well-order
    1.64 -in the set to an order filter of the fixed well-order is compatible w.r.t. to @{text "<o"} versus
    1.65 +in the set to an order filter of the fixed well-order is compatible w.r.t. to \<open><o\<close> versus
    1.66  {\em strict inclusion}; and we already know that strict inclusion of order filters is well-founded.\<close>
    1.67  
    1.68  definition ord_to_filter :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a set"
    1.69 @@ -885,8 +885,8 @@
    1.70  
    1.71  subsection \<open>Copy via direct images\<close>
    1.72  
    1.73 -text\<open>The direct image operator is the dual of the inverse image operator @{text "inv_image"}
    1.74 -from @{text "Relation.thy"}.  It is useful for transporting a well-order between
    1.75 +text\<open>The direct image operator is the dual of the inverse image operator \<open>inv_image\<close>
    1.76 +from \<open>Relation.thy\<close>.  It is useful for transporting a well-order between
    1.77  different types.\<close>
    1.78  
    1.79  definition dir_image :: "'a rel \<Rightarrow> ('a \<Rightarrow> 'a') \<Rightarrow> 'a' rel"
    1.80 @@ -1045,8 +1045,8 @@
    1.81  
    1.82  subsection \<open>Bounded square\<close>
    1.83  
    1.84 -text\<open>This construction essentially defines, for an order relation @{text "r"}, a lexicographic
    1.85 -order @{text "bsqr r"} on @{text "(Field r) \<times> (Field r)"}, applying the
    1.86 +text\<open>This construction essentially defines, for an order relation \<open>r\<close>, a lexicographic
    1.87 +order \<open>bsqr r\<close> on \<open>(Field r) \<times> (Field r)\<close>, applying the
    1.88  following criteria (in this order):
    1.89  \begin{itemize}
    1.90  \item compare the maximums;