--- 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.
--- 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
--- 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
--- 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
--- 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"
--- 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"
--- 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)"
--- 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"}),
--- 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
--- 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)
--- 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