# HG changeset patch
# User hoelzl
# Date 1416828035 -3600
# Node ID 8d7cec9b861d8d48ee64b6f4d060d542ce7b9b1a
# Parent  db5a718e8c098450a41adbfc594ba7c2b71b79c9
cleanup measurability prover

diff -r db5a718e8c09 -r 8d7cec9b861d src/HOL/Probability/Measurable.thy
--- a/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:20:35 2014 +0100
@@ -51,23 +51,23 @@
 ML_file "measurable.ML"
 
 attribute_setup measurable = {*
-  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
-    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
+  Scan.lift (
+    (Args.add >> K true || Args.del >> K false || Scan.succeed true) --
+    Scan.optional (Args.parens (
+      Scan.optional (Args.$$$ "raw" >> K true) false --
       Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
-    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
+    (false, Measurable.Concrete) >>
+    Measurable.measurable_thm_attr)
 *} "declaration of measurability theorems"
 
-attribute_setup measurable_dest = {*
-  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
-*} "add dest rule for measurability prover"
+attribute_setup measurable_dest = Measurable.dest_thm_attr
+  "add dest rule for measurability prover"
 
-attribute_setup measurable_app = {*
-  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
-*} "add application rule for measurability prover"
+attribute_setup measurable_app = Measurable.app_thm_attr
+  "add application rule for measurability prover"
 
-method_setup measurable = {*
-  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
-*} "measurability prover"
+method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
+  "measurability prover"
 
 simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
 
diff -r db5a718e8c09 -r 8d7cec9b861d src/HOL/Probability/measurable.ML
--- a/src/HOL/Probability/measurable.ML	Mon Nov 24 12:35:13 2014 +0100
+++ b/src/HOL/Probability/measurable.ML	Mon Nov 24 12:20:35 2014 +0100
@@ -8,20 +8,16 @@
 sig
   datatype level = Concrete | Generic
 
-  val add_app : thm -> Context.generic -> Context.generic
-  val add_dest : thm -> Context.generic -> Context.generic
-  val add_thm : bool * level -> thm -> Context.generic -> Context.generic
-  val del_thm : bool * level -> thm -> Context.generic -> Context.generic
-  val add_del_thm : bool -> (bool * level) -> thm -> Context.generic -> Context.generic
+  val app_thm_attr : attribute context_parser
+  val dest_thm_attr : attribute context_parser
+  val measurable_thm_attr : bool * (bool * level) -> attribute
 
   val measurable_tac : Proof.context -> thm list -> tactic
 
   val simproc : Proof.context -> cterm -> thm option
 
-  val get : level -> Proof.context -> thm list
+  val get_thms : Proof.context -> thm list
   val get_all : Proof.context -> thm list
-
-  val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
 end ;
 
 structure Measurable : MEASURABLE =
@@ -29,23 +25,23 @@
 
 datatype level = Concrete | Generic;
 
+fun eq_measurable_thms ((th1, d1), (th2, d2)) = 
+  d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
+
 structure Data = Generic_Data
 (
   type T = {
-    concrete_thms : thm Item_Net.T,
-    generic_thms : thm Item_Net.T,
+    measurable_thms : (thm * (bool * level)) Item_Net.T,
     dest_thms : thm Item_Net.T,
     app_thms : thm Item_Net.T }
   val empty = {
-    concrete_thms = Thm.full_rules,
-    generic_thms = Thm.full_rules,
+    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 };
   val extend = I;
-  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
-      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
-    concrete_thms = Item_Net.merge (ct1, ct2),
-    generic_thms = Item_Net.merge (gt1, gt2),
+  fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1 },
+      {measurable_thms = t2, dest_thms = dt2, app_thms = at2 }) = {
+    measurable_thms = Item_Net.merge (t1, t2),
     dest_thms = Item_Net.merge (dt1, dt2),
     app_thms = Item_Net.merge (at1, at2) };
 );
@@ -53,38 +49,36 @@
 val debug =
   Attrib.setup_config_bool @{binding measurable_debug} (K false)
 
-val backtrack =
-  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
-
 val split =
   Attrib.setup_config_bool @{binding measurable_split} (K true)
 
-fun TAKE n tac = Seq.take n o tac
+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 get lv =
-  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
-  Data.get o Context.Proof;
-
-fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
+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_data f1 f2 f3 f4
-  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
-  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
+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
 
-fun map_concrete_thms f = map_data f I I I
-fun map_generic_thms f = map_data I f I I
-fun map_dest_thms f = map_data I I f I
-fun map_app_thms f = map_data I I I f
+val dest_thm_attr = generic_add_del map_dest_thms
 
-fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
-fun add thms' = update (fold Item_Net.update thms');
-fun del thms' = update (fold Item_Net.remove thms');
+fun del_thm th net =
+  let
+    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
+  in fold Item_Net.remove thms net end ;
+
+fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
+  (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 add_dest = Data.map o map_dest_thms o Item_Net.update;
-
 val get_app = Item_Net.content o #app_thms o Data.get;
-val add_app = Data.map o map_app_thms o Item_Net.update;
 
 fun is_too_generic thm =
   let 
@@ -95,12 +89,18 @@
 fun import_theorem ctxt thm = if is_too_generic thm then [] else
   [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
 
-fun add_del_thm_gen f (raw, lv) thm ctxt = f (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
+val get = Context.Proof #> Data.get #> #measurable_thms #> Item_Net.content ;
+
+val get_all = get #> map fst ;
 
-val add_thm = add_del_thm_gen add;
-val del_thm = add_del_thm_gen del;
-fun add_del_thm true = add_thm
-  | add_del_thm false = del_thm
+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;
 
 fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
 
@@ -158,10 +158,46 @@
     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)
 
-fun measurable_tac' ctxt facts =
+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_all ctxt
+      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_thms ctxt
 
     fun debug_facts msg () =
       msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
@@ -169,42 +205,6 @@
 
     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 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 REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
 
     val depth_measurable_tac = REPEAT_cnt (fn n =>
@@ -216,14 +216,11 @@
 
   in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
 
-fun measurable_tac ctxt facts =
-  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
-
 fun simproc ctxt redex =
   let
     val t = HOLogic.mk_Trueprop (term_of redex);
     fun tac {context = ctxt, prems = _ } =
-      SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt));
+      SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
   in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
 
 end