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

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"