src/HOL/Tools/res_atp.ML
author paulson
Fri Oct 06 15:38:29 2006 +0200 (2006-10-06)
changeset 20870 992bcbff055a
parent 20868 724ab9896068
child 20954 3bbe7cab8037
permissions -rw-r--r--
Tidied code to delete tmp files.
Fixed the printing of the used theorems by maintaining separate lists for each subgoal.
     1 (*  Author: Jia Meng, Cambridge University Computer Laboratory, NICTA
     2     ID: $Id$
     3     Copyright 2004 University of Cambridge
     4 
     5 ATPs with TPTP format input.
     6 *)
     7 
     8 (*FIXME: Do we need this signature?*)
     9 signature RES_ATP =
    10 sig
    11   val prover: string ref
    12   val custom_spass: string list ref
    13   val destdir: string ref
    14   val helper_path: string -> string -> string
    15   val problem_name: string ref
    16   val time_limit: int ref
    17    
    18   datatype mode = Auto | Fol | Hol
    19   val linkup_logic_mode : mode ref
    20   val write_subgoal_file: bool -> mode -> Proof.context -> thm list -> thm list -> int -> string
    21   val vampire_time: int ref
    22   val eprover_time: int ref
    23   val spass_time: int ref
    24   val run_vampire: int -> unit
    25   val run_eprover: int -> unit
    26   val run_spass: int -> unit
    27   val vampireLimit: unit -> int
    28   val eproverLimit: unit -> int
    29   val spassLimit: unit -> int
    30   val atp_method: (Proof.context -> thm list -> int -> tactic) ->
    31     Method.src -> Proof.context -> Proof.method
    32   val cond_rm_tmp: string -> unit
    33   val fol_keep_types: bool ref
    34   val hol_full_types: unit -> unit
    35   val hol_partial_types: unit -> unit
    36   val hol_const_types_only: unit -> unit
    37   val hol_no_types: unit -> unit
    38   val hol_typ_level: unit -> ResHolClause.type_level
    39   val include_all: bool ref
    40   val run_relevance_filter: bool ref
    41   val run_blacklist_filter: bool ref
    42   val blacklist: string list ref
    43   val add_all : unit -> unit
    44   val add_claset : unit -> unit
    45   val add_simpset : unit -> unit
    46   val add_clasimp : unit -> unit
    47   val add_atpset : unit -> unit
    48   val rm_all : unit -> unit
    49   val rm_claset : unit -> unit
    50   val rm_simpset : unit -> unit
    51   val rm_atpset : unit -> unit
    52   val rm_clasimp : unit -> unit
    53 end;
    54 
    55 structure ResAtp =
    56 struct
    57 
    58 (********************************************************************)
    59 (* some settings for both background automatic ATP calling procedure*)
    60 (* and also explicit ATP invocation methods                         *)
    61 (********************************************************************)
    62 
    63 (*** background linkup ***)
    64 val call_atp = ref false; 
    65 val hook_count = ref 0;
    66 val time_limit = ref 80;
    67 val prover = ref "E";   (* use E as the default prover *)
    68 val custom_spass =   (*specialized options for SPASS*)
    69       ref ["-Auto=0","-FullRed=0","-IORe","-IOFc","-RTaut","-RFSub","-RBSub"];
    70 val destdir = ref "";   (*Empty means write files to /tmp*)
    71 val problem_name = ref "prob";
    72 
    73 (*Return the path to a "helper" like SPASS or tptp2X, first checking that
    74   it exists.  FIXME: modify to use Path primitives and move to some central place.*)  
    75 fun helper_path evar base =
    76   case getenv evar of
    77       "" => error  ("Isabelle environment variable " ^ evar ^ " not defined")
    78     | home => 
    79         let val path = home ^ "/" ^ base
    80         in  if File.exists (File.unpack_platform_path path) then path 
    81 	    else error ("Could not find the file " ^ path)
    82 	end;  
    83 
    84 fun probfile_nosuffix _ = 
    85   if !destdir = "" then File.platform_path (File.tmp_path (Path.basic (!problem_name)))
    86   else if File.exists (File.unpack_platform_path (!destdir))
    87   then !destdir ^ "/" ^ !problem_name
    88   else error ("No such directory: " ^ !destdir);
    89 
    90 fun prob_pathname n = probfile_nosuffix n ^ "_" ^ Int.toString n;
    91 
    92 
    93 (*** ATP methods ***)
    94 val vampire_time = ref 60;
    95 val eprover_time = ref 60;
    96 val spass_time = ref 60;
    97 
    98 fun run_vampire time =  
    99     if (time >0) then vampire_time:= time
   100     else vampire_time:=60;
   101 
   102 fun run_eprover time = 
   103     if (time > 0) then eprover_time:= time
   104     else eprover_time:=60;
   105 
   106 fun run_spass time = 
   107     if (time > 0) then spass_time:=time
   108     else spass_time:=60;
   109 
   110 
   111 fun vampireLimit () = !vampire_time;
   112 fun eproverLimit () = !eprover_time;
   113 fun spassLimit () = !spass_time;
   114 
   115 val fol_keep_types = ResClause.keep_types;
   116 val hol_full_types = ResHolClause.full_types;
   117 val hol_partial_types = ResHolClause.partial_types;
   118 val hol_const_types_only = ResHolClause.const_types_only;
   119 val hol_no_types = ResHolClause.no_types;
   120 fun hol_typ_level () = ResHolClause.find_typ_level ();
   121 fun is_typed_hol () = 
   122     let val tp_level = hol_typ_level()
   123     in
   124 	not (tp_level = ResHolClause.T_NONE)
   125     end;
   126 
   127 fun atp_input_file () =
   128     let val file = !problem_name 
   129     in
   130 	if !destdir = "" then File.platform_path (File.tmp_path (Path.basic file))
   131 	else if File.exists (File.unpack_platform_path (!destdir))
   132 	then !destdir ^ "/" ^ file
   133 	else error ("No such directory: " ^ !destdir)
   134     end;
   135 
   136 val include_all = ref true;
   137 val include_simpset = ref false;
   138 val include_claset = ref false; 
   139 val include_atpset = ref true;
   140 
   141 (*Tests show that follow_defs gives VERY poor results with "include_all"*)
   142 fun add_all() = (include_all:=true; ReduceAxiomsN.follow_defs := false);
   143 fun rm_all() = include_all:=false;
   144 
   145 fun add_simpset() = include_simpset:=true;
   146 fun rm_simpset() = include_simpset:=false;
   147 
   148 fun add_claset() = include_claset:=true;
   149 fun rm_claset() = include_claset:=false;
   150 
   151 fun add_clasimp() = (include_simpset:=true;include_claset:=true);
   152 fun rm_clasimp() = (include_simpset:=false;include_claset:=false);
   153 
   154 fun add_atpset() = include_atpset:=true;
   155 fun rm_atpset() = include_atpset:=false;
   156 
   157 
   158 (**** relevance filter ****)
   159 val run_relevance_filter = ReduceAxiomsN.run_relevance_filter;
   160 val run_blacklist_filter = ref true;
   161 
   162 (******************************************************************)
   163 (* detect whether a given problem (clauses) is FOL/HOL/HOLC/HOLCS *)
   164 (******************************************************************)
   165 
   166 datatype logic = FOL | HOL | HOLC | HOLCS;
   167 
   168 fun string_of_logic FOL = "FOL"
   169   | string_of_logic HOL = "HOL"
   170   | string_of_logic HOLC = "HOLC"
   171   | string_of_logic HOLCS = "HOLCS";
   172 
   173 fun is_fol_logic FOL = true
   174   | is_fol_logic  _ = false
   175 
   176 (*HOLCS will not occur here*)
   177 fun upgrade_lg HOLC _ = HOLC
   178   | upgrade_lg HOL HOLC = HOLC
   179   | upgrade_lg HOL _ = HOL
   180   | upgrade_lg FOL lg = lg; 
   181 
   182 (* check types *)
   183 fun has_bool_hfn (Type("bool",_)) = true
   184   | has_bool_hfn (Type("fun",_)) = true
   185   | has_bool_hfn (Type(_, Ts)) = exists has_bool_hfn Ts
   186   | has_bool_hfn _ = false;
   187 
   188 fun is_hol_fn tp =
   189     let val (targs,tr) = strip_type tp
   190     in
   191 	exists (has_bool_hfn) (tr::targs)
   192     end;
   193 
   194 fun is_hol_pred tp =
   195     let val (targs,tr) = strip_type tp
   196     in
   197 	exists (has_bool_hfn) targs
   198     end;
   199 
   200 exception FN_LG of term;
   201 
   202 fun fn_lg (t as Const(f,tp)) (lg,seen) = 
   203     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   204   | fn_lg (t as Free(f,tp)) (lg,seen) = 
   205     if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   206   | fn_lg (t as Var(f,tp)) (lg,seen) =
   207     if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
   208   | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
   209   | fn_lg f _ = raise FN_LG(f); 
   210 
   211 
   212 fun term_lg [] (lg,seen) = (lg,seen)
   213   | term_lg (tm::tms) (FOL,seen) =
   214       let val (f,args) = strip_comb tm
   215 	  val (lg',seen') = if f mem seen then (FOL,seen) 
   216 			    else fn_lg f (FOL,seen)
   217       in
   218 	if is_fol_logic lg' then ()
   219         else Output.debug ("Found a HOL term: " ^ Display.raw_string_of_term f);
   220         term_lg (args@tms) (lg',seen')
   221       end
   222   | term_lg _ (lg,seen) = (lg,seen)
   223 
   224 exception PRED_LG of term;
   225 
   226 fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   227       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
   228   | pred_lg (t as Free(P,tp)) (lg,seen) =
   229       if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
   230   | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   231   | pred_lg P _ = raise PRED_LG(P);
   232 
   233 
   234 fun lit_lg (Const("Not",_) $ P) (lg,seen) = lit_lg P (lg,seen)
   235   | lit_lg P (lg,seen) =
   236       let val (pred,args) = strip_comb P
   237 	  val (lg',seen') = if pred mem seen then (lg,seen) 
   238 			    else pred_lg pred (lg,seen)
   239       in
   240 	if is_fol_logic lg' then ()
   241 	else Output.debug ("Found a HOL predicate: " ^ Display.raw_string_of_term pred);
   242 	term_lg args (lg',seen')
   243       end;
   244 
   245 fun lits_lg [] (lg,seen) = (lg,seen)
   246   | lits_lg (lit::lits) (FOL,seen) =
   247       let val (lg,seen') = lit_lg lit (FOL,seen)
   248       in
   249 	if is_fol_logic lg then ()
   250 	else Output.debug ("Found a HOL literal: " ^ Display.raw_string_of_term lit);
   251 	lits_lg lits (lg,seen')
   252       end
   253   | lits_lg lits (lg,seen) = (lg,seen);
   254 
   255 fun dest_disj_aux (Const ("op |", _) $ t $ t') disjs = 
   256     dest_disj_aux t (dest_disj_aux t' disjs)
   257   | dest_disj_aux t disjs = t::disjs;
   258 
   259 fun dest_disj t = dest_disj_aux t [];
   260 
   261 fun logic_of_clause tm (lg,seen) =
   262     let val tm' = HOLogic.dest_Trueprop tm
   263 	val disjs = dest_disj tm'
   264     in
   265 	lits_lg disjs (lg,seen)
   266     end;
   267 
   268 fun logic_of_clauses [] (lg,seen) = (lg,seen)
   269   | logic_of_clauses (cls::clss) (FOL,seen) =
   270     let val (lg,seen') = logic_of_clause cls (FOL,seen)
   271 	val _ =
   272           if is_fol_logic lg then ()
   273           else Output.debug ("Found a HOL clause: " ^ Display.raw_string_of_term cls)
   274     in
   275 	logic_of_clauses clss (lg,seen')
   276     end
   277   | logic_of_clauses (cls::clss) (lg,seen) = (lg,seen);
   278 
   279 fun problem_logic_goals_aux [] (lg,seen) = lg
   280   | problem_logic_goals_aux (subgoal::subgoals) (lg,seen) = 
   281     problem_logic_goals_aux subgoals (logic_of_clauses subgoal (lg,seen));
   282     
   283 fun problem_logic_goals subgoals = problem_logic_goals_aux subgoals (FOL,[]);
   284 
   285 (***************************************************************)
   286 (* Retrieving and filtering lemmas                             *)
   287 (***************************************************************)
   288 
   289 (*** white list and black list of lemmas ***)
   290 
   291 (*The rule subsetI is frequently omitted by the relevance filter.*)
   292 val whitelist = ref [subsetI]; 
   293 
   294 (*Names of theorems and theorem lists to be banned. The final numeric suffix of
   295   theorem lists is first removed.
   296 
   297   These theorems typically produce clauses that are prolific (match too many equality or
   298   membership literals) and relate to seldom-used facts. Some duplicate other rules.
   299   FIXME: this blacklist needs to be maintained using theory data and added to using
   300   an attribute.*)
   301 val blacklist = ref
   302   ["Datatype.prod.size",
   303    "Datatype.unit.induct", (*"unit" thms cause unsound proofs; unit.nchotomy is caught automatically*)
   304    "Datatype.unit.inducts",
   305    "Datatype.unit.split_asm", 
   306    "Datatype.unit.split",
   307    "Datatype.unit.splits",
   308    "Divides.dvd_0_left_iff",
   309    "Finite_Set.card_0_eq",
   310    "Finite_Set.card_infinite",
   311    "Finite_Set.Max_ge",
   312    "Finite_Set.Max_in",
   313    "Finite_Set.Max_le_iff",
   314    "Finite_Set.Max_less_iff",
   315    "Finite_Set.max.f_below_strict_below.below_f_conv", (*duplicates in Orderings.*)
   316    "Finite_Set.max.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   317    "Finite_Set.Min_ge_iff",
   318    "Finite_Set.Min_gr_iff",
   319    "Finite_Set.Min_in",
   320    "Finite_Set.Min_le",
   321    "Finite_Set.min_max.below_inf_sup_Inf_Sup.inf_Sup_absorb", 
   322    "Finite_Set.min_max.below_inf_sup_Inf_Sup.sup_Inf_absorb", 
   323    "Finite_Set.min.f_below_strict_below.below_f_conv",        (*duplicates in Orderings.*)
   324    "Finite_Set.min.f_below_strict_below.strict_below_f_conv", (*duplicates in Orderings.*)
   325    "Fun.vimage_image_eq",   (*involves an existential quantifier*)
   326    "HOL.split_if_asm",     (*splitting theorem*)
   327    "HOL.split_if",         (*splitting theorem*)
   328    "IntDef.abs_split",
   329    "IntDef.Integ.Abs_Integ_inject",
   330    "IntDef.Integ.Abs_Integ_inverse",
   331    "IntDiv.zdvd_0_left",
   332    "List.append_eq_append_conv",
   333    "List.hd_Cons_tl",   (*Says everything is [] or Cons. Probably prolific.*)
   334    "List.in_listsD",
   335    "List.in_listsI",
   336    "List.lists.Cons",
   337    "List.listsE",
   338    "Nat.less_one", (*not directional? obscure*)
   339    "Nat.not_gr0",
   340    "Nat.one_eq_mult_iff", (*duplicate by symmetry*)
   341    "NatArith.of_nat_0_eq_iff",
   342    "NatArith.of_nat_eq_0_iff",
   343    "NatArith.of_nat_le_0_iff",
   344    "NatSimprocs.divide_le_0_iff_number_of",  (*too many clauses*)
   345    "NatSimprocs.divide_less_0_iff_number_of",
   346    "NatSimprocs.equation_minus_iff_1",  (*not directional*)
   347    "NatSimprocs.equation_minus_iff_number_of", (*not directional*)
   348    "NatSimprocs.le_minus_iff_1", (*not directional*)
   349    "NatSimprocs.le_minus_iff_number_of",  (*not directional*)
   350    "NatSimprocs.less_minus_iff_1", (*not directional*)
   351    "NatSimprocs.less_minus_iff_number_of", (*not directional*)
   352    "NatSimprocs.minus_equation_iff_number_of", (*not directional*)
   353    "NatSimprocs.minus_le_iff_1", (*not directional*)
   354    "NatSimprocs.minus_le_iff_number_of", (*not directional*)
   355    "NatSimprocs.minus_less_iff_1", (*not directional*)
   356    "NatSimprocs.mult_le_cancel_left_number_of", (*excessive case analysis*)
   357    "NatSimprocs.mult_le_cancel_right_number_of", (*excessive case analysis*)
   358    "NatSimprocs.mult_less_cancel_left_number_of", (*excessive case analysis*)
   359    "NatSimprocs.mult_less_cancel_right_number_of", (*excessive case analysis*)
   360    "NatSimprocs.zero_le_divide_iff_number_of", (*excessive case analysis*)
   361    "NatSimprocs.zero_less_divide_iff_number_of",
   362    "OrderedGroup.abs_0_eq", (*duplicate by symmetry*)
   363    "OrderedGroup.diff_eq_0_iff_eq", (*prolific?*)
   364    "OrderedGroup.join_0_eq_0",
   365    "OrderedGroup.meet_0_eq_0",
   366    "OrderedGroup.pprt_eq_0",   (*obscure*)
   367    "OrderedGroup.pprt_eq_id",   (*obscure*)
   368    "OrderedGroup.pprt_mono",   (*obscure*)
   369    "Orderings.split_max",      (*splitting theorem*)
   370    "Orderings.split_min",      (*splitting theorem*)
   371    "Parity.even_nat_power",   (*obscure, somewhat prolilfic*)
   372    "Parity.power_eq_0_iff_number_of",
   373    "Parity.power_le_zero_eq_number_of",   (*obscure and prolific*)
   374    "Parity.power_less_zero_eq_number_of",
   375    "Parity.zero_le_power_eq_number_of",   (*obscure and prolific*)
   376    "Parity.zero_less_power_eq_number_of",   (*obscure and prolific*)
   377    "Power.zero_less_power_abs_iff",
   378    "Product_Type.split_eta_SetCompr",   (*involves an existential quantifier*)
   379    "Product_Type.split_paired_Ball_Sigma",     (*splitting theorem*)
   380    "Product_Type.split_paired_Bex_Sigma",      (*splitting theorem*)
   381    "Product_Type.split_split_asm",             (*splitting theorem*)
   382    "Product_Type.split_split",                 (*splitting theorem*)
   383    "Product_Type.unit_abs_eta_conv",
   384    "Product_Type.unit_induct",
   385    "Relation.diagI",
   386    "Relation.Domain_def",   (*involves an existential quantifier*)
   387    "Relation.Image_def",   (*involves an existential quantifier*)
   388    "Relation.ImageI",
   389    "Ring_and_Field.divide_cancel_left", (*fields are seldom used & often prolific*)
   390    "Ring_and_Field.divide_cancel_right",
   391    "Ring_and_Field.divide_divide_eq_left",
   392    "Ring_and_Field.divide_divide_eq_right",
   393    "Ring_and_Field.divide_eq_0_iff",
   394    "Ring_and_Field.divide_eq_1_iff",
   395    "Ring_and_Field.divide_eq_eq_1",
   396    "Ring_and_Field.divide_le_0_1_iff",
   397    "Ring_and_Field.divide_le_eq_1_neg",  (*obscure and prolific*)
   398    "Ring_and_Field.divide_le_eq_1_pos",  (*obscure and prolific*)
   399    "Ring_and_Field.divide_less_0_1_iff",
   400    "Ring_and_Field.divide_less_eq_1_neg",  (*obscure and prolific*)
   401    "Ring_and_Field.divide_less_eq_1_pos",  (*obscure and prolific*)
   402    "Ring_and_Field.eq_divide_eq_1", (*duplicate by symmetry*)
   403    "Ring_and_Field.field_mult_cancel_left",
   404    "Ring_and_Field.field_mult_cancel_right",
   405    "Ring_and_Field.inverse_le_iff_le_neg",
   406    "Ring_and_Field.inverse_le_iff_le",
   407    "Ring_and_Field.inverse_less_iff_less_neg",
   408    "Ring_and_Field.inverse_less_iff_less",
   409    "Ring_and_Field.le_divide_eq_1_neg", (*obscure and prolific*)
   410    "Ring_and_Field.le_divide_eq_1_pos", (*obscure and prolific*)
   411    "Ring_and_Field.less_divide_eq_1_neg", (*obscure and prolific*)
   412    "Ring_and_Field.less_divide_eq_1_pos", (*obscure and prolific*)
   413    "Ring_and_Field.one_eq_divide_iff",  (*duplicate by symmetry*)
   414    "Set.ball_simps", "Set.bex_simps",   (*quantifier rewriting: useless*)
   415    "Set.Collect_bex_eq",   (*involves an existential quantifier*)
   416    "Set.Collect_ex_eq",   (*involves an existential quantifier*)
   417    "Set.Diff_eq_empty_iff", (*redundant with paramodulation*)
   418    "Set.Diff_insert0",
   419    "Set.disjoint_insert",
   420    "Set.empty_Union_conv",   (*redundant with paramodulation*)
   421    "Set.full_SetCompr_eq",   (*involves an existential quantifier*)
   422    "Set.image_Collect",      (*involves an existential quantifier*)
   423    "Set.image_def",          (*involves an existential quantifier*)
   424    "Set.insert_disjoint",
   425    "Set.Int_UNIV",  (*redundant with paramodulation*)
   426    "Set.Inter_iff", (*We already have InterI, InterE*)
   427    "Set.Inter_UNIV_conv",
   428    "Set.psubsetE",    (*too prolific and obscure*)
   429    "Set.psubsetI",
   430    "Set.singleton_insert_inj_eq'",
   431    "Set.singleton_insert_inj_eq",
   432    "Set.singletonD",  (*these two duplicate some "insert" lemmas*)
   433    "Set.singletonI",
   434    "Set.Un_empty", (*redundant with paramodulation*)
   435    "Set.UNION_def",   (*involves an existential quantifier*)
   436    "Set.Union_empty_conv", (*redundant with paramodulation*)
   437    "Set.Union_iff",              (*We already have UnionI, UnionE*)
   438    "SetInterval.atLeastAtMost_iff", (*obscure and prolific*)
   439    "SetInterval.atLeastLessThan_iff", (*obscure and prolific*)
   440    "SetInterval.greaterThanAtMost_iff", (*obscure and prolific*)
   441    "SetInterval.greaterThanLessThan_iff", (*obscure and prolific*)
   442    "SetInterval.ivl_subset"];  (*excessive case analysis*)
   443 
   444 
   445 (*These might be prolific but are probably OK, and min and max are basic.
   446    "Orderings.max_less_iff_conj", 
   447    "Orderings.min_less_iff_conj",
   448    "Orderings.min_max.below_inf.below_inf_conv",
   449    "Orderings.min_max.below_sup.above_sup_conv",
   450 Very prolific and somewhat obscure:
   451    "Set.InterD",
   452    "Set.UnionI",
   453 *)
   454 
   455 (*** retrieve lemmas from clasimpset and atpset, may filter them ***)
   456 
   457 (*Hashing to detect duplicate and variant clauses, e.g. from the [iff] attribute*)
   458 
   459 exception HASH_CLAUSE and HASH_STRING;
   460 
   461 (*Catches (for deletion) theorems automatically generated from other theorems*)
   462 fun insert_suffixed_names ht x = 
   463      (Polyhash.insert ht (x^"_iff1", ()); 
   464       Polyhash.insert ht (x^"_iff2", ()); 
   465       Polyhash.insert ht (x^"_dest", ())); 
   466 
   467 (*Are all characters in this string digits?*)
   468 fun all_numeric s = null (String.tokens Char.isDigit s);
   469 
   470 (*Delete a suffix of the form _\d+*)
   471 fun delete_numeric_suffix s =
   472   case rev (String.fields (fn c => c = #"_") s) of
   473       last::rest => 
   474           if all_numeric last 
   475           then [s, space_implode "_" (rev rest)]
   476           else [s]
   477     | [] => [s];
   478 
   479 fun banned_thmlist s =
   480   (Sign.base_name s) mem_string ["induct","inducts","split","splits","split_asm"];
   481 
   482 (*Reject theorems with names like "List.filter.filter_list_def" or
   483   "Accessible_Part.acc.defs", as these are definitions arising from packages.
   484   FIXME: this will also block definitions within locales*)
   485 fun is_package_def a =
   486    length (NameSpace.unpack a) > 2 andalso 
   487    String.isSuffix "_def" a  orelse  String.isSuffix "_defs" a;
   488 
   489 fun make_banned_test xs = 
   490   let val ht = Polyhash.mkTable (Polyhash.hash_string, op =)
   491                                 (6000, HASH_STRING)
   492       fun banned_aux s = 
   493             isSome (Polyhash.peek ht s) orelse banned_thmlist s orelse is_package_def s
   494       fun banned s = exists banned_aux (delete_numeric_suffix s)
   495   in  app (fn x => Polyhash.insert ht (x,())) (!blacklist);
   496       app (insert_suffixed_names ht) (!blacklist @ xs); 
   497       banned
   498   end;
   499 
   500 (** a hash function from Term.term to int, and also a hash table **)
   501 val xor_words = List.foldl Word.xorb 0w0;
   502 
   503 fun hashw_term ((Const(c,_)), w) = Polyhash.hashw_string (c,w)
   504   | hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   505   | hashw_term ((Var(_,_)), w) = w
   506   | hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   507   | hashw_term ((Abs(_,_,t)), w) = hashw_term (t, w)
   508   | hashw_term ((P$Q), w) = hashw_term (Q, (hashw_term (P, w)));
   509 
   510 fun hashw_pred (P,w) = 
   511     let val (p,args) = strip_comb P
   512     in
   513 	List.foldl hashw_term w (p::args)
   514     end;
   515 
   516 fun hash_literal (Const("Not",_)$P) = Word.notb(hashw_pred(P,0w0))
   517   | hash_literal P = hashw_pred(P,0w0);
   518 
   519 
   520 fun get_literals (Const("Trueprop",_)$P) lits = get_literals P lits
   521   | get_literals (Const("op |",_)$P$Q) lits = get_literals Q (get_literals P lits)
   522   | get_literals lit lits = (lit::lits);
   523 
   524 
   525 fun hash_term t = Word.toIntX (xor_words (map hash_literal (get_literals t [])));
   526 
   527 (*Versions ONLY for "faking" a theorem name. Here we take variable names into account
   528   so that similar theorems don't collide.  FIXME: this entire business of "faking" 
   529   theorem names must end!*)
   530 fun hashw_typ (TVar ((a,i), _), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
   531   | hashw_typ (TFree (a,_), w) = Polyhash.hashw_string (a,w)
   532   | hashw_typ (Type (a, Ts), w) = Polyhash.hashw_string (a, List.foldl hashw_typ w Ts);
   533 
   534 fun full_hashw_term ((Const(c,T)), w) = Polyhash.hashw_string (c, hashw_typ(T,w))
   535   | full_hashw_term ((Free(a,_)), w) = Polyhash.hashw_string (a,w)
   536   | full_hashw_term ((Var((a,i),_)), w) = Polyhash.hashw_string (a, Polyhash.hashw_int(i,w))
   537   | full_hashw_term ((Bound i), w) = Polyhash.hashw_int(i,w)
   538   | full_hashw_term ((Abs(_,T,t)), w) = full_hashw_term (t, hashw_typ(T,w))
   539   | full_hashw_term ((P$Q), w) = full_hashw_term (Q, (full_hashw_term (P, w)));
   540 
   541 fun full_hashw_thm (th,w) = 
   542   let val {prop,hyps,...} = rep_thm th
   543   in List.foldl full_hashw_term w (prop::hyps) end
   544 
   545 fun full_hash_thm th = full_hashw_thm (th,0w0);
   546 
   547 fun equal_thm (thm1,thm2) = Term.aconv(prop_of thm1, prop_of thm2);
   548 
   549 (*Create a hash table for clauses, of the given size*)
   550 fun mk_clause_table n =
   551       Polyhash.mkTable (hash_term o prop_of, equal_thm)
   552                        (n, HASH_CLAUSE);
   553 
   554 (*Use a hash table to eliminate duplicates from xs. Argument is a list of
   555   (thm * (string * int)) tuples. The theorems are hashed into the table. *)
   556 fun make_unique xs = 
   557   let val ht = mk_clause_table 7000
   558   in
   559       app (ignore o Polyhash.peekInsert ht) xs;  
   560       Polyhash.listItems ht
   561   end;
   562 
   563 (*Remove existing axiom clauses from the conjecture clauses, as this can dramatically
   564   boost an ATP's performance (for some reason)*)
   565 fun subtract_cls c_clauses ax_clauses = 
   566   let val ht = mk_clause_table 2200
   567       fun known x = isSome (Polyhash.peek ht x)
   568   in
   569       app (ignore o Polyhash.peekInsert ht) ax_clauses;  
   570       filter (not o known) c_clauses 
   571   end;
   572 
   573 (*Filter axiom clauses, but keep supplied clauses and clauses in whitelist. 
   574   Duplicates are removed later.*)
   575 fun get_relevant_clauses thy cls_thms white_cls goals =
   576   white_cls @ (ReduceAxiomsN.relevance_filter thy cls_thms goals);
   577 
   578 (*This name is cryptic but short. Unlike gensym, we get the same name each time.*)
   579 fun fake_thm_name th = 
   580     Context.theory_name (theory_of_thm th) ^ "." ^ Word.toString (full_hash_thm th);
   581 
   582 fun put_name_pair ("",th) = (fake_thm_name th, th)
   583   | put_name_pair (a,th)  = (a,th);
   584 
   585 fun display_thms [] = ()
   586   | display_thms ((name,thm)::nthms) = 
   587       let val nthm = name ^ ": " ^ (string_of_thm thm)
   588       in Output.debug nthm; display_thms nthms  end;
   589  
   590 fun all_facts_of ctxt =
   591   FactIndex.find (ProofContext.fact_index_of ctxt) ([], [])
   592   |> maps #2 |> map (`Thm.name_of_thm);
   593 
   594 (* get lemmas from claset, simpset, atpset and extra supplied rules *)
   595 fun get_clasimp_atp_lemmas ctxt user_thms = 
   596   let val included_thms =
   597 	if !include_all 
   598 	then (tap (fn ths => Output.debug
   599 	             ("Including all " ^ Int.toString (length ths) ^ " theorems")) 
   600 	          (all_facts_of ctxt @ PureThy.all_thms_of (ProofContext.theory_of ctxt)))
   601 	else 
   602 	let val claset_thms =
   603 		if !include_claset then ResAxioms.claset_rules_of_ctxt ctxt
   604 		else []
   605 	    val simpset_thms = 
   606 		if !include_simpset then ResAxioms.simpset_rules_of_ctxt ctxt
   607 		else []
   608 	    val atpset_thms =
   609 		if !include_atpset then ResAxioms.atpset_rules_of_ctxt ctxt
   610 		else []
   611 	    val _ = if !Output.show_debug_msgs 
   612 		    then (Output.debug "ATP theorems: "; display_thms atpset_thms) 
   613 		    else ()		 
   614 	in  claset_thms @ simpset_thms @ atpset_thms  end
   615       val user_rules = map (put_name_pair o ResAxioms.pairname)
   616 			   (if null user_thms then !whitelist else user_thms)
   617   in
   618       (map put_name_pair included_thms, user_rules)
   619   end;
   620 
   621 (*Remove lemmas that are banned from the backlist. Also remove duplicates. *)
   622 fun blacklist_filter thms = 
   623   if !run_blacklist_filter then 
   624       let val banned = make_banned_test (map #1 thms)
   625 	  fun ok (a,_) = not (banned a)
   626       in  filter ok thms  end
   627   else thms;
   628 
   629 
   630 (***************************************************************)
   631 (* ATP invocation methods setup                                *)
   632 (***************************************************************)
   633 
   634 fun cnf_hyps_thms ctxt = 
   635     let val ths = Assumption.prems_of ctxt
   636     in fold (fold (insert Thm.eq_thm) o ResAxioms.skolem_thm) ths [] end;
   637 
   638 (*Translation mode can be auto-detected, or forced to be first-order or higher-order*)
   639 datatype mode = Auto | Fol | Hol;
   640 
   641 val linkup_logic_mode = ref Auto;
   642 
   643 (*Ensures that no higher-order theorems "leak out"*)
   644 fun restrict_to_logic logic cls =
   645   if is_fol_logic logic then filter (Meson.is_fol_term o prop_of o fst) cls 
   646 	                else cls;
   647 
   648 fun tptp_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   649     if is_fol_logic logic 
   650     then ResClause.tptp_write_file goals filename (axioms, classrels, arities)
   651     else ResHolClause.tptp_write_file goals filename (axioms, classrels, arities) user_lemmas;
   652 
   653 fun dfg_writer logic goals filename (axioms,classrels,arities) user_lemmas =
   654     if is_fol_logic logic 
   655     then ResClause.dfg_write_file goals filename (axioms, classrels, arities)
   656     else ResHolClause.dfg_write_file goals filename (axioms, classrels, arities) user_lemmas;
   657 
   658 (*Called by the oracle-based methods declared in res_atp_methods.ML*)
   659 fun write_subgoal_file dfg mode ctxt conjectures user_thms n =
   660     let val conj_cls = make_clauses conjectures 
   661                          |> ResAxioms.assume_abstract_list |> Meson.finish_cnf
   662 	val hyp_cls = cnf_hyps_thms ctxt
   663 	val goal_cls = conj_cls@hyp_cls
   664 	val logic = case mode of 
   665                             Auto => problem_logic_goals [map prop_of goal_cls]
   666 			  | Fol => FOL
   667 			  | Hol => HOL
   668 	val (included_thms,user_rules) = get_clasimp_atp_lemmas ctxt user_thms
   669 	val cla_simp_atp_clauses = included_thms |> blacklist_filter
   670 	                             |> ResAxioms.cnf_rules_pairs |> make_unique 
   671                                      |> restrict_to_logic logic 
   672 	val user_cls = ResAxioms.cnf_rules_pairs user_rules
   673 	val thy = ProofContext.theory_of ctxt
   674 	val axclauses = get_relevant_clauses thy cla_simp_atp_clauses
   675 	                            user_cls (map prop_of goal_cls) |> make_unique
   676 	val keep_types = if is_fol_logic logic then !fol_keep_types else is_typed_hol ()
   677 	val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy else []
   678 	val arity_clauses = if keep_types then ResClause.arity_clause_thy thy else []
   679         val writer = if dfg then dfg_writer else tptp_writer 
   680 	and file = atp_input_file()
   681 	and user_lemmas_names = map #1 user_rules
   682     in
   683 	writer logic goal_cls file (axclauses,classrel_clauses,arity_clauses) user_lemmas_names;
   684 	Output.debug ("Writing to " ^ file);
   685 	file
   686     end;
   687 
   688 
   689 (**** remove tmp files ****)
   690 fun cond_rm_tmp file = 
   691     if !Output.show_debug_msgs orelse !destdir <> "" then Output.debug "ATP input kept..." 
   692     else OS.FileSys.remove file;
   693 
   694 
   695 (****** setup ATPs as Isabelle methods ******)
   696 fun atp_meth' tac ths ctxt = 
   697     Method.SIMPLE_METHOD' HEADGOAL
   698     (tac ctxt ths);
   699 
   700 fun atp_meth tac ths ctxt = 
   701     let val thy = ProofContext.theory_of ctxt
   702 	val _ = ResClause.init thy
   703 	val _ = ResHolClause.init thy
   704     in
   705 	atp_meth' tac ths ctxt
   706     end;
   707 
   708 fun atp_method tac = Method.thms_ctxt_args (atp_meth tac);
   709 
   710 (***************************************************************)
   711 (* automatic ATP invocation                                    *)
   712 (***************************************************************)
   713 
   714 (* call prover with settings and problem file for the current subgoal *)
   715 fun watcher_call_provers sign sg_terms (childin, childout, pid) =
   716   let
   717     fun make_atp_list [] n = []
   718       | make_atp_list (sg_term::xs) n =
   719           let
   720             val probfile = prob_pathname n
   721             val time = Int.toString (!time_limit)
   722           in
   723             Output.debug ("problem file in watcher_call_provers is " ^ probfile);
   724             (*options are separated by Watcher.setting_sep, currently #"%"*)
   725             if !prover = "spass"
   726             then
   727               let val spass = helper_path "SPASS_HOME" "SPASS"
   728                   val sopts =
   729    "-Auto%-SOS=1%-PGiven=0%-PProblem=0%-Splits=0%-FullRed=0%-DocProof%-TimeLimit=" ^ time
   730               in 
   731                   ("spass", spass, sopts, probfile) :: make_atp_list xs (n+1)
   732               end
   733             else if !prover = "vampire"
   734 	    then 
   735               let val vampire = helper_path "VAMPIRE_HOME" "vampire"
   736                   val casc = if !time_limit > 70 then "--mode casc%" else ""
   737                   val vopts = casc ^ "-m 100000%-t " ^ time
   738               in
   739                   ("vampire", vampire, vopts, probfile) :: make_atp_list xs (n+1)
   740               end
   741       	     else if !prover = "E"
   742       	     then
   743 	       let val Eprover = helper_path "E_HOME" "eproof"
   744 	       in
   745 		  ("E", Eprover, 
   746 		     "--tptp-in%-l5%-xAuto%-tAuto%--silent%--cpu-limit=" ^ time, probfile) ::
   747 		   make_atp_list xs (n+1)
   748 	       end
   749 	     else error ("Invalid prover name: " ^ !prover)
   750           end
   751 
   752     val atp_list = make_atp_list sg_terms 1
   753   in
   754     Watcher.callResProvers(childout,atp_list);
   755     Output.debug "Sent commands to watcher!"
   756   end
   757   
   758 fun trace_array fname =
   759   let val path = File.tmp_path (Path.basic fname)
   760   in  Array.app (File.append path o (fn s => s ^ "\n"))  end;
   761 
   762 (*Converting a subgoal into negated conjecture clauses*)
   763 fun neg_clauses th n =
   764   let val tacs = [rtac ccontr, ObjectLogic.atomize_tac, skolemize_tac]
   765       val st = Seq.hd (EVERY' tacs n th)
   766       val negs = Option.valOf (metahyps_thms n st)
   767   in make_clauses negs |> ResAxioms.assume_abstract_list |> Meson.finish_cnf end;
   768 		                       
   769 (*We write out problem files for each subgoal. Argument probfile generates filenames,
   770   and allows the suppression of the suffix "_1" in problem-generation mode.
   771   FIXME: does not cope with &&, and it isn't easy because one could have multiple
   772   subgoals, each involving &&.*)
   773 fun write_problem_files probfile (ctxt,th)  =
   774   let val goals = Thm.prems_of th
   775       val _ = Output.debug ("number of subgoals = " ^ Int.toString (length goals))
   776       val thy = ProofContext.theory_of ctxt
   777       fun get_neg_subgoals [] _ = []
   778         | get_neg_subgoals (gl::gls) n = neg_clauses th n :: get_neg_subgoals gls (n+1)
   779       val goal_cls = get_neg_subgoals goals 1
   780       val logic = case !linkup_logic_mode of
   781 		Auto => problem_logic_goals (map ((map prop_of)) goal_cls)
   782 	      | Fol => FOL
   783 	      | Hol => HOL
   784       val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt []
   785       val included_cls = included_thms |> blacklist_filter
   786                                        |> ResAxioms.cnf_rules_pairs |> make_unique 
   787                                        |> restrict_to_logic logic 
   788       val white_cls = ResAxioms.cnf_rules_pairs white_thms
   789       (*clauses relevant to goal gl*)
   790       val axcls_list = map (fn gl => get_relevant_clauses thy included_cls white_cls [gl])
   791                            goals
   792       val _ = Output.debug ("clauses = " ^ Int.toString(length included_cls))
   793       val keep_types = if is_fol_logic logic then !ResClause.keep_types 
   794                        else is_typed_hol ()
   795       val classrel_clauses = if keep_types then ResClause.classrel_clauses_thy thy
   796                              else []
   797       val _ = Output.debug ("classrel clauses = " ^ 
   798                             Int.toString (length classrel_clauses))
   799       val arity_clauses = if keep_types then ResClause.arity_clause_thy thy 
   800                           else []
   801       val _ = Output.debug ("arity clauses = " ^ Int.toString (length arity_clauses))
   802       val writer = if !prover = "spass" then dfg_writer else tptp_writer 
   803       fun write_all [] [] _ = []
   804 	| write_all (ccls::ccls_list) (axcls::axcls_list) k =
   805             let val fname = probfile k
   806                 val axcls = make_unique axcls
   807                 val ccls = subtract_cls ccls axcls
   808                 val clnames = writer logic ccls fname (axcls,classrel_clauses,arity_clauses) []
   809                 val thm_names = Array.fromList clnames
   810                 val _ = if !Output.show_debug_msgs 
   811                         then trace_array (fname ^ "_thm_names") thm_names else ()
   812             in  (thm_names,fname) :: write_all ccls_list axcls_list (k+1)  end
   813       val (thm_names_list, filenames) = ListPair.unzip (write_all goal_cls axcls_list 1)
   814   in
   815       (filenames, thm_names_list)
   816   end;
   817 
   818 val last_watcher_pid = ref (NONE : (TextIO.instream * TextIO.outstream * 
   819                                     Posix.Process.pid * string list) option);
   820 
   821 fun kill_last_watcher () =
   822     (case !last_watcher_pid of 
   823          NONE => ()
   824        | SOME (_, _, pid, files) => 
   825 	  (Output.debug ("Killing old watcher, pid = " ^ string_of_pid pid);
   826 	   Watcher.killWatcher pid;  
   827 	   ignore (map (try cond_rm_tmp) files)))
   828      handle OS.SysErr _ => Output.debug "Attempt to kill watcher failed";
   829 
   830 (*writes out the current clasimpset to a tptp file;
   831   turns off xsymbol at start of function, restoring it at end    *)
   832 val isar_atp = setmp print_mode [] 
   833  (fn (ctxt, th) =>
   834   if Thm.no_prems th then ()
   835   else
   836     let
   837       val _ = kill_last_watcher()
   838       val (files,thm_names_list) = write_problem_files prob_pathname (ctxt,th)
   839       val (childin, childout, pid) = Watcher.createWatcher (th, thm_names_list)
   840     in
   841       last_watcher_pid := SOME (childin, childout, pid, files);
   842       Output.debug ("problem files: " ^ space_implode ", " files); 
   843       Output.debug ("pid: " ^ string_of_pid pid);
   844       watcher_call_provers (sign_of_thm th) (Thm.prems_of th) (childin, childout, pid)
   845     end);
   846 
   847 val isar_atp_writeonly = setmp print_mode [] 
   848       (fn (ctxt,th) =>
   849        if Thm.no_prems th then ()
   850        else 
   851          let val probfile = if Thm.nprems_of th = 1 then probfile_nosuffix 
   852           	            else prob_pathname
   853          in ignore (write_problem_files probfile (ctxt,th)) end);
   854 
   855 
   856 (** the Isar toplevel hook **)
   857 
   858 fun invoke_atp_ml (ctxt, goal) =
   859   let val thy = ProofContext.theory_of ctxt;
   860   in
   861     Output.debug ("subgoals in isar_atp:\n" ^ 
   862 		  Pretty.string_of (ProofContext.pretty_term ctxt
   863 		    (Logic.mk_conjunction_list (Thm.prems_of goal))));
   864     Output.debug ("current theory: " ^ Context.theory_name thy);
   865     inc hook_count;
   866     Output.debug ("in hook for time: " ^ Int.toString (!hook_count));
   867     ResClause.init thy;
   868     ResHolClause.init thy;
   869     if !destdir = "" andalso !time_limit > 0 then isar_atp (ctxt, goal)
   870     else isar_atp_writeonly (ctxt, goal)
   871   end;
   872 
   873 val invoke_atp = Toplevel.no_timing o Toplevel.unknown_proof o Toplevel.keep
   874  (fn state =>
   875   let val (ctxt, (_, goal)) = Proof.get_goal (Toplevel.proof_of state)
   876   in  invoke_atp_ml (ctxt, goal)  end);
   877 
   878 val call_atpP =
   879   OuterSyntax.command 
   880     "ProofGeneral.call_atp" 
   881     "call automatic theorem provers" 
   882     OuterKeyword.diag
   883     (Scan.succeed invoke_atp);
   884 
   885 val _ = OuterSyntax.add_parsers [call_atpP];
   886 
   887 end;