author ballarin Fri Jan 12 15:37:21 2007 +0100 (2007-01-12) changeset 22063 717425609192 parent 22062 f4cfc4101c8f child 22064 3d716cc9bd7a
Reverted to structure representation with records.
 src/HOL/Algebra/Group.thy file | annotate | diff | revisions src/HOL/Algebra/IntRing.thy file | annotate | diff | revisions src/HOL/Algebra/Lattice.thy file | annotate | diff | revisions
     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.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.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.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.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,