src/HOL/Tools/res_atp.ML
author wenzelm
Thu Nov 12 20:33:26 2009 +0100 (2009-11-12 ago)
changeset 33641 af07d9cd86ce
parent 33316 6a72af4e84b8
permissions -rw-r--r--
all_valid_thms: more sophisticated check against global + local name space;
     1 (*  Title:      HOL/Tools/res_atp.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory, NICTA
     3 *)
     4 
     5 signature RES_ATP =
     6 sig
     7   datatype mode = Auto | Fol | Hol
     8   val tvar_classes_of_terms : term list -> string list
     9   val tfree_classes_of_terms : term list -> string list
    10   val type_consts_of_terms : theory -> term list -> string list
    11   val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
    12     (thm * (string * int)) list
    13   val prepare_clauses : bool -> thm list -> thm list ->
    14     (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list ->
    15     (thm * (Res_HOL_Clause.axiom_name * Res_HOL_Clause.clause_id)) list -> theory ->
    16     Res_HOL_Clause.axiom_name vector *
    17       (Res_HOL_Clause.clause list * Res_HOL_Clause.clause list * Res_HOL_Clause.clause list *
    18       Res_HOL_Clause.clause list * Res_Clause.classrelClause list * Res_Clause.arityClause list)
    19 end;
    20 
    21 structure Res_ATP: RES_ATP =
    22 struct
    23 
    24 
    25 (********************************************************************)
    26 (* some settings for both background automatic ATP calling procedure*)
    27 (* and also explicit ATP invocation methods                         *)
    28 (********************************************************************)
    29 
    30 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
    31 datatype mode = Auto | Fol | Hol;
    32 
    33 val linkup_logic_mode = Auto;
    34 
    35 (*** background linkup ***)
    36 val run_blacklist_filter = true;
    37 
    38 (*** relevance filter parameters ***)
    39 val run_relevance_filter = true;
    40 val pass_mark = 0.5;
    41 val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
    42 val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
    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 _ (_, 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 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
   217               forall is_Var args andalso uni_mem gctypes ct andalso
   218                 subset (op =) (Term.add_vars rhs [], Term.add_vars lhs [])
   219             end
   220             handle ConstFree => false
   221     in    
   222         case tm of Const ("Trueprop",_) $ (Const("op =",_) $ lhs $ rhs) => 
   223                    defs lhs rhs 
   224                  | _ => false
   225     end;
   226 
   227 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
   228        
   229 (*For a reverse sort, putting the largest values first.*)
   230 fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
   231 
   232 (*Limit the number of new clauses, to prevent runaway acceptance.*)
   233 fun take_best max_new (newpairs : (annotd_cls*real) list) =
   234   let val nnew = length newpairs
   235   in
   236     if nnew <= max_new then (map #1 newpairs, [])
   237     else 
   238       let val cls = sort compare_pairs newpairs
   239           val accepted = List.take (cls, max_new)
   240       in
   241         Res_Axioms.trace_msg (fn () => ("Number of candidates, " ^ Int.toString nnew ^ 
   242                        ", exceeds the limit of " ^ Int.toString (max_new)));
   243         Res_Axioms.trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
   244         Res_Axioms.trace_msg (fn () => "Actually passed: " ^
   245           space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
   246 
   247         (map #1 accepted, map #1 (List.drop (cls, max_new)))
   248       end
   249   end;
   250 
   251 fun relevant_clauses max_new thy ctab p rel_consts =
   252   let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
   253         | relevant (newpairs,rejects) [] =
   254             let val (newrels,more_rejects) = take_best max_new newpairs
   255                 val new_consts = maps #2 newrels
   256                 val rel_consts' = List.foldl add_const_typ_table rel_consts new_consts
   257                 val newp = p + (1.0-p) / convergence
   258             in
   259               Res_Axioms.trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
   260                (map #1 newrels) @ 
   261                (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
   262             end
   263         | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
   264             let val weight = clause_weight ctab rel_consts consts_typs
   265             in
   266               if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
   267               then (Res_Axioms.trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
   268                                             " passes: " ^ Real.toString weight));
   269                     relevant ((ax,weight)::newrels, rejects) axs)
   270               else relevant (newrels, ax::rejects) axs
   271             end
   272     in  Res_Axioms.trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
   273         relevant ([],[]) 
   274     end;
   275         
   276 fun relevance_filter max_new theory_const thy axioms goals = 
   277  if run_relevance_filter andalso pass_mark >= 0.1
   278  then
   279   let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
   280       val goal_const_tab = get_goal_consts_typs thy goals
   281       val _ = Res_Axioms.trace_msg (fn () => ("Initial constants: " ^
   282                                  space_implode ", " (Symtab.keys goal_const_tab)));
   283       val rels = relevant_clauses max_new thy const_tab (pass_mark) 
   284                    goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
   285   in
   286       Res_Axioms.trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
   287       rels
   288   end
   289  else axioms;
   290 
   291 (***************************************************************)
   292 (* Retrieving and filtering lemmas                             *)
   293 (***************************************************************)
   294 
   295 (*** retrieve lemmas and filter them ***)
   296 
   297 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   298 
   299 fun setinsert (x,s) = Symtab.update (x,()) s;
   300 
   301 (*Reject theorems with names like "List.filter.filter_list_def" or
   302   "Accessible_Part.acc.defs", as these are definitions arising from packages.*)
   303 fun is_package_def a =
   304   let val names = Long_Name.explode a
   305   in
   306      length names > 2 andalso
   307      not (hd names = "local") andalso
   308      String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a
   309   end;
   310 
   311 (** a hash function from Term.term to int, and also a hash table **)
   312 val xor_words = List.foldl Word.xorb 0w0;
   313 
   314 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   315   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   316   | hashw_term ((Var(_,_)), w) = w
   317   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   318   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   319   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   320 
   321 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_term(P,0w0))
   322   | hash_literal P = hashw_term(P,0w0);
   323 
   324 fun hash_term t = Word.toIntX (xor_words (map hash_literal (HOLogic.disjuncts (strip_Trueprop t))));
   325 
   326 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   327 
   328 exception HASH_CLAUSE;
   329 
   330 (*Create a hash table for clauses, of the given size*)
   331 fun mk_clause_table n =
   332       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   333                        (n, HASH_CLAUSE);
   334 
   335 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   336   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   337 fun make_unique xs =
   338   let val ht = mk_clause_table 7000
   339   in
   340       Res_Axioms.trace_msg (fn () => ("make_unique gets " ^ Int.toString (length xs) ^ " clauses"));
   341       app (ignore o Polyhash.peekInsert ht) xs;
   342       Polyhash.listItems ht
   343   end;
   344 
   345 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   346   boost an ATP's performance (for some reason)*)
   347 fun subtract_cls c_clauses ax_clauses =
   348   let val ht = mk_clause_table 2200
   349       fun known x = is_some (Polyhash.peek ht x)
   350   in
   351       app (ignore o Polyhash.peekInsert ht) ax_clauses;
   352       filter (not o known) c_clauses
   353   end;
   354 
   355 fun all_valid_thms ctxt =
   356   let
   357     val global_facts = PureThy.facts_of (ProofContext.theory_of ctxt);
   358     val local_facts = ProofContext.facts_of ctxt;
   359     val full_space =
   360       Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts);
   361 
   362     fun valid_facts facts =
   363       (facts, []) |-> Facts.fold_static (fn (name, ths0) =>
   364         let
   365           fun check_thms a =
   366             (case try (ProofContext.get_thms ctxt) a of
   367               NONE => false
   368             | SOME ths1 => Thm.eq_thms (ths0, ths1));
   369 
   370           val name1 = Facts.extern facts name;
   371           val name2 = Name_Space.extern full_space name;
   372           val ths = filter_out Res_Axioms.bad_for_atp ths0;
   373         in
   374           if Facts.is_concealed facts name orelse null ths orelse
   375             run_blacklist_filter andalso is_package_def name then I
   376           else
   377             (case find_first check_thms [name1, name2, name] of
   378               NONE => I
   379             | SOME a => cons (a, ths))
   380         end);
   381   in valid_facts global_facts @ valid_facts local_facts end;
   382 
   383 fun multi_name a th (n, pairs) =
   384   (n + 1, (a ^ "(" ^ Int.toString n ^ ")", th) :: pairs);
   385 
   386 fun add_single_names (a, []) pairs = pairs
   387   | add_single_names (a, [th]) pairs = (a, th) :: pairs
   388   | add_single_names (a, ths) pairs = #2 (fold (multi_name a) ths (1, pairs));
   389 
   390 (*Ignore blacklisted basenames*)
   391 fun add_multi_names (a, ths) pairs =
   392   if (Long_Name.base_name a) mem_string Res_Axioms.multi_base_blacklist then pairs
   393   else add_single_names (a, ths) pairs;
   394 
   395 fun is_multi (a, ths) = length ths > 1 orelse String.isSuffix ".axioms" a;
   396 
   397 (*The single theorems go BEFORE the multiple ones. Blacklist is applied to all.*)
   398 fun name_thm_pairs ctxt =
   399   let
   400     val (mults, singles) = List.partition is_multi (all_valid_thms ctxt)
   401     fun blacklisted (_, th) =
   402       run_blacklist_filter andalso Res_Blacklist.blacklisted ctxt th
   403   in
   404     filter_out blacklisted
   405       (fold add_single_names singles (fold add_multi_names mults []))
   406   end;
   407 
   408 fun check_named ("", th) =
   409       (warning ("No name for theorem " ^ Display.string_of_thm_without_context th); false)
   410   | check_named _ = true;
   411 
   412 fun get_all_lemmas ctxt =
   413   let val included_thms =
   414         tap (fn ths => Res_Axioms.trace_msg
   415                      (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
   416             (name_thm_pairs ctxt)
   417   in
   418     filter check_named included_thms
   419   end;
   420 
   421 (***************************************************************)
   422 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
   423 (***************************************************************)
   424 
   425 fun add_classes (sorts, cset) = List.foldl setinsert cset (flat sorts);
   426 
   427 (*Remove this trivial type class*)
   428 fun delete_type cset = Symtab.delete_safe "HOL.type" cset;
   429 
   430 fun tvar_classes_of_terms ts =
   431   let val sorts_list = map (map #2 o OldTerm.term_tvars) ts
   432   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   433 
   434 fun tfree_classes_of_terms ts =
   435   let val sorts_list = map (map #2 o OldTerm.term_tfrees) ts
   436   in  Symtab.keys (delete_type (List.foldl add_classes Symtab.empty sorts_list))  end;
   437 
   438 (*fold type constructors*)
   439 fun fold_type_consts f (Type (a, Ts)) x = fold (fold_type_consts f) Ts (f (a,x))
   440   | fold_type_consts _ _ x = x;
   441 
   442 val add_type_consts_in_type = fold_type_consts setinsert;
   443 
   444 (*Type constructors used to instantiate overloaded constants are the only ones needed.*)
   445 fun add_type_consts_in_term thy =
   446   let val const_typargs = Sign.const_typargs thy
   447       fun add_tcs (Const cT) x = fold add_type_consts_in_type (const_typargs cT) x
   448         | add_tcs (Abs (_, _, u)) x = add_tcs u x
   449         | add_tcs (t $ u) x = add_tcs t (add_tcs u x)
   450         | add_tcs _ x = x
   451   in  add_tcs  end
   452 
   453 fun type_consts_of_terms thy ts =
   454   Symtab.keys (fold (add_type_consts_in_term thy) ts Symtab.empty);
   455 
   456 
   457 (***************************************************************)
   458 (* ATP invocation methods setup                                *)
   459 (***************************************************************)
   460 
   461 (*Ensures that no higher-order theorems "leak out"*)
   462 fun restrict_to_logic thy true cls = filter (Meson.is_fol_term thy o prop_of o fst) cls
   463   | restrict_to_logic thy false cls = cls;
   464 
   465 (**** Predicates to detect unwanted clauses (prolific or likely to cause unsoundness) ****)
   466 
   467 (** Too general means, positive equality literal with a variable X as one operand,
   468   when X does not occur properly in the other operand. This rules out clearly
   469   inconsistent clauses such as V=a|V=b, though it by no means guarantees soundness. **)
   470 
   471 fun occurs ix =
   472     let fun occ(Var (jx,_)) = (ix=jx)
   473           | occ(t1$t2)      = occ t1 orelse occ t2
   474           | occ(Abs(_,_,t)) = occ t
   475           | occ _           = false
   476     in occ end;
   477 
   478 fun is_recordtype T = not (null (Record.dest_recTs T));
   479 
   480 (*Unwanted equalities include
   481   (1) those between a variable that does not properly occur in the second operand,
   482   (2) those between a variable and a record, since these seem to be prolific "cases" thms
   483 *)
   484 fun too_general_eqterms (Var (ix,T), t) = not (occurs ix t) orelse is_recordtype T
   485   | too_general_eqterms _ = false;
   486 
   487 fun too_general_equality (Const ("op =", _) $ x $ y) =
   488       too_general_eqterms (x,y) orelse too_general_eqterms(y,x)
   489   | too_general_equality _ = false;
   490 
   491 (* tautologous? *)
   492 fun is_taut (Const ("Trueprop", _) $ Const ("True", _)) = true
   493   | is_taut _ = false;
   494 
   495 fun has_typed_var tycons = exists_subterm
   496   (fn Var (_, Type (a, _)) => member (op =) tycons a | _ => false);
   497 
   498 (*Clauses are forbidden to contain variables of these types. The typical reason is that
   499   they lead to unsoundness. Note that "unit" satisfies numerous equations like ?X=().
   500   The resulting clause will have no type constraint, yielding false proofs. Even "bool"
   501   leads to many unsound proofs, though (obviously) only for higher-order problems.*)
   502 val unwanted_types = ["Product_Type.unit","bool"];
   503 
   504 fun unwanted t =
   505   is_taut t orelse has_typed_var unwanted_types t orelse
   506   forall too_general_equality (HOLogic.disjuncts (strip_Trueprop t));
   507 
   508 (*Clauses containing variables of type "unit" or "bool" are unlikely to be useful and
   509   likely to lead to unsound proofs.*)
   510 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
   511 
   512 fun isFO thy goal_cls = case linkup_logic_mode of
   513       Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
   514     | Fol => true
   515     | Hol => false
   516 
   517 fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
   518   let
   519     val thy = ProofContext.theory_of ctxt
   520     val isFO = isFO thy goal_cls
   521     val included_cls = get_all_lemmas ctxt
   522       |> Res_Axioms.cnf_rules_pairs thy |> make_unique
   523       |> restrict_to_logic thy isFO
   524       |> remove_unwanted_clauses
   525   in
   526     relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
   527   end;
   528 
   529 (* prepare for passing to writer,
   530    create additional clauses based on the information from extra_cls *)
   531 fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
   532   let
   533     (* add chain thms *)
   534     val chain_cls =
   535       Res_Axioms.cnf_rules_pairs thy (filter check_named (map Res_Axioms.pairname chain_ths))
   536     val axcls = chain_cls @ axcls
   537     val extra_cls = chain_cls @ extra_cls
   538     val isFO = isFO thy goal_cls
   539     val ccls = subtract_cls goal_cls extra_cls
   540     val _ = app (fn th => Res_Axioms.trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
   541     val ccltms = map prop_of ccls
   542     and axtms = map (prop_of o #1) extra_cls
   543     val subs = tfree_classes_of_terms ccltms
   544     and supers = tvar_classes_of_terms axtms
   545     and tycons = type_consts_of_terms thy (ccltms@axtms)
   546     (*TFrees in conjecture clauses; TVars in axiom clauses*)
   547     val conjectures = Res_HOL_Clause.make_conjecture_clauses dfg thy ccls
   548     val (_, extra_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy extra_cls)
   549     val (clnames,axiom_clauses) = ListPair.unzip (Res_HOL_Clause.make_axiom_clauses dfg thy axcls)
   550     val helper_clauses = Res_HOL_Clause.get_helper_clauses dfg thy isFO (conjectures, extra_cls, [])
   551     val (supers',arity_clauses) = Res_Clause.make_arity_clauses_dfg dfg thy tycons supers
   552     val classrel_clauses = Res_Clause.make_classrel_clauses thy subs supers'
   553   in
   554     (Vector.fromList clnames,
   555       (conjectures, axiom_clauses, extra_clauses, helper_clauses, classrel_clauses, arity_clauses))
   556   end
   557 
   558 end;
   559