# HG changeset patch
# User krauss
# Date 1315520538 -7200
# Node ID 5e51075cbd97e103a655bb3d84e129342014a693
# Parent  f74a4175a3a8bef0552bc03281711d0f76dbfe61
added syntactic classes for "inf" and "sup"

diff -r f74a4175a3a8 -r 5e51075cbd97 NEWS
--- a/NEWS	Thu Sep 08 08:41:28 2011 -0700
+++ b/NEWS	Fri Sep 09 00:22:18 2011 +0200
@@ -131,6 +131,10 @@
 
 INCOMPATIBILITY.
 
+* Added syntactic classes "inf" and "sup" for the respective
+constants.  INCOMPATIBILITY: Changes in the argument order of the
+(mostly internal) locale predicates for some derived classes.
+
 * Theorem collections ball_simps and bex_simps do not contain theorems
 referring to UNION any longer; these have been moved to collection
 UN_ball_bex_simps.  INCOMPATIBILITY.
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Big_Operators.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -1517,7 +1517,7 @@
   proof qed (auto simp add: max_def)
 
 lemma max_lattice:
-  "class.semilattice_inf (op \<ge>) (op >) max"
+  "class.semilattice_inf max (op \<ge>) (op >)"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max:
@@ -1611,7 +1611,7 @@
   assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
 proof -
-  interpret semilattice_inf "op \<ge>" "op >" max
+  interpret semilattice_inf max "op \<ge>" "op >"
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def fold1_belowI)
 qed
@@ -1625,7 +1625,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
 proof -
-  interpret semilattice_inf "op \<ge>" "op >" max
+  interpret semilattice_inf max "op \<ge>" "op >"
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
 qed
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Complete_Lattice.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -33,7 +33,7 @@
 begin
 
 lemma dual_complete_lattice:
-  "class.complete_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
     (unfold_locales, (fact bot_least top_greatest
         Sup_upper Sup_least Inf_lower Inf_greatest)+)
@@ -85,7 +85,7 @@
 lemma INF_foundation_dual [no_atp]:
   "complete_lattice.SUPR Inf = INFI"
 proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
     by (fact dual_complete_lattice)
   fix f :: "'b \<Rightarrow> 'a" and A
   show "complete_lattice.SUPR Inf A f = (\<Sqinter>a\<in>A. f a)"
@@ -95,7 +95,7 @@
 lemma SUP_foundation_dual [no_atp]:
   "complete_lattice.INFI Sup = SUPR"
 proof (rule ext)+
-  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
     by (fact dual_complete_lattice)
   fix f :: "'b \<Rightarrow> 'a" and A
   show "complete_lattice.INFI Sup A f = (\<Squnion>a\<in>A. f a)"
@@ -313,7 +313,7 @@
   "\<Squnion>A = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?P)
   "\<bottom> = \<Squnion>A \<longleftrightarrow> (\<forall>x\<in>A. x = \<bottom>)" (is ?Q)
 proof -
-  interpret dual: complete_lattice Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+  interpret dual: complete_lattice Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
     by (fact dual_complete_lattice)
   from dual.Inf_top_conv show ?P and ?Q by simp_all
 qed
@@ -407,7 +407,7 @@
   by (simp add: SUP_def inf_Sup image_image)
 
 lemma dual_complete_distrib_lattice:
-  "class.complete_distrib_lattice Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  "class.complete_distrib_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   apply (rule class.complete_distrib_lattice.intro)
   apply (fact dual_complete_lattice)
   apply (rule class.complete_distrib_lattice_axioms.intro)
@@ -458,7 +458,7 @@
 begin
 
 lemma dual_complete_boolean_algebra:
-  "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
+  "class.complete_boolean_algebra Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
   by (rule class.complete_boolean_algebra.intro, rule dual_complete_distrib_lattice, rule dual_boolean_algebra)
 
 lemma uminus_Inf:
@@ -489,7 +489,7 @@
 begin
 
 lemma dual_complete_linorder:
-  "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  "class.complete_linorder Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
   by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
 
 lemma Inf_less_iff (*[simp]*):
@@ -537,7 +537,7 @@
 lemma Inf_eq_bot_iff (*[simp]*):
   "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
 proof -
-  interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+  interpret dual: complete_linorder Sup Inf sup "op \<ge>" "op >" inf \<top> \<bottom>
     by (fact dual_complete_linorder)
   from dual.Sup_eq_top_iff show ?thesis .
 qed
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/GCD.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -1463,17 +1463,17 @@
 subsubsection {* The complete divisibility lattice *}
 
 
-interpretation gcd_semilattice_nat: semilattice_inf "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd
+interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
 proof
   case goal3 thus ?case by(metis gcd_unique_nat)
 qed auto
 
-interpretation lcm_semilattice_nat: semilattice_sup "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm
+interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)"
 proof
   case goal3 thus ?case by(metis lcm_unique_nat)
 qed auto
 
