# HG changeset patch
# User ballarin
# Date 1217437413 -7200
# Node ID 95b36bfe7fc484d21d6185309341667559d664aa
# Parent  007a339b9e7d19c86e547cbfea50d12d8288afca
New locales for orders and lattices where the equivalence relation is not restricted to equality.

diff -r 007a339b9e7d -r 95b36bfe7fc4 NEWS
--- a/NEWS	Wed Jul 30 16:07:00 2008 +0200
+++ b/NEWS	Wed Jul 30 19:03:33 2008 +0200
@@ -125,6 +125,13 @@
 
 *** HOL-Algebra ***
 
+* New locales for orders and lattices where the equivalence relation
+  is not restricted to equality.  INCOMPATIBILITY: all order and
+  lattice locales use a record structure with field eq for the
+  equivalence.
+
+* New theory of factorial domains.
+
 * Units_l_inv and Units_r_inv are now simprules by default.
 INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
 and/or r_inv will now also require deletion of these lemmas.
@@ -136,8 +143,6 @@
 greatest_carrier ~> greatest_closed
 greatest_Lower_above ~> greatest_Lower_below
 
-* New theory of factorial domains.
-
 
 *** HOL-NSA ***
 
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/Divisibility.thy
--- a/src/HOL/Algebra/Divisibility.thy	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/Algebra/Divisibility.thy	Wed Jul 30 19:03:33 2008 +0200
@@ -2,11 +2,12 @@
   Title:     Divisibility in monoids and rings
   Id:        $Id$
   Author:    Clemens Ballarin, started 18 July 2008
-  Copyright: Clemens Ballarin
+
+Based on work by Stefan Hohe.
 *)
 
 theory Divisibility
-imports Permutation Coset Group GLattice
+imports Permutation Coset Group
 begin
 
 subsection {* Monoid with cancelation law *}
@@ -490,8 +491,8 @@
        show "x divides y'" by simp
 qed
 
-lemma (in monoid) division_gpartial_order [simp, intro!]:
-  "gpartial_order (division_rel G)"
+lemma (in monoid) division_weak_partial_order [simp, intro!]:
+  "weak_partial_order (division_rel G)"
   apply unfold_locales
   apply simp_all
   apply (simp add: associated_sym)
@@ -731,12 +732,12 @@
  apply (iprover intro: divides_trans)+
 done
 
-lemma properfactor_glless:
+lemma properfactor_lless:
   fixes G (structure)
-  shows "properfactor G = glless (division_rel G)"
+  shows "properfactor G = lless (division_rel G)"
 apply (rule ext) apply (rule ext) apply rule
- apply (fastsimp elim: properfactorE2 intro: gllessI)
-apply (fastsimp elim: gllessE intro: properfactorI2)
+ apply (fastsimp elim: properfactorE2 intro: weak_llessI)
+apply (fastsimp elim: weak_llessE intro: properfactorI2)
 done
 
 lemma (in monoid) properfactor_cong_l [trans]:
@@ -745,9 +746,9 @@
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "properfactor G x' y"
 using pf
-unfolding properfactor_glless
+unfolding properfactor_lless
 proof -
-  interpret gpartial_order ["division_rel G"] ..
+  interpret weak_partial_order ["division_rel G"] ..
   from x'x
        have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
   also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
@@ -761,9 +762,9 @@
     and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
   shows "properfactor G x y'"
 using pf
-unfolding properfactor_glless
+unfolding properfactor_lless
 proof -
-  interpret gpartial_order ["division_rel G"] ..
+  interpret weak_partial_order ["division_rel G"] ..
   assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
   also from yy'
        have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
@@ -2630,7 +2631,7 @@
   "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
 
 constdefs (structure G)
-  "SomeGcd G A == ginf (division_rel G) A"
+  "SomeGcd G A == inf (division_rel G) A"
 
 
 locale gcd_condition_monoid = comm_monoid_cancel +
@@ -2648,12 +2649,12 @@
 
 subsubsection {* Connections to \texttt{Lattice.thy} *}
 
-lemma gcdof_ggreatestLower:
+lemma gcdof_greatestLower:
   fixes G (structure)
   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(x \<in> carrier G \<and> x gcdof a b) =
-         ggreatest (division_rel G) x (Lower (division_rel G) {a, b})"
-unfolding isgcd_def ggreatest_def Lower_def elem_def
+         greatest (division_rel G) x (Lower (division_rel G) {a, b})"
+unfolding isgcd_def greatest_def Lower_def elem_def
 proof (simp, safe)
   fix xa
   assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
@@ -2674,12 +2675,12 @@
        by (fast intro: r1)
 qed (simp, simp)
 
-lemma lcmof_gleastUpper:
+lemma lcmof_leastUpper:
   fixes G (structure)
   assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(x \<in> carrier G \<and> x lcmof a b) =
-         gleast (division_rel G) x (Upper (division_rel G) {a, b})"
-unfolding islcm_def gleast_def Upper_def elem_def
+         least (division_rel G) x (Upper (division_rel G) {a, b})"
+unfolding islcm_def least_def Upper_def elem_def
 proof (simp, safe)
   fix xa
   assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
@@ -2700,12 +2701,12 @@
        by (fast intro: r1)
 qed (simp, simp)
 
-lemma somegcd_gmeet:
+lemma somegcd_meet:
   fixes G (structure)
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
-  shows "somegcd G a b = gmeet (division_rel G) a b"
-unfolding somegcd_def gmeet_def ginf_def
-by (simp add: gcdof_ggreatestLower[OF carr])
+  shows "somegcd G a b = meet (division_rel G) a b"
+unfolding somegcd_def meet_def inf_def
+by (simp add: gcdof_greatestLower[OF carr])
 
 lemma (in monoid) isgcd_divides_l:
   assumes "a divides b"
@@ -2910,10 +2911,10 @@
 
 subsubsection {* Gcd condition *}
 
-lemma (in gcd_condition_monoid) division_glower_semilattice [simp]:
-  shows "glower_semilattice (division_rel G)"
+lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
+  shows "weak_lower_semilattice (division_rel G)"
 proof -
-  interpret gpartial_order ["division_rel G"] ..
+  interpret weak_partial_order ["division_rel G"] ..
   show ?thesis
   apply (unfold_locales, simp_all)
   proof -
@@ -2925,9 +2926,9 @@
         and isgcd: "z gcdof x y"
         by auto
     with carr
-    have "ggreatest (division_rel G) z (Lower (division_rel G) {x, y})"
-        by (subst gcdof_ggreatestLower[symmetric], simp+)
-    thus "\<exists>z. ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
+    have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
+        by (subst gcdof_greatestLower[symmetric], simp+)
+    thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
   qed
 qed
 
@@ -2938,15 +2939,15 @@
   shows "a' gcdof b c"
 proof -
   note carr = a'carr carr'
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   have "a' \<in> carrier G \<and> a' gcdof b c"
-    apply (simp add: gcdof_ggreatestLower carr')
-    apply (subst ggreatest_Lower_cong_l[of _ a])
+    apply (simp add: gcdof_greatestLower carr')
+    apply (subst greatest_Lower_cong_l[of _ a])
        apply (simp add: a'a)
       apply (simp add: carr)
      apply (simp add: carr)
     apply (simp add: carr)
-    apply (simp add: gcdof_ggreatestLower[symmetric] agcd carr)
+    apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
   done
   thus ?thesis ..
 qed
@@ -2955,10 +2956,10 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "somegcd G a b \<in> carrier G"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet[OF carr])
-    apply (rule gmeet_closed[simplified], fact+)
+    apply (simp add: somegcd_meet[OF carr])
+    apply (rule meet_closed[simplified], fact+)
   done
 qed
 
@@ -2966,12 +2967,12 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) gcdof a b"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   from carr
   have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
-    apply (subst gcdof_ggreatestLower, simp, simp)
-    apply (simp add: somegcd_gmeet[OF carr] gmeet_def)
-    apply (rule ginf_of_two_ggreatest[simplified], assumption+)
+    apply (subst gcdof_greatestLower, simp, simp)
+    apply (simp add: somegcd_meet[OF carr] meet_def)
+    apply (rule inf_of_two_greatest[simplified], assumption+)
   done
   thus "(somegcd G a b) gcdof a b" by simp
 qed
@@ -2980,10 +2981,10 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "\<exists>x\<in>carrier G. x = somegcd G a b"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet[OF carr])
-    apply (rule gmeet_closed[simplified], fact+)
+    apply (simp add: somegcd_meet[OF carr])
+    apply (rule meet_closed[simplified], fact+)
   done
 qed
 
@@ -2991,10 +2992,10 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides a"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet[OF carr])
-    apply (rule gmeet_left[simplified], fact+)
+    apply (simp add: somegcd_meet[OF carr])
+    apply (rule meet_left[simplified], fact+)
   done
 qed
 
@@ -3002,10 +3003,10 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   shows "(somegcd G a b) divides b"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet[OF carr])
-    apply (rule gmeet_right[simplified], fact+)
+    apply (simp add: somegcd_meet[OF carr])
+    apply (rule meet_right[simplified], fact+)
   done
 qed
 
@@ -3014,10 +3015,10 @@
     and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   shows "z divides (somegcd G x y)"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet L)
-    apply (rule gmeet_le[simplified], fact+)
+    apply (simp add: somegcd_meet L)
+    apply (rule meet_le[simplified], fact+)
   done
 qed
 
@@ -3026,10 +3027,10 @@
     and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   shows "somegcd G x y \<sim> somegcd G x' y"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet carr)
-    apply (rule gmeet_cong_l[simplified], fact+)
+    apply (simp add: somegcd_meet carr)
+    apply (rule meet_cong_l[simplified], fact+)
   done
 qed
 
@@ -3038,10 +3039,10 @@
     and yy': "y \<sim> y'"
   shows "somegcd G x y \<sim> somegcd G x y'"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (simp add: somegcd_gmeet carr)
-    apply (rule gmeet_cong_r[simplified], fact+)
+    apply (simp add: somegcd_meet carr)
+    apply (rule meet_cong_r[simplified], fact+)
   done
 qed
 
@@ -3089,10 +3090,10 @@
   assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
     apply (simp add: SomeGcd_def)
-    apply (rule finite_ginf_closed[simplified], fact+)
+    apply (rule finite_inf_closed[simplified], fact+)
   done
 qed
 
@@ -3100,11 +3101,11 @@
   assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
+  interpret weak_lower_semilattice ["division_rel G"] by simp
   show ?thesis
-    apply (subst (2 3) somegcd_gmeet, (simp add: carr)+)
-    apply (simp add: somegcd_gmeet carr)
-    apply (rule gmeet_assoc[simplified], fact+)
+    apply (subst (2 3) somegcd_meet, (simp add: carr)+)
+    apply (simp add: somegcd_meet carr)
+    apply (rule weak_meet_assoc[simplified], fact+)
   done
 qed
 
@@ -3866,12 +3867,12 @@
 interpretation factorial_monoid \<subseteq> gcd_condition_monoid
   by (unfold_locales, rule gcdof_exists)
 
-lemma (in factorial_monoid) division_glattice [simp]:
-  shows "glattice (division_rel G)"
+lemma (in factorial_monoid) division_weak_lattice [simp]:
+  shows "weak_lattice (division_rel G)"
 proof -
-  interpret glower_semilattice ["division_rel G"] by simp
-
-  show "glattice (division_rel G)"
+  interpret weak_lower_semilattice ["division_rel G"] by simp
+
+  show "weak_lattice (division_rel G)"
   apply (unfold_locales, simp_all)
   proof -
     fix x y
@@ -3883,9 +3884,9 @@
         and isgcd: "z lcmof x y"
         by auto
     with carr
