1.1 --- a/NEWS Thu Jul 21 21:29:10 2011 +0200
1.2 +++ b/NEWS Fri Jul 22 07:33:34 2011 +0200
1.3 @@ -63,15 +63,16 @@
1.4 * Classes bot and top require underlying partial order rather than preorder:
1.5 uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
1.6
1.7 -* Class 'complete_lattice': generalized a couple of lemmas from sets;
1.8 -generalized theorems INF_cong and SUP_cong. More consistent and less
1.9 -misunderstandable names:
1.10 +* Class complete_lattice: generalized a couple of lemmas from sets;
1.11 +generalized theorems INF_cong and SUP_cong. New type classes for complete
1.12 +boolean algebras and complete linear orderes. Lemmas Inf_less_iff,
1.13 +less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
1.14 +More consistent and less misunderstandable names:
1.15 INFI_def ~> INF_def
1.16 SUPR_def ~> SUP_def
1.17 le_SUPI ~> le_SUP_I
1.18 le_SUPI2 ~> le_SUP_I2
1.19 le_INFI ~> le_INF_I
1.20 - INF_subset ~> INF_superset_mono
1.21 INFI_bool_eq ~> INF_bool_eq
1.22 SUPR_bool_eq ~> SUP_bool_eq
1.23 INFI_apply ~> INF_apply
2.1 --- a/src/HOL/Complete_Lattice.thy Thu Jul 21 21:29:10 2011 +0200
2.2 +++ b/src/HOL/Complete_Lattice.thy Fri Jul 22 07:33:34 2011 +0200
2.3 @@ -292,12 +292,13 @@
2.4 by (force intro!: Sup_mono simp: SUP_def)
2.5
2.6 lemma INF_superset_mono:
2.7 - "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
2.8 - by (rule INF_mono) auto
2.9 + "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
2.10 + -- {* The last inclusion is POSITIVE! *}
2.11 + by (blast intro: INF_mono dest: subsetD)
2.12
2.13 lemma SUP_subset_mono:
2.14 - "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
2.15 - by (rule SUP_mono) auto
2.16 + "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
2.17 + by (blast intro: SUP_mono dest: subsetD)
2.18
2.19 lemma INF_commute: "(\<Sqinter>i\<in>A. \<Sqinter>j\<in>B. f i j) = (\<Sqinter>j\<in>B. \<Sqinter>i\<in>A. f i j)"
2.20 by (iprover intro: INF_leI le_INF_I order_trans antisym)
2.21 @@ -355,6 +356,24 @@
2.22 "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
2.23 by (auto simp add: SUP_def Sup_bot_conv)
2.24
2.25 +lemma less_INF_D:
2.26 + assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
2.27 +proof -
2.28 + note `y < (\<Sqinter>i\<in>A. f i)`
2.29 + also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
2.30 + by (rule INF_leI)
2.31 + finally show "y < f i" .
2.32 +qed
2.33 +
2.34 +lemma SUP_lessD:
2.35 + assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
2.36 +proof -
2.37 + have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
2.38 + by (rule le_SUP_I)
2.39 + also note `(\<Squnion>i\<in>A. f i) < y`
2.40 + finally show "f i < y" .
2.41 +qed
2.42 +
2.43 lemma INF_UNIV_range:
2.44 "(\<Sqinter>x. f x) = \<Sqinter>range f"
2.45 by (fact INF_def)
2.46 @@ -371,41 +390,15 @@
2.47 "(\<Squnion>b. A b) = A True \<squnion> A False"
2.48 by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
2.49
2.50 -lemma INF_mono':
2.51 - "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<sqsubseteq> (\<Sqinter>x\<in>B. g x)"
2.52 - -- {* The last inclusion is POSITIVE! *}
2.53 - by (rule INF_mono) auto
2.54 -
2.55 -lemma SUP_mono':
2.56 - "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<sqsubseteq> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<sqsubseteq> (\<Squnion>x\<in>B. g x)"
2.57 - -- {* The last inclusion is POSITIVE! *}
2.58 - by (blast intro: SUP_mono dest: subsetD)
2.59 -
2.60 end
2.61
2.62 -lemma Inf_less_iff:
2.63 - fixes a :: "'a\<Colon>{complete_lattice,linorder}"
2.64 - shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
2.65 - unfolding not_le [symmetric] le_Inf_iff by auto
2.66 -
2.67 -lemma less_Sup_iff:
2.68 - fixes a :: "'a\<Colon>{complete_lattice,linorder}"
2.69 - shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
2.70 - unfolding not_le [symmetric] Sup_le_iff by auto
2.71 -
2.72 -lemma INF_less_iff:
2.73 - fixes a :: "'a::{complete_lattice,linorder}"
2.74 - shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
2.75 - unfolding INF_def Inf_less_iff by auto
2.76 -
2.77 -lemma less_SUP_iff:
2.78 - fixes a :: "'a::{complete_lattice,linorder}"
2.79 - shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
2.80 - unfolding SUP_def less_Sup_iff by auto
2.81 -
2.82 class complete_boolean_algebra = boolean_algebra + complete_lattice
2.83 begin
2.84
2.85 +lemma dual_complete_boolean_algebra:
2.86 + "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
2.87 + by (rule class.complete_boolean_algebra.intro, rule dual_complete_lattice, rule dual_boolean_algebra)
2.88 +
2.89 lemma uminus_Inf:
2.90 "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
2.91 proof (rule antisym)
2.92 @@ -430,6 +423,61 @@
2.93
2.94 end
2.95
2.96 +class complete_linorder = linorder + complete_lattice
2.97 +begin
2.98 +
2.99 +lemma dual_complete_linorder:
2.100 + "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
2.101 + by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
2.102 +
2.103 +lemma Inf_less_iff:
2.104 + "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
2.105 + unfolding not_le [symmetric] le_Inf_iff by auto
2.106 +
2.107 +lemma less_Sup_iff:
2.108 + "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
2.109 + unfolding not_le [symmetric] Sup_le_iff by auto
2.110 +
2.111 +lemma INF_less_iff:
2.112 + "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
2.113 + unfolding INF_def Inf_less_iff by auto
2.114 +
2.115 +lemma less_SUP_iff:
2.116 + "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
2.117 + unfolding SUP_def less_Sup_iff by auto
2.118 +
2.119 +lemma Sup_eq_top_iff:
2.120 + "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
2.121 +proof
2.122 + assume *: "\<Squnion>A = \<top>"
2.123 + show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
2.124 + proof (intro allI impI)
2.125 + fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
2.126 + unfolding less_Sup_iff by auto
2.127 + qed
2.128 +next
2.129 + assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
2.130 + show "\<Squnion>A = \<top>"
2.131 + proof (rule ccontr)
2.132 + assume "\<Squnion>A \<noteq> \<top>"
2.133 + with top_greatest [of "\<Squnion>A"]
2.134 + have "\<Squnion>A < \<top>" unfolding le_less by auto
2.135 + then have "\<Squnion>A < \<Squnion>A"
2.136 + using * unfolding less_Sup_iff by auto
2.137 + then show False by auto
2.138 + qed
2.139 +qed
2.140 +
2.141 +lemma Inf_eq_bot_iff:
2.142 + "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
2.143 +proof -
2.144 + interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
2.145 + by (fact dual_complete_linorder)
2.146 + from dual.Sup_eq_top_iff show ?thesis .
2.147 +qed
2.148 +
2.149 +end
2.150 +
2.151
2.152 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
2.153
2.154 @@ -688,7 +736,7 @@
2.155 lemma INT_anti_mono:
2.156 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow> (\<Inter>x\<in>B. f x) \<subseteq> (\<Inter>x\<in>A. g x)"
2.157 -- {* The last inclusion is POSITIVE! *}
2.158 - by (fact INF_mono')
2.159 + by (fact INF_superset_mono)
2.160
2.161 lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
2.162 by blast
2.163 @@ -893,7 +941,7 @@
2.164 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
2.165 by (fact SUP_eq)
2.166
2.167 -lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize"
2.168 +lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
2.169 by blast
2.170
2.171 lemma UNION_empty_conv[simp]:
2.172 @@ -922,7 +970,7 @@
2.173 lemma UN_mono:
2.174 "A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
2.175 (\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
2.176 - by (fact SUP_mono')
2.177 + by (fact SUP_subset_mono)
2.178
2.179 lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
2.180 by blast
2.181 @@ -1047,6 +1095,17 @@
2.182 "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
2.183 by auto
2.184
2.185 +lemma (in complete_linorder) INF_eq_bot_iff:
2.186 + fixes f :: "'b \<Rightarrow> 'a"
2.187 + shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
2.188 + unfolding INF_def Inf_eq_bot_iff by auto
2.189 +
2.190 +lemma (in complete_linorder) SUP_eq_top_iff:
2.191 + fixes f :: "'b \<Rightarrow> 'a"
2.192 + shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
2.193 + unfolding SUP_def Sup_eq_top_iff by auto
2.194 +
2.195 +
2.196 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
2.197
2.198 lemma UN_extend_simps:
2.199 @@ -1083,7 +1142,12 @@
2.200 lemmas (in complete_lattice) le_SUPI = le_SUP_I
2.201 lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
2.202 lemmas (in complete_lattice) le_INFI = le_INF_I
2.203 -lemmas (in complete_lattice) INF_subset = INF_superset_mono
2.204 +lemmas (in complete_lattice) less_INFD = less_INF_D
2.205 +
2.206 +lemma (in complete_lattice) INF_subset:
2.207 + "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
2.208 + by (rule INF_superset_mono) auto
2.209 +
2.210 lemmas INFI_apply = INF_apply
2.211 lemmas SUPR_apply = SUP_apply
2.212
3.1 --- a/src/HOL/Library/Extended_Real.thy Thu Jul 21 21:29:10 2011 +0200
3.2 +++ b/src/HOL/Library/Extended_Real.thy Fri Jul 22 07:33:34 2011 +0200
3.3 @@ -8,7 +8,7 @@
3.4 header {* Extended real number line *}
3.5
3.6 theory Extended_Real
3.7 - imports Complex_Main Extended_Nat
3.8 +imports Complex_Main Extended_Nat
3.9 begin
3.10
3.11 text {*
3.12 @@ -1244,8 +1244,11 @@
3.13 with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
3.14 unfolding ereal_Sup_uminus_image_eq by force }
3.15 qed
3.16 +
3.17 end
3.18
3.19 +instance ereal :: complete_linorder ..
3.20 +
3.21 lemma ereal_SUPR_uminus:
3.22 fixes f :: "'a => ereal"
3.23 shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
3.24 @@ -1335,34 +1338,6 @@
3.25 by (cases e) auto
3.26 qed
3.27
3.28 -lemma Sup_eq_top_iff:
3.29 - fixes A :: "'a::{complete_lattice, linorder} set"
3.30 - shows "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
3.31 -proof
3.32 - assume *: "Sup A = top"
3.33 - show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding *[symmetric]
3.34 - proof (intro allI impI)
3.35 - fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
3.36 - unfolding less_Sup_iff by auto
3.37 - qed
3.38 -next
3.39 - assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
3.40 - show "Sup A = top"
3.41 - proof (rule ccontr)
3.42 - assume "Sup A \<noteq> top"
3.43 - with top_greatest[of "Sup A"]
3.44 - have "Sup A < top" unfolding le_less by auto
3.45 - then have "Sup A < Sup A"
3.46 - using * unfolding less_Sup_iff by auto
3.47 - then show False by auto
3.48 - qed
3.49 -qed
3.50 -
3.51 -lemma SUP_eq_top_iff:
3.52 - fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}"
3.53 - shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
3.54 - unfolding SUPR_def Sup_eq_top_iff by auto
3.55 -
3.56 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
3.57 proof -
3.58 { fix x ::ereal assume "x \<noteq> \<infinity>"
3.59 @@ -2182,12 +2157,12 @@
3.60 "Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
3.61
3.62 lemma Liminf_Sup:
3.63 - fixes f :: "'a => 'b::{complete_lattice, linorder}"
3.64 + fixes f :: "'a => 'b::complete_linorder"
3.65 shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
3.66 by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
3.67
3.68 lemma Limsup_Inf:
3.69 - fixes f :: "'a => 'b::{complete_lattice, linorder}"
3.70 + fixes f :: "'a => 'b::complete_linorder"
3.71 shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
3.72 by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
3.73
3.74 @@ -2208,7 +2183,7 @@
3.75 using assms by (auto intro!: Greatest_equality)
3.76
3.77 lemma Limsup_const:
3.78 - fixes c :: "'a::{complete_lattice, linorder}"
3.79 + fixes c :: "'a::complete_linorder"
3.80 assumes ntriv: "\<not> trivial_limit net"
3.81 shows "Limsup net (\<lambda>x. c) = c"
3.82 unfolding Limsup_Inf
3.83 @@ -2222,7 +2197,7 @@
3.84 qed auto
3.85
3.86 lemma Liminf_const:
3.87 - fixes c :: "'a::{complete_lattice, linorder}"
3.88 + fixes c :: "'a::complete_linorder"
3.89 assumes ntriv: "\<not> trivial_limit net"
3.90 shows "Liminf net (\<lambda>x. c) = c"
3.91 unfolding Liminf_Sup
3.92 @@ -2235,18 +2210,17 @@
3.93 qed
3.94 qed auto
3.95
3.96 -lemma mono_set:
3.97 - fixes S :: "('a::order) set"
3.98 - shows "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
3.99 +lemma (in order) mono_set:
3.100 + "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
3.101 by (auto simp: mono_def mem_def)
3.102
3.103 -lemma mono_greaterThan[intro, simp]: "mono {B<..}" unfolding mono_set by auto
3.104 -lemma mono_atLeast[intro, simp]: "mono {B..}" unfolding mono_set by auto
3.105 -lemma mono_UNIV[intro, simp]: "mono UNIV" unfolding mono_set by auto
3.106 -lemma mono_empty[intro, simp]: "mono {}" unfolding mono_set by auto
3.107 +lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto
3.108 +lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto
3.109 +lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto
3.110 +lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto
3.111
3.112 -lemma mono_set_iff:
3.113 - fixes S :: "'a::{linorder,complete_lattice} set"
3.114 +lemma (in complete_linorder) mono_set_iff:
3.115 + fixes S :: "'a set"
3.116 defines "a \<equiv> Inf S"
3.117 shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
3.118 proof
3.119 @@ -2257,13 +2231,13 @@
3.120 assume "a \<in> S"
3.121 show ?c
3.122 using mono[OF _ `a \<in> S`]
3.123 - by (auto intro: complete_lattice_class.Inf_lower simp: a_def)
3.124 + by (auto intro: Inf_lower simp: a_def)
3.125 next
3.126 assume "a \<notin> S"
3.127 have "S = {a <..}"
3.128 proof safe
3.129 fix x assume "x \<in> S"
3.130 - then have "a \<le> x" unfolding a_def by (rule complete_lattice_class.Inf_lower)
3.131 + then have "a \<le> x" unfolding a_def by (rule Inf_lower)
3.132 then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
3.133 next
3.134 fix x assume "a < x"
3.135 @@ -2373,14 +2347,6 @@
3.136
3.137 abbreviation "limsup \<equiv> Limsup sequentially"
3.138
3.139 -lemma (in complete_lattice) less_INFD:
3.140 - assumes "y < INFI A f"" i \<in> A" shows "y < f i"
3.141 -proof -
3.142 - note `y < INFI A f`
3.143 - also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
3.144 - finally show "y < f i" .
3.145 -qed
3.146 -
3.147 lemma liminf_SUPR_INFI:
3.148 fixes f :: "nat \<Rightarrow> ereal"
3.149 shows "liminf f = (SUP n. INF m:{n..}. f m)"
4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Jul 21 21:29:10 2011 +0200
4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy Fri Jul 22 07:33:34 2011 +0200
4.3 @@ -6,7 +6,7 @@
4.4 header {*Lebesgue Integration*}
4.5
4.6 theory Lebesgue_Integration
4.7 -imports Measure Borel_Space
4.8 + imports Measure Borel_Space
4.9 begin
4.10
4.11 lemma real_ereal_1[simp]: "real (1::ereal) = 1"