src/HOL/Tools/res_atp.ML
author Philipp Meyer
Wed Sep 30 11:33:59 2009 +0200 (2009-09-30)
changeset 32866 1238cbb7c08f
parent 32552 4d4ee06e9420
child 32952 aeb1e44fbc19
permissions -rw-r--r--
atp_minimal using chain_ths again
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA *)
     2 
     3 signature RES_ATP =
     4 sig
     5   datatype mode = Auto | Fol | Hol
     6   val tvar_classes_of_terms : term list -> string list
     7   val tfree_classes_of_terms : term list -> string list
     8   val type_consts_of_terms : theory -> term list -> string list
     9   val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
    10     (thm * (string * int)) list
    11   val prepare_clauses : bool -> thm list -> thm list ->
    12     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list ->
    13     (thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
    14     ResHolClause.axiom_name vector *
    15       (ResHolClause.clause list * ResHolClause.clause list * ResHolClause.clause list *
    16       ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
    17 end;
    18 
    19 structure ResAtp: RES_ATP =
    20 struct
    21 
    22 
    23 (********************************************************************)
    24 (* some settings for both background automatic ATP calling procedure*)
    25 (* and also explicit ATP invocation methods                         *)
    26 (********************************************************************)
    27 
    28 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
    29 datatype mode = Auto | Fol | Hol;
    30 
    31 val linkup_logic_mode = Auto;
    32 
    33 (*** background linkup ***)
    34 val run_blacklist_filter = true;
    35 
    36 (*** relevance filter parameters ***)
    37 val run_relevance_filter = true;
    38 val pass_mark = 0.5;
    39 val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
    40 val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
    41 val include_all = true;
    42 val include_atpset = true;
    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 = ["Trueprop","==>","all","==","op |","Not","op ="];
    69 
    70 
    71 (*** constants with types ***)
    72 
    73 (*An abstraction of Isabelle types*)
    74 datatype const_typ =  CTVar | CType of string * const_typ list
    75 
    76 (*Is the second type an instance of the first one?*)
    77 fun match_type (CType(con1,args1)) (CType(con2,args2)) = 
    78       con1=con2 andalso match_types args1 args2
    79   | match_type CTVar _ = true
    80   | match_type _ CTVar = false
    81 and match_types [] [] = true
    82   | match_types (a1::as1) (a2::as2) = match_type a1 a2 andalso match_types as1 as2;
    83 
    84 (*Is there a unifiable constant?*)
    85 fun uni_mem gctab (c,c_typ) =
    86   case Symtab.lookup gctab c of
    87       NONE => false
    88     | SOME ctyps_list => exists (match_types c_typ) ctyps_list;
    89   
    90 (*Maps a "real" type to a const_typ*)
    91 fun const_typ_of (Type (c,typs)) = CType (c, map const_typ_of typs) 
    92   | const_typ_of (TFree _) = CTVar
    93   | const_typ_of (TVar _) = CTVar
    94 
    95 (*Pairs a constant with the list of its type instantiations (using const_typ)*)
    96 fun const_with_typ thy (c,typ) = 
    97     let val tvars = Sign.const_typargs thy (c,typ)
    98     in (c, map const_typ_of tvars) end
    99     handle TYPE _ => (c,[]);   (*Variable (locale constant): monomorphic*)   
   100 
   101 (*Add a const/type pair to the table, but a [] entry means a standard connective,
   102   which we ignore.*)
   103 fun add_const_typ_table ((c,ctyps), tab) =
   104   Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
   105     tab;
   106 
   107 (*Free variables are included, as well as constants, to handle locales*)
   108 fun add_term_consts_typs_rm thy (Const(c, typ), tab) =
   109       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   110   | add_term_consts_typs_rm thy (Free(c, typ), tab) =
   111       add_const_typ_table (const_with_typ thy (c,typ), tab) 
   112   | add_term_consts_typs_rm thy (t $ u, tab) =
   113       add_term_consts_typs_rm thy (t, add_term_consts_typs_rm thy (u, tab))
   114   | add_term_consts_typs_rm thy (Abs(_,_,t), tab) = add_term_consts_typs_rm thy (t, tab)
   115   | add_term_consts_typs_rm thy (_, tab) = tab;
   116 
   117 (*The empty list here indicates that the constant is being ignored*)
   118 fun add_standard_const (s,tab) = Symtab.update (s,[]) tab;
   119 
   120 val null_const_tab : const_typ list list Symtab.table = 
   121     List.foldl add_standard_const Symtab.empty standard_consts;
   122 
   123 fun get_goal_consts_typs thy = List.foldl (add_term_consts_typs_rm thy) null_const_tab;
   124 
   125 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   126   takes the given theory into account.*)
   127 fun const_prop_of theory_const th =
   128  if theory_const then
   129   let val name = Context.theory_name (theory_of_thm th)
   130       val t = Const (name ^ ". 1", HOLogic.boolT)
   131   in  t $ prop_of th  end
   132  else prop_of th;
   133 
   134 (**** Constant / Type Frequencies ****)
   135 
   136 (*A two-dimensional symbol table counts frequencies of constants. It's keyed first by
   137   constant name and second by its list of type instantiations. For the latter, we need
   138   a linear ordering on type const_typ list.*)
   139   
   140 local
   141 
   142 fun cons_nr CTVar = 0
   143   | cons_nr (CType _) = 1;
   144 
   145 in
   146 
   147 fun const_typ_ord TU =
   148   case TU of
   149     (CType (a, Ts), CType (b, Us)) =>
   150       (case fast_string_ord(a,b) of EQUAL => dict_ord const_typ_ord (Ts,Us) | ord => ord)
   151   | (T, U) => int_ord (cons_nr T, cons_nr U);
   152 
   153 end;
   154 
   155 structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
   156 
   157 fun count_axiom_consts theory_const thy ((thm,_), tab) = 
   158   let fun count_const (a, T, tab) =
   159 	let val (c, cts) = const_with_typ thy (a,T)
   160 	in  (*Two-dimensional table update. Constant maps to types maps to count.*)
   161 	    Symtab.map_default (c, CTtab.empty) 
   162 	                       (CTtab.map_default (cts,0) (fn n => n+1)) tab
   163 	end
   164       fun count_term_consts (Const(a,T), tab) = count_const(a,T,tab)
   165 	| count_term_consts (Free(a,T), tab) = count_const(a,T,tab)
   166 	| count_term_consts (t $ u, tab) =
   167 	    count_term_consts (t, count_term_consts (u, tab))
   168 	| count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
   169 	| count_term_consts (_, tab) = tab
   170   in  count_term_consts (const_prop_of theory_const thm, tab)  end;
   171 
   172 
   173 (**** Actual Filtering Code ****)
   174 
   175 (*The frequency of a constant is the sum of those of all instances of its type.*)
   176 fun const_frequency ctab (c, cts) =
   177   let val pairs = CTtab.dest (the (Symtab.lookup ctab c))
   178       fun add ((cts',m), n) = if match_types cts cts' then m+n else n
   179   in  List.foldl add 0 pairs  end;
   180 
   181 (*Add in a constant's weight, as determined by its frequency.*)
   182 fun add_ct_weight ctab ((c,T), w) =
   183   w + weight_fn (real (const_frequency ctab (c,T)));
   184 
   185 (*Relevant constants are weighted according to frequency, 
   186   but irrelevant constants are simply counted. Otherwise, Skolem functions,
   187   which are rare, would harm a clause's chances of being picked.*)
   188 fun clause_weight ctab gctyps consts_typs =
   189     let val rel = filter (uni_mem gctyps) consts_typs
   190         val rel_weight = List.foldl (add_ct_weight ctab) 0.0 rel
   191     in
   192 	rel_weight / (rel_weight + real (length consts_typs - length rel))
   193     end;
   194     
   195 (*Multiplies out to a list of pairs: 'a * 'b list -> ('a * 'b) list -> ('a * 'b) list*)
   196 fun add_expand_pairs (x,ys) xys = List.foldl (fn (y,acc) => (x,y)::acc) xys ys;
   197 
   198 fun consts_typs_of_term thy t = 
   199   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   200   in  Symtab.fold add_expand_pairs tab []  end;
   201 
   202 fun pair_consts_typs_axiom theory_const thy (thm,name) =
   203     ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
   204 
   205 exception ConstFree;
   206 fun dest_ConstFree (Const aT) = aT
   207   | dest_ConstFree (Free aT) = aT
   208   | dest_ConstFree _ = raise ConstFree;
   209 
   210 (*Look for definitions of the form f ?x1 ... ?xn = t, but not reversed.*)
   211 fun defines thy (thm,(name,n)) gctypes =
   212     let val tm = prop_of thm
   213 	fun defs lhs rhs =
   214             let val (rator,args) = strip_comb lhs
   215 		val ct = const_with_typ thy (dest_ConstFree rator)
   216             in  forall is_Var args andalso uni_mem gctypes ct andalso
   217                 Term.add_vars rhs [] subset Term.add_vars lhs []
   218             end
   219 	    handle ConstFree => false
   220     in    
   221 	case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   222 		   defs lhs rhs 
   223 		 | _ => false
   224     end;
   225 
   226 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
   227        
   228 (*For a reverse sort, putting the largest values first.*)
   229 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   230 
   231 (*Limit the number of new clauses, to prevent runaway acceptance.*)
   232 fun take_best max_new (newpairs : (annotd_cls*real) list) =
   233   let val nnew = length newpairs
   234   in
   235     if nnew <= max_new then (map #1 newpairs, [])
   236     else 
   237       let val cls = sort compare_pairs newpairs
   238           val accepted = List.take (cls, max_new)
   239       in
   240         Output.debug (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   241 		       ", exceeds the limit of " ^ Int.toString (max_new)));
   242         Output.debug (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   243         Output.debug (fn () => "Actually passed: " ^
   244           space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   245 
   246 	(map #1 accepted, map #1 (List.drop (cls, max_new)))
   247       end
   248   end;
   249 
   250 fun relevant_clauses max_new thy ctab p rel_consts =
   251   let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   252 	| relevant (newpairs,rejects) [] =
   253 	    let val (newrels,more_rejects) = take_best max_new newpairs
   254 		val new_consts = List.concat (map #2 newrels)
   255 		val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
   256 		val newp = p + (1.0-p) / convergence
   257 	    in
   258               Output.debug (fn () => ("relevant this iteration: " ^ Int.toString (length newrels)));
   259 	       (map #1 newrels) @ 
   260 	       (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
   261 	    end
   262 	| relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   263 	    let val weight = clause_weight ctab rel_consts consts_typs
   264 	    in
   265 	      if p <= weight orelse (follow_defs andalso defines thy clsthm rel_consts)
   266 	      then (Output.debug (fn () => (name ^ " clause " ^ Int.toString n ^ 
   267 	                                    " passes: " ^ Real.toString weight));
   268 	            relevant ((ax,weight)::newrels, rejects) axs)
   269 	      else relevant (newrels, ax::rejects) axs
   270 	    end
   271     in  Output.debug (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
   272         relevant ([],[]) 
   273     end;
   274 	
   275 fun relevance_filter max_new theory_const thy axioms goals = 
   276  if run_relevance_filter andalso pass_mark >= 0.1
   277  then
   278   let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
   279       val goal_const_tab = get_goal_consts_typs thy goals
   280       val _ = Output.debug (fn () => ("Initial constants: " ^
   281                                  space_implode ", " (Symtab.keys goal_const_tab)));
   282       val rels = relevant_clauses max_new thy const_tab (pass_mark) 
   283                    goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
   284   in
   285       Output.debug (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   286       rels
   287   end
   288  else axioms;
   289 
   290 (***************************************************************)
   291 (* Retrieving and filtering lemmas                             *)
   292 (***************************************************************)
   293 
   294 (*** white list and black list of lemmas ***)
   295 
   296 (*The rule subsetI is frequently omitted by the relevance filter. This could be theory data
   297   or identified with ATPset (which however is too big currently)*)
   298 val whitelist_fo = [subsetI];
   299 (* ext has been a 'helper clause', always given to the atps.
   300   As such it was not passed to metis, but metis does not include ext (in contrast
   301   to the other helper_clauses *)
   302 val whitelist_ho = [ResHolClause.ext];
   303 
   304 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   305 
   306 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   307 
   308 fun setinsert (x,s) = Symtab.update (x,()) s;
   309 
   310 (*Reject theorems with names like "List.filter.filter_list_def" or
   311   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   312 fun is_package_def a =
   313   let val names = Long_Name.explode a
   314   in
   315      length names > 2 andalso
   316      not (hd names = "local") andalso
   317      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   318   end;
   319 
   320 (** a hash function from Term.term to int, and also a hash table **)
   321 val xor_words = List.foldl Word.xorb 0w0;
   322 
   323 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   324   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   325   | hashw_term ((Var(_,_)), w) = w
   326   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   327   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   328   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   329 
   330 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   331   | hash_literal P = hashw_term(P,0w0);
   332 
   333 fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
   334 
   335 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   336 
   337 exception HASH_CLAUSE;
   338 
   339 (*Create a hash table for clauses, of the given size*)
   340 fun mk_clause_table n =
   341       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   342                        (n, HASH_CLAUSE);
   343 
   344 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   345   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   346 fun make_unique xs =
   347   let val ht = mk_clause_table 7000
   348   in
   349       Output.debug (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   350       app (ignore o Polyhash.peekInsert ht) xs;
   351       Polyhash.listItems ht
   352   end;
   353 
   354 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   355   boost an ATP's performance (for some reason)*)
   356 fun subtract_cls c_clauses ax_clauses =
   357   let val ht = mk_clause_table 2200
   358       fun known x = isSome (Polyhash.peek ht x)
   359   in
   360       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   361       filter (not o known) c_clauses
   362   end;
   363 
   364 fun valid_facts facts =
   365   Facts.fold_static (fn (name, ths) =>
   366     if run_blacklist_filter andalso is_package_def name then I
   367     else
   368       let val xname = Facts.extern facts name in
   369         if NameSpace.is_hidden xname then I
   370         else cons (xname, filter_out ResAxioms.bad_for_atp ths)
   371       end) facts [];
   372 
   373 fun all_valid_thms ctxt =
   374   let
   375     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   376     val local_facts = ProofContext.facts_of ctxt;
   377   in valid_facts global_facts @ valid_facts local_facts end;
   378 
   379 fun multi_name a (th, (n,pairs)) =
   380   (n+1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs)
   381 
   382 fun add_single_names ((a, []), pairs) = pairs
   383   | add_single_names ((a, [th]), pairs) = (a,th)::pairs
   384   | add_single_names ((a, ths), pairs) = #2 (List.foldl (multi_name a) (1,pairs) ths);
   385 
   386 (*Ignore blacklisted basenames*)
   387 fun add_multi_names ((a, ths), pairs) =
   388   if (Long_Name.base_name a) mem_string ResAxioms.multi_base_blacklist  then pairs
   389   else add_single_names ((a, ths), pairs);
   390 
   391 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   392 
   393 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   394 fun name_thm_pairs ctxt =
   395   let val (mults,singles) = List.partition is_multi (all_valid_thms ctxt)
   396       val ht = mk_clause_table 900   (*ht for blacklisted theorems*)
   397       fun blacklisted x = run_blacklist_filter andalso isSome (Polyhash.peek ht x)
   398   in
   399       app (fn th => ignore (Polyhash.peekInsert ht (th,()))) (ResBlacklist.get ctxt);
   400       filter (not o blacklisted o #2)
   401         (List.foldl add_single_names (List.foldl add_multi_names [] mults) singles)
   402   end;
   403 
   404 fun check_named ("", th) =
   405       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   406   | check_named (_, th) = true;
   407 
   408 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   409 fun get_clasimp_atp_lemmas ctxt =
   410   let val included_thms =
   411     if include_all
   412     then (tap (fn ths => Output.debug
   413                  (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   414               (name_thm_pairs ctxt))
   415     else
   416     let val atpset_thms =
   417             if include_atpset then ResAxioms.atpset_rules_of ctxt
   418             else []
   419     in  atpset_thms  end
   420   in
   421     filter check_named included_thms
   422   end;
   423 
   424 (***************************************************************)
   425 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   426 (***************************************************************)
   427 
   428 fun add_classes (sorts, cset) = List.foldl setinsert cset (List.concat sorts);
   429 
   430 (*Remove this trivial type class*)
   431 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   432 
   433 fun tvar_classes_of_terms ts =
   434   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   435   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   436 
   437 fun tfree_classes_of_terms ts =
   438   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   439   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   440 
   441 (*fold type constructors*)
   442 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   443   | fold_type_consts f T x = x;
   444 
   445 val add_type_consts_in_type = fold_type_consts setinsert;
   446 
   447 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   448 fun add_type_consts_in_term thy =
   449   let val const_typargs = Sign.const_typargs thy
   450       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   451         | add_tcs (Abs (_, T, u)) x = add_tcs u x
   452         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   453         | add_tcs _ x = x
   454   in  add_tcs  end
   455 
   456 fun type_consts_of_terms thy ts =
   457   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   458 
   459 
   460 (***************************************************************)
   461 (* ATP invocation methods setup                                *)
   462 (***************************************************************)
   463 
   464 (*Ensures that no higher-order theorems "leak out"*)
   465 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   466   | restrict_to_logic thy false cls = cls;
   467 
   468 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   469 
   470 (** Too general means, positive equality literal with a variable X as one operand,
   471   when X does not occur properly in the other operand. This rules out clearly
   472   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   473 
   474 fun occurs ix =
   475     let fun occ(Var (jx,_)) = (ix=jx)
   476           | occ(t1$t2)      = occ t1 orelse occ t2
   477           | occ(Abs(_,_,t)) = occ t
   478           | occ _           = false
   479     in occ end;
   480 
   481 fun is_recordtype T = not (null (Record.dest_recTs T));
   482 
   483 (*Unwanted equalities include
   484   (1) those between a variable that does not properly occur in the second operand,
   485   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   486 *)
   487 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   488   | too_general_eqterms _ = false;
   489 
   490 fun too_general_equality (Const ("op =", _) $ x $ y) =
   491       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   492   | too_general_equality _ = false;
   493 
   494 (* tautologous? *)
   495 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   496   | is_taut _ = false;
   497 
   498 fun has_typed_var tycons = exists_subterm
   499   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
   500 
   501 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   502   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   503   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   504   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   505 val unwanted_types = ["Product_Type.unit","bool"];
   506 
   507 fun unwanted t =
   508   is_taut t orelse has_typed_var unwanted_types t orelse
   509   forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   510 
   511 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   512   likely to lead to unsound proofs.*)
   513 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   514 
   515 fun isFO thy goal_cls = case linkup_logic_mode of
   516       Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   517     | Fol => true
   518     | Hol => false
   519 
   520 fun ths_to_cls thy ths =
   521   ResAxioms.cnf_rules_pairs thy (filter check_named (map ResAxioms.pairname ths))
   522 
   523 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   524   let
   525     val thy = ProofContext.theory_of ctxt
   526     val isFO = isFO thy goal_cls
   527     val included_thms = get_clasimp_atp_lemmas ctxt
   528     val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
   529                                      |> restrict_to_logic thy isFO
   530                                      |> remove_unwanted_clauses
   531     val axcls = relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
   532     (* add whitelist *)
   533     val white_cls = ths_to_cls thy (whitelist_fo @ (if isFO then [] else whitelist_ho))
   534   in
   535     white_cls @ axcls 
   536   end;
   537 
   538 (* prepare for passing to writer,
   539    create additional clauses based on the information from extra_cls *)
   540 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   541   let
   542     (* add chain thms *)
   543     val chain_cls = ths_to_cls thy chain_ths
   544     val axcls = chain_cls @ axcls
   545     val extra_cls = chain_cls @ extra_cls
   546     val isFO = isFO thy goal_cls
   547     val ccls = subtract_cls goal_cls extra_cls
   548     val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm_global thy th)) ccls
   549     val ccltms = map prop_of ccls
   550     and axtms = map (prop_of o #1) extra_cls
   551     val subs = tfree_classes_of_terms ccltms
   552     and supers = tvar_classes_of_terms axtms
   553     and tycons = type_consts_of_terms thy (ccltms@axtms)
   554     (*TFrees in conjecture clauses; TVars in axiom clauses*)
   555     val conjectures = ResHolClause.make_conjecture_clauses dfg thy ccls
   556     val (_, extra_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy extra_cls)
   557     val (clnames,axiom_clauses) = ListPair.unzip (ResHolClause.make_axiom_clauses dfg thy axcls)
   558     val helper_clauses = ResHolClause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   559     val (supers',arity_clauses) = ResClause.make_arity_clauses_dfg dfg thy tycons supers
   560     val classrel_clauses = ResClause.make_classrel_clauses thy subs supers'
   561   in
   562     (Vector.fromList clnames,
   563       (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   564   end
   565 
   566 end;
   567