src/HOL/Probability/measurable.ML
author wenzelm
Tue Dec 31 14:29:16 2013 +0100 (2013-12-31)
changeset 54883 dd04a8b654fc
parent 53043 8cbfbeb566a4
child 56491 a8ccf3d6a6e4
permissions -rw-r--r--
proper context for norm_hhf and derived operations;
clarified tool context in some boundary cases;
     1 (*  Title:      HOL/Probability/measurable.ML
     2     Author:     Johannes Hölzl <hoelzl@in.tum.de>
     3 
     4 Measurability prover.
     5 *)
     6 
     7 signature MEASURABLE = 
     8 sig
     9   datatype level = Concrete | Generic
    10 
    11   val add_app : thm -> Context.generic -> Context.generic
    12   val add_dest : thm -> Context.generic -> Context.generic
    13   val add_thm : bool * level -> thm -> Context.generic -> Context.generic
    14 
    15   val measurable_tac : Proof.context -> thm list -> tactic
    16 
    17   val simproc : Proof.context -> cterm -> thm option
    18 
    19   val get : level -> Proof.context -> thm list
    20   val get_all : Proof.context -> thm list
    21 
    22   val update : (thm Item_Net.T -> thm Item_Net.T) -> level -> Context.generic -> Context.generic
    23 
    24 end ;
    25 
    26 structure Measurable : MEASURABLE =
    27 struct
    28 
    29 datatype level = Concrete | Generic;
    30 
    31 structure Data = Generic_Data
    32 (
    33   type T = {
    34     concrete_thms : thm Item_Net.T,
    35     generic_thms : thm Item_Net.T,
    36     dest_thms : thm Item_Net.T,
    37     app_thms : thm Item_Net.T }
    38   val empty = {
    39     concrete_thms = Thm.full_rules,
    40     generic_thms = Thm.full_rules,
    41     dest_thms = Thm.full_rules,
    42     app_thms = Thm.full_rules};
    43   val extend = I;
    44   fun merge ({concrete_thms = ct1, generic_thms = gt1, dest_thms = dt1, app_thms = at1 },
    45       {concrete_thms = ct2, generic_thms = gt2, dest_thms = dt2, app_thms = at2 }) = {
    46     concrete_thms = Item_Net.merge (ct1, ct2),
    47     generic_thms = Item_Net.merge (gt1, gt2),
    48     dest_thms = Item_Net.merge (dt1, dt2),
    49     app_thms = Item_Net.merge (at1, at2) };
    50 );
    51 
    52 val debug =
    53   Attrib.setup_config_bool @{binding measurable_debug} (K false)
    54 
    55 val backtrack =
    56   Attrib.setup_config_int @{binding measurable_backtrack} (K 20)
    57 
    58 val split =
    59   Attrib.setup_config_bool @{binding measurable_split} (K true)
    60 
    61 fun TAKE n tac = Seq.take n o tac
    62 
    63 fun get lv =
    64   rev o Item_Net.content o (case lv of Concrete => #concrete_thms | Generic => #generic_thms) o
    65   Data.get o Context.Proof;
    66 
    67 fun get_all ctxt = get Concrete ctxt @ get Generic ctxt;
    68 
    69 fun map_data f1 f2 f3 f4
    70   {generic_thms = t1,    concrete_thms = t2,    dest_thms = t3,    app_thms = t4} =
    71   {generic_thms = f1 t1, concrete_thms = f2 t2, dest_thms = f3 t3, app_thms = f4 t4 }
    72 
    73 fun map_concrete_thms f = map_data f I I I
    74 fun map_generic_thms f = map_data I f I I
    75 fun map_dest_thms f = map_data I I f I
    76 fun map_app_thms f = map_data I I I f
    77 
    78 fun update f lv = Data.map (case lv of Concrete => map_concrete_thms f | Generic => map_generic_thms f);
    79 fun add thms' = update (fold Item_Net.update thms');
    80 
    81 val get_dest = Item_Net.content o #dest_thms o Data.get;
    82 val add_dest = Data.map o map_dest_thms o Item_Net.update;
    83 
    84 val get_app = Item_Net.content o #app_thms o Data.get;
    85 val add_app = Data.map o map_app_thms o Item_Net.update;
    86 
    87 fun is_too_generic thm =
    88   let 
    89     val concl = concl_of thm
    90     val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
    91   in is_Var (head_of concl') end
    92 
    93 fun import_theorem ctxt thm = if is_too_generic thm then [] else
    94   [thm] @ map_filter (try (fn th' => thm RS th')) (get_dest ctxt);
    95 
    96 fun add_thm (raw, lv) thm ctxt = add (if raw then [thm] else import_theorem ctxt thm) lv ctxt;
    97 
    98 fun debug_tac ctxt msg f = if Config.get ctxt debug then print_tac (msg ()) THEN f else f
    99 
   100 fun nth_hol_goal thm i =
   101   HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (prems_of thm) (i - 1))))
   102 
   103 fun dest_measurable_fun t =
   104   (case t of
   105     (Const (@{const_name "Set.member"}, _) $ f $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => f
   106   | _ => raise (TERM ("not a measurability predicate", [t])))
   107 
   108 fun is_cond_formula n thm = if length (prems_of thm) < n then false else
   109   (case nth_hol_goal thm n of
   110     (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "sets"}, _) $ _)) => false
   111   | (Const (@{const_name "Set.member"}, _) $ _ $ (Const (@{const_name "measurable"}, _) $ _ $ _)) => false
   112   | _ => true)
   113   handle TERM _ => true;
   114 
   115 fun indep (Bound i) t b = i < b orelse t <= i
   116   | indep (f $ t) top bot = indep f top bot andalso indep t top bot
   117   | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
   118   | indep _ _ _ = true;
   119 
   120 fun cnt_prefixes ctxt (Abs (n, T, t)) = let
   121       fun is_countable t = Type.of_sort (Proof_Context.tsig_of ctxt) (t, @{sort countable})
   122       fun cnt_walk (Abs (ns, T, t)) Ts =
   123           map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
   124         | cnt_walk (f $ g) Ts = let
   125             val n = length Ts - 1
   126           in
   127             map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
   128             map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
   129             (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
   130                 andalso indep g n 0 andalso g <> Bound n
   131               then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
   132               else [])
   133           end
   134         | cnt_walk _ _ = []
   135     in map (fn (t1, t2) => let
   136         val T1 = type_of1 ([T], t2)
   137         val T2 = type_of1 ([T], t)
   138       in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
   139         [SOME T1, SOME T, SOME T2])
   140       end) (cnt_walk t [T])
   141     end
   142   | cnt_prefixes _ _ = []
   143 
   144 val split_countable_tac =
   145   Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   146     let
   147       val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
   148       fun cert f = map (Option.map (f (Proof_Context.theory_of ctxt)))
   149       fun inst t (ts, Ts) = Drule.instantiate' (cert ctyp_of Ts) (cert cterm_of ts) t
   150       val cps = cnt_prefixes ctxt f |> map (inst @{thm measurable_compose_countable})
   151     in if null cps then no_tac else debug_tac ctxt (K "split countable fun") (resolve_tac cps i) end
   152     handle TERM _ => no_tac) 1)
   153 
   154 fun measurable_tac' ctxt facts =
   155   let
   156     val imported_thms =
   157       (maps (import_theorem (Context.Proof ctxt) o Simplifier.norm_hhf ctxt) facts) @ get_all ctxt
   158 
   159     fun debug_facts msg () =
   160       msg ^ " + " ^ Pretty.str_of (Pretty.list "[" "]"
   161         (map (Syntax.pretty_term ctxt o prop_of) (maps (import_theorem (Context.Proof ctxt)) facts)));
   162 
   163     val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
   164 
   165     val split_app_tac =
   166       Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
   167         let
   168           fun app_prefixes (Abs (n, T, (f $ g))) = let
   169                 val ps = (if not (loose_bvar1 (g, 0)) then [(f, g)] else [])
   170               in map (fn (f, c) => (Abs (n, T, f), c, T, type_of c, type_of1 ([T], f $ c))) ps end
   171             | app_prefixes _ = []
   172 
   173           fun dest_app (Abs (_, T, t as ((f $ Bound 0) $ c))) = (f, c, T, type_of c, type_of1 ([T], t))
   174             | dest_app t = raise (TERM ("not a measurability predicate of an application", [t]))
   175           val thy = Proof_Context.theory_of ctxt
   176           val tunify = Sign.typ_unify thy
   177           val thms = map
   178               (fn thm => (thm, dest_app (dest_measurable_fun (HOLogic.dest_Trueprop (concl_of thm)))))
   179               (get_app (Context.Proof ctxt))
   180           fun cert f = map (fn (t, t') => (f thy t, f thy t'))
   181           fun inst (f, c, T, Tc, Tf) (thm, (thmf, thmc, thmT, thmTc, thmTf)) =
   182             let
   183               val inst =
   184                 (Vartab.empty, ~1)
   185                 |> tunify (T, thmT)
   186                 |> tunify (Tf, thmTf)
   187                 |> tunify (Tc, thmTc)
   188                 |> Vartab.dest o fst
   189               val subst = subst_TVars (map (apsnd snd) inst)
   190             in
   191               Thm.instantiate (cert ctyp_of (map (fn (n, (s, T)) => (TVar (n, s), T)) inst),
   192                 cert cterm_of [(subst thmf, f), (subst thmc, c)]) thm
   193             end
   194           val cps = map_product inst (app_prefixes (dest_measurable_fun (HOLogic.dest_Trueprop t))) thms
   195         in if null cps then no_tac
   196             else debug_tac ctxt (K ("split app fun")) (resolve_tac cps i)
   197               ORELSE debug_tac ctxt (fn () => "FAILED") no_tac end
   198         handle TERM t => debug_tac ctxt (fn () => "TERM " ^ fst t ^ Pretty.str_of (Pretty.list "[" "]" (map (Syntax.pretty_term ctxt) (snd t)))) no_tac
   199         handle Type.TUNIFY => debug_tac ctxt (fn () => "TUNIFY") no_tac) 1)
   200 
   201     fun REPEAT_cnt f n st = ((f n THEN REPEAT_cnt f (n + 1)) ORELSE all_tac) st
   202 
   203     val depth_measurable_tac = REPEAT_cnt (fn n =>
   204        (COND (is_cond_formula 1)
   205         (debug_tac ctxt (K ("simp " ^ string_of_int n)) (SOLVED' (asm_full_simp_tac ctxt) 1))
   206         ((debug_tac ctxt (K ("single " ^ string_of_int n)) (resolve_tac imported_thms 1)) APPEND
   207           (split_app_tac ctxt 1) APPEND
   208           (splitter 1)))) 0
   209 
   210   in debug_tac ctxt (debug_facts "start") depth_measurable_tac end;
   211 
   212 fun measurable_tac ctxt facts =
   213   TAKE (Config.get ctxt backtrack) (measurable_tac' ctxt facts);
   214 
   215 fun simproc ctxt redex =
   216   let
   217     val t = HOLogic.mk_Trueprop (term_of redex);
   218     fun tac {context = ctxt, prems = _ } =
   219       SOLVE (measurable_tac' ctxt (Simplifier.prems_of ctxt));
   220   in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
   221 
   222 end
   223