src/HOL/BNF_Wellorder_Relation.thy
changeset 60758 d8d85a8172b5
parent 60585 48fdff264eb2
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/BNF_Wellorder_Relation.thy	Sat Jul 18 21:44:18 2015 +0200
     1.2 +++ b/src/HOL/BNF_Wellorder_Relation.thy	Sat Jul 18 22:58:50 2015 +0200
     1.3 @@ -5,24 +5,24 @@
     1.4  Well-order relations as needed by bounded natural functors.
     1.5  *)
     1.6  
     1.7 -section {* Well-Order Relations as Needed by Bounded Natural Functors *}
     1.8 +section \<open>Well-Order Relations as Needed by Bounded Natural Functors\<close>
     1.9  
    1.10  theory BNF_Wellorder_Relation
    1.11  imports Order_Relation
    1.12  begin
    1.13  
    1.14 -text{* In this section, we develop basic concepts and results pertaining
    1.15 +text\<open>In this section, we develop basic concepts and results pertaining
    1.16  to well-order relations.  Note that we consider well-order relations
    1.17  as {\em non-strict relations},
    1.18 -i.e., as containing the diagonals of their fields. *}
    1.19 +i.e., as containing the diagonals of their fields.\<close>
    1.20  
    1.21  locale wo_rel =
    1.22    fixes r :: "'a rel"
    1.23    assumes WELL: "Well_order r"
    1.24  begin
    1.25  
    1.26 -text{* The following context encompasses all this section. In other words,
    1.27 -for the whole section, we consider a fixed well-order relation @{term "r"}. *}
    1.28 +text\<open>The following context encompasses all this section. In other words,
    1.29 +for the whole section, we consider a fixed well-order relation @{term "r"}.\<close>
    1.30  
    1.31  (* context wo_rel  *)
    1.32  
    1.33 @@ -38,7 +38,7 @@
    1.34  lemmas ofilter_def = Order_Relation.ofilter_def[of r]
    1.35  
    1.36  
    1.37 -subsection {* Auxiliaries *}
    1.38 +subsection \<open>Auxiliaries\<close>
    1.39  
    1.40  lemma REFL: "Refl r"
    1.41  using WELL order_on_defs[of _ r] by auto
    1.42 @@ -72,13 +72,13 @@
    1.43  using TOTALS by auto
    1.44  
    1.45  
    1.46 -subsection {* Well-founded induction and recursion adapted to non-strict well-order relations *}
    1.47 +subsection \<open>Well-founded induction and recursion adapted to non-strict well-order relations\<close>
    1.48  
    1.49 -text{* Here we provide induction and recursion principles specific to {\em non-strict}
    1.50 +text\<open>Here we provide induction and recursion principles specific to {\em non-strict}
    1.51  well-order relations.
    1.52  Although minor variations of those for well-founded relations, they will be useful
    1.53  for doing away with the tediousness of
    1.54 -having to take out the diagonal each time in order to switch to a well-founded relation. *}
    1.55 +having to take out the diagonal each time in order to switch to a well-founded relation.\<close>
    1.56  
    1.57  lemma well_order_induct:
    1.58  assumes IND: "\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> P y \<Longrightarrow> P x"
    1.59 @@ -113,9 +113,9 @@
    1.60  qed
    1.61  
    1.62  
    1.63 -subsection {* The notions of maximum, minimum, supremum, successor and order filter *}
    1.64 +subsection \<open>The notions of maximum, minimum, supremum, successor and order filter\<close>
    1.65  
    1.66 -text{*
    1.67 +text\<open>
    1.68  We define the successor {\em of a set}, and not of an element (the latter is of course
    1.69  a particular case).  Also, we define the maximum {\em of two elements}, @{text "max2"},
    1.70  and the minimum {\em of a set}, @{text "minim"} -- we chose these variants since we
    1.71 @@ -124,7 +124,7 @@
    1.72  defined in terms of minimum as expected.
    1.73  The minimum is only meaningful for non-empty sets, and the successor is only
    1.74  meaningful for sets for which strict upper bounds exist.
    1.75 -Order filters for well-orders are also known as ``initial segments". *}
    1.76 +Order filters for well-orders are also known as ``initial segments".\<close>
    1.77  
    1.78  definition max2 :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    1.79  where "max2 a b \<equiv> if (a,b) \<in> r then b else a"
    1.80 @@ -142,7 +142,7 @@
    1.81  where "suc A \<equiv> minim (AboveS A)"
    1.82  
    1.83  
    1.84 -subsubsection {* Properties of max2 *}
    1.85 +subsubsection \<open>Properties of max2\<close>
    1.86  
    1.87  lemma max2_greater_among:
    1.88  assumes "a \<in> Field r" and "b \<in> Field r"
    1.89 @@ -191,7 +191,7 @@
    1.90  unfolding max2_def by auto
    1.91  
    1.92  
    1.93 -subsubsection {* Existence and uniqueness for isMinim and well-definedness of minim *}
    1.94 +subsubsection \<open>Existence and uniqueness for isMinim and well-definedness of minim\<close>
    1.95  
    1.96  lemma isMinim_unique:
    1.97  assumes MINIM: "isMinim B a" and MINIM': "isMinim B a'"
    1.98 @@ -254,7 +254,7 @@
    1.99    unfolding minim_def using theI[of ?phi b] by blast
   1.100  qed
   1.101  
   1.102 -subsubsection{* Properties of minim *}
   1.103 +subsubsection\<open>Properties of minim\<close>
   1.104  
   1.105  lemma minim_in:
   1.106  assumes "B \<le> Field r" and "B \<noteq> {}"
   1.107 @@ -294,7 +294,7 @@
   1.108    using isMinim_unique by auto
   1.109  qed
   1.110  
   1.111 -subsubsection{* Properties of successor *}
   1.112 +subsubsection\<open>Properties of successor\<close>
   1.113  
   1.114  lemma suc_AboveS:
   1.115  assumes SUB: "B \<le> Field r" and ABOVES: "AboveS B \<noteq> {}"
   1.116 @@ -388,7 +388,7 @@
   1.117  qed
   1.118  
   1.119  
   1.120 -subsubsection {* Properties of order filters *}
   1.121 +subsubsection \<open>Properties of order filters\<close>
   1.122  
   1.123  lemma under_ofilter:
   1.124  "ofilter (under a)"
   1.125 @@ -494,7 +494,7 @@
   1.126    thus "A \<le> (\<Union>a \<in> A. under a)" by blast
   1.127  qed
   1.128  
   1.129 -subsubsection{* Other properties *}
   1.130 +subsubsection\<open>Other properties\<close>
   1.131  
   1.132  lemma ofilter_linord:
   1.133  assumes OF1: "ofilter A" and OF2: "ofilter B"