cleanup measurability prover
authorhoelzl
Mon Nov 24 12:20:35 2014 +0100 (2014-11-24)
changeset 590478d7cec9b861d
parent 59046 db5a718e8c09
child 59048 7dc8ac6f0895
cleanup measurability prover
src/HOL/Probability/Measurable.thy
src/HOL/Probability/measurable.ML
     1.1 --- a/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:35:13 2014 +0100
     1.2 +++ b/src/HOL/Probability/Measurable.thy	Mon Nov 24 12:20:35 2014 +0100
     1.3 @@ -51,23 +51,23 @@
     1.4  ML_file "measurable.ML"
     1.5  
     1.6  attribute_setup measurable = {*
     1.7 -  Scan.lift (Scan.optional (Args.$$$ "del" >> K false) true --
     1.8 -    Scan.optional (Args.parens (Scan.optional (Args.$$$ "raw" >> K true) false --
     1.9 +  Scan.lift (
    1.10 +    (Args.add >> K true || Args.del >> K false || Scan.succeed true) --
    1.11 +    Scan.optional (Args.parens (
    1.12 +      Scan.optional (Args.$$$ "raw" >> K true) false --
    1.13        Scan.optional (Args.$$$ "generic" >> K Measurable.Generic) Measurable.Concrete))
    1.14 -    (false, Measurable.Concrete) >> (Thm.declaration_attribute o uncurry Measurable.add_del_thm))
    1.15 +    (false, Measurable.Concrete) >>
    1.16 +    Measurable.measurable_thm_attr)
    1.17  *} "declaration of measurability theorems"
    1.18  
    1.19 -attribute_setup measurable_dest = {*
    1.20 -  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_dest))
    1.21 -*} "add dest rule for measurability prover"
    1.22 +attribute_setup measurable_dest = Measurable.dest_thm_attr
    1.23 +  "add dest rule for measurability prover"
    1.24  
    1.25 -attribute_setup measurable_app = {*
    1.26 -  Scan.lift (Scan.succeed (Thm.declaration_attribute Measurable.add_app))
    1.27 -*} "add application rule for measurability prover"
    1.28 +attribute_setup measurable_app = Measurable.app_thm_attr
    1.29 +  "add application rule for measurability prover"
    1.30  
    1.31 -method_setup measurable = {*
    1.32 -  Scan.lift (Scan.succeed (fn ctxt => METHOD (fn facts => Measurable.measurable_tac ctxt facts)))
    1.33 -*} "measurability prover"
    1.34 +method_setup measurable = \<open> Scan.lift (Scan.succeed (METHOD o Measurable.measurable_tac)) \<close>
    1.35 +  "measurability prover"
    1.36  
    1.37  simproc_setup measurable ("A \<in> sets M" | "f \<in> measurable M N") = {* K Measurable.simproc *}
    1.38  
     2.1 --- a/src/HOL/Probability/measurable.ML	Mon Nov 24 12:35:13 2014 +0100
     2.2 +++ b/src/HOL/Probability/measurable.ML	Mon Nov 24 12:20:35 2014 +0100
     2.3 @@ -8,20 +8,16 @@
     2.4  sig
     2.5    datatype level = Concrete | Generic
     2.6  
     2.7 -  val add_app : thm -> Context.generic -> Context.generic
     2.8 -  val add_dest : thm -> Context.generic -> Context.generic
     2.9 -  val add_thm : bool * level -> thm -> Context.generic -> Context.generic
    2.10 -  val del_thm : bool * level -> thm -> Context.generic -> Context.generic
    2.11 -  val add_del_thm : bool -> (bool * level) -> thm -> Context.generic -> Context.generic
    2.12 +  val app_thm_attr : attribute context_parser
    2.13 +  val dest_thm_attr : attribute context_parser
    2.14 +  val measurable_thm_attr : bool * (bool * level) -> attribute
    2.15  
    2.16    val measurable_tac : Proof.context -> thm list -> tactic
    2.17  
    2.18    val simproc : Proof.context -> cterm -> thm option
    2.19  
    2.20 -  val get : level -> Proof.context -> thm list
    2.21 +  val get_thms : Proof.context -> thm list
    2.22    val get_all : Proof.context -> thm list
    2.23 -
    2.24 -  val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
    2.25  end ;
    2.26  
    2.27  structure Measurable : MEASURABLE =
    2.28 @@ -29,23 +25,23 @@
    2.29  
    2.30  datatype level = Concrete | Generic;
    2.31  
    2.32 +fun eq_measurable_thms ((th1, d1), (th2, d2)) = 
    2.33 +  d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
    2.34 +
    2.35  structure Data = Generic_Data
    2.36  (
    2.37    type T = {
    2.38 -    concrete_thms : thm Item_Net.T,
    2.39 -    generic_thms : thm Item_Net.T,
    2.40 +    measurable_thms : (thm * (bool * level)) Item_Net.T,
    2.41      dest_thms : thm Item_Net.T,
    2.42      app_thms : thm Item_Net.T }
    2.43    val empty = {
    2.44 -    concrete_thms = Thm.full_rules,
    2.45 -    generic_thms = Thm.full_rules,
    2.46 +    measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
    2.47      dest_thms = Thm.full_rules,
    2.48 -    app_thms = Thm.full_rules};
    2.49 +    app_thms = Thm.full_rules };
    2.50    val extend = I;
    2.51 -  fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
    2.52 -      {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
    2.53 -    concrete_thms = Item_Net.merge (ct1, ct2),
    2.54 -    generic_thms = Item_Net.merge (gt1, gt2),
    2.55 +  fun merge ({measurable_thms = t1, dest_thms = dt1, app_thms = at1 },
    2.56 +      {measurable_thms = t2, dest_thms = dt2, app_thms = at2 }) = {
    2.57 +    measurable_thms = Item_Net.merge (t1, t2),
    2.58      dest_thms = Item_Net.merge (dt1, dt2),
    2.59      app_thms = Item_Net.merge (at1, at2) };
    2.60  );
    2.61 @@ -53,38 +49,36 @@
    2.62  val debug =
    2.63    Attrib.setup_config_bool @{binding measurable_debug} (K false)
    2.64  
    2.65 -val backtrack =
    2.66 -  Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
    2.67 -
    2.68  val split =
    2.69    Attrib.setup_config_bool @{binding measurable_split} (K true)
    2.70  
    2.71 -fun TAKE n tac = Seq.take n o tac
    2.72 +fun map_data f1 f2 f3
    2.73 +  {measurable_thms = t1,    dest_thms = t2,    app_thms = t3} =
    2.74 +  {measurable_thms = f1 t1, dest_thms = f2 t2, app_thms = f3 t3 }
    2.75  
    2.76 -fun get lv =
    2.77 -  rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
    2.78 -  Data.get o Context.Proof;
    2.79 -
    2.80 -fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
    2.81 +fun map_measurable_thms f = map_data f I I
    2.82 +fun map_dest_thms f = map_data I f I
    2.83 +fun map_app_thms f = map_data I I f
    2.84  
    2.85 -fun map_data f1 f2 f3 f4
    2.86 -  {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
    2.87 -  {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
    2.88 +fun generic_add_del map = 
    2.89 +  Scan.lift
    2.90 +    (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
    2.91 +    (fn f => Thm.declaration_attribute (Data.map o map o f))
    2.92 +
    2.93 +val app_thm_attr = generic_add_del map_app_thms
    2.94  
    2.95 -fun map_concrete_thms f = map_data f I I I
    2.96 -fun map_generic_thms f = map_data I f I I
    2.97 -fun map_dest_thms f = map_data I I f I
    2.98 -fun map_app_thms f = map_data I I I f
    2.99 +val dest_thm_attr = generic_add_del map_dest_thms
   2.100  
   2.101 -fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
   2.102 -fun add thms' = update (fold Item_Net.update thms');
   2.103 -fun del thms' = update (fold Item_Net.remove thms');
   2.104 +fun del_thm th net =
   2.105 +  let
   2.106 +    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
   2.107 +  in fold Item_Net.remove thms net end ;
   2.108 +
   2.109 +fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
   2.110 +  (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm))
   2.111  
   2.112  val get_dest = Item_Net.content o #dest_thms o Data.get;
   2.113 -val add_dest = Data.map o map_dest_thms o Item_Net.update;
   2.114 -
   2.115  val get_app = Item_Net.content o #app_thms o Data.get;
   2.116 -val add_app = Data.map o map_app_thms o Item_Net.update;
   2.117  
   2.118  fun is_too_generic thm =
   2.119    let 
   2.120 @@ -95,12 +89,18 @@
   2.121  fun import_theorem ctxt thm = if is_too_generic thm then [] else
   2.122    [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
   2.123  
   2.124 -fun add_del_thm_gen f (raw, lv) thm ctxt = f (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
   2.125 +val get = Context.Proof #> Data.get #> #measurable_thms #> Item_Net.content ;
   2.126 +
   2.127 +val get_all = get #> map fst ;
   2.128  
   2.129 -val add_thm = add_del_thm_gen add;
   2.130 -val del_thm = add_del_thm_gen del;
   2.131 -fun add_del_thm true = add_thm
   2.132 -  | add_del_thm false = del_thm
   2.133 +fun get_thms ctxt =
   2.134 +  let
   2.135 +    val thms = ctxt |> get |> rev ;
   2.136 +    fun get lv = map_filter (fn (th, (rw, lv')) => if lv = lv' then SOME (th, rw) else NONE) thms
   2.137 +  in
   2.138 +    get Concrete @ get Generic |>
   2.139 +    maps (fn (th, rw) => if rw then [th] else import_theorem (Context.Proof ctxt) th)
   2.140 +  end;
   2.141  
   2.142  fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
   2.143  
   2.144 @@ -158,10 +158,46 @@
   2.145      in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
   2.146      handle TERM _ => no_tac) 1)
   2.147  
   2.148 -fun measurable_tac' ctxt facts =
   2.149 +val split_app_tac =
   2.150 +  Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   2.151 +    let
   2.152 +      fun app_prefixes (Abs (n, T, (f $ g))) = let
   2.153 +            val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   2.154 +          in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   2.155 +        | app_prefixes _ = []
   2.156 +
   2.157 +      fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   2.158 +        | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   2.159 +      val thy = Proof_Context.theory_of ctxt
   2.160 +      val tunify = Sign.typ_unify thy
   2.161 +      val thms = map
   2.162 +          (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   2.163 +          (get_app (Context.Proof ctxt))
   2.164 +      fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   2.165 +      fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   2.166 +        let
   2.167 +          val inst =
   2.168 +            (Vartab.empty, ~1)
   2.169 +            |> tunify (T, thmT)
   2.170 +            |> tunify (Tf, thmTf)
   2.171 +            |> tunify (Tc, thmTc)
   2.172 +            |> Vartab.dest o fst
   2.173 +          val subst = subst_TVars (map (apsnd snd) inst)
   2.174 +        in
   2.175 +          Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   2.176 +            cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   2.177 +        end
   2.178 +      val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   2.179 +    in if null cps then no_tac
   2.180 +        else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   2.181 +          ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   2.182 +    handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   2.183 +    handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   2.184 +
   2.185 +fun measurable_tac ctxt facts =
   2.186    let
   2.187      val imported_thms =
   2.188 -      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
   2.189 +      (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_thms ctxt
   2.190  
   2.191      fun debug_facts msg () =
   2.192        msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
   2.193 @@ -169,42 +205,6 @@
   2.194  
   2.195      val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
   2.196  
   2.197 -    val split_app_tac =
   2.198 -      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   2.199 -        let
   2.200 -          fun app_prefixes (Abs (n, T, (f $ g))) = let
   2.201 -                val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   2.202 -              in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   2.203 -            | app_prefixes _ = []
   2.204 -
   2.205 -          fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   2.206 -            | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   2.207 -          val thy = Proof_Context.theory_of ctxt
   2.208 -          val tunify = Sign.typ_unify thy
   2.209 -          val thms = map
   2.210 -              (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   2.211 -              (get_app (Context.Proof ctxt))
   2.212 -          fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   2.213 -          fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   2.214 -            let
   2.215 -              val inst =
   2.216 -                (Vartab.empty, ~1)
   2.217 -                |> tunify (T, thmT)
   2.218 -                |> tunify (Tf, thmTf)
   2.219 -                |> tunify (Tc, thmTc)
   2.220 -                |> Vartab.dest o fst
   2.221 -              val subst = subst_TVars (map (apsnd snd) inst)
   2.222 -            in
   2.223 -              Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   2.224 -                cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   2.225 -            end
   2.226 -          val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   2.227 -        in if null cps then no_tac
   2.228 -            else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   2.229 -              ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   2.230 -        handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   2.231 -        handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   2.232 -
   2.233      fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
   2.234  
   2.235      val depth_measurable_tac = REPEAT_cnt (fn n =>
   2.236 @@ -216,14 +216,11 @@
   2.237  
   2.238    in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
   2.239  
   2.240 -fun measurable_tac ctxt facts =
   2.241 -  TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
   2.242 -
   2.243  fun simproc ctxt redex =
   2.244    let
   2.245      val t = HOLogic.mk_Trueprop (term_of redex);
   2.246      fun tac {context = ctxt, prems = _ } =
   2.247 -      SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt));
   2.248 +      SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
   2.249    in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   2.250  
   2.251  end