-    have "gleast (division_rel G) z (Upper (division_rel G) {x, y})"
-        by (simp add: lcmof_gleastUpper[symmetric])
-    thus "\<exists>z. gleast (division_rel G) z (Upper (division_rel G) {x, y})" by fast
+    have "least (division_rel G) z (Upper (division_rel G) {x, y})"
+        by (simp add: lcmof_leastUpper[symmetric])
+    thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast
   qed
 qed
 
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/GLattice.thy
--- a/src/HOL/Algebra/GLattice.thy	Wed Jul 30 16:07:00 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,1181 +0,0 @@
-(*
-  Title:     HOL/Algebra/Lattice.thy
-  Id:        $Id$
-  Author:    Clemens Ballarin, started 7 November 2003
-  Copyright: Clemens Ballarin
-*)
-
-theory GLattice imports Congruence begin
-
-(* FIXME: unify with Lattice.thy *)
-
-
-section {* Orders and Lattices *}
-
-subsection {* Partial Orders *}
-
-record 'a gorder = "'a eq_object" +
-  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
-
-locale gpartial_order = equivalence L +
-  assumes le_refl [intro, simp]:
-      "x \<in> carrier L ==> x \<sqsubseteq> x"
-    and le_anti_sym [intro]:
-      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
-    and le_trans [trans]:
-      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
-    and le_cong:
-      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
-
-constdefs (structure L)
-  glless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
-
-
-subsubsection {* The order relation *}
-
-context gpartial_order begin
-
-lemma le_cong_l [intro, trans]:
-  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-  by (auto intro: le_cong [THEN iffD2])
-
-lemma le_cong_r [intro, trans]:
-  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
-  by (auto intro: le_cong [THEN iffD1])
-
-lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
-  by (simp add: le_cong_l)
-
-end
-
-lemma gllessI:
-  fixes R (structure)
-  assumes "x \<sqsubseteq> y" and "~(x .= y)"
-  shows "x \<sqsubset> y"
-  using assms
-  unfolding glless_def
-  by simp
-
-lemma gllessD1:
-  fixes R (structure)
-  assumes "x \<sqsubset> y"
-  shows "x \<sqsubseteq> y"
-  using assms
-  unfolding glless_def
-  by simp
-
-lemma gllessD2:
-  fixes R (structure)
-  assumes "x \<sqsubset> y"
-  shows "\<not> (x .= y)"
-  using assms
-  unfolding glless_def
-  by simp
-
-lemma gllessE:
-  fixes R (structure)
-  assumes p: "x \<sqsubset> y"
-    and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
-  shows "P"
-  using p
-  by (blast dest: gllessD1 gllessD2 e)
-
-(*
-lemma (in gpartial_order) lless_cong_l [trans]:
-  assumes xx': "x \<doteq> x'"
-    and xy: "x' \<sqsubset> y"
-    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
-  shows "x \<sqsubseteq> y"
-using xy
-unfolding lless_def
-proof clarify
-  note xx'
-  also assume "x' \<sqsubseteq> y"
-  finally show "x \<sqsubseteq> y" by (simp add: carr)
-qed
-*)
-
-lemma (in gpartial_order) glless_cong_l [trans]:
-  assumes xx': "x .= x'"
-    and xy: "x' \<sqsubset> y"
-    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
-  shows "x \<sqsubset> y"
-  using assms
-  apply (elim gllessE, intro gllessI)
-  apply (iprover intro: le_cong_l)
-  apply (iprover intro: trans sym)
-  done
-
-(*
-lemma (in gpartial_order) lless_cong_r:
-  assumes xy: "x \<sqsubset> y"
-    and  yy': "y \<doteq> y'"
-    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
-  shows "x \<sqsubseteq> y'"
-using xy
-unfolding lless_def
-proof clarify
-  assume "x \<sqsubseteq> y"
-  also note yy'
-  finally show "x \<sqsubseteq> y'" by (simp add: carr)
-qed
-*)
-
-lemma (in gpartial_order) glless_cong_r [trans]:
-  assumes xy: "x \<sqsubset> y"
-    and  yy': "y .= y'"
-    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
-  shows "x \<sqsubset> y'"
-  using assms
-  apply (elim gllessE, intro gllessI)
-  apply (iprover intro: le_cong_r)
-  apply (iprover intro: trans sym)
-  done
-
-(*
-lemma (in gpartial_order) glless_antisym:
-  assumes "a \<in> carrier L" "b \<in> carrier L"
-    and "a \<sqsubset> b" "b \<sqsubset> a"
-  shows "a \<doteq> b"
-  using assms
-  by (elim gllessE) (rule gle_anti_sym)
-
-lemma (in gpartial_order) glless_trans [trans]:
-  assumes "a .\<sqsubset> b" "b .\<sqsubset> c"
-    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
-  shows "a .\<sqsubset> c"
-using assms
-apply (elim gllessE, intro gllessI)
- apply (iprover dest: le_trans)
-proof (rule ccontr, simp)
-  assume ab: "a \<sqsubseteq> b" and bc: "b \<sqsubseteq> c"
-    and ac: "a \<doteq> c"
-    and nbc: "\<not> b \<doteq> c"
-  note ac[symmetric]
-  also note ab
-  finally have "c \<sqsubseteq> b" by simp
-  with bc have "b \<doteq> c" by (iprover intro: gle_anti_sym carr)
-  with nbc
-      show "False" by simp
-qed
-*)
-
-subsubsection {* Upper and lower bounds of a set *}
-
-constdefs (structure L)
-  Upper :: "[_, 'a set] => 'a set"
-  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
-
-  Lower :: "[_, 'a set] => 'a set"
-  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
-
-lemma Upper_closed [intro!, simp]:
-  "Upper L A \<subseteq> carrier L"
-  by (unfold Upper_def) clarify
-
-lemma Upper_memD [dest]:
-  fixes L (structure)
-  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
-  by (unfold Upper_def) blast
-
-lemma (in gpartial_order) Upper_elemD [dest]:
-  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
-  unfolding Upper_def elem_def
-  by (blast dest: sym)
-
-lemma Upper_memI:
-  fixes L (structure)
-  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
-  by (unfold Upper_def) blast
-
-lemma (in gpartial_order) Upper_elemI:
-  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
-  unfolding Upper_def by blast
-
-lemma Upper_antimono:
-  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
-  by (unfold Upper_def) blast
-
-lemma (in gpartial_order) Upper_is_closed [simp]:
-  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
-  by (rule is_closedI) (blast intro: Upper_memI)+
-
-lemma (in gpartial_order) Upper_mem_cong:
-  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
-    and aa': "a .= a'"
-    and aelem: "a \<in> Upper L A"
-  shows "a' \<in> Upper L A"
-proof (rule Upper_memI[OF _ a'carr])
-  fix y
-  assume yA: "y \<in> A"
-  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
-  also note aa'
-  finally
-      show "y \<sqsubseteq> a'"
-      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
-qed
-
-lemma (in gpartial_order) Upper_cong:
-  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "Upper L A = Upper L A'"
-unfolding Upper_def
-apply rule
- apply (rule, clarsimp) defer 1
- apply (rule, clarsimp) defer 1
-proof -
-  fix x a'
-  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
-    and a'A': "a' \<in> A'"
-  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
-
-  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
-  from this obtain a
-      where aA: "a \<in> A"
-      and a'a: "a' .= a"
-      by auto
-  note [simp] = subsetD[OF Acarr aA] carr
-
-  note a'a
-  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
-  finally show "a' \<sqsubseteq> x" by simp
-next
-  fix x a
-  assume carr: "x \<in> carrier L" "a \<in> carrier L"
-    and aA: "a \<in> A"
-  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
-
-  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
-  from this obtain a'
-      where a'A': "a' \<in> A'"
-      and aa': "a .= a'"
-      by auto
-  note [simp] = subsetD[OF A'carr a'A'] carr
-
-  note aa'
-  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
-  finally show "a \<sqsubseteq> x" by simp
-qed
-
-lemma Lower_closed [intro!, simp]:
-  "Lower L A \<subseteq> carrier L"
-  by (unfold Lower_def) clarify
-
-lemma Lower_memD [dest]:
-  fixes L (structure)
-  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
-  by (unfold Lower_def) blast
-
-lemma Lower_memI:
-  fixes L (structure)
-  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
-  by (unfold Lower_def) blast
-
-lemma Lower_antimono:
-  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
-  by (unfold Lower_def) blast
-
-lemma (in gpartial_order) Lower_is_closed [simp]:
-  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
-  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
-
-lemma (in gpartial_order) Lower_mem_cong:
-  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
-    and aa': "a .= a'"
-    and aelem: "a \<in> Lower L A"
-  shows "a' \<in> Lower L A"
-using assms Lower_closed[of L A]
-by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
-
-lemma (in gpartial_order) Lower_cong:
-  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "Lower L A = Lower L A'"
-using Lower_memD[of y]
-unfolding Lower_def
-apply safe
- apply clarsimp defer 1
- apply clarsimp defer 1
-proof -
-  fix x a'
-  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
-    and a'A': "a' \<in> A'"
-  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
-  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
-
-  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
-  from this obtain a
-      where aA: "a \<in> A"
-      and a'a: "a' .= a"
-      by auto
-
-  from aA and subsetD[OF Acarr aA]
-      have "x \<sqsubseteq> a" by (rule aLxCond)
-  also note a'a[symmetric]
-  finally
-      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
-next
-  fix x a
-  assume carr: "x \<in> carrier L" "a \<in> carrier L"
-    and aA: "a \<in> A"
-  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
-  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
-
-  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
-  from this obtain a'
-      where a'A': "a' \<in> A'"
-      and aa': "a .= a'"
-      by auto
-  from a'A' and subsetD[OF A'carr a'A']
-      have "x \<sqsubseteq> a'" by (rule a'LxCond)
-  also note aa'[symmetric]
-  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
-qed
-
-
-subsubsection {* Least and greatest, as predicate *}
-
-constdefs (structure L)
-  gleast :: "[_, 'a, 'a set] => bool"
-  "gleast L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
-
-  ggreatest :: "[_, 'a, 'a set] => bool"
-  "ggreatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
-
-lemma gleast_closed [intro, simp]:
-  "gleast L l A ==> l \<in> carrier L"
-  by (unfold gleast_def) fast
-
-lemma gleast_mem:
-  "gleast L l A ==> l \<in> A"
-  by (unfold gleast_def) fast
-
-lemma (in gpartial_order) gleast_unique:
-  "[| gleast L x A; gleast L y A |] ==> x .= y"
-  by (unfold gleast_def) blast
-
-lemma gleast_le:
-  fixes L (structure)
-  shows "[| gleast L x A; a \<in> A |] ==> x \<sqsubseteq> a"
-  by (unfold gleast_def) fast
-
-lemma (in gpartial_order) gleast_cong:
-  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> gleast L x A = gleast L x' A"
-  by (unfold gleast_def) (auto dest: sym)
-
-text {* @{const gleast} is not congruent in the second parameter for 
-  @{term [locale=gpartial_order] "A {.=} A'"} *}
-
-lemma (in gpartial_order) gleast_Upper_cong_l:
-  assumes "x .= x'"
-    and "x \<in> carrier L" "x' \<in> carrier L"
-    and "A \<subseteq> carrier L"
-  shows "gleast L x (Upper L A) = gleast L x' (Upper L A)"
-  apply (rule gleast_cong) using assms by auto
-
-lemma (in gpartial_order) gleast_Upper_cong_r:
-  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
-    and AA': "A {.=} A'"
-  shows "gleast L x (Upper L A) = gleast L x (Upper L A')"
-apply (subgoal_tac "Upper L A = Upper L A'", simp)
-by (rule Upper_cong) fact+
-
-lemma gleast_UpperI:
-  fixes L (structure)
-  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
-    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
-    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
-  shows "gleast L s (Upper L A)"
-proof -
-  have "Upper L A \<subseteq> carrier L" by simp
-  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
-  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
-  ultimately show ?thesis by (simp add: gleast_def)
-qed
-
-lemma gleast_Upper_above:
-  fixes L (structure)
-  shows "[| gleast L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
-  by (unfold gleast_def) blast
-
-lemma ggreatest_closed [intro, simp]:
-  "ggreatest L l A ==> l \<in> carrier L"
-  by (unfold ggreatest_def) fast
-
-lemma ggreatest_mem:
-  "ggreatest L l A ==> l \<in> A"
-  by (unfold ggreatest_def) fast
-
-lemma (in gpartial_order) ggreatest_unique:
-  "[| ggreatest L x A; ggreatest L y A |] ==> x .= y"
-  by (unfold ggreatest_def) blast
-
-lemma ggreatest_le:
-  fixes L (structure)
-  shows "[| ggreatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
-  by (unfold ggreatest_def) fast
-
-lemma (in gpartial_order) ggreatest_cong:
-  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
-  ggreatest L x A = ggreatest L x' A"
-  by (unfold ggreatest_def) (auto dest: sym)
-
-text {* @{const ggreatest} is not congruent in the second parameter for 
-  @{term [locale=gpartial_order] "A {.=} A'"} *}
-
-lemma (in gpartial_order) ggreatest_Lower_cong_l:
-  assumes "x .= x'"
-    and "x \<in> carrier L" "x' \<in> carrier L"
-    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
-  shows "ggreatest L x (Lower L A) = ggreatest L x' (Lower L A)"
-  apply (rule ggreatest_cong) using assms by auto
-
-lemma (in gpartial_order) ggreatest_Lower_cong_r:
-  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
-    and AA': "A {.=} A'"
-  shows "ggreatest L x (Lower L A) = ggreatest L x (Lower L A')"
-apply (subgoal_tac "Lower L A = Lower L A'", simp)
-by (rule Lower_cong) fact+
-
-lemma ggreatest_LowerI:
-  fixes L (structure)
-  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
-    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
-    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
-  shows "ggreatest L i (Lower L A)"
-proof -
-  have "Lower L A \<subseteq> carrier L" by simp
-  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
-  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
-  ultimately show ?thesis by (simp add: ggreatest_def)
-qed
-
-lemma ggreatest_Lower_below:
-  fixes L (structure)
-  shows "[| ggreatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
-  by (unfold ggreatest_def) blast
-
-text {* Supremum and infimum *}
-
-constdefs (structure L)
-  gsup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
-  "\<Squnion>A == SOME x. gleast L x (Upper L A)"
-
-  ginf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
-  "\<Sqinter>A == SOME x. ggreatest L x (Lower L A)"
-
-  gjoin :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
-  "x \<squnion> y == \<Squnion> {x, y}"
-
-  gmeet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
-  "x \<sqinter> y == \<Sqinter> {x, y}"
-
-
-subsection {* Lattices *}
-
-locale gupper_semilattice = gpartial_order +
-  assumes gsup_of_two_exists:
-    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. gleast L s (Upper L {x, y})"
-
-locale glower_semilattice = gpartial_order +
-  assumes ginf_of_two_exists:
-    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. ggreatest L s (Lower L {x, y})"
-
-locale glattice = gupper_semilattice + glower_semilattice
-
-
-subsubsection {* Supremum *}
-
-lemma (in gupper_semilattice) gjoinI:
-  "[| !!l. gleast L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
-  ==> P (x \<squnion> y)"
-proof (unfold gjoin_def gsup_def)
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-    and P: "!!l. gleast L l (Upper L {x, y}) ==> P l"
-  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
-  with L show "P (SOME l. gleast L l (Upper L {x, y}))"
-    by (fast intro: someI2 P)
-qed
-
-lemma (in gupper_semilattice) gjoin_closed [simp]:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
-  by (rule gjoinI) (rule gleast_closed)
-
-lemma (in gupper_semilattice) gjoin_cong_l:
-  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
-    and xx': "x .= x'"
-  shows "x \<squnion> y .= x' \<squnion> y"
-proof (rule gjoinI, rule gjoinI)
-  fix a b
-  from xx' carr
-      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
-
-  assume gleasta: "gleast L a (Upper L {x, y})"
-  assume "gleast L b (Upper L {x', y})"
-  with carr
-      have gleastb: "gleast L b (Upper L {x, y})"
-      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
-
-  from gleasta gleastb
-      show "a .= b" by (rule gleast_unique)
-qed (rule carr)+
-
-lemma (in gupper_semilattice) gjoin_cong_r:
-  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
-    and yy': "y .= y'"
-  shows "x \<squnion> y .= x \<squnion> y'"
-proof (rule gjoinI, rule gjoinI)
-  fix a b
-  have "{x, y} = {y, x}" by fast
-  also from carr yy'
-      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
-  also have "{y', x} = {x, y'}" by fast
-  finally
-      have seq: "{x, y} {.=} {x, y'}" .
-
-  assume gleasta: "gleast L a (Upper L {x, y})"
-  assume "gleast L b (Upper L {x, y'})"
-  with carr
-      have gleastb: "gleast L b (Upper L {x, y})"
-      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
-
-  from gleasta gleastb
-      show "a .= b" by (rule gleast_unique)
-qed (rule carr)+
-
-lemma (in gpartial_order) gsup_of_singletonI:      (* only reflexivity needed ? *)
-  "x \<in> carrier L ==> gleast L x (Upper L {x})"
-  by (rule gleast_UpperI) auto
-
-lemma (in gpartial_order) gsup_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Squnion>{x} .= x"
-  unfolding gsup_def
-  by (rule someI2) (auto intro: gleast_unique gsup_of_singletonI)
-
-lemma (in gpartial_order) gsup_of_singleton_closed [simp]:
-  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
-  unfolding gsup_def
-  by (rule someI2) (auto intro: gsup_of_singletonI)
-
-text {* Condition on @{text A}: supremum exists. *}
-
-lemma (in gupper_semilattice) gsup_insertI:
-  "[| !!s. gleast L s (Upper L (insert x A)) ==> P s;
-  gleast L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
-  ==> P (\<Squnion>(insert x A))"
-proof (unfold gsup_def)
-  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
-    and P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
-    and gleast_a: "gleast L a (Upper L A)"
-  from L gleast_a have La: "a \<in> carrier L" by simp
-  from L gsup_of_two_exists gleast_a
-  obtain s where gleast_s: "gleast L s (Upper L {a, x})" by blast
-  show "P (SOME l. gleast L l (Upper L (insert x A)))"
-  proof (rule someI2)
-    show "gleast L s (Upper L (insert x A))"
-    proof (rule gleast_UpperI)
-      fix z
-      assume "z \<in> insert x A"
-      then show "z \<sqsubseteq> s"
-      proof
-        assume "z = x" then show ?thesis
-          by (simp add: gleast_Upper_above [OF gleast_s] L La)
-      next
-        assume "z \<in> A"
-        with L gleast_s gleast_a show ?thesis
-          by (rule_tac le_trans [where y = a]) (auto dest: gleast_Upper_above)
-      qed
-    next
-      fix y
-      assume y: "y \<in> Upper L (insert x A)"
-      show "s \<sqsubseteq> y"
-      proof (rule gleast_le [OF gleast_s], rule Upper_memI)
-	fix z
-	assume z: "z \<in> {a, x}"
-	then show "z \<sqsubseteq> y"
-	proof
-          have y': "y \<in> Upper L A"
-            apply (rule subsetD [where A = "Upper L (insert x A)"])
-             apply (rule Upper_antimono)
-	     apply blast
-	    apply (rule y)
-            done
-          assume "z = a"
-          with y' gleast_a show ?thesis by (fast dest: gleast_le)
-	next
-	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
-          with y L show ?thesis by blast
-	qed
-      qed (rule Upper_closed [THEN subsetD, OF y])
-    next
-      from L show "insert x A \<subseteq> carrier L" by simp
-      from gleast_s show "s \<in> carrier L" by simp
-    qed
-  qed (rule P)
-qed
-
-lemma (in gupper_semilattice) finite_gsup_gleast:
-  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> gleast L (\<Squnion>A) (Upper L A)"
-proof (induct set: finite)
-  case empty
-  then show ?case by simp
-next
-  case (insert x A)
-  show ?case
-  proof (cases "A = {}")
-    case True
-    with insert show ?thesis
-      by simp (simp add: gleast_cong [OF gsup_of_singleton]
-	gsup_of_singleton_closed gsup_of_singletonI)
-	(* The above step is hairy; gleast_cong can make simp loop.
-	Would want special version of simp to apply gleast_cong. *)
-  next
-    case False
-    with insert have "gleast L (\<Squnion>A) (Upper L A)" by simp
-    with _ show ?thesis
-      by (rule gsup_insertI) (simp_all add: insert [simplified])
-  qed
-qed
-
-lemma (in gupper_semilattice) finite_gsup_insertI:
-  assumes P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
-    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Squnion> (insert x A))"
-proof (cases "A = {}")
-  case True with P and xA show ?thesis
-    by (simp add: finite_gsup_gleast)
-next
-  case False with P and xA show ?thesis
-    by (simp add: gsup_insertI finite_gsup_gleast)
-qed
-
-lemma (in gupper_semilattice) finite_gsup_closed [simp]:
-  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
-proof (induct set: finite)
-  case empty then show ?case by simp
-next
-  case insert then show ?case
-    by - (rule finite_gsup_insertI, simp_all)
-qed
-
-lemma (in gupper_semilattice) gjoin_left:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
-  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
-
-lemma (in gupper_semilattice) gjoin_right:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
-  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
-
-lemma (in gupper_semilattice) gsup_of_two_gleast:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> gleast L (\<Squnion>{x, y}) (Upper L {x, y})"
-proof (unfold gsup_def)
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
-  with L show "gleast L (SOME z. gleast L z (Upper L {x, y})) (Upper L {x, y})"
-  by (fast intro: someI2 gleast_unique)  (* blast fails *)
-qed
-
-lemma (in gupper_semilattice) gjoin_le:
-  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
-    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
-  shows "x \<squnion> y \<sqsubseteq> z"
-proof (rule gjoinI [OF _ x y])
-  fix s
-  assume "gleast L s (Upper L {x, y})"
-  with sub z show "s \<sqsubseteq> z" by (fast elim: gleast_le intro: Upper_memI)
-qed
-
-lemma (in gupper_semilattice) gjoin_assoc_lemma:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
-proof (rule finite_gsup_insertI)
-  -- {* The textbook argument in Jacobson I, p 457 *}
-  fix s
-  assume gsup: "gleast L s (Upper L {x, y, z})"
-  show "x \<squnion> (y \<squnion> z) .= s"
-  proof (rule le_anti_sym)
-    from gsup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
-      by (fastsimp intro!: gjoin_le elim: gleast_Upper_above)
-  next
-    from gsup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
-    by (erule_tac gleast_le)
-      (blast intro!: Upper_memI intro: le_trans gjoin_left gjoin_right gjoin_closed)
-  qed (simp_all add: L gleast_closed [OF gsup])
-qed (simp_all add: L)
-
-text {* Commutativity holds for @{text "="}. *}
-
-lemma gjoin_comm:
-  fixes L (structure)
-  shows "x \<squnion> y = y \<squnion> x"
-  by (unfold gjoin_def) (simp add: insert_commute)
-
-lemma (in gupper_semilattice) gjoin_assoc:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
-proof -
-  (* FIXME: could be simplified by improved simp: uniform use of .=,
-     omit [symmetric] in last step. *)
-  have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: gjoin_comm)
-  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: gjoin_assoc_lemma)
-  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
-  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: gjoin_assoc_lemma [symmetric])
-  finally show ?thesis by (simp add: L)
-qed
-
-
-subsubsection {* Infimum *}
-
-lemma (in glower_semilattice) gmeetI:
-  "[| !!i. ggreatest L i (Lower L {x, y}) ==> P i;
-  x \<in> carrier L; y \<in> carrier L |]
-  ==> P (x \<sqinter> y)"
-proof (unfold gmeet_def ginf_def)
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-    and P: "!!g. ggreatest L g (Lower L {x, y}) ==> P g"
-  with ginf_of_two_exists obtain i where "ggreatest L i (Lower L {x, y})" by fast
-  with L show "P (SOME g. ggreatest L g (Lower L {x, y}))"
-  by (fast intro: someI2 ggreatest_unique P)
-qed
-
-lemma (in glower_semilattice) gmeet_closed [simp]:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
-  by (rule gmeetI) (rule ggreatest_closed)
-
-lemma (in glower_semilattice) gmeet_cong_l:
-  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
-    and xx': "x .= x'"
-  shows "x \<sqinter> y .= x' \<sqinter> y"
-proof (rule gmeetI, rule gmeetI)
-  fix a b
-  from xx' carr
-      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
-
-  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
-  assume "ggreatest L b (Lower L {x', y})"
-  with carr
-      have ggreatestb: "ggreatest L b (Lower L {x, y})"
-      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
-
-  from ggreatesta ggreatestb
-      show "a .= b" by (rule ggreatest_unique)
-qed (rule carr)+
-
-lemma (in glower_semilattice) gmeet_cong_r:
-  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
-    and yy': "y .= y'"
-  shows "x \<sqinter> y .= x \<sqinter> y'"
-proof (rule gmeetI, rule gmeetI)
-  fix a b
-  have "{x, y} = {y, x}" by fast
-  also from carr yy'
-      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
-  also have "{y', x} = {x, y'}" by fast
-  finally
-      have seq: "{x, y} {.=} {x, y'}" .
-
-  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
-  assume "ggreatest L b (Lower L {x, y'})"
-  with carr
-      have ggreatestb: "ggreatest L b (Lower L {x, y})"
-      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
-
-  from ggreatesta ggreatestb
-      show "a .= b" by (rule ggreatest_unique)
-qed (rule carr)+
-
-lemma (in gpartial_order) ginf_of_singletonI:      (* only reflexivity needed ? *)
-  "x \<in> carrier L ==> ggreatest L x (Lower L {x})"
-  by (rule ggreatest_LowerI) auto
-
-lemma (in gpartial_order) ginf_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
-  unfolding ginf_def
-  by (rule someI2) (auto intro: ggreatest_unique ginf_of_singletonI)
-
-lemma (in gpartial_order) ginf_of_singleton_closed:
-  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
-  unfolding ginf_def
-  by (rule someI2) (auto intro: ginf_of_singletonI)
-
-text {* Condition on @{text A}: infimum exists. *}
-
-lemma (in glower_semilattice) ginf_insertI:
-  "[| !!i. ggreatest L i (Lower L (insert x A)) ==> P i;
-  ggreatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
-  ==> P (\<Sqinter>(insert x A))"
-proof (unfold ginf_def)
-  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
-    and P: "!!g. ggreatest L g (Lower L (insert x A)) ==> P g"
-    and ggreatest_a: "ggreatest L a (Lower L A)"
-  from L ggreatest_a have La: "a \<in> carrier L" by simp
-  from L ginf_of_two_exists ggreatest_a
-  obtain i where ggreatest_i: "ggreatest L i (Lower L {a, x})" by blast
-  show "P (SOME g. ggreatest L g (Lower L (insert x A)))"
-  proof (rule someI2)
-    show "ggreatest L i (Lower L (insert x A))"
-    proof (rule ggreatest_LowerI)
-      fix z
-      assume "z \<in> insert x A"
-      then show "i \<sqsubseteq> z"
-      proof
-        assume "z = x" then show ?thesis
-          by (simp add: ggreatest_Lower_below [OF ggreatest_i] L La)
-      next
-        assume "z \<in> A"
-        with L ggreatest_i ggreatest_a show ?thesis
-          by (rule_tac le_trans [where y = a]) (auto dest: ggreatest_Lower_below)
-      qed
-    next
-      fix y
-      assume y: "y \<in> Lower L (insert x A)"
-      show "y \<sqsubseteq> i"
-      proof (rule ggreatest_le [OF ggreatest_i], rule Lower_memI)
-	fix z
-	assume z: "z \<in> {a, x}"
-	then show "y \<sqsubseteq> z"
-	proof
-          have y': "y \<in> Lower L A"
-            apply (rule subsetD [where A = "Lower L (insert x A)"])
-            apply (rule Lower_antimono)
-	     apply blast
-	    apply (rule y)
-            done
-          assume "z = a"
-          with y' ggreatest_a show ?thesis by (fast dest: ggreatest_le)
-	next
-          assume "z \<in> {x}"
-          with y L show ?thesis by blast
-	qed
-      qed (rule Lower_closed [THEN subsetD, OF y])
-    next
-      from L show "insert x A \<subseteq> carrier L" by simp
-      from ggreatest_i show "i \<in> carrier L" by simp
-    qed
-  qed (rule P)
-qed
-
-lemma (in glower_semilattice) finite_ginf_ggreatest:
-  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> ggreatest L (\<Sqinter>A) (Lower L A)"
-proof (induct set: finite)
-  case empty then show ?case by simp
-next
-  case (insert x A)
-  show ?case
-  proof (cases "A = {}")
-    case True
-    with insert show ?thesis
-      by simp (simp add: ggreatest_cong [OF ginf_of_singleton]
-	ginf_of_singleton_closed ginf_of_singletonI)
-  next
-    case False
-    from insert show ?thesis
-    proof (rule_tac ginf_insertI)
-      from False insert show "ggreatest L (\<Sqinter>A) (Lower L A)" by simp
-    qed simp_all
-  qed
-qed
-
-lemma (in glower_semilattice) finite_ginf_insertI:
-  assumes P: "!!i. ggreatest L i (Lower L (insert x A)) ==> P i"
-    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
-  shows "P (\<Sqinter> (insert x A))"
-proof (cases "A = {}")
-  case True with P and xA show ?thesis
-    by (simp add: finite_ginf_ggreatest)
-next
-  case False with P and xA show ?thesis
-    by (simp add: ginf_insertI finite_ginf_ggreatest)
-qed
-
-lemma (in glower_semilattice) finite_ginf_closed [simp]:
-  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
-proof (induct set: finite)
-  case empty then show ?case by simp
-next
-  case insert then show ?case
-    by (rule_tac finite_ginf_insertI) (simp_all)
-qed
-
-lemma (in glower_semilattice) gmeet_left:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
-  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
-
-lemma (in glower_semilattice) gmeet_right:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
-  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
-
-lemma (in glower_semilattice) ginf_of_two_ggreatest:
-  "[| x \<in> carrier L; y \<in> carrier L |] ==>
-  ggreatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
-proof (unfold ginf_def)
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-  with ginf_of_two_exists obtain s where "ggreatest L s (Lower L {x, y})" by fast
-  with L
-  show "ggreatest L (SOME z. ggreatest L z (Lower L {x, y})) (Lower L {x, y})"
-  by (fast intro: someI2 ggreatest_unique)  (* blast fails *)
-qed
-
-lemma (in glower_semilattice) gmeet_le:
-  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
-    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
-  shows "z \<sqsubseteq> x \<sqinter> y"
-proof (rule gmeetI [OF _ x y])
-  fix i
-  assume "ggreatest L i (Lower L {x, y})"
-  with sub z show "z \<sqsubseteq> i" by (fast elim: ggreatest_le intro: Lower_memI)
-qed
-
-lemma (in glower_semilattice) gmeet_assoc_lemma:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
-proof (rule finite_ginf_insertI)
-  txt {* The textbook argument in Jacobson I, p 457 *}
-  fix i
-  assume ginf: "ggreatest L i (Lower L {x, y, z})"
-  show "x \<sqinter> (y \<sqinter> z) .= i"
-  proof (rule le_anti_sym)
-    from ginf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
-      by (fastsimp intro!: gmeet_le elim: ggreatest_Lower_below)
-  next
-    from ginf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
-    by (erule_tac ggreatest_le)
-      (blast intro!: Lower_memI intro: le_trans gmeet_left gmeet_right gmeet_closed)
-  qed (simp_all add: L ggreatest_closed [OF ginf])
-qed (simp_all add: L)
-
-lemma gmeet_comm:
-  fixes L (structure)
-  shows "x \<sqinter> y = y \<sqinter> x"
-  by (unfold gmeet_def) (simp add: insert_commute)
-
-lemma (in glower_semilattice) gmeet_assoc:
-  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
-proof -
-  (* FIXME: improved simp, see gjoin_assoc above *)
-  have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: gmeet_comm)
-  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: gmeet_assoc_lemma)
-  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
-  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: gmeet_assoc_lemma [symmetric])
-  finally show ?thesis by (simp add: L)
-qed
-
-
-subsection {* Total Orders *}
-
-locale gtotal_order = gpartial_order +
-  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-
-text {* Introduction rule: the usual definition of total order *}
-
-lemma (in gpartial_order) gtotal_orderI:
-  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-  shows "gtotal_order L"
-  by unfold_locales (rule total)
-
-text {* Total orders are lattices. *}
-
-interpretation gtotal_order < glattice
-proof unfold_locales
-  fix x y
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-  show "EX s. gleast L s (Upper L {x, y})"
-  proof -
-    note total L
-    moreover
-    {
-      assume "x \<sqsubseteq> y"
-      with L have "gleast L y (Upper L {x, y})"
-        by (rule_tac gleast_UpperI) auto
-    }
-    moreover
-    {
-      assume "y \<sqsubseteq> x"
-      with L have "gleast L x (Upper L {x, y})"
-        by (rule_tac gleast_UpperI) auto
-    }
-    ultimately show ?thesis by blast
-  qed
-next
-  fix x y
-  assume L: "x \<in> carrier L"  "y \<in> carrier L"
-  show "EX i. ggreatest L i (Lower L {x, y})"
-  proof -
-    note total L
-    moreover
-    {
-      assume "y \<sqsubseteq> x"
-      with L have "ggreatest L y (Lower L {x, y})"
-        by (rule_tac ggreatest_LowerI) auto
-    }
-    moreover
-    {
-      assume "x \<sqsubseteq> y"
-      with L have "ggreatest L x (Lower L {x, y})"
-        by (rule_tac ggreatest_LowerI) auto
-    }
-    ultimately show ?thesis by blast
-  qed
-qed
-
-
-subsection {* Complete lattices *}
-
-locale complete_lattice = glattice +
-  assumes gsup_exists:
-    "[| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
-    and ginf_exists:
-    "[| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
-
-text {* Introduction rule: the usual definition of complete lattice *}
-
-lemma (in gpartial_order) complete_latticeI:
-  assumes gsup_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
-    and ginf_exists:
-    "!!A. [| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
-  shows "complete_lattice L"
-  by unfold_locales (auto intro: gsup_exists ginf_exists)
-
-constdefs (structure L)
-  top :: "_ => 'a" ("\<top>\<index>")
-  "\<top> == gsup L (carrier L)"
-
-  bottom :: "_ => 'a" ("\<bottom>\<index>")
-  "\<bottom> == ginf L (carrier L)"
-
-
-lemma (in complete_lattice) gsupI:
-  "[| !!l. gleast L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
-  ==> P (\<Squnion>A)"
-proof (unfold gsup_def)
-  assume L: "A \<subseteq> carrier L"
-    and P: "!!l. gleast L l (Upper L A) ==> P l"
-  with gsup_exists obtain s where "gleast L s (Upper L A)" by blast
-  with L show "P (SOME l. gleast L l (Upper L A))"
-  by (fast intro: someI2 gleast_unique P)
-qed
-
-lemma (in complete_lattice) gsup_closed [simp]:
-  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
-  by (rule gsupI) simp_all
-
-lemma (in complete_lattice) top_closed [simp, intro]:
-  "\<top> \<in> carrier L"
-  by (unfold top_def) simp
-
-lemma (in complete_lattice) ginfI:
-  "[| !!i. ggreatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
-  ==> P (\<Sqinter>A)"
-proof (unfold ginf_def)
-  assume L: "A \<subseteq> carrier L"
-    and P: "!!l. ggreatest L l (Lower L A) ==> P l"
-  with ginf_exists obtain s where "ggreatest L s (Lower L A)" by blast
-  with L show "P (SOME l. ggreatest L l (Lower L A))"
-  by (fast intro: someI2 ggreatest_unique P)
-qed
-
-lemma (in complete_lattice) ginf_closed [simp]:
-  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
-  by (rule ginfI) simp_all
-
-lemma (in complete_lattice) bottom_closed [simp, intro]:
-  "\<bottom> \<in> carrier L"
-  by (unfold bottom_def) simp
-
-text {* Jacobson: Theorem 8.1 *}
-
-lemma Lower_empty [simp]:
-  "Lower L {} = carrier L"
-  by (unfold Lower_def) simp
-
-lemma Upper_empty [simp]:
-  "Upper L {} = carrier L"
-  by (unfold Upper_def) simp
-
-theorem (in gpartial_order) complete_lattice_criterion1:
-  assumes top_exists: "EX g. ggreatest L g (carrier L)"
-    and ginf_exists:
-      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. ggreatest L i (Lower L A)"
-  shows "complete_lattice L"
-proof (rule complete_latticeI)
-  from top_exists obtain top where top: "ggreatest L top (carrier L)" ..
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  let ?B = "Upper L A"
-  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: ggreatest_le)
-  then have B_non_empty: "?B ~= {}" by fast
-  have B_L: "?B \<subseteq> carrier L" by simp
-  from ginf_exists [OF B_L B_non_empty]
-  obtain b where b_ginf_B: "ggreatest L b (Lower L ?B)" ..
-  have "gleast L b (Upper L A)"
-apply (rule gleast_UpperI)
-   apply (rule ggreatest_le [where A = "Lower L ?B"])
-    apply (rule b_ginf_B)
-   apply (rule Lower_memI)
-    apply (erule Upper_memD [THEN conjunct1])
-     apply assumption
-    apply (rule L)
-   apply (fast intro: L [THEN subsetD])
-  apply (erule ggreatest_Lower_below [OF b_ginf_B])
-  apply simp
- apply (rule L)
-apply (rule ggreatest_closed [OF b_ginf_B])
-done
-  then show "EX s. gleast L s (Upper L A)" ..
-next
-  fix A
-  assume L: "A \<subseteq> carrier L"
-  show "EX i. ggreatest L i (Lower L A)"
-  proof (cases "A = {}")
-    case True then show ?thesis
-      by (simp add: top_exists)
-  next
-    case False with L show ?thesis
-      by (rule ginf_exists)
-  qed
-qed
-
-(* TODO: prove dual version *)
-
-
-subsection {* Examples *}
-
-(* Not so useful for the generalised version.
-
-subsubsection {* Powerset of a Set is a Complete Lattice *}
-
-theorem powerset_is_complete_lattice:
-  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
-  (is "complete_lattice ?L")
-proof (rule gpartial_order.complete_latticeI)
-  show "gpartial_order ?L"
-    by (rule gpartial_order.intro) auto
-next
-  fix B
-  assume B: "B \<subseteq> carrier ?L"
-  show "EX s. gleast ?L s (Upper ?L B)"
-  proof
-    from B show "gleast ?L (\<Union> B) (Upper ?L B)"
-      by (fastsimp intro!: gleast_UpperI simp: Upper_def)
-  qed
-next
-  fix B
-  assume B: "B \<subseteq> carrier ?L"
-  show "EX i. ggreatest ?L i (Lower ?L B)"
-  proof
-    from B show "ggreatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
-      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
-	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
-      by (fastsimp intro!: ggreatest_LowerI simp: Lower_def)
-  qed
-qed
-
-text {* An other example, that of the lattice of subgroups of a group,
-  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
-
-*)
-
-end
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/Algebra/Group.thy	Wed Jul 30 19:03:33 2008 +0200
@@ -712,8 +712,8 @@
 text_raw {* \label{sec:subgroup-lattice} *}
 
 theorem (in group) subgroups_partial_order:
-  "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
-  by (rule partial_order.intro) simp_all
+  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
+  by unfold_locales simp_all
 
 lemma (in group) subgroup_self:
   "subgroup (carrier G) G"
@@ -757,7 +757,7 @@
 qed
 
 theorem (in group) subgroups_complete_lattice:
-  "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
+  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
     (is "complete_lattice ?L")
 proof (rule partial_order.complete_lattice_criterion1)
   show "partial_order ?L" by (rule subgroups_partial_order)
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Wed Jul 30 19:03:33 2008 +0200
@@ -208,27 +208,27 @@
   by simp_all
 
 interpretation int [unfolded UNIV]:
-  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
-  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
-    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
-    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
+  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
+    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
+    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
 proof -
-  show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
+  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
     by unfold_locales simp_all
-  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
+  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
     by simp
-  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
+  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
     by simp
-  show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
+  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
     by (simp add: lless_def) auto
 qed
 
 interpretation int [unfolded UNIV]:
-  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
-  where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
-    and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
+  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
+  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
+    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
 proof -
-  let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
+  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
   show "lattice ?Z"
     apply unfold_locales
     apply (simp add: least_def Upper_def)
@@ -250,7 +250,7 @@
 qed
 
 interpretation int [unfolded UNIV]:
-  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
+  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
   by unfold_locales clarsimp
 
 
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/Algebra/Lattice.thy	Wed Jul 30 19:03:33 2008 +0200
@@ -1,5 +1,5 @@
 (*
-  Title:     HOL/Algebra/Lattice.thy
+  Title:     HOL/Algebra/GLattice.thy
   Id:        $Id$
   Author:    Clemens Ballarin, started 7 November 2003
   Copyright: Clemens Ballarin
@@ -7,88 +7,202 @@
 
 theory Lattice imports Congruence begin
 
-
 section {* Orders and Lattices *}
 
 subsection {* Partial Orders *}
 
-record 'a order = "'a partial_object" +
+record 'a gorder = "'a eq_object" +
   le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
 
-locale partial_order =
-  fixes L (structure)
-  assumes refl [intro, simp]:
-                  "x \<in> carrier L ==> x \<sqsubseteq> x"
-    and anti_sym [intro]:
-                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
-    and trans [trans]:
-                  "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
-                   x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
+locale weak_partial_order = equivalence L +
+  assumes le_refl [intro, simp]:
+      "x \<in> carrier L ==> x \<sqsubseteq> x"
+    and weak_le_anti_sym [intro]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
+    and le_trans [trans]:
+      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
+    and le_cong:
+      "\<lbrakk> x .= y; z .= w; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L; w \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z \<longleftrightarrow> y \<sqsubseteq> w"
 
 constdefs (structure L)
   lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
-  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
+  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
+
+
+subsubsection {* The order relation *}
+
+context weak_partial_order begin
+
+lemma le_cong_l [intro, trans]:
+  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD2])
+
+lemma le_cong_r [intro, trans]:
+  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
+  by (auto intro: le_cong [THEN iffD1])
+
+lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
+  by (simp add: le_cong_l)
+
+end
+
+lemma weak_llessI:
+  fixes R (structure)
+  assumes "x \<sqsubseteq> y" and "~(x .= y)"
+  shows "x \<sqsubset> y"
+  using assms unfolding lless_def by simp
+
+lemma lless_imp_le:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "x \<sqsubseteq> y"
+  using assms unfolding lless_def by simp
+
+lemma weak_lless_imp_not_eq:
+  fixes R (structure)
+  assumes "x \<sqsubset> y"
+  shows "\<not> (x .= y)"
+  using assms unfolding lless_def by simp
 
