measurability prover: removed app splitting, replaced by more powerful destruction rules

--- 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 "(\<lambda>x. (f x, g x)) -` (A \<times> B) \<inter> space M \<in> sets M" .
 qed
 
-lemma measurable_Pair_compose_split[measurable_dest]:
-  assumes f: "split f \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
-  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
-  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
-  using measurable_compose[OF measurable_Pair f, OF g h] by simp
-
-lemma measurable_pair:
-  assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
-  shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
-  using measurable_Pair[OF assms] by simp
-
 lemma measurable_fst[intro!, simp, measurable]: "fst \<in> measurable (M1 \<Otimes>\<^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 \<in> measurable (M1 \<Otimes>\<^sub>M M2) N"
+  assumes g: "g \<in> measurable M M1" and h: "h \<in> measurable M M2"
+  shows "(\<lambda>x. f (g x) (h x)) \<in> measurable M N"
+  using measurable_compose[OF measurable_Pair f, OF g h] by simp
+
+lemma measurable_Pair1_compose[measurable_dest]:
+  assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
+  assumes [measurable]: "h \<in> measurable N M"
+  shows "(\<lambda>x. f (h x)) \<in> measurable N M1"
+  using measurable_compose[OF f measurable_fst] by simp
+
+lemma measurable_Pair2_compose[measurable_dest]:
+  assumes f: "(\<lambda>x. (f x, g x)) \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
+  assumes [measurable]: "h \<in> measurable N M"
+  shows "(\<lambda>x. g (h x)) \<in> measurable N M2"
+  using measurable_compose[OF f measurable_snd] by simp
+
+lemma measurable_pair:
+  assumes "(fst \<circ> f) \<in> measurable M M1" "(snd \<circ> f) \<in> measurable M M2"
+  shows "f \<in> measurable M (M1 \<Otimes>\<^sub>M M2)"
+  using measurable_Pair[OF assms] by simp
+
 lemma 
   assumes f[measurable]: "f \<in> measurable M (N \<Otimes>\<^sub>M P)" 
   shows measurable_fst': "(\<lambda>x. fst (f x)) \<in> measurable M N"
@@ -276,15 +288,13 @@
   show "countably_additive (sets (N \<Otimes>\<^sub>M M)) ?\<mu>"
   proof (rule countably_additiveI)
     fix F :: "nat \<Rightarrow> ('b \<times> 'a) set" assume F: "range F \<subseteq> sets (N \<Otimes>\<^sub>M M)" "disjoint_family F"
-    from F have *: "\<And>i. F i \<in> sets (N \<Otimes>\<^sub>M M)" "(\<Union>i. F i) \<in> sets (N \<Otimes>\<^sub>M M)" by auto
-    moreover from F have "\<And>i. (\<lambda>x. emeasure M (Pair x -` F i)) \<in> borel_measurable N"
-      by (intro measurable_emeasure_Pair) auto
+    from F have *: "\<And>i. F i \<in> sets (N \<Otimes>\<^sub>M M)" by auto
     moreover have "\<And>x. disjoint_family (\<lambda>i. Pair x -` F i)"
       by (intro disjoint_family_on_bisimulation[OF F(2)]) auto
     moreover have "\<And>x. range (\<lambda>i. Pair x -` F i) \<subseteq> sets M"
       using F by (auto simp: sets_Pair1)
     ultimately show "(\<Sum>n. ?\<mu> (F n)) = ?\<mu> (\<Union>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 \<times> b |a b. a \<in> sets N \<and> b \<in> sets M} \<subseteq> Pow (space N \<times> space M)"

--- 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 \<Longrightarrow> f \<in> 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 \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
+  using borel_measurable_has_bochner_integral[measurable] by measurable
 
 lemma has_bochner_integral_simple_bochner_integrable:
   "simple_bochner_integrable M f \<Longrightarrow> has_bochner_integral M f (simple_bochner_integral M f)"
@@ -922,6 +926,10 @@
 lemma borel_measurable_integrable[measurable_dest]: "integrable M f \<Longrightarrow> f \<in> borel_measurable M"
   by (auto elim: integrable.cases has_bochner_integral.cases)
 
