src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
author haftmann
Thu Aug 26 20:51:17 2010 +0200 (2010-08-26 ago)
changeset 38786 e46e7a9cb622
parent 38752 6628adcae4a7
child 38795 848be46708dc
permissions -rw-r--r--
formerly unnamed infix impliciation now named HOL.implies
blanchet@35826
     1
(*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
blanchet@38027
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
blanchet@36393
     3
    Author:     Jasmin Blanchette, TU Muenchen
wenzelm@33309
     4
*)
paulson@15452
     5
blanchet@35826
     6
signature SLEDGEHAMMER_FACT_FILTER =
wenzelm@16802
     7
sig
blanchet@38752
     8
  datatype locality = General | Theory | Local | Chained
blanchet@38752
     9
blanchet@35966
    10
  type relevance_override =
blanchet@35966
    11
    {add: Facts.ref list,
blanchet@35966
    12
     del: Facts.ref list,
blanchet@35966
    13
     only: bool}
blanchet@35966
    14
blanchet@37616
    15
  val trace : bool Unsynchronized.ref
blanchet@38744
    16
  val name_thm_pairs_from_ref :
blanchet@38696
    17
    Proof.context -> unit Symtab.table -> thm list -> Facts.ref
blanchet@38752
    18
    -> ((string * locality) * thm) list
blanchet@37347
    19
  val relevant_facts :
blanchet@38745
    20
    bool -> real * real -> int -> bool -> relevance_override