-  -- {* Upper and lower bounds of a set. *}
+lemma weak_llessE:
+  fixes R (structure)
+  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
+  shows "P"
+  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
+
+lemma (in weak_partial_order) lless_cong_l [trans]:
+  assumes xx': "x .= x'"
+    and xy: "x' \<sqsubset> y"
+    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+  shows "x \<sqsubset> y"
+  using assms unfolding lless_def by (auto intro: trans sym)
+
+lemma (in weak_partial_order) lless_cong_r [trans]:
+  assumes xy: "x \<sqsubset> y"
+    and  yy': "y .= y'"
+    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+  shows "x \<sqsubset> y'"
+  using assms unfolding lless_def by (auto intro: trans sym)
+
+
+lemma (in weak_partial_order) lless_antisym:
+  assumes "a \<in> carrier L" "b \<in> carrier L"
+    and "a \<sqsubset> b" "b \<sqsubset> a"
+  shows "P"
+  using assms
+  by (elim weak_llessE) auto
+
+lemma (in weak_partial_order) lless_trans [trans]:
+  assumes "a \<sqsubset> b" "b \<sqsubset> c"
+    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
+  shows "a \<sqsubset> c"
+  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
+
+
+subsubsection {* Upper and lower bounds of a set *}
+
+constdefs (structure L)
   Upper :: "[_, 'a set] => 'a set"
