add congruence solver to measurability prover
authorhoelzl
Mon Nov 24 12:20:14 2014 +0100 (2014-11-24)
changeset 590487dc8ac6f0895
parent 59047 8d7cec9b861d
child 59049 0d1bfc982501
child 59050 376446e98951
add congruence solver to measurability prover
src/HOL/Probability/Binary_Product_Measure.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Probability/Convolution.thy
src/HOL/Probability/Fin_Map.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Giry_Monad.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measurable.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy
src/HOL/Probability/Probability_Mass_Function.thy
src/HOL/Probability/Sigma_Algebra.thy
src/HOL/Probability/Stream_Space.thy
src/HOL/Probability/measurable.ML
     1.1 --- a/src/HOL/Probability/Binary_Product_Measure.thy	Mon Nov 24 12:20:35 2014 +0100
     1.2 +++ b/src/HOL/Probability/Binary_Product_Measure.thy	Mon Nov 24 12:20:14 2014 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4    shows "sets (A \<Otimes>\<^sub>M B) \<subseteq> sets N"
     1.5    using assms by (auto intro!: sets.sigma_sets_subset simp: sets_pair_measure N)
     1.6  
     1.7 -lemma sets_pair_measure_cong[cong]:
     1.8 +lemma sets_pair_measure_cong[measurable_cong, cong]:
     1.9    "sets M1 = sets M1' \<Longrightarrow> sets M2 = sets M2' \<Longrightarrow> sets (M1 \<Otimes>\<^sub>M M2) = sets (M1' \<Otimes>\<^sub>M M2')"
    1.10    unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq)
    1.11  
     2.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Mon Nov 24 12:20:35 2014 +0100
     2.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Nov 24 12:20:14 2014 +0100
     2.3 @@ -2330,7 +2330,7 @@
     2.4  
     2.5  lemma tendsto_integral_at_top:
     2.6    fixes f :: "real \<Rightarrow> 'a::{banach, second_countable_topology}"
     2.7 -  assumes [simp]: "sets M = sets borel" and f[measurable]: "integrable M f"
     2.8 +  assumes [measurable_cong]: "sets M = sets borel" and f[measurable]: "integrable M f"
     2.9    shows "((\<lambda>y. \<integral> x. indicator {.. y} x *\<^sub>R f x \<partial>M) ---> \<integral> x. f x \<partial>M) at_top"
    2.10  proof (rule tendsto_at_topI_sequentially)
    2.11    fix X :: "nat \<Rightarrow> real" assume "filterlim X at_top sequentially"
     3.1 --- a/src/HOL/Probability/Convolution.thy	Mon Nov 24 12:20:35 2014 +0100
     3.2 +++ b/src/HOL/Probability/Convolution.thy	Mon Nov 24 12:20:14 2014 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5  lemma nn_integral_convolution:
     3.6    assumes "finite_measure M" "finite_measure N"
     3.7 -  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
     3.8 +  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
     3.9    assumes [measurable]: "f \<in> borel_measurable borel"
    3.10    shows "(\<integral>\<^sup>+x. f x \<partial>convolution M N) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f (x + y) \<partial>N \<partial>M)"
    3.11  proof -
    3.12 @@ -53,7 +53,7 @@
    3.13  
    3.14  lemma convolution_finite:
    3.15    assumes [simp]: "finite_measure M" "finite_measure N"
    3.16 -  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    3.17 +  assumes [measurable_cong]: "sets N = sets borel" "sets M = sets borel"
    3.18    shows "finite_measure (M \<star> N)"
    3.19    unfolding convolution_def
    3.20    by (intro finite_measure_pair_measure finite_measure.finite_measure_distr) auto
    3.21 @@ -71,7 +71,7 @@
    3.22  lemma convolution_emeasure_3':
    3.23    assumes [simp, measurable]:"A \<in> sets borel"
    3.24    assumes [simp]: "finite_measure M" "finite_measure N"  "finite_measure L"
    3.25 -  assumes [simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
    3.26 +  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel" "sets L = sets borel"
    3.27    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"
    3.28    apply (subst nn_integral_indicator[symmetric], simp)+
    3.29    apply (subst nn_integral_convolution)
    3.30 @@ -82,7 +82,7 @@
    3.31  
    3.32  lemma convolution_commutative:
    3.33    assumes [simp]: "finite_measure M" "finite_measure N"
    3.34 -  assumes [simp]: "sets N = sets borel" "sets M = sets borel"
    3.35 +  assumes [measurable_cong, simp]: "sets N = sets borel" "sets M = sets borel"
    3.36    shows "(M \<star> N) = (N \<star> M)"
    3.37  proof (rule measure_eqI)  
    3.38    interpret M: finite_measure M by fact
     4.1 --- a/src/HOL/Probability/Fin_Map.thy	Mon Nov 24 12:20:35 2014 +0100
     4.2 +++ b/src/HOL/Probability/Fin_Map.thy	Mon Nov 24 12:20:14 2014 +0100
     4.3 @@ -1311,7 +1311,7 @@
     4.4    assumes "X \<in> sets (PiF (Collect finite) (\<lambda>_. N))"
     4.5    shows "emeasure (mapmeasure M (\<lambda>_. N)) X = emeasure M ((fm -` X \<inter> extensional J))"
     4.6    using assms
     4.7 -  by (auto simp: measurable_eqI[OF s1 refl s2 refl] mapmeasure_def emeasure_distr
     4.8 +  by (auto simp: measurable_cong_sets[OF s2 refl] mapmeasure_def emeasure_distr
     4.9      fm_measurable space_PiM PiE_def)
    4.10  
    4.11  lemma mapmeasure_PiM:
    4.12 @@ -1322,7 +1322,7 @@
    4.13    assumes X: "X \<in> sets M"
    4.14    shows "emeasure M X = emeasure (mapmeasure M (\<lambda>_. N)) (fm ` X)"
    4.15    unfolding mapmeasure_def
    4.16 -proof (subst emeasure_distr, subst measurable_eqI[OF s1 refl s2 refl], rule fm_measurable)
    4.17 +proof (subst emeasure_distr, subst measurable_cong_sets[OF s2 refl], rule fm_measurable)
    4.18    have "X \<subseteq> space (Pi\<^sub>M J (\<lambda>_. N))" using assms by (simp add: sets.sets_into_space)
    4.19    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"
    4.20      by (auto simp: vimage_image_eq inj_on_def)
     5.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 24 12:20:35 2014 +0100
     5.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Mon Nov 24 12:20:14 2014 +0100
     5.3 @@ -369,7 +369,8 @@
     5.4    unfolding sets_PiM_single space[symmetric]
     5.5    by (intro sets.sigma_sets_subset subsetI) (auto intro: sets)
     5.6  
     5.7 -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)"
     5.8 +lemma sets_PiM_cong[measurable_cong]:
     5.9 +  assumes "I = J" "\<And>i. i \<in> J \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)"
    5.10    using assms sets_eq_imp_space_eq[OF assms(2)] by (simp add: sets_PiM_single cong: PiE_cong conj_cong)
    5.11  
    5.12  lemma sets_PiM_I:
    5.13 @@ -470,7 +471,7 @@
    5.14      "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
    5.15    shows "(\<lambda>x. case_nat (f x) (g x) i) \<in> measurable M N"
    5.16    by (cases i) simp_all
    5.17 -
    5.18 + 
    5.19  lemma measurable_case_nat'[measurable (raw)]:
    5.20    assumes fg[measurable]: "f \<in> measurable N M" "g \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
    5.21    shows "(\<lambda>x. case_nat (f x) (g x)) \<in> measurable N (\<Pi>\<^sub>M i\<in>UNIV. M)"
    5.22 @@ -885,6 +886,8 @@
    5.23    have eq: "\<And>x. x \<in> extensional {i} \<Longrightarrow> (\<lambda>j\<in>{i}. x i) = x"
    5.24      by (auto simp: extensional_def restrict_def)
    5.25  
    5.26 +  have [measurable]: "\<And>j. j \<in> {i} \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)" by simp
    5.27 +
    5.28    fix A assume A: "A \<in> sets ?P"
    5.29    then have "emeasure ?P A = (\<integral>\<^sup>+x. indicator A x \<partial>?P)" 
    5.30      by simp
     6.1 --- a/src/HOL/Probability/Giry_Monad.thy	Mon Nov 24 12:20:35 2014 +0100
     6.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Mon Nov 24 12:20:14 2014 +0100
     6.3 @@ -87,6 +87,25 @@
     6.4    using measurable_space[OF N x]
     6.5    by (auto simp: space_subprob_algebra intro!: measurable_cong_sets dest: sets_eq_imp_space_eq)
     6.6  
     6.7 +ML {*
     6.8 +
     6.9 +fun subprob_cong thm ctxt = (
    6.10 +  let
    6.11 +    val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
    6.12 +    val free = thm' |> concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
    6.13 +      dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
    6.14 +  in
    6.15 +    if free then ([], Measurable.add_local_cong (thm' RS @{thm subprob_measurableD(2)}) ctxt)
    6.16 +            else ([], ctxt)
    6.17 +  end
    6.18 +  handle THM _ => ([], ctxt) | TERM _ => ([], ctxt))
    6.19 +
    6.20 +*}
    6.21 +
    6.22 +setup \<open>
    6.23 +  Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong)
    6.24 +\<close>
    6.25 +
    6.26  context
    6.27    fixes K M N assumes K: "K \<in> measurable M (subprob_algebra N)"
    6.28  begin
    6.29 @@ -125,7 +144,7 @@
    6.30    ultimately show "space (subprob_algebra N) = {}" by (auto simp: space_subprob_algebra)
    6.31  qed
    6.32  
    6.33 -lemma nn_integral_measurable_subprob_algebra:
    6.34 +lemma nn_integral_measurable_subprob_algebra':
    6.35    assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
    6.36    shows "(\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)" (is "_ \<in> ?B")
    6.37    using f
    6.38 @@ -144,24 +163,30 @@
    6.39  next
    6.40    case (mult f c)
    6.41    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"
    6.42 -    by (intro measurable_cong nn_integral_cmult) (simp add: space_subprob_algebra)
    6.43 +    by (intro measurable_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
    6.44    ultimately show ?case
    6.45 +    using [[simp_trace_new]]
    6.46      by simp
    6.47  next
    6.48    case (add f g)
    6.49    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"
    6.50 -    by (intro measurable_cong nn_integral_add) (simp_all add: space_subprob_algebra)
    6.51 +    by (intro measurable_cong nn_integral_add) (auto simp add: space_subprob_algebra)
    6.52    ultimately show ?case
    6.53      by (simp add: ac_simps)
    6.54  next
    6.55    case (seq F)
    6.56    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"
    6.57      unfolding SUP_apply
    6.58 -    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (simp_all add: space_subprob_algebra)
    6.59 +    by (intro measurable_cong nn_integral_monotone_convergence_SUP) (auto simp add: space_subprob_algebra)
    6.60    ultimately show ?case
    6.61      by (simp add: ac_simps)
    6.62  qed
    6.63  
    6.64 +lemma nn_integral_measurable_subprob_algebra:
    6.65 +  "f \<in> borel_measurable N \<Longrightarrow> (\<lambda>M. integral\<^sup>N M f) \<in> borel_measurable (subprob_algebra N)"
    6.66 +  by (subst nn_integral_max_0[symmetric])
    6.67 +     (auto intro!: nn_integral_measurable_subprob_algebra')
    6.68 +
    6.69  lemma measurable_distr:
    6.70    assumes [measurable]: "f \<in> measurable M N"
    6.71    shows "(\<lambda>M'. distr M' N f) \<in> measurable (subprob_algebra M) (subprob_algebra N)"
    6.72 @@ -173,11 +198,12 @@
    6.73      then have "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M) \<longleftrightarrow>
    6.74        (\<lambda>M'. emeasure M' (f -` A \<inter> space M)) \<in> borel_measurable (subprob_algebra M)"
    6.75        by (intro measurable_cong)
    6.76 -         (auto simp: emeasure_distr space_subprob_algebra dest: sets_eq_imp_space_eq cong: measurable_cong)
    6.77 +         (auto simp: emeasure_distr space_subprob_algebra
    6.78 +               intro!: arg_cong2[where f=emeasure] sets_eq_imp_space_eq arg_cong2[where f="op \<inter>"])
    6.79      also have "\<dots>"
    6.80        using A by (intro measurable_emeasure_subprob_algebra) simp
    6.81      finally show "(\<lambda>M'. emeasure (distr M' N f) A) \<in> borel_measurable (subprob_algebra M)" .
    6.82 -  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty)
    6.83 +  qed (auto intro!: subprob_space.subprob_space_distr simp: space_subprob_algebra not_empty cong: measurable_cong_sets)
    6.84  qed (insert assms, auto simp: measurable_empty_iff space_subprob_algebra_empty_iff)
    6.85  
    6.86  lemma emeasure_space_subprob_algebra[measurable]:
    6.87 @@ -445,23 +471,17 @@
    6.88  qed
    6.89  
    6.90  lemma nn_integral_measurable_subprob_algebra2:
    6.91 -  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"
    6.92 +  assumes f[measurable]: "(\<lambda>(x, y). f x y) \<in> borel_measurable (M \<Otimes>\<^sub>M N)"
    6.93    assumes N[measurable]: "L \<in> measurable M (subprob_algebra N)"
    6.94    shows "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
    6.95  proof -
    6.96 +  note nn_integral_measurable_subprob_algebra[measurable]
    6.97 +  note measurable_distr2[measurable]
    6.98    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"
    6.99 -    apply (rule measurable_compose[OF _ nn_integral_measurable_subprob_algebra])
   6.100 -    apply (rule measurable_distr2)
   6.101 -    apply measurable
   6.102 -    apply (simp split: prod.split)
   6.103 -    done
   6.104 +    by measurable
   6.105    then show "(\<lambda>x. integral\<^sup>N (L x) (f x)) \<in> borel_measurable M"
   6.106 -    apply (rule measurable_cong[THEN iffD1, rotated])
   6.107 -    apply (subst nn_integral_distr)
   6.108 -    apply measurable
   6.109 -    apply (rule subprob_measurableD(2)[OF N], assumption)
   6.110 -    apply measurable
   6.111 -    done
   6.112 +    by (rule measurable_cong[THEN iffD1, rotated])
   6.113 +       (simp add: nn_integral_distr)
   6.114  qed
   6.115  
   6.116  lemma emeasure_measurable_subprob_algebra2:
   6.117 @@ -545,16 +565,14 @@
   6.118    by (simp_all add: join_def)
   6.119  
   6.120  lemma emeasure_join:
   6.121 -  assumes M[simp]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
   6.122 +  assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \<in> sets N"
   6.123    shows "emeasure (join M) A = (\<integral>\<^sup>+ M'. emeasure M' A \<partial>M)"
   6.124  proof (rule emeasure_measure_of[OF join_def])
   6.125 -  have eq: "borel_measurable M = borel_measurable (subprob_algebra N)"
   6.126 -    by auto
   6.127    show "countably_additive (sets (join M)) (\<lambda>B. \<integral>\<^sup>+ M'. emeasure M' B \<partial>M)"
   6.128    proof (rule countably_additiveI)
   6.129      fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (join M)" "disjoint_family A"
   6.130      have "(\<Sum>i. \<integral>\<^sup>+ M'. emeasure M' (A i) \<partial>M) = (\<integral>\<^sup>+M'. (\<Sum>i. emeasure M' (A i)) \<partial>M)"
   6.131 -      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra eq)
   6.132 +      using A by (subst nn_integral_suminf) (auto simp: measurable_emeasure_subprob_algebra)
   6.133      also have "\<dots> = (\<integral>\<^sup>+M'. emeasure M' (\<Union>i. A i) \<partial>M)"
   6.134      proof (rule nn_integral_cong)
   6.135        fix M' assume "M' \<in> space M"
   6.136 @@ -577,7 +595,7 @@
   6.137        by (intro emeasure_join) (auto simp: space_subprob_algebra `A\<in>sets N`)
   6.138    qed
   6.139    also have "(\<lambda>M'. \<integral>\<^sup>+M''. emeasure M'' A \<partial>M') \<in> ?B"
   6.140 -    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`] emeasure_nonneg[of _ A]
   6.141 +    using measurable_emeasure_subprob_algebra[OF `A\<in>sets N`]
   6.142      by (rule nn_integral_measurable_subprob_algebra)
   6.143    finally show "(\<lambda>M'. emeasure (join M') A) \<in> borel_measurable (subprob_algebra (subprob_algebra N))" .
   6.144  next
   6.145 @@ -596,8 +614,9 @@
   6.146    thus ?thesis by (simp add: measurable_empty_iff space_subprob_algebra_empty_iff)
   6.147  qed (auto simp: space_subprob_algebra)
   6.148  
   6.149 -lemma nn_integral_join:
   6.150 -  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x" and M: "sets M = sets (subprob_algebra N)"
   6.151 +lemma nn_integral_join':
   6.152 +  assumes f: "f \<in> borel_measurable N" "\<And>x. 0 \<le> f x"
   6.153 +    and M[measurable_cong]: "sets M = sets (subprob_algebra N)"
   6.154    shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
   6.155    using f
   6.156  proof induct
   6.157 @@ -619,51 +638,58 @@
   6.158  next
   6.159    case (mult f c)
   6.160    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)"
   6.161 -    using mult M
   6.162 -    by (intro nn_integral_cong nn_integral_cmult)
   6.163 -       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   6.164 +    using mult M M[THEN sets_eq_imp_space_eq]
   6.165 +    by (intro nn_integral_cong nn_integral_cmult) (auto simp add: space_subprob_algebra)
   6.166    also have "\<dots> = c * (\<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. f x \<partial>M' \<partial>M)"
   6.167 -    using nn_integral_measurable_subprob_algebra[OF mult(3,4)]
   6.168 +    using nn_integral_measurable_subprob_algebra[OF mult(3)]
   6.169      by (intro nn_integral_cmult mult) (simp add: M)
   6.170    also have "\<dots> = c * (integral\<^sup>N (join M) f)"
   6.171      by (simp add: mult)
   6.172    also have "\<dots> = (\<integral>\<^sup>+ x. c * f x \<partial>join M)"
   6.173 -    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M)
   6.174 +    using mult(2,3) by (intro nn_integral_cmult[symmetric] mult) (simp add: M cong: measurable_cong_sets)
   6.175    finally show ?case by simp
   6.176  next
   6.177    case (add f g)
   6.178    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)"
   6.179 -    using add M
   6.180 -    by (intro nn_integral_cong nn_integral_add)
   6.181 -       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   6.182 +    using add M M[THEN sets_eq_imp_space_eq]
   6.183 +    by (intro nn_integral_cong nn_integral_add) (auto simp add: space_subprob_algebra)
   6.184    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)"
   6.185 -    using nn_integral_measurable_subprob_algebra[OF add(1,2)]
   6.186 -    using nn_integral_measurable_subprob_algebra[OF add(5,6)]
   6.187 +    using nn_integral_measurable_subprob_algebra[OF add(1)]
   6.188 +    using nn_integral_measurable_subprob_algebra[OF add(5)]
   6.189      by (intro nn_integral_add add) (simp_all add: M nn_integral_nonneg)
   6.190    also have "\<dots> = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)"
   6.191      by (simp add: add)
   6.192    also have "\<dots> = (\<integral>\<^sup>+ x. f x + g x \<partial>join M)"
   6.193 -    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M)
   6.194 +    using add by (intro nn_integral_add[symmetric] add) (simp_all add: M cong: measurable_cong_sets)
   6.195    finally show ?case by (simp add: ac_simps)
   6.196  next
   6.197    case (seq F)
   6.198    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)"
   6.199 -    using seq M unfolding SUP_apply
   6.200 +    using seq M M[THEN sets_eq_imp_space_eq] unfolding SUP_apply
   6.201      by (intro nn_integral_cong nn_integral_monotone_convergence_SUP)
   6.202 -       (auto simp add: space_subprob_algebra cong: measurable_cong dest!: sets_eq_imp_space_eq)
   6.203 +       (auto simp add: space_subprob_algebra)
   6.204    also have "\<dots> = (SUP i. \<integral>\<^sup>+ M'. \<integral>\<^sup>+ x. F i x \<partial>M' \<partial>M)"
   6.205 -    using nn_integral_measurable_subprob_algebra[OF seq(1,2)] seq
   6.206 +    using nn_integral_measurable_subprob_algebra[OF seq(1)] seq
   6.207      by (intro nn_integral_monotone_convergence_SUP)
   6.208         (simp_all add: M nn_integral_nonneg incseq_nn_integral incseq_def le_fun_def nn_integral_mono )
   6.209    also have "\<dots> = (SUP i. integral\<^sup>N (join M) (F i))"
   6.210      by (simp add: seq)
   6.211    also have "\<dots> = (\<integral>\<^sup>+ x. (SUP i. F i x) \<partial>join M)"
   6.212 -    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq) (simp_all add: M)
   6.213 +    using seq by (intro nn_integral_monotone_convergence_SUP[symmetric] seq)
   6.214 +                 (simp_all add: M cong: measurable_cong_sets)
   6.215    finally show ?case by (simp add: ac_simps)
   6.216  qed
   6.217  
   6.218 +lemma nn_integral_join:
   6.219 +  assumes f[measurable]: "f \<in> borel_measurable N" "sets M = sets (subprob_algebra N)"
   6.220 +  shows "(\<integral>\<^sup>+x. f x \<partial>join M) = (\<integral>\<^sup>+M'. \<integral>\<^sup>+x. f x \<partial>M' \<partial>M)"
   6.221 +  apply (subst (1 3) nn_integral_max_0[symmetric])
   6.222 +  apply (rule nn_integral_join')
   6.223 +  apply (auto simp: f)
   6.224 +  done
   6.225 +
   6.226  lemma join_assoc:
   6.227 -  assumes M: "sets M = sets (subprob_algebra (subprob_algebra N))"
   6.228 +  assumes M[measurable_cong]: "sets M = sets (subprob_algebra (subprob_algebra N))"
   6.229    shows "join (distr M (subprob_algebra N) join) = join (join M)"
   6.230  proof (rule measure_eqI)
   6.231    fix A assume "A \<in> sets (join (distr M (subprob_algebra N) join))"
   6.232 @@ -671,8 +697,8 @@
   6.233    show "emeasure (join (distr M (subprob_algebra N) join)) A = emeasure (join (join M)) A"
   6.234      using measurable_join[of N]
   6.235      by (auto simp: M A nn_integral_distr emeasure_join measurable_emeasure_subprob_algebra emeasure_nonneg
   6.236 -                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ _ M]
   6.237 -             intro!: nn_integral_cong emeasure_join cong: measurable_cong)
   6.238 +                   sets_eq_imp_space_eq[OF M] space_subprob_algebra nn_integral_join[OF _ M]
   6.239 +             intro!: nn_integral_cong emeasure_join)
   6.240  qed (simp add: M)
   6.241  
   6.242  lemma join_return: 
   6.243 @@ -746,15 +772,15 @@
   6.244  lemma space_bind_empty: "space M = {} \<Longrightarrow> space (bind M f) = {}"
   6.245    by (simp add: bind_def)
   6.246  
   6.247 -lemma sets_bind[simp]: 
   6.248 -  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
   6.249 +lemma sets_bind[simp, measurable_cong]:
   6.250 +  assumes f: "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and M: "space M \<noteq> {}"
   6.251    shows "sets (bind M f) = sets N"
   6.252 -    using assms(2) by (force simp: bind_nonempty intro!: sets_kernel[OF assms(1) someI_ex])
   6.253 +  using f [of "SOME x. x \<in> space M"] by (simp add: bind_nonempty M some_in_eq)
   6.254  
   6.255  lemma space_bind[simp]: 
   6.256 -  assumes "f \<in> measurable M (subprob_algebra N)" and "space M \<noteq> {}"
   6.257 +  assumes "\<And>x. x \<in> space M \<Longrightarrow> sets (f x) = sets N" and "space M \<noteq> {}"
   6.258    shows "space (bind M f) = space N"
   6.259 -    using assms by (intro sets_eq_imp_space_eq sets_bind)
   6.260 +  using assms by (intro sets_eq_imp_space_eq sets_bind)
   6.261  
   6.262  lemma bind_cong: 
   6.263    assumes "\<forall>x \<in> space M. f x = g x"
   6.264 @@ -785,8 +811,8 @@
   6.265        \<Longrightarrow> emeasure (M \<guillemotright>= f) X = \<integral>\<^sup>+x. emeasure (f x) X \<partial>M"
   6.266    by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra)
   6.267  
   6.268 -lemma nn_integral_bind':
   6.269 -  assumes f: "f \<in> borel_measurable B" "\<And>x. 0 \<le> f x"
   6.270 +lemma nn_integral_bind:
   6.271 +  assumes f: "f \<in> borel_measurable B"
   6.272    assumes N: "N \<in> measurable M (subprob_algebra B)"
   6.273    shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   6.274  proof cases
   6.275 @@ -795,15 +821,6 @@
   6.276      by (rule nn_integral_distr[OF N nn_integral_measurable_subprob_algebra[OF f]])
   6.277  qed (simp add: bind_empty space_empty[of M] nn_integral_count_space)
   6.278  
   6.279 -lemma nn_integral_bind:
   6.280 -  assumes [measurable]: "f \<in> borel_measurable B"
   6.281 -  assumes N: "N \<in> measurable M (subprob_algebra B)"
   6.282 -  shows "(\<integral>\<^sup>+x. f x \<partial>(M \<guillemotright>= N)) = (\<integral>\<^sup>+x. \<integral>\<^sup>+y. f y \<partial>N x \<partial>M)"
   6.283 -  apply (subst (1 3) nn_integral_max_0[symmetric])
   6.284 -  apply (rule nn_integral_bind'[OF _ _ N])
   6.285 -  apply auto
   6.286 -  done
   6.287 -
   6.288  lemma AE_bind:
   6.289    assumes P[measurable]: "Measurable.pred B P"
   6.290    assumes N[measurable]: "N \<in> measurable M (subprob_algebra B)"
   6.291 @@ -813,21 +830,20 @@
   6.292      unfolding bind_empty[OF M] unfolding space_empty[OF M] by (simp add: AE_count_space)
   6.293  next
   6.294    assume M: "space M \<noteq> {}"
   6.295 +  note sets_kernel[OF N, simp]
   6.296    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))"
   6.297 -    by (intro nn_integral_cong) (simp add: space_bind[OF N M] split: split_indicator)
   6.298 +    by (intro nn_integral_cong) (simp add: space_bind[OF _ M] split: split_indicator)
   6.299  
   6.300    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"
   6.301 -    by (simp add: AE_iff_nn_integral sets_bind[OF N M] space_bind[OF N M] * nn_integral_bind[where B=B]
   6.302 +    by (simp add: AE_iff_nn_integral sets_bind[OF _ M] space_bind[OF _ M] * nn_integral_bind[where B=B]
   6.303               del: nn_integral_indicator)
   6.304    also have "\<dots> = (AE x in M. AE y in N x. P y)"
   6.305      apply (subst nn_integral_0_iff_AE)
   6.306      apply (rule measurable_compose[OF N nn_integral_measurable_subprob_algebra])
   6.307      apply measurable
   6.308      apply (intro eventually_subst AE_I2)
   6.309 -    apply simp
   6.310 -    apply (subst nn_integral_0_iff_AE)
   6.311 -    apply (simp add: subprob_measurableD(3)[OF N])
   6.312 -    apply (auto simp add: ereal_indicator_le_0 subprob_measurableD(1)[OF N] intro!: eventually_subst)
   6.313 +    apply (auto simp add: emeasure_le_0_iff subprob_measurableD(1)[OF N]
   6.314 +                intro!: AE_iff_measurable[symmetric])
   6.315      done
   6.316    finally show ?thesis .
   6.317  qed
   6.318 @@ -852,7 +868,7 @@
   6.319      done
   6.320  qed
   6.321  
   6.322 -lemma measurable_bind:
   6.323 +lemma measurable_bind[measurable (raw)]:
   6.324    assumes M1: "f \<in> measurable M (subprob_algebra N)" and
   6.325            M2: "(\<lambda>x. g (fst x) (snd x)) \<in> measurable (M \<Otimes>\<^sub>M N) (subprob_algebra R)"
   6.326    shows "(\<lambda>x. bind (f x) (g x)) \<in> measurable M (subprob_algebra R)"
   6.327 @@ -881,7 +897,7 @@
   6.328  proof
   6.329    have "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = (\<integral>\<^sup>+x. emeasure (N x) (space (N x)) \<partial>M)"
   6.330      by (subst emeasure_bind[where N=S])
   6.331 -       (auto simp: not_empty space_bind[OF N] subprob_measurableD[OF N] intro!: nn_integral_cong)
   6.332 +       (auto simp: not_empty space_bind[OF sets_kernel] subprob_measurableD[OF N] intro!: nn_integral_cong)
   6.333    also have "\<dots> = (\<integral>\<^sup>+x. 1 \<partial>M)"
   6.334      using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1)
   6.335    finally show "emeasure (M \<guillemotright>= N) (space (M \<guillemotright>= N)) = 1"
   6.336 @@ -890,7 +906,7 @@
   6.337  
   6.338  lemma (in subprob_space) bind_in_space:
   6.339    "A \<in> measurable M (subprob_algebra N) \<Longrightarrow> (M \<guillemotright>= A) \<in> space (subprob_algebra N)"
   6.340 -  by (auto simp add: space_subprob_algebra subprob_not_empty intro!: subprob_space_bind)
   6.341 +  by (auto simp add: space_subprob_algebra subprob_not_empty sets_kernel intro!: subprob_space_bind)
   6.342       unfold_locales
   6.343  
   6.344  lemma (in subprob_space) measure_bind:
   6.345 @@ -1001,18 +1017,22 @@
   6.346    assumes X[simp]: "X \<in> sets K" "X \<noteq> {}"
   6.347    shows "restrict_space (bind M N) X = bind M (\<lambda>x. restrict_space (N x) X)"
   6.348  proof (rule measure_eqI)
   6.349 +  note N_sets = sets_bind[OF sets_kernel[OF N] assms(2), simp]
   6.350 +  note N_space = sets_eq_imp_space_eq[OF N_sets, simp]
   6.351 +  show "sets (restrict_space (bind M N) X) = sets (bind M (\<lambda>x. restrict_space (N x) X))"
   6.352 +    by (simp add: sets_restrict_space assms(2) sets_bind[OF sets_kernel[OF restrict_space_measurable[OF assms(4,3,1)]]])
   6.353    fix A assume "A \<in> sets (restrict_space (M \<guillemotright>= N) X)"
   6.354    with X have "A \<in> sets K" "A \<subseteq> X"
   6.355 -    by (auto simp: sets_restrict_space sets_bind[OF assms(1,2)])
   6.356 +    by (auto simp: sets_restrict_space)
   6.357    then show "emeasure (restrict_space (M \<guillemotright>= N) X) A = emeasure (M \<guillemotright>= (\<lambda>x. restrict_space (N x) X)) A"
   6.358      using assms
   6.359      apply (subst emeasure_restrict_space)
   6.360 -    apply (simp_all add: space_bind[OF assms(1,2)] sets_bind[OF assms(1,2)] emeasure_bind[OF assms(2,1)])
   6.361 +    apply (simp_all add: emeasure_bind[OF assms(2,1)])
   6.362      apply (subst emeasure_bind[OF _ restrict_space_measurable[OF _ _ N]])
   6.363      apply (auto simp: sets_restrict_space emeasure_restrict_space space_subprob_algebra
   6.364                  intro!: nn_integral_cong dest!: measurable_space)
   6.365      done
   6.366 -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)])
   6.367 +qed
   6.368  
   6.369  lemma bind_const': "\<lbrakk>prob_space M; subprob_space N\<rbrakk> \<Longrightarrow> M \<guillemotright>= (\<lambda>x. N) = N"
   6.370    by (intro measure_eqI) 
   6.371 @@ -1085,20 +1105,19 @@
   6.372    finally show ?thesis ..
   6.373  qed
   6.374  
   6.375 +lemma (in prob_space) M_in_subprob[measurable (raw)]: "M \<in> space (subprob_algebra M)"
   6.376 +  by (simp add: space_subprob_algebra) unfold_locales
   6.377 +
   6.378  lemma (in pair_prob_space) pair_measure_eq_bind:
   6.379    "(M1 \<Otimes>\<^sub>M M2) = (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
   6.380  proof (rule measure_eqI)
   6.381    have ps_M2: "prob_space M2" by unfold_locales
   6.382    note return_measurable[measurable]
   6.383 -  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))"
   6.384 -    by (auto simp add: space_subprob_algebra ps_M2
   6.385 -             intro!: measurable_bind[where N=M2] measurable_const prob_space_imp_subprob_space)
   6.386    show "sets (M1 \<Otimes>\<^sub>M M2) = sets (M1 \<guillemotright>= (\<lambda>x. M2 \<guillemotright>= (\<lambda>y. return (M1 \<Otimes>\<^sub>M M2) (x, y))))"
   6.387 -    by (simp add: M1.not_empty sets_bind[OF 1])
   6.388 +    by (simp_all add: M1.not_empty M2.not_empty)
   6.389    fix A assume [measurable]: "A \<in> sets (M1 \<Otimes>\<^sub>M M2)"
   6.390    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"
   6.391 -    by (auto simp: M2.emeasure_pair_measure emeasure_bind[OF _ 1] M1.not_empty
   6.392 -                          emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"] M2.not_empty
   6.393 +    by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \<Otimes>\<^sub>M M2"]
   6.394               intro!: nn_integral_cong)
   6.395  qed
   6.396  
     7.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 24 12:20:35 2014 +0100
     7.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Mon Nov 24 12:20:14 2014 +0100
     7.3 @@ -300,7 +300,7 @@
     7.4      emeasure (interval_measure F) {a <.. b} = (if a \<le> b then F b - F a else 0)"
     7.5    using emeasure_interval_measure_Ioc[of a b F] by auto
     7.6  
     7.7 -lemma sets_interval_measure [simp]: "sets (interval_measure F) = sets borel"
     7.8 +lemma sets_interval_measure [simp, measurable_cong]: "sets (interval_measure F) = sets borel"
     7.9    apply (simp add: sets_extend_measure interval_measure_def borel_sigma_sets_Ioc)
    7.10    apply (rule sigma_sets_eqI)
    7.11    apply auto
    7.12 @@ -367,7 +367,7 @@
    7.13    "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)"
    7.14  
    7.15  lemma 
    7.16 -  shows sets_lborel[simp]: "sets lborel = sets borel"
    7.17 +  shows sets_lborel[simp, measurable_cong]: "sets lborel = sets borel"
    7.18      and space_lborel[simp]: "space lborel = space borel"
    7.19      and measurable_lborel1[simp]: "measurable M lborel = measurable M borel"
    7.20      and measurable_lborel2[simp]: "measurable lborel M = measurable borel M"
     8.1 --- a/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:20:35 2014 +0100
     8.2 +++ b/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:20:14 2014 +0100
     8.3 @@ -61,10 +61,13 @@
     8.4  *} "declaration of measurability theorems"
     8.5  
     8.6  attribute_setup measurable_dest = Measurable.dest_thm_attr
     8.7 -  "add dest rule for measurability prover"
     8.8 +  "add dest rule to measurability prover"
     8.9  
    8.10  attribute_setup measurable_app = Measurable.app_thm_attr
    8.11 -  "add application rule for measurability prover"
    8.12 +  "add application rule to measurability prover"
    8.13 +
    8.14 +attribute_setup measurable_cong = Measurable.cong_thm_attr
    8.15 +  "add congurence rules to measurability prover"
    8.16  
    8.17  method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
    8.18    "measurability prover"
    8.19 @@ -72,7 +75,7 @@
    8.20  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    8.21  
    8.22  setup {*
    8.23 -  Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all o Context.proof_of)
    8.24 +  Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all)
    8.25  *}
    8.26  
    8.27  declare
    8.28 @@ -90,12 +93,15 @@
    8.29  declare
    8.30    measurable_count_space[measurable (raw)]
    8.31    measurable_ident[measurable (raw)]
    8.32 -  measurable_ident_sets[measurable (raw)]
    8.33 +  measurable_id[measurable (raw)]
    8.34    measurable_const[measurable (raw)]
    8.35    measurable_If[measurable (raw)]
    8.36    measurable_comp[measurable (raw)]
    8.37    measurable_sets[measurable (raw)]
    8.38  
    8.39 +declare measurable_cong_sets[measurable_cong]
    8.40 +declare sets_restrict_space_cong[measurable_cong]
    8.41 +
    8.42  lemma predE[measurable (raw)]: 
    8.43    "pred M P \<Longrightarrow> {x\<in>space M. P x} \<in> sets M"
    8.44    unfolding pred_def .
    8.45 @@ -589,3 +595,4 @@
    8.46  hide_const (open) pred
    8.47  
    8.48  end
    8.49 +
     9.1 --- a/src/HOL/Probability/Measure_Space.thy	Mon Nov 24 12:20:35 2014 +0100
     9.2 +++ b/src/HOL/Probability/Measure_Space.thy	Mon Nov 24 12:20:14 2014 +0100
     9.3 @@ -1180,7 +1180,7 @@
     9.4    "distr M N f = measure_of (space N) (sets N) (\<lambda>A. emeasure M (f -` A \<inter> space M))"
     9.5  
     9.6  lemma
     9.7 -  shows sets_distr[simp]: "sets (distr M N f) = sets N"
     9.8 +  shows sets_distr[simp, measurable_cong]: "sets (distr M N f) = sets N"
     9.9      and space_distr[simp]: "space (distr M N f) = space N"
    9.10    by (auto simp: distr_def)
    9.11  
    10.1 --- a/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Nov 24 12:20:35 2014 +0100
    10.2 +++ b/src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy	Mon Nov 24 12:20:14 2014 +0100
    10.3 @@ -1971,7 +1971,7 @@
    10.4    "density M f = measure_of (space M) (sets M) (\<lambda>A. \<integral>\<^sup>+ x. f x * indicator A x \<partial>M)"
    10.5  
    10.6  lemma 
    10.7 -  shows sets_density[simp]: "sets (density M f) = sets M"
    10.8 +  shows sets_density[simp, measurable_cong]: "sets (density M f) = sets M"
    10.9      and space_density[simp]: "space (density M f) = space M"
   10.10    by (auto simp: density_def)
   10.11  
   10.12 @@ -2204,6 +2204,9 @@
   10.13      and sets_point_measure: "sets (point_measure A f) = Pow A"
   10.14    by (auto simp: point_measure_def)
   10.15  
   10.16 +lemma sets_point_measure_count_space[measurable_cong]: "sets (point_measure A f) = sets (count_space A)"
   10.17 +  by (simp add: sets_point_measure)
   10.18 +
   10.19  lemma measurable_point_measure_eq1[simp]:
   10.20    "g \<in> measurable (point_measure A f) M \<longleftrightarrow> g \<in> A \<rightarrow> space M"
   10.21    unfolding point_measure_def by simp
   10.22 @@ -2272,7 +2275,7 @@
   10.23  definition "uniform_measure M A = density M (\<lambda>x. indicator A x / emeasure M A)"
   10.24  
   10.25  lemma
   10.26 -  shows sets_uniform_measure[simp]: "sets (uniform_measure M A) = sets M"
   10.27 +  shows sets_uniform_measure[simp, measurable_cong]: "sets (uniform_measure M A) = sets M"
   10.28      and space_uniform_measure[simp]: "space (uniform_measure M A) = space M"
   10.29    by (auto simp: uniform_measure_def)
   10.30  
   10.31 @@ -2356,6 +2359,10 @@
   10.32    shows space_uniform_count_measure: "space (uniform_count_measure A) = A"
   10.33      and sets_uniform_count_measure: "sets (uniform_count_measure A) = Pow A"
   10.34      unfolding uniform_count_measure_def by (auto simp: space_point_measure sets_point_measure)
   10.35 +
   10.36 +lemma sets_uniform_count_measure_count_space[measurable_cong]:
   10.37 +  "sets (uniform_count_measure A) = sets (count_space A)"
   10.38 +  by (simp add: sets_uniform_count_measure)
   10.39   
   10.40  lemma emeasure_uniform_count_measure:
   10.41    "finite A \<Longrightarrow> X \<subseteq> A \<Longrightarrow> emeasure (uniform_count_measure A) X = card X / card A"
    11.1 --- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:35 2014 +0100
    11.2 +++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Nov 24 12:20:14 2014 +0100
    11.3 @@ -98,6 +98,9 @@
    11.4  interpretation measure_pmf!: subprob_space "measure_pmf M" for M
    11.5    by (rule prob_space_imp_subprob_space) unfold_locales
    11.6  
    11.7 +lemma subprob_space_measure_pmf: "subprob_space (measure_pmf x)"
    11.8 +  by unfold_locales
    11.9 +
   11.10  locale pmf_as_measure
   11.11  begin
   11.12  
   11.13 @@ -141,12 +144,16 @@
   11.14  lemma sets_measure_pmf[simp]: "sets (measure_pmf p) = UNIV"
   11.15    by transfer metis
   11.16  
   11.17 -lemma sets_measure_pmf_count_space: "sets (measure_pmf M) = sets (count_space UNIV)"
   11.18 +lemma sets_measure_pmf_count_space[measurable_cong]:
   11.19 +  "sets (measure_pmf M) = sets (count_space UNIV)"
   11.20    by simp
   11.21  
   11.22  lemma space_measure_pmf[simp]: "space (measure_pmf p) = UNIV"
   11.23    using sets_eq_imp_space_eq[of "measure_pmf p" "count_space UNIV"] by simp
   11.24  
   11.25 +lemma measure_pmf_in_subprob_algebra[measurable (raw)]: "measure_pmf x \<in> space (subprob_algebra (count_space UNIV))"
   11.26 +  by (simp add: space_subprob_algebra subprob_space_measure_pmf)
   11.27 +
   11.28  lemma measurable_pmf_measure1[simp]: "measurable (M :: 'a pmf) N = UNIV \<rightarrow> space N"
   11.29    by (auto simp: measurable_def)
   11.30  
   11.31 @@ -555,11 +562,11 @@
   11.32    shows "bind (measure_pmf x) A = bind (measure_pmf x) B"
   11.33  proof (rule measure_eqI)
   11.34    show "sets (measure_pmf x \<guillemotright>= A) = sets (measure_pmf x \<guillemotright>= B)"
   11.35 -    using assms by (subst (1 2) sets_bind) auto
   11.36 +    using assms by (subst (1 2) sets_bind) (auto simp: space_subprob_algebra)
   11.37  next
   11.38    fix X assume "X \<in> sets (measure_pmf x \<guillemotright>= A)"
   11.39    then have X: "X \<in> sets N"
   11.40 -    using assms by (subst (asm) sets_bind) auto
   11.41 +    using assms by (subst (asm) sets_bind) (auto simp: space_subprob_algebra)
   11.42    show "emeasure (measure_pmf x \<guillemotright>= A) X = emeasure (measure_pmf x \<guillemotright>= B) X"
   11.43      using assms
   11.44      by (subst (1 2) emeasure_bind[where N=N, OF _ _ X])
   11.45 @@ -575,21 +582,19 @@
   11.46  proof (intro conjI)
   11.47    fix M :: "'a pmf pmf"
   11.48  
   11.49 -  have *: "measure_pmf \<in> measurable (measure_pmf M) (subprob_algebra (count_space UNIV))"
   11.50 -    using measurable_measure_pmf[of "\<lambda>x. x"] by simp
   11.51 -  
   11.52    interpret bind: prob_space "measure_pmf M \<guillemotright>= measure_pmf"
   11.53 -    apply (rule measure_pmf.prob_space_bind[OF _ *])
   11.54 -    apply (auto intro!: AE_I2)
   11.55 +    apply (intro measure_pmf.prob_space_bind[where S="count_space UNIV"] AE_I2)
   11.56 +    apply (auto intro!: subprob_space_measure_pmf simp: space_subprob_algebra)
   11.57      apply unfold_locales
   11.58      done
   11.59    show "prob_space (measure_pmf M \<guillemotright>= measure_pmf)"
   11.60      by intro_locales
   11.61    show "sets (measure_pmf M \<guillemotright>= measure_pmf) = UNIV"
   11.62 -    by (subst sets_bind[OF *]) auto
   11.63 +    by (subst sets_bind) auto
   11.64    have "AE x in measure_pmf M \<guillemotright>= measure_pmf. emeasure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
   11.65 -    by (auto simp add: AE_bind[OF _ *] AE_measure_pmf_iff emeasure_bind[OF _ *]
   11.66 -        nn_integral_0_iff_AE measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
   11.67 +    by (auto simp: AE_bind[where B="count_space UNIV"] measure_pmf_in_subprob_algebra
   11.68 +                   emeasure_bind[where N="count_space UNIV"] AE_measure_pmf_iff nn_integral_0_iff_AE
   11.69 +                   measure_pmf.emeasure_eq_measure measure_le_0_iff set_pmf_iff pmf.rep_eq)
   11.70    then show "AE x in measure_pmf M \<guillemotright>= measure_pmf. measure (measure_pmf M \<guillemotright>= measure_pmf) {x} \<noteq> 0"
   11.71      unfolding bind.emeasure_eq_measure by simp
   11.72  qed
   11.73 @@ -772,6 +777,10 @@
   11.74  lemma set_pair_pmf: "set_pmf (pair_pmf A B) = set_pmf A \<times> set_pmf B"
   11.75    unfolding pair_pmf_def set_bind_pmf set_return_pmf by auto
   11.76  
   11.77 +lemma measure_pmf_in_subprob_space[measurable (raw)]:
   11.78 +  "measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
   11.79 +  by (simp add: space_subprob_algebra) intro_locales
   11.80 +
   11.81  lemma bind_pair_pmf:
   11.82    assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
   11.83    shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
   11.84 @@ -780,46 +789,25 @@
   11.85    have M'[measurable]: "M \<in> measurable (pair_pmf A B) (subprob_algebra N)"
   11.86      using M[THEN measurable_space] by (simp_all add: space_pair_measure)
   11.87  
   11.88 +  note measurable_bind[where N="count_space UNIV", measurable]
   11.89 +  note measure_pmf_in_subprob_space[simp]
   11.90 +
   11.91    have sets_eq_N: "sets ?L = N"
   11.92 -    by (simp add: sets_bind[OF M'])
   11.93 +    by (subst sets_bind[OF sets_kernel[OF M']]) auto
   11.94    show "sets ?L = sets ?R"
   11.95 -    unfolding sets_eq_N
   11.96 -    apply (subst sets_bind[where N=N])
   11.97 -    apply (rule measurable_bind)
   11.98 -    apply (rule measurable_compose[OF _ measurable_measure_pmf])
   11.99 -    apply measurable
  11.100 -    apply (auto intro!: sets_pair_measure_cong sets_measure_pmf_count_space)
  11.101 -    done
  11.102 +    using measurable_space[OF M]
  11.103 +    by (simp add: sets_eq_N space_pair_measure space_subprob_algebra)
  11.104    fix X assume "X \<in> sets ?L"
  11.105    then have X[measurable]: "X \<in> sets N"
  11.106      unfolding sets_eq_N .
  11.107    then show "emeasure ?L X = emeasure ?R X"
  11.108      apply (simp add: emeasure_bind[OF _ M' X])
  11.109 -    unfolding pair_pmf_def measure_pmf_bind[of A]
  11.110 -    apply (subst nn_integral_bind)
  11.111 -    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
  11.112 -    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
  11.113 -    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
  11.114 -    apply measurable
  11.115 -    unfolding measure_pmf_bind
  11.116 -    apply (subst nn_integral_bind)
  11.117 -    apply (rule measurable_compose[OF M' measurable_emeasure_subprob_algebra, OF X])
  11.118 -    apply (subst measurable_cong_sets[OF sets_measure_pmf_count_space refl])
  11.119 -    apply (subst subprob_algebra_cong[OF sets_measure_pmf_count_space])
  11.120 +    apply (simp add: nn_integral_bind[where B="count_space UNIV"] pair_pmf_def measure_pmf_bind[of A]
  11.121 +      nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
  11.122 +    apply (subst emeasure_bind[OF _ _ X])
  11.123      apply measurable
  11.124 -    apply (simp add: nn_integral_measure_pmf_finite set_return_pmf emeasure_nonneg pmf_return one_ereal_def[symmetric])
  11.125      apply (subst emeasure_bind[OF _ _ X])
  11.126 -    apply simp
  11.127 -    apply (rule measurable_bind[where N="count_space UNIV"])
  11.128 -    apply (rule measurable_compose[OF _ measurable_measure_pmf])
  11.129      apply measurable
  11.130 -    apply (rule sets_pair_measure_cong sets_measure_pmf_count_space refl)+
  11.131 -    apply (subst measurable_cong_sets[OF sets_pair_measure_cong[OF sets_measure_pmf_count_space refl] refl])
  11.132 -    apply simp
  11.133 -    apply (subst emeasure_bind[OF _ _ X])
  11.134 -    apply simp
  11.135 -    apply (rule measurable_compose[OF _ M])
  11.136 -    apply (auto simp: space_pair_measure)
  11.137      done
  11.138  qed
  11.139  
    12.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 24 12:20:35 2014 +0100
    12.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Mon Nov 24 12:20:14 2014 +0100
    12.3 @@ -1933,12 +1933,6 @@
    12.4      f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable N N'"
    12.5    by (metis measurable_cong)
    12.6  
    12.7 -lemma measurable_eqI:
    12.8 -     "\<lbrakk> space m1 = space m1' ; space m2 = space m2' ;
    12.9 -        sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk>
   12.10 -      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
   12.11 -  by (simp add: measurable_def sigma_algebra_iff2)
   12.12 -
   12.13  lemma measurable_compose:
   12.14    assumes f: "f \<in> measurable M N" and g: "g \<in> measurable N L"
   12.15    shows "(\<lambda>x. g (f x)) \<in> measurable M L"
   12.16 @@ -1990,6 +1984,9 @@
   12.17  lemma measurable_ident: "id \<in> measurable M M"
   12.18    by (auto simp add: measurable_def)
   12.19  
   12.20 +lemma measurable_id: "(\<lambda>x. x) \<in> measurable M M"
   12.21 +  by (simp add: measurable_def)
   12.22 +
   12.23  lemma measurable_ident_sets:
   12.24    assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
   12.25    using measurable_ident[of M]
    13.1 --- a/src/HOL/Probability/Stream_Space.thy	Mon Nov 24 12:20:35 2014 +0100
    13.2 +++ b/src/HOL/Probability/Stream_Space.thy	Mon Nov 24 12:20:14 2014 +0100
    13.3 @@ -41,7 +41,8 @@
    13.4  lemma stream_space_eq_distr: "stream_space M = distr (\<Pi>\<^sub>M i\<in>UNIV. M) (stream_space M) to_stream"
    13.5    unfolding stream_space_def by (rule distr_cong) auto
    13.6  
    13.7 -lemma sets_stream_space_cong: "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
    13.8 +lemma sets_stream_space_cong[measurable_cong]:
    13.9 +  "sets M = sets N \<Longrightarrow> sets (stream_space M) = sets (stream_space N)"
   13.10    using sets_eq_imp_space_eq[of M N] by (simp add: stream_space_def vimage_algebra_def cong: sets_PiM_cong)
   13.11  
   13.12  lemma measurable_snth_PiM: "(\<lambda>\<omega> n. \<omega> !! n) \<in> measurable (stream_space M) (\<Pi>\<^sub>M i\<in>UNIV. M)"
    14.1 --- a/src/HOL/Probability/measurable.ML	Mon Nov 24 12:20:35 2014 +0100
    14.2 +++ b/src/HOL/Probability/measurable.ML	Mon Nov 24 12:20:14 2014 +0100
    14.3 @@ -6,44 +6,66 @@
    14.4  
    14.5  signature MEASURABLE = 
    14.6  sig
    14.7 +  type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
    14.8 +
    14.9    datatype level = Concrete | Generic
   14.10  
   14.11    val app_thm_attr : attribute context_parser
   14.12    val dest_thm_attr : attribute context_parser
   14.13 +  val cong_thm_attr : attribute context_parser
   14.14    val measurable_thm_attr : bool * (bool * level) -> attribute
   14.15  
   14.16 +  val add_del_cong_thm : bool -> thm -> Context.generic -> Context.generic ;
   14.17 +
   14.18 +  val get_all : Context.generic -> thm list
   14.19 +  val get_dest : Context.generic -> thm list
   14.20 +  val get_cong : Context.generic -> thm list
   14.21 +
   14.22    val measurable_tac : Proof.context -> thm list -> tactic
   14.23  
   14.24    val simproc : Proof.context -> cterm -> thm option
   14.25  
   14.26 -  val get_thms : Proof.context -> thm list
   14.27 -  val get_all : Proof.context -> thm list
   14.28 +  val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
   14.29 +  val del_preprocessor : string -> Context.generic -> Context.generic
   14.30 +  val add_local_cong : thm -> Proof.context -> Proof.context
   14.31  end ;
   14.32  
   14.33  structure Measurable : MEASURABLE =
   14.34  struct
   14.35  
   14.36 +type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
   14.37 +
   14.38  datatype level = Concrete | Generic;
   14.39  
   14.40  fun eq_measurable_thms ((th1, d1), (th2, d2)) = 
   14.41    d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
   14.42  
   14.43 +fun merge_dups (xs:(string * preprocessor) list) ys =
   14.44 +  xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) 
   14.45 +
   14.46  structure Data = Generic_Data
   14.47  (
   14.48    type T = {
   14.49      measurable_thms : (thm * (bool * level)) Item_Net.T,
   14.50      dest_thms : thm Item_Net.T,
   14.51 -    app_thms : thm Item_Net.T }
   14.52 +    app_thms : thm Item_Net.T,
   14.53 +    cong_thms : thm Item_Net.T,
   14.54 +    preprocessors : (string * preprocessor) list }
   14.55    val empty = {
   14.56      measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
   14.57      dest_thms = Thm.full_rules,
   14.58 -    app_thms = Thm.full_rules };
   14.59 +    app_thms = Thm.full_rules,
   14.60 +    cong_thms = Thm.full_rules,
   14.61 +    preprocessors = [] };
   14.62    val extend = I;
   14.63 -  fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1 },
   14.64 -      {measurable_thms = t2, dest_thms = dt2, app_thms = at2 }) = {
   14.65 +  fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1, cong_thms = ct1, preprocessors = i1 },
   14.66 +      {measurable_thms = t2, dest_thms = dt2, app_thms = at2, cong_thms = ct2, preprocessors = i2 }) = {
   14.67      measurable_thms = Item_Net.merge (t1, t2),
   14.68      dest_thms = Item_Net.merge (dt1, dt2),
   14.69 -    app_thms = Item_Net.merge (at1, at2) };
   14.70 +    app_thms = Item_Net.merge (at1, at2),
   14.71 +    cong_thms = Item_Net.merge (ct1, ct2),
   14.72 +    preprocessors = merge_dups i1 i2 
   14.73 +    };
   14.74  );
   14.75  
   14.76  val debug =
   14.77 @@ -52,13 +74,15 @@
   14.78  val split =
   14.79    Attrib.setup_config_bool @{binding measurable_split} (K true)
   14.80  
   14.81 -fun map_data f1 f2 f3
   14.82 -  {measurable_thms = t1,    dest_thms = t2,    app_thms = t3} =
   14.83 -  {measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3 }
   14.84 +fun map_data f1 f2 f3 f4 f5
   14.85 +  {measurable_thms = t1,    dest_thms = t2,    app_thms = t3,    cong_thms = t4,    preprocessors = t5 } =
   14.86 +  {measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3, cong_thms = f4 t4, preprocessors = f5 t5}
   14.87  
   14.88 -fun map_measurable_thms f = map_data f I I
   14.89 -fun map_dest_thms f = map_data I f I
   14.90 -fun map_app_thms f = map_data I I f
   14.91 +fun map_measurable_thms f = map_data f I I I I
   14.92 +fun map_dest_thms f = map_data I f I I I
   14.93 +fun map_app_thms f = map_data I I f I I
   14.94 +fun map_cong_thms f = map_data I I I f I
   14.95 +fun map_preprocessors f = map_data I I I I f
   14.96  
   14.97  fun generic_add_del map = 
   14.98    Scan.lift
   14.99 @@ -69,6 +93,8 @@
  14.100  
  14.101  val dest_thm_attr = generic_add_del map_dest_thms
  14.102  
  14.103 +val cong_thm_attr = generic_add_del map_cong_thms
  14.104 +
  14.105  fun del_thm th net =
  14.106    let
  14.107      val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
  14.108 @@ -80,29 +106,30 @@
  14.109  val get_dest = Item_Net.content o #dest_thms o Data.get;
  14.110  val get_app = Item_Net.content o #app_thms o Data.get;
  14.111  
  14.112 +val get_cong = Item_Net.content o #cong_thms o Data.get;
  14.113 +val add_cong = Data.map o map_cong_thms o Item_Net.update;
  14.114 +val del_cong = Data.map o map_cong_thms o Item_Net.remove;
  14.115 +fun add_del_cong_thm true = add_cong
  14.116 +  | add_del_cong_thm false = del_cong
  14.117 +
  14.118 +fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)]))
  14.119 +fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name)))
  14.120 +val add_local_cong = Context.proof_map o add_cong
  14.121 +
  14.122 +val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ;
  14.123 +
  14.124  fun is_too_generic thm =
  14.125    let 
  14.126      val concl = concl_of thm
  14.127      val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
  14.128    in is_Var (head_of concl') end
  14.129  
  14.130 -fun import_theorem ctxt thm = if is_too_generic thm then [] else
  14.131 -  [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
  14.132 -
  14.133 -val get = Context.Proof #> Data.get #> #measurable_thms #> Item_Net.content ;
  14.134 -
  14.135 -val get_all = get #> map fst ;
  14.136 +val get_thms = Data.get #> #measurable_thms #> Item_Net.content ;
  14.137  
  14.138 -fun get_thms ctxt =
  14.139 -  let
  14.140 -    val thms = ctxt |> get |> rev ;
  14.141 -    fun get lv = map_filter (fn (th, (rw, lv')) => if lv = lv' then SOME (th, rw) else NONE) thms
  14.142 -  in
  14.143 -    get Concrete @ get Generic |>
  14.144 -    maps (fn (th, rw) => if rw then [th] else import_theorem (Context.Proof ctxt) th)
  14.145 -  end;
  14.146 +val get_all = get_thms #> map fst ;
  14.147  
  14.148 -fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
  14.149 +fun debug_tac ctxt msg f =
  14.150 +  if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
  14.151  
  14.152  fun nth_hol_goal thm i =
  14.153    HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
  14.154 @@ -112,7 +139,7 @@
  14.155      (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
  14.156    | _ => raise (TERM ("not a measurability predicate", [t])))
  14.157  
  14.158 -fun is_cond_formula n thm = if length (prems_of thm) < n then false else
  14.159 +fun not_measurable_prop n thm = if length (prems_of thm) < n then false else
  14.160    (case nth_hol_goal thm n of
  14.161      (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
  14.162    | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
  14.163 @@ -148,73 +175,118 @@
  14.164      end
  14.165    | cnt_prefixes _ _ = []
  14.166  
  14.167 -val split_countable_tac =
  14.168 -  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
  14.169 -    let
  14.170 -      val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
  14.171 -      fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
  14.172 -      fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
  14.173 -      val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
  14.174 -    in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
  14.175 -    handle TERM _ => no_tac) 1)
  14.176 -
  14.177 -val split_app_tac =
  14.178 -  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
  14.179 -    let
  14.180 -      fun app_prefixes (Abs (n, T, (f $ g))) = let
  14.181 -            val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
  14.182 -          in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
  14.183 -        | app_prefixes _ = []
  14.184 -
  14.185 -      fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
  14.186 -        | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
  14.187 -      val thy = Proof_Context.theory_of ctxt
  14.188 -      val tunify = Sign.typ_unify thy
  14.189 -      val thms = map
  14.190 -          (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
  14.191 -          (get_app (Context.Proof ctxt))
  14.192 -      fun cert f = map (fn (t, t') => (f thy t, f thy t'))
  14.193 -      fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
  14.194 -        let
  14.195 -          val inst =
  14.196 -            (Vartab.empty, ~1)
  14.197 -            |> tunify (T, thmT)
  14.198 -            |> tunify (Tf, thmTf)
  14.199 -            |> tunify (Tc, thmTc)
  14.200 -            |> Vartab.dest o fst
  14.201 -          val subst = subst_TVars (map (apsnd snd) inst)
  14.202 -        in
  14.203 -          Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
  14.204 -            cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
  14.205 -        end
  14.206 -      val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
  14.207 -    in if null cps then no_tac
  14.208 -        else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
  14.209 -          ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
  14.210 -    handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
  14.211 -    handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
  14.212 -
  14.213  fun measurable_tac ctxt facts =
  14.214    let
  14.215 -    val imported_thms =
  14.216 -      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_thms ctxt
  14.217 +    fun debug_fact msg thm () =
  14.218 +      msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (prop_of thm))
  14.219 +
  14.220 +    fun IF' c t i = COND (c i) (t i) no_tac
  14.221 +
  14.222 +    fun r_tac msg =
  14.223 +      if Config.get ctxt debug
  14.224 +      then FIRST' o
  14.225 +        map (fn thm => resolve_tac [thm]
  14.226 +          THEN' K (debug_tac ctxt (debug_fact (msg ^ "resolved using") thm) all_tac))
  14.227 +      else resolve_tac
  14.228 +
  14.229 +    val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
  14.230 +
  14.231 +    val dests = get_dest (Context.Proof ctxt)
  14.232 +    fun prep_dest thm =
  14.233 +      (if is_too_generic thm then [] else [thm] @ map_filter (try (fn th' => thm RS th')) dests) ;
  14.234 +    val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ;
  14.235 +    fun preprocess_thm (thm, raw) =
  14.236 +      if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat
  14.237 +    
  14.238 +    fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ;
  14.239 +    fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ;
  14.240 +    val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic
  14.241 +
  14.242 +    val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat
  14.243  
  14.244 -    fun debug_facts msg () =
  14.245 -      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
  14.246 -        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
  14.247 +    fun is_sets_eq (Const (@{const_name "HOL.eq"}, _) $
  14.248 +          (Const (@{const_name "sets"}, _) $ _) $
  14.249 +          (Const (@{const_name "sets"}, _) $ _)) = true
  14.250 +      | is_sets_eq (Const (@{const_name "HOL.eq"}, _) $
  14.251 +          (Const (@{const_name "measurable"}, _) $ _ $ _) $
  14.252 +          (Const (@{const_name "measurable"}, _) $ _ $ _)) = true
  14.253 +      | is_sets_eq _ = false
  14.254 +
  14.255 +    val cong_thms = get_cong (Context.Proof ctxt) @
  14.256 +      filter (fn thm => concl_of thm |> HOLogic.dest_Trueprop |> is_sets_eq handle TERM _ => false) facts
  14.257 +
  14.258 +    fun sets_cong_tac i =
  14.259 +      Subgoal.FOCUS (fn {context = ctxt', prems = prems, ...} => (
  14.260 +        let
  14.261 +          val ctxt'' = Simplifier.add_prems prems ctxt'
  14.262 +        in
  14.263 +          r_tac "cong intro" [elem_congI]
  14.264 +          THEN' SOLVED' (fn i => REPEAT_DETERM (
  14.265 +              ((r_tac "cong solve" (cong_thms @ [@{thm refl}])
  14.266 +                ORELSE' IF' (fn i => fn thm => nprems_of thm > i)
  14.267 +                  (SOLVED' (asm_full_simp_tac ctxt''))) i)))
  14.268 +        end) 1) ctxt i
  14.269 +        THEN flexflex_tac ctxt
  14.270 +
  14.271 +    val simp_solver_tac = 
  14.272 +      IF' not_measurable_prop (debug_tac ctxt (K "simp ") o SOLVED' (asm_full_simp_tac ctxt))
  14.273 +
  14.274 +    val split_countable_tac =
  14.275 +      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
  14.276 +        let
  14.277 +          val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
  14.278 +          fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
  14.279 +          fun inst (ts, Ts) =
  14.280 +            Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) @{thm measurable_compose_countable}
  14.281 +        in r_tac "split countable" (cnt_prefixes ctxt f |> map inst) i end
  14.282 +        handle TERM _ => no_tac) 1)
  14.283  
  14.284      val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
  14.285  
  14.286 -    fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
  14.287 +    val split_app_tac =
  14.288 +      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
  14.289 +        let
  14.290 +          fun app_prefixes (Abs (n, T, (f $ g))) = let
  14.291 +                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
  14.292 +              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
  14.293 +            | app_prefixes _ = []
  14.294 +    
  14.295 +          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
  14.296 +            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
  14.297 +          val thy = Proof_Context.theory_of ctxt
  14.298 +          val tunify = Sign.typ_unify thy
  14.299 +          val thms = map
  14.300 +              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
  14.301 +              (get_app (Context.Proof ctxt))
  14.302 +          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
  14.303 +          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
  14.304 +            let
  14.305 +              val inst =
  14.306 +                (Vartab.empty, ~1)
  14.307 +                |> tunify (T, thmT)
  14.308 +                |> tunify (Tf, thmTf)
  14.309 +                |> tunify (Tc, thmTc)
  14.310 +                |> Vartab.dest o fst
  14.311 +              val subst = subst_TVars (map (apsnd snd) inst)
  14.312 +            in
  14.313 +              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
  14.314 +                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
  14.315 +            end
  14.316 +          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
  14.317 +        in if null cps then no_tac
  14.318 +            else r_tac "split app" cps i ORELSE debug_tac ctxt (fn () => "split app fun FAILED") no_tac end
  14.319 +        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
  14.320 +        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
  14.321  
  14.322 -    val depth_measurable_tac = REPEAT_cnt (fn n =>
  14.323 -       (COND (is_cond_formula 1)
  14.324 -        (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ctxt) 1))
  14.325 -        ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
  14.326 -          (split_app_tac ctxt 1) APPEND
  14.327 -          (splitter 1)))) 0
  14.328 +    val single_step_tac =
  14.329 +      simp_solver_tac
  14.330 +      ORELSE' r_tac "step" thms
  14.331 +      ORELSE' (split_app_tac ctxt)
  14.332 +      ORELSE' splitter
  14.333 +      ORELSE' (CHANGED o sets_cong_tac)
  14.334 +      ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac))
  14.335  
  14.336 -  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
  14.337 +  in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end;
  14.338  
  14.339  fun simproc ctxt redex =
  14.340    let