Order and lattice structures no longer based on records.
authorballarin
Mon Oct 16 10:27:54 2006 +0200 (2006-10-16)
changeset 2104160e418260b4d
parent 21040 983caf913a4c
child 21042 b96d37893dbb
Order and lattice structures no longer based on records.
NEWS
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
     1.1 --- a/NEWS	Sun Oct 15 12:16:20 2006 +0200
     1.2 +++ b/NEWS	Mon Oct 16 10:27:54 2006 +0200
     1.3 @@ -610,13 +610,15 @@
     1.4  
     1.5  *** HOL-Algebra ***
     1.6  
     1.7 +* Formalisation of ideals and the quotient construction over rings, contributed
     1.8 +  by Stephan Hohe.
     1.9 +
    1.10 +* Order and lattice theory no longer based on records.  INCOMPATIBILITY.
    1.11 +
    1.12  * Method algebra is now set up via an attribute.  For examples see CRing.thy.
    1.13    INCOMPATIBILITY: the method is now weaker on combinations of algebraic
    1.14    structures.
    1.15  
    1.16 -* Formalisation of ideals and the quotient construction over rings, contributed
    1.17 -  by Stephan Hohe.
    1.18 -
    1.19  * Renamed `CRing.thy' to `Ring.thy'.  INCOMPATIBILITY.
    1.20  
    1.21  
     2.1 --- a/src/HOL/Algebra/Group.thy	Sun Oct 15 12:16:20 2006 +0200
     2.2 +++ b/src/HOL/Algebra/Group.thy	Mon Oct 16 10:27:54 2006 +0200
     2.3 @@ -685,7 +685,7 @@
     2.4  text_raw {* \label{sec:subgroup-lattice} *}
     2.5  
     2.6  theorem (in group) subgroups_partial_order:
     2.7 -  "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
     2.8 +  "partial_order {H. subgroup H G} (op \<subseteq>)"
     2.9    by (rule partial_order.intro) simp_all
    2.10  
    2.11  lemma (in group) subgroup_self:
    2.12 @@ -730,22 +730,23 @@
    2.13  qed
    2.14  
    2.15  theorem (in group) subgroups_complete_lattice:
    2.16 -  "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
    2.17 -    (is "complete_lattice ?L")
    2.18 +  "complete_lattice {H. subgroup H G} (op \<subseteq>)"
    2.19 +    (is "complete_lattice ?car ?le")
    2.20  proof (rule partial_order.complete_lattice_criterion1)
    2.21 -  show "partial_order ?L" by (rule subgroups_partial_order)
    2.22 +  show "partial_order ?car ?le" by (rule subgroups_partial_order)
    2.23  next
    2.24 -  have "greatest ?L (carrier G) (carrier ?L)"
    2.25 -    by (unfold greatest_def) (simp add: subgroup.subset subgroup_self)
    2.26 -  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
    2.27 +  have "order_syntax.greatest ?car ?le (carrier G) ?car"
    2.28 +    by (unfold order_syntax.greatest_def)
    2.29 +      (simp add: subgroup.subset subgroup_self)
    2.30 +  then show "\<exists>G. order_syntax.greatest ?car ?le G ?car" ..
    2.31  next
    2.32    fix A
    2.33 -  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    2.34 +  assume L: "A \<subseteq> ?car" and non_empty: "A ~= {}"
    2.35    then have Int_subgroup: "subgroup (\<Inter>A) G"
    2.36      by (fastsimp intro: subgroups_Inter)
    2.37 -  have "greatest ?L (\<Inter>A) (Lower ?L A)"
    2.38 -    (is "greatest ?L ?Int _")
    2.39 -  proof (rule greatest_LowerI)
    2.40 +  have "order_syntax.greatest ?car ?le (\<Inter>A) (order_syntax.Lower ?car ?le A)"
    2.41 +    (is "order_syntax.greatest _ _ ?Int _")
    2.42 +  proof (rule order_syntax.greatest_LowerI)
    2.43      fix H
    2.44      assume H: "H \<in> A"
    2.45      with L have subgroupH: "subgroup H G" by auto
    2.46 @@ -754,17 +755,18 @@
    2.47      from groupH have monoidH: "monoid ?H"
    2.48        by (rule group.is_monoid)
    2.49      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    2.50 -    then show "le ?L ?Int H" by simp
    2.51 +    then show "?le ?Int H" by simp
    2.52    next
    2.53      fix H
    2.54 -    assume H: "H \<in> Lower ?L A"
    2.55 -    with L Int_subgroup show "le ?L H ?Int" by (fastsimp intro: Inter_greatest)
    2.56 +    assume H: "H \<in> order_syntax.Lower ?car ?le A"
    2.57 +    with L Int_subgroup show "?le H ?Int"
    2.58 +      by (fastsimp simp: order_syntax.Lower_def intro: Inter_greatest)
    2.59    next
    2.60 -    show "A \<subseteq> carrier ?L" by (rule L)
    2.61 +    show "A \<subseteq> ?car" by (rule L)
    2.62    next
    2.63 -    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    2.64 +    show "?Int \<in> ?car" by simp (rule Int_subgroup)
    2.65    qed
    2.66 -  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
    2.67 +  then show "\<exists>I. order_syntax.greatest ?car ?le I (order_syntax.Lower ?car ?le A)" ..
    2.68  qed
    2.69  
    2.70  end
     3.1 --- a/src/HOL/Algebra/IntRing.thy	Sun Oct 15 12:16:20 2006 +0200
     3.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Oct 16 10:27:54 2006 +0200
     3.3 @@ -71,9 +71,6 @@
     3.4    int_ring :: "int ring" ("\<Z>")
     3.5    "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
     3.6  
     3.7 -  int_order :: "int order"
     3.8 -  "int_order \<equiv> \<lparr>carrier = UNIV, le = op \<le>\<rparr>"
     3.9 -
    3.10  lemma int_Zcarr[simp,intro!]:
    3.11    "k \<in> carrier \<Z>"
    3.12  by (simp add: int_ring_def)
    3.13 @@ -99,14 +96,13 @@
    3.14  interpretation "domain" ["\<Z>"] by (rule int_is_domain)
    3.15  
    3.16  lemma int_le_total_order:
    3.17 -  "total_order int_order"
    3.18 -unfolding int_order_def
    3.19 +  "total_order (UNIV::int set) (op \<le>)"
    3.20  apply (rule partial_order.total_orderI)
    3.21   apply (rule partial_order.intro, simp+)
    3.22  apply clarsimp
    3.23  done
    3.24  
    3.25 -interpretation total_order ["int_order"] by (rule int_le_total_order)
    3.26 +interpretation total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
    3.27  
    3.28  
    3.29  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
     4.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Oct 15 12:16:20 2006 +0200
     4.2 +++ b/src/HOL/Algebra/Lattice.thy	Mon Oct 16 10:27:54 2006 +0200
     4.3 @@ -18,157 +18,191 @@
     4.4  
     4.5  subsection {* Partial Orders *}
     4.6  
     4.7 +(*
     4.8  record 'a order = "'a partial_object" +
     4.9    le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    4.10 +*)
    4.11  
    4.12 -locale partial_order =
    4.13 -  fixes L (structure)
    4.14 +text {* Locale @{text order_syntax} is required since we want to refer
    4.15 +  to definitions (and their derived theorems) outside of @{text partial_order}.
    4.16 +  *}
    4.17 +
    4.18 +locale order_syntax =
    4.19 +  fixes carrier :: "'a set" and le :: "['a, 'a] => bool" (infix "\<sqsubseteq>" 50)
    4.20 +
    4.21 +text {* Note that the type constraints above are necessary, because the
    4.22 +  definition command cannot specialise the types. *}
    4.23 +
    4.24 +definition (in order_syntax)
    4.25 +  less (infixl "\<sqsubset>" 50) "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    4.26 +
    4.27 +text {* Upper and lower bounds of a set. *}
    4.28 +
    4.29 +definition (in order_syntax)
    4.30 +  Upper where
    4.31 +  "Upper A == {u. (ALL x. x \<in> A \<inter> carrier --> x \<sqsubseteq> u)} \<inter>
    4.32 +              carrier"
    4.33 +
    4.34 +definition (in order_syntax)
    4.35 +  Lower :: "'a set => 'a set"
    4.36 +  "Lower A == {l. (ALL x. x \<in> A \<inter> carrier --> l \<sqsubseteq> x)} \<inter>
    4.37 +              carrier"
    4.38 +
    4.39 +text {* Least and greatest, as predicate. *}
    4.40 +
    4.41 +definition (in order_syntax)
    4.42 +  least :: "['a, 'a set] => bool"
    4.43 +  "least l A == A \<subseteq> carrier & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    4.44 +
    4.45 +definition (in order_syntax)
    4.46 +  greatest :: "['a, 'a set] => bool"
    4.47 +  "greatest g A == A \<subseteq> carrier & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    4.48 +
    4.49 +text {* Supremum and infimum *}
    4.50 +
    4.51 +definition (in order_syntax)
    4.52 +  sup :: "'a set => 'a" ("\<Squnion>")  (* FIXME precedence [90] 90 *)
    4.53 +  "\<Squnion>A == THE x. least x (Upper A)"
    4.54 +
    4.55 +definition (in order_syntax)
    4.56 +  inf :: "'a set => 'a" ("\<Sqinter>") (* FIXME precedence *)
    4.57 +  "\<Sqinter>A == THE x. greatest x (Lower A)"
    4.58 +
    4.59 +definition (in order_syntax)
    4.60 +  join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65)
    4.61 +  "x \<squnion> y == sup {x, y}"
    4.62 +
    4.63 +definition (in order_syntax)
    4.64 +  meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70)
    4.65 +  "x \<sqinter> y == inf {x, y}"
    4.66 +
    4.67 +locale partial_order = order_syntax +
    4.68    assumes refl [intro, simp]:
    4.69 -                  "x \<in> carrier L ==> x \<sqsubseteq> x"
    4.70 +                  "x \<in> carrier ==> x \<sqsubseteq> x"
    4.71      and anti_sym [intro]:
    4.72 -                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    4.73 +                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier; y \<in> carrier |] ==> x = y"
    4.74      and trans [trans]:
    4.75                    "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
    4.76 -                   x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    4.77 -
    4.78 -constdefs (structure L)
    4.79 -  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    4.80 -  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    4.81 -
    4.82 -  -- {* Upper and lower bounds of a set. *}
    4.83 -  Upper :: "[_, 'a set] => 'a set"
    4.84 -  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
    4.85 -                carrier L"
    4.86 -
    4.87 -  Lower :: "[_, 'a set] => 'a set"
    4.88 -  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
    4.89 -                carrier L"
    4.90 +                   x \<in> carrier; y \<in> carrier; z \<in> carrier |] ==> x \<sqsubseteq> z"
    4.91  
    4.92 -  -- {* Least and greatest, as predicate. *}
    4.93 -  least :: "[_, 'a, 'a set] => bool"
    4.94 -  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    4.95 -
    4.96 -  greatest :: "[_, 'a, 'a set] => bool"
    4.97 -  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    4.98 -
    4.99 -  -- {* Supremum and infimum *}
   4.100 -  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   4.101 -  "\<Squnion>A == THE x. least L x (Upper L A)"
   4.102 -
   4.103 -  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   4.104 -  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
   4.105 -
   4.106 -  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   4.107 -  "x \<squnion> y == sup L {x, y}"
   4.108 -
   4.109 -  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   4.110 -  "x \<sqinter> y == inf L {x, y}"
   4.111 +abbreviation (in partial_order)
   4.112 +  less (infixl "\<sqsubset>" 50) "less == order_syntax.less le"
   4.113 +abbreviation (in partial_order)
   4.114 +  Upper where "Upper == order_syntax.Upper carrier le"
   4.115 +abbreviation (in partial_order)
   4.116 +  Lower where "Lower == order_syntax.Lower carrier le"
   4.117 +abbreviation (in partial_order)
   4.118 +  least where "least == order_syntax.least carrier le"
   4.119 +abbreviation (in partial_order)
   4.120 +  greatest where "greatest == order_syntax.greatest carrier le"
   4.121 +abbreviation (in partial_order)
   4.122 +  sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le"
   4.123 +abbreviation (in partial_order)
   4.124 +  inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le"
   4.125 +abbreviation (in partial_order)
   4.126 +  join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le"
   4.127 +abbreviation (in partial_order)
   4.128 +  meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le"
   4.129  
   4.130  
   4.131  subsubsection {* Upper *}
   4.132  
   4.133 -lemma Upper_closed [intro, simp]:
   4.134 -  "Upper L A \<subseteq> carrier L"
   4.135 +lemma (in order_syntax) Upper_closed [intro, simp]:
   4.136 +  "Upper A \<subseteq> carrier"
   4.137    by (unfold Upper_def) clarify
   4.138  
   4.139 -lemma UpperD [dest]:
   4.140 +lemma (in order_syntax) UpperD [dest]:
   4.141    fixes L (structure)
   4.142 -  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   4.143 +  shows "[| u \<in> Upper A; x \<in> A; A \<subseteq> carrier |] ==> x \<sqsubseteq> u"
   4.144    by (unfold Upper_def) blast
   4.145  
   4.146 -lemma Upper_memI:
   4.147 +lemma (in order_syntax) Upper_memI:
   4.148    fixes L (structure)
   4.149 -  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   4.150 +  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier |] ==> x \<in> Upper A"
   4.151    by (unfold Upper_def) blast
   4.152  
   4.153 -lemma Upper_antimono:
   4.154 -  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   4.155 +lemma (in order_syntax) Upper_antimono:
   4.156 +  "A \<subseteq> B ==> Upper B \<subseteq> Upper A"
   4.157    by (unfold Upper_def) blast
   4.158  
   4.159  
   4.160  subsubsection {* Lower *}
   4.161  
   4.162 -lemma Lower_closed [intro, simp]:
   4.163 -  "Lower L A \<subseteq> carrier L"
   4.164 +lemma (in order_syntax) Lower_closed [intro, simp]:
   4.165 +  "Lower A \<subseteq> carrier"
   4.166    by (unfold Lower_def) clarify
   4.167  
   4.168 -lemma LowerD [dest]:
   4.169 -  fixes L (structure)
   4.170 -  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
   4.171 +lemma (in order_syntax) LowerD [dest]:
   4.172 +  "[| l \<in> Lower A; x \<in> A; A \<subseteq> carrier |] ==> l \<sqsubseteq> x"
   4.173    by (unfold Lower_def) blast
   4.174  
   4.175 -lemma Lower_memI:
   4.176 -  fixes L (structure)
   4.177 -  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   4.178 +lemma (in order_syntax) Lower_memI:
   4.179 +  "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier |] ==> x \<in> Lower A"
   4.180    by (unfold Lower_def) blast
   4.181  
   4.182 -lemma Lower_antimono:
   4.183 -  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   4.184 +lemma (in order_syntax) Lower_antimono:
   4.185 +  "A \<subseteq> B ==> Lower B \<subseteq> Lower A"
   4.186    by (unfold Lower_def) blast
   4.187  
   4.188  
   4.189  subsubsection {* least *}
   4.190  
   4.191 -lemma least_carrier [intro, simp]:
   4.192 -  shows "least L l A ==> l \<in> carrier L"
   4.193 +lemma (in order_syntax) least_carrier [intro, simp]:
   4.194 +  "least l A ==> l \<in> carrier"
   4.195    by (unfold least_def) fast
   4.196  
   4.197 -lemma least_mem:
   4.198 -  "least L l A ==> l \<in> A"
   4.199 +lemma (in order_syntax) least_mem:
   4.200 +  "least l A ==> l \<in> A"
   4.201    by (unfold least_def) fast
   4.202  
   4.203  lemma (in partial_order) least_unique:
   4.204 -  "[| least L x A; least L y A |] ==> x = y"
   4.205 +  "[| least x A; least y A |] ==> x = y"
   4.206    by (unfold least_def) blast
   4.207  
   4.208 -lemma least_le:
   4.209 -  fixes L (structure)
   4.210 -  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   4.211 +lemma (in order_syntax) least_le:
   4.212 +  "[| least x A; a \<in> A |] ==> x \<sqsubseteq> a"
   4.213    by (unfold least_def) fast
   4.214  
   4.215 -lemma least_UpperI:
   4.216 -  fixes L (structure)
   4.217 +lemma (in order_syntax) least_UpperI:
   4.218    assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   4.219 -    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   4.220 -    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   4.221 -  shows "least L s (Upper L A)"
   4.222 +    and below: "!! y. y \<in> Upper A ==> s \<sqsubseteq> y"
   4.223 +    and L: "A \<subseteq> carrier"  "s \<in> carrier"
   4.224 +  shows "least s (Upper A)"
   4.225  proof -
   4.226 -  have "Upper L A \<subseteq> carrier L" by simp
   4.227 -  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   4.228 -  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   4.229 +  have "Upper A \<subseteq> carrier" by simp
   4.230 +  moreover from above L have "s \<in> Upper A" by (simp add: Upper_def)
   4.231 +  moreover from below have "ALL x : Upper A. s \<sqsubseteq> x" by fast
   4.232    ultimately show ?thesis by (simp add: least_def)
   4.233  qed
   4.234  
   4.235  
   4.236  subsubsection {* greatest *}
   4.237  
   4.238 -lemma greatest_carrier [intro, simp]:
   4.239 -  shows "greatest L l A ==> l \<in> carrier L"
   4.240 +lemma (in order_syntax) greatest_carrier [intro, simp]:
   4.241 +  "greatest l A ==> l \<in> carrier"
   4.242    by (unfold greatest_def) fast
   4.243  
   4.244 -lemma greatest_mem:
   4.245 -  "greatest L l A ==> l \<in> A"
   4.246 +lemma (in order_syntax) greatest_mem:
   4.247 +  "greatest l A ==> l \<in> A"
   4.248    by (unfold greatest_def) fast
   4.249  
   4.250  lemma (in partial_order) greatest_unique:
   4.251 -  "[| greatest L x A; greatest L y A |] ==> x = y"
   4.252 +  "[| greatest x A; greatest y A |] ==> x = y"
   4.253    by (unfold greatest_def) blast
   4.254  
   4.255 -lemma greatest_le:
   4.256 -  fixes L (structure)
   4.257 -  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   4.258 +lemma (in order_syntax) greatest_le:
   4.259 +  "[| greatest x A; a \<in> A |] ==> a \<sqsubseteq> x"
   4.260    by (unfold greatest_def) fast
   4.261  
   4.262 -lemma greatest_LowerI:
   4.263 -  fixes L (structure)
   4.264 +lemma (in order_syntax) greatest_LowerI:
   4.265    assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   4.266 -    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   4.267 -    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   4.268 -  shows "greatest L i (Lower L A)"
   4.269 +    and above: "!! y. y \<in> Lower A ==> y \<sqsubseteq> i"
   4.270 +    and L: "A \<subseteq> carrier"  "i \<in> carrier"
   4.271 +  shows "greatest i (Lower A)"
   4.272  proof -
   4.273 -  have "Lower L A \<subseteq> carrier L" by simp
   4.274 -  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   4.275 -  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   4.276 +  have "Lower A \<subseteq> carrier" by simp
   4.277 +  moreover from below L have "i \<in> Lower A" by (simp add: Lower_def)
   4.278 +  moreover from above have "ALL x : Lower A. x \<sqsubseteq> i" by fast
   4.279    ultimately show ?thesis by (simp add: greatest_def)
   4.280  qed
   4.281  
   4.282 @@ -177,63 +211,80 @@
   4.283  
   4.284  locale lattice = partial_order +
   4.285    assumes sup_of_two_exists:
   4.286 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   4.287 +    "[| x \<in> carrier; y \<in> carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le {x, y})"
   4.288      and inf_of_two_exists:
   4.289 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   4.290 +    "[| x \<in> carrier; y \<in> carrier |] ==> EX s. order_syntax.greatest carrier le s (order_syntax.Lower carrier le {x, y})"
   4.291  
   4.292 -lemma least_Upper_above:
   4.293 -  fixes L (structure)
   4.294 -  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   4.295 +abbreviation (in lattice)
   4.296 +  less (infixl "\<sqsubset>" 50) "less == order_syntax.less le"
   4.297 +abbreviation (in lattice)
   4.298 +  Upper where "Upper == order_syntax.Upper carrier le"
   4.299 +abbreviation (in lattice)
   4.300 +  Lower where "Lower == order_syntax.Lower carrier le"
   4.301 +abbreviation (in lattice)
   4.302 +  least where "least == order_syntax.least carrier le"
   4.303 +abbreviation (in lattice)
   4.304 +  greatest where "greatest == order_syntax.greatest carrier le"
   4.305 +abbreviation (in lattice)
   4.306 +  sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le"
   4.307 +abbreviation (in lattice)
   4.308 +  inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le"
   4.309 +abbreviation (in lattice)
   4.310 +  join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le"
   4.311 +abbreviation (in lattice)
   4.312 +  meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le"
   4.313 +
   4.314 +lemma (in order_syntax) least_Upper_above:
   4.315 +  "[| least s (Upper A); x \<in> A; A \<subseteq> carrier |] ==> x \<sqsubseteq> s"
   4.316    by (unfold least_def) blast
   4.317  
   4.318 -lemma greatest_Lower_above:
   4.319 -  fixes L (structure)
   4.320 -  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   4.321 +lemma (in order_syntax) greatest_Lower_above:
   4.322 +  "[| greatest i (Lower A); x \<in> A; A \<subseteq> carrier |] ==> i \<sqsubseteq> x"
   4.323    by (unfold greatest_def) blast
   4.324  
   4.325  
   4.326  subsubsection {* Supremum *}
   4.327  
   4.328  lemma (in lattice) joinI:
   4.329 -  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   4.330 +  "[| !!l. least l (Upper {x, y}) ==> P l; x \<in> carrier; y \<in> carrier |]
   4.331    ==> P (x \<squnion> y)"
   4.332  proof (unfold join_def sup_def)
   4.333 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.334 -    and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   4.335 -  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   4.336 -  with L show "P (THE l. least L l (Upper L {x, y}))"
   4.337 +  assume L: "x \<in> carrier"  "y \<in> carrier"
   4.338 +    and P: "!!l. least l (Upper {x, y}) ==> P l"
   4.339 +  with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast
   4.340 +  with L show "P (THE l. least l (Upper {x, y}))"
   4.341      by (fast intro: theI2 least_unique P)
   4.342  qed
   4.343  
   4.344  lemma (in lattice) join_closed [simp]:
   4.345 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   4.346 +  "[| x \<in> carrier; y \<in> carrier |] ==> x \<squnion> y \<in> carrier"
   4.347    by (rule joinI) (rule least_carrier)
   4.348  
   4.349 -lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   4.350 -  "x \<in> carrier L ==> least L x (Upper L {x})"
   4.351 +lemma (in partial_order) sup_of_singletonI:     (* only reflexivity needed ? *)
   4.352 +  "x \<in> carrier ==> least x (Upper {x})"
   4.353    by (rule least_UpperI) fast+
   4.354  
   4.355  lemma (in partial_order) sup_of_singleton [simp]:
   4.356 -  "x \<in> carrier L ==> \<Squnion>{x} = x"
   4.357 +  "x \<in> carrier ==> \<Squnion>{x} = x"
   4.358    by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   4.359  
   4.360  
   4.361  text {* Condition on @{text A}: supremum exists. *}
   4.362  
   4.363  lemma (in lattice) sup_insertI:
   4.364 -  "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   4.365 -  least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   4.366 +  "[| !!s. least s (Upper (insert x A)) ==> P s;
   4.367 +  least a (Upper A); x \<in> carrier; A \<subseteq> carrier |]
   4.368    ==> P (\<Squnion>(insert x A))"
   4.369  proof (unfold sup_def)
   4.370 -  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   4.371 -    and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   4.372 -    and least_a: "least L a (Upper L A)"
   4.373 -  from L least_a have La: "a \<in> carrier L" by simp
   4.374 +  assume L: "x \<in> carrier"  "A \<subseteq> carrier"
   4.375 +    and P: "!!l. least l (Upper (insert x A)) ==> P l"
   4.376 +    and least_a: "least a (Upper A)"
   4.377 +  from least_a have La: "a \<in> carrier" by simp
   4.378    from L sup_of_two_exists least_a
   4.379 -  obtain s where least_s: "least L s (Upper L {a, x})" by blast
   4.380 -  show "P (THE l. least L l (Upper L (insert x A)))"
   4.381 +  obtain s where least_s: "least s (Upper {a, x})" by blast
   4.382 +  show "P (THE l. least l (Upper (insert x A)))"
   4.383    proof (rule theI2)
   4.384 -    show "least L s (Upper L (insert x A))"
   4.385 +    show "least s (Upper (insert x A))"
   4.386      proof (rule least_UpperI)
   4.387        fix z
   4.388        assume "z \<in> insert x A"
   4.389 @@ -248,15 +299,15 @@
   4.390        qed
   4.391      next
   4.392        fix y
   4.393 -      assume y: "y \<in> Upper L (insert x A)"
   4.394 +      assume y: "y \<in> Upper (insert x A)"
   4.395        show "s \<sqsubseteq> y"
   4.396        proof (rule least_le [OF least_s], rule Upper_memI)
   4.397  	fix z
   4.398  	assume z: "z \<in> {a, x}"
   4.399  	then show "z \<sqsubseteq> y"
   4.400  	proof
   4.401 -          have y': "y \<in> Upper L A"
   4.402 -            apply (rule subsetD [where A = "Upper L (insert x A)"])
   4.403 +          have y': "y \<in> Upper A"
   4.404 +            apply (rule subsetD [where A = "Upper (insert x A)"])
   4.405              apply (rule Upper_antimono) apply clarify apply assumption
   4.406              done
   4.407            assume "z = a"
   4.408 @@ -267,15 +318,15 @@
   4.409  	qed
   4.410        qed (rule Upper_closed [THEN subsetD])
   4.411      next
   4.412 -      from L show "insert x A \<subseteq> carrier L" by simp
   4.413 -      from least_s show "s \<in> carrier L" by simp
   4.414 +      from L show "insert x A \<subseteq> carrier" by simp
   4.415 +      from least_s show "s \<in> carrier" by simp
   4.416      qed
   4.417    next
   4.418      fix l
   4.419 -    assume least_l: "least L l (Upper L (insert x A))"
   4.420 +    assume least_l: "least l (Upper (insert x A))"
   4.421      show "l = s"
   4.422      proof (rule least_unique)
   4.423 -      show "least L s (Upper L (insert x A))"
   4.424 +      show "least s (Upper (insert x A))"
   4.425        proof (rule least_UpperI)
   4.426          fix z
   4.427          assume "z \<in> insert x A"
   4.428 @@ -290,15 +341,15 @@
   4.429  	qed
   4.430        next
   4.431          fix y
   4.432 -        assume y: "y \<in> Upper L (insert x A)"
   4.433 +        assume y: "y \<in> Upper (insert x A)"
   4.434          show "s \<sqsubseteq> y"
   4.435          proof (rule least_le [OF least_s], rule Upper_memI)
   4.436            fix z
   4.437            assume z: "z \<in> {a, x}"
   4.438            then show "z \<sqsubseteq> y"
   4.439            proof
   4.440 -            have y': "y \<in> Upper L A"
   4.441 -	      apply (rule subsetD [where A = "Upper L (insert x A)"])
   4.442 +            have y': "y \<in> Upper A"
   4.443 +	      apply (rule subsetD [where A = "Upper (insert x A)"])
   4.444  	      apply (rule Upper_antimono) apply clarify apply assumption
   4.445  	      done
   4.446              assume "z = a"
   4.447 @@ -309,15 +360,15 @@
   4.448            qed
   4.449          qed (rule Upper_closed [THEN subsetD])
   4.450        next
   4.451 -        from L show "insert x A \<subseteq> carrier L" by simp
   4.452 -        from least_s show "s \<in> carrier L" by simp
   4.453 +        from L show "insert x A \<subseteq> carrier" by simp
   4.454 +        from least_s show "s \<in> carrier" by simp
   4.455        qed
   4.456      qed
   4.457    qed
   4.458  qed
   4.459  
   4.460  lemma (in lattice) finite_sup_least:
   4.461 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   4.462 +  "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> least (\<Squnion>A) (Upper A)"
   4.463  proof (induct set: Finites)
   4.464    case empty
   4.465    then show ?case by simp
   4.466 @@ -329,15 +380,15 @@
   4.467      with insert show ?thesis by (simp add: sup_of_singletonI)
   4.468    next
   4.469      case False
   4.470 -    with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   4.471 +    with insert have "least (\<Squnion>A) (Upper A)" by simp
   4.472      with _ show ?thesis
   4.473        by (rule sup_insertI) (simp_all add: insert [simplified])
   4.474    qed
   4.475  qed
   4.476  
   4.477  lemma (in lattice) finite_sup_insertI:
   4.478 -  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   4.479 -    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   4.480 +  assumes P: "!!l. least l (Upper (insert x A)) ==> P l"
   4.481 +    and xA: "finite A"  "x \<in> carrier"  "A \<subseteq> carrier"
   4.482    shows "P (\<Squnion> (insert x A))"
   4.483  proof (cases "A = {}")
   4.484    case True with P and xA show ?thesis
   4.485 @@ -348,7 +399,7 @@
   4.486  qed
   4.487  
   4.488  lemma (in lattice) finite_sup_closed:
   4.489 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   4.490 +  "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> \<Squnion>A \<in> carrier"
   4.491  proof (induct set: Finites)
   4.492    case empty then show ?case by simp
   4.493  next
   4.494 @@ -357,39 +408,39 @@
   4.495  qed
   4.496  
   4.497  lemma (in lattice) join_left:
   4.498 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   4.499 +  "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> x \<squnion> y"
   4.500    by (rule joinI [folded join_def]) (blast dest: least_mem)
   4.501  
   4.502  lemma (in lattice) join_right:
   4.503 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   4.504 +  "[| x \<in> carrier; y \<in> carrier |] ==> y \<sqsubseteq> x \<squnion> y"
   4.505    by (rule joinI [folded join_def]) (blast dest: least_mem)
   4.506  
   4.507  lemma (in lattice) sup_of_two_least:
   4.508 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   4.509 +  "[| x \<in> carrier; y \<in> carrier |] ==> least (\<Squnion>{x, y}) (Upper {x, y})"
   4.510  proof (unfold sup_def)
   4.511 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.512 -  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   4.513 -  with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
   4.514 +  assume L: "x \<in> carrier"  "y \<in> carrier"
   4.515 +  with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast
   4.516 +  with L show "least (THE xa. least xa (Upper {x, y})) (Upper {x, y})"
   4.517    by (fast intro: theI2 least_unique)  (* blast fails *)
   4.518  qed
   4.519  
   4.520  lemma (in lattice) join_le:
   4.521    assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   4.522 -    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.523 +    and L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.524    shows "x \<squnion> y \<sqsubseteq> z"
   4.525  proof (rule joinI)
   4.526    fix s
   4.527 -  assume "least L s (Upper L {x, y})"
   4.528 +  assume "least s (Upper {x, y})"
   4.529    with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   4.530  qed
   4.531  
   4.532  lemma (in lattice) join_assoc_lemma:
   4.533 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.534 +  assumes L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.535    shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   4.536  proof (rule finite_sup_insertI)
   4.537    -- {* The textbook argument in Jacobson I, p 457 *}
   4.538    fix s
   4.539 -  assume sup: "least L s (Upper L {x, y, z})"
   4.540 +  assume sup: "least s (Upper {x, y, z})"
   4.541    show "x \<squnion> (y \<squnion> z) = s"
   4.542    proof (rule anti_sym)
   4.543      from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   4.544 @@ -401,13 +452,12 @@
   4.545    qed (simp_all add: L least_carrier [OF sup])
   4.546  qed (simp_all add: L)
   4.547  
   4.548 -lemma join_comm:
   4.549 -  fixes L (structure)
   4.550 -  shows "x \<squnion> y = y \<squnion> x"
   4.551 +lemma (in order_syntax) join_comm:
   4.552 +  "x \<squnion> y = y \<squnion> x"
   4.553    by (unfold join_def) (simp add: insert_commute)
   4.554  
   4.555  lemma (in lattice) join_assoc:
   4.556 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.557 +  assumes L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.558    shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   4.559  proof -
   4.560    have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   4.561 @@ -421,45 +471,45 @@
   4.562  subsubsection {* Infimum *}
   4.563  
   4.564  lemma (in lattice) meetI:
   4.565 -  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   4.566 -  x \<in> carrier L; y \<in> carrier L |]
   4.567 +  "[| !!i. greatest i (Lower {x, y}) ==> P i;
   4.568 +  x \<in> carrier; y \<in> carrier |]
   4.569    ==> P (x \<sqinter> y)"
   4.570  proof (unfold meet_def inf_def)
   4.571 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.572 -    and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   4.573 -  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   4.574 -  with L show "P (THE g. greatest L g (Lower L {x, y}))"
   4.575 +  assume L: "x \<in> carrier"  "y \<in> carrier"
   4.576 +    and P: "!!g. greatest g (Lower {x, y}) ==> P g"
   4.577 +  with inf_of_two_exists obtain i where "greatest i (Lower {x, y})" by fast
   4.578 +  with L show "P (THE g. greatest g (Lower {x, y}))"
   4.579    by (fast intro: theI2 greatest_unique P)
   4.580  qed
   4.581  
   4.582  lemma (in lattice) meet_closed [simp]:
   4.583 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   4.584 +  "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<in> carrier"
   4.585    by (rule meetI) (rule greatest_carrier)
   4.586  
   4.587  lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   4.588 -  "x \<in> carrier L ==> greatest L x (Lower L {x})"
   4.589 +  "x \<in> carrier ==> greatest x (Lower {x})"
   4.590    by (rule greatest_LowerI) fast+
   4.591  
   4.592  lemma (in partial_order) inf_of_singleton [simp]:
   4.593 -  "x \<in> carrier L ==> \<Sqinter> {x} = x"
   4.594 +  "x \<in> carrier ==> \<Sqinter> {x} = x"
   4.595    by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   4.596  
   4.597  text {* Condition on A: infimum exists. *}
   4.598  
   4.599  lemma (in lattice) inf_insertI:
   4.600 -  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   4.601 -  greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   4.602 +  "[| !!i. greatest i (Lower (insert x A)) ==> P i;
   4.603 +  greatest a (Lower A); x \<in> carrier; A \<subseteq> carrier |]
   4.604    ==> P (\<Sqinter>(insert x A))"
   4.605  proof (unfold inf_def)
   4.606 -  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   4.607 -    and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   4.608 -    and greatest_a: "greatest L a (Lower L A)"
   4.609 -  from L greatest_a have La: "a \<in> carrier L" by simp
   4.610 +  assume L: "x \<in> carrier"  "A \<subseteq> carrier"
   4.611 +    and P: "!!g. greatest g (Lower (insert x A)) ==> P g"
   4.612 +    and greatest_a: "greatest a (Lower A)"
   4.613 +  from greatest_a have La: "a \<in> carrier" by simp
   4.614    from L inf_of_two_exists greatest_a
   4.615 -  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   4.616 -  show "P (THE g. greatest L g (Lower L (insert x A)))"
   4.617 +  obtain i where greatest_i: "greatest i (Lower {a, x})" by blast
   4.618 +  show "P (THE g. greatest g (Lower (insert x A)))"
   4.619    proof (rule theI2)
   4.620 -    show "greatest L i (Lower L (insert x A))"
   4.621 +    show "greatest i (Lower (insert x A))"
   4.622      proof (rule greatest_LowerI)
   4.623        fix z
   4.624        assume "z \<in> insert x A"
   4.625 @@ -474,15 +524,15 @@
   4.626        qed
   4.627      next
   4.628        fix y
   4.629 -      assume y: "y \<in> Lower L (insert x A)"
   4.630 +      assume y: "y \<in> Lower (insert x A)"
   4.631        show "y \<sqsubseteq> i"
   4.632        proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   4.633  	fix z
   4.634  	assume z: "z \<in> {a, x}"
   4.635  	then show "y \<sqsubseteq> z"
   4.636  	proof
   4.637 -          have y': "y \<in> Lower L A"
   4.638 -            apply (rule subsetD [where A = "Lower L (insert x A)"])
   4.639 +          have y': "y \<in> Lower A"
   4.640 +            apply (rule subsetD [where A = "Lower (insert x A)"])
   4.641              apply (rule Lower_antimono) apply clarify apply assumption
   4.642              done
   4.643            assume "z = a"
   4.644 @@ -493,15 +543,15 @@
   4.645  	qed
   4.646        qed (rule Lower_closed [THEN subsetD])
   4.647      next
   4.648 -      from L show "insert x A \<subseteq> carrier L" by simp
   4.649 -      from greatest_i show "i \<in> carrier L" by simp
   4.650 +      from L show "insert x A \<subseteq> carrier" by simp
   4.651 +      from greatest_i show "i \<in> carrier" by simp
   4.652      qed
   4.653    next
   4.654      fix g
   4.655 -    assume greatest_g: "greatest L g (Lower L (insert x A))"
   4.656 +    assume greatest_g: "greatest g (Lower (insert x A))"
   4.657      show "g = i"
   4.658      proof (rule greatest_unique)
   4.659 -      show "greatest L i (Lower L (insert x A))"
   4.660 +      show "greatest i (Lower (insert x A))"
   4.661        proof (rule greatest_LowerI)
   4.662          fix z
   4.663          assume "z \<in> insert x A"
   4.664 @@ -516,15 +566,15 @@
   4.665          qed
   4.666        next
   4.667          fix y
   4.668 -        assume y: "y \<in> Lower L (insert x A)"
   4.669 +        assume y: "y \<in> Lower (insert x A)"
   4.670          show "y \<sqsubseteq> i"
   4.671          proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   4.672            fix z
   4.673            assume z: "z \<in> {a, x}"
   4.674            then show "y \<sqsubseteq> z"
   4.675            proof
   4.676 -            have y': "y \<in> Lower L A"
   4.677 -	      apply (rule subsetD [where A = "Lower L (insert x A)"])
   4.678 +            have y': "y \<in> Lower A"
   4.679 +	      apply (rule subsetD [where A = "Lower (insert x A)"])
   4.680  	      apply (rule Lower_antimono) apply clarify apply assumption
   4.681  	      done
   4.682              assume "z = a"
   4.683 @@ -535,15 +585,15 @@
   4.684  	  qed
   4.685          qed (rule Lower_closed [THEN subsetD])
   4.686        next
   4.687 -        from L show "insert x A \<subseteq> carrier L" by simp
   4.688 -        from greatest_i show "i \<in> carrier L" by simp
   4.689 +        from L show "insert x A \<subseteq> carrier" by simp
   4.690 +        from greatest_i show "i \<in> carrier" by simp
   4.691        qed
   4.692      qed
   4.693    qed
   4.694  qed
   4.695  
   4.696  lemma (in lattice) finite_inf_greatest:
   4.697 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   4.698 +  "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> greatest (\<Sqinter>A) (Lower A)"
   4.699  proof (induct set: Finites)
   4.700    case empty then show ?case by simp
   4.701  next
   4.702 @@ -556,14 +606,14 @@
   4.703      case False
   4.704      from insert show ?thesis
   4.705      proof (rule_tac inf_insertI)
   4.706 -      from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   4.707 +      from False insert show "greatest (\<Sqinter>A) (Lower A)" by simp
   4.708      qed simp_all
   4.709    qed
   4.710  qed
   4.711  
   4.712  lemma (in lattice) finite_inf_insertI:
   4.713 -  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   4.714 -    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   4.715 +  assumes P: "!!i. greatest i (Lower (insert x A)) ==> P i"
   4.716 +    and xA: "finite A"  "x \<in> carrier"  "A \<subseteq> carrier"
   4.717    shows "P (\<Sqinter> (insert x A))"
   4.718  proof (cases "A = {}")
   4.719    case True with P and xA show ?thesis
   4.720 @@ -574,7 +624,7 @@
   4.721  qed
   4.722  
   4.723  lemma (in lattice) finite_inf_closed:
   4.724 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   4.725 +  "[| finite A; A \<subseteq> carrier; A ~= {} |] ==> \<Sqinter>A \<in> carrier"
   4.726  proof (induct set: Finites)
   4.727    case empty then show ?case by simp
   4.728  next
   4.729 @@ -583,41 +633,41 @@
   4.730  qed
   4.731  
   4.732  lemma (in lattice) meet_left:
   4.733 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   4.734 +  "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<sqsubseteq> x"
   4.735    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   4.736  
   4.737  lemma (in lattice) meet_right:
   4.738 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   4.739 +  "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqinter> y \<sqsubseteq> y"
   4.740    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   4.741  
   4.742  lemma (in lattice) inf_of_two_greatest:
   4.743 -  "[| x \<in> carrier L; y \<in> carrier L |] ==>
   4.744 -  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   4.745 +  "[| x \<in> carrier; y \<in> carrier |] ==>
   4.746 +  greatest (\<Sqinter> {x, y}) (Lower {x, y})"
   4.747  proof (unfold inf_def)
   4.748 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.749 -  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   4.750 +  assume L: "x \<in> carrier"  "y \<in> carrier"
   4.751 +  with inf_of_two_exists obtain s where "greatest s (Lower {x, y})" by fast
   4.752    with L
   4.753 -  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
   4.754 +  show "greatest (THE xa. greatest xa (Lower {x, y})) (Lower {x, y})"
   4.755    by (fast intro: theI2 greatest_unique)  (* blast fails *)
   4.756  qed
   4.757  
   4.758  lemma (in lattice) meet_le:
   4.759    assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   4.760 -    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.761 +    and L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.762    shows "z \<sqsubseteq> x \<sqinter> y"
   4.763  proof (rule meetI)
   4.764    fix i
   4.765 -  assume "greatest L i (Lower L {x, y})"
   4.766 +  assume "greatest i (Lower {x, y})"
   4.767    with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   4.768  qed
   4.769  
   4.770  lemma (in lattice) meet_assoc_lemma:
   4.771 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.772 +  assumes L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.773    shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   4.774  proof (rule finite_inf_insertI)
   4.775    txt {* The textbook argument in Jacobson I, p 457 *}
   4.776    fix i
   4.777 -  assume inf: "greatest L i (Lower L {x, y, z})"
   4.778 +  assume inf: "greatest i (Lower {x, y, z})"
   4.779    show "x \<sqinter> (y \<sqinter> z) = i"
   4.780    proof (rule anti_sym)
   4.781      from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   4.782 @@ -629,13 +679,12 @@
   4.783    qed (simp_all add: L greatest_carrier [OF inf])
   4.784  qed (simp_all add: L)
   4.785  
   4.786 -lemma meet_comm:
   4.787 -  fixes L (structure)
   4.788 -  shows "x \<sqinter> y = y \<sqinter> x"
   4.789 +lemma (in order_syntax) meet_comm:
   4.790 +  "x \<sqinter> y = y \<sqinter> x"
   4.791    by (unfold meet_def) (simp add: insert_commute)
   4.792  
   4.793  lemma (in lattice) meet_assoc:
   4.794 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   4.795 +  assumes L: "x \<in> carrier"  "y \<in> carrier"  "z \<in> carrier"
   4.796    shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   4.797  proof -
   4.798    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   4.799 @@ -649,51 +698,70 @@
   4.800  subsection {* Total Orders *}
   4.801  
   4.802  locale total_order = lattice +
   4.803 -  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   4.804 +  assumes total: "[| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   4.805 +
   4.806 +abbreviation (in total_order)
   4.807 +  less (infixl "\<sqsubset>" 50) "less == order_syntax.less le"
   4.808 +abbreviation (in total_order)
   4.809 +  Upper where "Upper == order_syntax.Upper carrier le"
   4.810 +abbreviation (in total_order)
   4.811 +  Lower where "Lower == order_syntax.Lower carrier le"
   4.812 +abbreviation (in total_order)
   4.813 +  least where "least == order_syntax.least carrier le"
   4.814 +abbreviation (in total_order)
   4.815 +  greatest where "greatest == order_syntax.greatest carrier le"
   4.816 +abbreviation (in total_order)
   4.817 +  sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le"
   4.818 +abbreviation (in total_order)
   4.819 +  inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le"
   4.820 +abbreviation (in total_order)
   4.821 +  join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le"
   4.822 +abbreviation (in total_order)
   4.823 +  meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le"
   4.824  
   4.825  text {* Introduction rule: the usual definition of total order *}
   4.826  
   4.827  lemma (in partial_order) total_orderI:
   4.828 -  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   4.829 -  shows "total_order L"
   4.830 +  assumes total: "!!x y. [| x \<in> carrier; y \<in> carrier |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   4.831 +  shows "total_order carrier le"
   4.832  proof intro_locales
   4.833 -  show "lattice_axioms L"
   4.834 +  show "lattice_axioms carrier le"
   4.835    proof (rule lattice_axioms.intro)
   4.836      fix x y
   4.837 -    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.838 -    show "EX s. least L s (Upper L {x, y})"
   4.839 +    assume L: "x \<in> carrier"  "y \<in> carrier"
   4.840 +    show "EX s. least s (Upper {x, y})"
   4.841      proof -
   4.842        note total L
   4.843        moreover
   4.844        {
   4.845          assume "x \<sqsubseteq> y"
   4.846 -        with L have "least L y (Upper L {x, y})"
   4.847 +        with L have "least y (Upper {x, y})"
   4.848            by (rule_tac least_UpperI) auto
   4.849        }
   4.850        moreover
   4.851        {
   4.852          assume "y \<sqsubseteq> x"
   4.853 -        with L have "least L x (Upper L {x, y})"
   4.854 +        with L have "least x (Upper {x, y})"
   4.855            by (rule_tac least_UpperI) auto
   4.856        }
   4.857        ultimately show ?thesis by blast
   4.858      qed
   4.859    next
   4.860      fix x y
   4.861 -    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   4.862 -    show "EX i. greatest L i (Lower L {x, y})"
   4.863 +    assume L: "x \<in> carrier"  "y \<in> carrier"
   4.864 +    show "EX i. greatest i (Lower {x, y})"
   4.865      proof -
   4.866        note total L
   4.867        moreover
   4.868        {
   4.869          assume "y \<sqsubseteq> x"
   4.870 -        with L have "greatest L y (Lower L {x, y})"
   4.871 +        with L have "greatest y (Lower {x, y})"
   4.872            by (rule_tac greatest_LowerI) auto
   4.873        }
   4.874        moreover
   4.875        {
   4.876          assume "x \<sqsubseteq> y"
   4.877 -        with L have "greatest L x (Lower L {x, y})"
   4.878 +        with L have "greatest x (Lower {x, y})"
   4.879            by (rule_tac greatest_LowerI) auto
   4.880        }
   4.881        ultimately show ?thesis by blast
   4.882 @@ -706,97 +774,134 @@
   4.883  
   4.884  locale complete_lattice = lattice +
   4.885    assumes sup_exists:
   4.886 -    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   4.887 +    "[| A \<subseteq> carrier |] ==> EX s. order_syntax.least carrier le s (order_syntax.Upper carrier le A)"
   4.888      and inf_exists:
   4.889 -    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   4.890 +    "[| A \<subseteq> carrier |] ==> EX i. order_syntax.greatest carrier le i (order_syntax.Lower carrier le A)"
   4.891 +
   4.892 +abbreviation (in complete_lattice)
   4.893 +  less (infixl "\<sqsubset>" 50) "less == order_syntax.less le"
   4.894 +abbreviation (in complete_lattice)
   4.895 +  Upper where "Upper == order_syntax.Upper carrier le"
   4.896 +abbreviation (in complete_lattice)
   4.897 +  Lower where "Lower == order_syntax.Lower carrier le"
   4.898 +abbreviation (in complete_lattice)
   4.899 +  least where "least == order_syntax.least carrier le"
   4.900 +abbreviation (in complete_lattice)
   4.901 +  greatest where "greatest == order_syntax.greatest carrier le"
   4.902 +abbreviation (in complete_lattice)
   4.903 +  sup ("\<Squnion>") (* FIXME precedence *) "sup == order_syntax.sup carrier le"
   4.904 +abbreviation (in complete_lattice)
   4.905 +  inf ("\<Sqinter>") (* FIXME precedence *) "inf == order_syntax.inf carrier le"
   4.906 +abbreviation (in complete_lattice)
   4.907 +  join (infixl "\<squnion>" 65) "join == order_syntax.join carrier le"
   4.908 +abbreviation (in complete_lattice)
   4.909 +  meet (infixl "\<sqinter>" 70) "meet == order_syntax.meet carrier le"
   4.910  
   4.911  text {* Introduction rule: the usual definition of complete lattice *}
   4.912  
   4.913  lemma (in partial_order) complete_latticeI:
   4.914    assumes sup_exists:
   4.915 -    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   4.916 +    "!!A. [| A \<subseteq> carrier |] ==> EX s. least s (Upper A)"
   4.917      and inf_exists:
   4.918 -    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   4.919 -  shows "complete_lattice L"
   4.920 +    "!!A. [| A \<subseteq> carrier |] ==> EX i. greatest i (Lower A)"
   4.921 +  shows "complete_lattice carrier le"
   4.922  proof intro_locales
   4.923 -  show "lattice_axioms L"
   4.924 +  show "lattice_axioms carrier le"
   4.925      by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   4.926  qed (assumption | rule complete_lattice_axioms.intro)+
   4.927  
   4.928 -constdefs (structure L)
   4.929 -  top :: "_ => 'a" ("\<top>\<index>")
   4.930 -  "\<top> == sup L (carrier L)"
   4.931 +definition (in order_syntax)
   4.932 +  top ("\<top>")
   4.933 +  "\<top> == sup carrier"
   4.934 +
   4.935 +definition (in order_syntax)
   4.936 +  bottom ("\<bottom>")
   4.937 +  "\<bottom> == inf carrier"
   4.938  
   4.939 -  bottom :: "_ => 'a" ("\<bottom>\<index>")
   4.940 -  "\<bottom> == inf L (carrier L)"
   4.941 +abbreviation (in partial_order)
   4.942 +  top ("\<top>") "top == order_syntax.top carrier le"
   4.943 +abbreviation (in partial_order)
   4.944 +  bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le"
   4.945 +abbreviation (in lattice)
   4.946 +  top ("\<top>") "top == order_syntax.top carrier le"
   4.947 +abbreviation (in lattice)
   4.948 +  bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le"
   4.949 +abbreviation (in total_order)
   4.950 +  top ("\<top>") "top == order_syntax.top carrier le"
   4.951 +abbreviation (in total_order)
   4.952 +  bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le"
   4.953 +abbreviation (in complete_lattice)
   4.954 +  top ("\<top>") "top == order_syntax.top carrier le"
   4.955 +abbreviation (in complete_lattice)
   4.956 +  bottom ("\<bottom>") "bottom == order_syntax.bottom carrier le"
   4.957  
   4.958  
   4.959  lemma (in complete_lattice) supI:
   4.960 -  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   4.961 +  "[| !!l. least l (Upper A) ==> P l; A \<subseteq> carrier |]
   4.962    ==> P (\<Squnion>A)"
   4.963  proof (unfold sup_def)
   4.964 -  assume L: "A \<subseteq> carrier L"
   4.965 -    and P: "!!l. least L l (Upper L A) ==> P l"
   4.966 -  with sup_exists obtain s where "least L s (Upper L A)" by blast
   4.967 -  with L show "P (THE l. least L l (Upper L A))"
   4.968 +  assume L: "A \<subseteq> carrier"
   4.969 +    and P: "!!l. least l (Upper A) ==> P l"
   4.970 +  with sup_exists obtain s where "least s (Upper A)" by blast
   4.971 +  with L show "P (THE l. least l (Upper A))"
   4.972    by (fast intro: theI2 least_unique P)
   4.973  qed
   4.974  
   4.975  lemma (in complete_lattice) sup_closed [simp]:
   4.976 -  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   4.977 +  "A \<subseteq> carrier ==> \<Squnion>A \<in> carrier"
   4.978    by (rule supI) simp_all
   4.979  
   4.980  lemma (in complete_lattice) top_closed [simp, intro]:
   4.981 -  "\<top> \<in> carrier L"
   4.982 +  "\<top> \<in> carrier"
   4.983    by (unfold top_def) simp
   4.984  
   4.985  lemma (in complete_lattice) infI:
   4.986 -  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   4.987 +  "[| !!i. greatest i (Lower A) ==> P i; A \<subseteq> carrier |]
   4.988    ==> P (\<Sqinter>A)"
   4.989  proof (unfold inf_def)
   4.990 -  assume L: "A \<subseteq> carrier L"
   4.991 -    and P: "!!l. greatest L l (Lower L A) ==> P l"
   4.992 -  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
   4.993 -  with L show "P (THE l. greatest L l (Lower L A))"
   4.994 +  assume L: "A \<subseteq> carrier"
   4.995 +    and P: "!!l. greatest l (Lower A) ==> P l"
   4.996 +  with inf_exists obtain s where "greatest s (Lower A)" by blast
   4.997 +  with L show "P (THE l. greatest l (Lower A))"
   4.998    by (fast intro: theI2 greatest_unique P)
   4.999  qed
  4.1000  
  4.1001  lemma (in complete_lattice) inf_closed [simp]:
  4.1002 -  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
  4.1003 +  "A \<subseteq> carrier ==> \<Sqinter>A \<in> carrier"
  4.1004    by (rule infI) simp_all
  4.1005  
  4.1006  lemma (in complete_lattice) bottom_closed [simp, intro]:
  4.1007 -  "\<bottom> \<in> carrier L"
  4.1008 +  "\<bottom> \<in> carrier"
  4.1009    by (unfold bottom_def) simp
  4.1010  
  4.1011  text {* Jacobson: Theorem 8.1 *}
  4.1012  
  4.1013 -lemma Lower_empty [simp]:
  4.1014 -  "Lower L {} = carrier L"
  4.1015 +lemma (in order_syntax) Lower_empty [simp]:
  4.1016 +  "Lower {} = carrier"
  4.1017    by (unfold Lower_def) simp
  4.1018  
  4.1019 -lemma Upper_empty [simp]:
  4.1020 -  "Upper L {} = carrier L"
  4.1021 +lemma (in order_syntax) Upper_empty [simp]:
  4.1022 +  "Upper {} = carrier"
  4.1023    by (unfold Upper_def) simp
  4.1024  
  4.1025  theorem (in partial_order) complete_lattice_criterion1:
  4.1026 -  assumes top_exists: "EX g. greatest L g (carrier L)"
  4.1027 +  assumes top_exists: "EX g. greatest g (carrier)"
  4.1028      and inf_exists:
  4.1029 -      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
  4.1030 -  shows "complete_lattice L"
  4.1031 +      "!!A. [| A \<subseteq> carrier; A ~= {} |] ==> EX i. greatest i (Lower A)"
  4.1032 +  shows "complete_lattice carrier le"
  4.1033  proof (rule complete_latticeI)
  4.1034 -  from top_exists obtain top where top: "greatest L top (carrier L)" ..
  4.1035 +  from top_exists obtain top where top: "greatest top (carrier)" ..
  4.1036    fix A
  4.1037 -  assume L: "A \<subseteq> carrier L"
  4.1038 -  let ?B = "Upper L A"
  4.1039 +  assume L: "A \<subseteq> carrier"
  4.1040 +  let ?B = "Upper A"
  4.1041    from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
  4.1042    then have B_non_empty: "?B ~= {}" by fast
  4.1043 -  have B_L: "?B \<subseteq> carrier L" by simp
  4.1044 +  have B_L: "?B \<subseteq> carrier" by simp
  4.1045    from inf_exists [OF B_L B_non_empty]
  4.1046 -  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
  4.1047 -  have "least L b (Upper L A)"
  4.1048 +  obtain b where b_inf_B: "greatest b (Lower ?B)" ..
  4.1049 +  have "least b (Upper A)"
  4.1050  apply (rule least_UpperI)
  4.1051 -   apply (rule greatest_le [where A = "Lower L ?B"])
  4.1052 +   apply (rule greatest_le [where A = "Lower ?B"])
  4.1053      apply (rule b_inf_B)
  4.1054     apply (rule Lower_memI)
  4.1055      apply (erule UpperD)
  4.1056 @@ -808,11 +913,11 @@
  4.1057   apply (rule L)
  4.1058  apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)
  4.1059  done
  4.1060 -  then show "EX s. least L s (Upper L A)" ..
  4.1061 +  then show "EX s. least s (Upper A)" ..
  4.1062  next
  4.1063    fix A
  4.1064 -  assume L: "A \<subseteq> carrier L"
  4.1065 -  show "EX i. greatest L i (Lower L A)"
  4.1066 +  assume L: "A \<subseteq> carrier"
  4.1067 +  show "EX i. greatest i (Lower A)"
  4.1068    proof (cases "A = {}")
  4.1069      case True then show ?thesis
  4.1070        by (simp add: top_exists)
  4.1071 @@ -830,25 +935,25 @@
  4.1072  subsubsection {* Powerset of a Set is a Complete Lattice *}
  4.1073  
  4.1074  theorem powerset_is_complete_lattice:
  4.1075 -  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
  4.1076 -  (is "complete_lattice ?L")
  4.1077 +  "complete_lattice (Pow A) (op \<subseteq>)"
  4.1078 +  (is "complete_lattice ?car ?le")
  4.1079  proof (rule partial_order.complete_latticeI)
  4.1080 -  show "partial_order ?L"
  4.1081 +  show "partial_order ?car ?le"
  4.1082      by (rule partial_order.intro) auto
  4.1083  next
  4.1084    fix B
  4.1085 -  assume "B \<subseteq> carrier ?L"
  4.1086 -  then have "least ?L (\<Union> B) (Upper ?L B)"
  4.1087 -    by (fastsimp intro!: least_UpperI simp: Upper_def)
  4.1088 -  then show "EX s. least ?L s (Upper ?L B)" ..
  4.1089 +  assume "B \<subseteq> ?car"
  4.1090 +  then have "order_syntax.least ?car ?le (\<Union> B) (order_syntax.Upper ?car ?le B)"
  4.1091 +    by (fastsimp intro!: order_syntax.least_UpperI simp: order_syntax.Upper_def)
  4.1092 +  then show "EX s. order_syntax.least ?car ?le s (order_syntax.Upper ?car ?le B)" ..
  4.1093  next
  4.1094    fix B
  4.1095 -  assume "B \<subseteq> carrier ?L"
  4.1096 -  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
  4.1097 +  assume "B \<subseteq> ?car"
  4.1098 +  then have "order_syntax.greatest ?car ?le (\<Inter> B \<inter> A) (order_syntax.Lower ?car ?le B)"
  4.1099      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
  4.1100        @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
  4.1101 -    by (fastsimp intro!: greatest_LowerI simp: Lower_def)
  4.1102 -  then show "EX i. greatest ?L i (Lower ?L B)" ..
  4.1103 +    by (fastsimp intro!: order_syntax.greatest_LowerI simp: order_syntax.Lower_def)
  4.1104 +  then show "EX i. order_syntax.greatest ?car ?le i (order_syntax.Lower ?car ?le B)" ..
  4.1105  qed
  4.1106  
  4.1107  text {* An other example, that of the lattice of subgroups of a group,