New locales for orders and lattices where the equivalence relation is not restricted to equality.
authorballarin
Wed Jul 30 19:03:33 2008 +0200 (2008-07-30)
changeset 2771395b36bfe7fc4
parent 27712 007a339b9e7d
child 27714 27b4d7c01f8b
New locales for orders and lattices where the equivalence relation is not restricted to equality.
NEWS
src/HOL/Algebra/Divisibility.thy
src/HOL/Algebra/GLattice.thy
src/HOL/Algebra/Group.thy
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/ROOT.ML
src/HOL/IsaMakefile
     1.1 --- a/NEWS	Wed Jul 30 16:07:00 2008 +0200
     1.2 +++ b/NEWS	Wed Jul 30 19:03:33 2008 +0200
     1.3 @@ -125,6 +125,13 @@
     1.4  
     1.5  *** HOL-Algebra ***
     1.6  
     1.7 +* New locales for orders and lattices where the equivalence relation
     1.8 +  is not restricted to equality.  INCOMPATIBILITY: all order and
     1.9 +  lattice locales use a record structure with field eq for the
    1.10 +  equivalence.
    1.11 +
    1.12 +* New theory of factorial domains.
    1.13 +
    1.14  * Units_l_inv and Units_r_inv are now simprules by default.
    1.15  INCOMPATIBILITY.  Simplifier proof that require deletion of l_inv
    1.16  and/or r_inv will now also require deletion of these lemmas.
    1.17 @@ -136,8 +143,6 @@
    1.18  greatest_carrier ~> greatest_closed
    1.19  greatest_Lower_above ~> greatest_Lower_below
    1.20  
    1.21 -* New theory of factorial domains.
    1.22 -
    1.23  
    1.24  *** HOL-NSA ***
    1.25  
     2.1 --- a/src/HOL/Algebra/Divisibility.thy	Wed Jul 30 16:07:00 2008 +0200
     2.2 +++ b/src/HOL/Algebra/Divisibility.thy	Wed Jul 30 19:03:33 2008 +0200
     2.3 @@ -2,11 +2,12 @@
     2.4    Title:     Divisibility in monoids and rings
     2.5    Id:        $Id$
     2.6    Author:    Clemens Ballarin, started 18 July 2008
     2.7 -  Copyright: Clemens Ballarin
     2.8 +
     2.9 +Based on work by Stefan Hohe.
    2.10  *)
    2.11  
    2.12  theory Divisibility
    2.13 -imports Permutation Coset Group GLattice
    2.14 +imports Permutation Coset Group
    2.15  begin
    2.16  
    2.17  subsection {* Monoid with cancelation law *}
    2.18 @@ -490,8 +491,8 @@
    2.19         show "x divides y'" by simp
    2.20  qed
    2.21  
    2.22 -lemma (in monoid) division_gpartial_order [simp, intro!]:
    2.23 -  "gpartial_order (division_rel G)"
    2.24 +lemma (in monoid) division_weak_partial_order [simp, intro!]:
    2.25 +  "weak_partial_order (division_rel G)"
    2.26    apply unfold_locales
    2.27    apply simp_all
    2.28    apply (simp add: associated_sym)
    2.29 @@ -731,12 +732,12 @@
    2.30   apply (iprover intro: divides_trans)+
    2.31  done
    2.32  
    2.33 -lemma properfactor_glless:
    2.34 +lemma properfactor_lless:
    2.35    fixes G (structure)
    2.36 -  shows "properfactor G = glless (division_rel G)"
    2.37 +  shows "properfactor G = lless (division_rel G)"
    2.38  apply (rule ext) apply (rule ext) apply rule
    2.39 - apply (fastsimp elim: properfactorE2 intro: gllessI)
    2.40 -apply (fastsimp elim: gllessE intro: properfactorI2)
    2.41 + apply (fastsimp elim: properfactorE2 intro: weak_llessI)
    2.42 +apply (fastsimp elim: weak_llessE intro: properfactorI2)
    2.43  done
    2.44  
    2.45  lemma (in monoid) properfactor_cong_l [trans]:
    2.46 @@ -745,9 +746,9 @@
    2.47      and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
    2.48    shows "properfactor G x' y"
    2.49  using pf
    2.50 -unfolding properfactor_glless
    2.51 +unfolding properfactor_lless
    2.52  proof -
    2.53 -  interpret gpartial_order ["division_rel G"] ..
    2.54 +  interpret weak_partial_order ["division_rel G"] ..
    2.55    from x'x
    2.56         have "x' .=\<^bsub>division_rel G\<^esub> x" by simp
    2.57    also assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
    2.58 @@ -761,9 +762,9 @@
    2.59      and carr: "x \<in> carrier G"  "y \<in> carrier G"  "y' \<in> carrier G"
    2.60    shows "properfactor G x y'"
    2.61  using pf
    2.62 -unfolding properfactor_glless
    2.63 +unfolding properfactor_lless
    2.64  proof -
    2.65 -  interpret gpartial_order ["division_rel G"] ..
    2.66 +  interpret weak_partial_order ["division_rel G"] ..
    2.67    assume "x \<sqsubset>\<^bsub>division_rel G\<^esub> y"
    2.68    also from yy'
    2.69         have "y .=\<^bsub>division_rel G\<^esub> y'" by simp
    2.70 @@ -2630,7 +2631,7 @@
    2.71    "somelcm G a b == SOME x. x \<in> carrier G \<and> x lcmof a b"
    2.72  
    2.73  constdefs (structure G)
    2.74 -  "SomeGcd G A == ginf (division_rel G) A"
    2.75 +  "SomeGcd G A == inf (division_rel G) A"
    2.76  
    2.77  
    2.78  locale gcd_condition_monoid = comm_monoid_cancel +
    2.79 @@ -2648,12 +2649,12 @@
    2.80  
    2.81  subsubsection {* Connections to \texttt{Lattice.thy} *}
    2.82  
    2.83 -lemma gcdof_ggreatestLower:
    2.84 +lemma gcdof_greatestLower:
    2.85    fixes G (structure)
    2.86    assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
    2.87    shows "(x \<in> carrier G \<and> x gcdof a b) =
    2.88 -         ggreatest (division_rel G) x (Lower (division_rel G) {a, b})"
    2.89 -unfolding isgcd_def ggreatest_def Lower_def elem_def
    2.90 +         greatest (division_rel G) x (Lower (division_rel G) {a, b})"
    2.91 +unfolding isgcd_def greatest_def Lower_def elem_def
    2.92  proof (simp, safe)
    2.93    fix xa
    2.94    assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> xa divides x"
    2.95 @@ -2674,12 +2675,12 @@
    2.96         by (fast intro: r1)
    2.97  qed (simp, simp)
    2.98  
    2.99 -lemma lcmof_gleastUpper:
   2.100 +lemma lcmof_leastUpper:
   2.101    fixes G (structure)
   2.102    assumes carr[simp]: "a \<in> carrier G"  "b \<in> carrier G"
   2.103    shows "(x \<in> carrier G \<and> x lcmof a b) =
   2.104 -         gleast (division_rel G) x (Upper (division_rel G) {a, b})"
   2.105 -unfolding islcm_def gleast_def Upper_def elem_def
   2.106 +         least (division_rel G) x (Upper (division_rel G) {a, b})"
   2.107 +unfolding islcm_def least_def Upper_def elem_def
   2.108  proof (simp, safe)
   2.109    fix xa
   2.110    assume r1[rule_format]: "\<forall>x. (x = a \<or> x = b) \<and> x \<in> carrier G \<longrightarrow> x divides xa"
   2.111 @@ -2700,12 +2701,12 @@
   2.112         by (fast intro: r1)
   2.113  qed (simp, simp)
   2.114  
   2.115 -lemma somegcd_gmeet:
   2.116 +lemma somegcd_meet:
   2.117    fixes G (structure)
   2.118    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.119 -  shows "somegcd G a b = gmeet (division_rel G) a b"
   2.120 -unfolding somegcd_def gmeet_def ginf_def
   2.121 -by (simp add: gcdof_ggreatestLower[OF carr])
   2.122 +  shows "somegcd G a b = meet (division_rel G) a b"
   2.123 +unfolding somegcd_def meet_def inf_def
   2.124 +by (simp add: gcdof_greatestLower[OF carr])
   2.125  
   2.126  lemma (in monoid) isgcd_divides_l:
   2.127    assumes "a divides b"
   2.128 @@ -2910,10 +2911,10 @@
   2.129  
   2.130  subsubsection {* Gcd condition *}
   2.131  
   2.132 -lemma (in gcd_condition_monoid) division_glower_semilattice [simp]:
   2.133 -  shows "glower_semilattice (division_rel G)"
   2.134 +lemma (in gcd_condition_monoid) division_weak_lower_semilattice [simp]:
   2.135 +  shows "weak_lower_semilattice (division_rel G)"
   2.136  proof -
   2.137 -  interpret gpartial_order ["division_rel G"] ..
   2.138 +  interpret weak_partial_order ["division_rel G"] ..
   2.139    show ?thesis
   2.140    apply (unfold_locales, simp_all)
   2.141    proof -
   2.142 @@ -2925,9 +2926,9 @@
   2.143          and isgcd: "z gcdof x y"
   2.144          by auto
   2.145      with carr
   2.146 -    have "ggreatest (division_rel G) z (Lower (division_rel G) {x, y})"
   2.147 -        by (subst gcdof_ggreatestLower[symmetric], simp+)
   2.148 -    thus "\<exists>z. ggreatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
   2.149 +    have "greatest (division_rel G) z (Lower (division_rel G) {x, y})"
   2.150 +        by (subst gcdof_greatestLower[symmetric], simp+)
   2.151 +    thus "\<exists>z. greatest (division_rel G) z (Lower (division_rel G) {x, y})" by fast
   2.152    qed
   2.153  qed
   2.154  
   2.155 @@ -2938,15 +2939,15 @@
   2.156    shows "a' gcdof b c"
   2.157  proof -
   2.158    note carr = a'carr carr'
   2.159 -  interpret glower_semilattice ["division_rel G"] by simp
   2.160 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.161    have "a' \<in> carrier G \<and> a' gcdof b c"
   2.162 -    apply (simp add: gcdof_ggreatestLower carr')
   2.163 -    apply (subst ggreatest_Lower_cong_l[of _ a])
   2.164 +    apply (simp add: gcdof_greatestLower carr')
   2.165 +    apply (subst greatest_Lower_cong_l[of _ a])
   2.166         apply (simp add: a'a)
   2.167        apply (simp add: carr)
   2.168       apply (simp add: carr)
   2.169      apply (simp add: carr)
   2.170 -    apply (simp add: gcdof_ggreatestLower[symmetric] agcd carr)
   2.171 +    apply (simp add: gcdof_greatestLower[symmetric] agcd carr)
   2.172    done
   2.173    thus ?thesis ..
   2.174  qed
   2.175 @@ -2955,10 +2956,10 @@
   2.176    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.177    shows "somegcd G a b \<in> carrier G"
   2.178  proof -
   2.179 -  interpret glower_semilattice ["division_rel G"] by simp
   2.180 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.181    show ?thesis
   2.182 -    apply (simp add: somegcd_gmeet[OF carr])
   2.183 -    apply (rule gmeet_closed[simplified], fact+)
   2.184 +    apply (simp add: somegcd_meet[OF carr])
   2.185 +    apply (rule meet_closed[simplified], fact+)
   2.186    done
   2.187  qed
   2.188  
   2.189 @@ -2966,12 +2967,12 @@
   2.190    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.191    shows "(somegcd G a b) gcdof a b"
   2.192  proof -
   2.193 -  interpret glower_semilattice ["division_rel G"] by simp
   2.194 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.195    from carr
   2.196    have "somegcd G a b \<in> carrier G \<and> (somegcd G a b) gcdof a b"
   2.197 -    apply (subst gcdof_ggreatestLower, simp, simp)
   2.198 -    apply (simp add: somegcd_gmeet[OF carr] gmeet_def)
   2.199 -    apply (rule ginf_of_two_ggreatest[simplified], assumption+)
   2.200 +    apply (subst gcdof_greatestLower, simp, simp)
   2.201 +    apply (simp add: somegcd_meet[OF carr] meet_def)
   2.202 +    apply (rule inf_of_two_greatest[simplified], assumption+)
   2.203    done
   2.204    thus "(somegcd G a b) gcdof a b" by simp
   2.205  qed
   2.206 @@ -2980,10 +2981,10 @@
   2.207    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.208    shows "\<exists>x\<in>carrier G. x = somegcd G a b"
   2.209  proof -
   2.210 -  interpret glower_semilattice ["division_rel G"] by simp
   2.211 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.212    show ?thesis
   2.213 -    apply (simp add: somegcd_gmeet[OF carr])
   2.214 -    apply (rule gmeet_closed[simplified], fact+)
   2.215 +    apply (simp add: somegcd_meet[OF carr])
   2.216 +    apply (rule meet_closed[simplified], fact+)
   2.217    done
   2.218  qed
   2.219  
   2.220 @@ -2991,10 +2992,10 @@
   2.221    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.222    shows "(somegcd G a b) divides a"
   2.223  proof -
   2.224 -  interpret glower_semilattice ["division_rel G"] by simp
   2.225 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.226    show ?thesis
   2.227 -    apply (simp add: somegcd_gmeet[OF carr])
   2.228 -    apply (rule gmeet_left[simplified], fact+)
   2.229 +    apply (simp add: somegcd_meet[OF carr])
   2.230 +    apply (rule meet_left[simplified], fact+)
   2.231    done
   2.232  qed
   2.233  
   2.234 @@ -3002,10 +3003,10 @@
   2.235    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"
   2.236    shows "(somegcd G a b) divides b"
   2.237  proof -
   2.238 -  interpret glower_semilattice ["division_rel G"] by simp
   2.239 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.240    show ?thesis
   2.241 -    apply (simp add: somegcd_gmeet[OF carr])
   2.242 -    apply (rule gmeet_right[simplified], fact+)
   2.243 +    apply (simp add: somegcd_meet[OF carr])
   2.244 +    apply (rule meet_right[simplified], fact+)
   2.245    done
   2.246  qed
   2.247  
   2.248 @@ -3014,10 +3015,10 @@
   2.249      and L: "x \<in> carrier G"  "y \<in> carrier G"  "z \<in> carrier G"
   2.250    shows "z divides (somegcd G x y)"
   2.251  proof -
   2.252 -  interpret glower_semilattice ["division_rel G"] by simp
   2.253 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.254    show ?thesis
   2.255 -    apply (simp add: somegcd_gmeet L)
   2.256 -    apply (rule gmeet_le[simplified], fact+)
   2.257 +    apply (simp add: somegcd_meet L)
   2.258 +    apply (rule meet_le[simplified], fact+)
   2.259    done
   2.260  qed
   2.261  
   2.262 @@ -3026,10 +3027,10 @@
   2.263      and carr: "x \<in> carrier G"  "x' \<in> carrier G"  "y \<in> carrier G"
   2.264    shows "somegcd G x y \<sim> somegcd G x' y"
   2.265  proof -
   2.266 -  interpret glower_semilattice ["division_rel G"] by simp
   2.267 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.268    show ?thesis
   2.269 -    apply (simp add: somegcd_gmeet carr)
   2.270 -    apply (rule gmeet_cong_l[simplified], fact+)
   2.271 +    apply (simp add: somegcd_meet carr)
   2.272 +    apply (rule meet_cong_l[simplified], fact+)
   2.273    done
   2.274  qed
   2.275  
   2.276 @@ -3038,10 +3039,10 @@
   2.277      and yy': "y \<sim> y'"
   2.278    shows "somegcd G x y \<sim> somegcd G x y'"
   2.279  proof -
   2.280 -  interpret glower_semilattice ["division_rel G"] by simp
   2.281 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.282    show ?thesis
   2.283 -    apply (simp add: somegcd_gmeet carr)
   2.284 -    apply (rule gmeet_cong_r[simplified], fact+)
   2.285 +    apply (simp add: somegcd_meet carr)
   2.286 +    apply (rule meet_cong_r[simplified], fact+)
   2.287    done
   2.288  qed
   2.289  
   2.290 @@ -3089,10 +3090,10 @@
   2.291    assumes "finite A"  "A \<subseteq> carrier G"  "A \<noteq> {}"
   2.292    shows "\<exists>x\<in> carrier G. x = SomeGcd G A"
   2.293  proof -
   2.294 -  interpret glower_semilattice ["division_rel G"] by simp
   2.295 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.296    show ?thesis
   2.297      apply (simp add: SomeGcd_def)
   2.298 -    apply (rule finite_ginf_closed[simplified], fact+)
   2.299 +    apply (rule finite_inf_closed[simplified], fact+)
   2.300    done
   2.301  qed
   2.302  
   2.303 @@ -3100,11 +3101,11 @@
   2.304    assumes carr: "a \<in> carrier G"  "b \<in> carrier G"  "c \<in> carrier G"
   2.305    shows "somegcd G (somegcd G a b) c \<sim> somegcd G a (somegcd G b c)"
   2.306  proof -
   2.307 -  interpret glower_semilattice ["division_rel G"] by simp
   2.308 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.309    show ?thesis
   2.310 -    apply (subst (2 3) somegcd_gmeet, (simp add: carr)+)
   2.311 -    apply (simp add: somegcd_gmeet carr)
   2.312 -    apply (rule gmeet_assoc[simplified], fact+)
   2.313 +    apply (subst (2 3) somegcd_meet, (simp add: carr)+)
   2.314 +    apply (simp add: somegcd_meet carr)
   2.315 +    apply (rule weak_meet_assoc[simplified], fact+)
   2.316    done
   2.317  qed
   2.318  
   2.319 @@ -3866,12 +3867,12 @@
   2.320  interpretation factorial_monoid \<subseteq> gcd_condition_monoid
   2.321    by (unfold_locales, rule gcdof_exists)
   2.322  
   2.323 -lemma (in factorial_monoid) division_glattice [simp]:
   2.324 -  shows "glattice (division_rel G)"
   2.325 +lemma (in factorial_monoid) division_weak_lattice [simp]:
   2.326 +  shows "weak_lattice (division_rel G)"
   2.327  proof -
   2.328 -  interpret glower_semilattice ["division_rel G"] by simp
   2.329 -
   2.330 -  show "glattice (division_rel G)"
   2.331 +  interpret weak_lower_semilattice ["division_rel G"] by simp
   2.332 +
   2.333 +  show "weak_lattice (division_rel G)"
   2.334    apply (unfold_locales, simp_all)
   2.335    proof -
   2.336      fix x y
   2.337 @@ -3883,9 +3884,9 @@
   2.338          and isgcd: "z lcmof x y"
   2.339          by auto
   2.340      with carr
   2.341 -    have "gleast (division_rel G) z (Upper (division_rel G) {x, y})"
   2.342 -        by (simp add: lcmof_gleastUpper[symmetric])
   2.343 -    thus "\<exists>z. gleast (division_rel G) z (Upper (division_rel G) {x, y})" by fast
   2.344 +    have "least (division_rel G) z (Upper (division_rel G) {x, y})"
   2.345 +        by (simp add: lcmof_leastUpper[symmetric])
   2.346 +    thus "\<exists>z. least (division_rel G) z (Upper (division_rel G) {x, y})" by fast
   2.347    qed
   2.348  qed
   2.349  
     3.1 --- a/src/HOL/Algebra/GLattice.thy	Wed Jul 30 16:07:00 2008 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,1181 +0,0 @@
     3.4 -(*
     3.5 -  Title:     HOL/Algebra/Lattice.thy
     3.6 -  Id:        $Id$
     3.7 -  Author:    Clemens Ballarin, started 7 November 2003
     3.8 -  Copyright: Clemens Ballarin
     3.9 -*)
    3.10 -
    3.11 -theory GLattice imports Congruence begin
    3.12 -
    3.13 -(* FIXME: unify with Lattice.thy *)
    3.14 -
    3.15 -
    3.16 -section {* Orders and Lattices *}
    3.17 -
    3.18 -subsection {* Partial Orders *}
    3.19 -
    3.20 -record 'a gorder = "'a eq_object" +
    3.21 -  le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    3.22 -
    3.23 -locale gpartial_order = equivalence L +
    3.24 -  assumes le_refl [intro, simp]:
    3.25 -      "x \<in> carrier L ==> x \<sqsubseteq> x"
    3.26 -    and le_anti_sym [intro]:
    3.27 -      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    3.28 -    and le_trans [trans]:
    3.29 -      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    3.30 -    and le_cong:
    3.31 -      "\<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"
    3.32 -
    3.33 -constdefs (structure L)
    3.34 -  glless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    3.35 -  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
    3.36 -
    3.37 -
    3.38 -subsubsection {* The order relation *}
    3.39 -
    3.40 -context gpartial_order begin
    3.41 -
    3.42 -lemma le_cong_l [intro, trans]:
    3.43 -  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    3.44 -  by (auto intro: le_cong [THEN iffD2])
    3.45 -
    3.46 -lemma le_cong_r [intro, trans]:
    3.47 -  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    3.48 -  by (auto intro: le_cong [THEN iffD1])
    3.49 -
    3.50 -lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    3.51 -  by (simp add: le_cong_l)
    3.52 -
    3.53 -end
    3.54 -
    3.55 -lemma gllessI:
    3.56 -  fixes R (structure)
    3.57 -  assumes "x \<sqsubseteq> y" and "~(x .= y)"
    3.58 -  shows "x \<sqsubset> y"
    3.59 -  using assms
    3.60 -  unfolding glless_def
    3.61 -  by simp
    3.62 -
    3.63 -lemma gllessD1:
    3.64 -  fixes R (structure)
    3.65 -  assumes "x \<sqsubset> y"
    3.66 -  shows "x \<sqsubseteq> y"
    3.67 -  using assms
    3.68 -  unfolding glless_def
    3.69 -  by simp
    3.70 -
    3.71 -lemma gllessD2:
    3.72 -  fixes R (structure)
    3.73 -  assumes "x \<sqsubset> y"
    3.74 -  shows "\<not> (x .= y)"
    3.75 -  using assms
    3.76 -  unfolding glless_def
    3.77 -  by simp
    3.78 -
    3.79 -lemma gllessE:
    3.80 -  fixes R (structure)
    3.81 -  assumes p: "x \<sqsubset> y"
    3.82 -    and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    3.83 -  shows "P"
    3.84 -  using p
    3.85 -  by (blast dest: gllessD1 gllessD2 e)
    3.86 -
    3.87 -(*
    3.88 -lemma (in gpartial_order) lless_cong_l [trans]:
    3.89 -  assumes xx': "x \<doteq> x'"
    3.90 -    and xy: "x' \<sqsubset> y"
    3.91 -    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    3.92 -  shows "x \<sqsubseteq> y"
    3.93 -using xy
    3.94 -unfolding lless_def
    3.95 -proof clarify
    3.96 -  note xx'
    3.97 -  also assume "x' \<sqsubseteq> y"
    3.98 -  finally show "x \<sqsubseteq> y" by (simp add: carr)
    3.99 -qed
   3.100 -*)
   3.101 -
   3.102 -lemma (in gpartial_order) glless_cong_l [trans]:
   3.103 -  assumes xx': "x .= x'"
   3.104 -    and xy: "x' \<sqsubset> y"
   3.105 -    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   3.106 -  shows "x \<sqsubset> y"
   3.107 -  using assms
   3.108 -  apply (elim gllessE, intro gllessI)
   3.109 -  apply (iprover intro: le_cong_l)
   3.110 -  apply (iprover intro: trans sym)
   3.111 -  done
   3.112 -
   3.113 -(*
   3.114 -lemma (in gpartial_order) lless_cong_r:
   3.115 -  assumes xy: "x \<sqsubset> y"
   3.116 -    and  yy': "y \<doteq> y'"
   3.117 -    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   3.118 -  shows "x \<sqsubseteq> y'"
   3.119 -using xy
   3.120 -unfolding lless_def
   3.121 -proof clarify
   3.122 -  assume "x \<sqsubseteq> y"
   3.123 -  also note yy'
   3.124 -  finally show "x \<sqsubseteq> y'" by (simp add: carr)
   3.125 -qed
   3.126 -*)
   3.127 -
   3.128 -lemma (in gpartial_order) glless_cong_r [trans]:
   3.129 -  assumes xy: "x \<sqsubset> y"
   3.130 -    and  yy': "y .= y'"
   3.131 -    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   3.132 -  shows "x \<sqsubset> y'"
   3.133 -  using assms
   3.134 -  apply (elim gllessE, intro gllessI)
   3.135 -  apply (iprover intro: le_cong_r)
   3.136 -  apply (iprover intro: trans sym)
   3.137 -  done
   3.138 -
   3.139 -(*
   3.140 -lemma (in gpartial_order) glless_antisym:
   3.141 -  assumes "a \<in> carrier L" "b \<in> carrier L"
   3.142 -    and "a \<sqsubset> b" "b \<sqsubset> a"
   3.143 -  shows "a \<doteq> b"
   3.144 -  using assms
   3.145 -  by (elim gllessE) (rule gle_anti_sym)
   3.146 -
   3.147 -lemma (in gpartial_order) glless_trans [trans]:
   3.148 -  assumes "a .\<sqsubset> b" "b .\<sqsubset> c"
   3.149 -    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   3.150 -  shows "a .\<sqsubset> c"
   3.151 -using assms
   3.152 -apply (elim gllessE, intro gllessI)
   3.153 - apply (iprover dest: le_trans)
   3.154 -proof (rule ccontr, simp)
   3.155 -  assume ab: "a \<sqsubseteq> b" and bc: "b \<sqsubseteq> c"
   3.156 -    and ac: "a \<doteq> c"
   3.157 -    and nbc: "\<not> b \<doteq> c"
   3.158 -  note ac[symmetric]
   3.159 -  also note ab
   3.160 -  finally have "c \<sqsubseteq> b" by simp
   3.161 -  with bc have "b \<doteq> c" by (iprover intro: gle_anti_sym carr)
   3.162 -  with nbc
   3.163 -      show "False" by simp
   3.164 -qed
   3.165 -*)
   3.166 -
   3.167 -subsubsection {* Upper and lower bounds of a set *}
   3.168 -
   3.169 -constdefs (structure L)
   3.170 -  Upper :: "[_, 'a set] => 'a set"
   3.171 -  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
   3.172 -
   3.173 -  Lower :: "[_, 'a set] => 'a set"
   3.174 -  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
   3.175 -
   3.176 -lemma Upper_closed [intro!, simp]:
   3.177 -  "Upper L A \<subseteq> carrier L"
   3.178 -  by (unfold Upper_def) clarify
   3.179 -
   3.180 -lemma Upper_memD [dest]:
   3.181 -  fixes L (structure)
   3.182 -  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   3.183 -  by (unfold Upper_def) blast
   3.184 -
   3.185 -lemma (in gpartial_order) Upper_elemD [dest]:
   3.186 -  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   3.187 -  unfolding Upper_def elem_def
   3.188 -  by (blast dest: sym)
   3.189 -
   3.190 -lemma Upper_memI:
   3.191 -  fixes L (structure)
   3.192 -  shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   3.193 -  by (unfold Upper_def) blast
   3.194 -
   3.195 -lemma (in gpartial_order) Upper_elemI:
   3.196 -  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   3.197 -  unfolding Upper_def by blast
   3.198 -
   3.199 -lemma Upper_antimono:
   3.200 -  "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   3.201 -  by (unfold Upper_def) blast
   3.202 -
   3.203 -lemma (in gpartial_order) Upper_is_closed [simp]:
   3.204 -  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   3.205 -  by (rule is_closedI) (blast intro: Upper_memI)+
   3.206 -
   3.207 -lemma (in gpartial_order) Upper_mem_cong:
   3.208 -  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   3.209 -    and aa': "a .= a'"
   3.210 -    and aelem: "a \<in> Upper L A"
   3.211 -  shows "a' \<in> Upper L A"
   3.212 -proof (rule Upper_memI[OF _ a'carr])
   3.213 -  fix y
   3.214 -  assume yA: "y \<in> A"
   3.215 -  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   3.216 -  also note aa'
   3.217 -  finally
   3.218 -      show "y \<sqsubseteq> a'"
   3.219 -      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   3.220 -qed
   3.221 -
   3.222 -lemma (in gpartial_order) Upper_cong:
   3.223 -  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   3.224 -    and AA': "A {.=} A'"
   3.225 -  shows "Upper L A = Upper L A'"
   3.226 -unfolding Upper_def
   3.227 -apply rule
   3.228 - apply (rule, clarsimp) defer 1
   3.229 - apply (rule, clarsimp) defer 1
   3.230 -proof -
   3.231 -  fix x a'
   3.232 -  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   3.233 -    and a'A': "a' \<in> A'"
   3.234 -  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   3.235 -
   3.236 -  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   3.237 -  from this obtain a
   3.238 -      where aA: "a \<in> A"
   3.239 -      and a'a: "a' .= a"
   3.240 -      by auto
   3.241 -  note [simp] = subsetD[OF Acarr aA] carr
   3.242 -
   3.243 -  note a'a
   3.244 -  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   3.245 -  finally show "a' \<sqsubseteq> x" by simp
   3.246 -next
   3.247 -  fix x a
   3.248 -  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   3.249 -    and aA: "a \<in> A"
   3.250 -  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   3.251 -
   3.252 -  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   3.253 -  from this obtain a'
   3.254 -      where a'A': "a' \<in> A'"
   3.255 -      and aa': "a .= a'"
   3.256 -      by auto
   3.257 -  note [simp] = subsetD[OF A'carr a'A'] carr
   3.258 -
   3.259 -  note aa'
   3.260 -  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   3.261 -  finally show "a \<sqsubseteq> x" by simp
   3.262 -qed
   3.263 -
   3.264 -lemma Lower_closed [intro!, simp]:
   3.265 -  "Lower L A \<subseteq> carrier L"
   3.266 -  by (unfold Lower_def) clarify
   3.267 -
   3.268 -lemma Lower_memD [dest]:
   3.269 -  fixes L (structure)
   3.270 -  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   3.271 -  by (unfold Lower_def) blast
   3.272 -
   3.273 -lemma Lower_memI:
   3.274 -  fixes L (structure)
   3.275 -  shows "[| !! y. y \<in> A ==> x \<sqsubseteq> y; x \<in> carrier L |] ==> x \<in> Lower L A"
   3.276 -  by (unfold Lower_def) blast
   3.277 -
   3.278 -lemma Lower_antimono:
   3.279 -  "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   3.280 -  by (unfold Lower_def) blast
   3.281 -
   3.282 -lemma (in gpartial_order) Lower_is_closed [simp]:
   3.283 -  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   3.284 -  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   3.285 -
   3.286 -lemma (in gpartial_order) Lower_mem_cong:
   3.287 -  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   3.288 -    and aa': "a .= a'"
   3.289 -    and aelem: "a \<in> Lower L A"
   3.290 -  shows "a' \<in> Lower L A"
   3.291 -using assms Lower_closed[of L A]
   3.292 -by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   3.293 -
   3.294 -lemma (in gpartial_order) Lower_cong:
   3.295 -  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   3.296 -    and AA': "A {.=} A'"
   3.297 -  shows "Lower L A = Lower L A'"
   3.298 -using Lower_memD[of y]
   3.299 -unfolding Lower_def
   3.300 -apply safe
   3.301 - apply clarsimp defer 1
   3.302 - apply clarsimp defer 1
   3.303 -proof -
   3.304 -  fix x a'
   3.305 -  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   3.306 -    and a'A': "a' \<in> A'"
   3.307 -  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   3.308 -  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   3.309 -
   3.310 -  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   3.311 -  from this obtain a
   3.312 -      where aA: "a \<in> A"
   3.313 -      and a'a: "a' .= a"
   3.314 -      by auto
   3.315 -
   3.316 -  from aA and subsetD[OF Acarr aA]
   3.317 -      have "x \<sqsubseteq> a" by (rule aLxCond)
   3.318 -  also note a'a[symmetric]
   3.319 -  finally
   3.320 -      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   3.321 -next
   3.322 -  fix x a
   3.323 -  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   3.324 -    and aA: "a \<in> A"
   3.325 -  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   3.326 -  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   3.327 -
   3.328 -  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   3.329 -  from this obtain a'
   3.330 -      where a'A': "a' \<in> A'"
   3.331 -      and aa': "a .= a'"
   3.332 -      by auto
   3.333 -  from a'A' and subsetD[OF A'carr a'A']
   3.334 -      have "x \<sqsubseteq> a'" by (rule a'LxCond)
   3.335 -  also note aa'[symmetric]
   3.336 -  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   3.337 -qed
   3.338 -
   3.339 -
   3.340 -subsubsection {* Least and greatest, as predicate *}
   3.341 -
   3.342 -constdefs (structure L)
   3.343 -  gleast :: "[_, 'a, 'a set] => bool"
   3.344 -  "gleast L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
   3.345 -
   3.346 -  ggreatest :: "[_, 'a, 'a set] => bool"
   3.347 -  "ggreatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
   3.348 -
   3.349 -lemma gleast_closed [intro, simp]:
   3.350 -  "gleast L l A ==> l \<in> carrier L"
   3.351 -  by (unfold gleast_def) fast
   3.352 -
   3.353 -lemma gleast_mem:
   3.354 -  "gleast L l A ==> l \<in> A"
   3.355 -  by (unfold gleast_def) fast
   3.356 -
   3.357 -lemma (in gpartial_order) gleast_unique:
   3.358 -  "[| gleast L x A; gleast L y A |] ==> x .= y"
   3.359 -  by (unfold gleast_def) blast
   3.360 -
   3.361 -lemma gleast_le:
   3.362 -  fixes L (structure)
   3.363 -  shows "[| gleast L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   3.364 -  by (unfold gleast_def) fast
   3.365 -
   3.366 -lemma (in gpartial_order) gleast_cong:
   3.367 -  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> gleast L x A = gleast L x' A"
   3.368 -  by (unfold gleast_def) (auto dest: sym)
   3.369 -
   3.370 -text {* @{const gleast} is not congruent in the second parameter for 
   3.371 -  @{term [locale=gpartial_order] "A {.=} A'"} *}
   3.372 -
   3.373 -lemma (in gpartial_order) gleast_Upper_cong_l:
   3.374 -  assumes "x .= x'"
   3.375 -    and "x \<in> carrier L" "x' \<in> carrier L"
   3.376 -    and "A \<subseteq> carrier L"
   3.377 -  shows "gleast L x (Upper L A) = gleast L x' (Upper L A)"
   3.378 -  apply (rule gleast_cong) using assms by auto
   3.379 -
   3.380 -lemma (in gpartial_order) gleast_Upper_cong_r:
   3.381 -  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   3.382 -    and AA': "A {.=} A'"
   3.383 -  shows "gleast L x (Upper L A) = gleast L x (Upper L A')"
   3.384 -apply (subgoal_tac "Upper L A = Upper L A'", simp)
   3.385 -by (rule Upper_cong) fact+
   3.386 -
   3.387 -lemma gleast_UpperI:
   3.388 -  fixes L (structure)
   3.389 -  assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   3.390 -    and below: "!! y. y \<in> Upper L A ==> s \<sqsubseteq> y"
   3.391 -    and L: "A \<subseteq> carrier L"  "s \<in> carrier L"
   3.392 -  shows "gleast L s (Upper L A)"
   3.393 -proof -
   3.394 -  have "Upper L A \<subseteq> carrier L" by simp
   3.395 -  moreover from above L have "s \<in> Upper L A" by (simp add: Upper_def)
   3.396 -  moreover from below have "ALL x : Upper L A. s \<sqsubseteq> x" by fast
   3.397 -  ultimately show ?thesis by (simp add: gleast_def)
   3.398 -qed
   3.399 -
   3.400 -lemma gleast_Upper_above:
   3.401 -  fixes L (structure)
   3.402 -  shows "[| gleast L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   3.403 -  by (unfold gleast_def) blast
   3.404 -
   3.405 -lemma ggreatest_closed [intro, simp]:
   3.406 -  "ggreatest L l A ==> l \<in> carrier L"
   3.407 -  by (unfold ggreatest_def) fast
   3.408 -
   3.409 -lemma ggreatest_mem:
   3.410 -  "ggreatest L l A ==> l \<in> A"
   3.411 -  by (unfold ggreatest_def) fast
   3.412 -
   3.413 -lemma (in gpartial_order) ggreatest_unique:
   3.414 -  "[| ggreatest L x A; ggreatest L y A |] ==> x .= y"
   3.415 -  by (unfold ggreatest_def) blast
   3.416 -
   3.417 -lemma ggreatest_le:
   3.418 -  fixes L (structure)
   3.419 -  shows "[| ggreatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   3.420 -  by (unfold ggreatest_def) fast
   3.421 -
   3.422 -lemma (in gpartial_order) ggreatest_cong:
   3.423 -  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   3.424 -  ggreatest L x A = ggreatest L x' A"
   3.425 -  by (unfold ggreatest_def) (auto dest: sym)
   3.426 -
   3.427 -text {* @{const ggreatest} is not congruent in the second parameter for 
   3.428 -  @{term [locale=gpartial_order] "A {.=} A'"} *}
   3.429 -
   3.430 -lemma (in gpartial_order) ggreatest_Lower_cong_l:
   3.431 -  assumes "x .= x'"
   3.432 -    and "x \<in> carrier L" "x' \<in> carrier L"
   3.433 -    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   3.434 -  shows "ggreatest L x (Lower L A) = ggreatest L x' (Lower L A)"
   3.435 -  apply (rule ggreatest_cong) using assms by auto
   3.436 -
   3.437 -lemma (in gpartial_order) ggreatest_Lower_cong_r:
   3.438 -  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   3.439 -    and AA': "A {.=} A'"
   3.440 -  shows "ggreatest L x (Lower L A) = ggreatest L x (Lower L A')"
   3.441 -apply (subgoal_tac "Lower L A = Lower L A'", simp)
   3.442 -by (rule Lower_cong) fact+
   3.443 -
   3.444 -lemma ggreatest_LowerI:
   3.445 -  fixes L (structure)
   3.446 -  assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   3.447 -    and above: "!! y. y \<in> Lower L A ==> y \<sqsubseteq> i"
   3.448 -    and L: "A \<subseteq> carrier L"  "i \<in> carrier L"
   3.449 -  shows "ggreatest L i (Lower L A)"
   3.450 -proof -
   3.451 -  have "Lower L A \<subseteq> carrier L" by simp
   3.452 -  moreover from below L have "i \<in> Lower L A" by (simp add: Lower_def)
   3.453 -  moreover from above have "ALL x : Lower L A. x \<sqsubseteq> i" by fast
   3.454 -  ultimately show ?thesis by (simp add: ggreatest_def)
   3.455 -qed
   3.456 -
   3.457 -lemma ggreatest_Lower_below:
   3.458 -  fixes L (structure)
   3.459 -  shows "[| ggreatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   3.460 -  by (unfold ggreatest_def) blast
   3.461 -
   3.462 -text {* Supremum and infimum *}
   3.463 -
   3.464 -constdefs (structure L)
   3.465 -  gsup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   3.466 -  "\<Squnion>A == SOME x. gleast L x (Upper L A)"
   3.467 -
   3.468 -  ginf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   3.469 -  "\<Sqinter>A == SOME x. ggreatest L x (Lower L A)"
   3.470 -
   3.471 -  gjoin :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   3.472 -  "x \<squnion> y == \<Squnion> {x, y}"
   3.473 -
   3.474 -  gmeet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   3.475 -  "x \<sqinter> y == \<Sqinter> {x, y}"
   3.476 -
   3.477 -
   3.478 -subsection {* Lattices *}
   3.479 -
   3.480 -locale gupper_semilattice = gpartial_order +
   3.481 -  assumes gsup_of_two_exists:
   3.482 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. gleast L s (Upper L {x, y})"
   3.483 -
   3.484 -locale glower_semilattice = gpartial_order +
   3.485 -  assumes ginf_of_two_exists:
   3.486 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. ggreatest L s (Lower L {x, y})"
   3.487 -
   3.488 -locale glattice = gupper_semilattice + glower_semilattice
   3.489 -
   3.490 -
   3.491 -subsubsection {* Supremum *}
   3.492 -
   3.493 -lemma (in gupper_semilattice) gjoinI:
   3.494 -  "[| !!l. gleast L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   3.495 -  ==> P (x \<squnion> y)"
   3.496 -proof (unfold gjoin_def gsup_def)
   3.497 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.498 -    and P: "!!l. gleast L l (Upper L {x, y}) ==> P l"
   3.499 -  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
   3.500 -  with L show "P (SOME l. gleast L l (Upper L {x, y}))"
   3.501 -    by (fast intro: someI2 P)
   3.502 -qed
   3.503 -
   3.504 -lemma (in gupper_semilattice) gjoin_closed [simp]:
   3.505 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   3.506 -  by (rule gjoinI) (rule gleast_closed)
   3.507 -
   3.508 -lemma (in gupper_semilattice) gjoin_cong_l:
   3.509 -  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   3.510 -    and xx': "x .= x'"
   3.511 -  shows "x \<squnion> y .= x' \<squnion> y"
   3.512 -proof (rule gjoinI, rule gjoinI)
   3.513 -  fix a b
   3.514 -  from xx' carr
   3.515 -      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   3.516 -
   3.517 -  assume gleasta: "gleast L a (Upper L {x, y})"
   3.518 -  assume "gleast L b (Upper L {x', y})"
   3.519 -  with carr
   3.520 -      have gleastb: "gleast L b (Upper L {x, y})"
   3.521 -      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
   3.522 -
   3.523 -  from gleasta gleastb
   3.524 -      show "a .= b" by (rule gleast_unique)
   3.525 -qed (rule carr)+
   3.526 -
   3.527 -lemma (in gupper_semilattice) gjoin_cong_r:
   3.528 -  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   3.529 -    and yy': "y .= y'"
   3.530 -  shows "x \<squnion> y .= x \<squnion> y'"
   3.531 -proof (rule gjoinI, rule gjoinI)
   3.532 -  fix a b
   3.533 -  have "{x, y} = {y, x}" by fast
   3.534 -  also from carr yy'
   3.535 -      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   3.536 -  also have "{y', x} = {x, y'}" by fast
   3.537 -  finally
   3.538 -      have seq: "{x, y} {.=} {x, y'}" .
   3.539 -
   3.540 -  assume gleasta: "gleast L a (Upper L {x, y})"
   3.541 -  assume "gleast L b (Upper L {x, y'})"
   3.542 -  with carr
   3.543 -      have gleastb: "gleast L b (Upper L {x, y})"
   3.544 -      by (simp add: gleast_Upper_cong_r[OF _ _ seq])
   3.545 -
   3.546 -  from gleasta gleastb
   3.547 -      show "a .= b" by (rule gleast_unique)
   3.548 -qed (rule carr)+
   3.549 -
   3.550 -lemma (in gpartial_order) gsup_of_singletonI:      (* only reflexivity needed ? *)
   3.551 -  "x \<in> carrier L ==> gleast L x (Upper L {x})"
   3.552 -  by (rule gleast_UpperI) auto
   3.553 -
   3.554 -lemma (in gpartial_order) gsup_of_singleton [simp]:
   3.555 -  "x \<in> carrier L ==> \<Squnion>{x} .= x"
   3.556 -  unfolding gsup_def
   3.557 -  by (rule someI2) (auto intro: gleast_unique gsup_of_singletonI)
   3.558 -
   3.559 -lemma (in gpartial_order) gsup_of_singleton_closed [simp]:
   3.560 -  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   3.561 -  unfolding gsup_def
   3.562 -  by (rule someI2) (auto intro: gsup_of_singletonI)
   3.563 -
   3.564 -text {* Condition on @{text A}: supremum exists. *}
   3.565 -
   3.566 -lemma (in gupper_semilattice) gsup_insertI:
   3.567 -  "[| !!s. gleast L s (Upper L (insert x A)) ==> P s;
   3.568 -  gleast L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   3.569 -  ==> P (\<Squnion>(insert x A))"
   3.570 -proof (unfold gsup_def)
   3.571 -  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.572 -    and P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
   3.573 -    and gleast_a: "gleast L a (Upper L A)"
   3.574 -  from L gleast_a have La: "a \<in> carrier L" by simp
   3.575 -  from L gsup_of_two_exists gleast_a
   3.576 -  obtain s where gleast_s: "gleast L s (Upper L {a, x})" by blast
   3.577 -  show "P (SOME l. gleast L l (Upper L (insert x A)))"
   3.578 -  proof (rule someI2)
   3.579 -    show "gleast L s (Upper L (insert x A))"
   3.580 -    proof (rule gleast_UpperI)
   3.581 -      fix z
   3.582 -      assume "z \<in> insert x A"
   3.583 -      then show "z \<sqsubseteq> s"
   3.584 -      proof
   3.585 -        assume "z = x" then show ?thesis
   3.586 -          by (simp add: gleast_Upper_above [OF gleast_s] L La)
   3.587 -      next
   3.588 -        assume "z \<in> A"
   3.589 -        with L gleast_s gleast_a show ?thesis
   3.590 -          by (rule_tac le_trans [where y = a]) (auto dest: gleast_Upper_above)
   3.591 -      qed
   3.592 -    next
   3.593 -      fix y
   3.594 -      assume y: "y \<in> Upper L (insert x A)"
   3.595 -      show "s \<sqsubseteq> y"
   3.596 -      proof (rule gleast_le [OF gleast_s], rule Upper_memI)
   3.597 -	fix z
   3.598 -	assume z: "z \<in> {a, x}"
   3.599 -	then show "z \<sqsubseteq> y"
   3.600 -	proof
   3.601 -          have y': "y \<in> Upper L A"
   3.602 -            apply (rule subsetD [where A = "Upper L (insert x A)"])
   3.603 -             apply (rule Upper_antimono)
   3.604 -	     apply blast
   3.605 -	    apply (rule y)
   3.606 -            done
   3.607 -          assume "z = a"
   3.608 -          with y' gleast_a show ?thesis by (fast dest: gleast_le)
   3.609 -	next
   3.610 -	  assume "z \<in> {x}"  (* FIXME "z = x"; declare specific elim rule for "insert x {}" (!?) *)
   3.611 -          with y L show ?thesis by blast
   3.612 -	qed
   3.613 -      qed (rule Upper_closed [THEN subsetD, OF y])
   3.614 -    next
   3.615 -      from L show "insert x A \<subseteq> carrier L" by simp
   3.616 -      from gleast_s show "s \<in> carrier L" by simp
   3.617 -    qed
   3.618 -  qed (rule P)
   3.619 -qed
   3.620 -
   3.621 -lemma (in gupper_semilattice) finite_gsup_gleast:
   3.622 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> gleast L (\<Squnion>A) (Upper L A)"
   3.623 -proof (induct set: finite)
   3.624 -  case empty
   3.625 -  then show ?case by simp
   3.626 -next
   3.627 -  case (insert x A)
   3.628 -  show ?case
   3.629 -  proof (cases "A = {}")
   3.630 -    case True
   3.631 -    with insert show ?thesis
   3.632 -      by simp (simp add: gleast_cong [OF gsup_of_singleton]
   3.633 -	gsup_of_singleton_closed gsup_of_singletonI)
   3.634 -	(* The above step is hairy; gleast_cong can make simp loop.
   3.635 -	Would want special version of simp to apply gleast_cong. *)
   3.636 -  next
   3.637 -    case False
   3.638 -    with insert have "gleast L (\<Squnion>A) (Upper L A)" by simp
   3.639 -    with _ show ?thesis
   3.640 -      by (rule gsup_insertI) (simp_all add: insert [simplified])
   3.641 -  qed
   3.642 -qed
   3.643 -
   3.644 -lemma (in gupper_semilattice) finite_gsup_insertI:
   3.645 -  assumes P: "!!l. gleast L l (Upper L (insert x A)) ==> P l"
   3.646 -    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.647 -  shows "P (\<Squnion> (insert x A))"
   3.648 -proof (cases "A = {}")
   3.649 -  case True with P and xA show ?thesis
   3.650 -    by (simp add: finite_gsup_gleast)
   3.651 -next
   3.652 -  case False with P and xA show ?thesis
   3.653 -    by (simp add: gsup_insertI finite_gsup_gleast)
   3.654 -qed
   3.655 -
   3.656 -lemma (in gupper_semilattice) finite_gsup_closed [simp]:
   3.657 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   3.658 -proof (induct set: finite)
   3.659 -  case empty then show ?case by simp
   3.660 -next
   3.661 -  case insert then show ?case
   3.662 -    by - (rule finite_gsup_insertI, simp_all)
   3.663 -qed
   3.664 -
   3.665 -lemma (in gupper_semilattice) gjoin_left:
   3.666 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   3.667 -  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
   3.668 -
   3.669 -lemma (in gupper_semilattice) gjoin_right:
   3.670 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   3.671 -  by (rule gjoinI [folded gjoin_def]) (blast dest: gleast_mem)
   3.672 -
   3.673 -lemma (in gupper_semilattice) gsup_of_two_gleast:
   3.674 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> gleast L (\<Squnion>{x, y}) (Upper L {x, y})"
   3.675 -proof (unfold gsup_def)
   3.676 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.677 -  with gsup_of_two_exists obtain s where "gleast L s (Upper L {x, y})" by fast
   3.678 -  with L show "gleast L (SOME z. gleast L z (Upper L {x, y})) (Upper L {x, y})"
   3.679 -  by (fast intro: someI2 gleast_unique)  (* blast fails *)
   3.680 -qed
   3.681 -
   3.682 -lemma (in gupper_semilattice) gjoin_le:
   3.683 -  assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   3.684 -    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   3.685 -  shows "x \<squnion> y \<sqsubseteq> z"
   3.686 -proof (rule gjoinI [OF _ x y])
   3.687 -  fix s
   3.688 -  assume "gleast L s (Upper L {x, y})"
   3.689 -  with sub z show "s \<sqsubseteq> z" by (fast elim: gleast_le intro: Upper_memI)
   3.690 -qed
   3.691 -
   3.692 -lemma (in gupper_semilattice) gjoin_assoc_lemma:
   3.693 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.694 -  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
   3.695 -proof (rule finite_gsup_insertI)
   3.696 -  -- {* The textbook argument in Jacobson I, p 457 *}
   3.697 -  fix s
   3.698 -  assume gsup: "gleast L s (Upper L {x, y, z})"
   3.699 -  show "x \<squnion> (y \<squnion> z) .= s"
   3.700 -  proof (rule le_anti_sym)
   3.701 -    from gsup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   3.702 -      by (fastsimp intro!: gjoin_le elim: gleast_Upper_above)
   3.703 -  next
   3.704 -    from gsup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   3.705 -    by (erule_tac gleast_le)
   3.706 -      (blast intro!: Upper_memI intro: le_trans gjoin_left gjoin_right gjoin_closed)
   3.707 -  qed (simp_all add: L gleast_closed [OF gsup])
   3.708 -qed (simp_all add: L)
   3.709 -
   3.710 -text {* Commutativity holds for @{text "="}. *}
   3.711 -
   3.712 -lemma gjoin_comm:
   3.713 -  fixes L (structure)
   3.714 -  shows "x \<squnion> y = y \<squnion> x"
   3.715 -  by (unfold gjoin_def) (simp add: insert_commute)
   3.716 -
   3.717 -lemma (in gupper_semilattice) gjoin_assoc:
   3.718 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.719 -  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
   3.720 -proof -
   3.721 -  (* FIXME: could be simplified by improved simp: uniform use of .=,
   3.722 -     omit [symmetric] in last step. *)
   3.723 -  have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: gjoin_comm)
   3.724 -  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: gjoin_assoc_lemma)
   3.725 -  also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   3.726 -  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: gjoin_assoc_lemma [symmetric])
   3.727 -  finally show ?thesis by (simp add: L)
   3.728 -qed
   3.729 -
   3.730 -
   3.731 -subsubsection {* Infimum *}
   3.732 -
   3.733 -lemma (in glower_semilattice) gmeetI:
   3.734 -  "[| !!i. ggreatest L i (Lower L {x, y}) ==> P i;
   3.735 -  x \<in> carrier L; y \<in> carrier L |]
   3.736 -  ==> P (x \<sqinter> y)"
   3.737 -proof (unfold gmeet_def ginf_def)
   3.738 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.739 -    and P: "!!g. ggreatest L g (Lower L {x, y}) ==> P g"
   3.740 -  with ginf_of_two_exists obtain i where "ggreatest L i (Lower L {x, y})" by fast
   3.741 -  with L show "P (SOME g. ggreatest L g (Lower L {x, y}))"
   3.742 -  by (fast intro: someI2 ggreatest_unique P)
   3.743 -qed
   3.744 -
   3.745 -lemma (in glower_semilattice) gmeet_closed [simp]:
   3.746 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   3.747 -  by (rule gmeetI) (rule ggreatest_closed)
   3.748 -
   3.749 -lemma (in glower_semilattice) gmeet_cong_l:
   3.750 -  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   3.751 -    and xx': "x .= x'"
   3.752 -  shows "x \<sqinter> y .= x' \<sqinter> y"
   3.753 -proof (rule gmeetI, rule gmeetI)
   3.754 -  fix a b
   3.755 -  from xx' carr
   3.756 -      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   3.757 -
   3.758 -  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
   3.759 -  assume "ggreatest L b (Lower L {x', y})"
   3.760 -  with carr
   3.761 -      have ggreatestb: "ggreatest L b (Lower L {x, y})"
   3.762 -      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
   3.763 -
   3.764 -  from ggreatesta ggreatestb
   3.765 -      show "a .= b" by (rule ggreatest_unique)
   3.766 -qed (rule carr)+
   3.767 -
   3.768 -lemma (in glower_semilattice) gmeet_cong_r:
   3.769 -  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   3.770 -    and yy': "y .= y'"
   3.771 -  shows "x \<sqinter> y .= x \<sqinter> y'"
   3.772 -proof (rule gmeetI, rule gmeetI)
   3.773 -  fix a b
   3.774 -  have "{x, y} = {y, x}" by fast
   3.775 -  also from carr yy'
   3.776 -      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   3.777 -  also have "{y', x} = {x, y'}" by fast
   3.778 -  finally
   3.779 -      have seq: "{x, y} {.=} {x, y'}" .
   3.780 -
   3.781 -  assume ggreatesta: "ggreatest L a (Lower L {x, y})"
   3.782 -  assume "ggreatest L b (Lower L {x, y'})"
   3.783 -  with carr
   3.784 -      have ggreatestb: "ggreatest L b (Lower L {x, y})"
   3.785 -      by (simp add: ggreatest_Lower_cong_r[OF _ _ seq])
   3.786 -
   3.787 -  from ggreatesta ggreatestb
   3.788 -      show "a .= b" by (rule ggreatest_unique)
   3.789 -qed (rule carr)+
   3.790 -
   3.791 -lemma (in gpartial_order) ginf_of_singletonI:      (* only reflexivity needed ? *)
   3.792 -  "x \<in> carrier L ==> ggreatest L x (Lower L {x})"
   3.793 -  by (rule ggreatest_LowerI) auto
   3.794 -
   3.795 -lemma (in gpartial_order) ginf_of_singleton [simp]:
   3.796 -  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
   3.797 -  unfolding ginf_def
   3.798 -  by (rule someI2) (auto intro: ggreatest_unique ginf_of_singletonI)
   3.799 -
   3.800 -lemma (in gpartial_order) ginf_of_singleton_closed:
   3.801 -  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
   3.802 -  unfolding ginf_def
   3.803 -  by (rule someI2) (auto intro: ginf_of_singletonI)
   3.804 -
   3.805 -text {* Condition on @{text A}: infimum exists. *}
   3.806 -
   3.807 -lemma (in glower_semilattice) ginf_insertI:
   3.808 -  "[| !!i. ggreatest L i (Lower L (insert x A)) ==> P i;
   3.809 -  ggreatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   3.810 -  ==> P (\<Sqinter>(insert x A))"
   3.811 -proof (unfold ginf_def)
   3.812 -  assume L: "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.813 -    and P: "!!g. ggreatest L g (Lower L (insert x A)) ==> P g"
   3.814 -    and ggreatest_a: "ggreatest L a (Lower L A)"
   3.815 -  from L ggreatest_a have La: "a \<in> carrier L" by simp
   3.816 -  from L ginf_of_two_exists ggreatest_a
   3.817 -  obtain i where ggreatest_i: "ggreatest L i (Lower L {a, x})" by blast
   3.818 -  show "P (SOME g. ggreatest L g (Lower L (insert x A)))"
   3.819 -  proof (rule someI2)
   3.820 -    show "ggreatest L i (Lower L (insert x A))"
   3.821 -    proof (rule ggreatest_LowerI)
   3.822 -      fix z
   3.823 -      assume "z \<in> insert x A"
   3.824 -      then show "i \<sqsubseteq> z"
   3.825 -      proof
   3.826 -        assume "z = x" then show ?thesis
   3.827 -          by (simp add: ggreatest_Lower_below [OF ggreatest_i] L La)
   3.828 -      next
   3.829 -        assume "z \<in> A"
   3.830 -        with L ggreatest_i ggreatest_a show ?thesis
   3.831 -          by (rule_tac le_trans [where y = a]) (auto dest: ggreatest_Lower_below)
   3.832 -      qed
   3.833 -    next
   3.834 -      fix y
   3.835 -      assume y: "y \<in> Lower L (insert x A)"
   3.836 -      show "y \<sqsubseteq> i"
   3.837 -      proof (rule ggreatest_le [OF ggreatest_i], rule Lower_memI)
   3.838 -	fix z
   3.839 -	assume z: "z \<in> {a, x}"
   3.840 -	then show "y \<sqsubseteq> z"
   3.841 -	proof
   3.842 -          have y': "y \<in> Lower L A"
   3.843 -            apply (rule subsetD [where A = "Lower L (insert x A)"])
   3.844 -            apply (rule Lower_antimono)
   3.845 -	     apply blast
   3.846 -	    apply (rule y)
   3.847 -            done
   3.848 -          assume "z = a"
   3.849 -          with y' ggreatest_a show ?thesis by (fast dest: ggreatest_le)
   3.850 -	next
   3.851 -          assume "z \<in> {x}"
   3.852 -          with y L show ?thesis by blast
   3.853 -	qed
   3.854 -      qed (rule Lower_closed [THEN subsetD, OF y])
   3.855 -    next
   3.856 -      from L show "insert x A \<subseteq> carrier L" by simp
   3.857 -      from ggreatest_i show "i \<in> carrier L" by simp
   3.858 -    qed
   3.859 -  qed (rule P)
   3.860 -qed
   3.861 -
   3.862 -lemma (in glower_semilattice) finite_ginf_ggreatest:
   3.863 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> ggreatest L (\<Sqinter>A) (Lower L A)"
   3.864 -proof (induct set: finite)
   3.865 -  case empty then show ?case by simp
   3.866 -next
   3.867 -  case (insert x A)
   3.868 -  show ?case
   3.869 -  proof (cases "A = {}")
   3.870 -    case True
   3.871 -    with insert show ?thesis
   3.872 -      by simp (simp add: ggreatest_cong [OF ginf_of_singleton]
   3.873 -	ginf_of_singleton_closed ginf_of_singletonI)
   3.874 -  next
   3.875 -    case False
   3.876 -    from insert show ?thesis
   3.877 -    proof (rule_tac ginf_insertI)
   3.878 -      from False insert show "ggreatest L (\<Sqinter>A) (Lower L A)" by simp
   3.879 -    qed simp_all
   3.880 -  qed
   3.881 -qed
   3.882 -
   3.883 -lemma (in glower_semilattice) finite_ginf_insertI:
   3.884 -  assumes P: "!!i. ggreatest L i (Lower L (insert x A)) ==> P i"
   3.885 -    and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   3.886 -  shows "P (\<Sqinter> (insert x A))"
   3.887 -proof (cases "A = {}")
   3.888 -  case True with P and xA show ?thesis
   3.889 -    by (simp add: finite_ginf_ggreatest)
   3.890 -next
   3.891 -  case False with P and xA show ?thesis
   3.892 -    by (simp add: ginf_insertI finite_ginf_ggreatest)
   3.893 -qed
   3.894 -
   3.895 -lemma (in glower_semilattice) finite_ginf_closed [simp]:
   3.896 -  "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   3.897 -proof (induct set: finite)
   3.898 -  case empty then show ?case by simp
   3.899 -next
   3.900 -  case insert then show ?case
   3.901 -    by (rule_tac finite_ginf_insertI) (simp_all)
   3.902 -qed
   3.903 -
   3.904 -lemma (in glower_semilattice) gmeet_left:
   3.905 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   3.906 -  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
   3.907 -
   3.908 -lemma (in glower_semilattice) gmeet_right:
   3.909 -  "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   3.910 -  by (rule gmeetI [folded gmeet_def]) (blast dest: ggreatest_mem)
   3.911 -
   3.912 -lemma (in glower_semilattice) ginf_of_two_ggreatest:
   3.913 -  "[| x \<in> carrier L; y \<in> carrier L |] ==>
   3.914 -  ggreatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   3.915 -proof (unfold ginf_def)
   3.916 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.917 -  with ginf_of_two_exists obtain s where "ggreatest L s (Lower L {x, y})" by fast
   3.918 -  with L
   3.919 -  show "ggreatest L (SOME z. ggreatest L z (Lower L {x, y})) (Lower L {x, y})"
   3.920 -  by (fast intro: someI2 ggreatest_unique)  (* blast fails *)
   3.921 -qed
   3.922 -
   3.923 -lemma (in glower_semilattice) gmeet_le:
   3.924 -  assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
   3.925 -    and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   3.926 -  shows "z \<sqsubseteq> x \<sqinter> y"
   3.927 -proof (rule gmeetI [OF _ x y])
   3.928 -  fix i
   3.929 -  assume "ggreatest L i (Lower L {x, y})"
   3.930 -  with sub z show "z \<sqsubseteq> i" by (fast elim: ggreatest_le intro: Lower_memI)
   3.931 -qed
   3.932 -
   3.933 -lemma (in glower_semilattice) gmeet_assoc_lemma:
   3.934 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.935 -  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
   3.936 -proof (rule finite_ginf_insertI)
   3.937 -  txt {* The textbook argument in Jacobson I, p 457 *}
   3.938 -  fix i
   3.939 -  assume ginf: "ggreatest L i (Lower L {x, y, z})"
   3.940 -  show "x \<sqinter> (y \<sqinter> z) .= i"
   3.941 -  proof (rule le_anti_sym)
   3.942 -    from ginf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
   3.943 -      by (fastsimp intro!: gmeet_le elim: ggreatest_Lower_below)
   3.944 -  next
   3.945 -    from ginf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
   3.946 -    by (erule_tac ggreatest_le)
   3.947 -      (blast intro!: Lower_memI intro: le_trans gmeet_left gmeet_right gmeet_closed)
   3.948 -  qed (simp_all add: L ggreatest_closed [OF ginf])
   3.949 -qed (simp_all add: L)
   3.950 -
   3.951 -lemma gmeet_comm:
   3.952 -  fixes L (structure)
   3.953 -  shows "x \<sqinter> y = y \<sqinter> x"
   3.954 -  by (unfold gmeet_def) (simp add: insert_commute)
   3.955 -
   3.956 -lemma (in glower_semilattice) gmeet_assoc:
   3.957 -  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   3.958 -  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
   3.959 -proof -
   3.960 -  (* FIXME: improved simp, see gjoin_assoc above *)
   3.961 -  have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: gmeet_comm)
   3.962 -  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: gmeet_assoc_lemma)
   3.963 -  also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
   3.964 -  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: gmeet_assoc_lemma [symmetric])
   3.965 -  finally show ?thesis by (simp add: L)
   3.966 -qed
   3.967 -
   3.968 -
   3.969 -subsection {* Total Orders *}
   3.970 -
   3.971 -locale gtotal_order = gpartial_order +
   3.972 -  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.973 -
   3.974 -text {* Introduction rule: the usual definition of total order *}
   3.975 -
   3.976 -lemma (in gpartial_order) gtotal_orderI:
   3.977 -  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
   3.978 -  shows "gtotal_order L"
   3.979 -  by unfold_locales (rule total)
   3.980 -
   3.981 -text {* Total orders are lattices. *}
   3.982 -
   3.983 -interpretation gtotal_order < glattice
   3.984 -proof unfold_locales
   3.985 -  fix x y
   3.986 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
   3.987 -  show "EX s. gleast L s (Upper L {x, y})"
   3.988 -  proof -
   3.989 -    note total L
   3.990 -    moreover
   3.991 -    {
   3.992 -      assume "x \<sqsubseteq> y"
   3.993 -      with L have "gleast L y (Upper L {x, y})"
   3.994 -        by (rule_tac gleast_UpperI) auto
   3.995 -    }
   3.996 -    moreover
   3.997 -    {
   3.998 -      assume "y \<sqsubseteq> x"
   3.999 -      with L have "gleast L x (Upper L {x, y})"
  3.1000 -        by (rule_tac gleast_UpperI) auto
  3.1001 -    }
  3.1002 -    ultimately show ?thesis by blast
  3.1003 -  qed
  3.1004 -next
  3.1005 -  fix x y
  3.1006 -  assume L: "x \<in> carrier L"  "y \<in> carrier L"
  3.1007 -  show "EX i. ggreatest L i (Lower L {x, y})"
  3.1008 -  proof -
  3.1009 -    note total L
  3.1010 -    moreover
  3.1011 -    {
  3.1012 -      assume "y \<sqsubseteq> x"
  3.1013 -      with L have "ggreatest L y (Lower L {x, y})"
  3.1014 -        by (rule_tac ggreatest_LowerI) auto
  3.1015 -    }
  3.1016 -    moreover
  3.1017 -    {
  3.1018 -      assume "x \<sqsubseteq> y"
  3.1019 -      with L have "ggreatest L x (Lower L {x, y})"
  3.1020 -        by (rule_tac ggreatest_LowerI) auto
  3.1021 -    }
  3.1022 -    ultimately show ?thesis by blast
  3.1023 -  qed
  3.1024 -qed
  3.1025 -
  3.1026 -
  3.1027 -subsection {* Complete lattices *}
  3.1028 -
  3.1029 -locale complete_lattice = glattice +
  3.1030 -  assumes gsup_exists:
  3.1031 -    "[| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
  3.1032 -    and ginf_exists:
  3.1033 -    "[| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
  3.1034 -
  3.1035 -text {* Introduction rule: the usual definition of complete lattice *}
  3.1036 -
  3.1037 -lemma (in gpartial_order) complete_latticeI:
  3.1038 -  assumes gsup_exists:
  3.1039 -    "!!A. [| A \<subseteq> carrier L |] ==> EX s. gleast L s (Upper L A)"
  3.1040 -    and ginf_exists:
  3.1041 -    "!!A. [| A \<subseteq> carrier L |] ==> EX i. ggreatest L i (Lower L A)"
  3.1042 -  shows "complete_lattice L"
  3.1043 -  by unfold_locales (auto intro: gsup_exists ginf_exists)
  3.1044 -
  3.1045 -constdefs (structure L)
  3.1046 -  top :: "_ => 'a" ("\<top>\<index>")
  3.1047 -  "\<top> == gsup L (carrier L)"
  3.1048 -
  3.1049 -  bottom :: "_ => 'a" ("\<bottom>\<index>")
  3.1050 -  "\<bottom> == ginf L (carrier L)"
  3.1051 -
  3.1052 -
  3.1053 -lemma (in complete_lattice) gsupI:
  3.1054 -  "[| !!l. gleast L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
  3.1055 -  ==> P (\<Squnion>A)"
  3.1056 -proof (unfold gsup_def)
  3.1057 -  assume L: "A \<subseteq> carrier L"
  3.1058 -    and P: "!!l. gleast L l (Upper L A) ==> P l"
  3.1059 -  with gsup_exists obtain s where "gleast L s (Upper L A)" by blast
  3.1060 -  with L show "P (SOME l. gleast L l (Upper L A))"
  3.1061 -  by (fast intro: someI2 gleast_unique P)
  3.1062 -qed
  3.1063 -
  3.1064 -lemma (in complete_lattice) gsup_closed [simp]:
  3.1065 -  "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
  3.1066 -  by (rule gsupI) simp_all
  3.1067 -
  3.1068 -lemma (in complete_lattice) top_closed [simp, intro]:
  3.1069 -  "\<top> \<in> carrier L"
  3.1070 -  by (unfold top_def) simp
  3.1071 -
  3.1072 -lemma (in complete_lattice) ginfI:
  3.1073 -  "[| !!i. ggreatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
  3.1074 -  ==> P (\<Sqinter>A)"
  3.1075 -proof (unfold ginf_def)
  3.1076 -  assume L: "A \<subseteq> carrier L"
  3.1077 -    and P: "!!l. ggreatest L l (Lower L A) ==> P l"
  3.1078 -  with ginf_exists obtain s where "ggreatest L s (Lower L A)" by blast
  3.1079 -  with L show "P (SOME l. ggreatest L l (Lower L A))"
  3.1080 -  by (fast intro: someI2 ggreatest_unique P)
  3.1081 -qed
  3.1082 -
  3.1083 -lemma (in complete_lattice) ginf_closed [simp]:
  3.1084 -  "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
  3.1085 -  by (rule ginfI) simp_all
  3.1086 -
  3.1087 -lemma (in complete_lattice) bottom_closed [simp, intro]:
  3.1088 -  "\<bottom> \<in> carrier L"
  3.1089 -  by (unfold bottom_def) simp
  3.1090 -
  3.1091 -text {* Jacobson: Theorem 8.1 *}
  3.1092 -
  3.1093 -lemma Lower_empty [simp]:
  3.1094 -  "Lower L {} = carrier L"
  3.1095 -  by (unfold Lower_def) simp
  3.1096 -
  3.1097 -lemma Upper_empty [simp]:
  3.1098 -  "Upper L {} = carrier L"
  3.1099 -  by (unfold Upper_def) simp
  3.1100 -
  3.1101 -theorem (in gpartial_order) complete_lattice_criterion1:
  3.1102 -  assumes top_exists: "EX g. ggreatest L g (carrier L)"
  3.1103 -    and ginf_exists:
  3.1104 -      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. ggreatest L i (Lower L A)"
  3.1105 -  shows "complete_lattice L"
  3.1106 -proof (rule complete_latticeI)
  3.1107 -  from top_exists obtain top where top: "ggreatest L top (carrier L)" ..
  3.1108 -  fix A
  3.1109 -  assume L: "A \<subseteq> carrier L"
  3.1110 -  let ?B = "Upper L A"
  3.1111 -  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: ggreatest_le)
  3.1112 -  then have B_non_empty: "?B ~= {}" by fast
  3.1113 -  have B_L: "?B \<subseteq> carrier L" by simp
  3.1114 -  from ginf_exists [OF B_L B_non_empty]
  3.1115 -  obtain b where b_ginf_B: "ggreatest L b (Lower L ?B)" ..
  3.1116 -  have "gleast L b (Upper L A)"
  3.1117 -apply (rule gleast_UpperI)
  3.1118 -   apply (rule ggreatest_le [where A = "Lower L ?B"])
  3.1119 -    apply (rule b_ginf_B)
  3.1120 -   apply (rule Lower_memI)
  3.1121 -    apply (erule Upper_memD [THEN conjunct1])
  3.1122 -     apply assumption
  3.1123 -    apply (rule L)
  3.1124 -   apply (fast intro: L [THEN subsetD])
  3.1125 -  apply (erule ggreatest_Lower_below [OF b_ginf_B])
  3.1126 -  apply simp
  3.1127 - apply (rule L)
  3.1128 -apply (rule ggreatest_closed [OF b_ginf_B])
  3.1129 -done
  3.1130 -  then show "EX s. gleast L s (Upper L A)" ..
  3.1131 -next
  3.1132 -  fix A
  3.1133 -  assume L: "A \<subseteq> carrier L"
  3.1134 -  show "EX i. ggreatest L i (Lower L A)"
  3.1135 -  proof (cases "A = {}")
  3.1136 -    case True then show ?thesis
  3.1137 -      by (simp add: top_exists)
  3.1138 -  next
  3.1139 -    case False with L show ?thesis
  3.1140 -      by (rule ginf_exists)
  3.1141 -  qed
  3.1142 -qed
  3.1143 -
  3.1144 -(* TODO: prove dual version *)
  3.1145 -
  3.1146 -
  3.1147 -subsection {* Examples *}
  3.1148 -
  3.1149 -(* Not so useful for the generalised version.
  3.1150 -
  3.1151 -subsubsection {* Powerset of a Set is a Complete Lattice *}
  3.1152 -
  3.1153 -theorem powerset_is_complete_lattice:
  3.1154 -  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
  3.1155 -  (is "complete_lattice ?L")
  3.1156 -proof (rule gpartial_order.complete_latticeI)
  3.1157 -  show "gpartial_order ?L"
  3.1158 -    by (rule gpartial_order.intro) auto
  3.1159 -next
  3.1160 -  fix B
  3.1161 -  assume B: "B \<subseteq> carrier ?L"
  3.1162 -  show "EX s. gleast ?L s (Upper ?L B)"
  3.1163 -  proof
  3.1164 -    from B show "gleast ?L (\<Union> B) (Upper ?L B)"
  3.1165 -      by (fastsimp intro!: gleast_UpperI simp: Upper_def)
  3.1166 -  qed
  3.1167 -next
  3.1168 -  fix B
  3.1169 -  assume B: "B \<subseteq> carrier ?L"
  3.1170 -  show "EX i. ggreatest ?L i (Lower ?L B)"
  3.1171 -  proof
  3.1172 -    from B show "ggreatest ?L (\<Inter> B \<inter> A) (Lower ?L B)"
  3.1173 -      txt {* @{term "\<Inter> B"} is not the infimum of @{term B}:
  3.1174 -	@{term "\<Inter> {} = UNIV"} which is in general bigger than @{term "A"}! *}
  3.1175 -      by (fastsimp intro!: ggreatest_LowerI simp: Lower_def)
  3.1176 -  qed
  3.1177 -qed
  3.1178 -
  3.1179 -text {* An other example, that of the lattice of subgroups of a group,
  3.1180 -  can be found in Group theory (Section~\ref{sec:subgroup-lattice}). *}
  3.1181 -
  3.1182 -*)
  3.1183 -
  3.1184 -end
     4.1 --- a/src/HOL/Algebra/Group.thy	Wed Jul 30 16:07:00 2008 +0200
     4.2 +++ b/src/HOL/Algebra/Group.thy	Wed Jul 30 19:03:33 2008 +0200
     4.3 @@ -712,8 +712,8 @@
     4.4  text_raw {* \label{sec:subgroup-lattice} *}
     4.5  
     4.6  theorem (in group) subgroups_partial_order:
     4.7 -  "partial_order (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
     4.8 -  by (rule partial_order.intro) simp_all
     4.9 +  "partial_order (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
    4.10 +  by unfold_locales simp_all
    4.11  
    4.12  lemma (in group) subgroup_self:
    4.13    "subgroup (carrier G) G"
    4.14 @@ -757,7 +757,7 @@
    4.15  qed
    4.16  
    4.17  theorem (in group) subgroups_complete_lattice:
    4.18 -  "complete_lattice (| carrier = {H. subgroup H G}, le = op \<subseteq> |)"
    4.19 +  "complete_lattice (| carrier = {H. subgroup H G}, eq = op =, le = op \<subseteq> |)"
    4.20      (is "complete_lattice ?L")
    4.21  proof (rule partial_order.complete_lattice_criterion1)
    4.22    show "partial_order ?L" by (rule subgroups_partial_order)
     5.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Jul 30 16:07:00 2008 +0200
     5.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Jul 30 19:03:33 2008 +0200
     5.3 @@ -208,27 +208,27 @@
     5.4    by simp_all
     5.5  
     5.6  interpretation int [unfolded UNIV]:
     5.7 -  partial_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
     5.8 -  where "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
     5.9 -    and "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    5.10 -    and "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    5.11 +  partial_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.12 +  where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    5.13 +    and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    5.14 +    and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    5.15  proof -
    5.16 -  show "partial_order (| carrier = UNIV::int set, le = op \<le> |)"
    5.17 +  show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    5.18      by unfold_locales simp_all
    5.19 -  show "carrier (| carrier = UNIV::int set, le = op \<le> |) = UNIV"
    5.20 +  show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
    5.21      by simp
    5.22 -  show "le (| carrier = UNIV::int set, le = op \<le> |) x y = (x \<le> y)"
    5.23 +  show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
    5.24      by simp
    5.25 -  show "lless (| carrier = UNIV::int set, le = op \<le> |) x y = (x < y)"
    5.26 +  show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
    5.27      by (simp add: lless_def) auto
    5.28  qed
    5.29  
    5.30  interpretation int [unfolded UNIV]:
    5.31 -  lattice ["(| carrier = UNIV::int set, le = op \<le> |)"]
    5.32 -  where "join (| carrier = UNIV::int set, le = op \<le> |) x y = max x y"
    5.33 -    and "meet (| carrier = UNIV::int set, le = op \<le> |) x y = min x y"
    5.34 +  lattice ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.35 +  where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
    5.36 +    and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
    5.37  proof -
    5.38 -  let ?Z = "(| carrier = UNIV::int set, le = op \<le> |)"
    5.39 +  let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
    5.40    show "lattice ?Z"
    5.41      apply unfold_locales
    5.42      apply (simp add: least_def Upper_def)
    5.43 @@ -250,7 +250,7 @@
    5.44  qed
    5.45  
    5.46  interpretation int [unfolded UNIV]:
    5.47 -  total_order ["(| carrier = UNIV::int set, le = op \<le> |)"]
    5.48 +  total_order ["(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"]
    5.49    by unfold_locales clarsimp
    5.50  
    5.51  
     6.1 --- a/src/HOL/Algebra/Lattice.thy	Wed Jul 30 16:07:00 2008 +0200
     6.2 +++ b/src/HOL/Algebra/Lattice.thy	Wed Jul 30 19:03:33 2008 +0200
     6.3 @@ -1,5 +1,5 @@
     6.4  (*
     6.5 -  Title:     HOL/Algebra/Lattice.thy
     6.6 +  Title:     HOL/Algebra/GLattice.thy
     6.7    Id:        $Id$
     6.8    Author:    Clemens Ballarin, started 7 November 2003
     6.9    Copyright: Clemens Ballarin
    6.10 @@ -7,88 +7,202 @@
    6.11  
    6.12  theory Lattice imports Congruence begin
    6.13  
    6.14 -
    6.15  section {* Orders and Lattices *}
    6.16  
    6.17  subsection {* Partial Orders *}
    6.18  
    6.19 -record 'a order = "'a partial_object" +
    6.20 +record 'a gorder = "'a eq_object" +
    6.21    le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>\<index>" 50)
    6.22  
    6.23 -locale partial_order =
    6.24 -  fixes L (structure)
    6.25 -  assumes refl [intro, simp]:
    6.26 -                  "x \<in> carrier L ==> x \<sqsubseteq> x"
    6.27 -    and anti_sym [intro]:
    6.28 -                  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    6.29 -    and trans [trans]:
    6.30 -                  "[| x \<sqsubseteq> y; y \<sqsubseteq> z;
    6.31 -                   x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    6.32 +locale weak_partial_order = equivalence L +
    6.33 +  assumes le_refl [intro, simp]:
    6.34 +      "x \<in> carrier L ==> x \<sqsubseteq> x"
    6.35 +    and weak_le_anti_sym [intro]:
    6.36 +      "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    6.37 +    and le_trans [trans]:
    6.38 +      "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    6.39 +    and le_cong:
    6.40 +      "\<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"
    6.41  
    6.42  constdefs (structure L)
    6.43    lless :: "[_, 'a, 'a] => bool" (infixl "\<sqsubset>\<index>" 50)
    6.44 -  "x \<sqsubset> y == x \<sqsubseteq> y & x ~= y"
    6.45 +  "x \<sqsubset> y == x \<sqsubseteq> y & x .\<noteq> y"
    6.46 +
    6.47 +
    6.48 +subsubsection {* The order relation *}
    6.49 +
    6.50 +context weak_partial_order begin
    6.51 +
    6.52 +lemma le_cong_l [intro, trans]:
    6.53 +  "\<lbrakk> x .= y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    6.54 +  by (auto intro: le_cong [THEN iffD2])
    6.55 +
    6.56 +lemma le_cong_r [intro, trans]:
    6.57 +  "\<lbrakk> x \<sqsubseteq> y; y .= z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> z"
    6.58 +  by (auto intro: le_cong [THEN iffD1])
    6.59 +
    6.60 +lemma gen_refl [intro, simp]: "\<lbrakk> x .= y; x \<in> carrier L; y \<in> carrier L \<rbrakk> \<Longrightarrow> x \<sqsubseteq> y"
    6.61 +  by (simp add: le_cong_l)
    6.62 +
    6.63 +end
    6.64 +
    6.65 +lemma weak_llessI:
    6.66 +  fixes R (structure)
    6.67 +  assumes "x \<sqsubseteq> y" and "~(x .= y)"
    6.68 +  shows "x \<sqsubset> y"
    6.69 +  using assms unfolding lless_def by simp
    6.70 +
    6.71 +lemma lless_imp_le:
    6.72 +  fixes R (structure)
    6.73 +  assumes "x \<sqsubset> y"
    6.74 +  shows "x \<sqsubseteq> y"
    6.75 +  using assms unfolding lless_def by simp
    6.76 +
    6.77 +lemma weak_lless_imp_not_eq:
    6.78 +  fixes R (structure)
    6.79 +  assumes "x \<sqsubset> y"
    6.80 +  shows "\<not> (x .= y)"
    6.81 +  using assms unfolding lless_def by simp
    6.82  
    6.83 -  -- {* Upper and lower bounds of a set. *}
    6.84 +lemma weak_llessE:
    6.85 +  fixes R (structure)
    6.86 +  assumes p: "x \<sqsubset> y" and e: "\<lbrakk>x \<sqsubseteq> y; \<not> (x .= y)\<rbrakk> \<Longrightarrow> P"
    6.87 +  shows "P"
    6.88 +  using p by (blast dest: lless_imp_le weak_lless_imp_not_eq e)
    6.89 +
    6.90 +lemma (in weak_partial_order) lless_cong_l [trans]:
    6.91 +  assumes xx': "x .= x'"
    6.92 +    and xy: "x' \<sqsubset> y"
    6.93 +    and carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
    6.94 +  shows "x \<sqsubset> y"
    6.95 +  using assms unfolding lless_def by (auto intro: trans sym)
    6.96 +
    6.97 +lemma (in weak_partial_order) lless_cong_r [trans]:
    6.98 +  assumes xy: "x \<sqsubset> y"
    6.99 +    and  yy': "y .= y'"
   6.100 +    and carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   6.101 +  shows "x \<sqsubset> y'"
   6.102 +  using assms unfolding lless_def by (auto intro: trans sym)
   6.103 +
   6.104 +
   6.105 +lemma (in weak_partial_order) lless_antisym:
   6.106 +  assumes "a \<in> carrier L" "b \<in> carrier L"
   6.107 +    and "a \<sqsubset> b" "b \<sqsubset> a"
   6.108 +  shows "P"
   6.109 +  using assms
   6.110 +  by (elim weak_llessE) auto
   6.111 +
   6.112 +lemma (in weak_partial_order) lless_trans [trans]:
   6.113 +  assumes "a \<sqsubset> b" "b \<sqsubset> c"
   6.114 +    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
   6.115 +  shows "a \<sqsubset> c"
   6.116 +  using assms unfolding lless_def by (blast dest: le_trans intro: sym)
   6.117 +
   6.118 +
   6.119 +subsubsection {* Upper and lower bounds of a set *}
   6.120 +
   6.121 +constdefs (structure L)
   6.122    Upper :: "[_, 'a set] => 'a set"
   6.123 -  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter>
   6.124 -                carrier L"
   6.125 +  "Upper L A == {u. (ALL x. x \<in> A \<inter> carrier L --> x \<sqsubseteq> u)} \<inter> carrier L"
   6.126  
   6.127    Lower :: "[_, 'a set] => 'a set"
   6.128 -  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter>
   6.129 -                carrier L"
   6.130 -
   6.131 -  -- {* Least and greatest, as predicate. *}
   6.132 -  least :: "[_, 'a, 'a set] => bool"
   6.133 -  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
   6.134 -
   6.135 -  greatest :: "[_, 'a, 'a set] => bool"
   6.136 -  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
   6.137 -
   6.138 -  -- {* Supremum and infimum *}
   6.139 -  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   6.140 -  "\<Squnion>A == THE x. least L x (Upper L A)"
   6.141 +  "Lower L A == {l. (ALL x. x \<in> A \<inter> carrier L --> l \<sqsubseteq> x)} \<inter> carrier L"
   6.142  
   6.143 -  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   6.144 -  "\<Sqinter>A == THE x. greatest L x (Lower L A)"
   6.145 -
   6.146 -  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   6.147 -  "x \<squnion> y == sup L {x, y}"
   6.148 -
   6.149 -  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   6.150 -  "x \<sqinter> y == inf L {x, y}"
   6.151 -
   6.152 -
   6.153 -subsubsection {* Upper *}
   6.154 -
   6.155 -lemma Upper_closed [intro, simp]:
   6.156 +lemma Upper_closed [intro!, simp]:
   6.157    "Upper L A \<subseteq> carrier L"
   6.158    by (unfold Upper_def) clarify
   6.159  
   6.160  lemma Upper_memD [dest]:
   6.161    fixes L (structure)
   6.162 -  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   6.163 +  shows "[| u \<in> Upper L A; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u \<and> u \<in> carrier L"
   6.164    by (unfold Upper_def) blast
   6.165  
   6.166 +lemma (in weak_partial_order) Upper_elemD [dest]:
   6.167 +  "[| u .\<in> Upper L A; u \<in> carrier L; x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> u"
   6.168 +  unfolding Upper_def elem_def
   6.169 +  by (blast dest: sym)
   6.170 +
   6.171  lemma Upper_memI:
   6.172    fixes L (structure)
   6.173    shows "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x \<in> Upper L A"
   6.174    by (unfold Upper_def) blast
   6.175  
   6.176 +lemma (in weak_partial_order) Upper_elemI:
   6.177 +  "[| !! y. y \<in> A ==> y \<sqsubseteq> x; x \<in> carrier L |] ==> x .\<in> Upper L A"
   6.178 +  unfolding Upper_def by blast
   6.179 +
   6.180  lemma Upper_antimono:
   6.181    "A \<subseteq> B ==> Upper L B \<subseteq> Upper L A"
   6.182    by (unfold Upper_def) blast
   6.183  
   6.184 +lemma (in weak_partial_order) Upper_is_closed [simp]:
   6.185 +  "A \<subseteq> carrier L ==> is_closed (Upper L A)"
   6.186 +  by (rule is_closedI) (blast intro: Upper_memI)+
   6.187  
   6.188 -subsubsection {* Lower *}
   6.189 +lemma (in weak_partial_order) Upper_mem_cong:
   6.190 +  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   6.191 +    and aa': "a .= a'"
   6.192 +    and aelem: "a \<in> Upper L A"
   6.193 +  shows "a' \<in> Upper L A"
   6.194 +proof (rule Upper_memI[OF _ a'carr])
   6.195 +  fix y
   6.196 +  assume yA: "y \<in> A"
   6.197 +  hence "y \<sqsubseteq> a" by (intro Upper_memD[OF aelem, THEN conjunct1] Acarr)
   6.198 +  also note aa'
   6.199 +  finally
   6.200 +      show "y \<sqsubseteq> a'"
   6.201 +      by (simp add: a'carr subsetD[OF Acarr yA] subsetD[OF Upper_closed aelem])
   6.202 +qed
   6.203 +
   6.204 +lemma (in weak_partial_order) Upper_cong:
   6.205 +  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   6.206 +    and AA': "A {.=} A'"
   6.207 +  shows "Upper L A = Upper L A'"
   6.208 +unfolding Upper_def
   6.209 +apply rule
   6.210 + apply (rule, clarsimp) defer 1
   6.211 + apply (rule, clarsimp) defer 1
   6.212 +proof -
   6.213 +  fix x a'
   6.214 +  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   6.215 +    and a'A': "a' \<in> A'"
   6.216 +  assume aLxCond[rule_format]: "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> a \<sqsubseteq> x"
   6.217  
   6.218 -lemma Lower_closed [intro, simp]:
   6.219 +  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   6.220 +  from this obtain a
   6.221 +      where aA: "a \<in> A"
   6.222 +      and a'a: "a' .= a"
   6.223 +      by auto
   6.224 +  note [simp] = subsetD[OF Acarr aA] carr
   6.225 +
   6.226 +  note a'a
   6.227 +  also have "a \<sqsubseteq> x" by (simp add: aLxCond aA)
   6.228 +  finally show "a' \<sqsubseteq> x" by simp
   6.229 +next
   6.230 +  fix x a
   6.231 +  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   6.232 +    and aA: "a \<in> A"
   6.233 +  assume a'LxCond[rule_format]: "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> a' \<sqsubseteq> x"
   6.234 +
   6.235 +  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   6.236 +  from this obtain a'
   6.237 +      where a'A': "a' \<in> A'"
   6.238 +      and aa': "a .= a'"
   6.239 +      by auto
   6.240 +  note [simp] = subsetD[OF A'carr a'A'] carr
   6.241 +
   6.242 +  note aa'
   6.243 +  also have "a' \<sqsubseteq> x" by (simp add: a'LxCond a'A')
   6.244 +  finally show "a \<sqsubseteq> x" by simp
   6.245 +qed
   6.246 +
   6.247 +lemma Lower_closed [intro!, simp]:
   6.248    "Lower L A \<subseteq> carrier L"
   6.249    by (unfold Lower_def) clarify
   6.250  
   6.251  lemma Lower_memD [dest]:
   6.252    fixes L (structure)
   6.253 -  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x"
   6.254 +  shows "[| l \<in> Lower L A; x \<in> A; A \<subseteq> carrier L |] ==> l \<sqsubseteq> x \<and> l \<in> carrier L"
   6.255    by (unfold Lower_def) blast
   6.256  
   6.257  lemma Lower_memI:
   6.258 @@ -100,19 +214,86 @@
   6.259    "A \<subseteq> B ==> Lower L B \<subseteq> Lower L A"
   6.260    by (unfold Lower_def) blast
   6.261  
   6.262 +lemma (in weak_partial_order) Lower_is_closed [simp]:
   6.263 +  "A \<subseteq> carrier L \<Longrightarrow> is_closed (Lower L A)"
   6.264 +  by (rule is_closedI) (blast intro: Lower_memI dest: sym)+
   6.265  
   6.266 -subsubsection {* least *}
   6.267 +lemma (in weak_partial_order) Lower_mem_cong:
   6.268 +  assumes a'carr: "a' \<in> carrier L" and Acarr: "A \<subseteq> carrier L"
   6.269 +    and aa': "a .= a'"
   6.270 +    and aelem: "a \<in> Lower L A"
   6.271 +  shows "a' \<in> Lower L A"
   6.272 +using assms Lower_closed[of L A]
   6.273 +by (intro Lower_memI) (blast intro: le_cong_l[OF aa'[symmetric]])
   6.274 +
   6.275 +lemma (in weak_partial_order) Lower_cong:
   6.276 +  assumes Acarr: "A \<subseteq> carrier L" and A'carr: "A' \<subseteq> carrier L"
   6.277 +    and AA': "A {.=} A'"
   6.278 +  shows "Lower L A = Lower L A'"
   6.279 +using Lower_memD[of y]
   6.280 +unfolding Lower_def
   6.281 +apply safe
   6.282 + apply clarsimp defer 1
   6.283 + apply clarsimp defer 1
   6.284 +proof -
   6.285 +  fix x a'
   6.286 +  assume carr: "x \<in> carrier L" "a' \<in> carrier L"
   6.287 +    and a'A': "a' \<in> A'"
   6.288 +  assume "\<forall>a. a \<in> A \<and> a \<in> carrier L \<longrightarrow> x \<sqsubseteq> a"
   6.289 +  hence aLxCond: "\<And>a. \<lbrakk>a \<in> A; a \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a" by fast
   6.290 +
   6.291 +  from AA' and a'A' have "\<exists>a\<in>A. a' .= a" by (rule set_eqD2)
   6.292 +  from this obtain a
   6.293 +      where aA: "a \<in> A"
   6.294 +      and a'a: "a' .= a"
   6.295 +      by auto
   6.296 +
   6.297 +  from aA and subsetD[OF Acarr aA]
   6.298 +      have "x \<sqsubseteq> a" by (rule aLxCond)
   6.299 +  also note a'a[symmetric]
   6.300 +  finally
   6.301 +      show "x \<sqsubseteq> a'" by (simp add: carr subsetD[OF Acarr aA])
   6.302 +next
   6.303 +  fix x a
   6.304 +  assume carr: "x \<in> carrier L" "a \<in> carrier L"
   6.305 +    and aA: "a \<in> A"
   6.306 +  assume "\<forall>a'. a' \<in> A' \<and> a' \<in> carrier L \<longrightarrow> x \<sqsubseteq> a'"
   6.307 +  hence a'LxCond: "\<And>a'. \<lbrakk>a' \<in> A'; a' \<in> carrier L\<rbrakk> \<Longrightarrow> x \<sqsubseteq> a'" by fast+
   6.308 +
   6.309 +  from AA' and aA have "\<exists>a'\<in>A'. a .= a'" by (rule set_eqD1)
   6.310 +  from this obtain a'
   6.311 +      where a'A': "a' \<in> A'"
   6.312 +      and aa': "a .= a'"
   6.313 +      by auto
   6.314 +  from a'A' and subsetD[OF A'carr a'A']
   6.315 +      have "x \<sqsubseteq> a'" by (rule a'LxCond)
   6.316 +  also note aa'[symmetric]
   6.317 +  finally show "x \<sqsubseteq> a" by (simp add: carr subsetD[OF A'carr a'A'])
   6.318 +qed
   6.319 +
   6.320 +
   6.321 +subsubsection {* Least and greatest, as predicate *}
   6.322 +
   6.323 +constdefs (structure L)
   6.324 +  least :: "[_, 'a, 'a set] => bool"
   6.325 +  "least L l A == A \<subseteq> carrier L & l \<in> A & (ALL x : A. l \<sqsubseteq> x)"
   6.326 +
   6.327 +  greatest :: "[_, 'a, 'a set] => bool"
   6.328 +  "greatest L g A == A \<subseteq> carrier L & g \<in> A & (ALL x : A. x \<sqsubseteq> g)"
   6.329 +
   6.330 +text {* Could weaken these to @{term [locale=weak_partial_order] "l \<in> carrier L \<and> l
   6.331 +  .\<in> A"} and @{term [locale=weak_partial_order] "g \<in> carrier L \<and> g .\<in> A"}. *}
   6.332  
   6.333  lemma least_closed [intro, simp]:
   6.334 -  shows "least L l A ==> l \<in> carrier L"
   6.335 +  "least L l A ==> l \<in> carrier L"
   6.336    by (unfold least_def) fast
   6.337  
   6.338  lemma least_mem:
   6.339    "least L l A ==> l \<in> A"
   6.340    by (unfold least_def) fast
   6.341  
   6.342 -lemma (in partial_order) least_unique:
   6.343 -  "[| least L x A; least L y A |] ==> x = y"
   6.344 +lemma (in weak_partial_order) weak_least_unique:
   6.345 +  "[| least L x A; least L y A |] ==> x .= y"
   6.346    by (unfold least_def) blast
   6.347  
   6.348  lemma least_le:
   6.349 @@ -120,6 +301,27 @@
   6.350    shows "[| least L x A; a \<in> A |] ==> x \<sqsubseteq> a"
   6.351    by (unfold least_def) fast
   6.352  
   6.353 +lemma (in weak_partial_order) least_cong:
   6.354 +  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==> least L x A = least L x' A"
   6.355 +  by (unfold least_def) (auto dest: sym)
   6.356 +
   6.357 +text {* @{const least} is not congruent in the second parameter for 
   6.358 +  @{term [locale=weak_partial_order] "A {.=} A'"} *}
   6.359 +
   6.360 +lemma (in weak_partial_order) least_Upper_cong_l:
   6.361 +  assumes "x .= x'"
   6.362 +    and "x \<in> carrier L" "x' \<in> carrier L"
   6.363 +    and "A \<subseteq> carrier L"
   6.364 +  shows "least L x (Upper L A) = least L x' (Upper L A)"
   6.365 +  apply (rule least_cong) using assms by auto
   6.366 +
   6.367 +lemma (in weak_partial_order) least_Upper_cong_r:
   6.368 +  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L" (* unneccessary with current Upper? *)
   6.369 +    and AA': "A {.=} A'"
   6.370 +  shows "least L x (Upper L A) = least L x (Upper L A')"
   6.371 +apply (subgoal_tac "Upper L A = Upper L A'", simp)
   6.372 +by (rule Upper_cong) fact+
   6.373 +
   6.374  lemma least_UpperI:
   6.375    fixes L (structure)
   6.376    assumes above: "!! x. x \<in> A ==> x \<sqsubseteq> s"
   6.377 @@ -133,19 +335,21 @@
   6.378    ultimately show ?thesis by (simp add: least_def)
   6.379  qed
   6.380  
   6.381 -
   6.382 -subsubsection {* greatest *}
   6.383 +lemma least_Upper_above:
   6.384 +  fixes L (structure)
   6.385 +  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   6.386 +  by (unfold least_def) blast
   6.387  
   6.388  lemma greatest_closed [intro, simp]:
   6.389 -  shows "greatest L l A ==> l \<in> carrier L"
   6.390 +  "greatest L l A ==> l \<in> carrier L"
   6.391    by (unfold greatest_def) fast
   6.392  
   6.393  lemma greatest_mem:
   6.394    "greatest L l A ==> l \<in> A"
   6.395    by (unfold greatest_def) fast
   6.396  
   6.397 -lemma (in partial_order) greatest_unique:
   6.398 -  "[| greatest L x A; greatest L y A |] ==> x = y"
   6.399 +lemma (in weak_partial_order) weak_greatest_unique:
   6.400 +  "[| greatest L x A; greatest L y A |] ==> x .= y"
   6.401    by (unfold greatest_def) blast
   6.402  
   6.403  lemma greatest_le:
   6.404 @@ -153,6 +357,28 @@
   6.405    shows "[| greatest L x A; a \<in> A |] ==> a \<sqsubseteq> x"
   6.406    by (unfold greatest_def) fast
   6.407  
   6.408 +lemma (in weak_partial_order) greatest_cong:
   6.409 +  "[| x .= x'; x \<in> carrier L; x' \<in> carrier L; is_closed A |] ==>
   6.410 +  greatest L x A = greatest L x' A"
   6.411 +  by (unfold greatest_def) (auto dest: sym)
   6.412 +
   6.413 +text {* @{const greatest} is not congruent in the second parameter for 
   6.414 +  @{term [locale=weak_partial_order] "A {.=} A'"} *}
   6.415 +
   6.416 +lemma (in weak_partial_order) greatest_Lower_cong_l:
   6.417 +  assumes "x .= x'"
   6.418 +    and "x \<in> carrier L" "x' \<in> carrier L"
   6.419 +    and "A \<subseteq> carrier L" (* unneccessary with current Lower *)
   6.420 +  shows "greatest L x (Lower L A) = greatest L x' (Lower L A)"
   6.421 +  apply (rule greatest_cong) using assms by auto
   6.422 +
   6.423 +lemma (in weak_partial_order) greatest_Lower_cong_r:
   6.424 +  assumes Acarrs: "A \<subseteq> carrier L" "A' \<subseteq> carrier L"
   6.425 +    and AA': "A {.=} A'"
   6.426 +  shows "greatest L x (Lower L A) = greatest L x (Lower L A')"
   6.427 +apply (subgoal_tac "Lower L A = Lower L A'", simp)
   6.428 +by (rule Lower_cong) fact+
   6.429 +
   6.430  lemma greatest_LowerI:
   6.431    fixes L (structure)
   6.432    assumes below: "!! x. x \<in> A ==> i \<sqsubseteq> x"
   6.433 @@ -166,55 +392,116 @@
   6.434    ultimately show ?thesis by (simp add: greatest_def)
   6.435  qed
   6.436  
   6.437 -
   6.438 -subsection {* Lattices *}
   6.439 -
   6.440 -locale lattice = partial_order +
   6.441 -  assumes sup_of_two_exists:
   6.442 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   6.443 -    and inf_of_two_exists:
   6.444 -    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   6.445 -
   6.446 -lemma least_Upper_above:
   6.447 -  fixes L (structure)
   6.448 -  shows "[| least L s (Upper L A); x \<in> A; A \<subseteq> carrier L |] ==> x \<sqsubseteq> s"
   6.449 -  by (unfold least_def) blast
   6.450 -
   6.451  lemma greatest_Lower_below:
   6.452    fixes L (structure)
   6.453    shows "[| greatest L i (Lower L A); x \<in> A; A \<subseteq> carrier L |] ==> i \<sqsubseteq> x"
   6.454    by (unfold greatest_def) blast
   6.455  
   6.456 +text {* Supremum and infimum *}
   6.457 +
   6.458 +constdefs (structure L)
   6.459 +  sup :: "[_, 'a set] => 'a" ("\<Squnion>\<index>_" [90] 90)
   6.460 +  "\<Squnion>A == SOME x. least L x (Upper L A)"
   6.461 +
   6.462 +  inf :: "[_, 'a set] => 'a" ("\<Sqinter>\<index>_" [90] 90)
   6.463 +  "\<Sqinter>A == SOME x. greatest L x (Lower L A)"
   6.464 +
   6.465 +  join :: "[_, 'a, 'a] => 'a" (infixl "\<squnion>\<index>" 65)
   6.466 +  "x \<squnion> y == \<Squnion> {x, y}"
   6.467 +
   6.468 +  meet :: "[_, 'a, 'a] => 'a" (infixl "\<sqinter>\<index>" 70)
   6.469 +  "x \<sqinter> y == \<Sqinter> {x, y}"
   6.470 +
   6.471 +
   6.472 +subsection {* Lattices *}
   6.473 +
   6.474 +locale weak_upper_semilattice = weak_partial_order +
   6.475 +  assumes sup_of_two_exists:
   6.476 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
   6.477 +
   6.478 +locale weak_lower_semilattice = weak_partial_order +
   6.479 +  assumes inf_of_two_exists:
   6.480 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
   6.481 +
   6.482 +locale weak_lattice = weak_upper_semilattice + weak_lower_semilattice
   6.483 +
   6.484  
   6.485  subsubsection {* Supremum *}
   6.486  
   6.487 -lemma (in lattice) joinI:
   6.488 +lemma (in weak_upper_semilattice) joinI:
   6.489    "[| !!l. least L l (Upper L {x, y}) ==> P l; x \<in> carrier L; y \<in> carrier L |]
   6.490    ==> P (x \<squnion> y)"
   6.491  proof (unfold join_def sup_def)
   6.492    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   6.493      and P: "!!l. least L l (Upper L {x, y}) ==> P l"
   6.494    with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   6.495 -  with L show "P (THE l. least L l (Upper L {x, y}))"
   6.496 -    by (fast intro: theI2 least_unique P)
   6.497 +  with L show "P (SOME l. least L l (Upper L {x, y}))"
   6.498 +    by (fast intro: someI2 P)
   6.499  qed
   6.500  
   6.501 -lemma (in lattice) join_closed [simp]:
   6.502 +lemma (in weak_upper_semilattice) join_closed [simp]:
   6.503    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<squnion> y \<in> carrier L"
   6.504    by (rule joinI) (rule least_closed)
   6.505  
   6.506 -lemma (in partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   6.507 -  "x \<in> carrier L ==> least L x (Upper L {x})"
   6.508 -  by (rule least_UpperI) fast+
   6.509 +lemma (in weak_upper_semilattice) join_cong_l:
   6.510 +  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   6.511 +    and xx': "x .= x'"
   6.512 +  shows "x \<squnion> y .= x' \<squnion> y"
   6.513 +proof (rule joinI, rule joinI)
   6.514 +  fix a b
   6.515 +  from xx' carr
   6.516 +      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   6.517 +
   6.518 +  assume leasta: "least L a (Upper L {x, y})"
   6.519 +  assume "least L b (Upper L {x', y})"
   6.520 +  with carr
   6.521 +      have leastb: "least L b (Upper L {x, y})"
   6.522 +      by (simp add: least_Upper_cong_r[OF _ _ seq])
   6.523 +
   6.524 +  from leasta leastb
   6.525 +      show "a .= b" by (rule weak_least_unique)
   6.526 +qed (rule carr)+
   6.527  
   6.528 -lemma (in partial_order) sup_of_singleton [simp]:
   6.529 -  "x \<in> carrier L ==> \<Squnion>{x} = x"
   6.530 -  by (unfold sup_def) (blast intro: least_unique least_UpperI sup_of_singletonI)
   6.531 +lemma (in weak_upper_semilattice) join_cong_r:
   6.532 +  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   6.533 +    and yy': "y .= y'"
   6.534 +  shows "x \<squnion> y .= x \<squnion> y'"
   6.535 +proof (rule joinI, rule joinI)
   6.536 +  fix a b
   6.537 +  have "{x, y} = {y, x}" by fast
   6.538 +  also from carr yy'
   6.539 +      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   6.540 +  also have "{y', x} = {x, y'}" by fast
   6.541 +  finally
   6.542 +      have seq: "{x, y} {.=} {x, y'}" .
   6.543  
   6.544 +  assume leasta: "least L a (Upper L {x, y})"
   6.545 +  assume "least L b (Upper L {x, y'})"
   6.546 +  with carr
   6.547 +      have leastb: "least L b (Upper L {x, y})"
   6.548 +      by (simp add: least_Upper_cong_r[OF _ _ seq])
   6.549 +
   6.550 +  from leasta leastb
   6.551 +      show "a .= b" by (rule weak_least_unique)
   6.552 +qed (rule carr)+
   6.553 +
   6.554 +lemma (in weak_partial_order) sup_of_singletonI:      (* only reflexivity needed ? *)
   6.555 +  "x \<in> carrier L ==> least L x (Upper L {x})"
   6.556 +  by (rule least_UpperI) auto
   6.557 +
   6.558 +lemma (in weak_partial_order) weak_sup_of_singleton [simp]:
   6.559 +  "x \<in> carrier L ==> \<Squnion>{x} .= x"
   6.560 +  unfolding sup_def
   6.561 +  by (rule someI2) (auto intro: weak_least_unique sup_of_singletonI)
   6.562 +
   6.563 +lemma (in weak_partial_order) sup_of_singleton_closed [simp]:
   6.564 +  "x \<in> carrier L \<Longrightarrow> \<Squnion>{x} \<in> carrier L"
   6.565 +  unfolding sup_def
   6.566 +  by (rule someI2) (auto intro: sup_of_singletonI)
   6.567  
   6.568  text {* Condition on @{text A}: supremum exists. *}
   6.569  
   6.570 -lemma (in lattice) sup_insertI:
   6.571 +lemma (in weak_upper_semilattice) sup_insertI:
   6.572    "[| !!s. least L s (Upper L (insert x A)) ==> P s;
   6.573    least L a (Upper L A); x \<in> carrier L; A \<subseteq> carrier L |]
   6.574    ==> P (\<Squnion>(insert x A))"
   6.575 @@ -225,8 +512,8 @@
   6.576    from L least_a have La: "a \<in> carrier L" by simp
   6.577    from L sup_of_two_exists least_a
   6.578    obtain s where least_s: "least L s (Upper L {a, x})" by blast
   6.579 -  show "P (THE l. least L l (Upper L (insert x A)))"
   6.580 -  proof (rule theI2)
   6.581 +  show "P (SOME l. least L l (Upper L (insert x A)))"
   6.582 +  proof (rule someI2)
   6.583      show "least L s (Upper L (insert x A))"
   6.584      proof (rule least_UpperI)
   6.585        fix z
   6.586 @@ -238,7 +525,7 @@
   6.587        next
   6.588          assume "z \<in> A"
   6.589          with L least_s least_a show ?thesis
   6.590 -          by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   6.591 +          by (rule_tac le_trans [where y = a]) (auto dest: least_Upper_above)
   6.592        qed
   6.593      next
   6.594        fix y
   6.595 @@ -266,55 +553,10 @@
   6.596        from L show "insert x A \<subseteq> carrier L" by simp
   6.597        from least_s show "s \<in> carrier L" by simp
   6.598      qed
   6.599 -  next
   6.600 -    fix l
   6.601 -    assume least_l: "least L l (Upper L (insert x A))"
   6.602 -    show "l = s"
   6.603 -    proof (rule least_unique)
   6.604 -      show "least L s (Upper L (insert x A))"
   6.605 -      proof (rule least_UpperI)
   6.606 -        fix z
   6.607 -        assume "z \<in> insert x A"
   6.608 -        then show "z \<sqsubseteq> s"
   6.609 -	proof
   6.610 -          assume "z = x" then show ?thesis
   6.611 -            by (simp add: least_Upper_above [OF least_s] L La)
   6.612 -	next
   6.613 -          assume "z \<in> A"
   6.614 -          with L least_s least_a show ?thesis
   6.615 -            by (rule_tac trans [where y = a]) (auto dest: least_Upper_above)
   6.616 -	qed
   6.617 -      next
   6.618 -        fix y
   6.619 -        assume y: "y \<in> Upper L (insert x A)"
   6.620 -        show "s \<sqsubseteq> y"
   6.621 -        proof (rule least_le [OF least_s], rule Upper_memI)
   6.622 -          fix z
   6.623 -          assume z: "z \<in> {a, x}"
   6.624 -          then show "z \<sqsubseteq> y"
   6.625 -          proof
   6.626 -            have y': "y \<in> Upper L A"
   6.627 -	      apply (rule subsetD [where A = "Upper L (insert x A)"])
   6.628 -	      apply (rule Upper_antimono)
   6.629 -	       apply blast
   6.630 -	      apply (rule y)
   6.631 -	      done
   6.632 -            assume "z = a"
   6.633 -            with y' least_a show ?thesis by (fast dest: least_le)
   6.634 -	  next
   6.635 -            assume "z \<in> {x}"
   6.636 -            with y L show ?thesis by blast
   6.637 -          qed
   6.638 -        qed (rule Upper_closed [THEN subsetD, OF y])
   6.639 -      next
   6.640 -        from L show "insert x A \<subseteq> carrier L" by simp
   6.641 -        from least_s show "s \<in> carrier L" by simp
   6.642 -      qed
   6.643 -    qed (rule least_l)
   6.644    qed (rule P)
   6.645  qed
   6.646  
   6.647 -lemma (in lattice) finite_sup_least:
   6.648 +lemma (in weak_upper_semilattice) finite_sup_least:
   6.649    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> least L (\<Squnion>A) (Upper L A)"
   6.650  proof (induct set: finite)
   6.651    case empty
   6.652 @@ -324,7 +566,11 @@
   6.653    show ?case
   6.654    proof (cases "A = {}")
   6.655      case True
   6.656 -    with insert show ?thesis by (simp add: sup_of_singletonI)
   6.657 +    with insert show ?thesis
   6.658 +      by simp (simp add: least_cong [OF weak_sup_of_singleton]
   6.659 +	sup_of_singleton_closed sup_of_singletonI)
   6.660 +	(* The above step is hairy; least_cong can make simp loop.
   6.661 +	Would want special version of simp to apply least_cong. *)
   6.662    next
   6.663      case False
   6.664      with insert have "least L (\<Squnion>A) (Upper L A)" by simp
   6.665 @@ -333,19 +579,19 @@
   6.666    qed
   6.667  qed
   6.668  
   6.669 -lemma (in lattice) finite_sup_insertI:
   6.670 +lemma (in weak_upper_semilattice) finite_sup_insertI:
   6.671    assumes P: "!!l. least L l (Upper L (insert x A)) ==> P l"
   6.672      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   6.673    shows "P (\<Squnion> (insert x A))"
   6.674  proof (cases "A = {}")
   6.675    case True with P and xA show ?thesis
   6.676 -    by (simp add: sup_of_singletonI)
   6.677 +    by (simp add: finite_sup_least)
   6.678  next
   6.679    case False with P and xA show ?thesis
   6.680      by (simp add: sup_insertI finite_sup_least)
   6.681  qed
   6.682  
   6.683 -lemma (in lattice) finite_sup_closed:
   6.684 +lemma (in weak_upper_semilattice) finite_sup_closed [simp]:
   6.685    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Squnion>A \<in> carrier L"
   6.686  proof (induct set: finite)
   6.687    case empty then show ?case by simp
   6.688 @@ -354,24 +600,24 @@
   6.689      by - (rule finite_sup_insertI, simp_all)
   6.690  qed
   6.691  
   6.692 -lemma (in lattice) join_left:
   6.693 +lemma (in weak_upper_semilattice) join_left:
   6.694    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> x \<squnion> y"
   6.695    by (rule joinI [folded join_def]) (blast dest: least_mem)
   6.696  
   6.697 -lemma (in lattice) join_right:
   6.698 +lemma (in weak_upper_semilattice) join_right:
   6.699    "[| x \<in> carrier L; y \<in> carrier L |] ==> y \<sqsubseteq> x \<squnion> y"
   6.700    by (rule joinI [folded join_def]) (blast dest: least_mem)
   6.701  
   6.702 -lemma (in lattice) sup_of_two_least:
   6.703 +lemma (in weak_upper_semilattice) sup_of_two_least:
   6.704    "[| x \<in> carrier L; y \<in> carrier L |] ==> least L (\<Squnion>{x, y}) (Upper L {x, y})"
   6.705  proof (unfold sup_def)
   6.706    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   6.707    with sup_of_two_exists obtain s where "least L s (Upper L {x, y})" by fast
   6.708 -  with L show "least L (THE xa. least L xa (Upper L {x, y})) (Upper L {x, y})"
   6.709 -  by (fast intro: theI2 least_unique)  (* blast fails *)
   6.710 +  with L show "least L (SOME z. least L z (Upper L {x, y})) (Upper L {x, y})"
   6.711 +  by (fast intro: someI2 weak_least_unique)  (* blast fails *)
   6.712  qed
   6.713  
   6.714 -lemma (in lattice) join_le:
   6.715 +lemma (in weak_upper_semilattice) join_le:
   6.716    assumes sub: "x \<sqsubseteq> z"  "y \<sqsubseteq> z"
   6.717      and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
   6.718    shows "x \<squnion> y \<sqsubseteq> z"
   6.719 @@ -381,44 +627,48 @@
   6.720    with sub z show "s \<sqsubseteq> z" by (fast elim: least_le intro: Upper_memI)
   6.721  qed
   6.722  
   6.723 -lemma (in lattice) join_assoc_lemma:
   6.724 +lemma (in weak_upper_semilattice) weak_join_assoc_lemma:
   6.725    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   6.726 -  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
   6.727 +  shows "x \<squnion> (y \<squnion> z) .= \<Squnion>{x, y, z}"
   6.728  proof (rule finite_sup_insertI)
   6.729    -- {* The textbook argument in Jacobson I, p 457 *}
   6.730    fix s
   6.731    assume sup: "least L s (Upper L {x, y, z})"
   6.732 -  show "x \<squnion> (y \<squnion> z) = s"
   6.733 -  proof (rule anti_sym)
   6.734 +  show "x \<squnion> (y \<squnion> z) .= s"
   6.735 +  proof (rule weak_le_anti_sym)
   6.736      from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
   6.737        by (fastsimp intro!: join_le elim: least_Upper_above)
   6.738    next
   6.739      from sup L show "s \<sqsubseteq> x \<squnion> (y \<squnion> z)"
   6.740      by (erule_tac least_le)
   6.741 -      (blast intro!: Upper_memI intro: trans join_left join_right join_closed)
   6.742 +      (blast intro!: Upper_memI intro: le_trans join_left join_right join_closed)
   6.743    qed (simp_all add: L least_closed [OF sup])
   6.744  qed (simp_all add: L)
   6.745  
   6.746 +text {* Commutativity holds for @{text "="}. *}
   6.747 +
   6.748  lemma join_comm:
   6.749    fixes L (structure)
   6.750    shows "x \<squnion> y = y \<squnion> x"
   6.751    by (unfold join_def) (simp add: insert_commute)
   6.752  
   6.753 -lemma (in lattice) join_assoc:
   6.754 +lemma (in weak_upper_semilattice) weak_join_assoc:
   6.755    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
   6.756 -  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
   6.757 +  shows "(x \<squnion> y) \<squnion> z .= x \<squnion> (y \<squnion> z)"
   6.758  proof -
   6.759 +  (* FIXME: could be simplified by improved simp: uniform use of .=,
   6.760 +     omit [symmetric] in last step. *)
   6.761    have "(x \<squnion> y) \<squnion> z = z \<squnion> (x \<squnion> y)" by (simp only: join_comm)
   6.762 -  also from L have "... = \<Squnion>{z, x, y}" by (simp add: join_assoc_lemma)
   6.763 +  also from L have "... .= \<Squnion>{z, x, y}" by (simp add: weak_join_assoc_lemma)
   6.764    also from L have "... = \<Squnion>{x, y, z}" by (simp add: insert_commute)
   6.765 -  also from L have "... = x \<squnion> (y \<squnion> z)" by (simp add: join_assoc_lemma)
   6.766 -  finally show ?thesis .
   6.767 +  also from L have "... .= x \<squnion> (y \<squnion> z)" by (simp add: weak_join_assoc_lemma [symmetric])
   6.768 +  finally show ?thesis by (simp add: L)
   6.769  qed
   6.770  
   6.771  
   6.772  subsubsection {* Infimum *}
   6.773  
   6.774 -lemma (in lattice) meetI:
   6.775 +lemma (in weak_lower_semilattice) meetI:
   6.776    "[| !!i. greatest L i (Lower L {x, y}) ==> P i;
   6.777    x \<in> carrier L; y \<in> carrier L |]
   6.778    ==> P (x \<sqinter> y)"
   6.779 @@ -426,25 +676,73 @@
   6.780    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   6.781      and P: "!!g. greatest L g (Lower L {x, y}) ==> P g"
   6.782    with inf_of_two_exists obtain i where "greatest L i (Lower L {x, y})" by fast
   6.783 -  with L show "P (THE g. greatest L g (Lower L {x, y}))"
   6.784 -  by (fast intro: theI2 greatest_unique P)
   6.785 +  with L show "P (SOME g. greatest L g (Lower L {x, y}))"
   6.786 +  by (fast intro: someI2 weak_greatest_unique P)
   6.787  qed
   6.788  
   6.789 -lemma (in lattice) meet_closed [simp]:
   6.790 +lemma (in weak_lower_semilattice) meet_closed [simp]:
   6.791    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<in> carrier L"
   6.792    by (rule meetI) (rule greatest_closed)
   6.793  
   6.794 -lemma (in partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   6.795 -  "x \<in> carrier L ==> greatest L x (Lower L {x})"
   6.796 -  by (rule greatest_LowerI) fast+
   6.797 +lemma (in weak_lower_semilattice) meet_cong_l:
   6.798 +  assumes carr: "x \<in> carrier L" "x' \<in> carrier L" "y \<in> carrier L"
   6.799 +    and xx': "x .= x'"
   6.800 +  shows "x \<sqinter> y .= x' \<sqinter> y"
   6.801 +proof (rule meetI, rule meetI)
   6.802 +  fix a b
   6.803 +  from xx' carr
   6.804 +      have seq: "{x, y} {.=} {x', y}" by (rule set_eq_pairI)
   6.805 +
   6.806 +  assume greatesta: "greatest L a (Lower L {x, y})"
   6.807 +  assume "greatest L b (Lower L {x', y})"
   6.808 +  with carr
   6.809 +      have greatestb: "greatest L b (Lower L {x, y})"
   6.810 +      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   6.811 +
   6.812 +  from greatesta greatestb
   6.813 +      show "a .= b" by (rule weak_greatest_unique)
   6.814 +qed (rule carr)+
   6.815  
   6.816 -lemma (in partial_order) inf_of_singleton [simp]:
   6.817 -  "x \<in> carrier L ==> \<Sqinter> {x} = x"
   6.818 -  by (unfold inf_def) (blast intro: greatest_unique greatest_LowerI inf_of_singletonI)
   6.819 +lemma (in weak_lower_semilattice) meet_cong_r:
   6.820 +  assumes carr: "x \<in> carrier L" "y \<in> carrier L" "y' \<in> carrier L"
   6.821 +    and yy': "y .= y'"
   6.822 +  shows "x \<sqinter> y .= x \<sqinter> y'"
   6.823 +proof (rule meetI, rule meetI)
   6.824 +  fix a b
   6.825 +  have "{x, y} = {y, x}" by fast
   6.826 +  also from carr yy'
   6.827 +      have "{y, x} {.=} {y', x}" by (intro set_eq_pairI)
   6.828 +  also have "{y', x} = {x, y'}" by fast
   6.829 +  finally
   6.830 +      have seq: "{x, y} {.=} {x, y'}" .
   6.831 +
   6.832 +  assume greatesta: "greatest L a (Lower L {x, y})"
   6.833 +  assume "greatest L b (Lower L {x, y'})"
   6.834 +  with carr
   6.835 +      have greatestb: "greatest L b (Lower L {x, y})"
   6.836 +      by (simp add: greatest_Lower_cong_r[OF _ _ seq])
   6.837  
   6.838 -text {* Condition on A: infimum exists. *}
   6.839 +  from greatesta greatestb
   6.840 +      show "a .= b" by (rule weak_greatest_unique)
   6.841 +qed (rule carr)+
   6.842 +
   6.843 +lemma (in weak_partial_order) inf_of_singletonI:      (* only reflexivity needed ? *)
   6.844 +  "x \<in> carrier L ==> greatest L x (Lower L {x})"
   6.845 +  by (rule greatest_LowerI) auto
   6.846  
   6.847 -lemma (in lattice) inf_insertI:
   6.848 +lemma (in weak_partial_order) weak_inf_of_singleton [simp]:
   6.849 +  "x \<in> carrier L ==> \<Sqinter>{x} .= x"
   6.850 +  unfolding inf_def
   6.851 +  by (rule someI2) (auto intro: weak_greatest_unique inf_of_singletonI)
   6.852 +
   6.853 +lemma (in weak_partial_order) inf_of_singleton_closed:
   6.854 +  "x \<in> carrier L ==> \<Sqinter>{x} \<in> carrier L"
   6.855 +  unfolding inf_def
   6.856 +  by (rule someI2) (auto intro: inf_of_singletonI)
   6.857 +
   6.858 +text {* Condition on @{text A}: infimum exists. *}
   6.859 +
   6.860 +lemma (in weak_lower_semilattice) inf_insertI:
   6.861    "[| !!i. greatest L i (Lower L (insert x A)) ==> P i;
   6.862    greatest L a (Lower L A); x \<in> carrier L; A \<subseteq> carrier L |]
   6.863    ==> P (\<Sqinter>(insert x A))"
   6.864 @@ -455,8 +753,8 @@
   6.865    from L greatest_a have La: "a \<in> carrier L" by simp
   6.866    from L inf_of_two_exists greatest_a
   6.867    obtain i where greatest_i: "greatest L i (Lower L {a, x})" by blast
   6.868 -  show "P (THE g. greatest L g (Lower L (insert x A)))"
   6.869 -  proof (rule theI2)
   6.870 +  show "P (SOME g. greatest L g (Lower L (insert x A)))"
   6.871 +  proof (rule someI2)
   6.872      show "greatest L i (Lower L (insert x A))"
   6.873      proof (rule greatest_LowerI)
   6.874        fix z
   6.875 @@ -468,7 +766,7 @@
   6.876        next
   6.877          assume "z \<in> A"
   6.878          with L greatest_i greatest_a show ?thesis
   6.879 -          by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
   6.880 +          by (rule_tac le_trans [where y = a]) (auto dest: greatest_Lower_below)
   6.881        qed
   6.882      next
   6.883        fix y
   6.884 @@ -496,55 +794,10 @@
   6.885        from L show "insert x A \<subseteq> carrier L" by simp
   6.886        from greatest_i show "i \<in> carrier L" by simp
   6.887      qed
   6.888 -  next
   6.889 -    fix g
   6.890 -    assume greatest_g: "greatest L g (Lower L (insert x A))"
   6.891 -    show "g = i"
   6.892 -    proof (rule greatest_unique)
   6.893 -      show "greatest L i (Lower L (insert x A))"
   6.894 -      proof (rule greatest_LowerI)
   6.895 -        fix z
   6.896 -        assume "z \<in> insert x A"
   6.897 -        then show "i \<sqsubseteq> z"
   6.898 -	proof
   6.899 -          assume "z = x" then show ?thesis
   6.900 -            by (simp add: greatest_Lower_below [OF greatest_i] L La)
   6.901 -	next
   6.902 -          assume "z \<in> A"
   6.903 -          with L greatest_i greatest_a show ?thesis
   6.904 -            by (rule_tac trans [where y = a]) (auto dest: greatest_Lower_below)
   6.905 -        qed
   6.906 -      next
   6.907 -        fix y
   6.908 -        assume y: "y \<in> Lower L (insert x A)"
   6.909 -        show "y \<sqsubseteq> i"
   6.910 -        proof (rule greatest_le [OF greatest_i], rule Lower_memI)
   6.911 -          fix z
   6.912 -          assume z: "z \<in> {a, x}"
   6.913 -          then show "y \<sqsubseteq> z"
   6.914 -          proof
   6.915 -            have y': "y \<in> Lower L A"
   6.916 -	      apply (rule subsetD [where A = "Lower L (insert x A)"])
   6.917 -	      apply (rule Lower_antimono)
   6.918 -	       apply blast
   6.919 -	      apply (rule y)
   6.920 -	      done
   6.921 -            assume "z = a"
   6.922 -            with y' greatest_a show ?thesis by (fast dest: greatest_le)
   6.923 -	  next
   6.924 -            assume "z \<in> {x}"
   6.925 -            with y L show ?thesis by blast
   6.926 -	  qed
   6.927 -        qed (rule Lower_closed [THEN subsetD, OF y])
   6.928 -      next
   6.929 -        from L show "insert x A \<subseteq> carrier L" by simp
   6.930 -        from greatest_i show "i \<in> carrier L" by simp
   6.931 -      qed
   6.932 -    qed (rule greatest_g)
   6.933    qed (rule P)
   6.934  qed
   6.935  
   6.936 -lemma (in lattice) finite_inf_greatest:
   6.937 +lemma (in weak_lower_semilattice) finite_inf_greatest:
   6.938    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> greatest L (\<Sqinter>A) (Lower L A)"
   6.939  proof (induct set: finite)
   6.940    case empty then show ?case by simp
   6.941 @@ -553,7 +806,9 @@
   6.942    show ?case
   6.943    proof (cases "A = {}")
   6.944      case True
   6.945 -    with insert show ?thesis by (simp add: inf_of_singletonI)
   6.946 +    with insert show ?thesis
   6.947 +      by simp (simp add: greatest_cong [OF weak_inf_of_singleton]
   6.948 +	inf_of_singleton_closed inf_of_singletonI)
   6.949    next
   6.950      case False
   6.951      from insert show ?thesis
   6.952 @@ -563,19 +818,19 @@
   6.953    qed
   6.954  qed
   6.955  
   6.956 -lemma (in lattice) finite_inf_insertI:
   6.957 +lemma (in weak_lower_semilattice) finite_inf_insertI:
   6.958    assumes P: "!!i. greatest L i (Lower L (insert x A)) ==> P i"
   6.959      and xA: "finite A"  "x \<in> carrier L"  "A \<subseteq> carrier L"
   6.960    shows "P (\<Sqinter> (insert x A))"
   6.961  proof (cases "A = {}")
   6.962    case True with P and xA show ?thesis
   6.963 -    by (simp add: inf_of_singletonI)
   6.964 +    by (simp add: finite_inf_greatest)
   6.965  next
   6.966    case False with P and xA show ?thesis
   6.967      by (simp add: inf_insertI finite_inf_greatest)
   6.968  qed
   6.969  
   6.970 -lemma (in lattice) finite_inf_closed:
   6.971 +lemma (in weak_lower_semilattice) finite_inf_closed [simp]:
   6.972    "[| finite A; A \<subseteq> carrier L; A ~= {} |] ==> \<Sqinter>A \<in> carrier L"
   6.973  proof (induct set: finite)
   6.974    case empty then show ?case by simp
   6.975 @@ -584,26 +839,26 @@
   6.976      by (rule_tac finite_inf_insertI) (simp_all)
   6.977  qed
   6.978  
   6.979 -lemma (in lattice) meet_left:
   6.980 +lemma (in weak_lower_semilattice) meet_left:
   6.981    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> x"
   6.982    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   6.983  
   6.984 -lemma (in lattice) meet_right:
   6.985 +lemma (in weak_lower_semilattice) meet_right:
   6.986    "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqinter> y \<sqsubseteq> y"
   6.987    by (rule meetI [folded meet_def]) (blast dest: greatest_mem)
   6.988  
   6.989 -lemma (in lattice) inf_of_two_greatest:
   6.990 +lemma (in weak_lower_semilattice) inf_of_two_greatest:
   6.991    "[| x \<in> carrier L; y \<in> carrier L |] ==>
   6.992    greatest L (\<Sqinter> {x, y}) (Lower L {x, y})"
   6.993  proof (unfold inf_def)
   6.994    assume L: "x \<in> carrier L"  "y \<in> carrier L"
   6.995    with inf_of_two_exists obtain s where "greatest L s (Lower L {x, y})" by fast
   6.996    with L
   6.997 -  show "greatest L (THE xa. greatest L xa (Lower L {x, y})) (Lower L {x, y})"
   6.998 -  by (fast intro: theI2 greatest_unique)  (* blast fails *)
   6.999 +  show "greatest L (SOME z. greatest L z (Lower L {x, y})) (Lower L {x, y})"
  6.1000 +  by (fast intro: someI2 weak_greatest_unique)  (* blast fails *)
  6.1001  qed
  6.1002  
  6.1003 -lemma (in lattice) meet_le:
  6.1004 +lemma (in weak_lower_semilattice) meet_le:
  6.1005    assumes sub: "z \<sqsubseteq> x"  "z \<sqsubseteq> y"
  6.1006      and x: "x \<in> carrier L" and y: "y \<in> carrier L" and z: "z \<in> carrier L"
  6.1007    shows "z \<sqsubseteq> x \<sqinter> y"
  6.1008 @@ -613,21 +868,21 @@
  6.1009    with sub z show "z \<sqsubseteq> i" by (fast elim: greatest_le intro: Lower_memI)
  6.1010  qed
  6.1011  
  6.1012 -lemma (in lattice) meet_assoc_lemma:
  6.1013 +lemma (in weak_lower_semilattice) weak_meet_assoc_lemma:
  6.1014    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1015 -  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
  6.1016 +  shows "x \<sqinter> (y \<sqinter> z) .= \<Sqinter>{x, y, z}"
  6.1017  proof (rule finite_inf_insertI)
  6.1018    txt {* The textbook argument in Jacobson I, p 457 *}
  6.1019    fix i
  6.1020    assume inf: "greatest L i (Lower L {x, y, z})"
  6.1021 -  show "x \<sqinter> (y \<sqinter> z) = i"
  6.1022 -  proof (rule anti_sym)
  6.1023 +  show "x \<sqinter> (y \<sqinter> z) .= i"
  6.1024 +  proof (rule weak_le_anti_sym)
  6.1025      from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
  6.1026        by (fastsimp intro!: meet_le elim: greatest_Lower_below)
  6.1027    next
  6.1028      from inf L show "x \<sqinter> (y \<sqinter> z) \<sqsubseteq> i"
  6.1029      by (erule_tac greatest_le)
  6.1030 -      (blast intro!: Lower_memI intro: trans meet_left meet_right meet_closed)
  6.1031 +      (blast intro!: Lower_memI intro: le_trans meet_left meet_right meet_closed)
  6.1032    qed (simp_all add: L greatest_closed [OF inf])
  6.1033  qed (simp_all add: L)
  6.1034  
  6.1035 @@ -636,33 +891,34 @@
  6.1036    shows "x \<sqinter> y = y \<sqinter> x"
  6.1037    by (unfold meet_def) (simp add: insert_commute)
  6.1038  
  6.1039 -lemma (in lattice) meet_assoc:
  6.1040 +lemma (in weak_lower_semilattice) weak_meet_assoc:
  6.1041    assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1042 -  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
  6.1043 +  shows "(x \<sqinter> y) \<sqinter> z .= x \<sqinter> (y \<sqinter> z)"
  6.1044  proof -
  6.1045 +  (* FIXME: improved simp, see weak_join_assoc above *)
  6.1046    have "(x \<sqinter> y) \<sqinter> z = z \<sqinter> (x \<sqinter> y)" by (simp only: meet_comm)
  6.1047 -  also from L have "... = \<Sqinter> {z, x, y}" by (simp add: meet_assoc_lemma)
  6.1048 +  also from L have "... .= \<Sqinter> {z, x, y}" by (simp add: weak_meet_assoc_lemma)
  6.1049    also from L have "... = \<Sqinter> {x, y, z}" by (simp add: insert_commute)
  6.1050 -  also from L have "... = x \<sqinter> (y \<sqinter> z)" by (simp add: meet_assoc_lemma)
  6.1051 -  finally show ?thesis .
  6.1052 +  also from L have "... .= x \<sqinter> (y \<sqinter> z)" by (simp add: weak_meet_assoc_lemma [symmetric])
  6.1053 +  finally show ?thesis by (simp add: L)
  6.1054  qed
  6.1055  
  6.1056  
  6.1057  subsection {* Total Orders *}
  6.1058  
  6.1059 -locale total_order = partial_order +
  6.1060 +locale weak_total_order = weak_partial_order +
  6.1061    assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  6.1062  
  6.1063  text {* Introduction rule: the usual definition of total order *}
  6.1064  
  6.1065 -lemma (in partial_order) total_orderI:
  6.1066 +lemma (in weak_partial_order) weak_total_orderI:
  6.1067    assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  6.1068 -  shows "total_order L"
  6.1069 +  shows "weak_total_order L"
  6.1070    by unfold_locales (rule total)
  6.1071  
  6.1072  text {* Total orders are lattices. *}
  6.1073  
  6.1074 -interpretation total_order < lattice
  6.1075 +interpretation weak_total_order < weak_lattice
  6.1076  proof unfold_locales
  6.1077    fix x y
  6.1078    assume L: "x \<in> carrier L"  "y \<in> carrier L"
  6.1079 @@ -708,7 +964,7 @@
  6.1080  
  6.1081  subsection {* Complete lattices *}
  6.1082  
  6.1083 -locale complete_lattice = lattice +
  6.1084 +locale weak_complete_lattice = weak_lattice +
  6.1085    assumes sup_exists:
  6.1086      "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  6.1087      and inf_exists:
  6.1088 @@ -716,16 +972,13 @@
  6.1089  
  6.1090  text {* Introduction rule: the usual definition of complete lattice *}
  6.1091  
  6.1092 -lemma (in partial_order) complete_latticeI:
  6.1093 +lemma (in weak_partial_order) weak_complete_latticeI:
  6.1094    assumes sup_exists:
  6.1095      "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  6.1096      and inf_exists:
  6.1097      "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  6.1098 -  shows "complete_lattice L"
  6.1099 -proof intro_locales
  6.1100 -  show "lattice_axioms L"
  6.1101 -    by (rule lattice_axioms.intro) (blast intro: sup_exists inf_exists)+
  6.1102 -qed (rule complete_lattice_axioms.intro sup_exists inf_exists | assumption)+
  6.1103 +  shows "weak_complete_lattice L"
  6.1104 +  by unfold_locales (auto intro: sup_exists inf_exists)
  6.1105  
  6.1106  constdefs (structure L)
  6.1107    top :: "_ => 'a" ("\<top>\<index>")
  6.1108 @@ -735,41 +988,41 @@
  6.1109    "\<bottom> == inf L (carrier L)"
  6.1110  
  6.1111  
  6.1112 -lemma (in complete_lattice) supI:
  6.1113 +lemma (in weak_complete_lattice) supI:
  6.1114    "[| !!l. least L l (Upper L A) ==> P l; A \<subseteq> carrier L |]
  6.1115    ==> P (\<Squnion>A)"
  6.1116  proof (unfold sup_def)
  6.1117    assume L: "A \<subseteq> carrier L"
  6.1118      and P: "!!l. least L l (Upper L A) ==> P l"
  6.1119    with sup_exists obtain s where "least L s (Upper L A)" by blast
  6.1120 -  with L show "P (THE l. least L l (Upper L A))"
  6.1121 -  by (fast intro: theI2 least_unique P)
  6.1122 +  with L show "P (SOME l. least L l (Upper L A))"
  6.1123 +  by (fast intro: someI2 weak_least_unique P)
  6.1124  qed
  6.1125  
  6.1126 -lemma (in complete_lattice) sup_closed [simp]:
  6.1127 +lemma (in weak_complete_lattice) sup_closed [simp]:
  6.1128    "A \<subseteq> carrier L ==> \<Squnion>A \<in> carrier L"
  6.1129    by (rule supI) simp_all
  6.1130  
  6.1131 -lemma (in complete_lattice) top_closed [simp, intro]:
  6.1132 +lemma (in weak_complete_lattice) top_closed [simp, intro]:
  6.1133    "\<top> \<in> carrier L"
  6.1134    by (unfold top_def) simp
  6.1135  
  6.1136 -lemma (in complete_lattice) infI:
  6.1137 +lemma (in weak_complete_lattice) infI:
  6.1138    "[| !!i. greatest L i (Lower L A) ==> P i; A \<subseteq> carrier L |]
  6.1139    ==> P (\<Sqinter>A)"
  6.1140  proof (unfold inf_def)
  6.1141    assume L: "A \<subseteq> carrier L"
  6.1142      and P: "!!l. greatest L l (Lower L A) ==> P l"
  6.1143    with inf_exists obtain s where "greatest L s (Lower L A)" by blast
  6.1144 -  with L show "P (THE l. greatest L l (Lower L A))"
  6.1145 -  by (fast intro: theI2 greatest_unique P)
  6.1146 +  with L show "P (SOME l. greatest L l (Lower L A))"
  6.1147 +  by (fast intro: someI2 weak_greatest_unique P)
  6.1148  qed
  6.1149  
  6.1150 -lemma (in complete_lattice) inf_closed [simp]:
  6.1151 +lemma (in weak_complete_lattice) inf_closed [simp]:
  6.1152    "A \<subseteq> carrier L ==> \<Sqinter>A \<in> carrier L"
  6.1153    by (rule infI) simp_all
  6.1154  
  6.1155 -lemma (in complete_lattice) bottom_closed [simp, intro]:
  6.1156 +lemma (in weak_complete_lattice) bottom_closed [simp, intro]:
  6.1157    "\<bottom> \<in> carrier L"
  6.1158    by (unfold bottom_def) simp
  6.1159  
  6.1160 @@ -783,6 +1036,216 @@
  6.1161    "Upper L {} = carrier L"
  6.1162    by (unfold Upper_def) simp
  6.1163  
  6.1164 +theorem (in weak_partial_order) weak_complete_lattice_criterion1:
  6.1165 +  assumes top_exists: "EX g. greatest L g (carrier L)"
  6.1166 +    and inf_exists:
  6.1167 +      "!!A. [| A \<subseteq> carrier L; A ~= {} |] ==> EX i. greatest L i (Lower L A)"
  6.1168 +  shows "weak_complete_lattice L"
  6.1169 +proof (rule weak_complete_latticeI)
  6.1170 +  from top_exists obtain top where top: "greatest L top (carrier L)" ..
  6.1171 +  fix A
  6.1172 +  assume L: "A \<subseteq> carrier L"
  6.1173 +  let ?B = "Upper L A"
  6.1174 +  from L top have "top \<in> ?B" by (fast intro!: Upper_memI intro: greatest_le)
  6.1175 +  then have B_non_empty: "?B ~= {}" by fast
  6.1176 +  have B_L: "?B \<subseteq> carrier L" by simp
  6.1177 +  from inf_exists [OF B_L B_non_empty]
  6.1178 +  obtain b where b_inf_B: "greatest L b (Lower L ?B)" ..
  6.1179 +  have "least L b (Upper L A)"
  6.1180 +apply (rule least_UpperI)
  6.1181 +   apply (rule greatest_le [where A = "Lower L ?B"])
  6.1182 +    apply (rule b_inf_B)
  6.1183 +   apply (rule Lower_memI)
  6.1184 +    apply (erule Upper_memD [THEN conjunct1])
  6.1185 +     apply assumption
  6.1186 +    apply (rule L)
  6.1187 +   apply (fast intro: L [THEN subsetD])
  6.1188 +  apply (erule greatest_Lower_below [OF b_inf_B])
  6.1189 +  apply simp
  6.1190 + apply (rule L)
  6.1191 +apply (rule greatest_closed [OF b_inf_B])
  6.1192 +done
  6.1193 +  then show "EX s. least L s (Upper L A)" ..
  6.1194 +next
  6.1195 +  fix A
  6.1196 +  assume L: "A \<subseteq> carrier L"
  6.1197 +  show "EX i. greatest L i (Lower L A)"
  6.1198 +  proof (cases "A = {}")
  6.1199 +    case True then show ?thesis
  6.1200 +      by (simp add: top_exists)
  6.1201 +  next
  6.1202 +    case False with L show ?thesis
  6.1203 +      by (rule inf_exists)
  6.1204 +  qed
  6.1205 +qed
  6.1206 +
  6.1207 +(* TODO: prove dual version *)
  6.1208 +
  6.1209 +
  6.1210 +subsection {* Orders and Lattices where @{text eq} is the Equality *}
  6.1211 +
  6.1212 +locale partial_order = weak_partial_order +
  6.1213 +  assumes eq_is_equal: "op .= = op ="
  6.1214 +begin
  6.1215 +
  6.1216 +declare weak_le_anti_sym [rule del]
  6.1217 +
  6.1218 +lemma le_anti_sym [intro]:
  6.1219 +  "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
  6.1220 +  using weak_le_anti_sym unfolding eq_is_equal .
  6.1221 +
  6.1222 +lemma lless_eq:
  6.1223 +  "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
  6.1224 +  unfolding lless_def by (simp add: eq_is_equal)
  6.1225 +
  6.1226 +lemma lless_asym:
  6.1227 +  assumes "a \<in> carrier L" "b \<in> carrier L"
  6.1228 +    and "a \<sqsubset> b" "b \<sqsubset> a"
  6.1229 +  shows "P"
  6.1230 +  using assms unfolding lless_eq by auto
  6.1231 +
  6.1232 +lemma lless_trans [trans]:
  6.1233 +  assumes "a \<sqsubset> b" "b \<sqsubset> c"
  6.1234 +    and carr[simp]: "a \<in> carrier L" "b \<in> carrier L" "c \<in> carrier L"
  6.1235 +  shows "a \<sqsubset> c"
  6.1236 +  using assms unfolding lless_eq by (blast dest: le_trans intro: sym)
  6.1237 +
  6.1238 +end
  6.1239 +
  6.1240 +
  6.1241 +subsubsection {* Upper and lower bounds of a set *}
  6.1242 +
  6.1243 +(* all relevant lemmas are global and already proved above *)
  6.1244 +
  6.1245 +
  6.1246 +subsubsection {* Least and greatest, as predicate *}
  6.1247 +
  6.1248 +lemma (in partial_order) least_unique:
  6.1249 +  "[| least L x A; least L y A |] ==> x = y"
  6.1250 +  using weak_least_unique unfolding eq_is_equal .
  6.1251 +
  6.1252 +lemma (in partial_order) greatest_unique:
  6.1253 +  "[| greatest L x A; greatest L y A |] ==> x = y"
  6.1254 +  using weak_greatest_unique unfolding eq_is_equal .
  6.1255 +
  6.1256 +
  6.1257 +subsection {* Lattices *}
  6.1258 +
  6.1259 +locale upper_semilattice = partial_order +
  6.1260 +  assumes sup_of_two_exists:
  6.1261 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. least L s (Upper L {x, y})"
  6.1262 +
  6.1263 +interpretation upper_semilattice < weak_upper_semilattice
  6.1264 +  by unfold_locales (rule sup_of_two_exists)
  6.1265 +
  6.1266 +locale lower_semilattice = partial_order +
  6.1267 +  assumes inf_of_two_exists:
  6.1268 +    "[| x \<in> carrier L; y \<in> carrier L |] ==> EX s. greatest L s (Lower L {x, y})"
  6.1269 +
  6.1270 +interpretation lower_semilattice < weak_lower_semilattice
  6.1271 +  by unfold_locales (rule inf_of_two_exists)
  6.1272 +
  6.1273 +locale lattice = upper_semilattice + lower_semilattice
  6.1274 +
  6.1275 +
  6.1276 +subsubsection {* Supremum *}
  6.1277 +
  6.1278 +context partial_order begin
  6.1279 +
  6.1280 +declare weak_sup_of_singleton [simp del]
  6.1281 +
  6.1282 +lemma sup_of_singleton [simp]:
  6.1283 +  "x \<in> carrier L ==> \<Squnion>{x} = x"
  6.1284 +  using weak_sup_of_singleton unfolding eq_is_equal .
  6.1285 +
  6.1286 +end
  6.1287 +
  6.1288 +context upper_semilattice begin
  6.1289 +
  6.1290 +lemma join_assoc_lemma:
  6.1291 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1292 +  shows "x \<squnion> (y \<squnion> z) = \<Squnion>{x, y, z}"
  6.1293 +  using weak_join_assoc_lemma unfolding eq_is_equal .
  6.1294 +
  6.1295 +end
  6.1296 +
  6.1297 +lemma (in upper_semilattice) join_assoc:
  6.1298 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1299 +  shows "(x \<squnion> y) \<squnion> z = x \<squnion> (y \<squnion> z)"
  6.1300 +  using weak_join_assoc unfolding eq_is_equal .
  6.1301 +
  6.1302 +
  6.1303 +subsubsection {* Infimum *}
  6.1304 +
  6.1305 +context partial_order begin
  6.1306 +
  6.1307 +declare weak_inf_of_singleton [simp del]
  6.1308 +
  6.1309 +lemma inf_of_singleton [simp]:
  6.1310 +  "x \<in> carrier L ==> \<Sqinter>{x} = x"
  6.1311 +  using weak_inf_of_singleton unfolding eq_is_equal .
  6.1312 +
  6.1313 +end
  6.1314 +
  6.1315 +context lower_semilattice begin
  6.1316 +
  6.1317 +text {* Condition on @{text A}: infimum exists. *}
  6.1318 +
  6.1319 +lemma meet_assoc_lemma:
  6.1320 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1321 +  shows "x \<sqinter> (y \<sqinter> z) = \<Sqinter>{x, y, z}"
  6.1322 +  using weak_meet_assoc_lemma unfolding eq_is_equal .
  6.1323 +
  6.1324 +end
  6.1325 +
  6.1326 +lemma (in lower_semilattice) meet_assoc:
  6.1327 +  assumes L: "x \<in> carrier L"  "y \<in> carrier L"  "z \<in> carrier L"
  6.1328 +  shows "(x \<sqinter> y) \<sqinter> z = x \<sqinter> (y \<sqinter> z)"
  6.1329 +  using weak_meet_assoc unfolding eq_is_equal .
  6.1330 +
  6.1331 +
  6.1332 +subsection {* Total Orders *}
  6.1333 +
  6.1334 +locale total_order = partial_order +
  6.1335 +  assumes total: "[| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  6.1336 +
  6.1337 +interpretation total_order < weak_total_order
  6.1338 +  by unfold_locales (rule total)
  6.1339 +
  6.1340 +text {* Introduction rule: the usual definition of total order *}
  6.1341 +
  6.1342 +lemma (in partial_order) total_orderI:
  6.1343 +  assumes total: "!!x y. [| x \<in> carrier L; y \<in> carrier L |] ==> x \<sqsubseteq> y | y \<sqsubseteq> x"
  6.1344 +  shows "total_order L"
  6.1345 +  by unfold_locales (rule total)
  6.1346 +
  6.1347 +text {* Total orders are lattices. *}
  6.1348 +
  6.1349 +interpretation total_order < lattice
  6.1350 +  by unfold_locales (auto intro: sup_of_two_exists inf_of_two_exists)
  6.1351 +
  6.1352 +
  6.1353 +subsection {* Complete lattices *}
  6.1354 +
  6.1355 +locale complete_lattice = lattice +
  6.1356 +  assumes sup_exists:
  6.1357 +    "[| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  6.1358 +    and inf_exists:
  6.1359 +    "[| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  6.1360 +
  6.1361 +interpretation complete_lattice < weak_complete_lattice
  6.1362 +  by unfold_locales (auto intro: sup_exists inf_exists)
  6.1363 +
  6.1364 +text {* Introduction rule: the usual definition of complete lattice *}
  6.1365 +
  6.1366 +lemma (in partial_order) complete_latticeI:
  6.1367 +  assumes sup_exists:
  6.1368 +    "!!A. [| A \<subseteq> carrier L |] ==> EX s. least L s (Upper L A)"
  6.1369 +    and inf_exists:
  6.1370 +    "!!A. [| A \<subseteq> carrier L |] ==> EX i. greatest L i (Lower L A)"
  6.1371 +  shows "complete_lattice L"
  6.1372 +  by unfold_locales (auto intro: sup_exists inf_exists)
  6.1373 +
  6.1374  theorem (in partial_order) complete_lattice_criterion1:
  6.1375    assumes top_exists: "EX g. greatest L g (carrier L)"
  6.1376      and inf_exists:
  6.1377 @@ -803,7 +1266,7 @@
  6.1378     apply (rule greatest_le [where A = "Lower L ?B"])
  6.1379      apply (rule b_inf_B)
  6.1380     apply (rule Lower_memI)
  6.1381 -    apply (erule Upper_memD)
  6.1382 +    apply (erule Upper_memD [THEN conjunct1])
  6.1383       apply assumption
  6.1384      apply (rule L)
  6.1385     apply (fast intro: L [THEN subsetD])
  6.1386 @@ -834,11 +1297,11 @@
  6.1387  subsubsection {* Powerset of a Set is a Complete Lattice *}
  6.1388  
  6.1389  theorem powerset_is_complete_lattice:
  6.1390 -  "complete_lattice (| carrier = Pow A, le = op \<subseteq> |)"
  6.1391 +  "complete_lattice (| carrier = Pow A, eq = op =, le = op \<subseteq> |)"
  6.1392    (is "complete_lattice ?L")
  6.1393  proof (rule partial_order.complete_latticeI)
  6.1394    show "partial_order ?L"
  6.1395 -    by (rule partial_order.intro) auto
  6.1396 +    by unfold_locales auto
  6.1397  next
  6.1398    fix B
  6.1399    assume B: "B \<subseteq> carrier ?L"
     7.1 --- a/src/HOL/Algebra/ROOT.ML	Wed Jul 30 16:07:00 2008 +0200
     7.2 +++ b/src/HOL/Algebra/ROOT.ML	Wed Jul 30 19:03:33 2008 +0200
     7.3 @@ -5,7 +5,7 @@
     7.4  *)
     7.5  
     7.6  (* Preliminaries from set and number theory *)
     7.7 -no_document use_thys ["FuncSet", "Primes", "Binomial"];
     7.8 +no_document use_thys ["FuncSet", "Primes", "Binomial", "Permutation"];
     7.9  
    7.10  
    7.11  (*** New development, based on explicit structures ***)
    7.12 @@ -17,8 +17,9 @@
    7.13    "Bij",                (* Automorphism Groups *)
    7.14  
    7.15    (* Rings *)
    7.16 -  "UnivPoly",           (* Rings and polynomials *)
    7.17 -  "IntRing"             (* Ideals and residue classes *)
    7.18 +  "Divisibility",       (* Rings *)
    7.19 +  "IntRing",            (* Ideals and residue classes *)
    7.20 +  "UnivPoly"            (* Polynomials *)
    7.21  ];
    7.22  
    7.23  
     8.1 --- a/src/HOL/IsaMakefile	Wed Jul 30 16:07:00 2008 +0200
     8.2 +++ b/src/HOL/IsaMakefile	Wed Jul 30 19:03:33 2008 +0200
     8.3 @@ -509,7 +509,7 @@
     8.4    Library/Multiset.thy Library/Permutation.thy Library/Primes.thy	\
     8.5    Algebra/AbelCoset.thy Algebra/Bij.thy	Algebra/Congruence.thy		\
     8.6    Algebra/Coset.thy Algebra/Divisibility.thy Algebra/Exponent.thy	\
     8.7 -  Algebra/FiniteProduct.thy Algebra/GLattice.thy			\
     8.8 +  Algebra/FiniteProduct.thy						\
     8.9    Algebra/Group.thy Algebra/Ideal.thy Algebra/IntRing.thy		\
    8.10    Algebra/Lattice.thy Algebra/Module.thy Algebra/QuotRing.thy		\
    8.11    Algebra/Ring.thy Algebra/RingHom.thy Algebra/Sylow.thy		\