# HG changeset patch
# User nipkow
# Date 1165752883 -3600
# Node ID 283461c15fa70fefdfa3a427efa1159a56b960fc
# Parent  131dd2a271370ffc34dc7d0ee6c0c2ac5dfcc953
renaming

diff -r 131dd2a27137 -r 283461c15fa7 src/HOL/LOrder.thy
--- a/src/HOL/LOrder.thy	Sun Dec 10 07:12:26 2006 +0100
+++ b/src/HOL/LOrder.thy	Sun Dec 10 13:14:43 2006 +0100
@@ -1,6 +1,11 @@
 (*  Title:   HOL/LOrder.thy
     ID:      $Id$
     Author:  Steven Obua, TU Muenchen
+
+FIXME integrate properly with lattice locales
+- make it a class?
+- get rid of the implicit there-is-a-meet/join but require eplicit ops.
+Also rename meet/join to inf/sup. 
 *)
 
 header "Lattice Orders"
@@ -114,7 +119,7 @@
 
 declare
  join_semilat.antisym_intro[rule del] meet_semilat.antisym_intro[rule del]
- join_semilat.less_eq_supE[rule del] meet_semilat.less_eq_infE[rule del]
+ join_semilat.le_supE[rule del] meet_semilat.le_infE[rule del]
 
 interpretation meet_join_lat:
   lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
@@ -122,17 +127,17 @@
 
 lemmas meet_left_le = meet_semilat.inf_le1
 lemmas meet_right_le = meet_semilat.inf_le2
-lemmas le_meetI[rule del] = meet_semilat.less_eq_infI
+lemmas le_meetI[rule del] = meet_semilat.le_infI
 (* intro! breaks a proof in Hyperreal/SEQ and NumberTheory/IntPrimes *)
 lemmas join_left_le = join_semilat.sup_ge1
 lemmas join_right_le = join_semilat.sup_ge2
-lemmas join_leI[rule del] = join_semilat.less_eq_supI
+lemmas join_leI[rule del] = join_semilat.le_supI
 
 lemmas meet_join_le = meet_left_le meet_right_le join_left_le join_right_le
 
-lemmas le_meet = meet_semilat.less_eq_inf_conv
+lemmas le_meet = meet_semilat.le_inf_iff
 
-lemmas le_join = join_semilat.above_sup_conv
+lemmas le_join = join_semilat.ge_sup_conv
 
 lemma is_meet_min: "is_meet (min::'a \<Rightarrow> 'a \<Rightarrow> ('a::linorder))"
 by (auto simp add: is_meet_def min_def)
@@ -162,10 +167,10 @@
 lemmas join_idempotent = join_semilat.sup_idem
 lemmas meet_comm = meet_semilat.inf_commute
 lemmas join_comm = join_semilat.sup_commute
-lemmas meet_leI1[rule del] = meet_semilat.less_eq_infI1
-lemmas meet_leI2[rule del] = meet_semilat.less_eq_infI2
-lemmas le_joinI1[rule del] = join_semilat.less_eq_supI1
-lemmas le_joinI2[rule del] = join_semilat.less_eq_supI2
+lemmas meet_leI1[rule del] = meet_semilat.le_infI1
+lemmas meet_leI2[rule del] = meet_semilat.le_infI2
+lemmas le_joinI1[rule del] = join_semilat.le_supI1
+lemmas le_joinI2[rule del] = join_semilat.le_supI2
 lemmas meet_assoc = meet_semilat.inf_assoc
 lemmas join_assoc = join_semilat.sup_assoc
 lemmas meet_left_comm = meet_semilat.inf_left_commute
@@ -176,21 +181,8 @@
 lemmas meet_aci = meet_assoc meet_comm meet_left_comm meet_left_idempotent
 lemmas join_aci = join_assoc join_comm join_left_comm join_left_idempotent
 
-lemma le_def_meet: "(x <= y) = (meet x y = x)"
-apply rule
-apply(simp add: order_antisym)
-apply(subgoal_tac "meet x y <= y")
-apply(simp)
-apply(simp (no_asm))
-done
-
-lemma le_def_join: "(x <= y) = (join x y = y)"
-apply rule
-apply(simp add: order_antisym)
-apply(subgoal_tac "x <= join x y")
-apply(simp)
-apply(simp (no_asm))
-done
+lemmas le_def_meet = meet_semilat.le_iff_inf
+lemmas le_def_join = join_semilat.le_iff_sup
 
 lemmas join_absorp2 = join_semilat.sup_absorb2
 lemmas join_absorp1 = join_semilat.sup_absorb1