-  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
-                carrier L"
+  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
 
   Lower :: "[_, 'a set] => 'a set"
-  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
-                carrier L"
-
-  -- {* Least and greatest, as predicate. *}
-  least :: "[_, 'a, 'a set] => bool"
-  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
-
-  greatest :: "[_, 'a, 'a set] => bool"
-  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
-
-  -- {* Supremum and infimum *}
-  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
-  "\<Squnion>A == THE x. least L x (Upper L A)"
+  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
 
-  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
-  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
-
-  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
-  "x \<squnion> y == sup L {x, y}"
-
-  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
-  "x \<sqinter> y == inf L {x, y}"
-
-
-subsubsection {* Upper *}
-
-lemma Upper_closed [intro, simp]:
+lemma Upper_closed [intro!, simp]:
   "Upper L A \<subseteq> carrier L"
   by (unfold Upper_def) clarify
 
 lemma Upper_memD [dest]:
   fixes L (structure)
-  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
+  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   by (unfold Upper_def) blast
 
+lemma (in weak_partial_order) Upper_elemD [dest]:
+  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
+  unfolding Upper_def elem_def
+  by (blast dest: sym)
+
 lemma Upper_memI:
   fixes L (structure)
   shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   by (unfold Upper_def) blast
 
+lemma (in weak_partial_order) Upper_elemI:
+  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
+  unfolding Upper_def by blast
+
 lemma Upper_antimono:
   "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   by (unfold Upper_def) blast
 
