Measures form a CCPO

--- a/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:39:10 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy	Thu Jul 23 16:40:47 2015 +0200
@@ -3182,6 +3182,77 @@
 qed
 
 
+lemma SUP_ereal_add_directed:
+  fixes f g :: "'a \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
+  assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
+  shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+proof cases
+  assume "I = {}" then show ?thesis
+    by (simp add: bot_ereal_def)
+next
+  assume "I \<noteq> {}"
+  show ?thesis
+  proof (rule antisym)
+    show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+      by (rule SUP_least; intro ereal_add_mono SUP_upper)
+  next
+    have "bot < (SUP i:I. g i)"
+      using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
+    then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+      by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
+    also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+      using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
+    also have "\<dots> \<le> (SUP i:I. f i + g i)"
+      using directed by (intro SUP_least) (blast intro: SUP_upper2)
+    finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+  qed
+qed
+
+lemma SUP_ereal_setsum_directed:
+  fixes f g :: "'a \<Rightarrow> 'b \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
+  assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
+  shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
+proof -
+  have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
+  proof (induction N rule: infinite_finite_induct)
+    case (insert n N)
+    moreover have "(SUP i:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
+    proof (rule SUP_ereal_add_directed)
+      fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
+        using insert by (auto intro!: setsum_nonneg nonneg)
+    next
+      fix i j assume "i \<in> I" "j \<in> I"
+      from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
+      then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)" 
+        by (intro bexI[of _ k]) (auto intro!: ereal_add_mono setsum_mono)
+    qed
+    ultimately show ?case
+      by simp
+  qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)
+  from this[of A] show ?thesis by simp
+qed
+
+lemma suminf_SUP_eq_directed:
+  fixes f :: "_ \<Rightarrow> nat \<Rightarrow> ereal"
+  assumes "I \<noteq> {}"
+  assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
+  assumes nonneg: "\<And>n i. 0 \<le> f n i"
+  shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
+proof (subst (1 2) suminf_ereal_eq_SUP)
+  show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
+    using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
+  show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
+    apply (subst SUP_commute)
+    apply (subst SUP_ereal_setsum_directed)
+    apply (auto intro!: assms simp: finite_subset)
+    done
+qed
+
+subsection \<open>More Limits\<close>
+
 lemma convergent_limsup_cl:
   fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
   shows "convergent X \<Longrightarrow> limsup X = lim X"

--- a/src/HOL/Probability/Measure_Space.thy	Thu Jul 23 16:39:10 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Thu Jul 23 16:40:47 2015 +0200
@@ -2053,5 +2053,174 @@
 lemma measure_null_measure[simp]: "measure (null_measure M) X = 0"
   by (simp add: measure_def)
 
+subsection \<open>Measures form a chain-complete partial order\<close>
+
+instantiation measure :: (type) order_bot
+begin
+
+definition bot_measure :: "'a measure" where
+  "bot_measure = sigma {} {{}}"
+
+lemma space_bot[simp]: "space bot = {}"
+  unfolding bot_measure_def by (rule space_measure_of) auto
+
+lemma sets_bot[simp]: "sets bot = {{}}"
+  unfolding bot_measure_def by (subst sets_measure_of) auto
+
+lemma emeasure_bot[simp]: "emeasure bot = (\<lambda>x. 0)"
+  unfolding bot_measure_def by (rule emeasure_sigma)
+
+inductive less_eq_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+  "sets N = sets M \<Longrightarrow> (\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A \<le> emeasure N A) \<Longrightarrow> less_eq_measure M N"
+| "less_eq_measure bot N"
+
+definition less_measure :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> bool" where
+  "less_measure M N \<longleftrightarrow> (M \<le> N \<and> \<not> N \<le> M)"
+
+instance
+proof (standard, goals)
+  case 1 then show ?case
+    unfolding less_measure_def ..
+next
+  case (2 M) then show ?case
+    by (intro less_eq_measure.intros) auto
+next
+  case (3 M N L) then show ?case
+    apply (safe elim!: less_eq_measure.cases)
+    apply (simp_all add: less_eq_measure.intros)
+    apply (rule less_eq_measure.intros)
+    apply simp
+    apply (blast intro: order_trans) []
+    unfolding less_eq_measure.simps
+    apply (rule disjI2)
+    apply simp
+    apply (rule measure_eqI)
+    apply (auto intro!: antisym)
+    done
+next
+  case (4 M N) then show ?case
+    apply (safe elim!: less_eq_measure.cases intro!: measure_eqI)
+    apply simp
+    apply simp
+    apply (blast intro: antisym)
+    apply (simp)
+    apply (blast intro: antisym)
+    apply simp
+    done
+qed (rule less_eq_measure.intros)
 end
 