@@ -198,41 +190,14 @@
 lemmas meet_absorp1 = meet_semilat.inf_absorb1
 lemmas meet_absorp2 = meet_semilat.inf_absorb2
 
-lemma meet_join_absorp: "meet x (join x y) = x"
-by(simp add:meet_absorp1)
-
-lemma join_meet_absorp: "join x (meet x y) = x"
-by(simp add:join_absorp1)
-
-lemma meet_mono: "y \<le> z \<Longrightarrow> meet x y \<le> meet x z"
-by(simp add:meet_leI2)
-
-lemma join_mono: "y \<le> z \<Longrightarrow> join x y \<le> join x z"
-by(simp add:le_joinI2)
+interpretation meet_join_lat:
+  lattice ["op \<le> \<Colon> 'a\<Colon>{meet_semilorder,join_semilorder} \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
+by unfold_locales
 
-lemma distrib_join_le: "join x (meet y z) \<le> meet (join x y) (join x z)" (is "_ <= ?r")
-proof -
-  have a: "x <= ?r" by (simp_all add:le_meetI)
-  have b: "meet y z <= ?r" by (simp add:le_joinI2)
-  from a b show ?thesis by (simp add: join_leI)
-qed
-  
-lemma distrib_meet_le: "join (meet x y) (meet x z) \<le> meet x (join y z)" (is "?l <= _")
-proof -
-  have a: "?l <= x" by (simp_all add: join_leI)
-  have b: "?l <= join y z" by (simp add:meet_leI2)
-  from a b show ?thesis by (simp add: le_meetI)
-qed
+lemmas meet_join_absorp = meet_join_lat.inf_sup_absorb
+lemmas join_meet_absorp = meet_join_lat.sup_inf_absorb
 
-lemma meet_join_eq_imp_le: "a = c \<or> a = d \<or> b = c \<or> b = d \<Longrightarrow> meet a b \<le> join c d"
-by (auto simp:meet_leI2 meet_leI1)
-
-lemma modular_le: "x \<le> z \<Longrightarrow> join x (meet y z) \<le> meet (join x y) z" (is "_ \<Longrightarrow> ?t <= _")
-proof -
-  assume a: "x <= z"
-  have b: "?t <= join x y" by (simp_all add: join_leI meet_join_eq_imp_le )
-  have c: "?t <= z" by (simp_all add: a join_leI)
-  from b c show ?thesis by (simp add: le_meetI)
-qed
+lemmas distrib_join_le = meet_join_lat.distrib_sup_le
+lemmas distrib_meet_le = meet_join_lat.distrib_inf_le
 
 end
diff -r 131dd2a27137 -r 283461c15fa7 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Dec 10 07:12:26 2006 +0100
+++ b/src/HOL/Lattices.thy	Sun Dec 10 13:14:43 2006 +0100
@@ -35,30 +35,35 @@
 
 lemmas antisym_intro[intro!] = antisym
 
-lemma less_eq_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI1[intro]: "a \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> a")
  apply(blast intro:trans)
 apply simp
 done
 
-lemma less_eq_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
+lemma le_infI2[intro]: "b \<sqsubseteq> x \<Longrightarrow> a \<sqinter> b \<sqsubseteq> x"
 apply(subgoal_tac "a \<sqinter> b \<sqsubseteq> b")
  apply(blast intro:trans)
 apply simp
 done
 
-lemma less_eq_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
+lemma le_infI[intro!]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<sqinter> b"
 by(blast intro: inf_greatest)
 
-lemma less_eq_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_infE[elim!]: "x \<sqsubseteq> a \<sqinter> b \<Longrightarrow> (x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> b \<Longrightarrow> P) \<Longrightarrow> P"
 by(blast intro: trans)
 
-lemma less_eq_inf_conv [simp]:
+lemma le_inf_iff [simp]:
  "x \<sqsubseteq> y \<sqinter> z = (x \<sqsubseteq> y \<and> x \<sqsubseteq> z)"
 by blast
 
