# HG changeset patch
# User haftmann
# Date 1311312814 -7200
# Node ID 48065e997df03a62b9a1b74c2534cfd2b57d8aaf
# Parent  081718c0b0a86dc08e9248cd27055b7ab531f4ee# Parent  b1b436f7507055193e872ac39e755e493b9e34d5
merged

diff -r 081718c0b0a8 -r 48065e997df0 NEWS
--- a/NEWS	Thu Jul 21 21:29:10 2011 +0200
+++ b/NEWS	Fri Jul 22 07:33:34 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
diff -r 081718c0b0a8 -r 48065e997df0 src/HOL/Complete_Lattice.thy
--- a/src/HOL/Complete_Lattice.thy	Thu Jul 21 21:29:10 2011 +0200
+++ b/src/HOL/Complete_Lattice.thy	Fri Jul 22 07:33:34 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)
@@ -355,6 +356,24 @@
  "(\<Squnion>x\<in>A. B x) = \<bottom> \<longleftrightarrow> (\<forall>x\<in>A. B x = \<bottom>)"
   by (auto simp add: SUP_def Sup_bot_conv)
 
+lemma less_INF_D:
+  assumes "y < (\<Sqinter>i\<in>A. f i)" "i \<in> A" shows "y < f i"
+proof -
+  note `y < (\<Sqinter>i\<in>A. f i)`
+  also have "(\<Sqinter>i\<in>A. f i) \<le> f i" using `i \<in> A`
+    by (rule INF_leI)
+  finally show "y < f i" .
+qed
+
+lemma SUP_lessD:
+  assumes "(\<Squnion>i\<in>A. f i) < y" "i \<in> A" shows "f i < y"
+proof -
+  have "f i \<le> (\<Squnion>i\<in>A. f i)" using `i \<in> A`
+    by (rule le_SUP_I)
+  also note `(\<Squnion>i\<in>A. f i) < y`
+  finally show "f i < y" .
+qed
+
 lemma INF_UNIV_range:
   "(\<Sqinter>x. f x) = \<Sqinter>range f"
   by (fact INF_def)
@@ -371,41 +390,15 @@
   "(\<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
 
+lemma dual_complete_boolean_algebra:
+  "class.complete_boolean_algebra Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom> (\<lambda>x y. x \<squnion> - y) uminus"
+  by (rule class.complete_boolean_algebra.intro, rule dual_complete_lattice, rule dual_boolean_algebra)
+
 lemma uminus_Inf:
   "- (\<Sqinter>A) = \<Squnion>(uminus ` A)"
 proof (rule antisym)
@@ -430,6 +423,61 @@
 
 end
 
+class complete_linorder = linorder + complete_lattice
+begin
+
+lemma dual_complete_linorder:
+  "class.complete_linorder Sup Inf (op \<ge>) (op >) sup inf \<top> \<bottom>"
+  by (rule class.complete_linorder.intro, rule dual_complete_lattice, rule dual_linorder)
+
+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
+
+lemma Sup_eq_top_iff:
+  "\<Squnion>A = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < i)"
+proof
+  assume *: "\<Squnion>A = \<top>"
+  show "(\<forall>x<\<top>. \<exists>i\<in>A. x < i)" unfolding * [symmetric]
+  proof (intro allI impI)
+    fix x assume "x < \<Squnion>A" then show "\<exists>i\<in>A. x < i"
+      unfolding less_Sup_iff by auto
+  qed
+next
+  assume *: "\<forall>x<\<top>. \<exists>i\<in>A. x < i"
+  show "\<Squnion>A = \<top>"
+  proof (rule ccontr)
+    assume "\<Squnion>A \<noteq> \<top>"
+    with top_greatest [of "\<Squnion>A"]
+    have "\<Squnion>A < \<top>" unfolding le_less by auto
+    then have "\<Squnion>A < \<Squnion>A"
+      using * unfolding less_Sup_iff by auto
+    then show False by auto
+  qed
+qed
+
+lemma Inf_eq_bot_iff:
+  "\<Sqinter>A = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. i < x)"
+proof -
+  interpret dual: complete_linorder Sup Inf "op \<ge>" "op >" sup inf \<top> \<bottom>
+    by (fact dual_complete_linorder)
+  from dual.Sup_eq_top_iff show ?thesis .
+qed
+
+end
+
 
 subsection {* @{typ bool} and @{typ "_ \<Rightarrow> _"} as complete lattice *}
 
