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