# HG changeset patch
# User haftmann
# Date 1254837094 -7200
# Node ID 7f5ce7af45fdf929da09fe672b4239ccc312d445
# Parent  f8d995b5dd60da54984944119e3f5217a82c5747
added syntactic Inf and Sup

diff -r f8d995b5dd60 -r 7f5ce7af45fd src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Mon Oct 05 17:28:59 2009 +0100
+++ b/src/HOL/Complete_Lattice.thy	Tue Oct 06 15:51:34 2009 +0200
@@ -15,21 +15,25 @@
   bot ("\<bottom>")
 
 
+subsection {* Syntactic infimum and supremum operations *}
+
+class Inf =
+  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
+
+class Sup =
+  fixes Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+
 subsection {* Abstract complete lattices *}
 
-class complete_lattice = lattice + bot + top +
-  fixes Inf :: "'a set \<Rightarrow> 'a" ("\<Sqinter>_" [900] 900)
-    and Sup :: "'a set \<Rightarrow> 'a" ("\<Squnion>_" [900] 900)
+class complete_lattice = lattice + bot + top + Inf + Sup +
   assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
      and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
   assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
      and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
 begin
 
-term complete_lattice
-
 lemma dual_complete_lattice:
-  "complete_lattice (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom> Sup Inf"
+  "complete_lattice Sup Inf (op \<ge>) (op >) (op \<squnion>) (op \<sqinter>) \<top> \<bottom>"
   by (auto intro!: complete_lattice.intro dual_lattice
     bot.intro top.intro dual_preorder, unfold_locales)
       (fact bot_least top_greatest
diff -r f8d995b5dd60 -r 7f5ce7af45fd src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Oct 05 17:28:59 2009 +0100
+++ b/src/HOL/GCD.thy	Tue Oct 06 15:51:34 2009 +0200
@@ -1575,7 +1575,7 @@
 qed
 
 interpretation gcd_lcm_complete_lattice_nat:
-  complete_lattice "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0 GCD LCM
+  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
 proof
   case goal1 show ?case by simp
 next