# HG changeset patch # User hoelzl # Date 1421172636 -3600 # Node ID f0707dc3d9aaa1757e33a72243ccedb31a6ac9ae # Parent 63c02d05166146b48aa2aed682e86f4ab256f600 measurability prover: removed app splitting, replaced by more powerful destruction rules diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Binary_Product_Measure.thy --- a/src/HOL/Probability/Binary_Product_Measure.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Binary_Product_Measure.thy Tue Jan 13 19:10:36 2015 +0100 @@ -79,17 +79,6 @@ finally show "(\x. (f x, g x)) -` (A \ B) \ space M \ sets M" . qed -lemma measurable_Pair_compose_split[measurable_dest]: - assumes f: "split f \ measurable (M1 \\<^sub>M M2) N" - assumes g: "g \ measurable M M1" and h: "h \ measurable M M2" - shows "(\x. f (g x) (h x)) \ measurable M N" - using measurable_compose[OF measurable_Pair f, OF g h] by simp - -lemma measurable_pair: - assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2" - shows "f \ measurable M (M1 \\<^sub>M M2)" - using measurable_Pair[OF assms] by simp - lemma measurable_fst[intro!, simp, measurable]: "fst \ measurable (M1 \\<^sub>M M2) M1" by (auto simp: fst_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times measurable_def) @@ -98,6 +87,29 @@ by (auto simp: snd_vimage_eq_Times space_pair_measure sets.sets_into_space times_Int_times measurable_def) +lemma measurable_Pair_compose_split[measurable_dest]: + assumes f: "split f \ measurable (M1 \\<^sub>M M2) N" + assumes g: "g \ measurable M M1" and h: "h \ measurable M M2" + shows "(\x. f (g x) (h x)) \ measurable M N" + using measurable_compose[OF measurable_Pair f, OF g h] by simp + +lemma measurable_Pair1_compose[measurable_dest]: + assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)" + assumes [measurable]: "h \ measurable N M" + shows "(\x. f (h x)) \ measurable N M1" + using measurable_compose[OF f measurable_fst] by simp + +lemma measurable_Pair2_compose[measurable_dest]: + assumes f: "(\x. (f x, g x)) \ measurable M (M1 \\<^sub>M M2)" + assumes [measurable]: "h \ measurable N M" + shows "(\x. g (h x)) \ measurable N M2" + using measurable_compose[OF f measurable_snd] by simp + +lemma measurable_pair: + assumes "(fst \ f) \ measurable M M1" "(snd \ f) \ measurable M M2" + shows "f \ measurable M (M1 \\<^sub>M M2)" + using measurable_Pair[OF assms] by simp + lemma assumes f[measurable]: "f \ measurable M (N \\<^sub>M P)" shows measurable_fst': "(\x. fst (f x)) \ measurable M N" @@ -276,15 +288,13 @@ show "countably_additive (sets (N \\<^sub>M M)) ?\" proof (rule countably_additiveI) fix F :: "nat \ ('b \ 'a) set" assume F: "range F \ sets (N \\<^sub>M M)" "disjoint_family F" - from F have *: "\i. F i \ sets (N \\<^sub>M M)" "(\i. F i) \ sets (N \\<^sub>M M)" by auto - moreover from F have "\i. (\x. emeasure M (Pair x -` F i)) \ borel_measurable N" - by (intro measurable_emeasure_Pair) auto + from F have *: "\i. F i \ sets (N \\<^sub>M M)" by auto moreover have "\x. disjoint_family (\i. Pair x -` F i)" by (intro disjoint_family_on_bisimulation[OF F(2)]) auto moreover have "\x. range (\i. Pair x -` F i) \ sets M" using F by (auto simp: sets_Pair1) ultimately show "(\n. ?\ (F n)) = ?\ (\i. F i)" - by (auto simp add: vimage_UN nn_integral_suminf[symmetric] suminf_emeasure subset_eq emeasure_nonneg sets_Pair1 + by (auto simp add: nn_integral_suminf[symmetric] vimage_UN suminf_emeasure emeasure_nonneg intro!: nn_integral_cong nn_integral_indicator[symmetric]) qed show "{a \ b |a b. a \ sets N \ b \ sets M} \ Pow (space N \ space M)" diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Bochner_Integration.thy --- a/src/HOL/Probability/Bochner_Integration.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Bochner_Integration.thy Tue Jan 13 19:10:36 2015 +0100 @@ -534,9 +534,13 @@ nn_integral_cong_AE) auto -lemma borel_measurable_has_bochner_integral[measurable_dest]: +lemma borel_measurable_has_bochner_integral: "has_bochner_integral M f x \ f \ borel_measurable M" - by (auto elim: has_bochner_integral.cases) + by (rule has_bochner_integral.cases) + +lemma borel_measurable_has_bochner_integral'[measurable_dest]: + "has_bochner_integral M f x \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" + using borel_measurable_has_bochner_integral[measurable] by measurable lemma has_bochner_integral_simple_bochner_integrable: "simple_bochner_integrable M f \ has_bochner_integral M f (simple_bochner_integral M f)" @@ -922,6 +926,10 @@ lemma borel_measurable_integrable[measurable_dest]: "integrable M f \ f \ borel_measurable M" by (auto elim: integrable.cases has_bochner_integral.cases) +lemma borel_measurable_integrable'[measurable_dest]: + "integrable M f \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" + using borel_measurable_integrable[measurable] by measurable + lemma integrable_cong: "M = N \ (\x. x \ space N \ f x = g x) \ integrable M f \ integrable N g" using assms by (simp cong: has_bochner_integral_cong add: integrable.simps) @@ -2765,6 +2773,7 @@ shows "integrable (Pi\<^sub>M I M) (\x. (\i\I. f i (x i)))" (is "integrable _ ?f") proof (unfold integrable_iff_bounded, intro conjI) interpret finite_product_sigma_finite M I by default fact + show "?f \ borel_measurable (Pi\<^sub>M I M)" using assms by simp have "(\\<^sup>+ x. ereal (norm (\i\I. f i (x i))) \Pi\<^sub>M I M) = @@ -2854,3 +2863,4 @@ hide_const simple_bochner_integrable end + diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Borel_Space.thy Tue Jan 13 19:10:36 2015 +0100 @@ -1211,6 +1211,10 @@ show "f \ borel_measurable M" by auto qed auto +lemma borel_measurable_erealD[measurable_dest]: + "(\x. ereal (f x)) \ borel_measurable M \ g \ measurable N M \ (\x. f (g x)) \ borel_measurable N" + unfolding borel_measurable_ereal_iff by simp + lemma borel_measurable_ereal_iff_real: fixes f :: "'a \ ereal" shows "f \ borel_measurable M \ diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Finite_Product_Measure.thy --- a/src/HOL/Probability/Finite_Product_Measure.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Finite_Product_Measure.thy Tue Jan 13 19:10:36 2015 +0100 @@ -540,7 +540,7 @@ shows "(PIE j:I. E j) \ sets (PIM i:I. M i)" using sets_PiM_I[of I I E M] sets.sets_into_space[OF sets] `finite I` sets by auto -lemma measurable_component_singleton: +lemma measurable_component_singleton[measurable (raw)]: assumes "i \ I" shows "(\x. x i) \ measurable (Pi\<^sub>M I M) (M i)" proof (unfold measurable_def, intro CollectI conjI ballI) fix A assume "A \ sets (M i)" @@ -551,13 +551,14 @@ using `A \ sets (M i)` `i \ I` by (auto intro!: sets_PiM_I) qed (insert `i \ I`, auto simp: space_PiM) -lemma measurable_component_singleton'[measurable_app]: +lemma measurable_component_singleton'[measurable_dest]: assumes f: "f \ measurable N (Pi\<^sub>M I M)" + assumes g: "g \ measurable L N" assumes i: "i \ I" - shows "(\x. (f x) i) \ measurable N (M i)" - using measurable_compose[OF f measurable_component_singleton, OF i] . + shows "(\x. (f (g x)) i) \ measurable L (M i)" + using measurable_compose[OF measurable_compose[OF g f] measurable_component_singleton, OF i] . -lemma measurable_PiM_component_rev[measurable (raw)]: +lemma measurable_PiM_component_rev: "i \ I \ f \ measurable (M i) N \ (\x. f (x i)) \ measurable (PiM I M) N" by simp diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Measurable.thy --- a/src/HOL/Probability/Measurable.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Measurable.thy Tue Jan 13 19:10:36 2015 +0100 @@ -63,9 +63,6 @@ attribute_setup measurable_dest = Measurable.dest_thm_attr "add dest rule to measurability prover" -attribute_setup measurable_app = Measurable.app_thm_attr - "add application rule to measurability prover" - attribute_setup measurable_cong = Measurable.cong_thm_attr "add congurence rules to measurability prover" @@ -77,9 +74,8 @@ setup {* Global_Theory.add_thms_dynamic (@{binding measurable}, Measurable.get_all) *} - + declare - measurable_compose_rev[measurable_dest] pred_sets1[measurable_dest] pred_sets2[measurable_dest] sets.sets_into_space[measurable_dest] diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/Probability_Measure.thy --- a/src/HOL/Probability/Probability_Measure.thy Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/Probability_Measure.thy Tue Jan 13 19:10:36 2015 +0100 @@ -514,22 +514,17 @@ and distributed_real_AE: "distributed M N X (\x. ereal (f x)) \ (AE x in N. 0 \ f x)" by (simp_all add: distributed_def borel_measurable_ereal_iff) -lemma - assumes D: "distributed M N X (\x. ereal (f x))" - shows distributed_real_measurable'[measurable_dest]: - "h \ measurable L N \ (\x. f (h x)) \ borel_measurable L" - using distributed_real_measurable[OF D] - by simp_all +lemma distributed_real_measurable': + "distributed M N X (\x. ereal (f x)) \ h \ measurable L N \ (\x. f (h x)) \ borel_measurable L" + by simp -lemma - assumes D: "distributed M (S \\<^sub>M T) (\x. (X x, Y x)) f" - shows joint_distributed_measurable1[measurable_dest]: - "h1 \ measurable N M \ (\x. X (h1 x)) \ measurable N S" - and joint_distributed_measurable2[measurable_dest]: - "h2 \ measurable N M \ (\x. Y (h2 x)) \ measurable N T" - using measurable_compose[OF distributed_measurable[OF D] measurable_fst] - using measurable_compose[OF distributed_measurable[OF D] measurable_snd] - by auto +lemma joint_distributed_measurable1: + "distributed M (S \\<^sub>M T) (\x. (X x, Y x)) f \ h1 \ measurable N M \ (\x. X (h1 x)) \ measurable N S" + by simp + +lemma joint_distributed_measurable2: + "distributed M (S \\<^sub>M T) (\x. (X x, Y x)) f \ h2 \ measurable N M \ (\x. Y (h2 x)) \ measurable N T" + by simp lemma distributed_count_space: assumes X: "distributed M (count_space A) X P" and a: "a \ A" and A: "finite A" diff -r 63c02d051661 -r f0707dc3d9aa src/HOL/Probability/measurable.ML --- a/src/HOL/Probability/measurable.ML Sun Jan 11 21:06:47 2015 +0100 +++ b/src/HOL/Probability/measurable.ML Tue Jan 13 19:10:36 2015 +0100 @@ -10,7 +10,6 @@ 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 @@ -28,6 +27,8 @@ 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 + + val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context) end ; structure Measurable : MEASURABLE = @@ -48,21 +49,18 @@ type T = { measurable_thms : (thm * (bool * level)) Item_Net.T, dest_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, cong_thms = Thm.full_rules, preprocessors = [] }; val extend = I; - 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 }) = { + fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 }, + {measurable_thms = t2, dest_thms = dt2, 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), cong_thms = Item_Net.merge (ct1, ct2), preprocessors = merge_dups i1 i2 }; @@ -74,23 +72,20 @@ val split = Attrib.setup_config_bool @{binding measurable_split} (K true) -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_data f1 f2 f3 f4 + {measurable_thms = t1, dest_thms = t2, cong_thms = t3, preprocessors = t4 } = + {measurable_thms = f1 t1, dest_thms = f2 t2, cong_thms = f3 t3, preprocessors = f4 t4} -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 map_measurable_thms f = map_data f I I I +fun map_dest_thms f = map_data I f I I +fun map_cong_thms f = map_data I I f I +fun map_preprocessors f = map_data I I I f fun generic_add_del map = Scan.lift (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >> (fn f => Thm.declaration_attribute (Data.map o map o f)) -val app_thm_attr = generic_add_del map_app_thms - val dest_thm_attr = generic_add_del map_dest_thms val cong_thm_attr = generic_add_del map_cong_thms @@ -104,7 +99,6 @@ (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm)) 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; @@ -175,6 +169,35 @@ end | cnt_prefixes _ _ = [] +fun apply_dests thm dests = + let + fun apply thm th' = + let + val th'' = thm RS th' + in [th''] @ loop th'' end + handle (THM _) => [] + and loop thm = + flat (map (apply thm) dests) + in + [thm] @ ([thm RS @{thm measurable_compose_rev}] handle (THM _) => []) @ loop thm + end + +fun prepare_facts ctxt facts = + let + val dests = get_dest (Context.Proof ctxt) + fun prep_dest thm = + (if is_too_generic thm then [] else apply_dests thm 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 + in (thms, ctxt) end + fun measurable_tac ctxt facts = let fun debug_fact msg thm () = @@ -186,23 +209,12 @@ 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)) + 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 + val (thms, ctxt) = prepare_facts ctxt facts fun is_sets_eq (Const (@{const_name "HOL.eq"}, _) $ (Const (@{const_name "sets"}, _) $ _) $ @@ -243,45 +255,9 @@ val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac - 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 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))