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