-interpretation gcd_lcm_lattice_nat: lattice "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" gcd lcm ..
+interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(%m n::nat. m dvd n & ~ n dvd m)" lcm ..
 
 text{* Lifting gcd and lcm to finite (Gcd/Lcm) and infinite sets (GCD/LCM).
 GCD is defined via LCM to facilitate the proof that we have a complete lattice.
@@ -1579,7 +1579,7 @@
 qed
 
 interpretation gcd_lcm_complete_lattice_nat:
-  complete_lattice GCD LCM "op dvd" "%m n::nat. m dvd n & ~ n dvd m" gcd lcm 1 0
+  complete_lattice GCD LCM gcd "op dvd" "%m n::nat. m dvd n & ~ n dvd m" lcm 1 0
 proof
   case goal1 show ?case by simp
 next
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -145,9 +145,9 @@
   GEQ > HOL.eq
   GSPEC > Set.Collect
   SETSPEC > HOLLightCompat.SETSPEC
-  UNION > Lattices.semilattice_sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+  UNION > Lattices.sup_class.sup :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   UNIONS > Complete_Lattice.Sup_class.Sup :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
-  INTER > Lattices.semilattice_inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
+  INTER > Lattices.inf_class.inf :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   INTERS > Complete_Lattice.Inf_class.Inf :: "(('a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   DIFF > Groups.minus_class.minus :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> bool"
   SUBSET > Orderings.ord_class.less_eq :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Import/HOLLight/hollight.imp
--- a/src/HOL/Import/HOLLight/hollight.imp	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Import/HOLLight/hollight.imp	Fri Sep 09 00:22:18 2011 +0200
@@ -267,7 +267,7 @@
   "WF" > "Wellfounded.wfP"
   "UNIV" > "Orderings.top_class.top" :: "'a => bool"
   "UNIONS" > "Complete_Lattice.Sup_class.Sup" :: "(('a => bool) => bool) => 'a => bool"
-  "UNION" > "Lattices.semilattice_sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
+  "UNION" > "Lattices.sup_class.sup" :: "('a => bool) => ('a => bool) => 'a => bool"
   "UNCURRY" > "HOLLight.hollight.UNCURRY"
   "TL" > "List.tl"
   "T" > "HOL.True"
@@ -317,7 +317,7 @@
   "ITLIST" > "List.foldr"
   "ISO" > "HOLLight.hollight.ISO"
   "INTERS" > "Complete_Lattice.Inf_class.Inf" :: "(('a => bool) => bool) => 'a => bool"
-  "INTER" > "Lattices.semilattice_inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
+  "INTER" > "Lattices.inf_class.inf" :: "('a => bool) => ('a => bool) => 'a => bool"
   "INSERT" > "Set.insert"
   "INR" > "Sum_Type.Inr"
   "INL" > "Sum_Type.Inl"
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Lattices.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -51,15 +51,18 @@
   bot ("\<bottom>") and
   top ("\<top>")
 
+class inf =
+  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
 
-class semilattice_inf = order +
-  fixes inf :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<sqinter>" 70)
+class sup = 
+  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+
+class semilattice_inf =  order + inf +
   assumes inf_le1 [simp]: "x \<sqinter> y \<sqsubseteq> x"
   and inf_le2 [simp]: "x \<sqinter> y \<sqsubseteq> y"
   and inf_greatest: "x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<sqinter> z"
 
-class semilattice_sup = order +
-  fixes sup :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<squnion>" 65)
+class semilattice_sup = order + sup +
   assumes sup_ge1 [simp]: "x \<sqsubseteq> x \<squnion> y"
   and sup_ge2 [simp]: "y \<sqsubseteq> x \<squnion> y"
   and sup_least: "y \<sqsubseteq> x \<Longrightarrow> z \<sqsubseteq> x \<Longrightarrow> y \<squnion> z \<sqsubseteq> x"
@@ -68,7 +71,7 @@
 text {* Dual lattice *}
 
 lemma dual_semilattice:
-  "class.semilattice_inf greater_eq greater sup"
+  "class.semilattice_inf sup greater_eq greater"
 by (rule class.semilattice_inf.intro, rule dual_order)
   (unfold_locales, simp_all add: sup_least)
 
@@ -236,7 +239,7 @@
 begin
 
 lemma dual_lattice:
-  "class.lattice (op \<ge>) (op >) sup inf"
+  "class.lattice sup (op \<ge>) (op >) inf"
   by (rule class.lattice.intro, rule dual_semilattice, rule class.semilattice_sup.intro, rule dual_order)
     (unfold_locales, auto)
 
@@ -307,7 +310,7 @@
 lemma less_supI1:
   "x \<sqsubset> a \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
-  interpret dual: semilattice_inf "op \<ge>" "op >" sup
+  interpret dual: semilattice_inf sup "op \<ge>" "op >"
     by (fact dual_semilattice)
   assume "x \<sqsubset> a"
   then show "x \<sqsubset> a \<squnion> b"
@@ -317,7 +320,7 @@
 lemma less_supI2:
   "x \<sqsubset> b \<Longrightarrow> x \<sqsubset> a \<squnion> b"
 proof -
-  interpret dual: semilattice_inf "op \<ge>" "op >" sup
+  interpret dual: semilattice_inf sup "op \<ge>" "op >"
     by (fact dual_semilattice)
   assume "x \<sqsubset> b"
   then show "x \<sqsubset> a \<squnion> b"
@@ -348,7 +351,7 @@
 by(simp add: inf_sup_aci inf_sup_distrib1)
 
 lemma dual_distrib_lattice:
-  "class.distrib_lattice (op \<ge>) (op >) sup inf"
+  "class.distrib_lattice sup (op \<ge>) (op >) inf"
   by (rule class.distrib_lattice.intro, rule dual_lattice)
     (unfold_locales, fact inf_sup_distrib1)
 
@@ -420,7 +423,7 @@
 begin
 
 lemma dual_bounded_lattice:
-  "class.bounded_lattice greater_eq greater sup inf \<top> \<bottom>"
+  "class.bounded_lattice sup greater_eq greater inf \<top> \<bottom>"
   by unfold_locales (auto simp add: less_le_not_le)
 
 end
@@ -432,7 +435,7 @@
 begin
 
 lemma dual_boolean_algebra:
-  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus greater_eq greater sup inf \<top> \<bottom>"
+  "class.boolean_algebra (\<lambda>x y. x \<squnion> - y) uminus sup greater_eq greater inf \<top> \<bottom>"
   by (rule class.boolean_algebra.intro, rule dual_bounded_lattice, rule dual_distrib_lattice)
     (unfold_locales, auto simp add: inf_compl_bot sup_compl_top diff_eq)
 
@@ -506,7 +509,7 @@
 lemma compl_sup [simp]:
   "- (x \<squnion> y) = - x \<sqinter> - y"
 proof -
-  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus greater_eq greater sup inf \<top> \<bottom>
+  interpret boolean_algebra "\<lambda>x y. x \<squnion> - y" uminus sup greater_eq greater inf \<top> \<bottom>
     by (rule dual_boolean_algebra)
   then show ?thesis by simp
 qed
@@ -591,7 +594,7 @@
 subsection {* @{const min}/@{const max} on linear orders as
   special case of @{const inf}/@{const sup} *}
 
-sublocale linorder < min_max!: distrib_lattice less_eq less min max
+sublocale linorder < min_max!: distrib_lattice min less_eq less max
 proof
   fix x y z
   show "max x (min y z) = min (max x y) (max x z)"
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Sep 09 00:22:18 2011 +0200
@@ -286,8 +286,8 @@
    (@{const_name "Groups.minus_class.minus"}, @{typ "prop => prop => prop"}),
    (@{const_name "Groups.times_class.times"}, @{typ "prop => prop => prop"}),
    (@{const_name "Fields.inverse_class.divide"}, @{typ "prop => prop => prop"}),
-   (@{const_name "Lattices.semilattice_inf_class.inf"}, @{typ "prop => prop => prop"}),
-   (@{const_name "Lattices.semilattice_sup_class.sup"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Lattices.inf_class.inf"}, @{typ "prop => prop => prop"}),
+   (@{const_name "Lattices.sup_class.sup"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.bot_class.bot"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.ord_class.min"}, @{typ "prop => prop => prop"}),
    (@{const_name "Orderings.ord_class.max"}, @{typ "prop => prop => prop"}),
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Quickcheck.thy
--- a/src/HOL/Quickcheck.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Quickcheck.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -183,7 +183,7 @@
 where
   "union R1 R2 = (\<lambda>s. let
      (P1, s') = R1 s; (P2, s'') = R2 s'
-   in (semilattice_sup_class.sup P1 P2, s''))"
+   in (sup_class.sup P1 P2, s''))"
 
 definition if_randompred :: "bool \<Rightarrow> unit randompred"
 where
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/ex/Quickcheck_Lattice_Examples.thy
--- a/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/ex/Quickcheck_Lattice_Examples.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -125,7 +125,7 @@
   by (rule inf_absorb1) simp
 
 lemma inf_eq_top_iff [simp]:
-  "x \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
+  "(x :: 'a :: bounded_lattice_top) \<sqinter> y = \<top> \<longleftrightarrow> x = \<top> \<and> y = \<top>"
   quickcheck[expect = no_counterexample]
   by (simp add: eq_iff)
 
diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/ex/RPred.thy
--- a/src/HOL/ex/RPred.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/ex/RPred.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -25,7 +25,7 @@
 (* (infixl "\<squnion>" 80) *)
 where
   "supp RP1 RP2 = (\<lambda>s. let (P1, s') = RP1 s; (P2, s'') = RP2 s'
-  in (semilattice_sup_class.sup P1 P2, s''))"
+  in (sup_class.sup P1 P2, s''))"
 
 definition if_rpred :: "bool \<Rightarrow> unit rpred"
 where