--- a/src/HOL/Complete_Lattices.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Complete_Lattices.thy Thu Jul 25 08:57:16 2013 +0200
@@ -22,17 +22,31 @@
subsection {* Abstract complete lattices *}
-class complete_lattice = bounded_lattice + Inf + Sup +
+text {* A complete lattice always has a bottom and a top,
+so we include them into the following type class,
+along with assumptions that define bottom and top
+in terms of infimum and supremum. *}
+
+class complete_lattice = lattice + Inf + Sup + bot + top +
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"
+ assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
+ assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
begin
+subclass bounded_lattice
+proof
+ fix a
+ show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
+ show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
+qed
+
lemma dual_complete_lattice:
"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
+ by (auto intro!: class.complete_lattice.intro dual_lattice)
+ (unfold_locales, (fact Inf_empty Sup_empty
Sup_upper Sup_least Inf_lower Inf_greatest)+)
definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
@@ -141,17 +155,21 @@
lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
by (auto simp add: SUP_def Sup_le_iff)
-lemma Inf_empty [simp]:
- "\<Sqinter>{} = \<top>"
- by (auto intro: antisym Inf_greatest)
+lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
+ by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
+
+lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
+ by (simp add: INF_def)
+
+lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
+ by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
+
+lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
+ by (simp add: SUP_def)
lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
by (simp add: INF_def)
-lemma Sup_empty [simp]:
- "\<Squnion>{} = \<bottom>"
- by (auto intro: antisym Sup_least)
-
lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
by (simp add: SUP_def)
@@ -163,18 +181,6 @@
"\<Squnion>UNIV = \<top>"
by (auto intro!: antisym Sup_upper)
-lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
- by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
-
-lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
- by (simp add: INF_def)
-
-lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
- by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
-
-lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
- by (simp add: SUP_def)
-
lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
by (simp add: INF_def image_image)
--- a/src/HOL/GCD.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/GCD.thy Thu Jul 25 08:57:16 2013 +0200
@@ -1560,17 +1560,17 @@
proof -
show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
proof
- case goal1 show ?case by simp
+ case goal1 thus ?case by (simp add: Gcd_nat_def)
next
- case goal2 show ?case by simp
+ case goal2 thus ?case by (simp add: Gcd_nat_def)
next
- case goal5 thus ?case by (rule dvd_Lcm_nat)
+ case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
next
- case goal6 thus ?case by simp
+ case goal6 show ?case by (simp add: Lcm_nat_empty)
next
- case goal3 thus ?case by (simp add: Gcd_nat_def)
+ case goal3 thus ?case by simp
next
- case goal4 thus ?case by (simp add: Gcd_nat_def)
+ case goal4 thus ?case by simp
qed
then interpret gcd_lcm_complete_lattice_nat:
complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
--- a/src/HOL/IMP/Abs_Int0.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy Thu Jul 25 08:57:16 2013 +0200
@@ -6,11 +6,11 @@
subsection "Orderings"
-text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are
+text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
If you view this theory with jedit, just click on the names to get there. *}
-class semilattice_sup_top = semilattice_sup + top
+class semilattice_sup_top = semilattice_sup + order_top
instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..
@@ -78,7 +78,7 @@
lemma [simp]: "(Some x < Some y) = (x < y)"
by(auto simp: less_le)
-instantiation option :: (order)bot
+instantiation option :: (order)order_bot
begin
definition bot_option :: "'a option" where
--- a/src/HOL/IMP/Abs_Int1.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy Thu Jul 25 08:57:16 2013 +0200
@@ -100,7 +100,7 @@
subsubsection "Termination"
locale Measure1 =
-fixes m :: "'av::{order,top} \<Rightarrow> nat"
+fixes m :: "'av::{order,order_top} \<Rightarrow> nat"
fixes h :: "nat"
assumes h: "m x \<le> h"
begin
@@ -134,14 +134,14 @@
end
-fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
+fun top_on_st :: "'a::order_top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
"top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
-fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
+fun top_on_opt :: "'a::order_top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
"top_on_opt (Some S) X = top_on_st S X" |
"top_on_opt None X = True"
-definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
+definition top_on_acom :: "'a::order_top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
"top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
lemma top_on_top: "top_on_opt (\<top>::_ st option) X"
--- a/src/HOL/IMP/Abs_Int3.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_Int3.thy Thu Jul 25 08:57:16 2013 +0200
@@ -25,7 +25,7 @@
end
-lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,top})"
+lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})"
by (metis eq_iff top_greatest widen2)
instantiation ivl :: wn
@@ -53,7 +53,7 @@
end
-instantiation st :: ("{top,wn}")wn
+instantiation st :: ("{order_top,wn}")wn
begin
lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
@@ -335,7 +335,7 @@
widening. *}
locale Measure_wn = Measure1 where m=m
- for m :: "'av::{top,wn} \<Rightarrow> nat" +
+ for m :: "'av::{order_top,wn} \<Rightarrow> nat" +
fixes n :: "'av \<Rightarrow> nat"
assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
--- a/src/HOL/IMP/Abs_State.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy Thu Jul 25 08:57:16 2013 +0200
@@ -6,7 +6,7 @@
type_synonym 'a st_rep = "(vname * 'a) list"
-fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
+fun fun_rep :: "('a::order_top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
"fun_rep [] = (\<lambda>x. \<top>)" |
"fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
@@ -14,23 +14,23 @@
"fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
by(induction ps rule: fun_rep.induct) auto
-definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
+definition eq_st :: "('a::order_top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
"eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
hide_type st --"hide previous def to avoid long names"
-quotient_type 'a st = "('a::top) st_rep" / eq_st
+quotient_type 'a st = "('a::order_top) st_rep" / eq_st
morphisms rep_st St
by (metis eq_st_def equivpI reflpI sympI transpI)
-lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
+lift_definition update :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
is "\<lambda>ps x a. (x,a)#ps"
by(auto simp: eq_st_def)
-lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
+lift_definition "fun" :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
by(simp add: eq_st_def)
-definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
+definition show_st :: "vname set \<Rightarrow> ('a::order_top) st \<Rightarrow> (vname * 'a)set" where
"show_st X S = (\<lambda>x. (x, fun S x)) ` X"
definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
@@ -39,10 +39,10 @@
lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
by transfer auto
-definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
+definition \<gamma>_st :: "(('a::order_top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
"\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
-instantiation st :: ("{order,top}") order
+instantiation st :: ("{order,order_top}") order
begin
definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
@@ -83,7 +83,7 @@
lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
by transfer (rule less_eq_st_rep_iff)
-fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
+fun map2_st_rep :: "('a::order_top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
"map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
"map2_st_rep f ((x,y)#ps1) ps2 =
(let y2 = fun_rep ps2 x
--- a/src/HOL/Lattices.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Lattices.thy Thu Jul 25 08:57:16 2013 +0200
@@ -466,7 +466,7 @@
subsection {* Bounded lattices and boolean algebras *}
-class bounded_semilattice_inf_top = semilattice_inf + top
+class bounded_semilattice_inf_top = semilattice_inf + order_top
begin
sublocale inf_top!: semilattice_neutr inf top
@@ -479,7 +479,7 @@
end
-class bounded_semilattice_sup_bot = semilattice_sup + bot
+class bounded_semilattice_sup_bot = semilattice_sup + order_bot
begin
sublocale sup_bot!: semilattice_neutr sup bot
@@ -492,7 +492,7 @@
end
-class bounded_lattice_bot = lattice + bot
+class bounded_lattice_bot = lattice + order_bot
begin
subclass bounded_semilattice_sup_bot ..
@@ -523,7 +523,7 @@
end
-class bounded_lattice_top = lattice + top
+class bounded_lattice_top = lattice + order_top
begin
subclass bounded_semilattice_inf_top ..
@@ -550,7 +550,7 @@
end
-class bounded_lattice = lattice + bot + top
+class bounded_lattice = lattice + order_bot + order_top
begin
subclass bounded_lattice_bot ..
--- a/src/HOL/Library/Extended_Nat.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Thu Jul 25 08:57:16 2013 +0200
@@ -452,7 +452,7 @@
apply (erule (1) le_less_trans)
done
-instantiation enat :: "{bot, top}"
+instantiation enat :: "{order_bot, order_top}"
begin
definition bot_enat :: enat where
@@ -623,7 +623,8 @@
unfolding Sup_enat_def by (cases "finite A") auto }
{ assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
unfolding Sup_enat_def using finite_enat_bounded by auto }
-qed (simp_all add: inf_enat_def sup_enat_def)
+qed (simp_all add:
+ inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def)
end
instance enat :: complete_linorder ..
--- a/src/HOL/Library/Extended_Real.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jul 25 08:57:16 2013 +0200
@@ -1144,8 +1144,22 @@
using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
instance
- by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
- simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
+proof
+ show "Sup {} = (bot::ereal)"
+ apply (auto simp: bot_ereal_def Sup_ereal_def)
+ apply (rule some1_equality)
+ apply (metis ereal_bot ereal_less_eq(2))
+ apply (metis ereal_less_eq(2))
+ done
+next
+ show "Inf {} = (top::ereal)"
+ apply (auto simp: top_ereal_def Inf_ereal_def)
+ apply (rule some1_equality)
+ apply (metis ereal_top ereal_less_eq(1))
+ apply (metis ereal_less_eq(1))
+ done
+qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
+ simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
end
--- a/src/HOL/Library/Finite_Lattice.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Finite_Lattice.thy Thu Jul 25 08:57:16 2013 +0200
@@ -13,31 +13,39 @@
with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
along with assumptions that define these operators
in terms of the ones of classes @{class finite} and @{class lattice}.
-The resulting class is a subclass of @{class complete_lattice}.
-Classes @{class bot} and @{class top} already include assumptions that suffice
-to define the operators @{const bot} and @{const top} (as proved below),
-and so no explicit assumptions on these two operators are needed
-in the following type class.%
-\footnote{The Isabelle/HOL library does not provide
-syntactic classes for the operators @{const bot} and @{const top}.} *}
+The resulting class is a subclass of @{class complete_lattice}. *}
class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
+assumes bot_def: "bot = Inf_fin UNIV"
+assumes top_def: "top = Sup_fin UNIV"
assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
--- "No explicit assumptions on @{const bot} or @{const top}."
+
+text {* The definitional assumptions
+on the operators @{const bot} and @{const top}
+of class @{class finite_lattice_complete}
+ensure that they yield bottom and top. *}
+
+lemma finite_lattice_complete_bot_least:
+"(bot::'a::finite_lattice_complete) \<le> x"
+by (auto simp: bot_def intro: Inf_fin.coboundedI)
+
+instance finite_lattice_complete \<subseteq> order_bot
+proof qed (auto simp: finite_lattice_complete_bot_least)
+
+lemma finite_lattice_complete_top_greatest:
+"(top::'a::finite_lattice_complete) \<ge> x"
+by (auto simp: top_def Sup_fin.coboundedI)
+
+instance finite_lattice_complete \<subseteq> order_top
+proof qed (auto simp: finite_lattice_complete_top_greatest)
instance finite_lattice_complete \<subseteq> bounded_lattice ..
--- "This subclass relation eases the proof of the next two lemmas."
-lemma finite_lattice_complete_bot_def:
- "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
-by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
--- "Derived definition of @{const bot}."
-
-lemma finite_lattice_complete_top_def:
- "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
-by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
--- "Derived definition of @{const top}."
+text {* The definitional assumptions
+on the operators @{const Inf} and @{const Sup}
+of class @{class finite_lattice_complete}
+ensure that they yield infimum and supremum. *}
lemma finite_lattice_complete_Inf_empty:
"Inf {} = (top :: 'a::finite_lattice_complete)"
@@ -63,12 +71,6 @@
show ?thesis by (simp add: Sup_def)
qed
-text {* The definitional assumptions
-on the operators @{const Inf} and @{const Sup}
-of class @{class finite_lattice_complete}
-ensure that they yield infimum and supremum,
-as required for a complete lattice. *}
-
lemma finite_lattice_complete_Inf_lower:
"(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
@@ -91,28 +93,48 @@
finite_lattice_complete_Inf_lower
finite_lattice_complete_Inf_greatest
finite_lattice_complete_Sup_upper
- finite_lattice_complete_Sup_least)
-
+ finite_lattice_complete_Sup_least
+ finite_lattice_complete_Inf_empty
+ finite_lattice_complete_Sup_empty)
text {* The product of two finite lattices is already a finite lattice. *}
+lemma finite_bot_prod:
+ "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
+ Inf_fin UNIV"
+by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
+
+lemma finite_top_prod:
+ "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
+ Sup_fin UNIV"
+by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
+
lemma finite_Inf_prod:
- "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
+ "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold inf top A"
by (metis Inf_fold_inf finite_code)
lemma finite_Sup_prod:
- "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
+ "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
Finite_Set.fold sup bot A"
by (metis Sup_fold_sup finite_code)
instance prod ::
(finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
-proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
+proof
+qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
text {* Functions with a finite domain and with a finite lattice as codomain
already form a finite lattice. *}
+lemma finite_bot_fun:
+ "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
+by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
+
+lemma finite_top_fun:
+ "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
+by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
+
lemma finite_Inf_fun:
"Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
Finite_Set.fold inf top A"
@@ -124,7 +146,8 @@
by (metis Sup_fold_sup finite_code)
instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
-proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
+proof
+qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
subsection {* Finite Distributive Lattices *}
@@ -178,11 +201,9 @@
subsection {* Linear Orders *}
text {* A linear order is a distributive lattice.
-Since in Isabelle/HOL
-a subclass must have all the parameters of its superclasses,
-class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
-So class @{class linorder} is extended with
-the operators @{const inf} and @{const sup},
+A type class is defined
+that extends class @{class linorder}
+with the operators @{const inf} and @{const sup},
along with assumptions that define these operators
in terms of the ones of class @{class linorder}.
The resulting class is a subclass of @{class distrib_lattice}. *}
@@ -194,9 +215,8 @@
text {* The definitional assumptions
on the operators @{const inf} and @{const sup}
of class @{class linorder_lattice}
-ensure that they yield infimum and supremum,
-and that they distribute over each other,
-as required for a distributive lattice. *}
+ensure that they yield infimum and supremum
+and that they distribute over each other. *}
lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
unfolding inf_def by (metis (full_types) linorder_linear)
@@ -250,3 +270,4 @@
end
+
--- a/src/HOL/Library/List_lexord.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/List_lexord.thy Thu Jul 25 08:57:16 2013 +0200
@@ -91,7 +91,7 @@
lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
by (unfold list_le_def) auto
-instantiation list :: (order) bot
+instantiation list :: (order) order_bot
begin
definition
--- a/src/HOL/Library/Option_ord.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Option_ord.thy Thu Jul 25 08:57:16 2013 +0200
@@ -73,7 +73,7 @@
instance option :: (linorder) linorder proof
qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
-instantiation option :: (order) bot
+instantiation option :: (order) order_bot
begin
definition bot_option where
@@ -84,7 +84,7 @@
end
-instantiation option :: (top) top
+instantiation option :: (order_top) order_top
begin
definition top_option where
@@ -272,6 +272,12 @@
then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
with Some show ?thesis by (simp add: Sup_option_def)
qed
+next
+ show "\<Squnion>{} = (\<bottom>::'a option)"
+ by (auto simp: bot_option_def)
+next
+ show "\<Sqinter>{} = (\<top>::'a option)"
+ by (auto simp: top_option_def Inf_option_def)
qed
end
--- a/src/HOL/Library/Product_Lexorder.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Product_Lexorder.thy Thu Jul 25 08:57:16 2013 +0200
@@ -65,22 +65,26 @@
definition
"bot = (bot, bot)"
-instance
- by default (auto simp add: bot_prod_def)
+instance ..
end
+instance prod :: (order_bot, order_bot) order_bot
+ by default (auto simp add: bot_prod_def)
+
instantiation prod :: (top, top) top
begin
definition
"top = (top, top)"
-instance
- by default (auto simp add: top_prod_def)
+instance ..
end
+instance prod :: (order_top, order_top) order_top
+ by default (auto simp add: top_prod_def)
+
instance prod :: (wellorder, wellorder) wellorder
proof
fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
--- a/src/HOL/Library/Product_Order.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Product_Order.thy Thu Jul 25 08:57:16 2013 +0200
@@ -108,6 +108,10 @@
definition
"top = (top, top)"
+instance ..
+
+end
+
lemma fst_top [simp]: "fst top = top"
unfolding top_prod_def by simp
@@ -117,17 +121,19 @@
lemma Pair_top_top: "(top, top) = top"
unfolding top_prod_def by simp
-instance
+instance prod :: (order_top, order_top) order_top
by default (auto simp add: top_prod_def)
-end
-
instantiation prod :: (bot, bot) bot
begin
definition
"bot = (bot, bot)"
+instance ..
+
+end
+
lemma fst_bot [simp]: "fst bot = bot"
unfolding bot_prod_def by simp
@@ -137,11 +143,9 @@
lemma Pair_bot_bot: "(bot, bot) = bot"
unfolding bot_prod_def by simp
-instance
+instance prod :: (order_bot, order_bot) order_bot
by default (auto simp add: bot_prod_def)
-end
-
instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
@@ -161,7 +165,7 @@
instance
by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
- INF_lower SUP_upper le_INF_iff SUP_le_iff)
+ INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
end
--- a/src/HOL/Library/Saturated.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Saturated.thy Thu Jul 25 08:57:16 2013 +0200
@@ -263,6 +263,12 @@
note finite
moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
ultimately show "Sup A \<le> z" by (induct A) auto
+next
+ show "Inf {} = (top::'a sat)"
+ by (auto simp: top_sat_def)
+next
+ show "Sup {} = (bot::'a sat)"
+ by (auto simp: bot_sat_def)
qed
hide_const (open) sat_of_nat
--- a/src/HOL/Library/Sublist.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Sublist.thy Thu Jul 25 08:57:16 2013 +0200
@@ -20,7 +20,7 @@
interpretation prefix_order: order prefixeq prefix
by default (auto simp: prefixeq_def prefix_def)
-interpretation prefix_bot: bot prefixeq prefix Nil
+interpretation prefix_bot: order_bot Nil prefixeq prefix
by default (simp add: prefixeq_def)
lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
--- a/src/HOL/Nat.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Nat.thy Thu Jul 25 08:57:16 2013 +0200
@@ -444,7 +444,7 @@
end
-instantiation nat :: bot
+instantiation nat :: order_bot
begin
definition bot_nat :: nat where
@@ -1318,7 +1318,8 @@
subsection {* Kleene iteration *}
-lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
+lemma Kleene_iter_lpfp:
+assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
proof(induction k)
case 0 show ?case by simp
next
--- a/src/HOL/Orderings.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Orderings.thy Thu Jul 25 08:57:16 2013 +0200
@@ -1167,14 +1167,16 @@
subsection {* (Unique) top and bottom elements *}
-class bot = order +
+class bot =
fixes bot :: 'a ("\<bottom>")
+
+class order_bot = order + bot +
assumes bot_least: "\<bottom> \<le> a"
-sublocale bot < bot!: ordering_top greater_eq greater bot
+sublocale order_bot < bot!: ordering_top greater_eq greater bot
by default (fact bot_least)
-context bot
+context order_bot
begin
lemma le_bot:
@@ -1195,14 +1197,16 @@
end
-class top = order +
+class top =
fixes top :: 'a ("\<top>")
+
+class order_top = order + top +
assumes top_greatest: "a \<le> \<top>"
-sublocale top < top!: ordering_top less_eq less top
+sublocale order_top < top!: ordering_top less_eq less top
by default (fact top_greatest)
-context top
+context order_top
begin
lemma top_le:
@@ -1380,7 +1384,7 @@
subsection {* Order on @{typ bool} *}
-instantiation bool :: "{bot, top, linorder}"
+instantiation bool :: "{order_bot, order_top, linorder}"
begin
definition
@@ -1454,6 +1458,13 @@
definition
"\<bottom> = (\<lambda>x. \<bottom>)"
+instance ..
+
+end
+
+instantiation "fun" :: (type, order_bot) order_bot
+begin
+
lemma bot_apply [simp, code]:
"\<bottom> x = \<bottom>"
by (simp add: bot_fun_def)
@@ -1469,6 +1480,13 @@
definition
[no_atp]: "\<top> = (\<lambda>x. \<top>)"
+instance ..
+
+end
+
+instantiation "fun" :: (type, order_top) order_top
+begin
+
lemma top_apply [simp, code]:
"\<top> x = \<top>"
by (simp add: top_fun_def)
--- a/src/HOL/Set_Interval.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Set_Interval.thy Thu Jul 25 08:57:16 2013 +0200
@@ -197,8 +197,8 @@
by (simp add: atLeastAtMost_def)
text {* The above four lemmas could be declared as iffs. Unfortunately this
-breaks many proofs. Since it only helps blast, it is better to leave well
-alone *}
+breaks many proofs. Since it only helps blast, it is better to leave them
+alone. *}
lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
by auto
@@ -452,10 +452,10 @@
shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
using atLeastLessThan_inj assms by auto
-lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
+lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
by (auto simp: set_eq_iff intro: le_bot)
-lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
+lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
by (auto simp: set_eq_iff intro: top_le)
lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
--- a/src/HOL/Topological_Spaces.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Topological_Spaces.thy Thu Jul 25 08:57:16 2013 +0200
@@ -471,27 +471,28 @@
unfolding le_filter_def by simp }
{ assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
unfolding le_filter_def filter_eq_iff by fast }
- { show "F \<le> top"
- unfolding le_filter_def eventually_top by (simp add: always_eventually) }
- { show "bot \<le> F"
- unfolding le_filter_def by simp }
- { show "F \<le> sup F F'" and "F' \<le> sup F F'"
- unfolding le_filter_def eventually_sup by simp_all }
- { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
- unfolding le_filter_def eventually_sup by simp }
{ show "inf F F' \<le> F" and "inf F F' \<le> F'"
unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
{ assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
unfolding le_filter_def eventually_inf
by (auto elim!: eventually_mono intro: eventually_conj) }
+ { show "F \<le> sup F F'" and "F' \<le> sup F F'"
+ unfolding le_filter_def eventually_sup by simp_all }
+ { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
+ unfolding le_filter_def eventually_sup by simp }
+ { assume "F'' \<in> S" thus "Inf S \<le> F''"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+ { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
+ unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
{ assume "F \<in> S" thus "F \<le> Sup S"
unfolding le_filter_def eventually_Sup by simp }
{ assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
unfolding le_filter_def eventually_Sup by simp }
- { assume "F'' \<in> S" thus "Inf S \<le> F''"
- unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
- { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
- unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
+ { show "Inf {} = (top::'a filter)"
+ by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
+ (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) }
+ { show "Sup {} = (bot::'a filter)"
+ by (auto simp: bot_filter_def Sup_filter_def) }
qed
end
--- a/src/HOL/ex/FinFunPred.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/ex/FinFunPred.thy Thu Jul 25 08:57:16 2013 +0200
@@ -31,7 +31,7 @@
instance "finfun" :: (type, order) order
by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
-instantiation "finfun" :: (type, bot) bot begin
+instantiation "finfun" :: (type, order_bot) order_bot begin
definition "bot = finfun_const bot"
instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
end
@@ -39,7 +39,7 @@
lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
by(auto simp add: bot_finfun_def)
-instantiation "finfun" :: (type, top) top begin
+instantiation "finfun" :: (type, order_top) order_top begin
definition "top = finfun_const top"
instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
end