--- a/NEWS Thu Jul 21 08:33:57 2011 +0200
+++ b/NEWS Thu Jul 21 21:56:24 2011 +0200
@@ -63,15 +63,16 @@
* Classes bot and top require underlying partial order rather than preorder:
uniqueness of bot and top is guaranteed. INCOMPATIBILITY.
-* Class 'complete_lattice': generalized a couple of lemmas from sets;
-generalized theorems INF_cong and SUP_cong. More consistent and less
-misunderstandable names:
+* Class complete_lattice: generalized a couple of lemmas from sets;
+generalized theorems INF_cong and SUP_cong. New type classes for complete
+boolean algebras and complete linear orderes. Lemmas Inf_less_iff,
+less_Sup_iff, INF_less_iff, less_SUP_iff now reside in class complete_linorder.
+More consistent and less misunderstandable names:
INFI_def ~> INF_def
SUPR_def ~> SUP_def
le_SUPI ~> le_SUP_I
le_SUPI2 ~> le_SUP_I2
le_INFI ~> le_INF_I
- INF_subset ~> INF_superset_mono
INFI_bool_eq ~> INF_bool_eq
SUPR_bool_eq ~> SUP_bool_eq
INFI_apply ~> INF_apply
--- a/src/HOL/Complete_Lattice.thy Thu Jul 21 08:33:57 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy Thu Jul 21 21:56:24 2011 +0200
@@ -292,12 +292,13 @@
by (force intro!: Sup_mono simp: SUP_def)
lemma INF_superset_mono:
- "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
- by (rule INF_mono) auto
+ "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)"
+ -- {* The last inclusion is POSITIVE! *}
+ by (blast intro: INF_mono dest: subsetD)
lemma SUP_subset_mono:
- "A \<subseteq> B \<Longrightarrow> SUPR A f \<sqsubseteq> SUPR B f"
- by (rule SUP_mono) auto
+ "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)"
+ by (blast intro: SUP_mono dest: subsetD)
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)"
by (iprover intro: INF_leI le_INF_I order_trans antisym)
@@ -371,38 +372,8 @@
"(\<Squnion>b. A b) = A True \<squnion> A False"
by (simp add: UNIV_bool SUP_empty SUP_insert sup_commute)
-lemma INF_mono':
- "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)"
- -- {* The last inclusion is POSITIVE! *}
- by (rule INF_mono) auto
-
-lemma SUP_mono':
- "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)"
- -- {* The last inclusion is POSITIVE! *}
- by (blast intro: SUP_mono dest: subsetD)
-
end
-lemma Inf_less_iff:
- fixes a :: "'a\<Colon>{complete_lattice,linorder}"
- shows "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
- unfolding not_le [symmetric] le_Inf_iff by auto
-
-lemma less_Sup_iff:
- fixes a :: "'a\<Colon>{complete_lattice,linorder}"
- shows "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
- unfolding not_le [symmetric] Sup_le_iff by auto
-
-lemma INF_less_iff:
- fixes a :: "'a::{complete_lattice,linorder}"
- shows "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
- unfolding INF_def Inf_less_iff by auto
-
-lemma less_SUP_iff:
- fixes a :: "'a::{complete_lattice,linorder}"
- shows "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
- unfolding SUP_def less_Sup_iff by auto
-
class complete_boolean_algebra = boolean_algebra + complete_lattice
begin
@@ -430,6 +401,27 @@
end
+class complete_linorder = linorder + complete_lattice
+begin
+
+lemma Inf_less_iff:
+ "\<Sqinter>S \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>S. x \<sqsubset> a)"
+ unfolding not_le [symmetric] le_Inf_iff by auto
+
+lemma less_Sup_iff:
+ "a \<sqsubset> \<Squnion>S \<longleftrightarrow> (\<exists>x\<in>S. a \<sqsubset> x)"
+ unfolding not_le [symmetric] Sup_le_iff by auto
+
+lemma INF_less_iff:
+ "(\<Sqinter>i\<in>A. f i) \<sqsubset> a \<longleftrightarrow> (\<exists>x\<in>A. f x \<sqsubset> a)"
+ unfolding INF_def Inf_less_iff by auto
+
+lemma less_SUP_iff:
+ "a \<sqsubset> (\<Squnion>i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a \<sqsubset> f x)"
+ unfolding SUP_def less_Sup_iff by auto
+
+end
+
subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
@@ -688,7 +680,7 @@
lemma INT_anti_mono:
"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)"
-- {* The last inclusion is POSITIVE! *}
- by (fact INF_mono')
+ by (fact INF_superset_mono)
lemma Pow_INT_eq: "Pow (\<Inter>x\<in>A. B x) = (\<Inter>x\<in>A. Pow (B x))"
by blast
@@ -922,7 +914,7 @@
lemma UN_mono:
"A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<subseteq> g x) \<Longrightarrow>
(\<Union>x\<in>A. f x) \<subseteq> (\<Union>x\<in>B. g x)"
- by (fact SUP_mono')
+ by (fact SUP_subset_mono)
lemma vimage_Union: "f -` (\<Union>A) = (\<Union>X\<in>A. f -` X)"
by blast
@@ -1083,7 +1075,11 @@
lemmas (in complete_lattice) le_SUPI = le_SUP_I
lemmas (in complete_lattice) le_SUPI2 = le_SUP_I2
lemmas (in complete_lattice) le_INFI = le_INF_I
-lemmas (in complete_lattice) INF_subset = INF_superset_mono
+
+lemma (in complete_lattice) INF_subset:
+ "B \<subseteq> A \<Longrightarrow> INFI A f \<sqsubseteq> INFI B f"
+ by (rule INF_superset_mono) auto
+
lemmas INFI_apply = INF_apply
lemmas SUPR_apply = SUP_apply
--- a/src/HOL/Library/Extended_Real.thy Thu Jul 21 08:33:57 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Thu Jul 21 21:56:24 2011 +0200
@@ -8,7 +8,7 @@
header {* Extended real number line *}
theory Extended_Real
- imports Complex_Main Extended_Nat
+imports Complex_Main Extended_Nat
begin
text {*
@@ -1244,8 +1244,11 @@
with Sup_le[of "uminus`A" "-x"] show "x \<le> Inf A"
unfolding ereal_Sup_uminus_image_eq by force }
qed
+
end
+instance ereal :: complete_linorder ..
+
lemma ereal_SUPR_uminus:
fixes f :: "'a => ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
@@ -1335,12 +1338,11 @@
by (cases e) auto
qed
-lemma Sup_eq_top_iff:
- fixes A :: "'a::{complete_lattice, linorder} set"
- shows "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
+lemma (in complete_linorder) Sup_eq_top_iff: -- "FIXME move"
+ "Sup A = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < i)"
proof
assume *: "Sup A = top"
- show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding *[symmetric]
+ show "(\<forall>x<top. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
proof (intro allI impI)
fix x assume "x < Sup A" then show "\<exists>i\<in>A. x < i"
unfolding less_Sup_iff by auto
@@ -1350,7 +1352,7 @@
show "Sup A = top"
proof (rule ccontr)
assume "Sup A \<noteq> top"
- with top_greatest[of "Sup A"]
+ with top_greatest [of "Sup A"]
have "Sup A < top" unfolding le_less by auto
then have "Sup A < Sup A"
using * unfolding less_Sup_iff by auto
@@ -1358,8 +1360,8 @@
qed
qed
-lemma SUP_eq_top_iff:
- fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}"
+lemma (in complete_linorder) SUP_eq_top_iff: -- "FIXME move"
+ fixes f :: "'b \<Rightarrow> 'a"
shows "(SUP i:A. f i) = top \<longleftrightarrow> (\<forall>x<top. \<exists>i\<in>A. x < f i)"
unfolding SUPR_def Sup_eq_top_iff by auto
@@ -2182,12 +2184,12 @@
"Limsup net f = (LEAST l. \<forall>y>l. eventually (\<lambda>x. f x < y) net)"
lemma Liminf_Sup:
- fixes f :: "'a => 'b::{complete_lattice, linorder}"
+ fixes f :: "'a => 'b::complete_linorder"
shows "Liminf net f = Sup {l. \<forall>y<l. eventually (\<lambda>x. y < f x) net}"
by (auto intro!: Greatest_equality complete_lattice_class.Sup_upper simp: less_Sup_iff Liminf_def)
lemma Limsup_Inf:
- fixes f :: "'a => 'b::{complete_lattice, linorder}"
+ fixes f :: "'a => 'b::complete_linorder"
shows "Limsup net f = Inf {l. \<forall>y>l. eventually (\<lambda>x. f x < y) net}"
by (auto intro!: Least_equality complete_lattice_class.Inf_lower simp: Inf_less_iff Limsup_def)
@@ -2208,7 +2210,7 @@
using assms by (auto intro!: Greatest_equality)
lemma Limsup_const:
- fixes c :: "'a::{complete_lattice, linorder}"
+ fixes c :: "'a::complete_linorder"
assumes ntriv: "\<not> trivial_limit net"
shows "Limsup net (\<lambda>x. c) = c"
unfolding Limsup_Inf
@@ -2222,7 +2224,7 @@
qed auto
lemma Liminf_const:
- fixes c :: "'a::{complete_lattice, linorder}"
+ fixes c :: "'a::complete_linorder"
assumes ntriv: "\<not> trivial_limit net"
shows "Liminf net (\<lambda>x. c) = c"
unfolding Liminf_Sup
@@ -2235,18 +2237,17 @@
qed
qed auto
-lemma mono_set:
- fixes S :: "('a::order) set"
- shows "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
+lemma (in order) mono_set:
+ "mono S \<longleftrightarrow> (\<forall>x y. x \<le> y \<longrightarrow> x \<in> S \<longrightarrow> y \<in> S)"
by (auto simp: mono_def mem_def)
-lemma mono_greaterThan[intro, simp]: "mono {B<..}" unfolding mono_set by auto
-lemma mono_atLeast[intro, simp]: "mono {B..}" unfolding mono_set by auto
-lemma mono_UNIV[intro, simp]: "mono UNIV" unfolding mono_set by auto
-lemma mono_empty[intro, simp]: "mono {}" unfolding mono_set by auto
+lemma (in order) mono_greaterThan [intro, simp]: "mono {B<..}" unfolding mono_set by auto
+lemma (in order) mono_atLeast [intro, simp]: "mono {B..}" unfolding mono_set by auto
+lemma (in order) mono_UNIV [intro, simp]: "mono UNIV" unfolding mono_set by auto
+lemma (in order) mono_empty [intro, simp]: "mono {}" unfolding mono_set by auto
-lemma mono_set_iff:
- fixes S :: "'a::{linorder,complete_lattice} set"
+lemma (in complete_linorder) mono_set_iff:
+ fixes S :: "'a set"
defines "a \<equiv> Inf S"
shows "mono S \<longleftrightarrow> (S = {a <..} \<or> S = {a..})" (is "_ = ?c")
proof
@@ -2257,13 +2258,13 @@
assume "a \<in> S"
show ?c
using mono[OF _ `a \<in> S`]
- by (auto intro: complete_lattice_class.Inf_lower simp: a_def)
+ by (auto intro: Inf_lower simp: a_def)
next
assume "a \<notin> S"
have "S = {a <..}"
proof safe
fix x assume "x \<in> S"
- then have "a \<le> x" unfolding a_def by (rule complete_lattice_class.Inf_lower)
+ then have "a \<le> x" unfolding a_def by (rule Inf_lower)
then show "a < x" using `x \<in> S` `a \<notin> S` by (cases "a = x") auto
next
fix x assume "a < x"
--- a/src/HOL/Probability/Lebesgue_Integration.thy Thu Jul 21 08:33:57 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Thu Jul 21 21:56:24 2011 +0200
@@ -6,7 +6,7 @@
header {*Lebesgue Integration*}
theory Lebesgue_Integration
-imports Measure Borel_Space
+ imports Measure Borel_Space
begin
lemma real_ereal_1[simp]: "real (1::ereal) = 1"