-lemmas below_inf_conv = less_eq_inf_conv
-  -- {* a duplicate for backward compatibility *}
+lemma le_iff_inf: "(x \<sqsubseteq> y) = (x \<sqinter> y = x)"
+apply rule
+ apply(simp add: antisym)
+apply(subgoal_tac "x \<sqinter> y \<sqsubseteq> y")
+ apply(simp)
+apply(simp (no_asm))
+done
 
 end
 
@@ -68,28 +73,36 @@
 
 lemmas antisym_intro[intro!] = antisym
 
-lemma less_eq_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI1[intro]: "x \<sqsubseteq> a \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
 apply(subgoal_tac "a \<sqsubseteq> a \<squnion> b")
  apply(blast intro:trans)
 apply simp
 done
 
-lemma less_eq_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
+lemma le_supI2[intro]: "x \<sqsubseteq> b \<Longrightarrow> x \<sqsubseteq> a \<squnion> b"
 apply(subgoal_tac "b \<sqsubseteq> a \<squnion> b")
  apply(blast intro:trans)
 apply simp
 done
 
-lemma less_eq_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
+lemma le_supI[intro!]: "a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> a \<squnion> b \<sqsubseteq> x"
 by(blast intro: sup_least)
 
-lemma less_eq_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
+lemma le_supE[elim!]: "a \<squnion> b \<sqsubseteq> x \<Longrightarrow> (a \<sqsubseteq> x \<Longrightarrow> b \<sqsubseteq> x \<Longrightarrow> P) \<Longrightarrow> P"
 by(blast intro: trans)
 
-lemma above_sup_conv[simp]:
+lemma ge_sup_conv[simp]:
  "x \<squnion> y \<sqsubseteq> z = (x \<sqsubseteq> z \<and> y \<sqsubseteq> z)"
 by blast
 
+lemma le_iff_sup: "(x \<sqsubseteq> y) = (x \<squnion> y = y)"
+apply rule
+ apply(simp add: antisym)
+apply(subgoal_tac "x \<sqsubseteq> x \<squnion> y")
+apply(simp)
+ apply(simp (no_asm))
+done
+
 end
 
 
@@ -162,9 +175,18 @@
 lemma sup_inf_absorb: "x \<squnion> (x \<sqinter> y) = x"
 by(blast intro: antisym sup_ge1 sup_least inf_le1)
 
-lemmas (in lattice) ACI = inf_ACI sup_ACI
+lemmas ACI = inf_ACI sup_ACI
+
+text{* Towards distributivity *}
 
-text{* Towards distributivity: if you have one of them, you have them all. *}
+lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
+by blast
+
+lemma distrib_inf_le: "(x \<sqinter> y) \<squnion> (x \<sqinter> z) \<sqsubseteq> x \<sqinter> (y \<squnion> z)"
+by blast
+
+
+text{* If you have one of them, you have them all. *}
 
 lemma distrib_imp1:
 assumes D: "!!x y z. x \<sqinter> (y \<squnion> z) = (x \<sqinter> y) \<squnion> (x \<sqinter> z)"
@@ -190,6 +212,10 @@
   finally show ?thesis .
 qed
 
+(* seems unused *)
+lemma modular_le: "x \<sqsubseteq> z \<Longrightarrow> x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> z"
+by blast
+
 end
 
 
@@ -237,10 +263,10 @@
 
 declare
  min_max.antisym_intro[rule del]
- min_max.less_eq_infI[rule del] min_max.less_eq_supI[rule del]
- min_max.less_eq_supE[rule del] min_max.less_eq_infE[rule del]
- min_max.less_eq_supI1[rule del] min_max.less_eq_supI2[rule del]
- min_max.less_eq_infI1[rule del] min_max.less_eq_infI2[rule del]
+ min_max.le_infI[rule del] min_max.le_supI[rule del]
+ min_max.le_supE[rule del] min_max.le_infE[rule del]
+ min_max.le_supI1[rule del] min_max.le_supI2[rule del]
+ min_max.le_infI1[rule del] min_max.le_infI2[rule del]
 
 lemmas le_maxI1 = min_max.sup_ge1
 lemmas le_maxI2 = min_max.sup_ge2