@@ -688,7 +736,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
@@ -893,7 +941,7 @@
 lemma UN_eq: "(\<Union>x\<in>A. B x) = \<Union>({Y. \<exists>x\<in>A. Y = B x})"
   by (fact SUP_eq)
 
-lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)" -- "FIXME generalize"
+lemma image_Union: "f ` \<Union>S = (\<Union>x\<in>S. f ` x)"
   by blast
 
 lemma UNION_empty_conv[simp]:
@@ -922,7 +970,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
@@ -1047,6 +1095,17 @@
   "\<And>A P. (\<not>(\<exists>x\<in>A. P x)) \<longleftrightarrow> (\<forall>x\<in>A. \<not> P x)"
   by auto
 
+lemma (in complete_linorder) INF_eq_bot_iff:
+  fixes f :: "'b \<Rightarrow> 'a"
+  shows "(\<Sqinter>i\<in>A. f i) = \<bottom> \<longleftrightarrow> (\<forall>x>\<bottom>. \<exists>i\<in>A. f i < x)"
+  unfolding INF_def Inf_eq_bot_iff by auto
+
+lemma (in complete_linorder) SUP_eq_top_iff:
+  fixes f :: "'b \<Rightarrow> 'a"
+  shows "(\<Squnion>i\<in>A. f i) = \<top> \<longleftrightarrow> (\<forall>x<\<top>. \<exists>i\<in>A. x < f i)"
+  unfolding SUP_def Sup_eq_top_iff by auto
+
+
 text {* \medskip Maxiscoping: pulling out big Unions and Intersections. *}
 
 lemma UN_extend_simps:
@@ -1083,7 +1142,12 @@
 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 
+lemmas (in complete_lattice) less_INFD = less_INF_D
+
+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
 
diff -r 081718c0b0a8 -r 48065e997df0 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 21 21:29:10 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Fri Jul 22 07:33:34 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,34 +1338,6 @@
     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)"
-proof
-  assume *: "Sup A = top"
-  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
-  qed
-next
-  assume *: "\<forall>x<top. \<exists>i\<in>A. x < i"
-  show "Sup A = top"
-  proof (rule ccontr)
-    assume "Sup A \<noteq> top"
-    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
-    then show False by auto
-  qed
-qed
-
-lemma SUP_eq_top_iff:
-  fixes f :: "'a \<Rightarrow> 'b::{complete_lattice, linorder}"
-  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
-
 lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
 proof -
   { fix x ::ereal assume "x \<noteq> \<infinity>"
@@ -2182,12 +2157,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 +2183,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 +2197,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 +2210,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 +2231,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"
@@ -2373,14 +2347,6 @@
 
 abbreviation "limsup \<equiv> Limsup sequentially"
 
-lemma (in complete_lattice) less_INFD:
-  assumes "y < INFI A f"" i \<in> A" shows "y < f i"
-proof -
-  note `y < INFI A f`
-  also have "INFI A f \<le> f i" using `i \<in> A` by (rule INF_leI)
-  finally show "y < f i" .
-qed
-
 lemma liminf_SUPR_INFI:
   fixes f :: "nat \<Rightarrow> ereal"
   shows "liminf f = (SUP n. INF m:{n..}. f m)"
diff -r 081718c0b0a8 -r 48065e997df0 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Thu Jul 21 21:29:10 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Fri Jul 22 07:33:34 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"