Reverted to structure representation with records.
authorballarin
Fri Jan 12 15:37:21 2007 +0100 (2007-01-12)
changeset 22063717425609192
parent 22062 f4cfc4101c8f
child 22064 3d716cc9bd7a
Reverted to structure representation with records.
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
     1.1 --- a/src/HOL/Algebra/Group.thy	Fri Jan 12 09:58:31 2007 +0100
     1.2 +++ b/src/HOL/Algebra/Group.thy	Fri Jan 12 15:37:21 2007 +0100
     1.3 @@ -685,7 +685,7 @@
     1.4  text_raw {* \label{sec:subgroup-lattice} *}
     1.5  
     1.6  theorem (in group) subgroups_partial_order:
     1.7 -  "partial_order {H. subgroup H G} (op \<subseteq>)"
     1.8 +  "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
     1.9    by (rule partial_order.intro) simp_all
    1.10  
    1.11  lemma (in group) subgroup_self:
    1.12 @@ -730,23 +730,23 @@
    1.13  qed
    1.14  
    1.15  theorem (in group) subgroups_complete_lattice:
    1.16 -  "complete_lattice {H. subgroup H G} (op \<subseteq>)"
    1.17 -    (is "complete_lattice ?car ?le")
    1.18 +  "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
    1.19 +    (is "complete_lattice ?L")
    1.20  proof (rule partial_order.complete_lattice_criterion1)
    1.21 -  show "partial_order ?car ?le" by (rule subgroups_partial_order)
    1.22 +  show "partial_order ?L" by (rule subgroups_partial_order)
    1.23  next
    1.24 -  have "order_syntax.greatest ?car ?le (carrier G) ?car"
    1.25 -    by (unfold order_syntax.greatest_def)
    1.26 +  have "greatest ?L (carrier G) (carrier ?L)"
    1.27 +    by (unfold greatest_def)
    1.28        (simp add: subgroup.subset subgroup_self)
    1.29 -  then show "\<exists>G. order_syntax.greatest ?car ?le G ?car" ..
    1.30 +  then show "\<exists>G. greatest ?L G (carrier ?L)" ..
    1.31  next
    1.32    fix A
    1.33 -  assume L: "A \<subseteq> ?car" and non_empty: "A ~= {}"
    1.34 +  assume L: "A \<subseteq> carrier ?L" and non_empty: "A ~= {}"
    1.35    then have Int_subgroup: "subgroup (\<Inter>A) G"
    1.36      by (fastsimp intro: subgroups_Inter)
    1.37 -  have "order_syntax.greatest ?car ?le (\<Inter>A) (order_syntax.Lower ?car ?le A)"
    1.38 -    (is "order_syntax.greatest _ _ ?Int _")
    1.39 -  proof (rule order_syntax.greatest_LowerI)
    1.40 +  have "greatest ?L (\<Inter>A) (Lower ?L A)"
    1.41 +    (is "greatest _ ?Int _")
    1.42 +  proof (rule greatest_LowerI)
    1.43      fix H
    1.44      assume H: "H \<in> A"
    1.45      with L have subgroupH: "subgroup H G" by auto
    1.46 @@ -755,18 +755,18 @@
    1.47      from groupH have monoidH: "monoid ?H"
    1.48        by (rule group.is_monoid)
    1.49      from H have Int_subset: "?Int \<subseteq> H" by fastsimp
    1.50 -    then show "?le ?Int H" by simp
    1.51 +    then show "le ?L ?Int H" by simp
    1.52    next
    1.53      fix H
    1.54 -    assume H: "H \<in> order_syntax.Lower ?car ?le A"
    1.55 -    with L Int_subgroup show "?le H ?Int"
    1.56 -      by (fastsimp simp: order_syntax.Lower_def intro: Inter_greatest)
    1.57 +    assume H: "H \<in> Lower ?L A"
    1.58 +    with L Int_subgroup show "le ?L H ?Int"
    1.59 +      by (fastsimp simp: Lower_def intro: Inter_greatest)
    1.60    next
    1.61 -    show "A \<subseteq> ?car" by (rule L)
    1.62 +    show "A \<subseteq> carrier ?L" by (rule L)
    1.63    next
    1.64 -    show "?Int \<in> ?car" by simp (rule Int_subgroup)
    1.65 +    show "?Int \<in> carrier ?L" by simp (rule Int_subgroup)
    1.66    qed
    1.67 -  then show "\<exists>I. order_syntax.greatest ?car ?le I (order_syntax.Lower ?car ?le A)" ..
    1.68 +  then show "\<exists>I. greatest ?L I (Lower ?L A)" ..
    1.69  qed
    1.70  
    1.71  end
     2.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jan 12 09:58:31 2007 +0100
     2.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Jan 12 15:37:21 2007 +0100
     2.3 @@ -96,54 +96,60 @@
     2.4  interpretation "domain" ["\<Z>"] by (rule int_is_domain)
     2.5  
     2.6  lemma int_le_total_order:
     2.7 -  "total_order (UNIV::int set) (op \<le>)"
     2.8 -apply (rule partial_order.total_orderI)
     2.9 - apply (rule partial_order.intro, simp+)
    2.10 -apply clarsimp
    2.11 -done
    2.12 +  "total_order (| carrier = UNIV::int set, le = op \<le> |)"
    2.13 +  apply (rule partial_order.total_orderI)
    2.14 +   apply (rule partial_order.intro, simp+)
    2.15 +  apply clarsimp
    2.16 +  done
    2.17  
    2.18  lemma less_int:
    2.19 -  "order_syntax.less (op \<le>::[int, int] => bool) = (op <)"
    2.20 -  by (auto simp add: expand_fun_eq order_syntax.less_def)
    2.21 +  "lless (| carrier = UNIV::int set, le = op \<le> |) = (op <)"
    2.22 +  by (auto simp add: expand_fun_eq lless_def)
    2.23  
    2.24  lemma join_int:
    2.25 -  "order_syntax.join (UNIV::int set) (op \<le>) = max"
    2.26 +  "join (| carrier = UNIV::int set, le = op \<le> |) = max"
    2.27    apply (simp add: expand_fun_eq max_def)
    2.28    apply (rule+)
    2.29    apply (rule lattice.joinI)
    2.30    apply (simp add: int_le_total_order total_order.axioms)
    2.31 -  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    2.32 +  apply (simp add: least_def Upper_def)
    2.33    apply arith
    2.34    apply simp apply simp
    2.35    apply (rule lattice.joinI)
    2.36    apply (simp add: int_le_total_order total_order.axioms)
    2.37 -  apply (simp add: order_syntax.least_def order_syntax.Upper_def)
    2.38 +  apply (simp add: least_def Upper_def)
    2.39    apply arith
    2.40    apply simp apply simp
    2.41    done
    2.42  
    2.43  lemma meet_int:
    2.44 -  "order_syntax.meet (UNIV::int set) (op \<le>) = min"
    2.45 +  "meet (| carrier = UNIV::int set, le = op \<le> |) = min"
    2.46    apply (simp add: expand_fun_eq min_def)
    2.47    apply (rule+)
    2.48    apply (rule lattice.meetI)
    2.49    apply (simp add: int_le_total_order total_order.axioms)
    2.50 -  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    2.51 +  apply (simp add: greatest_def Lower_def)
    2.52    apply arith
    2.53    apply simp apply simp
    2.54    apply (rule lattice.meetI)
    2.55    apply (simp add: int_le_total_order total_order.axioms)
    2.56 -  apply (simp add: order_syntax.greatest_def order_syntax.Lower_def)
    2.57 +  apply (simp add: greatest_def Lower_def)
    2.58    apply arith
    2.59    apply simp apply simp
    2.60    done
    2.61  
    2.62 -text {* Interpretation unfolding @{text less}, @{text join} and @{text
    2.63 +lemma carrier_int:
    2.64 +  "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    2.65 +  apply simp
    2.66 +  done
    2.67 +
    2.68 +text {* Interpretation unfolding @{text lless}, @{text join} and @{text
    2.69    meet} since they have natural representations in @{typ int}. *}
    2.70  
    2.71  interpretation 
    2.72 -  int [unfolded less_int join_int meet_int]:
    2.73 -  total_order ["UNIV::int set" "op \<le>"] by (rule int_le_total_order)
    2.74 +  int [unfolded less_int join_int meet_int carrier_int]:
    2.75 +  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    2.76 +  by (rule int_le_total_order)
    2.77  
    2.78  
    2.79  subsubsection {* Generated Ideals of @{text "\<Z>"} *}
     3.1 --- a/src/HOL/Algebra/Lattice.thy	Fri Jan 12 09:58:31 2007 +0100
     3.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Jan 12 15:37:21 2007 +0100
     3.3 @@ -18,163 +18,157 @@
     3.4  
     3.5  subsection {* Partial Orders *}
     3.6  
     3.7 -text {* Locale @{text order_syntax} is required since we want to refer
     3.8 -  to definitions (and their derived theorems) outside of @{text partial_order}.
     3.9 -  *}
    3.10 -
    3.11 -locale order_syntax =
    3.12 -  fixes L :: "'a set" and le :: "['a, 'a] => bool" (infix "\<sqsubseteq>" 50)
    3.13 -
    3.14 -text {* Note that the type constraints above are necessary, because the
    3.15 -  definition command cannot specialise the types. *}
    3.16 -
    3.17 -definition (in order_syntax)
    3.18 -  less (infixl "\<sqsubset>" 50) where "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    3.19 -
    3.20 -text {* Upper and lower bounds of a set. *}
    3.21 -
    3.22 -definition (in order_syntax)
    3.23 -  Upper :: "'a set => 'a set" where
    3.24 -  "Upper A == {u. (ALL x. x \<in> A \<inter> L --> x \<sqsubseteq> u)} \<inter> L"
    3.25 -
    3.26 -definition (in order_syntax)
    3.27 -  Lower :: "'a set => 'a set" where
    3.28 -  "Lower A == {l. (ALL x. x \<in> A \<inter> L --> l \<sqsubseteq> x)} \<inter> L"
    3.29 -
    3.30 -text {* Least and greatest, as predicate. *}
    3.31 +record 'a order = "'a partial_object" +
    3.32 +  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    3.33  
    3.34 -definition (in order_syntax)
    3.35 -  least :: "['a, 'a set] => bool" where
    3.36 -  "least l A == A \<subseteq> L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    3.37 -
    3.38 -definition (in order_syntax)
    3.39 -  greatest :: "['a, 'a set] => bool" where
    3.40 -  "greatest g A == A \<subseteq> L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    3.41 -
    3.42 -text {* Supremum and infimum *}
    3.43 -
    3.44 -definition (in order_syntax)
    3.45 -  sup :: "'a set => 'a" ("\<Squnion>_" [90] 90) where
    3.46 -  "\<Squnion>A == THE x. least x (Upper A)"
    3.47 -
    3.48 -definition (in order_syntax)
    3.49 -  inf :: "'a set => 'a" ("\<Sqinter>_" [90] 90) where
    3.50 -  "\<Sqinter>A == THE x. greatest x (Lower A)"
    3.51 -
    3.52 -definition (in order_syntax)
    3.53 -  join :: "['a, 'a] => 'a" (infixl "\<squnion>" 65) where
    3.54 -  "x \<squnion> y == sup {x, y}"
    3.55 -
    3.56 -definition (in order_syntax)
    3.57 -  meet :: "['a, 'a] => 'a" (infixl "\<sqinter>" 70) where
    3.58 -  "x \<sqinter> y == inf {x, y}"
    3.59 -
    3.60 -locale partial_order = order_syntax +
    3.61 +locale partial_order =
    3.62 +  fixes L (structure)
    3.63    assumes refl [intro, simp]:
    3.64 -                  "x \<in> L ==> x \<sqsubseteq> x"
    3.65 +                  "x \<in> carrier L ==> x \<sqsubseteq> x"
    3.66      and anti_sym [intro]:
    3.67 -                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> L; y \<in> L |] ==> x = y"
    3.68 +                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    3.69      and trans [trans]:
    3.70                    "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
    3.71 -                   x \<in> L; y \<in> L; z \<in> L |] ==> x \<sqsubseteq> z"
    3.72 +                   x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    3.73 +
    3.74 +constdefs (structure L)
    3.75 +  lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    3.76 +  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    3.77 +
    3.78 +  -- {* Upper and lower bounds of a set. *}
    3.79 +  Upper :: "[_, 'a set] => 'a set"
    3.80 +  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
    3.81 +                carrier L"
    3.82 +
    3.83 +  Lower :: "[_, 'a set] => 'a set"
    3.84 +  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
    3.85 +                carrier L"
    3.86 +
    3.87 +  -- {* Least and greatest, as predicate. *}
    3.88 +  least :: "[_, 'a, 'a set] => bool"
    3.89 +  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
    3.90 +
    3.91 +  greatest :: "[_, 'a, 'a set] => bool"
    3.92 +  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
    3.93 +
    3.94 +  -- {* Supremum and infimum *}
    3.95 +  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
    3.96 +  "\<Squnion>A == THE x. least L x (Upper L A)"
    3.97 +
    3.98 +  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
    3.99 +  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
   3.100 +
   3.101 +  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   3.102 +  "x \<squnion> y == sup L {x, y}"
   3.103 +
   3.104 +  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   3.105 +  "x \<sqinter> y == inf L {x, y}"
   3.106  
   3.107  
   3.108  subsubsection {* Upper *}
   3.109  
   3.110 -lemma (in order_syntax) Upper_closed [intro, simp]:
   3.111 -  "Upper A \<subseteq> L"
   3.112 +lemma Upper_closed [intro, simp]:
   3.113 +  "Upper L A \<subseteq> carrier L"
   3.114    by (unfold Upper_def) clarify
   3.115  
   3.116 -lemma (in order_syntax) UpperD [dest]:
   3.117 -  "[| u \<in> Upper A; x \<in> A; A \<subseteq> L |] ==> x \<sqsubseteq> u"
   3.118 +lemma UpperD [dest]:
   3.119 +  fixes L (structure)
   3.120 +  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   3.121    by (unfold Upper_def) blast
   3.122  
   3.123 -lemma (in order_syntax) Upper_memI:
   3.124 -  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> L |] ==> x \<in> Upper A"
   3.125 +lemma Upper_memI:
   3.126 +  fixes L (structure)
   3.127 +  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   3.128    by (unfold Upper_def) blast
   3.129  
   3.130 -lemma (in order_syntax) Upper_antimono:
   3.131 -  "A \<subseteq> B ==> Upper B \<subseteq> Upper A"
   3.132 +lemma Upper_antimono:
   3.133 +  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   3.134    by (unfold Upper_def) blast
   3.135  
   3.136  
   3.137  subsubsection {* Lower *}
   3.138  
   3.139 -lemma (in order_syntax) Lower_closed [intro, simp]:
   3.140 -  "Lower A \<subseteq> L"
   3.141 +lemma Lower_closed [intro, simp]:
   3.142 +  "Lower L A \<subseteq> carrier L"
   3.143    by (unfold Lower_def) clarify
   3.144  
   3.145 -lemma (in order_syntax) LowerD [dest]:
   3.146 -  "[| l \<in> Lower A; x \<in> A; A \<subseteq> L |] ==> l \<sqsubseteq> x"
   3.147 +lemma LowerD [dest]:
   3.148 +  fixes L (structure)
   3.149 +  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
   3.150    by (unfold Lower_def) blast
   3.151  
   3.152 -lemma (in order_syntax) Lower_memI:
   3.153 -  "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> L |] ==> x \<in> Lower A"
   3.154 +lemma Lower_memI:
   3.155 +  fixes L (structure)
   3.156 +  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   3.157    by (unfold Lower_def) blast
   3.158  
   3.159 -lemma (in order_syntax) Lower_antimono:
   3.160 -  "A \<subseteq> B ==> Lower B \<subseteq> Lower A"
   3.161 +lemma Lower_antimono:
   3.162 +  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   3.163    by (unfold Lower_def) blast
   3.164  
   3.165  
   3.166  subsubsection {* least *}
   3.167  
   3.168 -lemma (in order_syntax) least_closed [intro, simp]:
   3.169 -  "least l A ==> l \<in> L"
   3.170 +lemma least_carrier [intro, simp]:
   3.171 +  shows "least L l A ==> l \<in> carrier L"
   3.172    by (unfold least_def) fast
   3.173  
   3.174 -lemma (in order_syntax) least_mem:
   3.175 -  "least l A ==> l \<in> A"
   3.176 +lemma least_mem:
   3.177 +  "least L l A ==> l \<in> A"
   3.178    by (unfold least_def) fast
   3.179  
   3.180  lemma (in partial_order) least_unique:
   3.181 -  "[| least x A; least y A |] ==> x = y"
   3.182 +  "[| least L x A; least L y A |] ==> x = y"
   3.183    by (unfold least_def) blast
   3.184  
   3.185 -lemma (in order_syntax) least_le:
   3.186 -  "[| least x A; a \<in> A |] ==> x \<sqsubseteq> a"
   3.187 +lemma least_le:
   3.188 +  fixes L (structure)
   3.189 +  shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   3.190    by (unfold least_def) fast
   3.191  
   3.192 -lemma (in order_syntax) least_UpperI:
   3.193 +lemma least_UpperI:
   3.194 +  fixes L (structure)
   3.195    assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   3.196 -    and below: "!! y. y \<in> Upper A ==> s \<sqsubseteq> y"
   3.197 -    and L: "A \<subseteq> L"  "s \<in> L"
   3.198 -  shows "least s (Upper A)"
   3.199 +    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   3.200 +    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   3.201 +  shows "least L s (Upper L A)"
   3.202  proof -
   3.203 -  have "Upper A \<subseteq> L" by simp
   3.204 -  moreover from above L have "s \<in> Upper A" by (simp add: Upper_def)
   3.205 -  moreover from below have "ALL x : Upper A. s \<sqsubseteq> x" by fast
   3.206 +  have "Upper L A \<subseteq> carrier L" by simp
   3.207 +  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   3.208 +  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   3.209    ultimately show ?thesis by (simp add: least_def)
   3.210  qed
   3.211  
   3.212  
   3.213  subsubsection {* greatest *}
   3.214  
   3.215 -lemma (in order_syntax) greatest_closed [intro, simp]:
   3.216 -  "greatest l A ==> l \<in> L"
   3.217 +lemma greatest_carrier [intro, simp]:
   3.218 +  shows "greatest L l A ==> l \<in> carrier L"
   3.219    by (unfold greatest_def) fast
   3.220  
   3.221 -lemma (in order_syntax) greatest_mem:
   3.222 -  "greatest l A ==> l \<in> A"
   3.223 +lemma greatest_mem:
   3.224 +  "greatest L l A ==> l \<in> A"
   3.225    by (unfold greatest_def) fast
   3.226  
   3.227  lemma (in partial_order) greatest_unique:
   3.228 -  "[| greatest x A; greatest y A |] ==> x = y"
   3.229 +  "[| greatest L x A; greatest L y A |] ==> x = y"
   3.230    by (unfold greatest_def) blast
   3.231  
   3.232 -lemma (in order_syntax) greatest_le:
   3.233 -  "[| greatest x A; a \<in> A |] ==> a \<sqsubseteq> x"
   3.234 +lemma greatest_le:
   3.235 +  fixes L (structure)
   3.236 +  shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   3.237    by (unfold greatest_def) fast
   3.238  
   3.239 -lemma (in order_syntax) greatest_LowerI:
   3.240 +lemma greatest_LowerI:
   3.241 +  fixes L (structure)
   3.242    assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   3.243 -    and above: "!! y. y \<in> Lower A ==> y \<sqsubseteq> i"
   3.244 -    and L: "A \<subseteq> L"  "i \<in> L"
   3.245 -  shows "greatest i (Lower A)"
   3.246 +    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   3.247 +    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   3.248 +  shows "greatest L i (Lower L A)"
   3.249  proof -
   3.250 -  have "Lower A \<subseteq> L" by simp
   3.251 -  moreover from below L have "i \<in> Lower A" by (simp add: Lower_def)
   3.252 -  moreover from above have "ALL x : Lower A. x \<sqsubseteq> i" by fast
   3.253 +  have "Lower L A \<subseteq> carrier L" by simp
   3.254 +  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   3.255 +  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   3.256    ultimately show ?thesis by (simp add: greatest_def)
   3.257  qed
   3.258  
   3.259 @@ -183,61 +177,63 @@
   3.260  
   3.261  locale lattice = partial_order +
   3.262    assumes sup_of_two_exists:
   3.263 -    "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le {x, y})"
   3.264 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   3.265      and inf_of_two_exists:
   3.266 -    "[| x \<in> L; y \<in> L |] ==> EX s. order_syntax.greatest L le s (order_syntax.Lower L le {x, y})"
   3.267 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   3.268  
   3.269 -lemma (in order_syntax) least_Upper_above:
   3.270 -  "[| least s (Upper A); x \<in> A; A \<subseteq> L |] ==> x \<sqsubseteq> s"
   3.271 +lemma least_Upper_above:
   3.272 +  fixes L (structure)
   3.273 +  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   3.274    by (unfold least_def) blast
   3.275  
   3.276 -lemma (in order_syntax) greatest_Lower_above:
   3.277 -  "[| greatest i (Lower A); x \<in> A; A \<subseteq> L |] ==> i \<sqsubseteq> x"
   3.278 +lemma greatest_Lower_above:
   3.279 +  fixes L (structure)
   3.280 +  shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   3.281    by (unfold greatest_def) blast
   3.282  
   3.283  
   3.284  subsubsection {* Supremum *}
   3.285  
   3.286  lemma (in lattice) joinI:
   3.287 -  "[| !!l. least l (Upper {x, y}) ==> P l; x \<in> L; y \<in> L |]
   3.288 +  "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   3.289    ==> P (x \<squnion> y)"
   3.290  proof (unfold join_def sup_def)
   3.291 -  assume L: "x \<in> L"  "y \<in> L"
   3.292 -    and P: "!!l. least l (Upper {x, y}) ==> P l"
   3.293 -  with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast
   3.294 -  with L show "P (THE l. least l (Upper {x, y}))"
   3.295 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.296 +    and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   3.297 +  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   3.298 +  with L show "P (THE l. least L l (Upper L {x, y}))"
   3.299      by (fast intro: theI2 least_unique P)
   3.300  qed
   3.301  
   3.302  lemma (in lattice) join_closed [simp]:
   3.303 -  "[| x \<in> L; y \<in> L |] ==> x \<squnion> y \<in> L"
   3.304 -  by (rule joinI) (rule least_closed)
   3.305 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   3.306 +  by (rule joinI) (rule least_carrier)
   3.307  
   3.308 -lemma (in partial_order) sup_of_singletonI:     (* only reflexivity needed ? *)
   3.309 -  "x \<in> L ==> least x (Upper {x})"
   3.310 +lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   3.311 +  "x \<in> carrier L ==> least L x (Upper L {x})"
   3.312    by (rule least_UpperI) fast+
   3.313  
   3.314  lemma (in partial_order) sup_of_singleton [simp]:
   3.315 -  "x \<in> L ==> \<Squnion>{x} = x"
   3.316 +  "x \<in> carrier L ==> \<Squnion>{x} = x"
   3.317    by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   3.318  
   3.319  
   3.320  text {* Condition on @{text A}: supremum exists. *}
   3.321  
   3.322  lemma (in lattice) sup_insertI:
   3.323 -  "[| !!s. least s (Upper (insert x A)) ==> P s;
   3.324 -  least a (Upper A); x \<in> L; A \<subseteq> L |]
   3.325 +  "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   3.326 +  least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   3.327    ==> P (\<Squnion>(insert x A))"
   3.328  proof (unfold sup_def)
   3.329 -  assume L: "x \<in> L"  "A \<subseteq> L"
   3.330 -    and P: "!!l. least l (Upper (insert x A)) ==> P l"
   3.331 -    and least_a: "least a (Upper A)"
   3.332 -  from least_a have La: "a \<in> L" by simp
   3.333 +  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.334 +    and P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   3.335 +    and least_a: "least L a (Upper L A)"
   3.336 +  from L least_a have La: "a \<in> carrier L" by simp
   3.337    from L sup_of_two_exists least_a
   3.338 -  obtain s where least_s: "least s (Upper {a, x})" by blast
   3.339 -  show "P (THE l. least l (Upper (insert x A)))"
   3.340 +  obtain s where least_s: "least L s (Upper L {a, x})" by blast
   3.341 +  show "P (THE l. least L l (Upper L (insert x A)))"
   3.342    proof (rule theI2)
   3.343 -    show "least s (Upper (insert x A))"
   3.344 +    show "least L s (Upper L (insert x A))"
   3.345      proof (rule least_UpperI)
   3.346        fix z
   3.347        assume "z \<in> insert x A"
   3.348 @@ -252,15 +248,15 @@
   3.349        qed
   3.350      next
   3.351        fix y
   3.352 -      assume y: "y \<in> Upper (insert x A)"
   3.353 +      assume y: "y \<in> Upper L (insert x A)"
   3.354        show "s \<sqsubseteq> y"
   3.355        proof (rule least_le [OF least_s], rule Upper_memI)
   3.356  	fix z
   3.357  	assume z: "z \<in> {a, x}"
   3.358  	then show "z \<sqsubseteq> y"
   3.359  	proof
   3.360 -          have y': "y \<in> Upper A"
   3.361 -            apply (rule subsetD [where A = "Upper (insert x A)"])
   3.362 +          have y': "y \<in> Upper L A"
   3.363 +            apply (rule subsetD [where A = "Upper L (insert x A)"])
   3.364              apply (rule Upper_antimono) apply clarify apply assumption
   3.365              done
   3.366            assume "z = a"
   3.367 @@ -271,15 +267,15 @@
   3.368  	qed
   3.369        qed (rule Upper_closed [THEN subsetD])
   3.370      next
   3.371 -      from L show "insert x A \<subseteq> L" by simp
   3.372 -      from least_s show "s \<in> L" by simp
   3.373 +      from L show "insert x A \<subseteq> carrier L" by simp
   3.374 +      from least_s show "s \<in> carrier L" by simp
   3.375      qed
   3.376    next
   3.377      fix l
   3.378 -    assume least_l: "least l (Upper (insert x A))"
   3.379 +    assume least_l: "least L l (Upper L (insert x A))"
   3.380      show "l = s"
   3.381      proof (rule least_unique)
   3.382 -      show "least s (Upper (insert x A))"
   3.383 +      show "least L s (Upper L (insert x A))"
   3.384        proof (rule least_UpperI)
   3.385          fix z
   3.386          assume "z \<in> insert x A"
   3.387 @@ -294,15 +290,15 @@
   3.388  	qed
   3.389        next
   3.390          fix y
   3.391 -        assume y: "y \<in> Upper (insert x A)"
   3.392 +        assume y: "y \<in> Upper L (insert x A)"
   3.393          show "s \<sqsubseteq> y"
   3.394          proof (rule least_le [OF least_s], rule Upper_memI)
   3.395            fix z
   3.396            assume z: "z \<in> {a, x}"
   3.397            then show "z \<sqsubseteq> y"
   3.398            proof
   3.399 -            have y': "y \<in> Upper A"
   3.400 -	      apply (rule subsetD [where A = "Upper (insert x A)"])
   3.401 +            have y': "y \<in> Upper L A"
   3.402 +	      apply (rule subsetD [where A = "Upper L (insert x A)"])
   3.403  	      apply (rule Upper_antimono) apply clarify apply assumption
   3.404  	      done
   3.405              assume "z = a"
   3.406 @@ -313,15 +309,15 @@
   3.407            qed
   3.408          qed (rule Upper_closed [THEN subsetD])
   3.409        next
   3.410 -        from L show "insert x A \<subseteq> L" by simp
   3.411 -        from least_s show "s \<in> L" by simp
   3.412 +        from L show "insert x A \<subseteq> carrier L" by simp
   3.413 +        from least_s show "s \<in> carrier L" by simp
   3.414        qed
   3.415      qed
   3.416    qed
   3.417  qed
   3.418  
   3.419  lemma (in lattice) finite_sup_least:
   3.420 -  "[| finite A; A \<subseteq> L; A ~= {} |] ==> least (\<Squnion>A) (Upper A)"
   3.421 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   3.422  proof (induct set: Finites)
   3.423    case empty
   3.424    then show ?case by simp
   3.425 @@ -333,15 +329,15 @@
   3.426      with insert show ?thesis by (simp add: sup_of_singletonI)
   3.427    next
   3.428      case False
   3.429 -    with insert have "least (\<Squnion>A) (Upper A)" by simp
   3.430 +    with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   3.431      with _ show ?thesis
   3.432        by (rule sup_insertI) (simp_all add: insert [simplified])
   3.433    qed
   3.434  qed
   3.435  
   3.436  lemma (in lattice) finite_sup_insertI:
   3.437 -  assumes P: "!!l. least l (Upper (insert x A)) ==> P l"
   3.438 -    and xA: "finite A"  "x \<in> L"  "A \<subseteq> L"
   3.439 +  assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   3.440 +    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.441    shows "P (\<Squnion> (insert x A))"
   3.442  proof (cases "A = {}")
   3.443    case True with P and xA show ?thesis
   3.444 @@ -352,7 +348,7 @@
   3.445  qed
   3.446  
   3.447  lemma (in lattice) finite_sup_closed:
   3.448 -  "[| finite A; A \<subseteq> L; A ~= {} |] ==> \<Squnion>A \<in> L"
   3.449 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   3.450  proof (induct set: Finites)
   3.451    case empty then show ?case by simp
   3.452  next
   3.453 @@ -361,39 +357,39 @@
   3.454  qed
   3.455  
   3.456  lemma (in lattice) join_left:
   3.457 -  "[| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> x \<squnion> y"
   3.458 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   3.459    by (rule joinI [folded join_def]) (blast dest: least_mem)
   3.460  
   3.461  lemma (in lattice) join_right:
   3.462 -  "[| x \<in> L; y \<in> L |] ==> y \<sqsubseteq> x \<squnion> y"
   3.463 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   3.464    by (rule joinI [folded join_def]) (blast dest: least_mem)
   3.465  
   3.466  lemma (in lattice) sup_of_two_least:
   3.467 -  "[| x \<in> L; y \<in> L |] ==> least (\<Squnion>{x, y}) (Upper {x, y})"
   3.468 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   3.469  proof (unfold sup_def)
   3.470 -  assume L: "x \<in> L"  "y \<in> L"
   3.471 -  with sup_of_two_exists obtain s where "least s (Upper {x, y})" by fast
   3.472 -  with L show "least (THE xa. least xa (Upper {x, y})) (Upper {x, y})"
   3.473 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.474 +  with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   3.475 +  with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
   3.476    by (fast intro: theI2 least_unique)  (* blast fails *)
   3.477  qed
   3.478  
   3.479  lemma (in lattice) join_le:
   3.480    assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   3.481 -    and L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.482 +    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.483    shows "x \<squnion> y \<sqsubseteq> z"
   3.484  proof (rule joinI)
   3.485    fix s
   3.486 -  assume "least s (Upper {x, y})"
   3.487 +  assume "least L s (Upper L {x, y})"
   3.488    with sub L show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   3.489  qed
   3.490  
   3.491  lemma (in lattice) join_assoc_lemma:
   3.492 -  assumes L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.493 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.494    shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   3.495  proof (rule finite_sup_insertI)
   3.496    -- {* The textbook argument in Jacobson I, p 457 *}
   3.497    fix s
   3.498 -  assume sup: "least s (Upper {x, y, z})"
   3.499 +  assume sup: "least L s (Upper L {x, y, z})"
   3.500    show "x \<squnion> (y \<squnion> z) = s"
   3.501    proof (rule anti_sym)
   3.502      from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   3.503 @@ -402,15 +398,16 @@
   3.504      from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   3.505      by (erule_tac least_le)
   3.506        (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
   3.507 -  qed (simp_all add: L least_closed [OF sup])
   3.508 +  qed (simp_all add: L least_carrier [OF sup])
   3.509  qed (simp_all add: L)
   3.510  
   3.511 -lemma (in order_syntax) join_comm:
   3.512 -  "x \<squnion> y = y \<squnion> x"
   3.513 +lemma join_comm:
   3.514 +  fixes L (structure)
   3.515 +  shows "x \<squnion> y = y \<squnion> x"
   3.516    by (unfold join_def) (simp add: insert_commute)
   3.517  
   3.518  lemma (in lattice) join_assoc:
   3.519 -  assumes L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.520 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.521    shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   3.522  proof -
   3.523    have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   3.524 @@ -424,44 +421,45 @@
   3.525  subsubsection {* Infimum *}
   3.526  
   3.527  lemma (in lattice) meetI:
   3.528 -  "[| !!i. greatest i (Lower {x, y}) ==> P i; x \<in> L; y \<in> L |]
   3.529 +  "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   3.530 +  x \<in> carrier L; y \<in> carrier L |]
   3.531    ==> P (x \<sqinter> y)"
   3.532  proof (unfold meet_def inf_def)
   3.533 -  assume L: "x \<in> L"  "y \<in> L"
   3.534 -    and P: "!!g. greatest g (Lower {x, y}) ==> P g"
   3.535 -  with inf_of_two_exists obtain i where "greatest i (Lower {x, y})" by fast
   3.536 -  with L show "P (THE g. greatest g (Lower {x, y}))"
   3.537 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.538 +    and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   3.539 +  with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   3.540 +  with L show "P (THE g. greatest L g (Lower L {x, y}))"
   3.541    by (fast intro: theI2 greatest_unique P)
   3.542  qed
   3.543  
   3.544  lemma (in lattice) meet_closed [simp]:
   3.545 -  "[| x \<in> L; y \<in> L |] ==> x \<sqinter> y \<in> L"
   3.546 -  by (rule meetI) (rule greatest_closed)
   3.547 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   3.548 +  by (rule meetI) (rule greatest_carrier)
   3.549  
   3.550  lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   3.551 -  "x \<in> L ==> greatest x (Lower {x})"
   3.552 +  "x \<in> carrier L ==> greatest L x (Lower L {x})"
   3.553    by (rule greatest_LowerI) fast+
   3.554  
   3.555  lemma (in partial_order) inf_of_singleton [simp]:
   3.556 -  "x \<in> L ==> \<Sqinter> {x} = x"
   3.557 +  "x \<in> carrier L ==> \<Sqinter> {x} = x"
   3.558    by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   3.559  
   3.560  text {* Condition on A: infimum exists. *}
   3.561  
   3.562  lemma (in lattice) inf_insertI:
   3.563 -  "[| !!i. greatest i (Lower (insert x A)) ==> P i;
   3.564 -  greatest a (Lower A); x \<in> L; A \<subseteq> L |]
   3.565 +  "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   3.566 +  greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   3.567    ==> P (\<Sqinter>(insert x A))"
   3.568  proof (unfold inf_def)
   3.569 -  assume L: "x \<in> L"  "A \<subseteq> L"
   3.570 -    and P: "!!g. greatest g (Lower (insert x A)) ==> P g"
   3.571 -    and greatest_a: "greatest a (Lower A)"
   3.572 -  from greatest_a have La: "a \<in> L" by simp
   3.573 +  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.574 +    and P: "!!g. greatest L g (Lower L (insert x A)) ==> P g"
   3.575 +    and greatest_a: "greatest L a (Lower L A)"
   3.576 +  from L greatest_a have La: "a \<in> carrier L" by simp
   3.577    from L inf_of_two_exists greatest_a
   3.578 -  obtain i where greatest_i: "greatest i (Lower {a, x})" by blast
   3.579 -  show "P (THE g. greatest g (Lower (insert x A)))"
   3.580 +  obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   3.581 +  show "P (THE g. greatest L g (Lower L (insert x A)))"
   3.582    proof (rule theI2)
   3.583 -    show "greatest i (Lower (insert x A))"
   3.584 +    show "greatest L i (Lower L (insert x A))"
   3.585      proof (rule greatest_LowerI)
   3.586        fix z
   3.587        assume "z \<in> insert x A"
   3.588 @@ -476,15 +474,15 @@
   3.589        qed
   3.590      next
   3.591        fix y
   3.592 -      assume y: "y \<in> Lower (insert x A)"
   3.593 +      assume y: "y \<in> Lower L (insert x A)"
   3.594        show "y \<sqsubseteq> i"
   3.595        proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   3.596  	fix z
   3.597  	assume z: "z \<in> {a, x}"
   3.598  	then show "y \<sqsubseteq> z"
   3.599  	proof
   3.600 -          have y': "y \<in> Lower A"
   3.601 -            apply (rule subsetD [where A = "Lower (insert x A)"])
   3.602 +          have y': "y \<in> Lower L A"
   3.603 +            apply (rule subsetD [where A = "Lower L (insert x A)"])
   3.604              apply (rule Lower_antimono) apply clarify apply assumption
   3.605              done
   3.606            assume "z = a"
   3.607 @@ -495,15 +493,15 @@
   3.608  	qed
   3.609        qed (rule Lower_closed [THEN subsetD])
   3.610      next
   3.611 -      from L show "insert x A \<subseteq> L" by simp
   3.612 -      from greatest_i show "i \<in> L" by simp
   3.613 +      from L show "insert x A \<subseteq> carrier L" by simp
   3.614 +      from greatest_i show "i \<in> carrier L" by simp
   3.615      qed
   3.616    next
   3.617      fix g
   3.618 -    assume greatest_g: "greatest g (Lower (insert x A))"
   3.619 +    assume greatest_g: "greatest L g (Lower L (insert x A))"
   3.620      show "g = i"
   3.621      proof (rule greatest_unique)
   3.622 -      show "greatest i (Lower (insert x A))"
   3.623 +      show "greatest L i (Lower L (insert x A))"
   3.624        proof (rule greatest_LowerI)
   3.625          fix z
   3.626          assume "z \<in> insert x A"
   3.627 @@ -518,15 +516,15 @@
   3.628          qed
   3.629        next
   3.630          fix y
   3.631 -        assume y: "y \<in> Lower (insert x A)"
   3.632 +        assume y: "y \<in> Lower L (insert x A)"
   3.633          show "y \<sqsubseteq> i"
   3.634          proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   3.635            fix z
   3.636            assume z: "z \<in> {a, x}"
   3.637            then show "y \<sqsubseteq> z"
   3.638            proof
   3.639 -            have y': "y \<in> Lower A"
   3.640 -	      apply (rule subsetD [where A = "Lower (insert x A)"])
   3.641 +            have y': "y \<in> Lower L A"
   3.642 +	      apply (rule subsetD [where A = "Lower L (insert x A)"])
   3.643  	      apply (rule Lower_antimono) apply clarify apply assumption
   3.644  	      done
   3.645              assume "z = a"
   3.646 @@ -537,15 +535,15 @@
   3.647  	  qed
   3.648          qed (rule Lower_closed [THEN subsetD])
   3.649        next
   3.650 -        from L show "insert x A \<subseteq> L" by simp
   3.651 -        from greatest_i show "i \<in> L" by simp
   3.652 +        from L show "insert x A \<subseteq> carrier L" by simp
   3.653 +        from greatest_i show "i \<in> carrier L" by simp
   3.654        qed
   3.655      qed
   3.656    qed
   3.657  qed
   3.658  
   3.659  lemma (in lattice) finite_inf_greatest:
   3.660 -  "[| finite A; A \<subseteq> L; A ~= {} |] ==> greatest (\<Sqinter>A) (Lower A)"
   3.661 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   3.662  proof (induct set: Finites)
   3.663    case empty then show ?case by simp
   3.664  next
   3.665 @@ -558,14 +556,14 @@
   3.666      case False
   3.667      from insert show ?thesis
   3.668      proof (rule_tac inf_insertI)
   3.669 -      from False insert show "greatest (\<Sqinter>A) (Lower A)" by simp
   3.670 +      from False insert show "greatest L (\<Sqinter>A) (Lower L A)" by simp
   3.671      qed simp_all
   3.672    qed
   3.673  qed
   3.674  
   3.675  lemma (in lattice) finite_inf_insertI:
   3.676 -  assumes P: "!!i. greatest i (Lower (insert x A)) ==> P i"
   3.677 -    and xA: "finite A"  "x \<in> L"  "A \<subseteq> L"
   3.678 +  assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   3.679 +    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.680    shows "P (\<Sqinter> (insert x A))"
   3.681  proof (cases "A = {}")
   3.682    case True with P and xA show ?thesis
   3.683 @@ -576,7 +574,7 @@
   3.684  qed
   3.685  
   3.686  lemma (in lattice) finite_inf_closed:
   3.687 -  "[| finite A; A \<subseteq> L; A ~= {} |] ==> \<Sqinter>A \<in> L"
   3.688 +  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   3.689  proof (induct set: Finites)
   3.690    case empty then show ?case by simp
   3.691  next
   3.692 @@ -585,40 +583,41 @@
   3.693  qed
   3.694  
   3.695  lemma (in lattice) meet_left:
   3.696 -  "[| x \<in> L; y \<in> L |] ==> x \<sqinter> y \<sqsubseteq> x"
   3.697 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   3.698    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   3.699  
   3.700  lemma (in lattice) meet_right:
   3.701 -  "[| x \<in> L; y \<in> L |] ==> x \<sqinter> y \<sqsubseteq> y"
   3.702 +  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   3.703    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   3.704  
   3.705  lemma (in lattice) inf_of_two_greatest:
   3.706 -  "[| x \<in> L; y \<in> L |] ==> greatest (\<Sqinter> {x, y}) (Lower {x, y})"
   3.707 +  "[| x \<in> carrier L; y \<in> carrier L |] ==>
   3.708 +  greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   3.709  proof (unfold inf_def)
   3.710 -  assume L: "x \<in> L"  "y \<in> L"
   3.711 -  with inf_of_two_exists obtain s where "greatest s (Lower {x, y})" by fast
   3.712 +  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.713 +  with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   3.714    with L
   3.715 -  show "greatest (THE xa. greatest xa (Lower {x, y})) (Lower {x, y})"
   3.716 +  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
   3.717    by (fast intro: theI2 greatest_unique)  (* blast fails *)
   3.718  qed
   3.719  
   3.720  lemma (in lattice) meet_le:
   3.721    assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   3.722 -    and L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.723 +    and L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.724    shows "z \<sqsubseteq> x \<sqinter> y"
   3.725  proof (rule meetI)
   3.726    fix i
   3.727 -  assume "greatest i (Lower {x, y})"
   3.728 +  assume "greatest L i (Lower L {x, y})"
   3.729    with sub L show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
   3.730  qed
   3.731  
   3.732  lemma (in lattice) meet_assoc_lemma:
   3.733 -  assumes L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.734 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.735    shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
   3.736  proof (rule finite_inf_insertI)
   3.737    txt {* The textbook argument in Jacobson I, p 457 *}
   3.738    fix i
   3.739 -  assume inf: "greatest i (Lower {x, y, z})"
   3.740 +  assume inf: "greatest L i (Lower L {x, y, z})"
   3.741    show "x \<sqinter> (y \<sqinter> z) = i"
   3.742    proof (rule anti_sym)
   3.743      from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   3.744 @@ -627,15 +626,16 @@
   3.745      from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
   3.746      by (erule_tac greatest_le)
   3.747        (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
   3.748 -  qed (simp_all add: L greatest_closed [OF inf])
   3.749 +  qed (simp_all add: L greatest_carrier [OF inf])
   3.750  qed (simp_all add: L)
   3.751  
   3.752 -lemma (in order_syntax) meet_comm:
   3.753 -  "x \<sqinter> y = y \<sqinter> x"
   3.754 +lemma meet_comm:
   3.755 +  fixes L (structure)
   3.756 +  shows "x \<sqinter> y = y \<sqinter> x"
   3.757    by (unfold meet_def) (simp add: insert_commute)
   3.758  
   3.759  lemma (in lattice) meet_assoc:
   3.760 -  assumes L: "x \<in> L"  "y \<in> L"  "z \<in> L"
   3.761 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.762    shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
   3.763  proof -
   3.764    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
   3.765 @@ -649,52 +649,51 @@
   3.766  subsection {* Total Orders *}
   3.767  
   3.768  locale total_order = lattice +
   3.769 -  assumes total: "[| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.770 -
   3.771 +  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.772  
   3.773  text {* Introduction rule: the usual definition of total order *}
   3.774  
   3.775  lemma (in partial_order) total_orderI:
   3.776 -  assumes total: "!!x y. [| x \<in> L; y \<in> L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.777 -  shows "total_order L le"
   3.778 +  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.779 +  shows "total_order L"
   3.780  proof intro_locales
   3.781 -  show "lattice_axioms L le"
   3.782 +  show "lattice_axioms L"
   3.783    proof (rule lattice_axioms.intro)
   3.784      fix x y
   3.785 -    assume L: "x \<in> L"  "y \<in> L"
   3.786 -    show "EX s. least s (Upper {x, y})"
   3.787 +    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.788 +    show "EX s. least L s (Upper L {x, y})"
   3.789      proof -
   3.790        note total L
   3.791        moreover
   3.792        {
   3.793          assume "x \<sqsubseteq> y"
   3.794 -        with L have "least y (Upper {x, y})"
   3.795 +        with L have "least L y (Upper L {x, y})"
   3.796            by (rule_tac least_UpperI) auto
   3.797        }
   3.798        moreover
   3.799        {
   3.800          assume "y \<sqsubseteq> x"
   3.801 -        with L have "least x (Upper {x, y})"
   3.802 +        with L have "least L x (Upper L {x, y})"
   3.803            by (rule_tac least_UpperI) auto
   3.804        }
   3.805        ultimately show ?thesis by blast
   3.806      qed
   3.807    next
   3.808      fix x y
   3.809 -    assume L: "x \<in> L"  "y \<in> L"
   3.810 -    show "EX i. greatest i (Lower {x, y})"
   3.811 +    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.812 +    show "EX i. greatest L i (Lower L {x, y})"
   3.813      proof -
   3.814        note total L
   3.815        moreover
   3.816        {
   3.817          assume "y \<sqsubseteq> x"
   3.818 -        with L have "greatest y (Lower {x, y})"
   3.819 +        with L have "greatest L y (Lower L {x, y})"
   3.820            by (rule_tac greatest_LowerI) auto
   3.821        }
   3.822        moreover
   3.823        {
   3.824          assume "x \<sqsubseteq> y"
   3.825 -        with L have "greatest x (Lower {x, y})"
   3.826 +        with L have "greatest L x (Lower L {x, y})"
   3.827            by (rule_tac greatest_LowerI) auto
   3.828        }
   3.829        ultimately show ?thesis by blast
   3.830 @@ -707,98 +706,97 @@
   3.831  
   3.832  locale complete_lattice = lattice +
   3.833    assumes sup_exists:
   3.834 -    "[| A \<subseteq> L |] ==> EX s. order_syntax.least L le s (order_syntax.Upper L le A)"
   3.835 +    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   3.836      and inf_exists:
   3.837 -    "[| A \<subseteq> L |] ==> EX i. order_syntax.greatest L le i (order_syntax.Lower L le A)"
   3.838 +    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   3.839  
   3.840  text {* Introduction rule: the usual definition of complete lattice *}
   3.841  
   3.842  lemma (in partial_order) complete_latticeI:
   3.843    assumes sup_exists:
   3.844 -    "!!A. [| A \<subseteq> L |] ==> EX s. least s (Upper A)"
   3.845 +    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
   3.846      and inf_exists:
   3.847 -    "!!A. [| A \<subseteq> L |] ==> EX i. greatest i (Lower A)"
   3.848 -  shows "complete_lattice L le"
   3.849 +    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
   3.850 +  shows "complete_lattice L"
   3.851  proof intro_locales
   3.852 -  show "lattice_axioms L le"
   3.853 +  show "lattice_axioms L"
   3.854      by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
   3.855  qed (assumption | rule complete_lattice_axioms.intro)+
   3.856  
   3.857 -definition (in order_syntax)
   3.858 -  top ("\<top>") where
   3.859 -  "\<top> == sup L"
   3.860 +constdefs (structure L)
   3.861 +  top :: "_ => 'a" ("\<top>\<index>")
   3.862 +  "\<top> == sup L (carrier L)"
   3.863  
   3.864 -definition (in order_syntax)
   3.865 -  bottom ("\<bottom>") where
   3.866 -  "\<bottom> == inf L"
   3.867 +  bottom :: "_ => 'a" ("\<bottom>\<index>")
   3.868 +  "\<bottom> == inf L (carrier L)"
   3.869  
   3.870  
   3.871  lemma (in complete_lattice) supI:
   3.872 -  "[| !!l. least l (Upper A) ==> P l; A \<subseteq> L |]
   3.873 +  "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   3.874    ==> P (\<Squnion>A)"
   3.875  proof (unfold sup_def)
   3.876 -  assume L: "A \<subseteq> L"
   3.877 -    and P: "!!l. least l (Upper A) ==> P l"
   3.878 -  with sup_exists obtain s where "least s (Upper A)" by blast
   3.879 -  with L show "P (THE l. least l (Upper A))"
   3.880 +  assume L: "A \<subseteq> carrier L"
   3.881 +    and P: "!!l. least L l (Upper L A) ==> P l"
   3.882 +  with sup_exists obtain s where "least L s (Upper L A)" by blast
   3.883 +  with L show "P (THE l. least L l (Upper L A))"
   3.884    by (fast intro: theI2 least_unique P)
   3.885  qed
   3.886  
   3.887  lemma (in complete_lattice) sup_closed [simp]:
   3.888 -  "A \<subseteq> L ==> \<Squnion>A \<in> L"
   3.889 +  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   3.890    by (rule supI) simp_all
   3.891  
   3.892  lemma (in complete_lattice) top_closed [simp, intro]:
   3.893 -  "\<top> \<in> L"
   3.894 +  "\<top> \<in> carrier L"
   3.895    by (unfold top_def) simp
   3.896  
   3.897  lemma (in complete_lattice) infI:
   3.898 -  "[| !!i. greatest i (Lower A) ==> P i; A \<subseteq> L |]
   3.899 +  "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   3.900    ==> P (\<Sqinter>A)"
   3.901  proof (unfold inf_def)
   3.902 -  assume L: "A \<subseteq> L"
   3.903 -    and P: "!!l. greatest l (Lower A) ==> P l"
   3.904 -  with inf_exists obtain s where "greatest s (Lower A)" by blast
   3.905 -  with L show "P (THE l. greatest l (Lower A))"
   3.906 +  assume L: "A \<subseteq> carrier L"
   3.907 +    and P: "!!l. greatest L l (Lower L A) ==> P l"
   3.908 +  with inf_exists obtain s where "greatest L s (Lower L A)" by blast
   3.909 +  with L show "P (THE l. greatest L l (Lower L A))"
   3.910    by (fast intro: theI2 greatest_unique P)
   3.911  qed
   3.912  
   3.913  lemma (in complete_lattice) inf_closed [simp]:
   3.914 -  "A \<subseteq> L ==> \<Sqinter>A \<in> L"
   3.915 +  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   3.916    by (rule infI) simp_all
   3.917  
   3.918  lemma (in complete_lattice) bottom_closed [simp, intro]:
   3.919 -  "\<bottom> \<in> L"
   3.920 +  "\<bottom> \<in> carrier L"
   3.921    by (unfold bottom_def) simp
   3.922  
   3.923  text {* Jacobson: Theorem 8.1 *}
   3.924  
   3.925 -lemma (in order_syntax) Lower_empty [simp]:
   3.926 -  "Lower {} = L"
   3.927 +lemma Lower_empty [simp]:
   3.928 +  "Lower L {} = carrier L"
   3.929    by (unfold Lower_def) simp
   3.930  
   3.931 -lemma (in order_syntax) Upper_empty [simp]:
   3.932 -  "Upper {} = L"
   3.933 +lemma Upper_empty [simp]:
   3.934 +  "Upper L {} = carrier L"
   3.935    by (unfold Upper_def) simp
   3.936  
   3.937  theorem (in partial_order) complete_lattice_criterion1:
   3.938 -  assumes top_exists: "EX g. greatest g L"
   3.939 +  assumes top_exists: "EX g. greatest L g (carrier L)"
   3.940      and inf_exists:
   3.941 -      "!!A. [| A \<subseteq> L; A ~= {} |] ==> EX i. greatest i (Lower A)"
   3.942 -  shows "complete_lattice L le"
   3.943 +      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
   3.944 +  shows "complete_lattice L"
   3.945  proof (rule complete_latticeI)
   3.946 -  from top_exists obtain top where top: "greatest top L" ..
   3.947 +  from top_exists obtain top where top: "greatest L top (carrier L)" ..
   3.948    fix A
   3.949 -  assume L: "A \<subseteq> L"
   3.950 -  let ?B = "Upper A"
   3.951 +  assume L: "A \<subseteq> carrier L"
   3.952 +  let ?B = "Upper L A"
   3.953    from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
   3.954    then have B_non_empty: "?B ~= {}" by fast
   3.955 -  have B_L: "?B \<subseteq> L" by simp
   3.956 +  have B_L: "?B \<subseteq> carrier L" by simp
   3.957    from inf_exists [OF B_L B_non_empty]
   3.958 -  obtain b where b_inf_B: "greatest b (Lower ?B)" ..
   3.959 -  have "least b (Upper A)"
   3.960 +  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
   3.961 +  have "least L b (Upper L A)"
   3.962  apply (rule least_UpperI)
   3.963 -   apply (rule greatest_le [where A = "Lower ?B"])
   3.964 +   apply (rule greatest_le [where A = "Lower L ?B"])
   3.965      apply (rule b_inf_B)
   3.966     apply (rule Lower_memI)
   3.967      apply (erule UpperD)
   3.968 @@ -808,13 +806,13 @@
   3.969    apply (erule greatest_Lower_above [OF b_inf_B])
   3.970    apply simp
   3.971   apply (rule L)
   3.972 -apply (rule greatest_closed [OF b_inf_B]) (* rename rule: _closed *)
   3.973 +apply (rule greatest_carrier [OF b_inf_B]) (* rename rule: _closed *)
   3.974  done
   3.975 -  then show "EX s. least s (Upper A)" ..
   3.976 +  then show "EX s. least L s (Upper L A)" ..
   3.977  next
   3.978    fix A
   3.979 -  assume L: "A \<subseteq> L"
   3.980 -  show "EX i. greatest i (Lower A)"
   3.981 +  assume L: "A \<subseteq> carrier L"
   3.982 +  show "EX i. greatest L i (Lower L A)"
   3.983    proof (cases "A = {}")
   3.984      case True then show ?thesis
   3.985        by (simp add: top_exists)
   3.986 @@ -832,25 +830,25 @@
   3.987  subsubsection {* Powerset of a Set is a Complete Lattice *}
   3.988  
   3.989  theorem powerset_is_complete_lattice:
   3.990 -  "complete_lattice (Pow A) (op \<subseteq>)"
   3.991 -  (is "complete_lattice ?L ?le")
   3.992 +  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
   3.993 +  (is "complete_lattice ?L")
   3.994  proof (rule partial_order.complete_latticeI)
   3.995 -  show "partial_order ?L ?le"
   3.996 +  show "partial_order ?L"
   3.997      by (rule partial_order.intro) auto
   3.998  next
   3.999    fix B
  3.1000 -  assume "B \<subseteq> ?L"
  3.1001 -  then have "order_syntax.least ?L ?le (\<Union> B) (order_syntax.Upper ?L ?le B)"
  3.1002 -    by (fastsimp intro!: order_syntax.least_UpperI simp: order_syntax.Upper_def)
  3.1003 -  then show "EX s. order_syntax.least ?L ?le s (order_syntax.Upper ?L ?le B)" ..
  3.1004 +  assume "B \<subseteq> carrier ?L"
  3.1005 +  then have "least ?L (\<Union> B) (Upper ?L B)"
  3.1006 +    by (fastsimp intro!: least_UpperI simp: Upper_def)
  3.1007 +  then show "EX s. least ?L s (Upper ?L B)" ..
  3.1008  next
  3.1009    fix B
  3.1010 -  assume "B \<subseteq> ?L"
  3.1011 -  then have "order_syntax.greatest ?L ?le (\<Inter> B \<inter> A) (order_syntax.Lower ?L ?le B)"
  3.1012 +  assume "B \<subseteq> carrier ?L"
  3.1013 +  then have "greatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
  3.1014      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
  3.1015        @{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
  3.1016 -    by (fastsimp intro!: order_syntax.greatest_LowerI simp: order_syntax.Lower_def)
  3.1017 -  then show "EX i. order_syntax.greatest ?L ?le i (order_syntax.Lower ?L ?le B)" ..
  3.1018 +    by (fastsimp intro!: greatest_LowerI simp: Lower_def)
  3.1019 +  then show "EX i. greatest ?L i (Lower ?L B)" ..
  3.1020  qed
  3.1021  
  3.1022  text {* An other example, that of the lattice of subgroups of a group,