src/HOL/Analysis/measurable.ML
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (4 weeks ago)
changeset 69981 3dced198b9ec
parent 69597 ff784d5a5bfb
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/measurable.ML
hoelzl@50387
     2
    Author:     Johannes Hölzl <hoelzl@in.tum.de>
hoelzl@50387
     3
hoelzl@50387
     4
Measurability prover.
hoelzl@50387
     5
*)
hoelzl@50387
     6
hoelzl@50387
     7
signature MEASURABLE = 
hoelzl@50387
     8
sig
hoelzl@59048
     9
  type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
hoelzl@59048
    10
hoelzl@50387
    11
  datatype level = Concrete | Generic
hoelzl@50387
    12
hoelzl@59047
    13
  val dest_thm_attr : attribute context_parser
hoelzl@59048
    14
  val cong_thm_attr : attribute context_parser
hoelzl@59047
    15
  val measurable_thm_attr : bool * (bool * level) -> attribute
wenzelm@53043
    16
hoelzl@59048
    17
  val add_del_cong_thm : bool -> thm -> Context.generic -> Context.generic ;
hoelzl@59048
    18
hoelzl@59048
    19
  val get_all : Context.generic -> thm list
hoelzl@59048
    20
  val get_dest : Context.generic -> thm list
hoelzl@59048
    21
  val get_cong : Context.generic -> thm list
hoelzl@59048
    22
hoelzl@50387
    23
  val measurable_tac : Proof.context -> thm list -> tactic
hoelzl@50387
    24
wenzelm@53043
    25
  val simproc : Proof.context -> cterm -> thm option
hoelzl@50387
    26
hoelzl@59048
    27
  val add_preprocessor : string -> preprocessor -> Context.generic -> Context.generic
hoelzl@59048
    28
  val del_preprocessor : string -> Context.generic -> Context.generic
hoelzl@59048
    29
  val add_local_cong : thm -> Proof.context -> Proof.context
hoelzl@59353
    30
hoelzl@59353
    31
  val prepare_facts : Proof.context -> thm list -> (thm list * Proof.context)
hoelzl@50387
    32
end ;
hoelzl@50387
    33
hoelzl@50387
    34
structure Measurable : MEASURABLE =
hoelzl@50387
    35
struct
hoelzl@50387
    36
hoelzl@59048
    37
type preprocessor = thm -> Proof.context -> (thm list * Proof.context)
hoelzl@59048
    38
hoelzl@50387
    39
datatype level = Concrete | Generic;
hoelzl@50387
    40
hoelzl@59047
    41
fun eq_measurable_thms ((th1, d1), (th2, d2)) = 
hoelzl@59047
    42
  d1 = d2 andalso Thm.eq_thm_prop (th1, th2) ;
hoelzl@59047
    43
hoelzl@59048
    44
