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