# HG changeset patch
# User haftmann
# Date 1174077130 -3600
# Node ID c3654ba76a09aef385e7bece4c24befb6ed4de1e
# Parent  530db8c36f532cecf828c5501e6c2cc1e77e949b
integrated with LOrder.thy

diff -r 530db8c36f53 -r c3654ba76a09 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Mar 16 21:32:09 2007 +0100
+++ b/src/HOL/Lattices.thy	Fri Mar 16 21:32:10 2007 +0100
@@ -3,7 +3,7 @@
     Author:     Tobias Nipkow
 *)
 
-header {* Lattices via Locales *}
+header {* Abstract lattices *}
 
 theory Lattices
 imports Orderings
@@ -11,10 +11,11 @@
 
 subsection{* Lattices *}
 
-text{* This theory of lattice locales only defines binary sup and inf
-operations. The extension to finite sets is done in theory @{text
-Finite_Set}. In the longer term it may be better to define arbitrary
-sups and infs via @{text THE}. *}
+text{*
+  This theory of lattices only defines binary sup and inf
+  operations. The extension to (finite) sets is done in theories @{text FixedPoint}
+  and @{text Finite_Set}.
+*}
 
 class lower_semilattice = order +
   fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
@@ -178,6 +179,8 @@
 
 lemmas ACI = inf_ACI sup_ACI
 
+lemmas inf_sup_ord = inf_le1 inf_le2 sup_ge1 sup_ge2
+
 text{* Towards distributivity *}
 
 lemma distrib_sup_le: "x \<squnion> (y \<sqinter> z) \<sqsubseteq> (x \<squnion> y) \<sqinter> (x \<squnion> z)"
@@ -222,7 +225,7 @@
 
 subsection{* Distributive lattices *}
 
-locale distrib_lattice = lattice +
+class distrib_lattice = lattice +
   assumes sup_inf_distrib1: "x \<squnion> (y \<sqinter> z) = (x \<squnion> y) \<sqinter> (x \<squnion> z)"
 
 context distrib_lattice
@@ -246,10 +249,37 @@
 end
 
 
+subsection {* Uniqueness of inf and sup *}
+
+lemma inf_unique:
+  fixes f (infixl "\<triangle>" 70)
+  assumes le1: "\<And>x y. x \<triangle> y \<le> x" and le2: "\<And>x y. x \<triangle> y \<le> y"
+  and greatest: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z"
+  shows "inf x y = f x y"
+proof (rule antisym)
+  show "x \<triangle> y \<le> inf x y" by (rule le_infI) (rule le1 le2)
+next
+  have leI: "\<And>x y z. x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> y \<triangle> z" by (blast intro: greatest)
+  show "inf x y \<le> x \<triangle> y" by (rule leI) simp_all
+qed
+
+lemma sup_unique:
+  fixes f (infixl "\<nabla>" 70)
+  assumes ge1 [simp]: "\<And>x y. x \<le> x \<nabla> y" and ge2: "\<And>x y. y \<le> x \<nabla> y"
+  and least: "\<And>x y z. y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> y \<nabla> z \<le> x"
+  shows "sup x y = f x y"
+proof (rule antisym)
+  show "sup x y \<le> x \<nabla> y" by (rule le_supI) (rule ge1 ge2)
+next
+  have leI: "\<And>x y z. x \<le> z \<Longrightarrow> y \<le> z \<Longrightarrow> x \<nabla> y \<le> z" by (blast intro: least)
+  show "x \<nabla> y \<le> sup x y" by (rule leI) simp_all
+qed
+  
+
 subsection {* min/max on linear orders as special case of inf/sup *}
 
 interpretation min_max:
-  distrib_lattice ["op \<le>" "op <" "min \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> 'a" "max"]
+  distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
 apply unfold_locales
 apply (simp add: min_def linorder_not_le order_less_imp_le)
 apply (simp add: min_def linorder_not_le order_less_imp_le)
@@ -258,15 +288,11 @@
 apply (simp add: max_def linorder_not_le order_less_imp_le)
 unfolding min_def max_def by auto
 
-text {*
-  Now we have inherited antisymmetry as an intro-rule on all
-  linear orders. This is a problem because it applies to bool, which is
-  undesirable.
-*}
+lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+  by (rule ext)+ auto
 
-lemmas [rule del] = min_max.antisym_intro  min_max.le_infI min_max.le_supI
-  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
-  min_max.le_infI1 min_max.le_infI2
+lemma sup_max: "sup = (max \<Colon> 'a\<Colon>{upper_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
+  by (rule ext)+ auto
 
 lemmas le_maxI1 = min_max.sup_ge1
 lemmas le_maxI2 = min_max.sup_ge2
@@ -277,6 +303,31 @@
 lemmas min_ac = min_max.inf_assoc min_max.inf_commute
   mk_left_commute [of min, OF min_max.inf_assoc min_max.inf_commute]
 
+text {*
+  Now we have inherited antisymmetry as an intro-rule on all
+  linear orders. This is a problem because it applies to bool, which is
+  undesirable.
+*}
+
+lemmas [rule del] = min_max.antisym_intro min_max.le_infI min_max.le_supI
+  min_max.le_supE min_max.le_infE min_max.le_supI1 min_max.le_supI2
+  min_max.le_infI1 min_max.le_infI2
+
+
+subsection {* Bool as lattice *}
+
+instance bool :: distrib_lattice
+  inf_bool_eq: "inf P Q \<equiv> P \<and> Q"
+  sup_bool_eq: "sup P Q \<equiv> P \<or> Q"
+  by intro_classes (auto simp add: inf_bool_eq sup_bool_eq le_bool_def)
+
+
+text {* duplicates *}
+
+lemmas inf_aci = inf_ACI
+lemmas sup_aci = sup_ACI
+
+
 text {* ML legacy bindings *}
 
 ML {*