src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
author blanchet
Tue Jun 29 10:25:53 2010 +0200 (2010-06-29)
changeset 37626 1146291fe718
parent 37616 c8d2d84d6011
child 37995 06f02b15ef8a
permissions -rw-r--r--
move blacklisting completely out of the clausifier;
the only reason it was in the clausifier as well was the Skolem cache
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 *)
     5 
     6 signature SLEDGEHAMMER_FACT_FILTER =
     7 sig
     8   type relevance_override =
     9     {add: Facts.ref list,
    10      del: Facts.ref list,
    11      only: bool}
    12 
    13   val trace : bool Unsynchronized.ref
    14   val chained_prefix : string
    15   val name_thms_pair_from_ref :
    16     Proof.context -> thm list -> Facts.ref -> string * thm list
    17   val relevant_facts :
    18     bool -> real -> real -> bool -> int -> bool -> relevance_override
    19     -> Proof.context * (thm list * 'a) -> thm list -> (string * thm) list
    20 end;
    21 
    22 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
    23 struct
    24 
    25 val trace = Unsynchronized.ref false
    26 fun trace_msg msg = if !trace then tracing (msg ()) else ()
    27 
    28 val respect_no_atp = true
    29 
    30 type relevance_override =
    31   {add: Facts.ref list,
    32    del: Facts.ref list,
    33    only: bool}
    34 
    35 val sledgehammer_prefix = "Sledgehammer" ^ Long_Name.separator
    36 (* Used to label theorems chained into the goal. *)
    37 val chained_prefix = sledgehammer_prefix ^ "chained_"
    38 
    39 fun name_thms_pair_from_ref ctxt chained_ths xref =
    40   let
    41     val ths = ProofContext.get_fact ctxt xref
    42     val name = Facts.string_of_ref xref
    43                |> forall (member Thm.eq_thm chained_ths) ths
    44                   ? prefix chained_prefix
    45   in (name, ths) end
    46 
    47 
    48 (***************************************************************)
    49 (* Relevance Filtering                                         *)
    50 (***************************************************************)
    51 
    52 fun strip_Trueprop (@{const Trueprop} $ t) = t
    53   | strip_Trueprop t = t;
    54 
    55 (*** constants with types ***)
    56 
    57 (*An abstraction of Isabelle types*)
    58 datatype const_typ =  CTVar | CType of string * const_typ list
    59 
    60 (*Is the second type an instance of the first one?*)
    61 fun match_type (CType(con1,args1)) (CType(con2,args2)) =
    62       con1=con2 andalso match_types args1 args2
    63   | match_type CTVar _ = true
    64   | match_type _ CTVar = false
    65 and match_types [] [] = true
    66   | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
    67 
    68 (*Is there a unifiable constant?*)
    69 fun uni_mem goal_const_tab (c, c_typ) =
    70   exists (match_types c_typ) (these (Symtab.lookup goal_const_tab c))
    71 
    72 (*Maps a "real" type to a const_typ*)
    73 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs)
    74   | const_typ_of (TFree _) = CTVar
    75   | const_typ_of (TVar _) = CTVar
    76 
    77 (*Pairs a constant with the list of its type instantiations (using const_typ)*)
    78 fun const_with_typ thy (c,typ) =
    79     let val tvars = Sign.const_typargs thy (c,typ)
    80     in (c, map const_typ_of tvars) end
    81     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)
    82 
    83 (*Add a const/type pair to the table, but a [] entry means a standard connective,
    84   which we ignore.*)
    85 fun add_const_type_to_table (c, ctyps) =
    86   Symtab.map_default (c, [ctyps])
    87                      (fn [] => [] | ctypss => insert (op =) ctyps ctypss)
    88 
    89 val fresh_prefix = "Sledgehammer.Fresh."
    90 
    91 val flip = Option.map not
    92 
    93 val boring_natural_consts = [@{const_name If}]
    94 (* Including equality in this list might be expected to stop rules like
    95    subset_antisym from being chosen, but for some reason filtering works better
    96    with them listed. The logical signs All, Ex, &, and --> are omitted for CNF
    97    because any remaining occurrences must be within comprehensions. *)
    98 val boring_cnf_consts =
    99   [@{const_name Trueprop}, @{const_name "==>"}, @{const_name all},
   100    @{const_name "=="}, @{const_name "op |"}, @{const_name Not},
   101    @{const_name "op ="}]
   102 
   103 fun get_consts_typs thy pos ts =
   104   let
   105     (* Free variables are included, as well as constants, to handle locales.
   106        "skolem_id" is included to increase the complexity of theorems containing
   107        Skolem functions. In non-CNF form, "Ex" is included but each occurrence
   108        is considered fresh, to simulate the effect of Skolemization. *)
   109     fun do_term t =
   110       case t of
   111         Const x => add_const_type_to_table (const_with_typ thy x)
   112       | Free x => add_const_type_to_table (const_with_typ thy x)
   113       | (t as Const (@{const_name skolem_id}, _)) $ _ => do_term t
   114       | t1 $ t2 => do_term t1 #> do_term t2
   115       | Abs (_, _, t) =>
   116         (* Abstractions lead to combinators, so we add a penalty for them. *)
   117         add_const_type_to_table (gensym fresh_prefix, [])
   118         #> do_term t
   119       | _ => I
   120     fun do_quantifier sweet_pos pos body_t =
   121       do_formula pos body_t
   122       #> (if pos = SOME sweet_pos then I
   123           else add_const_type_to_table (gensym fresh_prefix, []))
   124     and do_equality T t1 t2 =
   125       fold (if T = @{typ bool} orelse T = @{typ prop} then do_formula NONE
   126             else do_term) [t1, t2]
   127     and do_formula pos t =
   128       case t of
   129         Const (@{const_name all}, _) $ Abs (_, _, body_t) =>
   130         do_quantifier false pos body_t
   131       | @{const "==>"} $ t1 $ t2 =>
   132         do_formula (flip pos) t1 #> do_formula pos t2
   133       | Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2 =>
   134         do_equality T t1 t2
   135       | @{const Trueprop} $ t1 => do_formula pos t1
   136       | @{const Not} $ t1 => do_formula (flip pos) t1
   137       | Const (@{const_name All}, _) $ Abs (_, _, body_t) =>
   138         do_quantifier false pos body_t
   139       | Const (@{const_name Ex}, _) $ Abs (_, _, body_t) =>
   140         do_quantifier true pos body_t
   141       | @{const "op &"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   142       | @{const "op |"} $ t1 $ t2 => fold (do_formula pos) [t1, t2]
   143       | @{const "op -->"} $ t1 $ t2 =>
   144         do_formula (flip pos) t1 #> do_formula pos t2
   145       | Const (@{const_name "op ="}, Type (_, [T, _])) $ t1 $ t2 =>
   146         do_equality T t1 t2
   147       | (t0 as Const (_, @{typ bool})) $ t1 =>
   148         do_term t0 #> do_formula pos t1  (* theory constant *)
   149       | _ => do_term t
   150   in
   151     Symtab.empty
   152     |> fold (Symtab.update o rpair []) boring_natural_consts
   153     |> fold (do_formula pos) ts
   154   end
   155 
   156 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   157   takes the given theory into account.*)
   158 fun theory_const_prop_of theory_relevant th =
   159   if theory_relevant then
   160     let
   161       val name = Context.theory_name (theory_of_thm th)
   162       val t = Const (name ^ ". 1", @{typ bool})
   163     in t $ prop_of th end
   164   else
   165     prop_of th
   166 
   167 (**** Constant / Type Frequencies ****)
   168 
   169 (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
   170   constant name and second by its list of type instantiations. For the latter, we need
   171   a linear ordering on type const_typ list.*)
   172 
   173 local
   174 
   175 fun cons_nr CTVar = 0
   176   | cons_nr (CType _) = 1;
   177 
   178 in
   179 
   180 fun const_typ_ord TU =
   181   case TU of
   182     (CType (a, Ts), CType (b, Us)) =>
   183       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   184   | (T, U) => int_ord (cons_nr T, cons_nr U);
   185 
   186 end;
   187 
   188 structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
   189 
   190 fun count_axiom_consts theory_relevant thy (_, th) =
   191   let
   192     fun do_const (a, T) =
   193       let val (c, cts) = const_with_typ thy (a,T) in
   194         (* Two-dimensional table update. Constant maps to types maps to
   195            count. *)
   196         CTtab.map_default (cts, 0) (Integer.add 1)
   197         |> Symtab.map_default (c, CTtab.empty)
   198       end
   199     fun do_term (Const x) = do_const x
   200       | do_term (Free x) = do_const x
   201       | do_term (Const (x as (@{const_name skolem_id}, _)) $ _) = do_const x
   202       | do_term (t $ u) = do_term t #> do_term u
   203       | do_term (Abs (_, _, t)) = do_term t
   204       | do_term _ = I
   205   in th |> theory_const_prop_of theory_relevant |> do_term end
   206 
   207 
   208 (**** Actual Filtering Code ****)
   209 
   210 (*The frequency of a constant is the sum of those of all instances of its type.*)
   211 fun const_frequency const_tab (c, cts) =
   212   CTtab.fold (fn (cts', m) => match_types cts cts' ? Integer.add m)
   213              (the (Symtab.lookup const_tab c)
   214               handle Option.Option => raise Fail ("Const: " ^ c)) 0
   215 
   216 (*A surprising number of theorems contain only a few significant constants.
   217   These include all induction rules, and other general theorems. Filtering
   218   theorems in clause form reveals these complexities in the form of Skolem
   219   functions. If we were instead to filter theorems in their natural form,
   220   some other method of measuring theorem complexity would become necessary.*)
   221 
   222 (* "log" seems best in practice. A constant function of one ignores the constant
   223    frequencies. *)
   224 fun log_weight2 (x:real) = 1.0 + 2.0 / Math.ln (x + 1.0)
   225 
   226 (* Computes a constant's weight, as determined by its frequency. *)
   227 val ct_weight = log_weight2 o real oo const_frequency
   228 
   229 (*Relevant constants are weighted according to frequency,
   230   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   231   which are rare, would harm a clause's chances of being picked.*)
   232 fun clause_weight const_tab gctyps consts_typs =
   233     let val rel = filter (uni_mem gctyps) consts_typs
   234         val rel_weight = fold (curry Real.+ o ct_weight const_tab) rel 0.0
   235     in
   236         rel_weight / (rel_weight + real (length consts_typs - length rel))
   237     end;
   238 
   239 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   240 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
   241 
   242 fun consts_typs_of_term thy t =
   243   Symtab.fold add_expand_pairs (get_consts_typs thy (SOME false) [t]) []
   244 
   245 fun pair_consts_typs_axiom theory_relevant thy axiom =
   246   (axiom, axiom |> snd |> theory_const_prop_of theory_relevant
   247                 |> consts_typs_of_term thy)
   248 
   249 exception CONST_OR_FREE of unit
   250 
   251 fun dest_Const_or_Free (Const x) = x
   252   | dest_Const_or_Free (Free x) = x
   253   | dest_Const_or_Free _ = raise CONST_OR_FREE ()
   254 
   255 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   256 fun defines thy thm gctypes =
   257     let val tm = prop_of thm
   258         fun defs lhs rhs =
   259             let val (rator,args) = strip_comb lhs
   260                 val ct = const_with_typ thy (dest_Const_or_Free rator)
   261             in
   262               forall is_Var args andalso uni_mem gctypes ct andalso
   263                 subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
   264             end
   265             handle CONST_OR_FREE () => false
   266     in
   267         case tm of
   268           @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) =>
   269             defs lhs rhs
   270         | _ => false
   271     end;
   272 
   273 type annotated_cnf_thm = (string * thm) * (string * const_typ list) list
   274 
   275 (*For a reverse sort, putting the largest values first.*)
   276 fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
   277 
   278 (*Limit the number of new clauses, to prevent runaway acceptance.*)
   279 fun take_best max_new (newpairs : (annotated_cnf_thm * real) list) =
   280   let val nnew = length newpairs
   281   in
   282     if nnew <= max_new then (map #1 newpairs, [])
   283     else
   284       let val cls = sort compare_pairs newpairs
   285           val accepted = List.take (cls, max_new)
   286       in
   287         trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^
   288                        ", exceeds the limit of " ^ Int.toString (max_new)));
   289         trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   290         trace_msg (fn () => "Actually passed: " ^
   291           space_implode ", " (map (fst o fst o fst) accepted));
   292 
   293         (map #1 accepted, map #1 (List.drop (cls, max_new)))
   294       end
   295   end;
   296 
   297 fun relevant_clauses ctxt relevance_convergence defs_relevant max_new
   298                      ({add, del, ...} : relevance_override) const_tab =
   299   let
   300     val thy = ProofContext.theory_of ctxt
   301     val add_thms = maps (ProofContext.get_fact ctxt) add
   302     val del_thms = maps (ProofContext.get_fact ctxt) del
   303     fun iter threshold rel_const_tab =
   304       let
   305         fun relevant ([], _) [] = []  (* Nothing added this iteration *)
   306           | relevant (newpairs, rejects) [] =
   307             let
   308               val (newrels, more_rejects) = take_best max_new newpairs
   309               val new_consts = maps #2 newrels
   310               val rel_const_tab =
   311                 rel_const_tab |> fold add_const_type_to_table new_consts
   312               val threshold =
   313                 threshold + (1.0 - threshold) / relevance_convergence
   314             in
   315               trace_msg (fn () => "relevant this iteration: " ^
   316                                   Int.toString (length newrels));
   317               map #1 newrels @ iter threshold rel_const_tab
   318                   (more_rejects @ rejects)
   319             end
   320           | relevant (newrels, rejects)
   321                      ((ax as (clsthm as (name, th), consts_typs)) :: axs) =
   322             let
   323               val weight =
   324                 if member Thm.eq_thm add_thms th then 1.0
   325                 else if member Thm.eq_thm del_thms th then 0.0
   326                 else clause_weight const_tab rel_const_tab consts_typs
   327             in
   328               if weight >= threshold orelse
   329                  (defs_relevant andalso defines thy th rel_const_tab) then
   330                 (trace_msg (fn () =>
   331                      name ^ " passes: " ^ Real.toString weight
   332                      (* ^ " consts: " ^ commas (map fst consts_typs) *));
   333                  relevant ((ax, weight) :: newrels, rejects) axs)
   334               else
   335                 relevant (newrels, ax :: rejects) axs
   336             end
   337         in
   338           trace_msg (fn () => "relevant_clauses, current threshold: " ^
   339                               Real.toString threshold);
   340           relevant ([], [])
   341         end
   342   in iter end
   343 
   344 fun relevance_filter ctxt relevance_threshold relevance_convergence
   345                      defs_relevant max_new theory_relevant relevance_override
   346                      thy axioms goals =
   347   if relevance_threshold > 1.0 then
   348     []
   349   else if relevance_threshold < 0.0 then
   350     axioms
   351   else
   352     let
   353       val const_tab = fold (count_axiom_consts theory_relevant thy) axioms
   354                            Symtab.empty
   355       val goal_const_tab = get_consts_typs thy (SOME true) goals
   356       val relevance_threshold = 0.9 * relevance_threshold (* FIXME *)
   357       val _ =
   358         trace_msg (fn () => "Initial constants: " ^
   359                             commas (goal_const_tab
   360                                     |> Symtab.dest
   361                                     |> filter (curry (op <>) [] o snd)
   362                                     |> map fst))
   363       val relevant =
   364         relevant_clauses ctxt relevance_convergence defs_relevant max_new
   365                          relevance_override const_tab relevance_threshold
   366                          goal_const_tab
   367                          (map (pair_consts_typs_axiom theory_relevant thy)
   368                               axioms)
   369     in
   370       trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
   371       relevant
   372     end
   373 
   374 (***************************************************************)
   375 (* Retrieving and filtering lemmas                             *)
   376 (***************************************************************)
   377 
   378 (*** retrieve lemmas and filter them ***)
   379 
   380 (*Reject theorems with names like "List.filter.filter_list_def" or
   381   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   382 fun is_package_def a =
   383   let val names = Long_Name.explode a
   384   in
   385      length names > 2 andalso
   386      not (hd names = "local") andalso
   387      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   388   end;
   389 
   390 fun make_clause_table xs =
   391   fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty
   392 
   393 fun make_unique xs =
   394   Termtab.fold (cons o snd) (make_clause_table xs) []
   395 
   396 (* FIXME: put other record thms here, or declare as "no_atp" *)
   397 val multi_base_blacklist =
   398   ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
   399    "split_asm", "cases", "ext_cases"]
   400 
   401 val max_lambda_nesting = 3
   402 
   403 fun term_has_too_many_lambdas max (t1 $ t2) =
   404     exists (term_has_too_many_lambdas max) [t1, t2]
   405   | term_has_too_many_lambdas max (Abs (_, _, t)) =
   406     max = 0 orelse term_has_too_many_lambdas (max - 1) t
   407   | term_has_too_many_lambdas _ _ = false
   408 
   409 fun is_formula_type T = (T = HOLogic.boolT orelse T = propT)
   410 
   411 (* Don't count nested lambdas at the level of formulas, since they are
   412    quantifiers. *)
   413 fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) =
   414     formula_has_too_many_lambdas (T :: Ts) t
   415   | formula_has_too_many_lambdas Ts t =
   416     if is_formula_type (fastype_of1 (Ts, t)) then
   417       exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t))
   418     else
   419       term_has_too_many_lambdas max_lambda_nesting t
   420 
   421 (* The max apply depth of any "metis" call in "Metis_Examples" (on 31-10-2007)
   422    was 11. *)
   423 val max_apply_depth = 15
   424 
   425 fun apply_depth (f $ t) = Int.max (apply_depth f, apply_depth t + 1)
   426   | apply_depth (Abs (_, _, t)) = apply_depth t
   427   | apply_depth _ = 0
   428 
   429 fun is_formula_too_complex t =
   430   apply_depth t > max_apply_depth orelse Meson.too_many_clauses NONE t orelse
   431   formula_has_too_many_lambdas [] t
   432 
   433 val exists_sledgehammer_const =
   434   exists_Const (fn (s, _) => String.isPrefix sledgehammer_prefix s)
   435 
   436 fun is_strange_thm th =
   437   case head_of (concl_of th) of
   438       Const (a, _) => (a <> @{const_name Trueprop} andalso
   439                        a <> @{const_name "=="})
   440     | _ => false
   441 
   442 val type_has_top_sort =
   443   exists_subtype (fn TFree (_, []) => true | TVar (_, []) => true | _ => false)
   444 
   445 fun is_theorem_bad_for_atps thm =
   446   let val t = prop_of thm in
   447     is_formula_too_complex t orelse exists_type type_has_top_sort t orelse
   448     exists_sledgehammer_const t orelse is_strange_thm thm
   449   end
   450 
   451 fun all_name_thms_pairs ctxt chained_ths =
   452   let
   453     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   454     val local_facts = ProofContext.facts_of ctxt;
   455     val full_space =
   456       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
   457 
   458     fun valid_facts facts =
   459       (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
   460         if Facts.is_concealed facts name orelse
   461            (respect_no_atp andalso is_package_def name) orelse
   462            member (op =) multi_base_blacklist (Long_Name.base_name name) then
   463           I
   464         else
   465           let
   466             fun check_thms a =
   467               (case try (ProofContext.get_thms ctxt) a of
   468                 NONE => false
   469               | SOME ths1 => Thm.eq_thms (ths0, ths1));
   470 
   471             val name1 = Facts.extern facts name;
   472             val name2 = Name_Space.extern full_space name;
   473             val ths = filter_out is_theorem_bad_for_atps ths0
   474           in
   475             case find_first check_thms [name1, name2, name] of
   476               NONE => I
   477             | SOME name' =>
   478               cons (name' |> forall (member Thm.eq_thm chained_ths) ths
   479                              ? prefix chained_prefix, ths)
   480           end)
   481   in valid_facts global_facts @ valid_facts local_facts end;
   482 
   483 fun multi_name a th (n, pairs) =
   484   (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
   485 
   486 fun add_names (_, []) pairs = pairs
   487   | add_names (a, [th]) pairs = (a, th) :: pairs
   488   | add_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs))
   489 
   490 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   491 
   492 (* The single-name theorems go after the multiple-name ones, so that single
   493    names are preferred when both are available. *)
   494 fun name_thm_pairs ctxt respect_no_atp name_thms_pairs =
   495   let
   496     val (mults, singles) = List.partition is_multi name_thms_pairs
   497     val ps = [] |> fold add_names singles |> fold add_names mults
   498   in ps |> respect_no_atp ? filter_out (No_ATPs.member ctxt o snd) end;
   499 
   500 fun is_named ("", th) =
   501     (warning ("No name for theorem " ^
   502               Display.string_of_thm_without_context th); false)
   503   | is_named _ = true
   504 fun checked_name_thm_pairs respect_no_atp ctxt =
   505   name_thm_pairs ctxt respect_no_atp
   506   #> tap (fn ps => trace_msg
   507                         (fn () => ("Considering " ^ Int.toString (length ps) ^
   508                                    " theorems")))
   509   #> filter is_named
   510 
   511 (***************************************************************)
   512 (* ATP invocation methods setup                                *)
   513 (***************************************************************)
   514 
   515 (**** Predicates to detect unwanted clauses (prolific or likely to cause
   516       unsoundness) ****)
   517 
   518 (** Too general means, positive equality literal with a variable X as one operand,
   519   when X does not occur properly in the other operand. This rules out clearly
   520   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   521 
   522 fun var_occurs_in_term ix =
   523   let
   524     fun aux (Var (jx, _)) = (ix = jx)
   525       | aux (t1 $ t2) = aux t1 orelse aux t2
   526       | aux (Abs (_, _, t)) = aux t
   527       | aux _ = false
   528   in aux end
   529 
   530 fun is_record_type T = not (null (Record.dest_recTs T))
   531 
   532 (*Unwanted equalities include
   533   (1) those between a variable that does not properly occur in the second operand,
   534   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   535 *)
   536 fun too_general_eqterms (Var (ix,T), t) =
   537     not (var_occurs_in_term ix t) orelse is_record_type T
   538   | too_general_eqterms _ = false;
   539 
   540 fun too_general_equality (Const (@{const_name "op ="}, _) $ x $ y) =
   541       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   542   | too_general_equality _ = false;
   543 
   544 fun has_typed_var tycons = exists_subterm
   545   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
   546 
   547 (* Clauses are forbidden to contain variables of these types. The typical reason
   548    is that they lead to unsoundness. Note that "unit" satisfies numerous
   549    equations like "?x = ()". The resulting clause will have no type constraint,
   550    yielding false proofs. Even "bool" leads to many unsound proofs, though only
   551    for higher-order problems. *)
   552 val dangerous_types = [@{type_name unit}, @{type_name bool}];
   553 
   554 (* Clauses containing variables of type "unit" or "bool" or of the form
   555    "?x = A | ?x = B | ?x = C" are likely to lead to unsound proofs if types are
   556    omitted. *)
   557 fun is_dangerous_term _ @{prop True} = true
   558   | is_dangerous_term full_types t =
   559     not full_types andalso
   560     (has_typed_var dangerous_types t orelse
   561      forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t)))
   562 
   563 fun relevant_facts full_types relevance_threshold relevance_convergence
   564                    defs_relevant max_new theory_relevant
   565                    (relevance_override as {add, del, only})
   566                    (ctxt, (chained_ths, _)) goal_cls =
   567   let
   568     val thy = ProofContext.theory_of ctxt
   569     val add_thms = maps (ProofContext.get_fact ctxt) add
   570     val has_override = not (null add) orelse not (null del)
   571     val is_FO = forall (Meson.is_fol_term thy o prop_of) goal_cls
   572     val axioms =
   573       checked_name_thm_pairs (respect_no_atp andalso not only) ctxt
   574           (map (name_thms_pair_from_ref ctxt chained_ths) add @
   575            (if only then [] else all_name_thms_pairs ctxt chained_ths))
   576       |> not has_override ? make_unique
   577       |> filter (fn (_, th) =>
   578                     member Thm.eq_thm add_thms th orelse
   579                     ((* ### FIXME: keep? (not is_FO orelse is_quasi_fol_theorem thy th) andalso*)
   580                      not (is_dangerous_term full_types (prop_of th))))
   581   in
   582     relevance_filter ctxt relevance_threshold relevance_convergence
   583                      defs_relevant max_new theory_relevant relevance_override
   584                      thy axioms (map prop_of goal_cls)
   585     |> has_override ? make_unique
   586     |> sort_wrt fst
   587   end
   588 
   589 end;