--- a/src/HOL/Probability/Binary_Product_Measure.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Binary_Product_Measure.thy Mon Nov 24 12:20:14 2014 +0100
@@ -43,7 +43,7 @@
shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
-lemma sets_pair_measure_cong[cong]:
+lemma sets_pair_measure_cong[measurable_cong, cong]:
"sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
--- a/src/HOL/Probability/Bochner_Integration.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Nov 24 12:20:14 2014 +0100
@@ -2330,7 +2330,7 @@
lemma tendsto_integral_at_top:
fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
- assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
+ assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
proof (rule tendsto_at_topI_sequentially)
fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
--- a/src/HOL/Probability/Convolution.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Convolution.thy Mon Nov 24 12:20:14 2014 +0100
@@ -23,7 +23,7 @@
lemma nn_integral_convolution:
assumes "finite_measure M" "finite_measure N"
- assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+ assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
assumes [measurable]: "f \<in> borel_measurable borel"
shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
proof -
@@ -53,7 +53,7 @@
lemma convolution_finite:
assumes [simp]: "finite_measure M" "finite_measure N"
- assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+ assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
shows "finite_measure (M \<star> N)"
unfolding convolution_def
by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
@@ -71,7 +71,7 @@
lemma convolution_emeasure_3':
assumes [simp, measurable]:"A \<in> sets borel"
assumes [simp]: "finite_measure M" "finite_measure N" "finite_measure L"
- assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
+ assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
shows "emeasure ((L \<star> M) \<star> N ) A = \<integral>\<^sup>+x. \<integral>\<^sup>+y. \<integral>\<^sup>+z. indicator A (x + y + z) \<partial>N \<partial>M \<partial>L"
apply (subst nn_integral_indicator[symmetric], simp)+
apply (subst nn_integral_convolution)
@@ -82,7 +82,7 @@
lemma convolution_commutative:
assumes [simp]: "finite_measure M" "finite_measure N"
- assumes [simp]: "sets N = sets borel" "sets M = sets borel"
+ assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel"
shows "(M \<star> N) = (N \<star> M)"
proof (rule measure_eqI)
interpret M: finite_measure M by fact
--- a/src/HOL/Probability/Fin_Map.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Mon Nov 24 12:20:14 2014 +0100
@@ -1311,7 +1311,7 @@
assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
using assms
- by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
+ by (auto simp: measurable_cong_sets[OF s2 refl] mapmeasure_def emeasure_distr
fm_measurable space_PiM PiE_def)
lemma mapmeasure_PiM:
@@ -1322,7 +1322,7 @@
assumes X: "X \<in> sets M"
shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
unfolding mapmeasure_def
-proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
+proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
have "X \<subseteq> space (Pi\<^sub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
from assms inj_on_fm[of "\<lambda>_. N"] set_mp[OF this] have "fm -` fm ` X \<inter> space (Pi\<^sub>M J (\<lambda>_. N)) = X"
by (auto simp: vimage_image_eq inj_on_def)
--- a/src/HOL/Probability/Finite_Product_Measure.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Mon Nov 24 12:20:14 2014 +0100
@@ -369,7 +369,8 @@
unfolding sets_PiM_single space[symmetric]
by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
-lemma sets_PiM_cong: assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
+lemma sets_PiM_cong[measurable_cong]:
+ assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
lemma sets_PiM_I:
@@ -470,7 +471,7 @@
"\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
by (cases i) simp_all
-
+
lemma measurable_case_nat'[measurable (raw)]:
assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
@@ -885,6 +886,8 @@
have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
by (auto simp: extensional_def restrict_def)
+ have [measurable]: "\<And>j. j \<in> {i} \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)" by simp
+
fix A assume A: "A \<in> sets ?P"
then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)"
by simp
--- a/src/HOL/Probability/Giry_Monad.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Mon Nov 24 12:20:14 2014 +0100
@@ -87,6 +87,25 @@
using measurable_space[OF N x]
by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
+ML {*
+
+fun subprob_cong thm ctxt = (
+ let
+ val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
+ val free = thm' |> concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
+ dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
+ in
+ if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)
+ else ([], ctxt)
+ end
+ handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))
+
+*}
+
+setup \<open>
+ Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
+\<close>
+
context
fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
begin
@@ -125,7 +144,7 @@
ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
qed
-lemma nn_integral_measurable_subprob_algebra:
+lemma nn_integral_measurable_subprob_algebra':
assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
using f
@@ -144,24 +163,30 @@
next
case (mult f c)
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. c * f M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. c * \<integral>\<^sup>+M''. f M'' \<partial>M') \<in> ?B"
- by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
+ by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
ultimately show ?case
+ using [[simp_trace_new]]
by simp
next
case (add f g)
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. f M'' + g M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. (\<integral>\<^sup>+M''. f M'' \<partial>M') + (\<integral>\<^sup>+M''. g M'' \<partial>M')) \<in> ?B"
- by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
+ by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
ultimately show ?case
by (simp add: ac_simps)
next
case (seq F)
moreover then have "(\<lambda>M'. \<integral>\<^sup>+M''. (SUP i. F i) M'' \<partial>M') \<in> ?B \<longleftrightarrow> (\<lambda>M'. SUP i. (\<integral>\<^sup>+M''. F i M'' \<partial>M')) \<in> ?B"
unfolding SUP_apply
- by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
+ by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
ultimately show ?case
by (simp add: ac_simps)
qed
+lemma nn_integral_measurable_subprob_algebra:
+ "f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)"
+ by (subst nn_integral_max_0[symmetric])
+ (auto intro!: nn_integral_measurable_subprob_algebra')
+
lemma measurable_distr:
assumes [measurable]: "f \<in> measurable M N"
shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
@@ -173,11 +198,12 @@
then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
(\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
by (intro measurable_cong)
- (auto simp: emeasure_distr space_subprob_algebra dest: sets_eq_imp_space_eq cong: measurable_cong)
+ (auto simp: emeasure_distr space_subprob_algebra
+ intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])
also have "\<dots>"
using A by (intro measurable_emeasure_subprob_algebra) simp
finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
- qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
+ qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)
qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
lemma emeasure_space_subprob_algebra[measurable]:
@@ -445,23 +471,17 @@
qed
lemma nn_integral_measurable_subprob_algebra2:
- assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)" and [simp]: "\<And>x y. 0 \<le> f x y"
+ assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
proof -
+ note nn_integral_measurable_subprob_algebra[measurable]
+ note measurable_distr2[measurable]
have "(\<lambda>x. integral\<^sup>N (distr (L x) (M \<Otimes>\<^sub>M N) (\<lambda>y. (x, y))) (\<lambda>(x, y). f x y)) \<in> borel_measurable M"
- apply (rule measurable_compose[OF _ nn_integral_measurable_subprob_algebra])
- apply (rule measurable_distr2)
- apply measurable
- apply (simp split: prod.split)
- done
+ by measurable
then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
- apply (rule measurable_cong[THEN iffD1, rotated])
- apply (subst nn_integral_distr)
- apply measurable
- apply (rule subprob_measurableD(2)[OF N], assumption)
- apply measurable
- done
+ by (rule measurable_cong[THEN iffD1, rotated])
+ (simp add: nn_integral_distr)
qed
lemma emeasure_measurable_subprob_algebra2:
@@ -545,16 +565,14 @@
by (simp_all add: join_def)
lemma emeasure_join:
- assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
+ assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
proof (rule emeasure_measure_of[OF join_def])
- have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
- by auto
show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
proof (rule countably_additiveI)
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
- using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
+ using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)
also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
proof (rule nn_integral_cong)
fix M' assume "M' \<in> space M"
@@ -577,7 +595,7 @@
by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
qed
also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
- using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
+ using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`]
by (rule nn_integral_measurable_subprob_algebra)
finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
next
@@ -596,8 +614,9 @@
thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
qed (auto simp: space_subprob_algebra)
-lemma nn_integral_join:
- assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
+lemma nn_integral_join':
+ assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
+ and M[measurable_cong]: "sets M = sets (subprob_algebra N)"
shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
using f
proof induct
@@ -619,51 +638,58 @@
next
case (mult f c)
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. c * f x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. c * \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
- using mult M
- by (intro nn_integral_cong nn_integral_cmult)
- (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+ using mult M M[THEN sets_eq_imp_space_eq]
+ by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
- using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
+ using nn_integral_measurable_subprob_algebra[OF mult(3)]
by (intro nn_integral_cmult mult) (simp add: M)
also have "\<dots> = c * (integral\<^sup>N (join M) f)"
by (simp add: mult)
also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
- using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
+ using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)
finally show ?case by simp
next
case (add f g)
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x + g x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (\<integral>\<^sup>+ x. f x \<partial>M') + (\<integral>\<^sup>+ x. g x \<partial>M') \<partial>M)"
- using add M
- by (intro nn_integral_cong nn_integral_add)
- (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+ using add M M[THEN sets_eq_imp_space_eq]
+ by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)
also have "\<dots> = (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M) + (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. g x \<partial>M' \<partial>M)"
- using nn_integral_measurable_subprob_algebra[OF add(1,2)]
- using nn_integral_measurable_subprob_algebra[OF add(5,6)]
+ using nn_integral_measurable_subprob_algebra[OF add(1)]
+ using nn_integral_measurable_subprob_algebra[OF add(5)]
by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
by (simp add: add)
also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
- using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
+ using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)
finally show ?case by (simp add: ac_simps)
next
case (seq F)
have "(\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. (SUP i. F i) x \<partial>M' \<partial>M) = (\<integral>\<^sup>+ M'. (SUP i. \<integral>\<^sup>+ x. F i x \<partial>M') \<partial>M)"
- using seq M unfolding SUP_apply
+ using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply
by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
- (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
+ (auto simp add: space_subprob_algebra)
also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
- using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
+ using nn_integral_measurable_subprob_algebra[OF seq(1)] seq
by (intro nn_integral_monotone_convergence_SUP)
(simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
by (simp add: seq)
also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
- using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
+ using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
+ (simp_all add: M cong: measurable_cong_sets)
finally show ?case by (simp add: ac_simps)
qed
+lemma nn_integral_join:
+ assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)"
+ shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
+ apply (subst (1 3) nn_integral_max_0[symmetric])
+ apply (rule nn_integral_join')
+ apply (auto simp: f)
+ done
+
lemma join_assoc:
- assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
+ assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
shows "join (distr M (subprob_algebra N) join) = join (join M)"
proof (rule measure_eqI)
fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
@@ -671,8 +697,8 @@
show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
using measurable_join[of N]
by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
- sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
- intro!: nn_integral_cong emeasure_join cong: measurable_cong)
+ sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]
+ intro!: nn_integral_cong emeasure_join)
qed (simp add: M)
lemma join_return:
@@ -746,15 +772,15 @@
lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
by (simp add: bind_def)
-lemma sets_bind[simp]:
- assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+lemma sets_bind[simp, measurable_cong]:
+ assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}"
shows "sets (bind M f) = sets N"
- using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
+ using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq)
lemma space_bind[simp]:
- assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
+ assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}"
shows "space (bind M f) = space N"
- using assms by (intro sets_eq_imp_space_eq sets_bind)
+ using assms by (intro sets_eq_imp_space_eq sets_bind)
lemma bind_cong:
assumes "\<forall>x \<in> space M. f x = g x"
@@ -785,8 +811,8 @@
\<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
-lemma nn_integral_bind':
- assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
+lemma nn_integral_bind:
+ assumes f: "f \<in> borel_measurable B"
assumes N: "N \<in> measurable M (subprob_algebra B)"
shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
proof cases
@@ -795,15 +821,6 @@
by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
-lemma nn_integral_bind:
- assumes [measurable]: "f \<in> borel_measurable B"
- assumes N: "N \<in> measurable M (subprob_algebra B)"
- shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
- apply (subst (1 3) nn_integral_max_0[symmetric])
- apply (rule nn_integral_bind'[OF _ _ N])
- apply auto
- done
-
lemma AE_bind:
assumes P[measurable]: "Measurable.pred B P"
assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
@@ -813,21 +830,20 @@
unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
next
assume M: "space M \<noteq> {}"
+ note sets_kernel[OF N, simp]
have *: "(\<integral>\<^sup>+x. indicator {x. \<not> P x} x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. indicator {x\<in>space B. \<not> P x} x \<partial>(M \<guillemotright>= N))"
- by (intro nn_integral_cong) (simp add: space_bind[OF N M] split: split_indicator)
+ by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
have "(AE x in M \<guillemotright>= N. P x) \<longleftrightarrow> (\<integral>\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \<in> space B. \<not> P x}) \<partial>M) = 0"
- by (simp add: AE_iff_nn_integral sets_bind[OF N M] space_bind[OF N M] * nn_integral_bind[where B=B]
+ by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
del: nn_integral_indicator)
also have "\<dots> = (AE x in M. AE y in N x. P y)"
apply (subst nn_integral_0_iff_AE)
apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
apply measurable
apply (intro eventually_subst AE_I2)
- apply simp
- apply (subst nn_integral_0_iff_AE)
- apply (simp add: subprob_measurableD(3)[OF N])
- apply (auto simp add: ereal_indicator_le_0 subprob_measurableD(1)[OF N] intro!: eventually_subst)
+ apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N]
+ intro!: AE_iff_measurable[symmetric])
done
finally show ?thesis .
qed
@@ -852,7 +868,7 @@
done
qed
-lemma measurable_bind:
+lemma measurable_bind[measurable (raw)]:
assumes M1: "f \<in> measurable M (subprob_algebra N)" and
M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
@@ -881,7 +897,7 @@
proof
have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
by (subst emeasure_bind[where N=S])
- (auto simp: not_empty space_bind[OF N] subprob_measurableD[OF N] intro!: nn_integral_cong)
+ (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
@@ -890,7 +906,7 @@
lemma (in subprob_space) bind_in_space:
"A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
- by (auto simp add: space_subprob_algebra subprob_not_empty intro!: subprob_space_bind)
+ by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
unfold_locales
lemma (in subprob_space) measure_bind:
@@ -1001,18 +1017,22 @@
assumes X[simp]: "X \<in> sets K" "X \<noteq> {}"
shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)"
proof (rule measure_eqI)
+ note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp]
+ note N_space = sets_eq_imp_space_eq[OF N_sets, simp]
+ show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))"
+ by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]])
fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
with X have "A \<in> sets K" "A \<subseteq> X"
- by (auto simp: sets_restrict_space sets_bind[OF assms(1,2)])
+ by (auto simp: sets_restrict_space)
then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
using assms
apply (subst emeasure_restrict_space)
- apply (simp_all add: space_bind[OF assms(1,2)] sets_bind[OF assms(1,2)] emeasure_bind[OF assms(2,1)])
+ apply (simp_all add: emeasure_bind[OF assms(2,1)])
apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]])
apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra
intro!: nn_integral_cong dest!: measurable_space)
done
-qed (simp add: sets_restrict_space sets_bind[OF assms(1,2)] sets_bind[OF restrict_space_measurable[OF assms(4,3,1)] assms(2)])
+qed
lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
by (intro measure_eqI)
@@ -1085,20 +1105,19 @@
finally show ?thesis ..
qed
+lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)"
+ by (simp add: space_subprob_algebra) unfold_locales
+
lemma (in pair_prob_space) pair_measure_eq_bind:
"(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
proof (rule measure_eqI)
have ps_M2: "prob_space M2" by unfold_locales
note return_measurable[measurable]
- have 1: "(\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))) \<in> measurable M1 (subprob_algebra (M1 \<Otimes>\<^sub>M M2))"
- by (auto simp add: space_subprob_algebra ps_M2
- intro!: measurable_bind[where N=M2] measurable_const prob_space_imp_subprob_space)
show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
- by (simp add: M1.not_empty sets_bind[OF 1])
+ by (simp_all add: M1.not_empty M2.not_empty)
fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
show "emeasure (M1 \<Otimes>\<^sub>M M2) A = emeasure (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y)))) A"
- by (auto simp: M2.emeasure_pair_measure emeasure_bind[OF _ 1] M1.not_empty
- emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] M2.not_empty
+ by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"]
intro!: nn_integral_cong)
qed
--- a/src/HOL/Probability/Lebesgue_Measure.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Mon Nov 24 12:20:14 2014 +0100
@@ -300,7 +300,7 @@
emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)"
using emeasure_interval_measure_Ioc[of a b F] by auto
-lemma sets_interval_measure [simp]: "sets (interval_measure F) = sets borel"
+lemma sets_interval_measure [simp, measurable_cong]: "sets (interval_measure F) = sets borel"
apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
apply (rule sigma_sets_eqI)
apply auto
@@ -367,7 +367,7 @@
"lborel = distr (\<Pi>\<^sub>M b\<in>Basis. interval_measure (\<lambda>x. x)) borel (\<lambda>f. \<Sum>b\<in>Basis. f b *\<^sub>R b)"
lemma
- shows sets_lborel[simp]: "sets lborel = sets borel"
+ shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
and space_lborel[simp]: "space lborel = space borel"
and measurable_lborel1[simp]: "measurable M lborel = measurable M borel"
and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
--- a/src/HOL/Probability/Measurable.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy Mon Nov 24 12:20:14 2014 +0100
@@ -61,10 +61,13 @@
*} "declaration of measurability theorems"
attribute_setup measurable_dest = Measurable.dest_thm_attr
- "add dest rule for measurability prover"
+ "add dest rule to measurability prover"
attribute_setup measurable_app = Measurable.app_thm_attr
- "add application rule for measurability prover"
+ "add application rule to measurability prover"
+
+attribute_setup measurable_cong = Measurable.cong_thm_attr
+ "add congurence rules to measurability prover"
method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
"measurability prover"
@@ -72,7 +75,7 @@
simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
setup {*
- Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of)
+ Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
*}
declare
@@ -90,12 +93,15 @@
declare
measurable_count_space[measurable (raw)]
measurable_ident[measurable (raw)]
- measurable_ident_sets[measurable (raw)]
+ measurable_id[measurable (raw)]
measurable_const[measurable (raw)]
measurable_If[measurable (raw)]
measurable_comp[measurable (raw)]
measurable_sets[measurable (raw)]
+declare measurable_cong_sets[measurable_cong]
+declare sets_restrict_space_cong[measurable_cong]
+
lemma predE[measurable (raw)]:
"pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
unfolding pred_def .
@@ -589,3 +595,4 @@
hide_const (open) pred
end
+
--- a/src/HOL/Probability/Measure_Space.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Mon Nov 24 12:20:14 2014 +0100
@@ -1180,7 +1180,7 @@
"distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
lemma
- shows sets_distr[simp]: "sets (distr M N f) = sets N"
+ shows sets_distr[simp, measurable_cong]: "sets (distr M N f) = sets N"
and space_distr[simp]: "space (distr M N f) = space N"
by (auto simp: distr_def)
--- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy Mon Nov 24 12:20:14 2014 +0100
@@ -1971,7 +1971,7 @@
"density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)"
lemma
- shows sets_density[simp]: "sets (density M f) = sets M"
+ shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M"
and space_density[simp]: "space (density M f) = space M"
by (auto simp: density_def)
@@ -2204,6 +2204,9 @@
and sets_point_measure: "sets (point_measure A f) = Pow A"
by (auto simp: point_measure_def)
+lemma sets_point_measure_count_space[measurable_cong]: "sets (point_measure A f) = sets (count_space A)"
+ by (simp add: sets_point_measure)
+
lemma measurable_point_measure_eq1[simp]:
"g \<in> measurable (point_measure A f) M \<longleftrightarrow> g \<in> A \<rightarrow> space M"
unfolding point_measure_def by simp
@@ -2272,7 +2275,7 @@
definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
lemma
- shows sets_uniform_measure[simp]: "sets (uniform_measure M A) = sets M"
+ shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M"
and space_uniform_measure[simp]: "space (uniform_measure M A) = space M"
by (auto simp: uniform_measure_def)
@@ -2356,6 +2359,10 @@
shows space_uniform_count_measure: "space (uniform_count_measure A) = A"
and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A"
unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure)
+
+lemma sets_uniform_count_measure_count_space[measurable_cong]:
+ "sets (uniform_count_measure A) = sets (count_space A)"
+ by (simp add: sets_uniform_count_measure)
lemma emeasure_uniform_count_measure:
"finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (uniform_count_measure A) X = card X / card A"
--- a/src/HOL/Probability/Probability_Mass_Function.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Mon Nov 24 12:20:14 2014 +0100
@@ -98,6 +98,9 @@
interpretation measure_pmf!: subprob_space "measure_pmf M" for M
by (rule prob_space_imp_subprob_space) unfold_locales
+lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
+ by unfold_locales
+
locale pmf_as_measure
begin
@@ -141,12 +144,16 @@
lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
by transfer metis
-lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)"
+lemma sets_measure_pmf_count_space[measurable_cong]:
+ "sets (measure_pmf M) = sets (count_space UNIV)"
by simp
lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
+lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
+ by (simp add: space_subprob_algebra subprob_space_measure_pmf)
+
lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N"
by (auto simp: measurable_def)
@@ -555,11 +562,11 @@
shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
proof (rule measure_eqI)
show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
- using assms by (subst (1 2) sets_bind) auto
+ using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
next
fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
then have X: "X \<in> sets N"
- using assms by (subst (asm) sets_bind) auto
+ using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
using assms
by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
@@ -575,21 +582,19 @@
proof (intro conjI)
fix M :: "'a pmf pmf"
- have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))"
- using measurable_measure_pmf[of "\<lambda>x. x"] by simp
-
interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf"
- apply (rule measure_pmf.prob_space_bind[OF _ *])
- apply (auto intro!: AE_I2)
+ apply (intro measure_pmf.prob_space_bind[where S="count_space UNIV"] AE_I2)
+ apply (auto intro!: subprob_space_measure_pmf simp: space_subprob_algebra)
apply unfold_locales
done
show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)"
by intro_locales
show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV"
- by (subst sets_bind[OF *]) auto
+ by (subst sets_bind) auto
have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
- by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *]
- nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
+ by (auto simp: AE_bind[where B="count_space UNIV"] measure_pmf_in_subprob_algebra
+ emeasure_bind[where N="count_space UNIV"] AE_measure_pmf_iff nn_integral_0_iff_AE
+ measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
unfolding bind.emeasure_eq_measure by simp
qed
@@ -772,6 +777,10 @@
lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
+lemma measure_pmf_in_subprob_space[measurable (raw)]:
+ "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
+ by (simp add: space_subprob_algebra) intro_locales
+
lemma bind_pair_pmf:
assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
@@ -780,46 +789,25 @@
have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
using M[THEN measurable_space] by (simp_all add: space_pair_measure)
+ note measurable_bind[where N="count_space UNIV", measurable]
+ note measure_pmf_in_subprob_space[simp]
+
have sets_eq_N: "sets ?L = N"
- by (simp add: sets_bind[OF M'])
+ by (subst sets_bind[OF sets_kernel[OF M']]) auto
show "sets ?L = sets ?R"
- unfolding sets_eq_N
- apply (subst sets_bind[where N=N])
- apply (rule measurable_bind)
- apply (rule measurable_compose[OF _ measurable_measure_pmf])
- apply measurable
- apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space)
- done
+ using measurable_space[OF M]
+ by (simp add: sets_eq_N space_pair_measure space_subprob_algebra)
fix X assume "X \<in> sets ?L"
then have X[measurable]: "X \<in> sets N"
unfolding sets_eq_N .
then show "emeasure ?L X = emeasure ?R X"
apply (simp add: emeasure_bind[OF _ M' X])
- unfolding pair_pmf_def measure_pmf_bind[of A]
- apply (subst nn_integral_bind)
- apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
- apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
- apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
- apply measurable
- unfolding measure_pmf_bind
- apply (subst nn_integral_bind)
- apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
- apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
- apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
+ apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
+ nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
+ apply (subst emeasure_bind[OF _ _ X])
apply measurable
- apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
apply (subst emeasure_bind[OF _ _ X])
- apply simp
- apply (rule measurable_bind[where N="count_space UNIV"])
- apply (rule measurable_compose[OF _ measurable_measure_pmf])
apply measurable
- apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+
- apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl])
- apply simp
- apply (subst emeasure_bind[OF _ _ X])
- apply simp
- apply (rule measurable_compose[OF _ M])
- apply (auto simp: space_pair_measure)
done
qed
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Sigma_Algebra.thy Mon Nov 24 12:20:14 2014 +0100
@@ -1933,12 +1933,6 @@
f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
by (metis measurable_cong)
-lemma measurable_eqI:
- "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
- sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
- \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
- by (simp add: measurable_def sigma_algebra_iff2)
-
lemma measurable_compose:
assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
shows "(\<lambda>x. g (f x)) \<in> measurable M L"
@@ -1990,6 +1984,9 @@
lemma measurable_ident: "id \<in> measurable M M"
by (auto simp add: measurable_def)
+lemma measurable_id: "(\<lambda>x. x) \<in> measurable M M"
+ by (simp add: measurable_def)
+
lemma measurable_ident_sets:
assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
using measurable_ident[of M]
--- a/src/HOL/Probability/Stream_Space.thy Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/Stream_Space.thy Mon Nov 24 12:20:14 2014 +0100
@@ -41,7 +41,8 @@
lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
unfolding stream_space_def by (rule distr_cong) auto
-lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
+lemma sets_stream_space_cong[measurable_cong]:
+ "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"
--- a/src/HOL/Probability/measurable.ML Mon Nov 24 12:20:35 2014 +0100
+++ b/src/HOL/Probability/measurable.ML Mon Nov 24 12:20:14 2014 +0100
@@ -6,44 +6,66 @@
signature MEASURABLE =
sig
+ type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
+
datatype level = Concrete | Generic
val app_thm_attr : attribute context_parser
val dest_thm_attr : attribute context_parser
+ val cong_thm_attr : attribute context_parser
val measurable_thm_attr : bool * (bool * level) -> attribute
+ val add_del_cong_thm : bool -> thm -> Context.generic -> Context.generic ;
+
+ val get_all : Context.generic -> thm list
+ val get_dest : Context.generic -> thm list
+ val get_cong : Context.generic -> thm list
+
val measurable_tac : Proof.context -> thm list -> tactic
val simproc : Proof.context -> cterm -> thm option
- val get_thms : Proof.context -> thm list
- val get_all : Proof.context -> thm list
+ val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
+ val del_preprocessor : string -> Context.generic -> Context.generic
+ val add_local_cong : thm -> Proof.context -> Proof.context
end ;
structure Measurable : MEASURABLE =
struct
+type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
+
datatype level = Concrete | Generic;
fun eq_measurable_thms ((th1, d1), (th2, d2)) =
d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
+fun merge_dups (xs:(string * preprocessor) list) ys =
+ xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys)
+
structure Data = Generic_Data
(
type T = {
measurable_thms : (thm * (bool * level)) Item_Net.T,
dest_thms : thm Item_Net.T,
- app_thms : thm Item_Net.T }
+ app_thms : thm Item_Net.T,
+ cong_thms : thm Item_Net.T,
+ preprocessors : (string * preprocessor) list }
val empty = {
measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
dest_thms = Thm.full_rules,
- app_thms = Thm.full_rules };
+ app_thms = Thm.full_rules,
+ cong_thms = Thm.full_rules,
+ preprocessors = [] };
val extend = I;
- fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1 },
- {measurable_thms = t2, dest_thms = dt2, app_thms = at2 }) = {
+ fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1, cong_thms = ct1, preprocessors = i1 },
+ {measurable_thms = t2, dest_thms = dt2, app_thms = at2, cong_thms = ct2, preprocessors = i2 }) = {
measurable_thms = Item_Net.merge (t1, t2),
dest_thms = Item_Net.merge (dt1, dt2),
- app_thms = Item_Net.merge (at1, at2) };
+ app_thms = Item_Net.merge (at1, at2),
+ cong_thms = Item_Net.merge (ct1, ct2),
+ preprocessors = merge_dups i1 i2
+ };
);
val debug =
@@ -52,13 +74,15 @@
val split =
Attrib.setup_config_bool @{binding measurable_split} (K true)
-fun map_data f1 f2 f3
- {measurable_thms = t1, dest_thms = t2, app_thms = t3} =
- {measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3 }
+fun map_data f1 f2 f3 f4 f5
+ {measurable_thms = t1, dest_thms = t2, app_thms = t3, cong_thms = t4, preprocessors = t5 } =
+ {measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3, cong_thms = f4 t4, preprocessors = f5 t5}
-fun map_measurable_thms f = map_data f I I
-fun map_dest_thms f = map_data I f I
-fun map_app_thms f = map_data I I f
+fun map_measurable_thms f = map_data f I I I I
+fun map_dest_thms f = map_data I f I I I
+fun map_app_thms f = map_data I I f I I
+fun map_cong_thms f = map_data I I I f I
+fun map_preprocessors f = map_data I I I I f
fun generic_add_del map =
Scan.lift
@@ -69,6 +93,8 @@
val dest_thm_attr = generic_add_del map_dest_thms
+val cong_thm_attr = generic_add_del map_cong_thms
+
fun del_thm th net =
let
val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
@@ -80,29 +106,30 @@
val get_dest = Item_Net.content o #dest_thms o Data.get;
val get_app = Item_Net.content o #app_thms o Data.get;
+val get_cong = Item_Net.content o #cong_thms o Data.get;
+val add_cong = Data.map o map_cong_thms o Item_Net.update;
+val del_cong = Data.map o map_cong_thms o Item_Net.remove;
+fun add_del_cong_thm true = add_cong
+ | add_del_cong_thm false = del_cong
+
+fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)]))
+fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name)))
+val add_local_cong = Context.proof_map o add_cong
+
+val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ;
+
fun is_too_generic thm =
let
val concl = concl_of thm
val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
in is_Var (head_of concl') end
-fun import_theorem ctxt thm = if is_too_generic thm then [] else
- [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
-
-val get = Context.Proof #> Data.get #> #measurable_thms #> Item_Net.content ;
-
-val get_all = get #> map fst ;
+val get_thms = Data.get #> #measurable_thms #> Item_Net.content ;
-fun get_thms ctxt =
- let
- val thms = ctxt |> get |> rev ;
- fun get lv = map_filter (fn (th, (rw, lv')) => if lv = lv' then SOME (th, rw) else NONE) thms
- in
- get Concrete @ get Generic |>
- maps (fn (th, rw) => if rw then [th] else import_theorem (Context.Proof ctxt) th)
- end;
+val get_all = get_thms #> map fst ;
-fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
+fun debug_tac ctxt msg f =
+ if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
fun nth_hol_goal thm i =
HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
@@ -112,7 +139,7 @@
(Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
| _ => raise (TERM ("not a measurability predicate", [t])))
-fun is_cond_formula n thm = if length (prems_of thm) < n then false else
+fun not_measurable_prop n thm = if length (prems_of thm) < n then false else
(case nth_hol_goal thm n of
(Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
| (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
@@ -148,73 +175,118 @@
end
| cnt_prefixes _ _ = []
-val split_countable_tac =
- Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
- let
- val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
- fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
- fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
- val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
- in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
- handle TERM _ => no_tac) 1)
-
-val split_app_tac =
- Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
- let
- fun app_prefixes (Abs (n, T, (f $ g))) = let
- val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
- in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
- | app_prefixes _ = []
-
- fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
- | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
- val thy = Proof_Context.theory_of ctxt
- val tunify = Sign.typ_unify thy
- val thms = map
- (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
- (get_app (Context.Proof ctxt))
- fun cert f = map (fn (t, t') => (f thy t, f thy t'))
- fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
- let
- val inst =
- (Vartab.empty, ~1)
- |> tunify (T, thmT)
- |> tunify (Tf, thmTf)
- |> tunify (Tc, thmTc)
- |> Vartab.dest o fst
- val subst = subst_TVars (map (apsnd snd) inst)
- in
- Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
- cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
- end
- val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
- in if null cps then no_tac
- else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
- ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
- handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
- handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
-
fun measurable_tac ctxt facts =
let
- val imported_thms =
- (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_thms ctxt
+ fun debug_fact msg thm () =
+ msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (prop_of thm))
+
+ fun IF' c t i = COND (c i) (t i) no_tac
+
+ fun r_tac msg =
+ if Config.get ctxt debug
+ then FIRST' o
+ map (fn thm => resolve_tac [thm]
+ THEN' K (debug_tac ctxt (debug_fact (msg ^ "resolved using") thm) all_tac))
+ else resolve_tac
+
+ val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
+
+ val dests = get_dest (Context.Proof ctxt)
+ fun prep_dest thm =
+ (if is_too_generic thm then [] else [thm] @ map_filter (try (fn th' => thm RS th')) dests) ;
+ val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ;
+ fun preprocess_thm (thm, raw) =
+ if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat
+
+ fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ;
+ fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ;
+ val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic
+
+ val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat
- fun debug_facts msg () =
- msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
- (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
+ fun is_sets_eq (Const (@{const_name "HOL.eq"}, _) $
+ (Const (@{const_name "sets"}, _) $ _) $
+ (Const (@{const_name "sets"}, _) $ _)) = true
+ | is_sets_eq (Const (@{const_name "HOL.eq"}, _) $
+ (Const (@{const_name "measurable"}, _) $ _ $ _) $
+ (Const (@{const_name "measurable"}, _) $ _ $ _)) = true
+ | is_sets_eq _ = false
+
+ val cong_thms = get_cong (Context.Proof ctxt) @
+ filter (fn thm => concl_of thm |> HOLogic.dest_Trueprop |> is_sets_eq handle TERM _ => false) facts
+
+ fun sets_cong_tac i =
+ Subgoal.FOCUS (fn {context = ctxt', prems = prems, ...} => (
+ let
+ val ctxt'' = Simplifier.add_prems prems ctxt'
+ in
+ r_tac "cong intro" [elem_congI]
+ THEN' SOLVED' (fn i => REPEAT_DETERM (
+ ((r_tac "cong solve" (cong_thms @ [@{thm refl}])
+ ORELSE' IF' (fn i => fn thm => nprems_of thm > i)
+ (SOLVED' (asm_full_simp_tac ctxt''))) i)))
+ end) 1) ctxt i
+ THEN flexflex_tac ctxt
+
+ val simp_solver_tac =
+ IF' not_measurable_prop (debug_tac ctxt (K "simp ") o SOLVED' (asm_full_simp_tac ctxt))
+
+ val split_countable_tac =
+ Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+ let
+ val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
+ fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
+ fun inst (ts, Ts) =
+ Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) @{thm measurable_compose_countable}
+ in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
+ handle TERM _ => no_tac) 1)
val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
- fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
+ val split_app_tac =
+ Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
+ let
+ fun app_prefixes (Abs (n, T, (f $ g))) = let
+ val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
+ in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
+ | app_prefixes _ = []
+
+ fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
+ | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
+ val thy = Proof_Context.theory_of ctxt
+ val tunify = Sign.typ_unify thy
+ val thms = map
+ (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
+ (get_app (Context.Proof ctxt))
+ fun cert f = map (fn (t, t') => (f thy t, f thy t'))
+ fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
+ let
+ val inst =
+ (Vartab.empty, ~1)
+ |> tunify (T, thmT)
+ |> tunify (Tf, thmTf)
+ |> tunify (Tc, thmTc)
+ |> Vartab.dest o fst
+ val subst = subst_TVars (map (apsnd snd) inst)
+ in
+ Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
+ cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
+ end
+ val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
+ in if null cps then no_tac
+ else r_tac "split app" cps i ORELSE debug_tac ctxt (fn () => "split app fun FAILED") no_tac end
+ handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
+ handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
- val depth_measurable_tac = REPEAT_cnt (fn n =>
- (COND (is_cond_formula 1)
- (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ctxt) 1))
- ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
- (split_app_tac ctxt 1) APPEND
- (splitter 1)))) 0
+ val single_step_tac =
+ simp_solver_tac
+ ORELSE' r_tac "step" thms
+ ORELSE' (split_app_tac ctxt)
+ ORELSE' splitter
+ ORELSE' (CHANGED o sets_cong_tac)
+ ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac))
- in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
+ in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end;
fun simproc ctxt redex =
let