# HG changeset patch
# User haftmann
# Date 1163606739 -3600
# Node ID c4f79922bc81faa30b50abd83f027cf2428ac07b
# Parent  a0561695167a9258d3cf25784ed3d352b344559d
added interpretation

diff -r a0561695167a -r c4f79922bc81 src/HOL/LOrder.thy
--- a/src/HOL/LOrder.thy	Wed Nov 15 17:05:38 2006 +0100
+++ b/src/HOL/LOrder.thy	Wed Nov 15 17:05:39 2006 +0100
@@ -90,6 +90,22 @@
 lemma join_unique: "(is_join j) = (j = join)"
 by (insert is_join_join, auto simp add: is_join_unique)
 
+interpretation lattice:
+  lattice ["op \<le> \<Colon> 'a\<Colon>lorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" meet join]
+proof unfold_locales
+  fix x y z :: "'a\<Colon>lorder"
+  from is_meet_meet have "is_meet meet" by blast
+  note meet = this is_meet_def
+  from meet show "meet x y \<le> x" by blast
+  from meet show "meet x y \<le> y" by blast
+  from meet show "x \<le> y \<Longrightarrow> x \<le> z \<Longrightarrow> x \<le> meet y z" by blast
+  from is_join_join have "is_join join" by blast
+  note join = this is_join_def
+  from join show "x \<le> join x y" by blast
+  from join show "y \<le> join x y" by blast
+  from join show "y \<le> x \<Longrightarrow> z \<le> x \<Longrightarrow> join y z \<le> x" by blast
+qed
+
 lemma meet_left_le: "meet a b \<le> (a::'a::meet_semilorder)"
 by (insert is_meet_meet, auto simp add: is_meet_def)