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