1.1 --- a/src/HOL/Complete_Lattices.thy Wed Jul 24 17:15:59 2013 +0200
1.2 +++ b/src/HOL/Complete_Lattices.thy Thu Jul 25 08:57:16 2013 +0200
1.3 @@ -22,17 +22,31 @@
1.4
1.5 subsection {* Abstract complete lattices *}
1.6
1.7 -class complete_lattice = bounded_lattice + Inf + Sup +
1.8 +text {* A complete lattice always has a bottom and a top,
1.9 +so we include them into the following type class,
1.10 +along with assumptions that define bottom and top
1.11 +in terms of infimum and supremum. *}
1.12 +
1.13 +class complete_lattice = lattice + Inf + Sup + bot + top +
1.14 assumes Inf_lower: "x \<in> A \<Longrightarrow> \<Sqinter>A \<sqsubseteq> x"
1.15 and Inf_greatest: "(\<And>x. x \<in> A \<Longrightarrow> z \<sqsubseteq> x) \<Longrightarrow> z \<sqsubseteq> \<Sqinter>A"
1.16 assumes Sup_upper: "x \<in> A \<Longrightarrow> x \<sqsubseteq> \<Squnion>A"
1.17 and Sup_least: "(\<And>x. x \<in> A \<Longrightarrow> x \<sqsubseteq> z) \<Longrightarrow> \<Squnion>A \<sqsubseteq> z"
1.18 + assumes Inf_empty [simp]: "\<Sqinter>{} = \<top>"
1.19 + assumes Sup_empty [simp]: "\<Squnion>{} = \<bottom>"
1.20 begin
1.21
1.22 +subclass bounded_lattice
1.23 +proof
1.24 + fix a
1.25 + show "\<bottom> \<le> a" by (auto intro: Sup_least simp only: Sup_empty [symmetric])
1.26 + show "a \<le> \<top>" by (auto intro: Inf_greatest simp only: Inf_empty [symmetric])
1.27 +qed
1.28 +
1.29 lemma dual_complete_lattice:
1.30 "class.complete_lattice Sup Inf sup (op \<ge>) (op >) inf \<top> \<bottom>"
1.31 - by (auto intro!: class.complete_lattice.intro dual_bounded_lattice)
1.32 - (unfold_locales, (fact bot_least top_greatest
1.33 + by (auto intro!: class.complete_lattice.intro dual_lattice)
1.34 + (unfold_locales, (fact Inf_empty Sup_empty
1.35 Sup_upper Sup_least Inf_lower Inf_greatest)+)
1.36
1.37 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
1.38 @@ -141,17 +155,21 @@
1.39 lemma SUP_le_iff: "(\<Squnion>i\<in>A. f i) \<sqsubseteq> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<sqsubseteq> u)"
1.40 by (auto simp add: SUP_def Sup_le_iff)
1.41
1.42 -lemma Inf_empty [simp]:
1.43 - "\<Sqinter>{} = \<top>"
1.44 - by (auto intro: antisym Inf_greatest)
1.45 +lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
1.46 + by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
1.47 +
1.48 +lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
1.49 + by (simp add: INF_def)
1.50 +
1.51 +lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
1.52 + by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
1.53 +
1.54 +lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
1.55 + by (simp add: SUP_def)
1.56
1.57 lemma INF_empty [simp]: "(\<Sqinter>x\<in>{}. f x) = \<top>"
1.58 by (simp add: INF_def)
1.59
1.60 -lemma Sup_empty [simp]:
1.61 - "\<Squnion>{} = \<bottom>"
1.62 - by (auto intro: antisym Sup_least)
1.63 -
1.64 lemma SUP_empty [simp]: "(\<Squnion>x\<in>{}. f x) = \<bottom>"
1.65 by (simp add: SUP_def)
1.66
1.67 @@ -163,18 +181,6 @@
1.68 "\<Squnion>UNIV = \<top>"
1.69 by (auto intro!: antisym Sup_upper)
1.70
1.71 -lemma Inf_insert [simp]: "\<Sqinter>insert a A = a \<sqinter> \<Sqinter>A"
1.72 - by (auto intro: le_infI le_infI1 le_infI2 antisym Inf_greatest Inf_lower)
1.73 -
1.74 -lemma INF_insert: "(\<Sqinter>x\<in>insert a A. f x) = f a \<sqinter> INFI A f"
1.75 - by (simp add: INF_def)
1.76 -
1.77 -lemma Sup_insert [simp]: "\<Squnion>insert a A = a \<squnion> \<Squnion>A"
1.78 - by (auto intro: le_supI le_supI1 le_supI2 antisym Sup_least Sup_upper)
1.79 -
1.80 -lemma SUP_insert: "(\<Squnion>x\<in>insert a A. f x) = f a \<squnion> SUPR A f"
1.81 - by (simp add: SUP_def)
1.82 -
1.83 lemma INF_image [simp]: "(\<Sqinter>x\<in>f`A. g x) = (\<Sqinter>x\<in>A. g (f x))"
1.84 by (simp add: INF_def image_image)
1.85
2.1 --- a/src/HOL/GCD.thy Wed Jul 24 17:15:59 2013 +0200
2.2 +++ b/src/HOL/GCD.thy Thu Jul 25 08:57:16 2013 +0200
2.3 @@ -1560,17 +1560,17 @@
2.4 proof -
2.5 show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
2.6 proof
2.7 - case goal1 show ?case by simp
2.8 + case goal1 thus ?case by (simp add: Gcd_nat_def)
2.9 next
2.10 - case goal2 show ?case by simp
2.11 + case goal2 thus ?case by (simp add: Gcd_nat_def)
2.12 next
2.13 - case goal5 thus ?case by (rule dvd_Lcm_nat)
2.14 + case goal5 show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
2.15 next
2.16 - case goal6 thus ?case by simp
2.17 + case goal6 show ?case by (simp add: Lcm_nat_empty)
2.18 next
2.19 - case goal3 thus ?case by (simp add: Gcd_nat_def)
2.20 + case goal3 thus ?case by simp
2.21 next
2.22 - case goal4 thus ?case by (simp add: Gcd_nat_def)
2.23 + case goal4 thus ?case by simp
2.24 qed
2.25 then interpret gcd_lcm_complete_lattice_nat:
2.26 complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
3.1 --- a/src/HOL/IMP/Abs_Int0.thy Wed Jul 24 17:15:59 2013 +0200
3.2 +++ b/src/HOL/IMP/Abs_Int0.thy Thu Jul 25 08:57:16 2013 +0200
3.3 @@ -6,11 +6,11 @@
3.4
3.5 subsection "Orderings"
3.6
3.7 -text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class top} are
3.8 +text{* The basic type classes @{class order}, @{class semilattice_sup} and @{class order_top} are
3.9 defined in @{theory Main}, more precisely in theories @{theory Orderings} and @{theory Lattices}.
3.10 If you view this theory with jedit, just click on the names to get there. *}
3.11
3.12 -class semilattice_sup_top = semilattice_sup + top
3.13 +class semilattice_sup_top = semilattice_sup + order_top
3.14
3.15
3.16 instance "fun" :: (type, semilattice_sup_top) semilattice_sup_top ..
3.17 @@ -78,7 +78,7 @@
3.18 lemma [simp]: "(Some x < Some y) = (x < y)"
3.19 by(auto simp: less_le)
3.20
3.21 -instantiation option :: (order)bot
3.22 +instantiation option :: (order)order_bot
3.23 begin
3.24
3.25 definition bot_option :: "'a option" where
4.1 --- a/src/HOL/IMP/Abs_Int1.thy Wed Jul 24 17:15:59 2013 +0200
4.2 +++ b/src/HOL/IMP/Abs_Int1.thy Thu Jul 25 08:57:16 2013 +0200
4.3 @@ -100,7 +100,7 @@
4.4 subsubsection "Termination"
4.5
4.6 locale Measure1 =
4.7 -fixes m :: "'av::{order,top} \<Rightarrow> nat"
4.8 +fixes m :: "'av::{order,order_top} \<Rightarrow> nat"
4.9 fixes h :: "nat"
4.10 assumes h: "m x \<le> h"
4.11 begin
4.12 @@ -134,14 +134,14 @@
4.13
4.14 end
4.15
4.16 -fun top_on_st :: "'a::top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
4.17 +fun top_on_st :: "'a::order_top st \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>s") where
4.18 "top_on_st S X = (\<forall>x\<in>X. fun S x = \<top>)"
4.19
4.20 -fun top_on_opt :: "'a::top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
4.21 +fun top_on_opt :: "'a::order_top st option \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>o") where
4.22 "top_on_opt (Some S) X = top_on_st S X" |
4.23 "top_on_opt None X = True"
4.24
4.25 -definition top_on_acom :: "'a::top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
4.26 +definition top_on_acom :: "'a::order_top st option acom \<Rightarrow> vname set \<Rightarrow> bool" ("top'_on\<^isub>c") where
4.27 "top_on_acom C X = (\<forall>a \<in> set(annos C). top_on_opt a X)"
4.28
4.29 lemma top_on_top: "top_on_opt (\<top>::_ st option) X"
5.1 --- a/src/HOL/IMP/Abs_Int3.thy Wed Jul 24 17:15:59 2013 +0200
5.2 +++ b/src/HOL/IMP/Abs_Int3.thy Thu Jul 25 08:57:16 2013 +0200
5.3 @@ -25,7 +25,7 @@
5.4
5.5 end
5.6
5.7 -lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,top})"
5.8 +lemma top_widen_top[simp]: "\<top> \<nabla> \<top> = (\<top>::_::{wn,order_top})"
5.9 by (metis eq_iff top_greatest widen2)
5.10
5.11 instantiation ivl :: wn
5.12 @@ -53,7 +53,7 @@
5.13
5.14 end
5.15
5.16 -instantiation st :: ("{top,wn}")wn
5.17 +instantiation st :: ("{order_top,wn}")wn
5.18 begin
5.19
5.20 lift_definition widen_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<nabla>)"
5.21 @@ -335,7 +335,7 @@
5.22 widening. *}
5.23
5.24 locale Measure_wn = Measure1 where m=m
5.25 - for m :: "'av::{top,wn} \<Rightarrow> nat" +
5.26 + for m :: "'av::{order_top,wn} \<Rightarrow> nat" +
5.27 fixes n :: "'av \<Rightarrow> nat"
5.28 assumes m_anti_mono: "x \<le> y \<Longrightarrow> m x \<ge> m y"
5.29 assumes m_widen: "~ y \<le> x \<Longrightarrow> m(x \<nabla> y) < m x"
6.1 --- a/src/HOL/IMP/Abs_State.thy Wed Jul 24 17:15:59 2013 +0200
6.2 +++ b/src/HOL/IMP/Abs_State.thy Thu Jul 25 08:57:16 2013 +0200
6.3 @@ -6,7 +6,7 @@
6.4
6.5 type_synonym 'a st_rep = "(vname * 'a) list"
6.6
6.7 -fun fun_rep :: "('a::top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
6.8 +fun fun_rep :: "('a::order_top) st_rep \<Rightarrow> vname \<Rightarrow> 'a" where
6.9 "fun_rep [] = (\<lambda>x. \<top>)" |
6.10 "fun_rep ((x,a)#ps) = (fun_rep ps) (x := a)"
6.11
6.12 @@ -14,23 +14,23 @@
6.13 "fun_rep ps = (%x. case map_of ps x of None \<Rightarrow> \<top> | Some a \<Rightarrow> a)"
6.14 by(induction ps rule: fun_rep.induct) auto
6.15
6.16 -definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
6.17 +definition eq_st :: "('a::order_top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
6.18 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
6.19
6.20 hide_type st --"hide previous def to avoid long names"
6.21
6.22 -quotient_type 'a st = "('a::top) st_rep" / eq_st
6.23 +quotient_type 'a st = "('a::order_top) st_rep" / eq_st
6.24 morphisms rep_st St
6.25 by (metis eq_st_def equivpI reflpI sympI transpI)
6.26
6.27 -lift_definition update :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
6.28 +lift_definition update :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a \<Rightarrow> 'a st"
6.29 is "\<lambda>ps x a. (x,a)#ps"
6.30 by(auto simp: eq_st_def)
6.31
6.32 -lift_definition "fun" :: "('a::top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
6.33 +lift_definition "fun" :: "('a::order_top) st \<Rightarrow> vname \<Rightarrow> 'a" is fun_rep
6.34 by(simp add: eq_st_def)
6.35
6.36 -definition show_st :: "vname set \<Rightarrow> ('a::top) st \<Rightarrow> (vname * 'a)set" where
6.37 +definition show_st :: "vname set \<Rightarrow> ('a::order_top) st \<Rightarrow> (vname * 'a)set" where
6.38 "show_st X S = (\<lambda>x. (x, fun S x)) ` X"
6.39
6.40 definition "show_acom C = map_acom (Option.map (show_st (vars(strip C)))) C"
6.41 @@ -39,10 +39,10 @@
6.42 lemma fun_update[simp]: "fun (update S x y) = (fun S)(x:=y)"
6.43 by transfer auto
6.44
6.45 -definition \<gamma>_st :: "(('a::top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
6.46 +definition \<gamma>_st :: "(('a::order_top) \<Rightarrow> 'b set) \<Rightarrow> 'a st \<Rightarrow> (vname \<Rightarrow> 'b) set" where
6.47 "\<gamma>_st \<gamma> F = {f. \<forall>x. f x \<in> \<gamma>(fun F x)}"
6.48
6.49 -instantiation st :: ("{order,top}") order
6.50 +instantiation st :: ("{order,order_top}") order
6.51 begin
6.52
6.53 definition less_eq_st_rep :: "'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
6.54 @@ -83,7 +83,7 @@
6.55 lemma le_st_iff: "(F \<le> G) = (\<forall>x. fun F x \<le> fun G x)"
6.56 by transfer (rule less_eq_st_rep_iff)
6.57
6.58 -fun map2_st_rep :: "('a::top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
6.59 +fun map2_st_rep :: "('a::order_top \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep \<Rightarrow> 'a st_rep" where
6.60 "map2_st_rep f [] ps2 = map (%(x,y). (x, f \<top> y)) ps2" |
6.61 "map2_st_rep f ((x,y)#ps1) ps2 =
6.62 (let y2 = fun_rep ps2 x
7.1 --- a/src/HOL/Lattices.thy Wed Jul 24 17:15:59 2013 +0200
7.2 +++ b/src/HOL/Lattices.thy Thu Jul 25 08:57:16 2013 +0200
7.3 @@ -466,7 +466,7 @@
7.4
7.5 subsection {* Bounded lattices and boolean algebras *}
7.6
7.7 -class bounded_semilattice_inf_top = semilattice_inf + top
7.8 +class bounded_semilattice_inf_top = semilattice_inf + order_top
7.9 begin
7.10
7.11 sublocale inf_top!: semilattice_neutr inf top
7.12 @@ -479,7 +479,7 @@
7.13
7.14 end
7.15
7.16 -class bounded_semilattice_sup_bot = semilattice_sup + bot
7.17 +class bounded_semilattice_sup_bot = semilattice_sup + order_bot
7.18 begin
7.19
7.20 sublocale sup_bot!: semilattice_neutr sup bot
7.21 @@ -492,7 +492,7 @@
7.22
7.23 end
7.24
7.25 -class bounded_lattice_bot = lattice + bot
7.26 +class bounded_lattice_bot = lattice + order_bot
7.27 begin
7.28
7.29 subclass bounded_semilattice_sup_bot ..
7.30 @@ -523,7 +523,7 @@
7.31
7.32 end
7.33
7.34 -class bounded_lattice_top = lattice + top
7.35 +class bounded_lattice_top = lattice + order_top
7.36 begin
7.37
7.38 subclass bounded_semilattice_inf_top ..
7.39 @@ -550,7 +550,7 @@
7.40
7.41 end
7.42
7.43 -class bounded_lattice = lattice + bot + top
7.44 +class bounded_lattice = lattice + order_bot + order_top
7.45 begin
7.46
7.47 subclass bounded_lattice_bot ..
8.1 --- a/src/HOL/Library/Extended_Nat.thy Wed Jul 24 17:15:59 2013 +0200
8.2 +++ b/src/HOL/Library/Extended_Nat.thy Thu Jul 25 08:57:16 2013 +0200
8.3 @@ -452,7 +452,7 @@
8.4 apply (erule (1) le_less_trans)
8.5 done
8.6
8.7 -instantiation enat :: "{bot, top}"
8.8 +instantiation enat :: "{order_bot, order_top}"
8.9 begin
8.10
8.11 definition bot_enat :: enat where
8.12 @@ -623,7 +623,8 @@
8.13 unfolding Sup_enat_def by (cases "finite A") auto }
8.14 { assume "\<And>y. y \<in> A \<Longrightarrow> y \<le> x" then show "Sup A \<le> x"
8.15 unfolding Sup_enat_def using finite_enat_bounded by auto }
8.16 -qed (simp_all add: inf_enat_def sup_enat_def)
8.17 +qed (simp_all add:
8.18 + inf_enat_def sup_enat_def bot_enat_def top_enat_def Inf_enat_def Sup_enat_def)
8.19 end
8.20
8.21 instance enat :: complete_linorder ..
9.1 --- a/src/HOL/Library/Extended_Real.thy Wed Jul 24 17:15:59 2013 +0200
9.2 +++ b/src/HOL/Library/Extended_Real.thy Thu Jul 25 08:57:16 2013 +0200
9.3 @@ -1144,8 +1144,22 @@
9.4 using ereal_complete_Sup[of "uminus ` S"] unfolding ereal_complete_uminus_eq by auto
9.5
9.6 instance
9.7 - by default (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
9.8 - simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
9.9 +proof
9.10 + show "Sup {} = (bot::ereal)"
9.11 + apply (auto simp: bot_ereal_def Sup_ereal_def)
9.12 + apply (rule some1_equality)
9.13 + apply (metis ereal_bot ereal_less_eq(2))
9.14 + apply (metis ereal_less_eq(2))
9.15 + done
9.16 +next
9.17 + show "Inf {} = (top::ereal)"
9.18 + apply (auto simp: top_ereal_def Inf_ereal_def)
9.19 + apply (rule some1_equality)
9.20 + apply (metis ereal_top ereal_less_eq(1))
9.21 + apply (metis ereal_less_eq(1))
9.22 + done
9.23 +qed (auto intro: someI2_ex ereal_complete_Sup ereal_complete_Inf
9.24 + simp: Sup_ereal_def Inf_ereal_def bot_ereal_def top_ereal_def)
9.25
9.26 end
9.27
10.1 --- a/src/HOL/Library/Finite_Lattice.thy Wed Jul 24 17:15:59 2013 +0200
10.2 +++ b/src/HOL/Library/Finite_Lattice.thy Thu Jul 25 08:57:16 2013 +0200
10.3 @@ -13,31 +13,39 @@
10.4 with the operators @{const bot}, @{const top}, @{const Inf}, and @{const Sup},
10.5 along with assumptions that define these operators
10.6 in terms of the ones of classes @{class finite} and @{class lattice}.
10.7 -The resulting class is a subclass of @{class complete_lattice}.
10.8 -Classes @{class bot} and @{class top} already include assumptions that suffice
10.9 -to define the operators @{const bot} and @{const top} (as proved below),
10.10 -and so no explicit assumptions on these two operators are needed
10.11 -in the following type class.%
10.12 -\footnote{The Isabelle/HOL library does not provide
10.13 -syntactic classes for the operators @{const bot} and @{const top}.} *}
10.14 +The resulting class is a subclass of @{class complete_lattice}. *}
10.15
10.16 class finite_lattice_complete = finite + lattice + bot + top + Inf + Sup +
10.17 +assumes bot_def: "bot = Inf_fin UNIV"
10.18 +assumes top_def: "top = Sup_fin UNIV"
10.19 assumes Inf_def: "Inf A = Finite_Set.fold inf top A"
10.20 assumes Sup_def: "Sup A = Finite_Set.fold sup bot A"
10.21 --- "No explicit assumptions on @{const bot} or @{const top}."
10.22 +
10.23 +text {* The definitional assumptions
10.24 +on the operators @{const bot} and @{const top}
10.25 +of class @{class finite_lattice_complete}
10.26 +ensure that they yield bottom and top. *}
10.27 +
10.28 +lemma finite_lattice_complete_bot_least:
10.29 +"(bot::'a::finite_lattice_complete) \<le> x"
10.30 +by (auto simp: bot_def intro: Inf_fin.coboundedI)
10.31 +
10.32 +instance finite_lattice_complete \<subseteq> order_bot
10.33 +proof qed (auto simp: finite_lattice_complete_bot_least)
10.34 +
10.35 +lemma finite_lattice_complete_top_greatest:
10.36 +"(top::'a::finite_lattice_complete) \<ge> x"
10.37 +by (auto simp: top_def Sup_fin.coboundedI)
10.38 +
10.39 +instance finite_lattice_complete \<subseteq> order_top
10.40 +proof qed (auto simp: finite_lattice_complete_top_greatest)
10.41
10.42 instance finite_lattice_complete \<subseteq> bounded_lattice ..
10.43 --- "This subclass relation eases the proof of the next two lemmas."
10.44
10.45 -lemma finite_lattice_complete_bot_def:
10.46 - "(bot::'a::finite_lattice_complete) = \<Sqinter>\<^bsub>fin\<^esub>UNIV"
10.47 -by (metis finite_UNIV sup_Inf_absorb sup_bot_left iso_tuple_UNIV_I)
10.48 --- "Derived definition of @{const bot}."
10.49 -
10.50 -lemma finite_lattice_complete_top_def:
10.51 - "(top::'a::finite_lattice_complete) = \<Squnion>\<^bsub>fin\<^esub>UNIV"
10.52 -by (metis finite_UNIV inf_Sup_absorb inf_top_left iso_tuple_UNIV_I)
10.53 --- "Derived definition of @{const top}."
10.54 +text {* The definitional assumptions
10.55 +on the operators @{const Inf} and @{const Sup}
10.56 +of class @{class finite_lattice_complete}
10.57 +ensure that they yield infimum and supremum. *}
10.58
10.59 lemma finite_lattice_complete_Inf_empty:
10.60 "Inf {} = (top :: 'a::finite_lattice_complete)"
10.61 @@ -63,12 +71,6 @@
10.62 show ?thesis by (simp add: Sup_def)
10.63 qed
10.64
10.65 -text {* The definitional assumptions
10.66 -on the operators @{const Inf} and @{const Sup}
10.67 -of class @{class finite_lattice_complete}
10.68 -ensure that they yield infimum and supremum,
10.69 -as required for a complete lattice. *}
10.70 -
10.71 lemma finite_lattice_complete_Inf_lower:
10.72 "(x::'a::finite_lattice_complete) \<in> A \<Longrightarrow> Inf A \<le> x"
10.73 using finite [of A] by (induct A) (auto simp add: finite_lattice_complete_Inf_insert intro: le_infI2)
10.74 @@ -91,28 +93,48 @@
10.75 finite_lattice_complete_Inf_lower
10.76 finite_lattice_complete_Inf_greatest
10.77 finite_lattice_complete_Sup_upper
10.78 - finite_lattice_complete_Sup_least)
10.79 -
10.80 + finite_lattice_complete_Sup_least
10.81 + finite_lattice_complete_Inf_empty
10.82 + finite_lattice_complete_Sup_empty)
10.83
10.84 text {* The product of two finite lattices is already a finite lattice. *}
10.85
10.86 +lemma finite_bot_prod:
10.87 + "(bot :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
10.88 + Inf_fin UNIV"
10.89 +by (metis Inf_fin.coboundedI UNIV_I bot.extremum_uniqueI finite_UNIV)
10.90 +
10.91 +lemma finite_top_prod:
10.92 + "(top :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete)) =
10.93 + Sup_fin UNIV"
10.94 +by (metis Sup_fin.coboundedI UNIV_I top.extremum_uniqueI finite_UNIV)
10.95 +
10.96 lemma finite_Inf_prod:
10.97 - "Inf(A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
10.98 + "Inf(A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
10.99 Finite_Set.fold inf top A"
10.100 by (metis Inf_fold_inf finite_code)
10.101
10.102 lemma finite_Sup_prod:
10.103 - "Sup (A::('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
10.104 + "Sup (A :: ('a::finite_lattice_complete \<times> 'b::finite_lattice_complete) set) =
10.105 Finite_Set.fold sup bot A"
10.106 by (metis Sup_fold_sup finite_code)
10.107
10.108 instance prod ::
10.109 (finite_lattice_complete, finite_lattice_complete) finite_lattice_complete
10.110 -proof qed (auto simp: finite_Inf_prod finite_Sup_prod)
10.111 +proof
10.112 +qed (auto simp: finite_bot_prod finite_top_prod finite_Inf_prod finite_Sup_prod)
10.113
10.114 text {* Functions with a finite domain and with a finite lattice as codomain
10.115 already form a finite lattice. *}
10.116
10.117 +lemma finite_bot_fun:
10.118 + "(bot :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Inf_fin UNIV"
10.119 +by (metis Inf_UNIV Inf_fin_Inf empty_not_UNIV finite_code)
10.120 +
10.121 +lemma finite_top_fun:
10.122 + "(top :: ('a::finite \<Rightarrow> 'b::finite_lattice_complete)) = Sup_fin UNIV"
10.123 +by (metis Sup_UNIV Sup_fin_Sup empty_not_UNIV finite_code)
10.124 +
10.125 lemma finite_Inf_fun:
10.126 "Inf (A::('a::finite \<Rightarrow> 'b::finite_lattice_complete) set) =
10.127 Finite_Set.fold inf top A"
10.128 @@ -124,7 +146,8 @@
10.129 by (metis Sup_fold_sup finite_code)
10.130
10.131 instance "fun" :: (finite, finite_lattice_complete) finite_lattice_complete
10.132 -proof qed (auto simp: finite_Inf_fun finite_Sup_fun)
10.133 +proof
10.134 +qed (auto simp: finite_bot_fun finite_top_fun finite_Inf_fun finite_Sup_fun)
10.135
10.136
10.137 subsection {* Finite Distributive Lattices *}
10.138 @@ -178,11 +201,9 @@
10.139 subsection {* Linear Orders *}
10.140
10.141 text {* A linear order is a distributive lattice.
10.142 -Since in Isabelle/HOL
10.143 -a subclass must have all the parameters of its superclasses,
10.144 -class @{class linorder} cannot be a subclass of @{class distrib_lattice}.
10.145 -So class @{class linorder} is extended with
10.146 -the operators @{const inf} and @{const sup},
10.147 +A type class is defined
10.148 +that extends class @{class linorder}
10.149 +with the operators @{const inf} and @{const sup},
10.150 along with assumptions that define these operators
10.151 in terms of the ones of class @{class linorder}.
10.152 The resulting class is a subclass of @{class distrib_lattice}. *}
10.153 @@ -194,9 +215,8 @@
10.154 text {* The definitional assumptions
10.155 on the operators @{const inf} and @{const sup}
10.156 of class @{class linorder_lattice}
10.157 -ensure that they yield infimum and supremum,
10.158 -and that they distribute over each other,
10.159 -as required for a distributive lattice. *}
10.160 +ensure that they yield infimum and supremum
10.161 +and that they distribute over each other. *}
10.162
10.163 lemma linorder_lattice_inf_le1: "inf (x::'a::linorder_lattice) y \<le> x"
10.164 unfolding inf_def by (metis (full_types) linorder_linear)
10.165 @@ -250,3 +270,4 @@
10.166
10.167
10.168 end
10.169 +
11.1 --- a/src/HOL/Library/List_lexord.thy Wed Jul 24 17:15:59 2013 +0200
11.2 +++ b/src/HOL/Library/List_lexord.thy Thu Jul 25 08:57:16 2013 +0200
11.3 @@ -91,7 +91,7 @@
11.4 lemma Cons_le_Cons [simp]: "a # x \<le> b # y \<longleftrightarrow> a < b \<or> a = b \<and> x \<le> y"
11.5 by (unfold list_le_def) auto
11.6
11.7 -instantiation list :: (order) bot
11.8 +instantiation list :: (order) order_bot
11.9 begin
11.10
11.11 definition
12.1 --- a/src/HOL/Library/Option_ord.thy Wed Jul 24 17:15:59 2013 +0200
12.2 +++ b/src/HOL/Library/Option_ord.thy Thu Jul 25 08:57:16 2013 +0200
12.3 @@ -73,7 +73,7 @@
12.4 instance option :: (linorder) linorder proof
12.5 qed (auto simp add: less_eq_option_def less_option_def split: option.splits)
12.6
12.7 -instantiation option :: (order) bot
12.8 +instantiation option :: (order) order_bot
12.9 begin
12.10
12.11 definition bot_option where
12.12 @@ -84,7 +84,7 @@
12.13
12.14 end
12.15
12.16 -instantiation option :: (top) top
12.17 +instantiation option :: (order_top) order_top
12.18 begin
12.19
12.20 definition top_option where
12.21 @@ -272,6 +272,12 @@
12.22 then have "\<Squnion>Option.these A \<le> y" by (rule Sup_least)
12.23 with Some show ?thesis by (simp add: Sup_option_def)
12.24 qed
12.25 +next
12.26 + show "\<Squnion>{} = (\<bottom>::'a option)"
12.27 + by (auto simp: bot_option_def)
12.28 +next
12.29 + show "\<Sqinter>{} = (\<top>::'a option)"
12.30 + by (auto simp: top_option_def Inf_option_def)
12.31 qed
12.32
12.33 end
13.1 --- a/src/HOL/Library/Product_Lexorder.thy Wed Jul 24 17:15:59 2013 +0200
13.2 +++ b/src/HOL/Library/Product_Lexorder.thy Thu Jul 25 08:57:16 2013 +0200
13.3 @@ -65,22 +65,26 @@
13.4 definition
13.5 "bot = (bot, bot)"
13.6
13.7 -instance
13.8 - by default (auto simp add: bot_prod_def)
13.9 +instance ..
13.10
13.11 end
13.12
13.13 +instance prod :: (order_bot, order_bot) order_bot
13.14 + by default (auto simp add: bot_prod_def)
13.15 +
13.16 instantiation prod :: (top, top) top
13.17 begin
13.18
13.19 definition
13.20 "top = (top, top)"
13.21
13.22 -instance
13.23 - by default (auto simp add: top_prod_def)
13.24 +instance ..
13.25
13.26 end
13.27
13.28 +instance prod :: (order_top, order_top) order_top
13.29 + by default (auto simp add: top_prod_def)
13.30 +
13.31 instance prod :: (wellorder, wellorder) wellorder
13.32 proof
13.33 fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"
14.1 --- a/src/HOL/Library/Product_Order.thy Wed Jul 24 17:15:59 2013 +0200
14.2 +++ b/src/HOL/Library/Product_Order.thy Thu Jul 25 08:57:16 2013 +0200
14.3 @@ -108,6 +108,10 @@
14.4 definition
14.5 "top = (top, top)"
14.6
14.7 +instance ..
14.8 +
14.9 +end
14.10 +
14.11 lemma fst_top [simp]: "fst top = top"
14.12 unfolding top_prod_def by simp
14.13
14.14 @@ -117,17 +121,19 @@
14.15 lemma Pair_top_top: "(top, top) = top"
14.16 unfolding top_prod_def by simp
14.17
14.18 -instance
14.19 +instance prod :: (order_top, order_top) order_top
14.20 by default (auto simp add: top_prod_def)
14.21
14.22 -end
14.23 -
14.24 instantiation prod :: (bot, bot) bot
14.25 begin
14.26
14.27 definition
14.28 "bot = (bot, bot)"
14.29
14.30 +instance ..
14.31 +
14.32 +end
14.33 +
14.34 lemma fst_bot [simp]: "fst bot = bot"
14.35 unfolding bot_prod_def by simp
14.36
14.37 @@ -137,11 +143,9 @@
14.38 lemma Pair_bot_bot: "(bot, bot) = bot"
14.39 unfolding bot_prod_def by simp
14.40
14.41 -instance
14.42 +instance prod :: (order_bot, order_bot) order_bot
14.43 by default (auto simp add: bot_prod_def)
14.44
14.45 -end
14.46 -
14.47 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
14.48
14.49 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
14.50 @@ -161,7 +165,7 @@
14.51
14.52 instance
14.53 by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
14.54 - INF_lower SUP_upper le_INF_iff SUP_le_iff)
14.55 + INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
14.56
14.57 end
14.58
15.1 --- a/src/HOL/Library/Saturated.thy Wed Jul 24 17:15:59 2013 +0200
15.2 +++ b/src/HOL/Library/Saturated.thy Thu Jul 25 08:57:16 2013 +0200
15.3 @@ -263,6 +263,12 @@
15.4 note finite
15.5 moreover assume z: "\<And>x. x \<in> A \<Longrightarrow> x \<le> z"
15.6 ultimately show "Sup A \<le> z" by (induct A) auto
15.7 +next
15.8 + show "Inf {} = (top::'a sat)"
15.9 + by (auto simp: top_sat_def)
15.10 +next
15.11 + show "Sup {} = (bot::'a sat)"
15.12 + by (auto simp: bot_sat_def)
15.13 qed
15.14
15.15 hide_const (open) sat_of_nat
16.1 --- a/src/HOL/Library/Sublist.thy Wed Jul 24 17:15:59 2013 +0200
16.2 +++ b/src/HOL/Library/Sublist.thy Thu Jul 25 08:57:16 2013 +0200
16.3 @@ -20,7 +20,7 @@
16.4 interpretation prefix_order: order prefixeq prefix
16.5 by default (auto simp: prefixeq_def prefix_def)
16.6
16.7 -interpretation prefix_bot: bot prefixeq prefix Nil
16.8 +interpretation prefix_bot: order_bot Nil prefixeq prefix
16.9 by default (simp add: prefixeq_def)
16.10
16.11 lemma prefixeqI [intro?]: "ys = xs @ zs \<Longrightarrow> prefixeq xs ys"
17.1 --- a/src/HOL/Nat.thy Wed Jul 24 17:15:59 2013 +0200
17.2 +++ b/src/HOL/Nat.thy Thu Jul 25 08:57:16 2013 +0200
17.3 @@ -444,7 +444,7 @@
17.4
17.5 end
17.6
17.7 -instantiation nat :: bot
17.8 +instantiation nat :: order_bot
17.9 begin
17.10
17.11 definition bot_nat :: nat where
17.12 @@ -1318,7 +1318,8 @@
17.13
17.14 subsection {* Kleene iteration *}
17.15
17.16 -lemma Kleene_iter_lpfp: assumes "mono f" and "f p \<le> p" shows "(f^^k) bot \<le> p"
17.17 +lemma Kleene_iter_lpfp:
17.18 +assumes "mono f" and "f p \<le> p" shows "(f^^k) (bot::'a::order_bot) \<le> p"
17.19 proof(induction k)
17.20 case 0 show ?case by simp
17.21 next
18.1 --- a/src/HOL/Orderings.thy Wed Jul 24 17:15:59 2013 +0200
18.2 +++ b/src/HOL/Orderings.thy Thu Jul 25 08:57:16 2013 +0200
18.3 @@ -1167,14 +1167,16 @@
18.4
18.5 subsection {* (Unique) top and bottom elements *}
18.6
18.7 -class bot = order +
18.8 +class bot =
18.9 fixes bot :: 'a ("\<bottom>")
18.10 +
18.11 +class order_bot = order + bot +
18.12 assumes bot_least: "\<bottom> \<le> a"
18.13
18.14 -sublocale bot < bot!: ordering_top greater_eq greater bot
18.15 +sublocale order_bot < bot!: ordering_top greater_eq greater bot
18.16 by default (fact bot_least)
18.17
18.18 -context bot
18.19 +context order_bot
18.20 begin
18.21
18.22 lemma le_bot:
18.23 @@ -1195,14 +1197,16 @@
18.24
18.25 end
18.26
18.27 -class top = order +
18.28 +class top =
18.29 fixes top :: 'a ("\<top>")
18.30 +
18.31 +class order_top = order + top +
18.32 assumes top_greatest: "a \<le> \<top>"
18.33
18.34 -sublocale top < top!: ordering_top less_eq less top
18.35 +sublocale order_top < top!: ordering_top less_eq less top
18.36 by default (fact top_greatest)
18.37
18.38 -context top
18.39 +context order_top
18.40 begin
18.41
18.42 lemma top_le:
18.43 @@ -1380,7 +1384,7 @@
18.44
18.45 subsection {* Order on @{typ bool} *}
18.46
18.47 -instantiation bool :: "{bot, top, linorder}"
18.48 +instantiation bool :: "{order_bot, order_top, linorder}"
18.49 begin
18.50
18.51 definition
18.52 @@ -1454,6 +1458,13 @@
18.53 definition
18.54 "\<bottom> = (\<lambda>x. \<bottom>)"
18.55
18.56 +instance ..
18.57 +
18.58 +end
18.59 +
18.60 +instantiation "fun" :: (type, order_bot) order_bot
18.61 +begin
18.62 +
18.63 lemma bot_apply [simp, code]:
18.64 "\<bottom> x = \<bottom>"
18.65 by (simp add: bot_fun_def)
18.66 @@ -1469,6 +1480,13 @@
18.67 definition
18.68 [no_atp]: "\<top> = (\<lambda>x. \<top>)"
18.69
18.70 +instance ..
18.71 +
18.72 +end
18.73 +
18.74 +instantiation "fun" :: (type, order_top) order_top
18.75 +begin
18.76 +
18.77 lemma top_apply [simp, code]:
18.78 "\<top> x = \<top>"
18.79 by (simp add: top_fun_def)
19.1 --- a/src/HOL/Set_Interval.thy Wed Jul 24 17:15:59 2013 +0200
19.2 +++ b/src/HOL/Set_Interval.thy Thu Jul 25 08:57:16 2013 +0200
19.3 @@ -197,8 +197,8 @@
19.4 by (simp add: atLeastAtMost_def)
19.5
19.6 text {* The above four lemmas could be declared as iffs. Unfortunately this
19.7 -breaks many proofs. Since it only helps blast, it is better to leave well
19.8 -alone *}
19.9 +breaks many proofs. Since it only helps blast, it is better to leave them
19.10 +alone. *}
19.11
19.12 lemma greaterThanLessThan_eq: "{ a <..< b} = { a <..} \<inter> {..< b }"
19.13 by auto
19.14 @@ -452,10 +452,10 @@
19.15 shows "{a ..< b} = {c ..< d} \<longleftrightarrow> a = c \<and> b = d"
19.16 using atLeastLessThan_inj assms by auto
19.17
19.18 -lemma (in bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
19.19 +lemma (in order_bot) atLeast_eq_UNIV_iff: "{x..} = UNIV \<longleftrightarrow> x = bot"
19.20 by (auto simp: set_eq_iff intro: le_bot)
19.21
19.22 -lemma (in top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
19.23 +lemma (in order_top) atMost_eq_UNIV_iff: "{..x} = UNIV \<longleftrightarrow> x = top"
19.24 by (auto simp: set_eq_iff intro: top_le)
19.25
19.26 lemma (in bounded_lattice) atLeastAtMost_eq_UNIV_iff:
20.1 --- a/src/HOL/Topological_Spaces.thy Wed Jul 24 17:15:59 2013 +0200
20.2 +++ b/src/HOL/Topological_Spaces.thy Thu Jul 25 08:57:16 2013 +0200
20.3 @@ -471,27 +471,28 @@
20.4 unfolding le_filter_def by simp }
20.5 { assume "F \<le> F'" and "F' \<le> F" thus "F = F'"
20.6 unfolding le_filter_def filter_eq_iff by fast }
20.7 - { show "F \<le> top"
20.8 - unfolding le_filter_def eventually_top by (simp add: always_eventually) }
20.9 - { show "bot \<le> F"
20.10 - unfolding le_filter_def by simp }
20.11 - { show "F \<le> sup F F'" and "F' \<le> sup F F'"
20.12 - unfolding le_filter_def eventually_sup by simp_all }
20.13 - { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
20.14 - unfolding le_filter_def eventually_sup by simp }
20.15 { show "inf F F' \<le> F" and "inf F F' \<le> F'"
20.16 unfolding le_filter_def eventually_inf by (auto intro: eventually_True) }
20.17 { assume "F \<le> F'" and "F \<le> F''" thus "F \<le> inf F' F''"
20.18 unfolding le_filter_def eventually_inf
20.19 by (auto elim!: eventually_mono intro: eventually_conj) }
20.20 + { show "F \<le> sup F F'" and "F' \<le> sup F F'"
20.21 + unfolding le_filter_def eventually_sup by simp_all }
20.22 + { assume "F \<le> F''" and "F' \<le> F''" thus "sup F F' \<le> F''"
20.23 + unfolding le_filter_def eventually_sup by simp }
20.24 + { assume "F'' \<in> S" thus "Inf S \<le> F''"
20.25 + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
20.26 + { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
20.27 + unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
20.28 { assume "F \<in> S" thus "F \<le> Sup S"
20.29 unfolding le_filter_def eventually_Sup by simp }
20.30 { assume "\<And>F. F \<in> S \<Longrightarrow> F \<le> F'" thus "Sup S \<le> F'"
20.31 unfolding le_filter_def eventually_Sup by simp }
20.32 - { assume "F'' \<in> S" thus "Inf S \<le> F''"
20.33 - unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
20.34 - { assume "\<And>F'. F' \<in> S \<Longrightarrow> F \<le> F'" thus "F \<le> Inf S"
20.35 - unfolding le_filter_def Inf_filter_def eventually_Sup Ball_def by simp }
20.36 + { show "Inf {} = (top::'a filter)"
20.37 + by (auto simp: top_filter_def Inf_filter_def Sup_filter_def)
20.38 + (metis (full_types) Topological_Spaces.top_filter_def always_eventually eventually_top) }
20.39 + { show "Sup {} = (bot::'a filter)"
20.40 + by (auto simp: bot_filter_def Sup_filter_def) }
20.41 qed
20.42
20.43 end
21.1 --- a/src/HOL/ex/FinFunPred.thy Wed Jul 24 17:15:59 2013 +0200
21.2 +++ b/src/HOL/ex/FinFunPred.thy Thu Jul 25 08:57:16 2013 +0200
21.3 @@ -31,7 +31,7 @@
21.4 instance "finfun" :: (type, order) order
21.5 by(intro_classes)(auto simp add: le_finfun_def order_antisym_conv intro: finfun_ext)
21.6
21.7 -instantiation "finfun" :: (type, bot) bot begin
21.8 +instantiation "finfun" :: (type, order_bot) order_bot begin
21.9 definition "bot = finfun_const bot"
21.10 instance by(intro_classes)(simp add: bot_finfun_def le_finfun_def)
21.11 end
21.12 @@ -39,7 +39,7 @@
21.13 lemma bot_finfun_apply [simp]: "op $ bot = (\<lambda>_. bot)"
21.14 by(auto simp add: bot_finfun_def)
21.15
21.16 -instantiation "finfun" :: (type, top) top begin
21.17 +instantiation "finfun" :: (type, order_top) order_top begin
21.18 definition "top = finfun_const top"
21.19 instance by(intro_classes)(simp add: top_finfun_def le_finfun_def)
21.20 end