blanchet@37995
    21
    -> Proof.context * (thm list * 'a) -> term list -> term
blanchet@38752
    22
    -> ((string * locality) * thm) list
paulson@15347
    23
end;
paulson@15347
    24
blanchet@35826
    25
structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
paulson@15347
    26
struct
paulson@15347
    27
blanchet@38652
    28
open Sledgehammer_Util
blanchet@38652
    29
blanchet@37616
    30
val trace = Unsynchronized.ref false
blanchet@37616
    31
fun trace_msg msg = if !trace then tracing (msg ()) else ()
blanchet@35826
    32
blanchet@37580
    33
val respect_no_atp = true
blanchet@37505
    34
blanchet@38752
    35
datatype locality = General | Theory | Local | Chained
blanchet@38752
    36
blanchet@35966
    37
type relevance_override =
blanchet@35966
    38
  {add: Facts.ref list,
blanchet@35966
    39
   del: Facts.ref list,
blanchet@35966
    40
   only: bool}
paulson@21070
    41
blanchet@37616
    42
val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
blanchet@37616
    43
blanchet@38744
    44
fun repair_name reserved multi j name =
blanchet@38744
    45
  (name |> Symtab.defined reserved name ? quote) ^
blanchet@38744
    46
  (if multi then "(" ^ Int.toString j ^ ")" else "")
blanchet@38744
    47
blanchet@38744
    48
fun name_thm_pairs_from_ref ctxt reserved chained_ths xref =
blanchet@38744
    49
  let
blanchet@38744
    50
    val ths = ProofContext.get_fact ctxt xref
blanchet@38744
    51
    val name = Facts.string_of_ref xref
blanchet@38744
    52
    val multi = length ths > 1
blanchet@38744
    53
  in
blanchet@38752
    54
    (ths, (1, []))
blanchet@38752
    55
    |-> fold (fn th => fn (j, rest) =>
blanchet@38752
    56
                 (j + 1, ((repair_name reserved multi j name,
blanchet@38752
    57
                          if member Thm.eq_thm chained_ths th then Chained
blanchet@38752
    58
                          else General), th) :: rest))
blanchet@38744
    59
    |> snd
blanchet@38699
    60
  end
blanchet@37616
    61
wenzelm@28477
    62
(***************************************************************)
wenzelm@28477
    63
(* Relevance Filtering                                         *)
wenzelm@28477
    64
(***************************************************************)
mengj@19194
    65
paulson@24287
    66
(*** constants with types ***)
paulson@24287
    67
paulson@24287
    68
(*An abstraction of Isabelle types*)
blanchet@38744
    69
datatype pseudotype = PVar | PType of string * pseudotype list
blanchet@38744
    70
blanchet@38744
    71
fun string_for_pseudotype PVar = "?"
blanchet@38744
    72
  | string_for_pseudotype (PType (s, Ts)) =
blanchet@38744
    73
    (case Ts of
blanchet@38744
    74
       [] => ""
blanchet@38744
    75
     | [T] => string_for_pseudotype T
blanchet@38744
    76
     | Ts => string_for_pseudotypes Ts ^ " ") ^ s
blanchet@38744
    77
and string_for_pseudotypes Ts =
blanchet@38744
    78
  "(" ^ commas (map string_for_pseudotype Ts) ^ ")"
paulson@24287
    79
paulson@24287
    80
(*Is the second type an instance of the first one?*)
blanchet@38744
    81
fun match_pseudotype (PType (a, T), PType (b, U)) =
blanchet@38744
    82
    a = b andalso match_pseudotypes (T, U)
blanchet@38744
    83
  | match_pseudotype (PVar, _) = true
blanchet@38744
    84
  | match_pseudotype (_, PVar) = false
blanchet@38744
    85
and match_pseudotypes ([], []) = true
blanchet@38744
    86
  | match_pseudotypes (T :: Ts, U :: Us) =
blanchet@38744
    87
    match_pseudotype (T, U) andalso match_pseudotypes (Ts, Us)
paulson@24287
    88
paulson@24287
    89
(*Is there a unifiable constant?*)
blanchet@38744
    90
fun pseudoconst_mem f const_tab (c, c_typ) =
blanchet@38744
    91
  exists (curry (match_pseudotypes o f) c_typ)
blanchet@38744
    92
         (these (Symtab.lookup const_tab c))
blanchet@37505
    93
blanchet@38744
    94
fun pseudotype_for (Type (c,typs)) = PType (c, map pseudotype_for typs)
blanchet@38744
    95
  | pseudotype_for (TFree _) = PVar
blanchet@38744
    96
  | pseudotype_for (TVar _) = PVar
blanchet@38744
    97
(* Pairs a constant with the list of its type instantiations. *)
blanchet@38744
    98
fun pseudoconst_for thy (c, T) =
blanchet@38744
    99
  (c, map pseudotype_for (Sign.const_typargs thy (c, T)))
blanchet@38744
   100
  handle TYPE _ => (c, [])  (* Variable (locale constant): monomorphic *)
paulson@24287
   101
blanchet@38744
   102
fun string_for_pseudoconst (s, []) = s
blanchet@38744
   103
  | string_for_pseudoconst (s, Ts) = s ^ string_for_pseudotypes Ts
blanchet@38744
   104
fun string_for_super_pseudoconst (s, [[]]) = s
blanchet@38744
   105
  | string_for_super_pseudoconst (s, Tss) =
blanchet@38744
   106
    s ^ "{" ^ commas (map string_for_pseudotypes Tss) ^ "}"
paulson@24287
   107
blanchet@38749
   108
val abs_prefix = "Sledgehammer.abs"
blanchet@38749
   109
val skolem_prefix = "Sledgehammer.sko"
blanchet@38747
   110
blanchet@38747
   111
(* Add a pseudoconstant to the table, but a [] entry means a standard
blanchet@38747
   112
   connective, which we ignore.*)
blanchet@38747
   113
fun add_pseudoconst_to_table also_skolem (c, ctyps) =
blanchet@38747
   114
  if also_skolem orelse not (String.isPrefix skolem_prefix c) then
blanchet@38747
   115
    Symtab.map_default (c, [ctyps])
blanchet@38747
   116
                       (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
blanchet@38747
   117
  else
blanchet@38747
   118
    I
paulson@24287
   119
blanchet@38692
   120
fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
blanchet@38692
   121
blanchet@37537
   122
val flip = Option.map not
blanchet@38091
   123
(* These are typically simplified away by "Meson.presimplify". *)
blanchet@38682
   124
val boring_consts =
blanchet@38682
   125
  [@{const_name False}, @{const_name True}, @{const_name If}, @{const_name Let}]
blanchet@37537
   126
blanchet@38747
   127
fun get_pseudoconsts thy also_skolems pos ts =
blanchet@37505
   128
  let
blanchet@38587
   129
    (* We include free variables, as well as constants, to handle locales. For
blanchet@38587
   130
       each quantifiers that must necessarily be skolemized by the ATP, we
blanchet@38587
   131
       introduce a fresh constant to simulate the effect of Skolemization. *)
blanchet@37537
   132
    fun do_term t =
blanchet@37537
   133
      case t of
blanchet@38747
   134
        Const x => add_pseudoconst_to_table also_skolems (pseudoconst_for thy x)
blanchet@38747
   135
      | Free (s, _) => add_pseudoconst_to_table also_skolems (s, [])
blanchet@38688
   136
      | t1 $ t2 => fold do_term [t1, t2]
blanchet@38749
   137
      | Abs (_, _, t') =>
blanchet@38749
   138
        do_term t' #> add_pseudoconst_to_table true (abs_prefix, [])
blanchet@37537
   139
      | _ => I
blanchet@38587
   140
    fun do_quantifier will_surely_be_skolemized body_t =
blanchet@37537
   141
      do_formula pos body_t
blanchet@38747
   142
      #> (if also_skolems andalso will_surely_be_skolemized then
blanchet@38747
   143
            add_pseudoconst_to_table true (gensym skolem_prefix, [])
blanchet@38587
   144
          else
blanchet@38587
   145
            I)
blanchet@38587
   146
    and do_term_or_formula T =
blanchet@38692
   147
      if is_formula_type T then do_formula NONE else do_term
blanchet@37537
   148
    and do_formula pos t =
blanchet@37537
   149
      case t of
blanchet@37537
   150
        Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
blanchet@38587
   151
        do_quantifier (pos = SOME false) body_t
blanchet@37537
   152
      | @{const "==>"} $ t1 $ t2 =>
blanchet@37537
   153
        do_formula (flip pos) t1 #> do_formula pos t2
blanchet@37537
   154
      | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
blanchet@38587
   155
        fold (do_term_or_formula T) [t1, t2]
blanchet@37537
   156
      | @{const Trueprop} $ t1 => do_formula pos t1
blanchet@37537
   157
      | @{const Not} $ t1 => do_formula (flip pos) t1
blanchet@37537
   158
      | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
blanchet@38587
   159
        do_quantifier (pos = SOME false) body_t
blanchet@37537
   160
      | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
blanchet@38587
   161
        do_quantifier (pos = SOME true) body_t
blanchet@37537
   162
      | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
blanchet@37537
   163
      | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
haftmann@38786
   164
      | @{const HOL.implies} $ t1 $ t2 =>
blanchet@37537
   165
        do_formula (flip pos) t1 #> do_formula pos t2
blanchet@37537
   166
      | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
blanchet@38587
   167
        fold (do_term_or_formula T) [t1, t2]
blanchet@38587
   168
      | Const (@{const_name If}, Type (_, [_, Type (_, [T, _])]))
blanchet@38587
   169
        $ t1 $ t2 $ t3 =>
blanchet@38587
   170
        do_formula NONE t1 #> fold (do_term_or_formula T) [t2, t3]
blanchet@38587
   171
      | Const (@{const_name Ex1}, _) $ Abs (_, _, body_t) =>
blanchet@38587
   172
        do_quantifier (is_some pos) body_t
blanchet@38587
   173
      | Const (@{const_name Ball}, _) $ t1 $ Abs (_, _, body_t) =>
blanchet@38587
   174
        do_quantifier (pos = SOME false)
blanchet@38587
   175
                      (HOLogic.mk_imp (incr_boundvars 1 t1 $ Bound 0, body_t))
blanchet@38587
   176
      | Const (@{const_name Bex}, _) $ t1 $ Abs (_, _, body_t) =>
blanchet@38587
   177
        do_quantifier (pos = SOME true)
blanchet@38587
   178
                      (HOLogic.mk_conj (incr_boundvars 1 t1 $ Bound 0, body_t))
blanchet@37537
   179
      | (t0 as Const (_, @{typ bool})) $ t1 =>
blanchet@37537
   180
        do_term t0 #> do_formula pos t1  (* theory constant *)
blanchet@37537
   181
      | _ => do_term t
blanchet@37505
   182
  in
blanchet@38091
   183
    Symtab.empty |> fold (Symtab.update o rpair []) boring_consts
blanchet@37995
   184
                 |> fold (do_formula pos) ts
blanchet@37505
   185
  end
paulson@24287
   186
paulson@24287
   187
(*Inserts a dummy "constant" referring to the theory name, so that relevance
paulson@24287
   188
  takes the given theory into account.*)
blanchet@37616
   189
fun theory_const_prop_of theory_relevant th =
blanchet@37505
   190
  if theory_relevant then
blanchet@37505
   191
    let
blanchet@37505
   192
      val name = Context.theory_name (theory_of_thm th)
blanchet@37505
   193
      val t = Const (name ^ ". 1", @{typ bool})
blanchet@37505
   194
    in t $ prop_of th end
blanchet@37505
   195
  else
blanchet@37505
   196
    prop_of th
blanchet@37505
   197
paulson@24287
   198
(**** Constant / Type Frequencies ****)
paulson@24287
   199
blanchet@38743
   200
(* A two-dimensional symbol table counts frequencies of constants. It's keyed
blanchet@38743
   201
   first by constant name and second by its list of type instantiations. For the
blanchet@38744
   202
   latter, we need a linear ordering on "pseudotype list". *)
paulson@24287
   203
blanchet@38744
   204
fun pseudotype_ord p =
blanchet@38743
   205
  case p of
blanchet@38744
   206
    (PVar, PVar) => EQUAL
blanchet@38744
   207
  | (PVar, PType _) => LESS
blanchet@38744
   208
  | (PType _, PVar) => GREATER
blanchet@38744
   209
  | (PType q1, PType q2) =>
blanchet@38744
   210
    prod_ord fast_string_ord (dict_ord pseudotype_ord) (q1, q2)
paulson@24287
   211
blanchet@38743
   212
structure CTtab =
blanchet@38744
   213
  Table(type key = pseudotype list val ord = dict_ord pseudotype_ord)
paulson@24287
   214
blanchet@37616
   215
fun count_axiom_consts theory_relevant thy (_, th) =
blanchet@37503
   216
  let
blanchet@37503
   217
    fun do_const (a, T) =
blanchet@38744
   218
      let val (c, cts) = pseudoconst_for thy (a, T) in
blanchet@37503
   219
        (* Two-dimensional table update. Constant maps to types maps to
blanchet@37503
   220
           count. *)
blanchet@37503
   221
        CTtab.map_default (cts, 0) (Integer.add 1)
blanchet@37503
   222
        |> Symtab.map_default (c, CTtab.empty)
blanchet@37503
   223
      end
blanchet@37503
   224
    fun do_term (Const x) = do_const x
blanchet@37503
   225
      | do_term (Free x) = do_const x
blanchet@37503
   226
      | do_term (t $ u) = do_term t #> do_term u
blanchet@37503
   227
      | do_term (Abs (_, _, t)) = do_term t
blanchet@37503
   228
      | do_term _ = I
blanchet@37616
   229
  in th |> theory_const_prop_of theory_relevant |> do_term end
paulson@24287
   230
paulson@24287
   231
paulson@24287
   232
(**** Actual Filtering Code ****)
paulson@24287
   233
paulson@24287
   234
(*The frequency of a constant is the sum of those of all instances of its type.*)
blanchet@38744
   235
fun pseudoconst_freq match const_tab (c, cts) =
blanchet@38744
   236
  CTtab.fold (fn (cts', m) => match (cts, cts') ? Integer.add m)
blanchet@38686
   237
             (the (Symtab.lookup const_tab c)) 0
blanchet@38686
   238
  handle Option.Option => 0
blanchet@38686
   239
paulson@24287
   240
blanchet@38085
   241
(* A surprising number of theorems contain only a few significant constants.
blanchet@38085
   242
   These include all induction rules, and other general theorems. *)
blanchet@37503
   243
blanchet@37503
   244
(* "log" seems best in practice. A constant function of one ignores the constant
blanchet@37503
   245
   frequencies. *)
blanchet@38747
   246
fun rel_log n = 1.0 + 2.0 / Math.ln (Real.fromInt n + 1.0)
blanchet@38747
   247
(* TODO: experiment
blanchet@38747
   248
fun irrel_log n = 0.5 + 1.0 / Math.ln (Real.fromInt n + 1.0)
blanchet@38747
   249
*)
blanchet@38747
   250
fun irrel_log n = Math.ln (Real.fromInt n + 19.0) / 6.4
blanchet@37503
   251
blanchet@38752
   252
(* FUDGE *)
blanchet@38752
   253
val skolem_weight = 1.0
blanchet@38752
   254
val abs_weight = 2.0
blanchet@38752
   255
blanchet@37503
   256
(* Computes a constant's weight, as determined by its frequency. *)
blanchet@38747
   257
val rel_weight = rel_log oo pseudoconst_freq match_pseudotypes
blanchet@38747
   258
fun irrel_weight const_tab (c as (s, _)) =
blanchet@38752
   259
  if String.isPrefix skolem_prefix s then skolem_weight
blanchet@38752
   260
  else if String.isPrefix abs_prefix s then abs_weight
blanchet@38747
   261
  else irrel_log (pseudoconst_freq (match_pseudotypes o swap) const_tab c)
blanchet@38747
   262
(* TODO: experiment
blanchet@38747
   263
fun irrel_weight _ _ = 1.0
blanchet@38747
   264
*)
paulson@24287
   265
blanchet@38752
   266
(* FUDGE *)
blanchet@38752
   267
fun locality_multiplier General = 1.0
blanchet@38752
   268
  | locality_multiplier Theory = 1.1
blanchet@38752
   269
  | locality_multiplier Local = 1.3
blanchet@38752
   270
  | locality_multiplier Chained = 2.0
blanchet@38751
   271
blanchet@38752
   272
fun axiom_weight loc const_tab relevant_consts axiom_consts =
blanchet@38744
   273
  case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
blanchet@38744
   274
                    ||> filter_out (pseudoconst_mem swap relevant_consts) of
blanchet@38744
   275
    ([], []) => 0.0
blanchet@38744
   276
  | (_, []) => 1.0
blanchet@38744
   277
  | (rel, irrel) =>
blanchet@38744
   278
    let
blanchet@38744
   279
      val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
blanchet@38752
   280
                       |> curry Real.* (locality_multiplier loc)
blanchet@38744
   281
      val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
blanchet@38744
   282
      val res = rel_weight / (rel_weight + irrel_weight)
blanchet@38744
   283
    in if Real.isFinite res then res else 0.0 end
blanchet@37505
   284
blanchet@38747
   285
(* TODO: experiment
blanchet@38747
   286
fun debug_axiom_weight const_tab relevant_consts axiom_consts =
blanchet@38747
   287
  case axiom_consts |> List.partition (pseudoconst_mem I relevant_consts)
blanchet@38747
   288
                    ||> filter_out (pseudoconst_mem swap relevant_consts) of
blanchet@38747
   289
    ([], []) => 0.0
blanchet@38747
   290
  | (_, []) => 1.0
blanchet@38747
   291
  | (rel, irrel) =>
blanchet@38747
   292
    let
blanchet@38747
   293
val _ = tracing (PolyML.makestring ("REL: ", rel))
blanchet@38747
   294
val _ = tracing (PolyML.makestring ("IRREL: ", irrel))
blanchet@38747
   295
      val rel_weight = fold (curry Real.+ o rel_weight const_tab) rel 0.0
blanchet@38747
   296
      val irrel_weight = fold (curry Real.+ o irrel_weight const_tab) irrel 0.0
blanchet@38747
   297
      val res = rel_weight / (rel_weight + irrel_weight)
blanchet@38747
   298
    in if Real.isFinite res then res else 0.0 end
blanchet@38747
   299
*)
blanchet@38747
   300
blanchet@38747
   301
fun pseudoconsts_of_term thy t =
blanchet@38742
   302
  Symtab.fold (fn (x, ys) => fold (fn y => cons (x, y)) ys)
blanchet@38747
   303
              (get_pseudoconsts thy true (SOME true) [t]) []
blanchet@38687
   304
fun pair_consts_axiom theory_relevant thy axiom =
blanchet@37616
   305
  (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
blanchet@38747
   306
                |> pseudoconsts_of_term thy)
paulson@24287
   307
blanchet@38699
   308
type annotated_thm =
blanchet@38752
   309
  (((unit -> string) * locality) * thm) * (string * pseudotype list) list
blanchet@37505
   310
blanchet@38747
   311
fun take_most_relevant max_max_imperfect max_relevant remaining_max
blanchet@38747
   312
                       (candidates : (annotated_thm * real) list) =
blanchet@38744
   313
  let
blanchet@38747
   314
    val max_imperfect =
blanchet@38747
   315
      Real.ceil (Math.pow (max_max_imperfect,
blanchet@38747
   316
                           Real.fromInt remaining_max
blanchet@38747
   317
                           / Real.fromInt max_relevant))
blanchet@38747
   318
    val (perfect, imperfect) =
blanchet@38747
   319
      candidates |> List.partition (fn (_, w) => w > 0.99999)
blanchet@38745
   320
                 ||> sort (Real.compare o swap o pairself snd)
blanchet@38747
   321
    val ((accepts, more_rejects), rejects) =
blanchet@38747
   322
      chop max_imperfect imperfect |>> append perfect |>> chop remaining_max
blanchet@38744
   323
  in
blanchet@38744
   324
    trace_msg (fn () => "Number of candidates: " ^
blanchet@38745
   325
                        string_of_int (length candidates));
blanchet@38744
   326
    trace_msg (fn () => "Effective threshold: " ^
blanchet@38745
   327
                        Real.toString (#2 (hd accepts)));
blanchet@38747
   328
    trace_msg (fn () => "Actually passed (" ^ Int.toString (length accepts) ^
blanchet@38747
   329
        "): " ^ (accepts
blanchet@38752
   330
                 |> map (fn ((((name, _), _), _), weight) =>
blanchet@38752
   331
                            name () ^ " [" ^ Real.toString weight ^ "]")
blanchet@38745
   332
                 |> commas));
blanchet@38747
   333
    (accepts, more_rejects @ rejects)
blanchet@38744
   334
  end
paulson@24287
   335
blanchet@38752
   336
(* FUDGE *)
blanchet@38683
   337
val threshold_divisor = 2.0
blanchet@38683
   338
val ridiculous_threshold = 0.1
blanchet@38747
   339
val max_max_imperfect_fudge_factor = 0.66
blanchet@38683
   340
blanchet@38745
   341
fun relevance_filter ctxt threshold0 decay max_relevant theory_relevant
blanchet@38745
   342
                     ({add, del, ...} : relevance_override) axioms goal_ts =
blanchet@38739
   343
  let
blanchet@38739
   344
    val thy = ProofContext.theory_of ctxt
blanchet@38739
   345
    val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
blanchet@38739
   346
                         Symtab.empty
blanchet@38739
   347
    val add_thms = maps (ProofContext.get_fact ctxt) add
blanchet@38739
   348
    val del_thms = maps (ProofContext.get_fact ctxt) del
blanchet@38747
   349
    val max_max_imperfect =
blanchet@38747
   350
      Math.sqrt (Real.fromInt max_relevant * max_max_imperfect_fudge_factor)
blanchet@38747
   351
    fun iter j remaining_max threshold rel_const_tab hopeless hopeful =
blanchet@38739
   352
      let
blanchet@38744
   353
        fun game_over rejects =
blanchet@38747
   354
          (* Add "add:" facts. *)
blanchet@38747
   355
          if null add_thms then
blanchet@38747
   356
            []
blanchet@38744
   357
          else
blanchet@38747
   358
            map_filter (fn ((p as (_, th), _), _) =>
blanchet@38747
   359
                           if member Thm.eq_thm add_thms th then SOME p
blanchet@38747
   360
                           else NONE) rejects
blanchet@38747
   361
        fun relevant [] rejects hopeless [] =
blanchet@38747
   362
            (* Nothing has been added this iteration. *)
blanchet@38747
   363
            if j = 0 andalso threshold >= ridiculous_threshold then
blanchet@38747
   364
              (* First iteration? Try again. *)
blanchet@38747
   365
              iter 0 max_relevant (threshold / threshold_divisor) rel_const_tab
blanchet@38747
   366
                   hopeless hopeful
blanchet@38744
   367
            else
blanchet@38747
   368
              game_over (rejects @ hopeless)
blanchet@38747
   369
          | relevant candidates rejects hopeless [] =
blanchet@38739
   370
            let
blanchet@38747
   371
              val (accepts, more_rejects) =
blanchet@38747
   372
                take_most_relevant max_max_imperfect max_relevant remaining_max
blanchet@38747
   373
                                   candidates
blanchet@38739
   374
              val rel_const_tab' =
blanchet@38745
   375
                rel_const_tab
blanchet@38747
   376
                |> fold (add_pseudoconst_to_table false)
blanchet@38747
   377
                        (maps (snd o fst) accepts)
blanchet@38744
   378
              fun is_dirty (c, _) =
blanchet@38744
   379
                Symtab.lookup rel_const_tab' c <> Symtab.lookup rel_const_tab c
blanchet@38745
   380
              val (hopeful_rejects, hopeless_rejects) =
blanchet@38745
   381
                 (rejects @ hopeless, ([], []))
blanchet@38745
   382
                 |-> fold (fn (ax as (_, consts), old_weight) =>
blanchet@38745
   383
                              if exists is_dirty consts then
blanchet@38745
   384
                                apfst (cons (ax, NONE))
blanchet@38745
   385
                              else
blanchet@38745
   386
                                apsnd (cons (ax, old_weight)))
blanchet@38745
   387
                 |>> append (more_rejects
blanchet@38745
   388
                             |> map (fn (ax as (_, consts), old_weight) =>
blanchet@38745
   389
                                        (ax, if exists is_dirty consts then NONE
blanchet@38745
   390
                                             else SOME old_weight)))
blanchet@38747
   391
              val threshold =
blanchet@38747
   392
                threshold + (1.0 - threshold)
blanchet@38747
   393
                * Math.pow (decay, Real.fromInt (length accepts))
blanchet@38747
   394
              val remaining_max = remaining_max - length accepts
blanchet@38739
   395
            in
blanchet@38744
   396
              trace_msg (fn () => "New or updated constants: " ^
blanchet@38744
   397
                  commas (rel_const_tab' |> Symtab.dest
blanchet@38744
   398
                          |> subtract (op =) (Symtab.dest rel_const_tab)
blanchet@38744
   399
                          |> map string_for_super_pseudoconst));
blanchet@38745
   400
              map (fst o fst) accepts @
blanchet@38747
   401
              (if remaining_max = 0 then
blanchet@38745
   402
                 game_over (hopeful_rejects @ map (apsnd SOME) hopeless_rejects)
blanchet@38745
   403
               else
blanchet@38747
   404
                 iter (j + 1) remaining_max threshold rel_const_tab'
blanchet@38747
   405
                      hopeless_rejects hopeful_rejects)
blanchet@38739
   406
            end
blanchet@38747
   407
          | relevant candidates rejects hopeless
blanchet@38752
   408
                     (((ax as (((_, loc), th), axiom_consts)), cached_weight)
blanchet@38747
   409
                      :: hopeful) =
blanchet@38739
   410
            let
blanchet@38739
   411
              val weight =
blanchet@38739
   412
                case cached_weight of
blanchet@38739
   413
                  SOME w => w
blanchet@38752
   414
                | NONE => axiom_weight loc const_tab rel_const_tab axiom_consts
blanchet@38747
   415
(* TODO: experiment
blanchet@38752
   416
val name = fst (fst (fst ax)) ()
blanchet@38752
   417
val _ = if String.isPrefix "lift.simps(3" name then
blanchet@38752
   418
tracing ("*** " ^ name ^ PolyML.makestring (debug_axiom_weight const_tab rel_const_tab axiom_consts))
blanchet@38747
   419
else
blanchet@38747
   420
()
blanchet@38747
   421
*)
blanchet@38739
   422
            in
blanchet@38741
   423
              if weight >= threshold then
blanchet@38747
   424
                relevant ((ax, weight) :: candidates) rejects hopeless hopeful
blanchet@38739
   425
              else
blanchet@38747
   426
                relevant candidates ((ax, weight) :: rejects) hopeless hopeful
blanchet@38739
   427
            end
blanchet@38739
   428
        in
blanchet@38744
   429
          trace_msg (fn () =>
blanchet@38744
   430
              "ITERATION " ^ string_of_int j ^ ": current threshold: " ^
blanchet@38744
   431
              Real.toString threshold ^ ", constants: " ^
blanchet@38744
   432
              commas (rel_const_tab |> Symtab.dest
blanchet@38744
   433
                      |> filter (curry (op <>) [] o snd)
blanchet@38744
   434
                      |> map string_for_super_pseudoconst));
blanchet@38747
   435
          relevant [] [] hopeless hopeful
blanchet@38739
   436
        end
blanchet@38739
   437
  in
blanchet@38739
   438
    axioms |> filter_out (member Thm.eq_thm del_thms o snd)
blanchet@38739
   439
           |> map (rpair NONE o pair_consts_axiom theory_relevant thy)
blanchet@38745
   440
           |> iter 0 max_relevant threshold0
blanchet@38747
   441
                   (get_pseudoconsts thy false (SOME false) goal_ts) []
blanchet@38739
   442
           |> tap (fn res => trace_msg (fn () =>
blanchet@38686
   443
                                "Total relevant: " ^ Int.toString (length res)))
blanchet@38739
   444
  end
paulson@24287
   445
blanchet@38744
   446
paulson@24287
   447
(***************************************************************)
mengj@19768
   448
(* Retrieving and filtering lemmas                             *)
mengj@19768
   449
(***************************************************************)
mengj@19768
   450
paulson@33022
   451
(*** retrieve lemmas and filter them ***)
mengj@19768
   452
paulson@20757
   453
(*Reject theorems with names like "List.filter.filter_list_def" or
paulson@21690
   454
  "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
paulson@20757
   455
fun is_package_def a =
wenzelm@30364
   456
  let val names = Long_Name.explode a
paulson@21690
   457
  in
paulson@21690
   458
     length names > 2 andalso
paulson@21690
   459
     not (hd names = "local") andalso
paulson@21690
   460
     String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
paulson@21690
   461
  end;
paulson@20757
   462
blanchet@38085
   463
fun make_fact_table xs =
blanchet@37616
   464
  fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
blanchet@38085
   465
fun make_unique xs = Termtab.fold (cons o snd) (make_fact_table xs) []
mengj@19768
   466
blanchet@37626
   467
(* FIXME: put other record thms here, or declare as "no_atp" *)
blanchet@37626
   468
val multi_base_blacklist =
blanchet@37626
   469
  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
blanchet@38682
   470
   "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy",
blanchet@38682
   471
   "case_cong", "weak_case_cong"]
blanchet@38682
   472
  |> map (prefix ".")
blanchet@37626
   473
blanchet@37626
   474
val max_lambda_nesting = 3
blanchet@37626
   475
blanchet@37626
   476
fun term_has_too_many_lambdas max (t1 $ t2) =
blanchet@37626
   477
    exists (term_has_too_many_lambdas max) [t1, t2]
blanchet@37626
   478
  | term_has_too_many_lambdas max (Abs (_, _, t)) =
blanchet@37626
   479
    max = 0 orelse term_has_too_many_lambdas (max - 1) t
blanchet@37626
   480
  | term_has_too_many_lambdas _ _ = false
blanchet@37626
   481
blanchet@37626
   482
(* Don't count nested lambdas at the level of formulas, since they are
blanchet@37626
   483
   quantifiers. *)
blanchet@37626
   484
fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
blanchet@37626
   485
    formula_has_too_many_lambdas (T :: Ts) t
blanchet@37626
   486
  | formula_has_too_many_lambdas Ts t =
blanchet@37626
   487
    if is_formula_type (fastype_of1 (Ts, t)) then
blanchet@37626
   488
      exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
blanchet@37626
   489
    else
blanchet@37626
   490
      term_has_too_many_lambdas max_lambda_nesting t
blanchet@37626
   491
blanchet@38692
   492
(* The max apply depth of any "metis" call in "Metis_Examples" (on 2007-10-31)
blanchet@37626
   493
   was 11. *)
blanchet@37626
   494
val max_apply_depth = 15
blanchet@37626
   495
blanchet@37626
   496
fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
blanchet@37626
   497
  | apply_depth (Abs (_, _, t)) = apply_depth t
blanchet@37626
   498
  | apply_depth _ = 0
blanchet@37626
   499
blanchet@37626
   500
fun is_formula_too_complex t =
blanchet@38085
   501
  apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t
blanchet@37626
   502
blanchet@37543
   503
val exists_sledgehammer_const =
blanchet@37626
   504
  exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
blanchet@37626
   505
blanchet@38652
   506
fun is_strange_theorem th =
blanchet@37626
   507
  case head_of (concl_of th) of
blanchet@37626
   508
      Const (a, _) => (a <> @{const_name Trueprop} andalso
blanchet@37626
   509
                       a <> @{const_name "=="})
blanchet@37626
   510
    | _ => false
blanchet@37626
   511
blanchet@37626
   512
val type_has_top_sort =
blanchet@37626
   513
  exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
blanchet@37626
   514
blanchet@38085
   515
(**** Predicates to detect unwanted facts (prolific or likely to cause
blanchet@37347
   516
      unsoundness) ****)
paulson@21470
   517
blanchet@38289
   518
(* Too general means, positive equality literal with a variable X as one
blanchet@38289
   519
   operand, when X does not occur properly in the other operand. This rules out
blanchet@38289
   520
   clearly inconsistent facts such as X = a | X = b, though it by no means
blanchet@38289
   521
   guarantees soundness. *)
paulson@21470
   522
blanchet@38289
   523
(* Unwanted equalities are those between a (bound or schematic) variable that
blanchet@38289
   524
   does not properly occur in the second operand. *)
blanchet@38607
   525
val is_exhaustive_finite =
blanchet@38607
   526
  let
blanchet@38629
   527
    fun is_bad_equal (Var z) t =
blanchet@38629
   528
        not (exists_subterm (fn Var z' => z = z' | _ => false) t)
blanchet@38629
   529
      | is_bad_equal (Bound j) t = not (loose_bvar1 (t, j))
blanchet@38629
   530
      | is_bad_equal _ _ = false
blanchet@38629
   531
    fun do_equals t1 t2 = is_bad_equal t1 t2 orelse is_bad_equal t2 t1
blanchet@38607
   532
    fun do_formula pos t =
blanchet@38607
   533
      case (pos, t) of
blanchet@38615
   534
        (_, @{const Trueprop} $ t1) => do_formula pos t1
blanchet@38607
   535
      | (true, Const (@{const_name all}, _) $ Abs (_, _, t')) =>
blanchet@38607
   536
        do_formula pos t'
blanchet@38607
   537
      | (true, Const (@{const_name All}, _) $ Abs (_, _, t')) =>
blanchet@38607
   538
        do_formula pos t'
blanchet@38607
   539
      | (false, Const (@{const_name Ex}, _) $ Abs (_, _, t')) =>
blanchet@38607
   540
        do_formula pos t'
blanchet@38607
   541
      | (_, @{const "==>"} $ t1 $ t2) =>
blanchet@38629
   542
        do_formula (not pos) t1 andalso
blanchet@38629
   543
        (t2 = @{prop False} orelse do_formula pos t2)
haftmann@38786
   544
      | (_, @{const HOL.implies} $ t1 $ t2) =>
blanchet@38629
   545
        do_formula (not pos) t1 andalso
blanchet@38629
   546
        (t2 = @{const False} orelse do_formula pos t2)
blanchet@38607
   547
      | (_, @{const Not} $ t1) => do_formula (not pos) t1
blanchet@38607
   548
      | (true, @{const "op |"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
blanchet@38607
   549
      | (false, @{const "op &"} $ t1 $ t2) => forall (do_formula pos) [t1, t2]
blanchet@38607
   550
      | (true, Const (@{const_name "op ="}, _) $ t1 $ t2) => do_equals t1 t2
blanchet@38607
   551
      | (true, Const (@{const_name "=="}, _) $ t1 $ t2) => do_equals t1 t2
blanchet@38607
   552
      | _ => false
blanchet@38607
   553
  in do_formula true end
blanchet@38607
   554
blanchet@38592
   555
fun has_bound_or_var_of_type tycons =
blanchet@38592
   556
  exists_subterm (fn Var (_, Type (s, _)) => member (op =) tycons s
blanchet@38592
   557
                   | Abs (_, Type (s, _), _) => member (op =) tycons s
blanchet@38592
   558
                   | _ => false)
paulson@21431
   559
blanchet@38085
   560
(* Facts are forbidden to contain variables of these types. The typical reason
blanchet@37347
   561
   is that they lead to unsoundness. Note that "unit" satisfies numerous
blanchet@38085
   562
   equations like "?x = ()". The resulting clauses will have no type constraint,
blanchet@37347
   563
   yielding false proofs. Even "bool" leads to many unsound proofs, though only
blanchet@37347
   564
   for higher-order problems. *)
blanchet@38592
   565
val dangerous_types = [@{type_name unit}, @{type_name bool}, @{type_name prop}];
paulson@22217
   566
blanchet@38085
   567
(* Facts containing variables of type "unit" or "bool" or of the form
blanchet@38290
   568
   "ALL x. x = A | x = B | x = C" are likely to lead to unsound proofs if types
blanchet@38290
   569
   are omitted. *)
blanchet@38593
   570
fun is_dangerous_term full_types t =
blanchet@38609
   571
  not full_types andalso
blanchet@38679
   572
  let val t = transform_elim_term t in
blanchet@38679
   573
    has_bound_or_var_of_type dangerous_types t orelse
blanchet@38679
   574
    is_exhaustive_finite t
blanchet@38679
   575
  end
paulson@21470
   576
blanchet@38627
   577
fun is_theorem_bad_for_atps full_types thm =
blanchet@38627
   578
  let val t = prop_of thm in
blanchet@38627
   579
    is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
blanchet@38627
   580
    is_dangerous_term full_types t orelse exists_sledgehammer_const t orelse
blanchet@38652
   581
    is_strange_theorem thm
blanchet@38627
   582
  end
blanchet@38627
   583
blanchet@38696
   584
fun all_name_thms_pairs ctxt reserved full_types add_thms chained_ths =
blanchet@38627
   585
  let
blanchet@38752
   586
    val thy = ProofContext.theory_of ctxt
blanchet@38752
   587
    val thy_prefix = Context.theory_name thy ^ Long_Name.separator
blanchet@38752
   588
    val global_facts = PureThy.facts_of thy
blanchet@38644
   589
    val local_facts = ProofContext.facts_of ctxt
blanchet@38644
   590
    val named_locals = local_facts |> Facts.dest_static []
blanchet@38752
   591
    val is_chained = member Thm.eq_thm chained_ths
blanchet@38697
   592
    (* Unnamed, not chained formulas with schematic variables are omitted,
blanchet@38697
   593
       because they are rejected by the backticks (`...`) parser for some
blanchet@38697
   594
       reason. *)
blanchet@38738
   595
    fun is_good_unnamed_local th =
blanchet@38738
   596
      forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals
blanchet@38738
   597
      andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th))
blanchet@38644
   598
    val unnamed_locals =
blanchet@38738
   599
      local_facts |> Facts.props |> filter is_good_unnamed_local
blanchet@38697
   600
                  |> map (pair "" o single)
blanchet@38627
   601
    val full_space =
blanchet@38738
   602
      Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
blanchet@38752
   603
    fun add_facts global foldx facts =
blanchet@38699
   604
      foldx (fn (name0, ths) =>
blanchet@38699
   605
        if name0 <> "" andalso
blanchet@38699
   606
           forall (not o member Thm.eq_thm add_thms) ths andalso
blanchet@38699
   607
           (Facts.is_concealed facts name0 orelse
blanchet@38699
   608
            (respect_no_atp andalso is_package_def name0) orelse
blanchet@38699
   609
            exists (fn s => String.isSuffix s name0) multi_base_blacklist orelse
blanchet@38699
   610
            String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then
blanchet@38627
   611
          I
blanchet@38627
   612
        else
blanchet@38627
   613
          let
blanchet@38752
   614
            val base_loc =
blanchet@38752
   615
              if not global then Local
blanchet@38752
   616
              else if String.isPrefix thy_prefix name0 then Theory
blanchet@38752
   617
              else General
blanchet@38699
   618
            val multi = length ths > 1
blanchet@38696
   619
            fun backquotify th =
blanchet@38696
   620
              "`" ^ Print_Mode.setmp [Print_Mode.input]
blanchet@38696
   621
                                 (Syntax.string_of_term ctxt) (prop_of th) ^ "`"
blanchet@38738
   622
              |> String.translate (fn c => if Char.isPrint c then str c else "")
blanchet@38738
   623
              |> simplify_spaces
blanchet@38699
   624
            fun check_thms a =
blanchet@38699
   625
              case try (ProofContext.get_thms ctxt) a of
blanchet@38699
   626
                NONE => false
blanchet@38699
   627
              | SOME ths' => Thm.eq_thms (ths, ths')
blanchet@38627
   628
          in
blanchet@38699
   629
            pair 1
blanchet@38699
   630
            #> fold (fn th => fn (j, rest) =>
blanchet@38699
   631
                 (j + 1,
blanchet@38699
   632
                  if is_theorem_bad_for_atps full_types th andalso
blanchet@38699
   633
                     not (member Thm.eq_thm add_thms th) then
blanchet@38699
   634
                    rest
blanchet@38699
   635
                  else
blanchet@38752
   636
                    (((fn () =>
blanchet@38752
   637
                          if name0 = "" then
blanchet@38752
   638
                            th |> backquotify
blanchet@38752
   639
                          else
blanchet@38752
   640
                            let
blanchet@38752
   641
                              val name1 = Facts.extern facts name0
blanchet@38752
   642
                              val name2 = Name_Space.extern full_space name0
blanchet@38752
   643
                            in
blanchet@38752
   644
                              case find_first check_thms [name1, name2, name0] of
blanchet@38752
   645
                                SOME name => repair_name reserved multi j name
blanchet@38752
   646
                              | NONE => ""
blanchet@38752
   647
                            end), if is_chained th then Chained else base_loc),
blanchet@38752
   648
                      (multi, th)) :: rest)) ths
blanchet@38699
   649
            #> snd
blanchet@38627
   650
          end)
blanchet@38644
   651
  in
blanchet@38752
   652
    [] |> add_facts false fold local_facts (unnamed_locals @ named_locals)
blanchet@38752
   653
       |> add_facts true Facts.fold_static global_facts global_facts
blanchet@38644
   654
  end
blanchet@38627
   655
blanchet@38627
   656
(* The single-name theorems go after the multiple-name ones, so that single
blanchet@38627
   657
   names are preferred when both are available. *)
blanchet@38699
   658
fun name_thm_pairs ctxt respect_no_atp =
blanchet@38744
   659
  List.partition (fst o snd) #> op @ #> map (apsnd snd)
blanchet@38699
   660
  #> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd)
blanchet@38627
   661
blanchet@38627
   662
(***************************************************************)
blanchet@38627
   663
(* ATP invocation methods setup                                *)
blanchet@38627
   664
(***************************************************************)
blanchet@38627
   665
blanchet@38745
   666
fun relevant_facts full_types (threshold0, threshold1) max_relevant
blanchet@38744
   667
                   theory_relevant (relevance_override as {add, del, only})
blanchet@37995
   668
                   (ctxt, (chained_ths, _)) hyp_ts concl_t =
blanchet@37538
   669
  let
blanchet@38745
   670
    val decay = 1.0 - Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
blanchet@38745
   671
                                1.0 / Real.fromInt (max_relevant + 1))
blanchet@37538
   672
    val add_thms = maps (ProofContext.get_fact ctxt) add
blanchet@38696
   673
    val reserved = reserved_isar_keyword_table ()
blanchet@37538
   674
    val axioms =
blanchet@38699
   675
      (if only then
blanchet@38752
   676
         maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
blanchet@38752
   677
               o name_thm_pairs_from_ref ctxt reserved chained_ths) add
blanchet@38699
   678
       else
blanchet@38699
   679
         all_name_thms_pairs ctxt reserved full_types add_thms chained_ths)
blanchet@38688
   680
      |> name_thm_pairs ctxt (respect_no_atp andalso not only)
blanchet@38595
   681
      |> make_unique
blanchet@37538
   682
  in
blanchet@38688
   683
    trace_msg (fn () => "Considering " ^ Int.toString (length axioms) ^
blanchet@38688
   684
                        " theorems");
blanchet@38745
   685
    (if threshold0 > 1.0 orelse threshold0 > threshold1 then
blanchet@38739
   686
       []
blanchet@38745
   687
     else if threshold0 < 0.0 then
blanchet@38739
   688
       axioms
blanchet@38739
   689
     else
blanchet@38745
   690
       relevance_filter ctxt threshold0 decay max_relevant theory_relevant
blanchet@38745
   691
                        relevance_override axioms (concl_t :: hyp_ts))
blanchet@38752
   692
    |> map (apfst (apfst (fn f => f ()))) |> sort_wrt (fst o fst)
blanchet@37538
   693
  end
immler@30536
   694
paulson@15347
   695
end;