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