--- a/src/HOL/Tools/res_atp.ML Fri Mar 11 00:45:07 2005 +0100
+++ b/src/HOL/Tools/res_atp.ML Fri Mar 11 16:08:21 2005 +0100
@@ -1,6 +1,7 @@
-(* Author: Jia Meng, Cambridge University Computer Laboratory
- ID: $Id$
- Copyright 2004 University of Cambridge
+(* Title: HOL/Tools/res_atp.ML
+ ID: $Id$
+ Author: Jia Meng, Cambridge University Computer Laboratory
+ Copyright 2004 University of Cambridge
ATPs with TPTP format input.
*)
@@ -10,217 +11,207 @@
signature RES_ATP =
sig
-val trace_res : bool ref
-val axiom_file : Path.T
-val hyps_file : Path.T
-val isar_atp : ProofContext.context * Thm.thm -> unit
-val prob_file : Path.T
-val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
-val atp_tac : int -> Tactical.tactic
-val debug: bool ref
+ val trace_res : bool ref
+ val axiom_file : Path.T
+ val hyps_file : Path.T
+ val isar_atp : ProofContext.context * Thm.thm -> unit
+ val prob_file : Path.T
+ val atp_ax_tac : Thm.thm list -> int -> Tactical.tactic
+ val atp_tac : int -> Tactical.tactic
+ val debug : bool ref
end;
structure ResAtp : RES_ATP =
-
struct
-(* used for debug *)
-val debug = ref false;
+ (* used for debug *)
+ val debug = ref false;
-fun debug_tac tac = (warning "testing";tac);
-(* default value is false *)
+ fun debug_tac tac =
+ (warning "testing"; tac);
+ (* default value is false *)
-val trace_res = ref false;
+ val trace_res = ref false;
-val skolem_tac = skolemize_tac;
-
+ val skolem_tac = skolemize_tac;
-val atomize_tac =
- SUBGOAL
- (fn (prop,_) =>
- let val ts = Logic.strip_assums_hyp prop
- in EVERY1
- [METAHYPS
- (fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)),
- REPEAT_DETERM_N (length ts) o (etac thin_rl)]
- end);
+ val atomize_tac =
+ SUBGOAL (fn (prop, _) =>
+ let
+ val ts = Logic.strip_assums_hyp prop
+ in
+ EVERY1
+ [METAHYPS (fn hyps => cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1),
+ REPEAT_DETERM_N (length ts) o (etac thin_rl)]
+ end);
-(* temporarily use these files, which will be loaded by Vampire *)
-val prob_file = File.tmp_path (Path.basic "prob");
-val axiom_file = File.tmp_path (Path.basic "axioms");
-val hyps_file = File.tmp_path (Path.basic "hyps");
-val dummy_tac = PRIMITIVE(fn thm => thm );
-
-
+ (* temporarily use these files, which will be loaded by Vampire *)
+ val prob_file = File.tmp_path (Path.basic "prob");
+ val axiom_file = File.tmp_path (Path.basic "axioms");
+ val hyps_file = File.tmp_path (Path.basic "hyps");
+ val dummy_tac = PRIMITIVE (fn thm => thm );
-fun tptp_inputs thms n =
- let val clss = map (ResClause.make_conjecture_clause_thm) thms
- val tptp_clss = ResLib.flat_noDup(map ResClause.tptp_clause clss)
- val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
- val out = TextIO.openOut(probfile)
- in
- (ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; (if !trace_res then (warning probfile) else ()))
- end;
+ fun tptp_inputs thms n =
+ let
+ val clss = map (ResClause.make_conjecture_clause_thm) thms
+ val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
+ val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)
+ val out = TextIO.openOut probfile
+ in
+ ResLib.writeln_strs out tptp_clss;
+ TextIO.closeOut out;
+ if !trace_res then warning probfile else ()
+ end;
(**** for Isabelle/ML interface ****)
-fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
-
-
-
+ fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);
-fun atp_tac n = SELECT_GOAL
- (EVERY1 [rtac ccontr,atomize_tac, skolemize_tac,
- METAHYPS(fn negs => (call_atp_tac (make_clauses negs) n))]) n;
-
+ fun atp_tac n =
+ SELECT_GOAL (EVERY1
+ [rtac ccontr,atomize_tac, skolemize_tac,
+ METAHYPS (fn negs => call_atp_tac (make_clauses negs) n)]
+ ) n;
-fun atp_ax_tac axioms n =
- let val axcls = ResLib.flat_noDup(map ResAxioms.clausify_axiom axioms)
- val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup(map ResClause.tptp_clause axcls))
- val axiomfile = File.sysify_path axiom_file
- val out = TextIO.openOut (axiomfile)
- in
- (TextIO.output(out,axcls_str);TextIO.closeOut out; if !trace_res then (warning axiomfile) else (); atp_tac n)
- end;
+ fun atp_ax_tac axioms n =
+ let
+ val axcls = ResLib.flat_noDup (map ResAxioms.clausify_axiom axioms)
+ val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup (map ResClause.tptp_clause axcls))
+ val axiomfile = File.sysify_path axiom_file
+ val out = TextIO.openOut axiomfile
+ in
+ TextIO.output (out, axcls_str);
+ TextIO.closeOut out;
+ if !trace_res then warning axiomfile else ();
+ atp_tac n
+ end;
-
-fun atp thm =
- let val prems = prems_of thm
- in
- case prems of [] => ()
- | _ => (atp_tac 1 thm; ())
- end;
+ fun atp thm =
+ let
+ val prems = prems_of thm
+ in
+ case prems of [] => ()
+ | _ => (atp_tac 1 thm; ())
+ end;
(**** For running in Isar ****)
-(* same function as that in res_axioms.ML *)
-fun repeat_RS thm1 thm2 =
- let val thm1' = thm1 RS thm2 handle THM _ => thm1
- in
- if eq_thm(thm1,thm1') then thm1' else (repeat_RS thm1' thm2)
- end;
-
-(* a special version of repeat_RS *)
-fun repeat_someI_ex thm = repeat_RS thm someI_ex;
-
+ (* same function as that in res_axioms.ML *)
+ fun repeat_RS thm1 thm2 =
+ let
+ val thm1' = thm1 RS thm2 handle THM _ => thm1
+ in
+ if eq_thm (thm1, thm1') then thm1' else (repeat_RS thm1' thm2)
+ end;
-(* convert clauses from "assume" to conjecture. write to file "hyps" *)
-fun isar_atp_h thms =
- let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
- val prems' = map repeat_someI_ex prems
- val prems'' = make_clauses prems'
- val prems''' = ResAxioms.rm_Eps [] prems''
- val clss = map ResClause.make_conjecture_clause prems'''
- val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
- val hypsfile = File.sysify_path hyps_file
- val out = TextIO.openOut(hypsfile)
- in
- (ResLib.writeln_strs out tptp_clss; TextIO.closeOut out; if !trace_res then (warning hypsfile) else ())
- end;
-
-
+ (* a special version of repeat_RS *)
+ fun repeat_someI_ex thm =
+ repeat_RS thm someI_ex;
-
-val isar_atp_g = atp_tac;
-
+ (* convert clauses from "assume" to conjecture. write to file "hyps" *)
+ fun isar_atp_h thms =
+ let
+ val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms
+ val prems' = map repeat_someI_ex prems
+ val prems'' = make_clauses prems'
+ val prems''' = ResAxioms.rm_Eps [] prems''
+ val clss = map ResClause.make_conjecture_clause prems'''
+ val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)
+ val hypsfile = File.sysify_path hyps_file
+ val out = TextIO.openOut hypsfile
+ in
+ ResLib.writeln_strs out tptp_clss;
+ TextIO.closeOut out;
+ if !trace_res then warning hypsfile else ()
+ end;
-fun isar_atp_goal' thm k n =
- if (k > n) then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
-
-
-fun isar_atp_goal thm n_subgoals = (if (!debug) then warning (string_of_thm thm) else (isar_atp_goal' thm 1 n_subgoals));
-
-
+ val isar_atp_g = atp_tac;
-fun isar_atp_aux thms thm n_subgoals =
- (isar_atp_h thms; isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
+ fun isar_atp_goal' thm k n =
+ if k > n then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);
+ fun isar_atp_goal thm n_subgoals =
+ if !debug then warning (string_of_thm thm) else isar_atp_goal' thm 1 n_subgoals;
+
+ fun isar_atp_aux thms thm n_subgoals =
+ (isar_atp_h thms;
+ isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)
-fun isar_atp' (thms, thm) =
- let val prems = prems_of thm
- in
- case prems of [] => (if (!debug) then warning "entering forward, no goal" else ())
- | _ => (isar_atp_aux thms thm (length prems))
- end;
+ fun isar_atp' (thms, thm) =
+ let
+ val prems = prems_of thm
+ in
+ case prems of [] => if !debug then warning "entering forward, no goal" else ()
+ | _ => isar_atp_aux thms thm (length prems)
+ end;
-
-
-
-local
+ local
-fun get_thms_cs claset =
- let val clsset = rep_cs claset
- val safeEs = #safeEs clsset
- val safeIs = #safeIs clsset
- val hazEs = #hazEs clsset
- val hazIs = #hazIs clsset
- in
- safeEs @ safeIs @ hazEs @ hazIs
- end;
-
-
-
-fun append_name name [] _ = []
- | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1));
+ fun get_thms_cs claset =
+ let
+ val clsset = rep_cs claset
+ val safeEs = #safeEs clsset
+ val safeIs = #safeIs clsset
+ val hazEs = #hazEs clsset
+ val hazIs = #hazIs clsset
+ in
+ safeEs @ safeIs @ hazEs @ hazIs
+ end;
-fun append_names (name::names) (thms::thmss) =
- let val thms' = append_name name thms 0
- in
- thms'::(append_names names thmss)
- end;
-
+ fun append_name name [] _ = []
+ | append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)), thm)) :: (append_name name thms (k+1));
-fun get_thms_ss [] = []
- | get_thms_ss thms =
- let val names = map Thm.name_of_thm thms
- val thms' = map (mksimps mksimps_pairs) thms
- val thms'' = append_names names thms'
- in
- ResLib.flat_noDup thms''
- end;
-
-
-
+ fun append_names (name::names) (thms::thmss) =
+ let
+ val thms' = append_name name thms 0
+ in
+ thms'::(append_names names thmss)
+ end;
-in
-
+ fun get_thms_ss [] =
+ []
+ | get_thms_ss thms =
+ let
+ val names = map Thm.name_of_thm thms
+ val thms' = map (mksimps mksimps_pairs) thms
+ val thms'' = append_names names thms'
+ in
+ ResLib.flat_noDup thms''
+ end;
-(* convert locally declared rules to axiom clauses *)
-(* write axiom clauses to ax_file *)
-fun isar_local_thms (delta_cs, delta_ss_thms) =
- let val thms_cs = get_thms_cs delta_cs
- val thms_ss = get_thms_ss delta_ss_thms
- val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
- val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
- val ax_file = File.sysify_path axiom_file
- val out = TextIO.openOut ax_file
- in
- (ResLib.writeln_strs out clauses_strs; TextIO.closeOut out)
- end;
-
+ in
-
-
+ (* convert locally declared rules to axiom clauses *)
+ (* write axiom clauses to ax_file *)
+ fun isar_local_thms (delta_cs, delta_ss_thms) =
+ let
+ val thms_cs = get_thms_cs delta_cs
+ val thms_ss = get_thms_ss delta_ss_thms
+ val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))
+ val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)
+ val ax_file = File.sysify_path axiom_file
+ val out = TextIO.openOut ax_file
+ in
+ ResLib.writeln_strs out clauses_strs;
+ TextIO.closeOut out
+ end;
-(* called in Isar automatically *)
-fun isar_atp (ctxt,thm) =
- let val prems = ProofContext.prems_of ctxt
- val d_cs = Classical.get_delta_claset ctxt
- val d_ss_thms = Simplifier.get_delta_simpset ctxt
- in
- (isar_local_thms (d_cs,d_ss_thms); isar_atp' (prems, thm))
- end;
+ (* called in Isar automatically *)
+ fun isar_atp (ctxt, thm) =
+ let
+ val prems = ProofContext.prems_of ctxt
+ val d_cs = Classical.get_delta_claset ctxt
+ val d_ss_thms = Simplifier.get_delta_simpset ctxt
+ in
+ isar_local_thms (d_cs, d_ss_thms);
+ isar_atp' (prems, thm)
+ end;
-end
-
-
-
+ end (* local *)
end;
Proof.atp_hook := ResAtp.isar_atp;
-
-