+lemma le_emeasureD: "M \<le> N \<Longrightarrow> emeasure M A \<le> emeasure N A"
+  by (cases "A \<in> sets M") (auto elim!: less_eq_measure.cases simp: emeasure_notin_sets)
+
+lemma le_sets: "N \<le> M \<Longrightarrow> sets N \<le> sets M"
+  unfolding less_eq_measure.simps by auto
+
+instantiation measure :: (type) ccpo
+begin
+
+definition Sup_measure :: "'a measure set \<Rightarrow> 'a measure" where
+  "Sup_measure A = measure_of (SUP a:A. space a) (SUP a:A. sets a) (SUP a:A. emeasure a)"
+
+lemma
+  assumes A: "Complete_Partial_Order.chain op \<le> A" and a: "a \<noteq> bot" "a \<in> A"
+  shows space_Sup: "space (Sup A) = space a"
+    and sets_Sup: "sets (Sup A) = sets a"
+proof -
+  have sets: "(SUP a:A. sets a) = sets a"
+  proof (intro antisym SUP_least)
+    fix a' show "a' \<in> A \<Longrightarrow> sets a' \<subseteq> sets a" 
+      using a chainD[OF A, of a a'] by (auto elim!: less_eq_measure.cases)
+  qed (insert \<open>a\<in>A\<close>, auto)
+  have space: "(SUP a:A. space a) = space a"
+  proof (intro antisym SUP_least)
+    fix a' show "a' \<in> A \<Longrightarrow> space a' \<subseteq> space a" 
+      using a chainD[OF A, of a a'] by (intro sets_le_imp_space_le) (auto elim!: less_eq_measure.cases)
+  qed (insert \<open>a\<in>A\<close>, auto)
+  show "space (Sup A) = space a"
+    unfolding Sup_measure_def sets space sets.space_measure_of_eq ..
+  show "sets (Sup A) = sets a"
+    unfolding Sup_measure_def sets space sets.sets_measure_of_eq ..
+qed
+
+lemma emeasure_Sup:
+  assumes A: "Complete_Partial_Order.chain op \<le> A" "A \<noteq> {}"
+  assumes "X \<in> sets (Sup A)"
+  shows "emeasure (Sup A) X = (SUP a:A. emeasure a) X"
+proof (rule emeasure_measure_of[OF Sup_measure_def])
+  show "countably_additive (sets (Sup A)) (SUP a:A. emeasure a)"
+    unfolding countably_additive_def
+  proof safe
+    fix F :: "nat \<Rightarrow> 'a set" assume F: "range F \<subseteq> sets (Sup A)" "disjoint_family F"
+    show "(\<Sum>i. (SUP a:A. emeasure a) (F i)) = SUPREMUM A emeasure (UNION UNIV F)"
+      unfolding SUP_apply
+    proof (subst suminf_SUP_eq_directed)
+      fix N i j assume "i \<in> A" "j \<in> A"
+      with A(1)
+      show "\<exists>k\<in>A. \<forall>n\<in>N. emeasure i (F n) \<le> emeasure k (F n) \<and> emeasure j (F n) \<le> emeasure k (F n)"
+        by (blast elim: chainE dest: le_emeasureD)
+    next
+      show "(SUP n:A. \<Sum>i. emeasure n (F i)) = (SUP y:A. emeasure y (UNION UNIV F))"
+      proof (intro SUP_cong refl)
+        fix a assume "a \<in> A" then show "(\<Sum>i. emeasure a (F i)) = emeasure a (UNION UNIV F)"
+          using sets_Sup[OF A(1), of a] F by (cases "a = bot") (auto simp: suminf_emeasure)
+      qed
+    qed (insert F \<open>A \<noteq> {}\<close>, auto simp: suminf_emeasure intro!: SUP_cong)
+  qed
+qed (insert \<open>A \<noteq> {}\<close> \<open>X \<in> sets (Sup A)\<close>, auto simp: positive_def dest: sets.sets_into_space intro: SUP_upper2)
+
+instance
+proof
+  fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "x \<in> A"
+  show "x \<le> Sup A"
+  proof cases
+    assume "x \<noteq> bot"
+    show ?thesis
+    proof
+      show "sets (Sup A) = sets x"
+        using A \<open>x \<noteq> bot\<close> x by (rule sets_Sup)
+      with x show "\<And>a. a \<in> sets x \<Longrightarrow> emeasure x a \<le> emeasure (Sup A) a"
+        by (subst emeasure_Sup[OF A]) (auto intro: SUP_upper)
+    qed
+  qed simp
+next
+  fix A and x :: "'a measure" assume A: "Complete_Partial_Order.chain op \<le> A" and x: "\<And>z. z \<in> A \<Longrightarrow> z \<le> x"
+  consider "A = {}" | "A = {bot}" | x where "x\<in>A" "x \<noteq> bot"
+    by blast
+  then show "Sup A \<le> x"
+  proof cases
+    assume "A = {}"
+    moreover have "Sup ({}::'a measure set) = bot"
+      by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
+    ultimately show ?thesis
+      by simp
+  next
+    assume "A = {bot}"
+    moreover have "Sup ({bot}::'a measure set) = bot"
+      by (auto simp add: Sup_measure_def sigma_sets_empty_eq intro!: measure_eqI)
+     ultimately show ?thesis
+      by simp
+  next
+    fix a assume "a \<in> A" "a \<noteq> bot"
+    then have "a \<le> x" "x \<noteq> bot" "a \<noteq> bot"
+      using x[OF \<open>a \<in> A\<close>] by (auto simp: bot_unique)
+    then have "sets x = sets a"
+      by (auto elim: less_eq_measure.cases)
+
+    show "Sup A \<le> x"
+    proof (rule less_eq_measure.intros)
+      show "sets x = sets (Sup A)"
+        by (subst sets_Sup[OF A \<open>a \<noteq> bot\<close> \<open>a \<in> A\<close>]) fact
+    next
+      fix X assume "X \<in> sets (Sup A)"
+      then have "emeasure (Sup A) X \<le> (SUP a:A. emeasure a X)"
+        using \<open>a\<in>A\<close> by (subst emeasure_Sup[OF A _]) auto
+      also have "\<dots> \<le> emeasure x X"
+        by (intro SUP_least le_emeasureD x)
+      finally show "emeasure (Sup A) X \<le> emeasure x X" .
+    qed
+  qed
+qed
+end
+
+end

--- a/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:39:10 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Thu Jul 23 16:40:47 2015 +0200
@@ -1642,10 +1642,11 @@
   obtains (measure) \<Omega> A \<mu> where "x = Abs_measure (\<Omega>, A, \<mu>)" "\<forall>a\<in>-A. \<mu> a = 0" "measure_space \<Omega> A \<mu>"
   by atomize_elim (cases x, auto)
 
-lemma sets_eq_imp_space_eq:
-  "sets M = sets M' \<Longrightarrow> space M = space M'"
-  using sets.top[of M] sets.top[of M'] sets.space_closed[of M] sets.space_closed[of M']
-  by blast
+lemma sets_le_imp_space_le: "sets A \<subseteq> sets B \<Longrightarrow> space A \<subseteq> space B"
+  by (auto dest: sets.sets_into_space)
+
+lemma sets_eq_imp_space_eq: "sets M = sets M' \<Longrightarrow> space M = space M'"
+  by (auto intro!: antisym sets_le_imp_space_le)
 
 lemma emeasure_notin_sets: "A \<notin> sets M \<Longrightarrow> emeasure M A = 0"
   by (cases M) (auto simp: sets_def emeasure_def Abs_measure_inverse measure_space_def)