# HG changeset patch # User hoelzl # Date 1416828014 -3600 # Node ID 7dc8ac6f089528d216d5df4e4f2e5cb6317017f5 # Parent 8d7cec9b861d8d48ee64b6f4d060d542ce7b9b1a add congruence solver to measurability prover diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Binary_Product_Measure.thy --- 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 \\<^sub>M B) \ 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' \ sets M2 = sets M2' \ sets (M1 \\<^sub>M M2) = sets (M1' \\<^sub>M M2')" unfolding sets_pair_measure by (simp cong: sets_eq_imp_space_eq) diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Bochner_Integration.thy --- 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 \ '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 "((\y. \ x. indicator {.. y} x *\<^sub>R f x \M) ---> \ x. f x \M) at_top" proof (rule tendsto_at_topI_sequentially) fix X :: "nat \ real" assume "filterlim X at_top sequentially" diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Convolution.thy --- 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 \ borel_measurable borel" shows "(\\<^sup>+x. f x \convolution M N) = (\\<^sup>+x. \\<^sup>+y. f (x + y) \N \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 \ 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 \ 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 \ M) \ N ) A = \\<^sup>+x. \\<^sup>+y. \\<^sup>+z. indicator A (x + y + z) \N \M \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 \ N) = (N \ M)" proof (rule measure_eqI) interpret M: finite_measure M by fact diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Fin_Map.thy --- 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 \ sets (PiF (Collect finite) (\_. N))" shows "emeasure (mapmeasure M (\_. N)) X = emeasure M ((fm -` X \ 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 \ sets M" shows "emeasure M X = emeasure (mapmeasure M (\_. 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 \ space (Pi\<^sub>M J (\_. N))" using assms by (simp add: sets.sets_into_space) from assms inj_on_fm[of "\_. N"] set_mp[OF this] have "fm -` fm ` X \ space (Pi\<^sub>M J (\_. N)) = X" by (auto simp: vimage_image_eq inj_on_def) diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Finite_Product_Measure.thy --- 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" "\i. i \ J \ sets (M i) = sets (N i)" shows "sets (PiM I M) = sets (PiM J N)" +lemma sets_PiM_cong[measurable_cong]: + assumes "I = J" "\i. i \ J \ 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 @@ "\j. i = Suc j \ (\x. g x j) \ measurable M N" shows "(\x. case_nat (f x) (g x) i) \ measurable M N" by (cases i) simp_all - + lemma measurable_case_nat'[measurable (raw)]: assumes fg[measurable]: "f \ measurable N M" "g \ measurable N (\\<^sub>M i\UNIV. M)" shows "(\x. case_nat (f x) (g x)) \ measurable N (\\<^sub>M i\UNIV. M)" @@ -885,6 +886,8 @@ have eq: "\x. x \ extensional {i} \ (\j\{i}. x i) = x" by (auto simp: extensional_def restrict_def) + have [measurable]: "\j. j \ {i} \ (\x. x) \ measurable (M i) (M j)" by simp + fix A assume A: "A \ sets ?P" then have "emeasure ?P A = (\\<^sup>+x. indicator A x \?P)" by simp diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Giry_Monad.thy --- 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 \ + Context.theory_map (Measurable.add_preprocessor "subprob_cong" subprob_cong) +\ + context fixes K M N assumes K: "K \ 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 \ borel_measurable N" "\x. 0 \ f x" shows "(\M. integral\<^sup>N M f) \ borel_measurable (subprob_algebra N)" (is "_ \ ?B") using f @@ -144,24 +163,30 @@ next case (mult f c) moreover then have "(\M'. \\<^sup>+M''. c * f M'' \M') \ ?B \ (\M'. c * \\<^sup>+M''. f M'' \M') \ ?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 "(\M'. \\<^sup>+M''. f M'' + g M'' \M') \ ?B \ (\M'. (\\<^sup>+M''. f M'' \M') + (\\<^sup>+M''. g M'' \M')) \ ?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 "(\M'. \\<^sup>+M''. (SUP i. F i) M'' \M') \ ?B \ (\M'. SUP i. (\\<^sup>+M''. F i M'' \M')) \ ?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 \ borel_measurable N \ (\M. integral\<^sup>N M f) \ 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 \ measurable M N" shows "(\M'. distr M' N f) \ measurable (subprob_algebra M) (subprob_algebra N)" @@ -173,11 +198,12 @@ then have "(\M'. emeasure (distr M' N f) A) \ borel_measurable (subprob_algebra M) \ (\M'. emeasure M' (f -` A \ space M)) \ 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 \"]) also have "\" using A by (intro measurable_emeasure_subprob_algebra) simp finally show "(\M'. emeasure (distr M' N f) A) \ 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]: "(\(x, y). f x y) \ borel_measurable (M \\<^sub>M N)" and [simp]: "\x y. 0 \ f x y" + assumes f[measurable]: "(\(x, y). f x y) \ borel_measurable (M \\<^sub>M N)" assumes N[measurable]: "L \ measurable M (subprob_algebra N)" shows "(\x. integral\<^sup>N (L x) (f x)) \ borel_measurable M" proof - + note nn_integral_measurable_subprob_algebra[measurable] + note measurable_distr2[measurable] have "(\x. integral\<^sup>N (distr (L x) (M \\<^sub>M N) (\y. (x, y))) (\(x, y). f x y)) \ 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 "(\x. integral\<^sup>N (L x) (f x)) \ 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 \ sets N" + assumes M[simp, measurable_cong]: "sets M = sets (subprob_algebra N)" and A: "A \ sets N" shows "emeasure (join M) A = (\\<^sup>+ M'. emeasure M' A \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)) (\B. \\<^sup>+ M'. emeasure M' B \M)" proof (rule countably_additiveI) fix A :: "nat \ 'a set" assume A: "range A \ sets (join M)" "disjoint_family A" have "(\i. \\<^sup>+ M'. emeasure M' (A i) \M) = (\\<^sup>+M'. (\i. emeasure M' (A i)) \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 "\ = (\\<^sup>+M'. emeasure M' (\i. A i) \M)" proof (rule nn_integral_cong) fix M' assume "M' \ space M" @@ -577,7 +595,7 @@ by (intro emeasure_join) (auto simp: space_subprob_algebra `A\sets N`) qed also have "(\M'. \\<^sup>+M''. emeasure M'' A \M') \ ?B" - using measurable_emeasure_subprob_algebra[OF `A\sets N`] emeasure_nonneg[of _ A] + using measurable_emeasure_subprob_algebra[OF `A\sets N`] by (rule nn_integral_measurable_subprob_algebra) finally show "(\M'. emeasure (join M') A) \ 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 \ borel_measurable N" "\x. 0 \ f x" and M: "sets M = sets (subprob_algebra N)" +lemma nn_integral_join': + assumes f: "f \ borel_measurable N" "\x. 0 \ f x" + and M[measurable_cong]: "sets M = sets (subprob_algebra N)" shows "(\\<^sup>+x. f x \join M) = (\\<^sup>+M'. \\<^sup>+x. f x \M' \M)" using f proof induct @@ -619,51 +638,58 @@ next case (mult f c) have "(\\<^sup>+ M'. \\<^sup>+ x. c * f x \M' \M) = (\\<^sup>+ M'. c * \\<^sup>+ x. f x \M' \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 "\ = c * (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \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 "\ = c * (integral\<^sup>N (join M) f)" by (simp add: mult) also have "\ = (\\<^sup>+ x. c * f x \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 "(\\<^sup>+ M'. \\<^sup>+ x. f x + g x \M' \M) = (\\<^sup>+ M'. (\\<^sup>+ x. f x \M') + (\\<^sup>+ x. g x \M') \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 "\ = (\\<^sup>+ M'. \\<^sup>+ x. f x \M' \M) + (\\<^sup>+ M'. \\<^sup>+ x. g x \M' \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 "\ = (integral\<^sup>N (join M) f) + (integral\<^sup>N (join M) g)" by (simp add: add) also have "\ = (\\<^sup>+ x. f x + g x \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 "(\\<^sup>+ M'. \\<^sup>+ x. (SUP i. F i) x \M' \M) = (\\<^sup>+ M'. (SUP i. \\<^sup>+ x. F i x \M') \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 "\ = (SUP i. \\<^sup>+ M'. \\<^sup>+ x. F i x \M' \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 "\ = (SUP i. integral\<^sup>N (join M) (F i))" by (simp add: seq) also have "\ = (\\<^sup>+ x. (SUP i. F i x) \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 \ borel_measurable N" "sets M = sets (subprob_algebra N)" + shows "(\\<^sup>+x. f x \join M) = (\\<^sup>+M'. \\<^sup>+x. f x \M' \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 \ 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 = {} \ space (bind M f) = {}" by (simp add: bind_def) -lemma sets_bind[simp]: - assumes "f \ measurable M (subprob_algebra N)" and "space M \ {}" +lemma sets_bind[simp, measurable_cong]: + assumes f: "\x. x \ space M \ sets (f x) = sets N" and M: "space M \ {}" 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 \ space M"] by (simp add: bind_nonempty M some_in_eq) lemma space_bind[simp]: - assumes "f \ measurable M (subprob_algebra N)" and "space M \ {}" + assumes "\x. x \ space M \ sets (f x) = sets N" and "space M \ {}" 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 "\x \ space M. f x = g x" @@ -785,8 +811,8 @@ \ emeasure (M \= f) X = \\<^sup>+x. emeasure (f x) X \M" by (simp add: bind_nonempty'' emeasure_join nn_integral_distr measurable_emeasure_subprob_algebra) -lemma nn_integral_bind': - assumes f: "f \ borel_measurable B" "\x. 0 \ f x" +lemma nn_integral_bind: + assumes f: "f \ borel_measurable B" assumes N: "N \ measurable M (subprob_algebra B)" shows "(\\<^sup>+x. f x \(M \= N)) = (\\<^sup>+x. \\<^sup>+y. f y \N x \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 \ borel_measurable B" - assumes N: "N \ measurable M (subprob_algebra B)" - shows "(\\<^sup>+x. f x \(M \= N)) = (\\<^sup>+x. \\<^sup>+y. f y \N x \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 \ 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 \ {}" + note sets_kernel[OF N, simp] have *: "(\\<^sup>+x. indicator {x. \ P x} x \(M \= N)) = (\\<^sup>+x. indicator {x\space B. \ P x} x \(M \= 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 \= N. P x) \ (\\<^sup>+ x. integral\<^sup>N (N x) (indicator {x \ space B. \ P x}) \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 "\ = (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 \ measurable M (subprob_algebra N)" and M2: "(\x. g (fst x) (snd x)) \ measurable (M \\<^sub>M N) (subprob_algebra R)" shows "(\x. bind (f x) (g x)) \ measurable M (subprob_algebra R)" @@ -881,7 +897,7 @@ proof have "emeasure (M \= N) (space (M \= N)) = (\\<^sup>+x. emeasure (N x) (space (N x)) \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 "\ = (\\<^sup>+x. 1 \M)" using ae by (intro nn_integral_cong_AE, eventually_elim) (rule prob_space.emeasure_space_1) finally show "emeasure (M \= N) (space (M \= N)) = 1" @@ -890,7 +906,7 @@ lemma (in subprob_space) bind_in_space: "A \ measurable M (subprob_algebra N) \ (M \= A) \ 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 \ sets K" "X \ {}" shows "restrict_space (bind M N) X = bind M (\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 (\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 \ sets (restrict_space (M \= N) X)" with X have "A \ sets K" "A \ 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 \= N) X) A = emeasure (M \= (\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': "\prob_space M; subprob_space N\ \ M \= (\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 \ space (subprob_algebra M)" + by (simp add: space_subprob_algebra) unfold_locales + lemma (in pair_prob_space) pair_measure_eq_bind: "(M1 \\<^sub>M M2) = (M1 \= (\x. M2 \= (\y. return (M1 \\<^sub>M M2) (x, y))))" proof (rule measure_eqI) have ps_M2: "prob_space M2" by unfold_locales note return_measurable[measurable] - have 1: "(\x. M2 \= (\y. return (M1 \\<^sub>M M2) (x, y))) \ measurable M1 (subprob_algebra (M1 \\<^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 \\<^sub>M M2) = sets (M1 \= (\x. M2 \= (\y. return (M1 \\<^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 \ sets (M1 \\<^sub>M M2)" show "emeasure (M1 \\<^sub>M M2) A = emeasure (M1 \= (\x. M2 \= (\y. return (M1 \\<^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 \\<^sub>M M2"] M2.not_empty + by (auto simp: M2.emeasure_pair_measure M1.not_empty M2.not_empty emeasure_bind[where N="M1 \\<^sub>M M2"] intro!: nn_integral_cong) qed diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Lebesgue_Measure.thy --- 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 \ 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 (\\<^sub>M b\Basis. interval_measure (\x. x)) borel (\f. \b\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" diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Measurable.thy --- 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 = \ Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \ "measurability prover" @@ -72,7 +75,7 @@ simproc_setup measurable ("A \ sets M" | "f \ 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 \ {x\space M. P x} \ sets M" unfolding pred_def . @@ -589,3 +595,4 @@ hide_const (open) pred end + diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Measure_Space.thy --- 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) (\A. emeasure M (f -` A \ 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) diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Nonnegative_Lebesgue_Integration.thy --- 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) (\A. \\<^sup>+ x. f x * indicator A x \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 \ measurable (point_measure A f) M \ g \ A \ space M" unfolding point_measure_def by simp @@ -2272,7 +2275,7 @@ definition "uniform_measure M A = density M (\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 \ X \ A \ emeasure (uniform_count_measure A) X = card X / card A" diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Probability_Mass_Function.thy --- 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 \ 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 \ 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 \= A) = sets (measure_pmf x \= 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 \ sets (measure_pmf x \= A)" then have X: "X \ 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 \= A) X = emeasure (measure_pmf x \= 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 \ measurable (measure_pmf M) (subprob_algebra (count_space UNIV))" - using measurable_measure_pmf[of "\x. x"] by simp - interpret bind: prob_space "measure_pmf M \= 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 \= measure_pmf)" by intro_locales show "sets (measure_pmf M \= measure_pmf) = UNIV" - by (subst sets_bind[OF *]) auto + by (subst sets_bind) auto have "AE x in measure_pmf M \= measure_pmf. emeasure (measure_pmf M \= measure_pmf) {x} \ 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 \= measure_pmf. measure (measure_pmf M \= measure_pmf) {x} \ 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 \ 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 \ space (subprob_algebra (count_space UNIV))" + by (simp add: space_subprob_algebra) intro_locales + lemma bind_pair_pmf: assumes M[measurable]: "M \ measurable (count_space UNIV \\<^sub>M count_space UNIV) (subprob_algebra N)" shows "measure_pmf (pair_pmf A B) \= M = (measure_pmf A \= (\x. measure_pmf B \= (\y. M (x, y))))" @@ -780,46 +789,25 @@ have M'[measurable]: "M \ 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 \ sets ?L" then have X[measurable]: "X \ 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 diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Sigma_Algebra.thy --- 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 \ measurable M M' \ g \ measurable N N'" by (metis measurable_cong) -lemma measurable_eqI: - "\ space m1 = space m1' ; space m2 = space m2' ; - sets m1 = sets m1' ; sets m2 = sets m2' \ - \ measurable m1 m2 = measurable m1' m2'" - by (simp add: measurable_def sigma_algebra_iff2) - lemma measurable_compose: assumes f: "f \ measurable M N" and g: "g \ measurable N L" shows "(\x. g (f x)) \ measurable M L" @@ -1990,6 +1984,9 @@ lemma measurable_ident: "id \ measurable M M" by (auto simp add: measurable_def) +lemma measurable_id: "(\x. x) \ measurable M M" + by (simp add: measurable_def) + lemma measurable_ident_sets: assumes eq: "sets M = sets M'" shows "(\x. x) \ measurable M M'" using measurable_ident[of M] diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/Stream_Space.thy --- 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 (\\<^sub>M i\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 \ sets (stream_space M) = sets (stream_space N)" +lemma sets_stream_space_cong[measurable_cong]: + "sets M = sets N \ 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: "(\\ n. \ !! n) \ measurable (stream_space M) (\\<^sub>M i\UNIV. M)" diff -r 8d7cec9b861d -r 7dc8ac6f0895 src/HOL/Probability/measurable.ML --- 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 \ x \ B \ x \ 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