fun merge_dups (xs:(string * preprocessor) list) ys =
hoelzl@59048
    45
  xs @ (filter (fn (name, _) => is_none (find_first (fn (name', _) => name' = name) xs)) ys) 
hoelzl@59048
    46
hoelzl@50387
    47
structure Data = Generic_Data
hoelzl@50387
    48
(
hoelzl@50387
    49
  type T = {
hoelzl@59047
    50
    measurable_thms : (thm * (bool * level)) Item_Net.T,
hoelzl@50387
    51
    dest_thms : thm Item_Net.T,
hoelzl@59048
    52
    cong_thms : thm Item_Net.T,
hoelzl@59048
    53
    preprocessors : (string * preprocessor) list }
wenzelm@59992
    54
  val empty: T = {
hoelzl@59047
    55
    measurable_thms = Item_Net.init eq_measurable_thms (single o Thm.prop_of o fst),
hoelzl@50387
    56
    dest_thms = Thm.full_rules,
hoelzl@59048
    57
    cong_thms = Thm.full_rules,
hoelzl@59048
    58
    preprocessors = [] };
hoelzl@50387
    59
  val extend = I;
hoelzl@59353
    60
  fun merge ({measurable_thms = t1, dest_thms = dt1, cong_thms = ct1, preprocessors = i1 },
wenzelm@59992
    61
      {measurable_thms = t2, dest_thms = dt2, cong_thms = ct2, preprocessors = i2 }) : T = {
hoelzl@59047
    62
    measurable_thms = Item_Net.merge (t1, t2),
hoelzl@50387
    63
    dest_thms = Item_Net.merge (dt1, dt2),
hoelzl@59048
    64
    cong_thms = Item_Net.merge (ct1, ct2),
hoelzl@59048
    65
    preprocessors = merge_dups i1 i2 
hoelzl@59048
    66
    };
hoelzl@50387
    67
);
hoelzl@50387
    68
hoelzl@50387
    69
val debug =
wenzelm@69597
    70
  Attrib.setup_config_bool \<^binding>\<open>measurable_debug\<close> (K false)
hoelzl@50387
    71
hoelzl@50387
    72
val split =
wenzelm@69597
    73
  Attrib.setup_config_bool \<^binding>\<open>measurable_split\<close> (K true)
hoelzl@50387
    74
hoelzl@59353
    75
fun map_data f1 f2 f3 f4
hoelzl@59353
    76
  {measurable_thms = t1,    dest_thms = t2,    cong_thms = t3,    preprocessors = t4 } =
hoelzl@59353
    77
  {measurable_thms = f1 t1, dest_thms = f2 t2, cong_thms = f3 t3, preprocessors = f4 t4}
hoelzl@50387
    78
hoelzl@59353
    79
fun map_measurable_thms f = map_data f I I I
hoelzl@59353
    80
fun map_dest_thms f = map_data I f I I
hoelzl@59353
    81
fun map_cong_thms f = map_data I I f I
hoelzl@59353
    82
fun map_preprocessors f = map_data I I I f
hoelzl@50387
    83
wenzelm@59992
    84
fun generic_add_del map : attribute context_parser =
hoelzl@59047
    85
  Scan.lift
hoelzl@59047
    86
    (Args.add >> K Item_Net.update || Args.del >> K Item_Net.remove || Scan.succeed Item_Net.update) >>
hoelzl@59047
    87
    (fn f => Thm.declaration_attribute (Data.map o map o f))
hoelzl@59047
    88
hoelzl@59047
    89
val dest_thm_attr = generic_add_del map_dest_thms
hoelzl@50387
    90
hoelzl@59048
    91
val cong_thm_attr = generic_add_del map_cong_thms
hoelzl@59048
    92
hoelzl@59047
    93
fun del_thm th net =
hoelzl@59047
    94
  let
hoelzl@59047
    95
    val thms = net |> Item_Net.content |> filter (fn (th', _) => Thm.eq_thm (th, th'))
hoelzl@59047
    96
  in fold Item_Net.remove thms net end ;
hoelzl@59047
    97
hoelzl@59047
    98
fun measurable_thm_attr (do_add, d) = Thm.declaration_attribute
hoelzl@59047
    99
  (Data.map o map_measurable_thms o (if do_add then Item_Net.update o rpair d else del_thm))
hoelzl@50387
   100
hoelzl@50387
   101
val get_dest = Item_Net.content o #dest_thms o Data.get;
hoelzl@50387
   102
hoelzl@59048
   103
val get_cong = Item_Net.content o #cong_thms o Data.get;
hoelzl@59048
   104
val add_cong = Data.map o map_cong_thms o Item_Net.update;
hoelzl@59048
   105
val del_cong = Data.map o map_cong_thms o Item_Net.remove;
hoelzl@59048
   106
fun add_del_cong_thm true = add_cong
hoelzl@59048
   107
  | add_del_cong_thm false = del_cong
hoelzl@59048
   108
hoelzl@59048
   109
fun add_preprocessor name f = Data.map (map_preprocessors (fn xs => xs @ [(name, f)]))
hoelzl@59048
   110
fun del_preprocessor name = Data.map (map_preprocessors (filter (fn (n, _) => n <> name)))
hoelzl@59048
   111
val add_local_cong = Context.proof_map o add_cong
hoelzl@59048
   112
hoelzl@59048
   113
val get_preprocessors = Context.Proof #> Data.get #> #preprocessors ;
hoelzl@59048
   114
hoelzl@50387
   115
fun is_too_generic thm =
hoelzl@50387
   116
  let 
wenzelm@59582
   117
    val concl = Thm.concl_of thm
hoelzl@50387
   118
    val concl' = HOLogic.dest_Trueprop concl handle TERM _ => concl
hoelzl@50387
   119
  in is_Var (head_of concl') end
hoelzl@50387
   120
hoelzl@59048
   121
val get_thms = Data.get #> #measurable_thms #> Item_Net.content ;
Andreas@58965
   122
hoelzl@59048
   123
val get_all = get_thms #> map fst ;
hoelzl@50387
   124
hoelzl@59048
   125
fun debug_tac ctxt msg f =
hoelzl@59048
   126
  if Config.get ctxt debug then print_tac ctxt (msg ()) THEN f else f
hoelzl@50387
   127
hoelzl@50387
   128
fun nth_hol_goal thm i =
wenzelm@59582
   129
  HOLogic.dest_Trueprop (Logic.strip_imp_concl (strip_all_body (nth (Thm.prems_of thm) (i - 1))))
hoelzl@50387
   130
hoelzl@50387
   131
fun dest_measurable_fun t =
hoelzl@50387
   132
  (case t of
wenzelm@69597
   133
    (Const (\<^const_name>\<open>Set.member\<close>, _) $ f $ (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) => f
hoelzl@50387
   134
  | _ => raise (TERM ("not a measurability predicate", [t])))
hoelzl@50387
   135
wenzelm@59582
   136
fun not_measurable_prop n thm =
wenzelm@59582
   137
  if length (Thm.prems_of thm) < n then false
wenzelm@59582
   138
  else
wenzelm@59582
   139
    (case nth_hol_goal thm n of
wenzelm@69597
   140
      (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (Const (\<^const_name>\<open>sets\<close>, _) $ _)) => false
wenzelm@69597
   141
    | (Const (\<^const_name>\<open>Set.member\<close>, _) $ _ $ (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) => false
wenzelm@59582
   142
    | _ => true)
wenzelm@59582
   143
    handle TERM _ => true;
hoelzl@50387
   144
hoelzl@50387
   145
fun indep (Bound i) t b = i < b orelse t <= i
hoelzl@50387
   146
  | indep (f $ t) top bot = indep f top bot andalso indep t top bot
hoelzl@50387
   147
  | indep (Abs (_,_,t)) top bot = indep t (top + 1) (bot + 1)
hoelzl@50387
   148
  | indep _ _ _ = true;
hoelzl@50387
   149
wenzelm@59837
   150
fun cnt_prefixes ctxt (Abs (n, T, t)) =
wenzelm@59837
   151
    let
wenzelm@69597
   152
      fun is_countable ty = Sign.of_sort (Proof_Context.theory_of ctxt) (ty, \<^sort>\<open>countable\<close>)
hoelzl@50387
   153
      fun cnt_walk (Abs (ns, T, t)) Ts =
hoelzl@50387
   154
          map (fn (t', t'') => (Abs (ns, T, t'), t'')) (cnt_walk t (T::Ts))
hoelzl@50387
   155
        | cnt_walk (f $ g) Ts = let
hoelzl@50387
   156
            val n = length Ts - 1
hoelzl@50387
   157
          in
hoelzl@50387
   158
            map (fn (f', t) => (f' $ g, t)) (cnt_walk f Ts) @
hoelzl@50387
   159
            map (fn (g', t) => (f $ g', t)) (cnt_walk g Ts) @
hoelzl@50387
   160
            (if is_countable (type_of1 (Ts, g)) andalso loose_bvar1 (g, n)
hoelzl@50387
   161
                andalso indep g n 0 andalso g <> Bound n
hoelzl@50387
   162
              then [(f $ Bound (n + 1), incr_boundvars (~ n) g)]
hoelzl@50387
   163
              else [])
hoelzl@50387
   164
          end
hoelzl@50387
   165
        | cnt_walk _ _ = []
hoelzl@50387
   166
    in map (fn (t1, t2) => let
hoelzl@50387
   167
        val T1 = type_of1 ([T], t2)
hoelzl@50387
   168
        val T2 = type_of1 ([T], t)
hoelzl@50387
   169
      in ([SOME (Abs (n, T1, Abs (n, T, t1))), NONE, NONE, SOME (Abs (n, T, t2))],
hoelzl@50387
   170
        [SOME T1, SOME T, SOME T2])
hoelzl@50387
   171
      end) (cnt_walk t [T])
hoelzl@50387
   172
    end
hoelzl@50387
   173
  | cnt_prefixes _ _ = []
hoelzl@50387
   174
hoelzl@59353
   175
fun apply_dests thm dests =
hoelzl@59353
   176
  let
hoelzl@59353
   177
    fun apply thm th' =
hoelzl@59353
   178
      let
hoelzl@59353
   179
        val th'' = thm RS th'
hoelzl@59353
   180
      in [th''] @ loop th'' end
hoelzl@59353
   181
      handle (THM _) => []
hoelzl@59353
   182
    and loop thm =
hoelzl@59353
   183
      flat (map (apply thm) dests)
hoelzl@59353
   184
  in
hoelzl@59353
   185
    [thm] @ ([thm RS @{thm measurable_compose_rev}] handle (THM _) => []) @ loop thm
hoelzl@59353
   186
  end
hoelzl@59353
   187
hoelzl@59353
   188
fun prepare_facts ctxt facts = 
hoelzl@59353
   189
  let
hoelzl@59353
   190
    val dests = get_dest (Context.Proof ctxt)
hoelzl@59353
   191
    fun prep_dest thm =
hoelzl@59353
   192
      (if is_too_generic thm then [] else apply_dests thm dests) ;
hoelzl@59353
   193
    val preprocessors = (("std", prep_dest #> pair) :: get_preprocessors ctxt) ;
hoelzl@59353
   194
    fun preprocess_thm (thm, raw) =
hoelzl@59353
   195
      if raw then pair [thm] else fold_map (fn (_, proc) => proc thm) preprocessors #>> flat
hoelzl@59353
   196
    
hoelzl@59353
   197
    fun sel lv (th, (raw, lv')) = if lv = lv' then SOME (th, raw) else NONE ;
hoelzl@59353
   198
    fun get lv = ctxt |> Context.Proof |> get_thms |> rev |> map_filter (sel lv) ;
hoelzl@59353
   199
    val pre_thms = map (Simplifier.norm_hhf ctxt #> rpair false) facts @ get Concrete @ get Generic
hoelzl@59353
   200
hoelzl@59353
   201
    val (thms, ctxt) = fold_map preprocess_thm pre_thms ctxt |>> flat
hoelzl@59353
   202
  in (thms, ctxt) end
hoelzl@59353
   203
hoelzl@59047
   204
fun measurable_tac ctxt facts =
wenzelm@51717
   205
  let
hoelzl@59048
   206
    fun debug_fact msg thm () =
wenzelm@61877
   207
      msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
hoelzl@59048
   208
hoelzl@59048
   209
    fun IF' c t i = COND (c i) (t i) no_tac
hoelzl@59048
   210
hoelzl@59048
   211
    fun r_tac msg =
hoelzl@59048
   212
      if Config.get ctxt debug
hoelzl@59048
   213
      then FIRST' o
wenzelm@59498
   214
        map (fn thm => resolve_tac ctxt [thm]
hoelzl@59353
   215
          THEN' K (debug_tac ctxt (debug_fact (msg ^ " resolved using") thm) all_tac))
wenzelm@59498
   216
      else resolve_tac ctxt
hoelzl@59048
   217
hoelzl@59048
   218
    val elem_congI = @{lemma "A = B \<Longrightarrow> x \<in> B \<Longrightarrow> x \<in> A" by simp}
hoelzl@59048
   219
hoelzl@59353
   220
    val (thms, ctxt) = prepare_facts ctxt facts
hoelzl@50387
   221
wenzelm@69597
   222
    fun is_sets_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
wenzelm@69597
   223
          (Const (\<^const_name>\<open>sets\<close>, _) $ _) $
wenzelm@69597
   224
          (Const (\<^const_name>\<open>sets\<close>, _) $ _)) = true
wenzelm@69597
   225
      | is_sets_eq (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
wenzelm@69597
   226
          (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _) $
wenzelm@69597
   227
          (Const (\<^const_name>\<open>measurable\<close>, _) $ _ $ _)) = true
hoelzl@59048
   228
      | is_sets_eq _ = false
hoelzl@59048
   229
hoelzl@59048
   230
    val cong_thms = get_cong (Context.Proof ctxt) @
wenzelm@59582
   231
      filter (fn thm => Thm.concl_of thm |> HOLogic.dest_Trueprop |> is_sets_eq handle TERM _ => false) facts
hoelzl@59048
   232
hoelzl@59048
   233
    fun sets_cong_tac i =
hoelzl@59048
   234
      Subgoal.FOCUS (fn {context = ctxt', prems = prems, ...} => (
hoelzl@59048
   235
        let
hoelzl@59048
   236
          val ctxt'' = Simplifier.add_prems prems ctxt'
hoelzl@59048
   237
        in
hoelzl@59048
   238
          r_tac "cong intro" [elem_congI]
hoelzl@59048
   239
          THEN' SOLVED' (fn i => REPEAT_DETERM (
hoelzl@59048
   240
              ((r_tac "cong solve" (cong_thms @ [@{thm refl}])
wenzelm@59582
   241
                ORELSE' IF' (fn i => fn thm => Thm.nprems_of thm > i)
hoelzl@59048
   242
                  (SOLVED' (asm_full_simp_tac ctxt''))) i)))
hoelzl@59048
   243
        end) 1) ctxt i
hoelzl@59048
   244
        THEN flexflex_tac ctxt
hoelzl@59048
   245
hoelzl@59048
   246
    val simp_solver_tac = 
hoelzl@59048
   247
      IF' not_measurable_prop (debug_tac ctxt (K "simp ") o SOLVED' (asm_full_simp_tac ctxt))
hoelzl@59048
   248
hoelzl@59048
   249
    val split_countable_tac =
hoelzl@59048
   250
      Subgoal.FOCUS (fn {context = ctxt, ...} => SUBGOAL (fn (t, i) =>
hoelzl@59048
   251
        let
hoelzl@59048
   252
          val f = dest_measurable_fun (HOLogic.dest_Trueprop t)
hoelzl@59048
   253
          fun inst (ts, Ts) =
wenzelm@60807
   254
            Thm.instantiate'
wenzelm@60807
   255
              (map (Option.map (Thm.ctyp_of ctxt)) Ts)
wenzelm@60807
   256
              (map (Option.map (Thm.cterm_of ctxt)) ts)
wenzelm@59498
   257
              @{thm measurable_compose_countable}
haftmann@61424
   258
        in r_tac "case_prod countable" (cnt_prefixes ctxt f |> map inst) i end
hoelzl@59048
   259
        handle TERM _ => no_tac) 1)
hoelzl@50387
   260
hoelzl@50387
   261
    val splitter = if Config.get ctxt split then split_countable_tac ctxt else K no_tac
hoelzl@50387
   262
hoelzl@59048
   263
    val single_step_tac =
hoelzl@59048
   264
      simp_solver_tac
hoelzl@59048
   265
      ORELSE' r_tac "step" thms
hoelzl@59048
   266
      ORELSE' splitter
hoelzl@59048
   267
      ORELSE' (CHANGED o sets_cong_tac)
hoelzl@59048
   268
      ORELSE' (K (debug_tac ctxt (K "backtrack") no_tac))
hoelzl@50387
   269
hoelzl@59048
   270
  in debug_tac ctxt (K "start") (REPEAT (single_step_tac 1)) end;
hoelzl@50387
   271
wenzelm@51717
   272
fun simproc ctxt redex =
wenzelm@51717
   273
  let
wenzelm@59582
   274
    val t = HOLogic.mk_Trueprop (Thm.term_of redex);
hoelzl@50387
   275
    fun tac {context = ctxt, prems = _ } =
hoelzl@59047
   276
      SOLVE (measurable_tac ctxt (Simplifier.prems_of ctxt));
hoelzl@50387
   277
  in try (fn () => Goal.prove ctxt [] [] t tac RS @{thm Eq_TrueI}) () end;
hoelzl@50387
   278
hoelzl@50387
   279
end
hoelzl@50387
   280