add named theorems order_continuous_intros; lfp/gfp_funpow; bounded variant for lfp/gfp transfer
--- a/src/HOL/Inductive.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Inductive.thy Fri Jul 03 08:26:34 2015 +0200
@@ -230,7 +230,6 @@
apply (simp_all)
done
-
text{*Definition forms of @{text gfp_unfold} and @{text coinduct},
to control unfolding*}
@@ -283,15 +282,6 @@
qed
qed
-lemma lfp_square:
- assumes "mono f" shows "lfp f = lfp (\<lambda>x. f (f x))"
-proof (rule antisym)
- show "lfp f \<le> lfp (\<lambda>x. f (f x))"
- by (intro lfp_lowerbound) (simp add: assms lfp_rolling)
- show "lfp (\<lambda>x. f (f x)) \<le> lfp f"
- by (intro lfp_lowerbound) (simp add: lfp_unfold[OF assms, symmetric])
-qed
-
lemma lfp_lfp:
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
shows "lfp (\<lambda>x. lfp (f x)) = lfp (\<lambda>x. f x x)"
@@ -330,15 +320,6 @@
qed
qed
-lemma gfp_square:
- assumes "mono f" shows "gfp f = gfp (\<lambda>x. f (f x))"
-proof (rule antisym)
- show "gfp (\<lambda>x. f (f x)) \<le> gfp f"
- by (intro gfp_upperbound) (simp add: assms gfp_rolling)
- show "gfp f \<le> gfp (\<lambda>x. f (f x))"
- by (intro gfp_upperbound) (simp add: gfp_unfold[OF assms, symmetric])
-qed
-
lemma gfp_gfp:
assumes f: "\<And>x y w z. x \<le> y \<Longrightarrow> w \<le> z \<Longrightarrow> f x w \<le> f y z"
shows "gfp (\<lambda>x. gfp (f x)) = gfp (\<lambda>x. f x x)"
--- a/src/HOL/Library/Extended_Nat.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy Fri Jul 03 08:26:34 2015 +0200
@@ -6,7 +6,7 @@
section \<open>Extended natural numbers (i.e. with infinity)\<close>
theory Extended_Nat
-imports Main Countable
+imports Main Countable Order_Continuity
begin
class infinity =
@@ -472,6 +472,17 @@
apply (erule (1) le_less_trans)
done
+lemma eSuc_max: "eSuc (max x y) = max (eSuc x) (eSuc y)"
+ by (simp add: eSuc_def split: enat.split)
+
+lemma eSuc_Max:
+ assumes "finite A" "A \<noteq> {}"
+ shows "eSuc (Max A) = Max (eSuc ` A)"
+using assms proof induction
+ case (insert x A)
+ thus ?case by(cases "A = {}")(simp_all add: eSuc_max)
+qed simp
+
instantiation enat :: "{order_bot, order_top}"
begin
@@ -647,6 +658,12 @@
instance enat :: complete_linorder ..
+lemma eSuc_Sup: "A \<noteq> {} \<Longrightarrow> eSuc (Sup A) = Sup (eSuc ` A)"
+ by(auto simp add: Sup_enat_def eSuc_Max inj_on_def dest: finite_imageD)
+
+lemma sup_continuous_eSuc: "sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. eSuc (f x))"
+ using eSuc_Sup[of "_ ` UNIV"] by (auto simp: sup_continuous_def)
+
subsection \<open>Traditional theorem names\<close>
lemmas enat_defs = zero_enat_def one_enat_def eSuc_def
--- a/src/HOL/Library/Extended_Real.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Jul 03 08:26:34 2015 +0200
@@ -8,7 +8,7 @@
section \<open>Extended real number line\<close>
theory Extended_Real
-imports Complex_Main Extended_Nat Liminf_Limsup Order_Continuity
+imports Complex_Main Extended_Nat Liminf_Limsup
begin
text \<open>
@@ -2768,6 +2768,18 @@
qed
qed
+lemma not_MInfty_nonneg[simp]: "0 \<le> (x::ereal) \<Longrightarrow> x \<noteq> - \<infinity>"
+ by auto
+
+lemma sup_continuous_add_left[order_continuous_intros]: "0 \<le> c \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. f x + c :: ereal)"
+ by (auto simp: sup_continuous_def SUP_ereal_add_left)
+
+lemma sup_continuous_add_right[order_continuous_intros]: "0 \<le> c \<Longrightarrow> sup_continuous f \<Longrightarrow> sup_continuous (\<lambda>x. c + f x :: ereal)"
+ using sup_continuous_add_left by (simp add: ac_simps)
+
+lemma sup_continuous_multc[order_continuous_intros]: "0 \<le> c \<Longrightarrow> c < \<infinity> \<Longrightarrow> sup_continuous (\<lambda>f s. f s * c :: ereal)"
+ by (cases c) (auto simp: sup_continuous_def fun_eq_iff Sup_ereal_mult_right')
+
subsubsection \<open>Tests for code generator\<close>
(* A small list of simple arithmetic expressions *)
--- a/src/HOL/Library/Order_Continuity.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Library/Order_Continuity.thy Fri Jul 03 08:26:34 2015 +0200
@@ -5,7 +5,7 @@
section \<open>Continuity and iterations (of set transformers)\<close>
theory Order_Continuity
-imports Main
+imports Complex_Main
begin
(* TODO: Generalize theory to chain-complete partial orders *)
@@ -34,6 +34,8 @@
and have the advantage that these names are duals.
\<close>
+named_theorems order_continuous_intros
+
subsection \<open>Continuity for complete lattices\<close>
definition
@@ -55,12 +57,13 @@
by (simp add: SUP_nat_binary le_iff_sup)
qed
-lemma sup_continuous_intros:
+lemma [order_continuous_intros]:
shows sup_continuous_const: "sup_continuous (\<lambda>x. c)"
and sup_continuous_id: "sup_continuous (\<lambda>x. x)"
and sup_continuous_apply: "sup_continuous (\<lambda>f. f x)"
and sup_continuous_fun: "(\<And>s. sup_continuous (\<lambda>x. P x s)) \<Longrightarrow> sup_continuous P"
- by (auto simp: sup_continuous_def)
+ and sup_continuous_If: "sup_continuous F \<Longrightarrow> sup_continuous G \<Longrightarrow> sup_continuous (\<lambda>f. if C then F f else G f)"
+ by (auto simp: sup_continuous_def)
lemma sup_continuous_compose:
assumes f: "sup_continuous f" and g: "sup_continuous g"
@@ -74,6 +77,38 @@
by (auto simp: sup_continuous_def g[THEN sup_continuousD] f[THEN sup_continuousD])
qed
+lemma sup_continuous_sup[order_continuous_intros]:
+ "sup_continuous f \<Longrightarrow> sup_continuous g \<Longrightarrow> sup_continuous (\<lambda>x. sup (f x) (g x))"
+ by (simp add: sup_continuous_def SUP_sup_distrib)
+
+lemma sup_continuous_inf[order_continuous_intros]:
+ fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+ assumes P: "sup_continuous P" and Q: "sup_continuous Q"
+ shows "sup_continuous (\<lambda>x. inf (P x) (Q x))"
+ unfolding sup_continuous_def
+proof (safe intro!: antisym)
+ fix M :: "nat \<Rightarrow> 'a" assume M: "incseq M"
+ have "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP j i. inf (P (M i)) (Q (M j)))"
+ unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] inf_SUP SUP_inf ..
+ also have "\<dots> \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+ proof (intro SUP_least)
+ fix i j from M assms[THEN sup_continuous_mono] show "inf (P (M i)) (Q (M j)) \<le> (SUP i. inf (P (M i)) (Q (M i)))"
+ by (intro SUP_upper2[of "sup i j"] inf_mono) (auto simp: mono_def)
+ qed
+ finally show "inf (P (SUP i. M i)) (Q (SUP i. M i)) \<le> (SUP i. inf (P (M i)) (Q (M i)))" .
+
+ show "(SUP i. inf (P (M i)) (Q (M i))) \<le> inf (P (SUP i. M i)) (Q (SUP i. M i))"
+ unfolding sup_continuousD[OF P M] sup_continuousD[OF Q M] by (intro SUP_least inf_mono SUP_upper)
+qed
+
+lemma sup_continuous_and[order_continuous_intros]:
+ "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<and> Q x)"
+ using sup_continuous_inf[of P Q] by simp
+
+lemma sup_continuous_or[order_continuous_intros]:
+ "sup_continuous P \<Longrightarrow> sup_continuous Q \<Longrightarrow> sup_continuous (\<lambda>x. P x \<or> Q x)"
+ by (auto simp: sup_continuous_def)
+
lemma sup_continuous_lfp:
assumes "sup_continuous F" shows "lfp F = (SUP i. (F ^^ i) bot)" (is "lfp F = ?U")
proof (rule antisym)
@@ -122,6 +157,51 @@
unfolding sup_continuous_lfp[OF g] by simp
qed
+lemma lfp_transfer_bounded:
+ assumes P: "P bot" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. (\<And>i. P (M i)) \<Longrightarrow> P (SUP i::nat. M i)"
+ assumes \<alpha>: "\<And>M. mono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (SUP i. M i) = (SUP i. \<alpha> (M i))"
+ assumes f: "sup_continuous f" and g: "sup_continuous g"
+ assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+ assumes g_bound: "\<And>x. \<alpha> bot \<le> g x"
+ shows "\<alpha> (lfp f) = lfp g"
+proof (rule antisym)
+ note mono_g = sup_continuous_mono[OF g]
+ have lfp_bound: "\<alpha> bot \<le> lfp g"
+ by (subst lfp_unfold[OF mono_g]) (rule g_bound)
+
+ have P_pow: "P ((f ^^ i) bot)" for i
+ by (induction i) (auto intro!: P)
+ have incseq_pow: "mono (\<lambda>i. (f ^^ i) bot)"
+ unfolding mono_iff_le_Suc
+ proof
+ fix i show "(f ^^ i) bot \<le> (f ^^ (Suc i)) bot"
+ proof (induct i)
+ case Suc thus ?case using monoD[OF sup_continuous_mono[OF f] Suc] by auto
+ qed (simp add: le_fun_def)
+ qed
+ have P_lfp: "P (lfp f)"
+ using P_pow unfolding sup_continuous_lfp[OF f] by (auto intro!: P)
+
+ have "\<alpha> (lfp f) = (SUP i. \<alpha> ((f^^i) bot))"
+ unfolding sup_continuous_lfp[OF f] using incseq_pow P_pow by (rule \<alpha>)
+ also have "\<dots> \<le> lfp g"
+ proof (rule SUP_least)
+ fix i show "\<alpha> ((f^^i) bot) \<le> lfp g"
+ proof (induction i)
+ case (Suc n) then show ?case
+ by (subst lfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
+ qed (simp add: lfp_bound)
+ qed
+ finally show "\<alpha> (lfp f) \<le> lfp g" .
+
+ show "lfp g \<le> \<alpha> (lfp f)"
+ proof (induction rule: lfp_ordinal_induct[OF mono_g])
+ case (1 S) then show ?case
+ by (subst lfp_unfold[OF sup_continuous_mono[OF f]])
+ (simp add: monoD[OF mono_g] P_lfp)
+ qed (auto intro: Sup_least)
+qed
+
definition
inf_continuous :: "('a::complete_lattice \<Rightarrow> 'b::complete_lattice) \<Rightarrow> bool" where
"inf_continuous F \<longleftrightarrow> (\<forall>M::nat \<Rightarrow> 'a. antimono M \<longrightarrow> F (INF i. M i) = (INF i. F (M i)))"
@@ -141,12 +221,45 @@
by (simp add: INF_nat_binary le_iff_inf inf_commute)
qed
-lemma inf_continuous_intros:
+lemma [order_continuous_intros]:
shows inf_continuous_const: "inf_continuous (\<lambda>x. c)"
and inf_continuous_id: "inf_continuous (\<lambda>x. x)"
and inf_continuous_apply: "inf_continuous (\<lambda>f. f x)"
and inf_continuous_fun: "(\<And>s. inf_continuous (\<lambda>x. P x s)) \<Longrightarrow> inf_continuous P"
- by (auto simp: inf_continuous_def)
+ and inf_continuous_If: "inf_continuous F \<Longrightarrow> inf_continuous G \<Longrightarrow> inf_continuous (\<lambda>f. if C then F f else G f)"
+ by (auto simp: inf_continuous_def)
+
+lemma inf_continuous_inf[order_continuous_intros]:
+ "inf_continuous f \<Longrightarrow> inf_continuous g \<Longrightarrow> inf_continuous (\<lambda>x. inf (f x) (g x))"
+ by (simp add: inf_continuous_def INF_inf_distrib)
+
+lemma inf_continuous_sup[order_continuous_intros]:
+ fixes P Q :: "'a :: complete_lattice \<Rightarrow> 'b :: complete_distrib_lattice"
+ assumes P: "inf_continuous P" and Q: "inf_continuous Q"
+ shows "inf_continuous (\<lambda>x. sup (P x) (Q x))"
+ unfolding inf_continuous_def
+proof (safe intro!: antisym)
+ fix M :: "nat \<Rightarrow> 'a" assume M: "decseq M"
+ show "sup (P (INF i. M i)) (Q (INF i. M i)) \<le> (INF i. sup (P (M i)) (Q (M i)))"
+ unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] by (intro INF_greatest sup_mono INF_lower)
+
+ have "(INF i. sup (P (M i)) (Q (M i))) \<le> (INF j i. sup (P (M i)) (Q (M j)))"
+ proof (intro INF_greatest)
+ fix i j from M assms[THEN inf_continuous_mono] show "sup (P (M i)) (Q (M j)) \<ge> (INF i. sup (P (M i)) (Q (M i)))"
+ by (intro INF_lower2[of "sup i j"] sup_mono) (auto simp: mono_def antimono_def)
+ qed
+ also have "\<dots> \<le> sup (P (INF i. M i)) (Q (INF i. M i))"
+ unfolding inf_continuousD[OF P M] inf_continuousD[OF Q M] INF_sup sup_INF ..
+ finally show "sup (P (INF i. M i)) (Q (INF i. M i)) \<ge> (INF i. sup (P (M i)) (Q (M i)))" .
+qed
+
+lemma inf_continuous_and[order_continuous_intros]:
+ "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<and> Q x)"
+ using inf_continuous_inf[of P Q] by simp
+
+lemma inf_continuous_or[order_continuous_intros]:
+ "inf_continuous P \<Longrightarrow> inf_continuous Q \<Longrightarrow> inf_continuous (\<lambda>x. P x \<or> Q x)"
+ using inf_continuous_sup[of P Q] by simp
lemma inf_continuous_compose:
assumes f: "inf_continuous f" and g: "inf_continuous g"
@@ -208,4 +321,70 @@
unfolding inf_continuous_gfp[OF g] by simp
qed
+lemma gfp_transfer_bounded:
+ assumes P: "P (f top)" "\<And>x. P x \<Longrightarrow> P (f x)" "\<And>M. antimono M \<Longrightarrow> (\<And>i. P (M i)) \<Longrightarrow> P (INF i::nat. M i)"
+ assumes \<alpha>: "\<And>M. antimono M \<Longrightarrow> (\<And>i::nat. P (M i)) \<Longrightarrow> \<alpha> (INF i. M i) = (INF i. \<alpha> (M i))"
+ assumes f: "inf_continuous f" and g: "inf_continuous g"
+ assumes [simp]: "\<And>x. P x \<Longrightarrow> \<alpha> (f x) = g (\<alpha> x)"
+ assumes g_bound: "\<And>x. g x \<le> \<alpha> (f top)"
+ shows "\<alpha> (gfp f) = gfp g"
+proof (rule antisym)
+ note mono_g = inf_continuous_mono[OF g]
+
+ have P_pow: "P ((f ^^ i) (f top))" for i
+ by (induction i) (auto intro!: P)
+
+ have antimono_pow: "antimono (\<lambda>i. (f ^^ i) top)"
+ unfolding antimono_iff_le_Suc
+ proof
+ fix i show "(f ^^ Suc i) top \<le> (f ^^ i) top"
+ proof (induct i)
+ case Suc thus ?case using monoD[OF inf_continuous_mono[OF f] Suc] by auto
+ qed (simp add: le_fun_def)
+ qed
+ have antimono_pow2: "antimono (\<lambda>i. (f ^^ i) (f top))"
+ proof
+ show "x \<le> y \<Longrightarrow> (f ^^ y) (f top) \<le> (f ^^ x) (f top)" for x y
+ using antimono_pow[THEN antimonoD, of "Suc x" "Suc y"]
+ unfolding funpow_Suc_right by simp
+ qed
+
+ have gfp_f: "gfp f = (INF i. (f ^^ i) (f top))"
+ unfolding inf_continuous_gfp[OF f]
+ proof (rule INF_eq)
+ show "\<exists>j\<in>UNIV. (f ^^ j) (f top) \<le> (f ^^ i) top" for i
+ by (intro bexI[of _ "i - 1"]) (auto simp: diff_Suc funpow_Suc_right simp del: funpow.simps(2) split: nat.split)
+ show "\<exists>j\<in>UNIV. (f ^^ j) top \<le> (f ^^ i) (f top)" for i
+ by (intro bexI[of _ "Suc i"]) (auto simp: funpow_Suc_right simp del: funpow.simps(2))
+ qed
+
+ have P_lfp: "P (gfp f)"
+ unfolding gfp_f by (auto intro!: P P_pow antimono_pow2)
+
+ have "\<alpha> (gfp f) = (INF i. \<alpha> ((f^^i) (f top)))"
+ unfolding gfp_f by (rule \<alpha>) (auto intro!: P_pow antimono_pow2)
+ also have "\<dots> \<ge> gfp g"
+ proof (rule INF_greatest)
+ fix i show "gfp g \<le> \<alpha> ((f^^i) (f top))"
+ proof (induction i)
+ case (Suc n) then show ?case
+ by (subst gfp_unfold[OF mono_g]) (simp add: monoD[OF mono_g] P_pow)
+ next
+ case 0
+ have "gfp g \<le> \<alpha> (f top)"
+ by (subst gfp_unfold[OF mono_g]) (rule g_bound)
+ then show ?case
+ by simp
+ qed
+ qed
+ finally show "gfp g \<le> \<alpha> (gfp f)" .
+
+ show "\<alpha> (gfp f) \<le> gfp g"
+ proof (induction rule: gfp_ordinal_induct[OF mono_g])
+ case (1 S) then show ?case
+ by (subst gfp_unfold[OF inf_continuous_mono[OF f]])
+ (simp add: monoD[OF mono_g] P_lfp)
+ qed (auto intro: Inf_greatest)
+qed
+
end
--- a/src/HOL/Nat.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Nat.thy Fri Jul 03 08:26:34 2015 +0200
@@ -1416,6 +1416,42 @@
using Kleene_iter_lpfp[OF assms(1)] lfp_unfold[OF assms(1)] by simp
qed
+lemma mono_pow:
+ fixes f :: "'a \<Rightarrow> 'a::complete_lattice"
+ shows "mono f \<Longrightarrow> mono (f ^^ n)"
+ by (induction n) (auto simp: mono_def)
+
+lemma lfp_funpow:
+ assumes f: "mono f" shows "lfp (f ^^ Suc n) = lfp f"
+proof (rule antisym)
+ show "lfp f \<le> lfp (f ^^ Suc n)"
+ proof (rule lfp_lowerbound)
+ have "f (lfp (f ^^ Suc n)) = lfp (\<lambda>x. f ((f ^^ n) x))"
+ unfolding funpow_Suc_right by (simp add: lfp_rolling f mono_pow comp_def)
+ then show "f (lfp (f ^^ Suc n)) \<le> lfp (f ^^ Suc n)"
+ by (simp add: comp_def)
+ qed
+ have "(f^^n) (lfp f) = lfp f" for n
+ by (induction n) (auto intro: f lfp_unfold[symmetric])
+ then show "lfp (f^^Suc n) \<le> lfp f"
+ by (intro lfp_lowerbound) (simp del: funpow.simps)
+qed
+
+lemma gfp_funpow:
+ assumes f: "mono f" shows "gfp (f ^^ Suc n) = gfp f"
+proof (rule antisym)
+ show "gfp f \<ge> gfp (f ^^ Suc n)"
+ proof (rule gfp_upperbound)
+ have "f (gfp (f ^^ Suc n)) = gfp (\<lambda>x. f ((f ^^ n) x))"
+ unfolding funpow_Suc_right by (simp add: gfp_rolling f mono_pow comp_def)
+ then show "f (gfp (f ^^ Suc n)) \<ge> gfp (f ^^ Suc n)"
+ by (simp add: comp_def)
+ qed
+ have "(f^^n) (gfp f) = gfp f" for n
+ by (induction n) (auto intro: f gfp_unfold[symmetric])
+ then show "gfp (f^^Suc n) \<ge> gfp f"
+ by (intro gfp_upperbound) (simp del: funpow.simps)
+qed
subsection {* Embedding of the naturals into any @{text semiring_1}: @{term of_nat} *}
--- a/src/HOL/Probability/Measure_Space.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Measure_Space.thy Fri Jul 03 08:26:34 2015 +0200
@@ -548,7 +548,7 @@
using LIMSEQ_INF[OF decseq_emeasure, OF A]
using INF_emeasure_decseq[OF A fin] by simp
-lemma emeasure_lfp[consumes 1, case_names cont measurable]:
+lemma emeasure_lfp'[consumes 1, case_names cont measurable]:
assumes "P M"
assumes cont: "sup_continuous F"
assumes *: "\<And>M A. P M \<Longrightarrow> (\<And>N. P N \<Longrightarrow> Measurable.pred N A) \<Longrightarrow> Measurable.pred M (F A)"
@@ -574,6 +574,20 @@
by (subst SUP_emeasure_incseq) auto
qed
+lemma emeasure_lfp:
+ assumes [simp]: "\<And>s. sets (M s) = sets N"
+ assumes cont: "sup_continuous F" "sup_continuous f"
+ assumes nonneg: "\<And>P s. 0 \<le> f P s"
+ assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
+ assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
+ shows "emeasure (M s) {x\<in>space N. lfp F x} = lfp f s"
+proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and P="Measurable.pred N", symmetric])
+ fix C assume "incseq C" "\<And>i. Measurable.pred N (C i)"
+ then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (SUP i. C i) x}) = (SUP i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
+ unfolding SUP_apply[abs_def]
+ by (subst SUP_emeasure_incseq) (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
+qed (auto simp add: iter nonneg le_fun_def SUP_apply[abs_def] intro!: meas cont)
+
lemma emeasure_subadditive:
assumes [measurable]: "A \<in> sets M" "B \<in> sets M"
shows "emeasure M (A \<union> B) \<le> emeasure M A + emeasure M B"
@@ -1254,7 +1268,7 @@
have "emeasure (distr M' M f) {x \<in> space (distr M' M f). lfp F x} =
(SUP i. emeasure (distr M' M f) {x \<in> space (distr M' M f). (F ^^ i) (\<lambda>x. False) x})"
using `P M`
- proof (coinduction arbitrary: M rule: emeasure_lfp)
+ proof (coinduction arbitrary: M rule: emeasure_lfp')
case (measurable A N) then have "\<And>N. P N \<Longrightarrow> Measurable.pred (distr M' N f) A"
by metis
then have "\<And>N. P N \<Longrightarrow> Measurable.pred N A"
@@ -1662,6 +1676,26 @@
with f show "emeasure (distr M M' f) (space (distr M M' f)) \<noteq> \<infinity>" by (auto simp: emeasure_distr)
qed
+lemma emeasure_gfp[consumes 1, case_names cont measurable]:
+ assumes sets[simp]: "\<And>s. sets (M s) = sets N"
+ assumes "\<And>s. finite_measure (M s)"
+ assumes cont: "inf_continuous F" "inf_continuous f"
+ assumes meas: "\<And>P. Measurable.pred N P \<Longrightarrow> Measurable.pred N (F P)"
+ assumes iter: "\<And>P s. Measurable.pred N P \<Longrightarrow> emeasure (M s) {x\<in>space N. F P x} = f (\<lambda>s. emeasure (M s) {x\<in>space N. P x}) s"
+ assumes bound: "\<And>P. f P \<le> f (\<lambda>s. emeasure (M s) (space (M s)))"
+ shows "emeasure (M s) {x\<in>space N. gfp F x} = gfp f s"
+proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. emeasure (M s) {x\<in>space N. F x}" and g=f and f=F and
+ P="Measurable.pred N", symmetric])
+ interpret finite_measure "M s" for s by fact
+ fix C assume "decseq C" "\<And>i. Measurable.pred N (C i)"
+ then show "(\<lambda>s. emeasure (M s) {x \<in> space N. (INF i. C i) x}) = (INF i. (\<lambda>s. emeasure (M s) {x \<in> space N. C i x}))"
+ unfolding INF_apply[abs_def]
+ by (subst INF_emeasure_decseq) (auto simp: antimono_def fun_eq_iff intro!: arg_cong2[where f=emeasure])
+next
+ show "f x \<le> (\<lambda>s. emeasure (M s) {x \<in> space N. F top x})" for x
+ using bound[of x] sets_eq_imp_space_eq[OF sets] by (simp add: iter)
+qed (auto simp add: iter le_fun_def INF_apply[abs_def] intro!: meas cont)
+
subsection {* Counting space *}
lemma strict_monoI_Suc:
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Fri Jul 03 08:26:34 2015 +0200
@@ -1545,7 +1545,7 @@
finally show ?thesis unfolding nn_integral_max_0 .
qed
-lemma sup_continuous_nn_integral:
+lemma sup_continuous_nn_integral[order_continuous_intros]:
assumes f: "\<And>y. sup_continuous (f y)"
assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
shows "sup_continuous (\<lambda>x. (\<integral>\<^sup>+y. f y x \<partial>M))"
@@ -1557,7 +1557,7 @@
by (subst nn_integral_monotone_convergence_SUP) (auto simp: mono_def le_fun_def)
qed
-lemma inf_continuous_nn_integral:
+lemma inf_continuous_nn_integral[order_continuous_intros]:
assumes f: "\<And>y. inf_continuous (f y)"
assumes [measurable]: "\<And>x. (\<lambda>y. f y x) \<in> borel_measurable M"
assumes bnd: "\<And>x. (\<integral>\<^sup>+ y. f y x \<partial>M) \<noteq> \<infinity>"
@@ -1739,122 +1739,57 @@
qed
lemma nn_integral_lfp:
- assumes sets: "\<And>s. sets (M s) = sets N"
+ assumes sets[simp]: "\<And>s. sets (M s) = sets N"
assumes f: "sup_continuous f"
+ assumes g: "sup_continuous g"
+ assumes nonneg: "\<And>F s. 0 \<le> g F s"
assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
- assumes nonneg: "\<And>F s. 0 \<le> g F s"
- assumes g: "sup_continuous g"
assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
shows "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = lfp g s"
-proof (rule antisym)
- show "lfp g s \<le> (\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s)"
- proof (induction arbitrary: s rule: lfp_ordinal_induct[OF sup_continuous_mono[OF g]])
- case (1 F) then show ?case
- apply (subst lfp_unfold[OF sup_continuous_mono[OF f]])
- apply (subst step)
- apply (rule borel_measurable_lfp[OF f])
- apply (rule meas)
- apply assumption+
- apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
- apply (simp add: le_fun_def)
- done
- qed (auto intro: SUP_least)
-
- have lfp_nonneg: "\<And>s. 0 \<le> lfp g s"
- by (subst lfp_unfold[OF sup_continuous_mono[OF g]]) (rule nonneg)
-
- { fix i have "((f ^^ i) bot) \<in> borel_measurable N"
- by (induction i) (simp_all add: meas) }
-
- have "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (SUP i. (f ^^ i) bot \<omega>) \<partial>M s)"
- by (simp add: sup_continuous_lfp f)
- also have "\<dots> = (SUP i. \<integral>\<^sup>+\<omega>. (f ^^ i) bot \<omega> \<partial>M s)"
- proof (rule nn_integral_monotone_convergence_SUP)
- show "incseq (\<lambda>i. (f ^^ i) bot)"
- using f[THEN sup_continuous_mono] by (rule mono_funpow)
- show "\<And>i. ((f ^^ i) bot) \<in> borel_measurable (M s)"
- unfolding measurable_cong_sets[OF sets refl] by fact
- qed
- also have "\<dots> \<le> lfp g s"
- proof (rule SUP_least)
- fix i show "integral\<^sup>N (M s) ((f ^^ i) bot) \<le> lfp g s"
- proof (induction i arbitrary: s)
- case 0 then show ?case
- by (simp add: nn_integral_const_nonpos lfp_nonneg)
- next
- case (Suc n)
- show ?case
- apply (simp del: bot_apply)
- apply (subst step)
- apply fact
- apply (subst lfp_unfold[OF sup_continuous_mono[OF g]])
- apply (rule monoD[OF sup_continuous_mono[OF g], THEN le_funD])
- apply (rule le_funI)
- apply (rule Suc)
- done
- qed
- qed
- finally show "(\<integral>\<^sup>+\<omega>. lfp f \<omega> \<partial>M s) \<le> lfp g s" .
-qed
+proof (subst lfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f and P="\<lambda>f. f \<in> borel_measurable N", symmetric])
+ fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume "incseq C" "\<And>i. C i \<in> borel_measurable N"
+ then show "(\<lambda>s. \<integral>\<^sup>+x. (SUP i. C i) x \<partial>M s) = (SUP i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))"
+ unfolding SUP_apply[abs_def]
+ by (subst nn_integral_monotone_convergence_SUP)
+ (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets)
+next
+ show "\<And>x. (\<lambda>s. integral\<^sup>N (M s) bot) \<le> g x"
+ by (subst nn_integral_max_0[symmetric])
+ (simp add: sup_ereal_def[symmetric] le_fun_def nonneg del: sup_ereal_def)
+qed (auto simp add: step nonneg le_fun_def SUP_apply[abs_def] bot_fun_def intro!: meas f g)
lemma nn_integral_gfp:
- assumes sets: "\<And>s. sets (M s) = sets N"
- assumes f: "inf_continuous f"
+ assumes sets[simp]: "\<And>s. sets (M s) = sets N"
+ assumes f: "inf_continuous f" and g: "inf_continuous g"
assumes meas: "\<And>F. F \<in> borel_measurable N \<Longrightarrow> f F \<in> borel_measurable N"
- assumes bound: "\<And>F s. (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>"
+ assumes bound: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> (\<integral>\<^sup>+x. f F x \<partial>M s) < \<infinity>"
assumes non_zero: "\<And>s. emeasure (M s) (space (M s)) \<noteq> 0"
- assumes g: "inf_continuous g"
assumes step: "\<And>F s. F \<in> borel_measurable N \<Longrightarrow> integral\<^sup>N (M s) (f F) = g (\<lambda>s. integral\<^sup>N (M s) F) s"
shows "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = gfp g s"
-proof (rule antisym)
- show "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) \<le> gfp g s"
- proof (induction arbitrary: s rule: gfp_ordinal_induct[OF inf_continuous_mono[OF g]])
- case (1 F) then show ?case
- apply (subst gfp_unfold[OF inf_continuous_mono[OF f]])
- apply (subst step)
- apply (rule borel_measurable_gfp[OF f])
- apply (rule meas)
- apply assumption+
- apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
- apply (simp add: le_fun_def)
- done
- qed (auto intro: INF_greatest)
-
- { fix i have "((f ^^ i) top) \<in> borel_measurable N"
- by (induction i) (simp_all add: meas) }
-
- have "(\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s) = (\<integral>\<^sup>+\<omega>. (INF i. (f ^^ i) top \<omega>) \<partial>M s)"
- by (simp add: inf_continuous_gfp f)
- also have "\<dots> = (INF i. \<integral>\<^sup>+\<omega>. (f ^^ i) top \<omega> \<partial>M s)"
- proof (rule nn_integral_monotone_convergence_INF)
- show "decseq (\<lambda>i. (f ^^ i) top)"
- using f[THEN inf_continuous_mono] by (rule antimono_funpow)
- show "\<And>i. ((f ^^ i) top) \<in> borel_measurable (M s)"
- unfolding measurable_cong_sets[OF sets refl] by fact
- show "integral\<^sup>N (M s) ((f ^^ 1) top) < \<infinity>"
- using bound[of s top] by simp
- qed
- also have "\<dots> \<ge> gfp g s"
- proof (rule INF_greatest)
- fix i show "gfp g s \<le> integral\<^sup>N (M s) ((f ^^ i) top)"
- proof (induction i arbitrary: s)
- case 0 with non_zero[of s] show ?case
- by (simp add: top_ereal_def less_le emeasure_nonneg)
- next
- case (Suc n)
- show ?case
- apply (simp del: top_apply)
- apply (subst step)
- apply fact
- apply (subst gfp_unfold[OF inf_continuous_mono[OF g]])
- apply (rule monoD[OF inf_continuous_mono[OF g], THEN le_funD])
- apply (rule le_funI)
- apply (rule Suc)
- done
- qed
- qed
- finally show "gfp g s \<le> (\<integral>\<^sup>+\<omega>. gfp f \<omega> \<partial>M s)" .
-qed
+proof (subst gfp_transfer_bounded[where \<alpha>="\<lambda>F s. \<integral>\<^sup>+x. F x \<partial>M s" and g=g and f=f
+ and P="\<lambda>F. F \<in> borel_measurable N \<and> (\<forall>s. (\<integral>\<^sup>+x. F x \<partial>M s) < \<infinity>)", symmetric])
+ fix C :: "nat \<Rightarrow> 'b \<Rightarrow> ereal" assume "decseq C" "\<And>i. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)"
+ then show "(\<lambda>s. \<integral>\<^sup>+x. (INF i. C i) x \<partial>M s) = (INF i. (\<lambda>s. \<integral>\<^sup>+x. C i x \<partial>M s))"
+ unfolding INF_apply[abs_def]
+ by (subst nn_integral_monotone_convergence_INF)
+ (auto simp: mono_def fun_eq_iff intro!: arg_cong2[where f=emeasure] cong: measurable_cong_sets)
+next
+ show "\<And>x. g x \<le> (\<lambda>s. integral\<^sup>N (M s) (f top))"
+ by (subst step)
+ (auto simp add: top_fun_def top_ereal_def less_le emeasure_nonneg non_zero le_fun_def
+ cong del: if_cong intro!: monoD[OF inf_continuous_mono[OF g], THEN le_funD])
+next
+ fix C assume "\<And>i::nat. C i \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (C i) < \<infinity>)" "decseq C"
+ with bound show "INFIMUM UNIV C \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) (INFIMUM UNIV C) < \<infinity>)"
+ unfolding INF_apply[abs_def]
+ by (subst nn_integral_monotone_convergence_INF)
+ (auto cong: measurable_cong_sets intro!: borel_measurable_INF
+ simp: INF_less_iff simp del: ereal_infty_less(1))
+next
+ show "\<And>x. x \<in> borel_measurable N \<and> (\<forall>s. integral\<^sup>N (M s) x < \<infinity>) \<Longrightarrow>
+ (\<lambda>s. integral\<^sup>N (M s) (f x)) = g (\<lambda>s. integral\<^sup>N (M s) x)"
+ by (subst step) auto
+qed (insert bound, auto simp add: le_fun_def INF_apply[abs_def] top_fun_def intro!: meas f g)
subsection {* Integral under concrete measures *}
--- a/src/HOL/Probability/Regularity.thy Thu Jul 02 16:14:20 2015 +0200
+++ b/src/HOL/Probability/Regularity.thy Fri Jul 03 08:26:34 2015 +0200
@@ -55,7 +55,7 @@
assume "\<not> y \<le> x" hence "y > x" by simp hence "y \<noteq> - \<infinity>" by auto
hence y_fin: "\<bar>y\<bar> \<noteq> \<infinity>" using `y \<noteq> \<infinity>` by auto
have x_fin: "\<bar>x\<bar> \<noteq> \<infinity>" using `y > x` f_fin f_nonneg approx[where e = 1] A_notempty
- apply auto by (metis ereal_infty_less_eq(2) f_le_y)
+ by auto
def e \<equiv> "real ((y - x) / 2)"
have e: "y > x + e" "e > 0" using `y > x` y_fin x_fin by (auto simp: e_def field_simps)
from approx[OF `e > 0`] obtain i where i: "i \<in> A" "x + e \<ge> f i" by blast