+lemma (in weak_partial_order) Upper_is_closed [simp]:
+  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
+  by (rule is_closedI) (blast intro: Upper_memI)+
 
-subsubsection {* Lower *}
+lemma (in weak_partial_order) Upper_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Upper L A"
+  shows "a' \<in> Upper L A"
+proof (rule Upper_memI[OF _ a'carr])
+  fix y
+  assume yA: "y \<in> A"
+  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
+  also note aa'
+  finally
+      show "y \<sqsubseteq> a'"
+      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
+qed
+
+lemma (in weak_partial_order) Upper_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Upper L A = Upper L A'"
+unfolding Upper_def
+apply rule
+ apply (rule, clarsimp) defer 1
+ apply (rule, clarsimp) defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
 
-lemma Lower_closed [intro, simp]:
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+  note [simp] = subsetD[OF Acarr aA] carr
+
+  note a'a
+  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
+  finally show "a' \<sqsubseteq> x" by simp
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  note [simp] = subsetD[OF A'carr a'A'] carr
+
+  note aa'
+  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
+  finally show "a \<sqsubseteq> x" by simp
+qed
+
+lemma Lower_closed [intro!, simp]:
   "Lower L A \<subseteq> carrier L"
   by (unfold Lower_def) clarify
 
 lemma Lower_memD [dest]:
   fixes L (structure)
-  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
+  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   by (unfold Lower_def) blast
 
 lemma Lower_memI:
@@ -100,19 +214,86 @@
   "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   by (unfold Lower_def) blast
 
+lemma (in weak_partial_order) Lower_is_closed [simp]:
+  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
+  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
 
-subsubsection {* least *}
+lemma (in weak_partial_order) Lower_mem_cong:
+  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
+    and aa': "a .= a'"
+    and aelem: "a \<in> Lower L A"
+  shows "a' \<in> Lower L A"
+using assms Lower_closed[of L A]
+by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
+
+lemma (in weak_partial_order) Lower_cong:
+  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "Lower L A = Lower L A'"
+using Lower_memD[of y]
+unfolding Lower_def
+apply safe
+ apply clarsimp defer 1
+ apply clarsimp defer 1
+proof -
+  fix x a'
+  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
+    and a'A': "a' \<in> A'"
+  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
+  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
+
+  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
+  from this obtain a
+      where aA: "a \<in> A"
+      and a'a: "a' .= a"
+      by auto
+
+  from aA and subsetD[OF Acarr aA]
+      have "x \<sqsubseteq> a" by (rule aLxCond)
+  also note a'a[symmetric]
+  finally
+      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
+next
+  fix x a
+  assume carr: "x \<in> carrier L" "a \<in> carrier L"
+    and aA: "a \<in> A"
+  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
+  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
+
+  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
+  from this obtain a'
+      where a'A': "a' \<in> A'"
+      and aa': "a .= a'"
+      by auto
+  from a'A' and subsetD[OF A'carr a'A']
+      have "x \<sqsubseteq> a'" by (rule a'LxCond)
+  also note aa'[symmetric]
+  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
+qed
+
+
+subsubsection {* Least and greatest, as predicate *}
+
+constdefs (structure L)
+  least :: "[_, 'a, 'a set] => bool"
+  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
+
+  greatest :: "[_, 'a, 'a set] => bool"
+  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
+
+text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
+  .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
 
 lemma least_closed [intro, simp]:
-  shows "least L l A ==> l \<in> carrier L"
+  "least L l A ==> l \<in> carrier L"
   by (unfold least_def) fast
 
 lemma least_mem:
   "least L l A ==> l \<in> A"
   by (unfold least_def) fast
 
-lemma (in partial_order) least_unique:
-  "[| least L x A; least L y A |] ==> x = y"
+lemma (in weak_partial_order) weak_least_unique:
+  "[| least L x A; least L y A |] ==> x .= y"
   by (unfold least_def) blast
 
 lemma least_le:
@@ -120,6 +301,27 @@
   shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   by (unfold least_def) fast
 
+lemma (in weak_partial_order) least_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
+  by (unfold least_def) (auto dest: sym)
+
+text {* @{const least} is not congruent in the second parameter for 
+  @{term [locale=weak_partial_order] "A {.=} A'"} *}
+
+lemma (in weak_partial_order) least_Upper_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L"
+  shows "least L x (Upper L A) = least L x' (Upper L A)"
+  apply (rule least_cong) using assms by auto
+
+lemma (in weak_partial_order) least_Upper_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
+    and AA': "A {.=} A'"
+  shows "least L x (Upper L A) = least L x (Upper L A')"
+apply (subgoal_tac "Upper L A = Upper L A'", simp)
+by (rule Upper_cong) fact+
+
 lemma least_UpperI:
   fixes L (structure)
   assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
@@ -133,19 +335,21 @@
   ultimately show ?thesis by (simp add: least_def)
 qed
 
-
-subsubsection {* greatest *}
+lemma least_Upper_above:
+  fixes L (structure)
+  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
+  by (unfold least_def) blast
 
 lemma greatest_closed [intro, simp]:
-  shows "greatest L l A ==> l \<in> carrier L"
+  "greatest L l A ==> l \<in> carrier L"
   by (unfold greatest_def) fast
 
 lemma greatest_mem:
   "greatest L l A ==> l \<in> A"
   by (unfold greatest_def) fast
 
-lemma (in partial_order) greatest_unique:
-  "[| greatest L x A; greatest L y A |] ==> x = y"
+lemma (in weak_partial_order) weak_greatest_unique:
+  "[| greatest L x A; greatest L y A |] ==> x .= y"
   by (unfold greatest_def) blast
 
 lemma greatest_le:
@@ -153,6 +357,28 @@
   shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   by (unfold greatest_def) fast
 
+lemma (in weak_partial_order) greatest_cong:
+  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
+  greatest L x A = greatest L x' A"
+  by (unfold greatest_def) (auto dest: sym)
+
+text {* @{const greatest} is not congruent in the second parameter for 
+  @{term [locale=weak_partial_order] "A {.=} A'"} *}
+
+lemma (in weak_partial_order) greatest_Lower_cong_l:
+  assumes "x .= x'"
+    and "x \<in> carrier L" "x' \<in> carrier L"
+    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
+  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
+  apply (rule greatest_cong) using assms by auto
+
+lemma (in weak_partial_order) greatest_Lower_cong_r:
+  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
+    and AA': "A {.=} A'"
+  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
+apply (subgoal_tac "Lower L A = Lower L A'", simp)
+by (rule Lower_cong) fact+
+
 lemma greatest_LowerI:
   fixes L (structure)
   assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
@@ -166,55 +392,116 @@
   ultimately show ?thesis by (simp add: greatest_def)
 qed
 
-
-subsection {* Lattices *}
-
-locale lattice = partial_order +
-  assumes sup_of_two_exists:
-    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
-    and inf_of_two_exists:
-    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
-
-lemma least_Upper_above:
-  fixes L (structure)
-  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
-  by (unfold least_def) blast
-
 lemma greatest_Lower_below:
   fixes L (structure)
   shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   by (unfold greatest_def) blast
 
+text {* Supremum and infimum *}
+
+constdefs (structure L)
+  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
+  "\<Squnion>A == SOME x. least L x (Upper L A)"
+
+  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
+  "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
+
+  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
+  "x \<squnion> y == \<Squnion> {x, y}"
+
+  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
+  "x \<sqinter> y == \<Sqinter> {x, y}"
+
+
+subsection {* Lattices *}
+
+locale weak_upper_semilattice = weak_partial_order +
+  assumes sup_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
+
+locale weak_lower_semilattice = weak_partial_order +
+  assumes inf_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
+
+locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
+
 
 subsubsection {* Supremum *}
 
-lemma (in lattice) joinI:
+lemma (in weak_upper_semilattice) joinI:
   "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   ==> P (x \<squnion> y)"
 proof (unfold join_def sup_def)
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
     and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
-  with L show "P (THE l. least L l (Upper L {x, y}))"
-    by (fast intro: theI2 least_unique P)
+  with L show "P (SOME l. least L l (Upper L {x, y}))"
+    by (fast intro: someI2 P)
 qed
 
-lemma (in lattice) join_closed [simp]:
+lemma (in weak_upper_semilattice) join_closed [simp]:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   by (rule joinI) (rule least_closed)
 
-lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
-  "x \<in> carrier L ==> least L x (Upper L {x})"
-  by (rule least_UpperI) fast+
+lemma (in weak_upper_semilattice) join_cong_l:
+  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+    and xx': "x .= x'"
+  shows "x \<squnion> y .= x' \<squnion> y"
+proof (rule joinI, rule joinI)
+  fix a b
+  from xx' carr
+      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
+
+  assume leasta: "least L a (Upper L {x, y})"
+  assume "least L b (Upper L {x', y})"
+  with carr
+      have leastb: "least L b (Upper L {x, y})"
+      by (simp add: least_Upper_cong_r[OF _ _ seq])
+
+  from leasta leastb
+      show "a .= b" by (rule weak_least_unique)
+qed (rule carr)+
 
-lemma (in partial_order) sup_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Squnion>{x} = x"
-  by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
+lemma (in weak_upper_semilattice) join_cong_r:
+  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+    and yy': "y .= y'"
+  shows "x \<squnion> y .= x \<squnion> y'"
+proof (rule joinI, rule joinI)
+  fix a b
+  have "{x, y} = {y, x}" by fast
+  also from carr yy'
+      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
+  also have "{y', x} = {x, y'}" by fast
+  finally
+      have seq: "{x, y} {.=} {x, y'}" .
 
+  assume leasta: "least L a (Upper L {x, y})"
+  assume "least L b (Upper L {x, y'})"
+  with carr
+      have leastb: "least L b (Upper L {x, y})"
+      by (simp add: least_Upper_cong_r[OF _ _ seq])
+
+  from leasta leastb
+      show "a .= b" by (rule weak_least_unique)
+qed (rule carr)+
+
+lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
+  "x \<in> carrier L ==> least L x (Upper L {x})"
+  by (rule least_UpperI) auto
+
+lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Squnion>{x} .= x"
+  unfolding sup_def
+  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
+
+lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
+  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
+  unfolding sup_def
+  by (rule someI2) (auto intro: sup_of_singletonI)
 
 text {* Condition on @{text A}: supremum exists. *}
 
-lemma (in lattice) sup_insertI:
+lemma (in weak_upper_semilattice) sup_insertI:
   "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   ==> P (\<Squnion>(insert x A))"
@@ -225,8 +512,8 @@
   from L least_a have La: "a \<in> carrier L" by simp
   from L sup_of_two_exists least_a
   obtain s where least_s: "least L s (Upper L {a, x})" by blast
-  show "P (THE l. least L l (Upper L (insert x A)))"
-  proof (rule theI2)
+  show "P (SOME l. least L l (Upper L (insert x A)))"
+  proof (rule someI2)
     show "least L s (Upper L (insert x A))"
     proof (rule least_UpperI)
       fix z
@@ -238,7 +525,7 @@
       next
         assume "z \<in> A"
         with L least_s least_a show ?thesis
-          by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
+          by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
       qed
     next
       fix y
@@ -266,55 +553,10 @@
       from L show "insert x A \<subseteq> carrier L" by simp
       from least_s show "s \<in> carrier L" by simp
     qed
-  next
-    fix l
-    assume least_l: "least L l (Upper L (insert x A))"
-    show "l = s"
-    proof (rule least_unique)
-      show "least L s (Upper L (insert x A))"
-      proof (rule least_UpperI)
-        fix z
-        assume "z \<in> insert x A"
-        then show "z \<sqsubseteq> s"
-	proof
-          assume "z = x" then show ?thesis
-            by (simp add: least_Upper_above [OF least_s] L La)
-	next
-          assume "z \<in> A"
-          with L least_s least_a show ?thesis
-            by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
-	qed
-      next
-        fix y
-        assume y: "y \<in> Upper L (insert x A)"
-        show "s \<sqsubseteq> y"
-        proof (rule least_le [OF least_s], rule Upper_memI)
-          fix z
-          assume z: "z \<in> {a, x}"
-          then show "z \<sqsubseteq> y"
-          proof
-            have y': "y \<in> Upper L A"
-	      apply (rule subsetD [where A = "Upper L (insert x A)"])
-	      apply (rule Upper_antimono)
-	       apply blast
-	      apply (rule y)
-	      done
-            assume "z = a"
-            with y' least_a show ?thesis by (fast dest: least_le)
-	  next
-            assume "z \<in> {x}"
-            with y L show ?thesis by blast
-          qed
-        qed (rule Upper_closed [THEN subsetD, OF y])
-      next
-        from L show "insert x A \<subseteq> carrier L" by simp
-        from least_s show "s \<in> carrier L" by simp
-      qed
-    qed (rule least_l)
   qed (rule P)
 qed
 
-lemma (in lattice) finite_sup_least:
+lemma (in weak_upper_semilattice) finite_sup_least:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
 proof (induct set: finite)
   case empty
@@ -324,7 +566,11 @@
   show ?case
   proof (cases "A = {}")
     case True
-    with insert show ?thesis by (simp add: sup_of_singletonI)
+    with insert show ?thesis
+      by simp (simp add: least_cong [OF weak_sup_of_singleton]
+	sup_of_singleton_closed sup_of_singletonI)
+	(* The above step is hairy; least_cong can make simp loop.
+	Would want special version of simp to apply least_cong. *)
   next
     case False
     with insert have "least L (\<Squnion>A) (Upper L A)" by simp
@@ -333,19 +579,19 @@
   qed
 qed
 
-lemma (in lattice) finite_sup_insertI:
+lemma (in weak_upper_semilattice) finite_sup_insertI:
   assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   shows "P (\<Squnion> (insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
-    by (simp add: sup_of_singletonI)
+    by (simp add: finite_sup_least)
 next
   case False with P and xA show ?thesis
     by (simp add: sup_insertI finite_sup_least)
 qed
 
-lemma (in lattice) finite_sup_closed:
+lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
 proof (induct set: finite)
   case empty then show ?case by simp
@@ -354,24 +600,24 @@
     by - (rule finite_sup_insertI, simp_all)
 qed
 
-lemma (in lattice) join_left:
+lemma (in weak_upper_semilattice) join_left:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   by (rule joinI [folded join_def]) (blast dest: least_mem)
 
-lemma (in lattice) join_right:
+lemma (in weak_upper_semilattice) join_right:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   by (rule joinI [folded join_def]) (blast dest: least_mem)
 
-lemma (in lattice) sup_of_two_least:
+lemma (in weak_upper_semilattice) sup_of_two_least:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
 proof (unfold sup_def)
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
-  with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
-  by (fast intro: theI2 least_unique)  (* blast fails *)
+  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
+  by (fast intro: someI2 weak_least_unique)  (* blast fails *)
 qed
 
-lemma (in lattice) join_le:
+lemma (in weak_upper_semilattice) join_le:
   assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   shows "x \<squnion> y \<sqsubseteq> z"
@@ -381,44 +627,48 @@
   with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
 qed
 
-lemma (in lattice) join_assoc_lemma:
+lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
+  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
 proof (rule finite_sup_insertI)
   -- {* The textbook argument in Jacobson I, p 457 *}
   fix s
   assume sup: "least L s (Upper L {x, y, z})"
-  show "x \<squnion> (y \<squnion> z) = s"
-  proof (rule anti_sym)
+  show "x \<squnion> (y \<squnion> z) .= s"
+  proof (rule weak_le_anti_sym)
     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
       by (fastsimp intro!: join_le elim: least_Upper_above)
   next
     from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
     by (erule_tac least_le)
-      (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
+      (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   qed (simp_all add: L least_closed [OF sup])
 qed (simp_all add: L)
 
+text {* Commutativity holds for @{text "="}. *}
+
 lemma join_comm:
   fixes L (structure)
   shows "x \<squnion> y = y \<squnion> x"
   by (unfold join_def) (simp add: insert_commute)
 
-lemma (in lattice) join_assoc:
+lemma (in weak_upper_semilattice) weak_join_assoc:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
 proof -
+  (* FIXME: could be simplified by improved simp: uniform use of .=,
+     omit [symmetric] in last step. *)
   have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
-  also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)
+  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
   also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
-  also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
-  finally show ?thesis .
+  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
+  finally show ?thesis by (simp add: L)
 qed
 
 
 subsubsection {* Infimum *}
 
-lemma (in lattice) meetI:
+lemma (in weak_lower_semilattice) meetI:
   "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   x \<in> carrier L; y \<in> carrier L |]
   ==> P (x \<sqinter> y)"
@@ -426,25 +676,73 @@
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
     and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
-  with L show "P (THE g. greatest L g (Lower L {x, y}))"
-  by (fast intro: theI2 greatest_unique P)
+  with L show "P (SOME g. greatest L g (Lower L {x, y}))"
+  by (fast intro: someI2 weak_greatest_unique P)
 qed
 
-lemma (in lattice) meet_closed [simp]:
+lemma (in weak_lower_semilattice) meet_closed [simp]:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   by (rule meetI) (rule greatest_closed)
 
-lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
-  "x \<in> carrier L ==> greatest L x (Lower L {x})"
-  by (rule greatest_LowerI) fast+
+lemma (in weak_lower_semilattice) meet_cong_l:
+  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
+    and xx': "x .= x'"
+  shows "x \<sqinter> y .= x' \<sqinter> y"
+proof (rule meetI, rule meetI)
+  fix a b
+  from xx' carr
+      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
+
+  assume greatesta: "greatest L a (Lower L {x, y})"
+  assume "greatest L b (Lower L {x', y})"
+  with carr
+      have greatestb: "greatest L b (Lower L {x, y})"
+      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
+
+  from greatesta greatestb
+      show "a .= b" by (rule weak_greatest_unique)
+qed (rule carr)+
 
-lemma (in partial_order) inf_of_singleton [simp]:
-  "x \<in> carrier L ==> \<Sqinter> {x} = x"
-  by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
+lemma (in weak_lower_semilattice) meet_cong_r:
+  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
+    and yy': "y .= y'"
+  shows "x \<sqinter> y .= x \<sqinter> y'"
+proof (rule meetI, rule meetI)
+  fix a b
+  have "{x, y} = {y, x}" by fast
+  also from carr yy'
+      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
+  also have "{y', x} = {x, y'}" by fast
+  finally
+      have seq: "{x, y} {.=} {x, y'}" .
+
+  assume greatesta: "greatest L a (Lower L {x, y})"
+  assume "greatest L b (Lower L {x, y'})"
+  with carr
+      have greatestb: "greatest L b (Lower L {x, y})"
+      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
 
-text {* Condition on A: infimum exists. *}
+  from greatesta greatestb
+      show "a .= b" by (rule weak_greatest_unique)
+qed (rule carr)+
+
+lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
+  "x \<in> carrier L ==> greatest L x (Lower L {x})"
+  by (rule greatest_LowerI) auto
 
-lemma (in lattice) inf_insertI:
+lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
+  unfolding inf_def
+  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
+
+lemma (in weak_partial_order) inf_of_singleton_closed:
+  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
+  unfolding inf_def
+  by (rule someI2) (auto intro: inf_of_singletonI)
+
+text {* Condition on @{text A}: infimum exists. *}
+
+lemma (in weak_lower_semilattice) inf_insertI:
   "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   ==> P (\<Sqinter>(insert x A))"
@@ -455,8 +753,8 @@
   from L greatest_a have La: "a \<in> carrier L" by simp
   from L inf_of_two_exists greatest_a
   obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
-  show "P (THE g. greatest L g (Lower L (insert x A)))"
-  proof (rule theI2)
+  show "P (SOME g. greatest L g (Lower L (insert x A)))"
+  proof (rule someI2)
     show "greatest L i (Lower L (insert x A))"
     proof (rule greatest_LowerI)
       fix z
@@ -468,7 +766,7 @@
       next
         assume "z \<in> A"
         with L greatest_i greatest_a show ?thesis
-          by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
+          by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
       qed
     next
       fix y
@@ -496,55 +794,10 @@
       from L show "insert x A \<subseteq> carrier L" by simp
       from greatest_i show "i \<in> carrier L" by simp
     qed
-  next
-    fix g
-    assume greatest_g: "greatest L g (Lower L (insert x A))"
-    show "g = i"
-    proof (rule greatest_unique)
-      show "greatest L i (Lower L (insert x A))"
-      proof (rule greatest_LowerI)
-        fix z
-        assume "z \<in> insert x A"
-        then show "i \<sqsubseteq> z"
-	proof
-          assume "z = x" then show ?thesis
-            by (simp add: greatest_Lower_below [OF greatest_i] L La)
-	next
-          assume "z \<in> A"
-          with L greatest_i greatest_a show ?thesis
-            by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
-        qed
-      next
-        fix y
-        assume y: "y \<in> Lower L (insert x A)"
-        show "y \<sqsubseteq> i"
-        proof (rule greatest_le [OF greatest_i], rule Lower_memI)
-          fix z
-          assume z: "z \<in> {a, x}"
-          then show "y \<sqsubseteq> z"
-          proof
-            have y': "y \<in> Lower L A"
-	      apply (rule subsetD [where A = "Lower L (insert x A)"])
-	      apply (rule Lower_antimono)
-	       apply blast
-	      apply (rule y)
-	      done
-            assume "z = a"
-            with y' greatest_a show ?thesis by (fast dest: greatest_le)
-	  next
-            assume "z \<in> {x}"
-            with y L show ?thesis by blast
-	  qed
-        qed (rule Lower_closed [THEN subsetD, OF y])
-      next
-        from L show "insert x A \<subseteq> carrier L" by simp
-        from greatest_i show "i \<in> carrier L" by simp
-      qed
-    qed (rule greatest_g)
   qed (rule P)
 qed
 
-lemma (in lattice) finite_inf_greatest:
+lemma (in weak_lower_semilattice) finite_inf_greatest:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
 proof (induct set: finite)
   case empty then show ?case by simp
@@ -553,7 +806,9 @@
   show ?case
   proof (cases "A = {}")
     case True
-    with insert show ?thesis by (simp add: inf_of_singletonI)
+    with insert show ?thesis
+      by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
+	inf_of_singleton_closed inf_of_singletonI)
   next
     case False
     from insert show ?thesis
@@ -563,19 +818,19 @@
   qed
 qed
 
-lemma (in lattice) finite_inf_insertI:
+lemma (in weak_lower_semilattice) finite_inf_insertI:
   assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
     and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   shows "P (\<Sqinter> (insert x A))"
 proof (cases "A = {}")
   case True with P and xA show ?thesis
-    by (simp add: inf_of_singletonI)
+    by (simp add: finite_inf_greatest)
 next
   case False with P and xA show ?thesis
     by (simp add: inf_insertI finite_inf_greatest)
 qed
 
-lemma (in lattice) finite_inf_closed:
+lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
   "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
 proof (induct set: finite)
   case empty then show ?case by simp
@@ -584,26 +839,26 @@
     by (rule_tac finite_inf_insertI) (simp_all)
 qed
 
-lemma (in lattice) meet_left:
+lemma (in weak_lower_semilattice) meet_left:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
 
-lemma (in lattice) meet_right:
+lemma (in weak_lower_semilattice) meet_right:
   "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
 
-lemma (in lattice) inf_of_two_greatest:
+lemma (in weak_lower_semilattice) inf_of_two_greatest:
   "[| x \<in> carrier L; y \<in> carrier L |] ==>
   greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
 proof (unfold inf_def)
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
   with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   with L
-  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
-  by (fast intro: theI2 greatest_unique)  (* blast fails *)
+  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
+  by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
 qed
 
-lemma (in lattice) meet_le:
+lemma (in weak_lower_semilattice) meet_le:
   assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
     and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   shows "z \<sqsubseteq> x \<sqinter> y"
@@ -613,21 +868,21 @@
   with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
 qed
 
-lemma (in lattice) meet_assoc_lemma:
+lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
+  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
 proof (rule finite_inf_insertI)
   txt {* The textbook argument in Jacobson I, p 457 *}
   fix i
   assume inf: "greatest L i (Lower L {x, y, z})"
-  show "x \<sqinter> (y \<sqinter> z) = i"
-  proof (rule anti_sym)
+  show "x \<sqinter> (y \<sqinter> z) .= i"
+  proof (rule weak_le_anti_sym)
     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
       by (fastsimp intro!: meet_le elim: greatest_Lower_below)
   next
     from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
     by (erule_tac greatest_le)
-      (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
+      (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
   qed (simp_all add: L greatest_closed [OF inf])
 qed (simp_all add: L)
 
@@ -636,33 +891,34 @@
   shows "x \<sqinter> y = y \<sqinter> x"
   by (unfold meet_def) (simp add: insert_commute)
 
-lemma (in lattice) meet_assoc:
+lemma (in weak_lower_semilattice) weak_meet_assoc:
   assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
-  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
 proof -
+  (* FIXME: improved simp, see weak_join_assoc above *)
   have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
-  also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)
+  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
   also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
-  also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)
-  finally show ?thesis .
+  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
+  finally show ?thesis by (simp add: L)
 qed
 
 
 subsection {* Total Orders *}
 
-locale total_order = partial_order +
+locale weak_total_order = weak_partial_order +
   assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
 
 text {* Introduction rule: the usual definition of total order *}
 
-lemma (in partial_order) total_orderI:
+lemma (in weak_partial_order) weak_total_orderI:
   assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
-  shows "total_order L"
+  shows "weak_total_order L"
   by unfold_locales (rule total)
 
 text {* Total orders are lattices. *}
 
-interpretation total_order < lattice
+interpretation weak_total_order < weak_lattice
 proof unfold_locales
   fix x y
   assume L: "x \<in> carrier L"  "y \<in> carrier L"
@@ -708,7 +964,7 @@
 
 subsection {* Complete lattices *}
 
-locale complete_lattice = lattice +
+locale weak_complete_lattice = weak_lattice +
   assumes sup_exists:
     "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
@@ -716,16 +972,13 @@
 
 text {* Introduction rule: the usual definition of complete lattice *}
 
-lemma (in partial_order) complete_latticeI:
+lemma (in weak_partial_order) weak_complete_latticeI:
   assumes sup_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
     and inf_exists:
     "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
-  shows "complete_lattice L"
-proof intro_locales
-  show "lattice_axioms L"
-    by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
-qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
+  shows "weak_complete_lattice L"
+  by unfold_locales (auto intro: sup_exists inf_exists)
 
 constdefs (structure L)
   top :: "_ => 'a" ("\<top>\<index>")
@@ -735,41 +988,41 @@
   "\<bottom> == inf L (carrier L)"
 
 
-lemma (in complete_lattice) supI:
+lemma (in weak_complete_lattice) supI:
   "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
   ==> P (\<Squnion>A)"
 proof (unfold sup_def)
   assume L: "A \<subseteq> carrier L"
     and P: "!!l. least L l (Upper L A) ==> P l"
   with sup_exists obtain s where "least L s (Upper L A)" by blast
-  with L show "P (THE l. least L l (Upper L A))"
-  by (fast intro: theI2 least_unique P)
+  with L show "P (SOME l. least L l (Upper L A))"
+  by (fast intro: someI2 weak_least_unique P)
 qed
 
-lemma (in complete_lattice) sup_closed [simp]:
+lemma (in weak_complete_lattice) sup_closed [simp]:
   "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
   by (rule supI) simp_all
 
-lemma (in complete_lattice) top_closed [simp, intro]:
+lemma (in weak_complete_lattice) top_closed [simp, intro]:
   "\<top> \<in> carrier L"
   by (unfold top_def) simp
 
-lemma (in complete_lattice) infI:
+lemma (in weak_complete_lattice) infI:
   "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
   ==> P (\<Sqinter>A)"
 proof (unfold inf_def)
   assume L: "A \<subseteq> carrier L"
     and P: "!!l. greatest L l (Lower L A) ==> P l"
   with inf_exists obtain s where "greatest L s (Lower L A)" by blast
-  with L show "P (THE l. greatest L l (Lower L A))"
-  by (fast intro: theI2 greatest_unique P)
+  with L show "P (SOME l. greatest L l (Lower L A))"
+  by (fast intro: someI2 weak_greatest_unique P)
 qed
 
-lemma (in complete_lattice) inf_closed [simp]:
+lemma (in weak_complete_lattice) inf_closed [simp]:
   "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
   by (rule infI) simp_all
 
-lemma (in complete_lattice) bottom_closed [simp, intro]:
+lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
   "\<bottom> \<in> carrier L"
   by (unfold bottom_def) simp
 
@@ -783,6 +1036,216 @@
   "Upper L {} = carrier L"
   by (unfold Upper_def) simp
 
+theorem (in weak_partial_order) weak_complete_lattice_criterion1:
+  assumes top_exists: "EX g. greatest L g (carrier L)"
+    and inf_exists:
+      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
+  shows "weak_complete_lattice L"
+proof (rule weak_complete_latticeI)
+  from top_exists obtain top where top: "greatest L top (carrier L)" ..
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  let ?B = "Upper L A"
+  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
+  then have B_non_empty: "?B ~= {}" by fast
+  have B_L: "?B \<subseteq> carrier L" by simp
+  from inf_exists [OF B_L B_non_empty]
+  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
+  have "least L b (Upper L A)"
+apply (rule least_UpperI)
+   apply (rule greatest_le [where A = "Lower L ?B"])
+    apply (rule b_inf_B)
+   apply (rule Lower_memI)
+    apply (erule Upper_memD [THEN conjunct1])
+     apply assumption
+    apply (rule L)
+   apply (fast intro: L [THEN subsetD])
+  apply (erule greatest_Lower_below [OF b_inf_B])
+  apply simp
+ apply (rule L)
+apply (rule greatest_closed [OF b_inf_B])
+done
+  then show "EX s. least L s (Upper L A)" ..
+next
+  fix A
+  assume L: "A \<subseteq> carrier L"
+  show "EX i. greatest L i (Lower L A)"
+  proof (cases "A = {}")
+    case True then show ?thesis
+      by (simp add: top_exists)
+  next
+    case False with L show ?thesis
+      by (rule inf_exists)
+  qed
+qed
+
+(* TODO: prove dual version *)
+
+
+subsection {* Orders and Lattices where @{text eq} is the Equality *}
+
+locale partial_order = weak_partial_order +
+  assumes eq_is_equal: "op .= = op ="
+begin
+
+declare weak_le_anti_sym [rule del]
+
+lemma le_anti_sym [intro]:
+  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
+  using weak_le_anti_sym unfolding eq_is_equal .
+
+lemma lless_eq:
+  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
+  unfolding lless_def by (simp add: eq_is_equal)
+
+lemma lless_asym:
+  assumes "a \<in> carrier L" "b \<in> carrier L"
+    and "a \<sqsubset> b" "b \<sqsubset> a"
+  shows "P"
+  using assms unfolding lless_eq by auto
+
+lemma lless_trans [trans]:
+  assumes "a \<sqsubset> b" "b \<sqsubset> c"
+    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
+  shows "a \<sqsubset> c"
+  using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
+
+end
+
+
+subsubsection {* Upper and lower bounds of a set *}
+
+(* all relevant lemmas are global and already proved above *)
+
+
+subsubsection {* Least and greatest, as predicate *}
+
+lemma (in partial_order) least_unique:
+  "[| least L x A; least L y A |] ==> x = y"
+  using weak_least_unique unfolding eq_is_equal .
+
+lemma (in partial_order) greatest_unique:
+  "[| greatest L x A; greatest L y A |] ==> x = y"
+  using weak_greatest_unique unfolding eq_is_equal .
+
+
+subsection {* Lattices *}
+
+locale upper_semilattice = partial_order +
+  assumes sup_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
+
+interpretation upper_semilattice < weak_upper_semilattice
+  by unfold_locales (rule sup_of_two_exists)
+
+locale lower_semilattice = partial_order +
+  assumes inf_of_two_exists:
+    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
+
+interpretation lower_semilattice < weak_lower_semilattice
+  by unfold_locales (rule inf_of_two_exists)
+
+locale lattice = upper_semilattice + lower_semilattice
+
+
+subsubsection {* Supremum *}
+
+context partial_order begin
+
+declare weak_sup_of_singleton [simp del]
+
+lemma sup_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Squnion>{x} = x"
+  using weak_sup_of_singleton unfolding eq_is_equal .
+
+end
+
+context upper_semilattice begin
+
+lemma join_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
+  using weak_join_assoc_lemma unfolding eq_is_equal .
+
+end
+
+lemma (in upper_semilattice) join_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
+  using weak_join_assoc unfolding eq_is_equal .
+
+
+subsubsection {* Infimum *}
+
+context partial_order begin
+
+declare weak_inf_of_singleton [simp del]
+
+lemma inf_of_singleton [simp]:
+  "x \<in> carrier L ==> \<Sqinter>{x} = x"
+  using weak_inf_of_singleton unfolding eq_is_equal .
+
+end
+
+context lower_semilattice begin
+
+text {* Condition on @{text A}: infimum exists. *}
+
+lemma meet_assoc_lemma:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
+  using weak_meet_assoc_lemma unfolding eq_is_equal .
+
+end
+
+lemma (in lower_semilattice) meet_assoc:
+  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
+  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
+  using weak_meet_assoc unfolding eq_is_equal .
+
+
+subsection {* Total Orders *}
+
+locale total_order = partial_order +
+  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+
+interpretation total_order < weak_total_order
+  by unfold_locales (rule total)
+
+text {* Introduction rule: the usual definition of total order *}
+
+lemma (in partial_order) total_orderI:
+  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
+  shows "total_order L"
+  by unfold_locales (rule total)
+
+text {* Total orders are lattices. *}
+
+interpretation total_order < lattice
+  by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
+
+
+subsection {* Complete lattices *}
+
+locale complete_lattice = lattice +
+  assumes sup_exists:
+    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+
+interpretation complete_lattice < weak_complete_lattice
+  by unfold_locales (auto intro: sup_exists inf_exists)
+
+text {* Introduction rule: the usual definition of complete lattice *}
+
+lemma (in partial_order) complete_latticeI:
+  assumes sup_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
+    and inf_exists:
+    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
+  shows "complete_lattice L"
+  by unfold_locales (auto intro: sup_exists inf_exists)
+
 theorem (in partial_order) complete_lattice_criterion1:
   assumes top_exists: "EX g. greatest L g (carrier L)"
     and inf_exists:
@@ -803,7 +1266,7 @@
    apply (rule greatest_le [where A = "Lower L ?B"])
     apply (rule b_inf_B)
    apply (rule Lower_memI)
-    apply (erule Upper_memD)
+    apply (erule Upper_memD [THEN conjunct1])
      apply assumption
     apply (rule L)
    apply (fast intro: L [THEN subsetD])
@@ -834,11 +1297,11 @@
 subsubsection {* Powerset of a Set is a Complete Lattice *}
 
 theorem powerset_is_complete_lattice:
-  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
+  "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
   (is "complete_lattice ?L")
 proof (rule partial_order.complete_latticeI)
   show "partial_order ?L"
-    by (rule partial_order.intro) auto
+    by unfold_locales auto
 next
   fix B
   assume B: "B \<subseteq> carrier ?L"
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/Algebra/ROOT.ML
--- a/src/HOL/Algebra/ROOT.ML	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Wed Jul 30 19:03:33 2008 +0200
@@ -5,7 +5,7 @@
 *)
 
 (* Preliminaries from set and number theory *)
-no_document use_thys ["FuncSet", "Primes", "Binomial"];
+no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
 
 
 (*** New development, based on explicit structures ***)
@@ -17,8 +17,9 @@
   "Bij",                (* Automorphism Groups *)
 
   (* Rings *)
-  "UnivPoly",           (* Rings and polynomials *)
-  "IntRing"             (* Ideals and residue classes *)
+  "Divisibility",       (* Rings *)
+  "IntRing",            (* Ideals and residue classes *)
+  "UnivPoly"            (* Polynomials *)
 ];
 
 
diff -r 007a339b9e7d -r 95b36bfe7fc4 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Jul 30 16:07:00 2008 +0200
+++ b/src/HOL/IsaMakefile	Wed Jul 30 19:03:33 2008 +0200
@@ -509,7 +509,7 @@
   Library/Multiset.thy Library/Permutation.thy Library/Primes.thy	\
   Algebra/AbelCoset.thy Algebra/Bij.thy	Algebra/Congruence.thy		\
   Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy	\
-  Algebra/FiniteProduct.thy Algebra/GLattice.thy			\
+  Algebra/FiniteProduct.thy						\
   Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
   Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
   Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\