add support for function application to measurability prover
authorhoelzl
Tue Nov 06 19:18:35 2012 +0100 (2012-11-06)
changeset 50021d96a3f468203
parent 50020 6b9611abcd4c
child 50022 286dfcab9833
add support for function application to measurability prover
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Independent_Family.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Sigma_Algebra.thy
     1.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Nov 06 15:15:33 2012 +0100
     1.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Nov 06 19:18:35 2012 +0100
     1.3 @@ -74,7 +74,7 @@
     1.4      using assms[of S] by simp
     1.5  qed
     1.6  
     1.7 -lemma borel_measurable_const[measurable (raw)]:
     1.8 +lemma borel_measurable_const:
     1.9    "(\<lambda>x. c) \<in> borel_measurable M"
    1.10    by auto
    1.11  
    1.12 @@ -168,7 +168,8 @@
    1.13    shows borel_measurable_le[measurable]: "{w \<in> space M. f w \<le> g w} \<in> sets M"
    1.14      and borel_measurable_eq[measurable]: "{w \<in> space M. f w = g w} \<in> sets M"
    1.15      and borel_measurable_neq: "{w \<in> space M. f w \<noteq> g w} \<in> sets M"
    1.16 -  unfolding eq_iff not_less[symmetric] by measurable+
    1.17 +  unfolding eq_iff not_less[symmetric]
    1.18 +  by measurable
    1.19  
    1.20  subsection "Borel space equals sigma algebras over intervals"
    1.21  
     2.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 06 15:15:33 2012 +0100
     2.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Tue Nov 06 19:18:35 2012 +0100
     2.3 @@ -480,7 +480,7 @@
     2.4    shows "(PIE j:I. E j) \<in> sets (PIM i:I. M i)"
     2.5    using sets_PiM_I[of I I E M] sets_into_space[OF sets] `finite I` sets by auto
     2.6  
     2.7 -lemma measurable_component_singleton[measurable (raw)]:
     2.8 +lemma measurable_component_singleton:
     2.9    assumes "i \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^isub>M I M) (M i)"
    2.10  proof (unfold measurable_def, intro CollectI conjI ballI)
    2.11    fix A assume "A \<in> sets (M i)"
    2.12 @@ -491,6 +491,18 @@
    2.13      using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
    2.14  qed (insert `i \<in> I`, auto simp: space_PiM)
    2.15  
    2.16 +lemma measurable_component_singleton'[measurable_app]:
    2.17 +  assumes f: "f \<in> measurable N (Pi\<^isub>M I M)"
    2.18 +  assumes i: "i \<in> I"
    2.19 +  shows "(\<lambda>x. (f x) i) \<in> measurable N (M i)"
    2.20 +  using measurable_compose[OF f measurable_component_singleton, OF i] .
    2.21 +
    2.22 +lemma measurable_nat_case[measurable (raw)]:
    2.23 +  assumes [measurable (raw)]: "i = 0 \<Longrightarrow> f \<in> measurable M N"
    2.24 +    "\<And>j. i = Suc j \<Longrightarrow> (\<lambda>x. g x j) \<in> measurable M N"
    2.25 +  shows "(\<lambda>x. nat_case (f x) (g x) i) \<in> measurable M N"
    2.26 +  by (cases i) simp_all
    2.27 +
    2.28  lemma measurable_add_dim[measurable]:
    2.29    "(\<lambda>(f, y). f(i := y)) \<in> measurable (Pi\<^isub>M I M \<Otimes>\<^isub>M M i) (Pi\<^isub>M (insert i I) M)"
    2.30      (is "?f \<in> measurable ?P ?I")
     3.1 --- a/src/HOL/Probability/Independent_Family.thy	Tue Nov 06 15:15:33 2012 +0100
     3.2 +++ b/src/HOL/Probability/Independent_Family.thy	Tue Nov 06 19:18:35 2012 +0100
     3.3 @@ -1004,9 +1004,6 @@
     3.4    "A \<in> sets N \<Longrightarrow> f \<in> measurable M N \<Longrightarrow> (\<lambda>x. indicator A (f x)) \<in> borel_measurable M"
     3.5    using measurable_comp[OF _ borel_measurable_indicator, of f M N A] by (auto simp add: comp_def)
     3.6  
     3.7 -lemma measurable_id_prod[measurable (raw)]: "i = j \<Longrightarrow> (\<lambda>x. x) \<in> measurable (M i) (M j)"
     3.8 -  by simp
     3.9 -
    3.10  lemma (in product_sigma_finite) distr_component:
    3.11    "distr (M i) (Pi\<^isub>M {i} M) (\<lambda>x. \<lambda>i\<in>{i}. x) = Pi\<^isub>M {i} M" (is "?D = ?P")
    3.12  proof (intro measure_eqI[symmetric])
     4.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 06 15:15:33 2012 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Nov 06 19:18:35 2012 +0100
     4.3 @@ -270,7 +270,7 @@
     4.4      have "simple_function M (\<lambda>x. real (f x i))"
     4.5      proof (intro simple_function_borel_measurable)
     4.6        show "(\<lambda>x. real (f x i)) \<in> borel_measurable M"
     4.7 -        using u by (auto intro!: measurable_If simp: real_f)
     4.8 +        using u by (auto simp: real_f)
     4.9        have "(\<lambda>x. real (f x i))`space M \<subseteq> real`{..i*2^i}"
    4.10          using f_upper[of _ i] by auto
    4.11        then show "finite ((\<lambda>x. real (f x i))`space M)"
     5.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 06 15:15:33 2012 +0100
     5.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Nov 06 19:18:35 2012 +0100
     5.3 @@ -922,8 +922,7 @@
     5.4    then show "AE x in M. f x = f' x"
     5.5      unfolding eventually_ae_filter using h_borel pos
     5.6      by (auto simp add: h_null_sets null_sets_density_iff not_less[symmetric]
     5.7 -                          AE_iff_null_sets[symmetric])
     5.8 -       blast
     5.9 +                          AE_iff_null_sets[symmetric]) blast
    5.10  qed
    5.11  
    5.12  lemma (in sigma_finite_measure) density_unique_iff:
    5.13 @@ -1126,7 +1125,7 @@
    5.14    fixes T :: "'a \<Rightarrow> 'b"
    5.15    assumes T: "T \<in> measurable M M'" and T': "T' \<in> measurable M' M"
    5.16      and inv: "\<forall>x\<in>space M. T' (T x) = x"
    5.17 -  and ac: "absolutely_continuous (distr M M' T) (distr N M' T)"
    5.18 +  and ac[simp]: "absolutely_continuous (distr M M' T) (distr N M' T)"
    5.19    and N: "sets N = sets M"
    5.20    shows "AE x in M. RN_deriv (distr M M' T) (distr N M' T) (T x) = RN_deriv M N x"
    5.21  proof (rule RN_deriv_unique)
    5.22 @@ -1162,7 +1161,7 @@
    5.23      qed
    5.24    qed
    5.25    have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
    5.26 -    using T ac by measurable simp
    5.27 +    using T ac by measurable
    5.28    then show "(\<lambda>x. RN_deriv ?M' ?N' (T x)) \<in> borel_measurable M"
    5.29      by (simp add: comp_def)
    5.30    show "AE x in M. 0 \<le> RN_deriv ?M' ?N' (T x)" using M'.RN_deriv_nonneg[OF ac] by auto
     6.1 --- a/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 06 15:15:33 2012 +0100
     6.2 +++ b/src/HOL/Probability/Sigma_Algebra.thy	Tue Nov 06 19:18:35 2012 +0100
     6.3 @@ -1331,8 +1331,10 @@
     6.4  lemma measurable_ident: "id \<in> measurable M M"
     6.5    by (auto simp add: measurable_def)
     6.6  
     6.7 -lemma measurable_ident': "(\<lambda>x. x) \<in> measurable M M"
     6.8 -  by (auto simp add: measurable_def)
     6.9 +lemma measurable_ident_sets:
    6.10 +  assumes eq: "sets M = sets M'" shows "(\<lambda>x. x) \<in> measurable M M'"
    6.11 +  using measurable_ident[of M]
    6.12 +  unfolding id_def measurable_def eq sets_eq_imp_space_eq[OF eq] .
    6.13  
    6.14  lemma sets_Least:
    6.15    assumes meas: "\<And>i::nat. {x\<in>space M. P i x} \<in> M"
    6.16 @@ -1497,28 +1499,58 @@
    6.17  
    6.18  structure Data = Generic_Data
    6.19  (
    6.20 -  type T = (thm list * thm list) * thm list;
    6.21 -  val empty = (([], []), []);
    6.22 +  type T = {
    6.23 +    concrete_thms : thm Item_Net.T,
    6.24 +    generic_thms : thm Item_Net.T,
    6.25 +    dest_thms : thm Item_Net.T,
    6.26 +    app_thms : thm Item_Net.T }
    6.27 +  val empty = {
    6.28 +    concrete_thms = Thm.full_rules,
    6.29 +    generic_thms = Thm.full_rules,
    6.30 +    dest_thms = Thm.full_rules,
    6.31 +    app_thms = Thm.full_rules};
    6.32    val extend = I;
    6.33 -  val merge = fn (((c1, g1), d1), ((c2, g2), d2)) => ((c1 @ c2, g1 @ g2), d1 @ d2);
    6.34 +  fun merge (t1, t2) = {
    6.35 +    concrete_thms = Item_Net.merge (#concrete_thms t1, #concrete_thms t2),
    6.36 +    generic_thms = Item_Net.merge (#generic_thms t1, #generic_thms t2),
    6.37 +    dest_thms = Item_Net.merge (#dest_thms t1, #dest_thms t2),
    6.38 +    app_thms = Item_Net.merge (#app_thms t1, #app_thms t2) };
    6.39  );
    6.40  
    6.41  val debug =
    6.42    Attrib.setup_config_bool @{binding measurable_debug} (K false)
    6.43  
    6.44  val backtrack =
    6.45 -  Attrib.setup_config_int @{binding measurable_backtrack} (K 40)
    6.46 +  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
    6.47 +
    6.48 +val split =
    6.49 +  Attrib.setup_config_bool @{binding measurable_split} (K true)
    6.50  
    6.51 -fun get lv = (case lv of Concrete => fst | Generic => snd) o fst o Data.get o Context.Proof; 
    6.52 +fun TAKE n tac = Seq.take n o tac
    6.53 +
    6.54 +fun get lv =
    6.55 +  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
    6.56 +  Data.get o Context.Proof;
    6.57 +
    6.58  fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
    6.59  
    6.60 -fun update f lv = Data.map (apfst (case lv of Concrete => apfst f | Generic => apsnd f));
    6.61 -fun add thms' = update (fn thms => thms @ thms');
    6.62 +fun map_data f1 f2 f3 f4
    6.63 +  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
    6.64 +  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
    6.65 +
    6.66 +fun map_concrete_thms f = map_data f I I I
    6.67 +fun map_generic_thms f = map_data I f I I
    6.68 +fun map_dest_thms f = map_data I I f I
    6.69 +fun map_app_thms f = map_data I I I f
    6.70  
    6.71 -val get_dest = snd o Data.get;
    6.72 -fun add_dest thm = Data.map (apsnd (fn thms => thms @ [thm]));
    6.73 +fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
    6.74 +fun add thms' = update (fold Item_Net.update thms');
    6.75  
    6.76 -fun TRYALL' tacs = fold_rev (curry op APPEND') tacs (K no_tac);
    6.77 +val get_dest = Item_Net.content o #dest_thms o Data.get;
    6.78 +val add_dest = Data.map o map_dest_thms o Item_Net.update;
    6.79 +
    6.80 +val get_app = Item_Net.content o #app_thms o Data.get;
    6.81 +val add_app = Data.map o map_app_thms o Item_Net.update;
    6.82  
    6.83  fun is_too_generic thm =
    6.84    let 
    6.85 @@ -1531,9 +1563,7 @@
    6.86  
    6.87  fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
    6.88  
    6.89 -fun debug_tac ctxt msg f = if Config.get ctxt debug then K (print_tac (msg ())) THEN' f else f
    6.90 -
    6.91 -fun TAKE n f thm = Seq.take n (f thm)
    6.92 +fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
    6.93  
    6.94  fun nth_hol_goal thm i =
    6.95    HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
    6.96 @@ -1543,6 +1573,13 @@
    6.97      (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
    6.98    | _ => raise (TERM ("not a measurability predicate", [t])))
    6.99  
   6.100 +fun is_cond_formula n thm = if length (prems_of thm) < n then false else
   6.101 +  (case nth_hol_goal thm n of
   6.102 +    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   6.103 +  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   6.104 +  | _ => true)
   6.105 +  handle TERM _ => true;
   6.106 +
   6.107  fun indep (Bound i) t b = i < b orelse t <= i
   6.108    | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   6.109    | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   6.110 @@ -1557,51 +1594,89 @@
   6.111            in
   6.112              map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   6.113              map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   6.114 -            (if is_countable (fastype_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   6.115 +            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   6.116                  andalso indep g n 0 andalso g <> Bound n
   6.117                then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   6.118                else [])
   6.119            end
   6.120          | cnt_walk _ _ = []
   6.121      in map (fn (t1, t2) => let
   6.122 -        val T1 = fastype_of1 ([T], t2)
   6.123 -        val T2 = fastype_of1 ([T], t)
   6.124 +        val T1 = type_of1 ([T], t2)
   6.125 +        val T2 = type_of1 ([T], t)
   6.126        in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   6.127          [SOME T1, SOME T, SOME T2])
   6.128        end) (cnt_walk t [T])
   6.129      end
   6.130    | cnt_prefixes _ _ = []
   6.131  
   6.132 -val split_fun_tac =
   6.133 +val split_countable_tac =
   6.134    Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   6.135      let
   6.136        val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   6.137        fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   6.138        fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   6.139        val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   6.140 -    in if null cps then no_tac else debug_tac ctxt (K "split fun") (resolve_tac cps) i end
   6.141 +    in if null cps then no_tac else debug_tac ctxt (K ("split countable fun")) (resolve_tac cps i) end
   6.142      handle TERM _ => no_tac) 1)
   6.143  
   6.144 -fun single_measurable_tac ctxt facts =
   6.145 -  debug_tac ctxt (fn () => "single + " ^
   6.146 -    Pretty.str_of (Pretty.block (Pretty.commas (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)))))
   6.147 -  (resolve_tac ((maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt)
   6.148 -    APPEND' (split_fun_tac ctxt));
   6.149 +fun measurable_tac' ctxt ss facts = let
   6.150 +
   6.151 +    val imported_thms =
   6.152 +      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf) facts) @ get_all ctxt
   6.153 +
   6.154 +    fun debug_facts msg () =
   6.155 +      msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
   6.156 +        (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
   6.157 +
   6.158 +    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
   6.159 +
   6.160 +    val split_app_tac =
   6.161 +      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   6.162 +        let
   6.163 +          fun app_prefixes (Abs (n, T, (f $ g))) = let
   6.164 +                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   6.165 +              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   6.166 +            | app_prefixes _ = []
   6.167  
   6.168 -fun is_cond_formlua n thm = if length (prems_of thm) < n then false else
   6.169 -  (case nth_hol_goal thm n of
   6.170 -    (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   6.171 -  | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   6.172 -  | _ => true)
   6.173 -  handle TERM _ => true;
   6.174 +          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   6.175 +            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   6.176 +          val thy = Proof_Context.theory_of ctxt
   6.177 +          val tunify = Sign.typ_unify thy
   6.178 +          val thms = map
   6.179 +              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   6.180 +              (get_app (Context.Proof ctxt))
   6.181 +          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   6.182 +          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   6.183 +            let
   6.184 +              val inst =
   6.185 +                (Vartab.empty, ~1)
   6.186 +                |> tunify (T, thmT)
   6.187 +                |> tunify (Tf, thmTf)
   6.188 +                |> tunify (Tc, thmTc)
   6.189 +                |> Vartab.dest o fst
   6.190 +              val subst = subst_TVars (map (apsnd snd) inst)
   6.191 +            in
   6.192 +              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   6.193 +                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   6.194 +            end
   6.195 +          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   6.196 +        in if null cps then no_tac
   6.197 +            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   6.198 +              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   6.199 +        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   6.200 +        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   6.201  
   6.202 -fun measurable_tac' ctxt ss facts n =
   6.203 -  TAKE (Config.get ctxt backtrack)
   6.204 -  ((single_measurable_tac ctxt facts THEN'
   6.205 -   REPEAT o (single_measurable_tac ctxt facts APPEND'
   6.206 -             SOLVED' (fn n => COND (is_cond_formlua n) (debug_tac ctxt (K "simp") (asm_full_simp_tac ss) n) no_tac))) n);
   6.207 +    val depth_measurable_tac = REPEAT
   6.208 +      (COND (is_cond_formula 1)
   6.209 +        (debug_tac ctxt (K "simp") (SOLVED' (asm_full_simp_tac ss) 1))
   6.210 +        ((debug_tac ctxt (K "single") (resolve_tac imported_thms 1)) APPEND
   6.211 +          (split_app_tac ctxt 1) APPEND
   6.212 +          (splitter 1)))
   6.213  
   6.214 -fun measurable_tac ctxt = measurable_tac' ctxt (simpset_of ctxt);
   6.215 +  in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
   6.216 +
   6.217 +fun measurable_tac ctxt facts =
   6.218 +  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt (simpset_of ctxt) facts);
   6.219  
   6.220  val attr_add = Thm.declaration_attribute o add_thm;
   6.221  
   6.222 @@ -1612,14 +1687,17 @@
   6.223  val dest_attr : attribute context_parser =
   6.224    Scan.lift (Scan.succeed (Thm.declaration_attribute add_dest));
   6.225  
   6.226 +val app_attr : attribute context_parser =
   6.227 +  Scan.lift (Scan.succeed (Thm.declaration_attribute add_app));
   6.228 +
   6.229  val method : (Proof.context -> Method.method) context_parser =
   6.230 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts 1)));
   6.231 +  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => measurable_tac ctxt facts)));
   6.232  
   6.233  fun simproc ss redex = let
   6.234      val ctxt = Simplifier.the_context ss;
   6.235      val t = HOLogic.mk_Trueprop (term_of redex);
   6.236      fun tac {context = ctxt, ...} =
   6.237 -      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss) 1);
   6.238 +      SOLVE (measurable_tac' ctxt ss (Simplifier.prems_of ss));
   6.239    in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   6.240  
   6.241  end
   6.242 @@ -1628,6 +1706,7 @@
   6.243  
   6.244  attribute_setup measurable = {* Measurable.attr *} "declaration of measurability theorems"
   6.245  attribute_setup measurable_dest = {* Measurable.dest_attr *} "add dest rule for measurability prover"
   6.246 +attribute_setup measurable_app = {* Measurable.app_attr *} "add application rule for measurability prover"
   6.247  method_setup measurable = {* Measurable.method *} "measurability prover"
   6.248  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
   6.249  
   6.250 @@ -1646,8 +1725,7 @@
   6.251  declare
   6.252    measurable_count_space[measurable (raw)]
   6.253    measurable_ident[measurable (raw)]
   6.254 -  measurable_ident'[measurable (raw)]
   6.255 -  measurable_count_space_const[measurable (raw)]
   6.256 +  measurable_ident_sets[measurable (raw)]
   6.257    measurable_const[measurable (raw)]
   6.258    measurable_If[measurable (raw)]
   6.259    measurable_comp[measurable (raw)]
   6.260 @@ -1686,6 +1764,7 @@
   6.261    "pred M (\<lambda>x. Q x) \<Longrightarrow> pred M (\<lambda>x. P x) \<Longrightarrow> pred M (\<lambda>x. Q x = P x)"
   6.262    "pred M (\<lambda>x. f x \<in> UNIV)"
   6.263    "pred M (\<lambda>x. f x \<in> {})"
   6.264 +  "pred M (\<lambda>x. P' (f x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> {x. P' x})"
   6.265    "pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> - (B x))"
   6.266    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) - (B x))"
   6.267    "pred M (\<lambda>x. f x \<in> (A x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (B x)) \<Longrightarrow> pred M (\<lambda>x. f x \<in> (A x) \<inter> (B x))"
   6.268 @@ -1765,7 +1844,8 @@
   6.269    Int[measurable (raw)]
   6.270  
   6.271  lemma pred_in_If[measurable (raw)]:
   6.272 -  "pred M (\<lambda>x. (P x \<longrightarrow> x \<in> A x) \<and> (\<not> P x \<longrightarrow> x \<in> B x)) \<Longrightarrow> pred M (\<lambda>x. x \<in> (if P x then A x else B x))"
   6.273 +  "(P \<Longrightarrow> pred M (\<lambda>x. x \<in> A x)) \<Longrightarrow> (\<not> P \<Longrightarrow> pred M (\<lambda>x. x \<in> B x)) \<Longrightarrow>
   6.274 +    pred M (\<lambda>x. x \<in> (if P then A x else B x))"
   6.275    by auto
   6.276  
   6.277  lemma sets_range[measurable_dest]: