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