+lemma borel_measurable_integrable'[measurable_dest]:
+  "integrable M f \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
+  using borel_measurable_integrable[measurable] by measurable
+
 lemma integrable_cong:
   "M = N \<Longrightarrow> (\<And>x. x \<in> space N \<Longrightarrow> f x = g x) \<Longrightarrow> integrable M f \<longleftrightarrow> 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) (\<lambda>x. (\<Prod>i\<in>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 \<in> borel_measurable (Pi\<^sub>M I M)"
     using assms by simp
   have "(\<integral>\<^sup>+ x. ereal (norm (\<Prod>i\<in>I. f i (x i))) \<partial>Pi\<^sub>M I M) = 
@@ -2854,3 +2863,4 @@
 hide_const simple_bochner_integrable
 
 end
+

--- 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 \<in> borel_measurable M" by auto
 qed auto
 
+lemma borel_measurable_erealD[measurable_dest]:
+  "(\<lambda>x. ereal (f x)) \<in> borel_measurable M \<Longrightarrow> g \<in> measurable N M \<Longrightarrow> (\<lambda>x. f (g x)) \<in> borel_measurable N"
+  unfolding borel_measurable_ereal_iff by simp
+
 lemma borel_measurable_ereal_iff_real:
   fixes f :: "'a \<Rightarrow> ereal"
   shows "f \<in> borel_measurable M \<longleftrightarrow>

--- 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) \<in> 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 \<in> I" shows "(\<lambda>x. x i) \<in> measurable (Pi\<^sub>M I M) (M i)"
 proof (unfold measurable_def, intro CollectI conjI ballI)
   fix A assume "A \<in> sets (M i)"
@@ -551,13 +551,14 @@
     using `A \<in> sets (M i)` `i \<in> I` by (auto intro!: sets_PiM_I)
 qed (insert `i \<in> I`, auto simp: space_PiM)
 
-lemma measurable_component_singleton'[measurable_app]:
+lemma measurable_component_singleton'[measurable_dest]:
   assumes f: "f \<in> measurable N (Pi\<^sub>M I M)"
+  assumes g: "g \<in> measurable L N"
   assumes i: "i \<in> I"
-  shows "(\<lambda>x. (f x) i) \<in> measurable N (M i)"
-  using measurable_compose[OF f measurable_component_singleton, OF i] .
+  shows "(\<lambda>x. (f (g x)) i) \<in> 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 \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<lambda>x. f (x i)) \<in> measurable (PiM I M) N"
   by simp
 

--- 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]

--- 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 (\<lambda>x. ereal (f x)) \<Longrightarrow> (AE x in N. 0 \<le> f x)"
   by (simp_all add: distributed_def borel_measurable_ereal_iff)
 
-lemma
-  assumes D: "distributed M N X (\<lambda>x. ereal (f x))"
-  shows distributed_real_measurable'[measurable_dest]:
-      "h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
-  using distributed_real_measurable[OF D]
-  by simp_all
+lemma distributed_real_measurable':
+  "distributed M N X (\<lambda>x. ereal (f x)) \<Longrightarrow> h \<in> measurable L N \<Longrightarrow> (\<lambda>x. f (h x)) \<in> borel_measurable L"
+  by simp
 
-lemma
-  assumes D: "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f"
-  shows joint_distributed_measurable1[measurable_dest]:
-      "h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
-    and joint_distributed_measurable2[measurable_dest]:
-      "h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> 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 \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h1 \<in> measurable N M \<Longrightarrow> (\<lambda>x. X (h1 x)) \<in> measurable N S"
+  by simp
+
+lemma joint_distributed_measurable2:
+  "distributed M (S \<Otimes>\<^sub>M T) (\<lambda>x. (X x, Y x)) f \<Longrightarrow> h2 \<in> measurable N M \<Longrightarrow> (\<lambda>x. Y (h2 x)) \<in> measurable N T"
+  by simp
 
 lemma distributed_count_space:
   assumes X: "distributed M (count_space A) X P" and a: "a \<in> A" and A: "finite A"

--- 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 \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
 
-    val dests = get_dest (Context.Proof ctxt)
-    fun prep_dest thm =
-      (if is_too_generic thm then [] else [thm] @ map_filter (try (fn th' => thm RS th')) dests) ;
-    val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ;
-    fun preprocess_thm (thm, raw) =
-      if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat
-    
-    fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ;
-    fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ;
-    val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic
-
-    val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat
+    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))