Merged theory ResAtpOracle.thy into ResAtpMethods.thy
authormengj
Fri Oct 21 02:57:22 2005 +0200 (2005-10-21)
changeset 179393925ab7b8a18
parent 17938 6c20fae2416c
child 17940 3706c254d296
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
etc/settings
src/HOL/IsaMakefile
src/HOL/ResAtpMethods.thy
src/HOL/ResAtpOracle.thy
src/HOL/Tools/res_atp_setup.ML
     1.1 --- a/etc/settings	Wed Oct 19 21:53:34 2005 +0200
     1.2 +++ b/etc/settings	Fri Oct 21 02:57:22 2005 +0200
     1.3 @@ -87,6 +87,10 @@
     1.4  # The place for user configuration, heap files, etc.
     1.5  ISABELLE_HOME_USER=~/isabelle
     1.6  
     1.7 +# The places for external proversetc.
     1.8 +#VAMPIRE_HOME=~/Vampire
     1.9 +#E_HOME=~/E
    1.10 +
    1.11  # Where to look for isabelle tools (multiple dirs separated by ':').
    1.12  ISABELLE_TOOLS="$ISABELLE_HOME/lib/Tools"
    1.13  
     2.1 --- a/src/HOL/IsaMakefile	Wed Oct 19 21:53:34 2005 +0200
     2.2 +++ b/src/HOL/IsaMakefile	Fri Oct 21 02:57:22 2005 +0200
     2.3 @@ -113,8 +113,7 @@
     2.4    Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy		\
     2.5    Typedef.thy Wellfounded_Recursion.thy Wellfounded_Relations.thy		\
     2.6    antisym_setup.ML arith_data.ML blastdata.ML cladata.ML			\
     2.7 -  document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML	\
     2.8 -  ResAtpOracle.thy                                                             \
     2.9 +  document/root.tex eqrule_HOL_data.ML hologic.ML simpdata.ML			\
    2.10    ResAtpMethods.thy \
    2.11    Tools/res_atp_setup.ML Tools/res_atp_provers.ML Tools/res_atp_methods.ML 	
    2.12  	@$(ISATOOL) usedir $(HOL_USEDIR_OPTIONS) -b -g true $(OUT)/Pure HOL
     3.1 --- a/src/HOL/ResAtpMethods.thy	Wed Oct 19 21:53:34 2005 +0200
     3.2 +++ b/src/HOL/ResAtpMethods.thy	Fri Oct 21 02:57:22 2005 +0200
     3.3 @@ -5,12 +5,22 @@
     3.4  *)
     3.5  
     3.6  theory ResAtpMethods
     3.7 -  imports Reconstruction ResAtpOracle
     3.8 +  imports Reconstruction 
     3.9  
    3.10 -  uses "Tools/res_atp_setup.ML"
    3.11 -       "Tools/res_atp_methods.ML"
    3.12 +uses ("Tools/res_atp_setup.ML")
    3.13 +     ("Tools/res_atp_provers.ML")
    3.14 +     ("Tools/res_atp_methods.ML")
    3.15  
    3.16  begin
    3.17 -setup ResAtpMethods.ResAtps_setup
    3.18 +
    3.19 +ML{*use "Tools/res_atp_setup.ML"*}
    3.20 +ML{*use "Tools/res_atp_provers.ML"*}
    3.21  
    3.22 +oracle vampire_oracle ("string list * int") =  {*ResAtpProvers.vampire_o*}
    3.23 +oracle eprover_oracle ("string list * int") =  {*ResAtpProvers.eprover_o*}
    3.24 +
    3.25 +
    3.26 +ML{*use "Tools/res_atp_methods.ML"*}
    3.27 +
    3.28 +setup ResAtpMethods.ResAtps_setup
    3.29  end
     4.1 --- a/src/HOL/ResAtpOracle.thy	Wed Oct 19 21:53:34 2005 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,28 +0,0 @@
     4.4 -(* ID: $Id$
     4.5 -   Author: Jia Meng, NICTA
     4.6 -
     4.7 -setup vampire prover as an oracle
     4.8 -setup E prover as an oracle
     4.9 -*)
    4.10 -
    4.11 -theory ResAtpOracle 
    4.12 -  imports HOL   
    4.13 -uses "Tools/res_atp_setup.ML" 
    4.14 -     "Tools/res_atp_provers.ML"
    4.15 -
    4.16 -begin 
    4.17 -
    4.18 -
    4.19 -
    4.20 -
    4.21 -oracle vampire_oracle ("string list * int") = {*ResAtpProvers.vampire_o
    4.22 -*}
    4.23 -
    4.24 -
    4.25 -
    4.26 -
    4.27 -oracle eprover_oracle ("string list * int") = {*ResAtpProvers.eprover_o
    4.28 -  *}
    4.29 -
    4.30 -
    4.31 -end
     5.1 --- a/src/HOL/Tools/res_atp_setup.ML	Wed Oct 19 21:53:34 2005 +0200
     5.2 +++ b/src/HOL/Tools/res_atp_setup.ML	Fri Oct 21 02:57:22 2005 +0200
     5.3 @@ -15,16 +15,6 @@
     5.4    | writeln_strs out (s::ss) = (TextIO.output (out, s); TextIO.output (out, "\n"); writeln_strs out ss);
     5.5  
     5.6  
     5.7 -fun no_rep_add x []     = [x]
     5.8 -  | no_rep_add x (y::z) = if x=y then y::z else y::(no_rep_add x z);
     5.9 -
    5.10 -fun no_rep_app l1 []     = l1
    5.11 -  | no_rep_app l1 (x::y) = no_rep_app (no_rep_add x l1) y;
    5.12 -
    5.13 -
    5.14 -fun flat_noDup []     = []
    5.15 -  | flat_noDup (x::y) = no_rep_app x (flat_noDup y);
    5.16 -
    5.17  fun warning_thm thm nm = warning (nm ^ " " ^ (string_of_thm thm));
    5.18  
    5.19  fun warning_thms_n n thms nm =
    5.20 @@ -114,7 +104,7 @@
    5.21  fun tptp_form thms n tfrees =
    5.22      let val clss = ResClause.make_conjecture_clauses (map prop_of thms)
    5.23  	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss)
    5.24 -	val tfree_clss = map ResClause.tfree_clause ((flat_noDup tfree_litss) \\ tfrees)
    5.25 +	val tfree_clss = map ResClause.tfree_clause ((ResClause.union_all tfree_litss) \\ tfrees)
    5.26  	val probfile = File.platform_path prob_file ^ "_" ^ string_of_int n
    5.27  	val out = TextIO.openOut(probfile)		 	
    5.28      in
    5.29 @@ -134,7 +124,7 @@
    5.30          val prems''' = ResAxioms.rm_Eps [] prems''
    5.31          val clss = ResClause.make_conjecture_clauses prems'''
    5.32  	val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
    5.33 -	val tfree_lits = flat_noDup tfree_litss
    5.34 +	val tfree_lits = ResClause.union_all tfree_litss
    5.35  	val tfree_clss = map ResClause.tfree_clause tfree_lits 
    5.36          val hypsfile = File.platform_path hyps_file
    5.37          val out = TextIO.openOut(hypsfile)
    5.38 @@ -163,7 +153,7 @@
    5.39  fun write_rules [] file = [](* no rules, then no need to write anything, thus no clasimp file *)
    5.40    | write_rules rules file =
    5.41      let val out = TextIO.openOut(file)
    5.42 -	val clss = flat_noDup(ResAxioms.clausify_rules_pairs rules)
    5.43 +	val clss = ResClause.union_all(ResAxioms.clausify_rules_pairs rules)
    5.44  	val (clss',names) = ListPair.unzip clss
    5.45  	val (tptpclss,_) = ListPair.unzip(map ResClause.clause2tptp clss')
    5.46      in
    5.47 @@ -202,12 +192,14 @@
    5.48  (* setup ATPs as Isabelle methods                               *)
    5.49  (***************************************************************)
    5.50  fun atp_meth' tac prems ctxt = 
    5.51 -    let val rules = if !filter_ax then (find_relevant_ax ctxt) else (tptp_cnf_clasimp ctxt (!include_claset, !include_simpset)) 
    5.52 +    let val rules = if !filter_ax then find_relevant_ax ctxt 
    5.53 +		    else tptp_cnf_clasimp ctxt (!include_claset, !include_simpset) 
    5.54  	val (hyps,tfrees) = tptp_hyps (ProofContext.prems_of ctxt)
    5.55  	val files = hyps @ rules
    5.56      in
    5.57  	Method.METHOD (fn facts =>
    5.58 -			  if !debug then ((warning_thms_n (length facts) facts "facts");HEADGOAL (tac ctxt files tfrees)) else (HEADGOAL (tac ctxt files tfrees)))
    5.59 +			  if !debug then (warning_thms_n (length facts) facts "facts";HEADGOAL (tac ctxt files tfrees)) 
    5.60 +			  else HEADGOAL (tac ctxt files tfrees))
    5.61      end;
    5.62  
    5.63  
    5.64 @@ -228,7 +220,9 @@
    5.65    | rm_tmp_files1 (f::fs) =
    5.66      (OS.FileSys.remove f; rm_tmp_files1 fs);
    5.67  
    5.68 -fun cond_rm_tmp files = (if (!keep_atp_input) then (warning "ATP input kept...") else (warning "deleting ATP inputs..."; rm_tmp_files1 files));
    5.69 +fun cond_rm_tmp files = 
    5.70 +    if !keep_atp_input then warning "ATP input kept..." 
    5.71 +    else (warning "deleting ATP inputs..."; rm_tmp_files1 files);
    5.72  
    5.73  
    5.74  end