15603

1 
(* Title: HOL/Tools/res_atp.ML


2 
ID: $Id$


3 
Author: Jia Meng, Cambridge University Computer Laboratory


4 
Copyright 2004 University of Cambridge

15347

5 


6 
ATPs with TPTP format input.


7 
*)

15452

8 


9 
(*Jia: changed: isar_atp now processes entire proof context. fetch thms from delta simpset/claset*)


10 

15347

11 
signature RES_ATP =


12 
sig


13 

15603

14 
val trace_res : bool ref


15 
val axiom_file : Path.T


16 
val hyps_file : Path.T


17 
val isar_atp : ProofContext.context * Thm.thm > unit


18 
val prob_file : Path.T


19 
val atp_ax_tac : Thm.thm list > int > Tactical.tactic


20 
val atp_tac : int > Tactical.tactic


21 
val debug : bool ref

15347

22 


23 
end;


24 


25 
structure ResAtp : RES_ATP =


26 
struct


27 

15603

28 
(* used for debug *)


29 
val debug = ref false;

15452

30 

15603

31 
fun debug_tac tac =


32 
(warning "testing"; tac);


33 
(* default value is false *)

15347

34 

15603

35 
val trace_res = ref false;

15347

36 

15603

37 
val skolem_tac = skolemize_tac;

15347

38 

15603

39 
val atomize_tac =


40 
SUBGOAL (fn (prop, _) =>


41 
let


42 
val ts = Logic.strip_assums_hyp prop


43 
in


44 
EVERY1


45 
[METAHYPS (fn hyps => cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1),


46 
REPEAT_DETERM_N (length ts) o (etac thin_rl)]


47 
end);

15347

48 

15603

49 
(* temporarily use these files, which will be loaded by Vampire *)


50 
val prob_file = File.tmp_path (Path.basic "prob");


51 
val axiom_file = File.tmp_path (Path.basic "axioms");


52 
val hyps_file = File.tmp_path (Path.basic "hyps");


53 
val dummy_tac = PRIMITIVE (fn thm => thm );

15347

54 

15603

55 
fun tptp_inputs thms n =


56 
let


57 
val clss = map (ResClause.make_conjecture_clause_thm) thms


58 
val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)


59 
val probfile = (File.sysify_path prob_file) ^ "_" ^ (string_of_int n)


60 
val out = TextIO.openOut probfile


61 
in


62 
ResLib.writeln_strs out tptp_clss;


63 
TextIO.closeOut out;


64 
if !trace_res then warning probfile else ()


65 
end;

15347

66 


67 


68 
(**** for Isabelle/ML interface ****)


69 

15603

70 
fun call_atp_tac thms n = (tptp_inputs thms n; dummy_tac);

15452

71 

15603

72 
fun atp_tac n =


73 
SELECT_GOAL (EVERY1


74 
[rtac ccontr,atomize_tac, skolemize_tac,


75 
METAHYPS (fn negs => call_atp_tac (make_clauses negs) n)]


76 
) n;

15347

77 

15603

78 
fun atp_ax_tac axioms n =


79 
let


80 
val axcls = ResLib.flat_noDup (map ResAxioms.clausify_axiom axioms)


81 
val axcls_str = ResClause.tptp_clauses2str (ResLib.flat_noDup (map ResClause.tptp_clause axcls))


82 
val axiomfile = File.sysify_path axiom_file


83 
val out = TextIO.openOut axiomfile


84 
in


85 
TextIO.output (out, axcls_str);


86 
TextIO.closeOut out;


87 
if !trace_res then warning axiomfile else ();


88 
atp_tac n


89 
end;

15347

90 

15603

91 
fun atp thm =


92 
let


93 
val prems = prems_of thm


94 
in


95 
case prems of [] => ()


96 
 _ => (atp_tac 1 thm; ())


97 
end;

15347

98 


99 


100 
(**** For running in Isar ****)


101 

15603

102 
(* same function as that in res_axioms.ML *)


103 
fun repeat_RS thm1 thm2 =


104 
let


105 
val thm1' = thm1 RS thm2 handle THM _ => thm1


106 
in


107 
if eq_thm (thm1, thm1') then thm1' else (repeat_RS thm1' thm2)


108 
end;

15347

109 

15603

110 
(* a special version of repeat_RS *)


111 
fun repeat_someI_ex thm =


112 
repeat_RS thm someI_ex;

15347

113 

15603

114 
(* convert clauses from "assume" to conjecture. write to file "hyps" *)


115 
fun isar_atp_h thms =


116 
let


117 
val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms


118 
val prems' = map repeat_someI_ex prems


119 
val prems'' = make_clauses prems'


120 
val prems''' = ResAxioms.rm_Eps [] prems''


121 
val clss = map ResClause.make_conjecture_clause prems'''


122 
val tptp_clss = ResLib.flat_noDup (map ResClause.tptp_clause clss)


123 
val hypsfile = File.sysify_path hyps_file


124 
val out = TextIO.openOut hypsfile


125 
in


126 
ResLib.writeln_strs out tptp_clss;


127 
TextIO.closeOut out;


128 
if !trace_res then warning hypsfile else ()


129 
end;

15452

130 

15603

131 
val isar_atp_g = atp_tac;

15452

132 

15603

133 
fun isar_atp_goal' thm k n =


134 
if k > n then () else (isar_atp_g k thm; isar_atp_goal' thm (k+1) n);

15452

135 

15603

136 
fun isar_atp_goal thm n_subgoals =


137 
if !debug then warning (string_of_thm thm) else isar_atp_goal' thm 1 n_subgoals;


138 


139 
fun isar_atp_aux thms thm n_subgoals =


140 
(isar_atp_h thms;


141 
isar_atp_goal thm n_subgoals); (* convert both to conjecture clauses, but write to different files *)

15452

142 

15603

143 
fun isar_atp' (thms, thm) =


144 
let


145 
val prems = prems_of thm


146 
in


147 
case prems of [] => if !debug then warning "entering forward, no goal" else ()


148 
 _ => isar_atp_aux thms thm (length prems)


149 
end;

15452

150 

15603

151 
local

15452

152 

15603

153 
fun get_thms_cs claset =


154 
let


155 
val clsset = rep_cs claset


156 
val safeEs = #safeEs clsset


157 
val safeIs = #safeIs clsset


158 
val hazEs = #hazEs clsset


159 
val hazIs = #hazIs clsset


160 
in


161 
safeEs @ safeIs @ hazEs @ hazIs


162 
end;

15452

163 

15603

164 
fun append_name name [] _ = []


165 
 append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)), thm)) :: (append_name name thms (k+1));

15452

166 

15603

167 
fun append_names (name::names) (thms::thmss) =


168 
let


169 
val thms' = append_name name thms 0


170 
in


171 
thms'::(append_names names thmss)


172 
end;

15452

173 

15603

174 
fun get_thms_ss [] =


175 
[]


176 
 get_thms_ss thms =


177 
let


178 
val names = map Thm.name_of_thm thms


179 
val thms' = map (mksimps mksimps_pairs) thms


180 
val thms'' = append_names names thms'


181 
in


182 
ResLib.flat_noDup thms''


183 
end;

15452

184 

15603

185 
in

15347

186 

15603

187 
(* convert locally declared rules to axiom clauses *)


188 
(* write axiom clauses to ax_file *)


189 
fun isar_local_thms (delta_cs, delta_ss_thms) =


190 
let


191 
val thms_cs = get_thms_cs delta_cs


192 
val thms_ss = get_thms_ss delta_ss_thms


193 
val thms_clauses = ResLib.flat_noDup (map ResAxioms.clausify_axiom (thms_cs @ thms_ss))


194 
val clauses_strs = ResLib.flat_noDup (map ResClause.tptp_clause thms_clauses) (*string list*)


195 
val ax_file = File.sysify_path axiom_file


196 
val out = TextIO.openOut ax_file


197 
in


198 
ResLib.writeln_strs out clauses_strs;


199 
TextIO.closeOut out


200 
end;

15347

201 

15603

202 
(* called in Isar automatically *)


203 
fun isar_atp (ctxt, thm) =


204 
let


205 
val prems = ProofContext.prems_of ctxt


206 
val d_cs = Classical.get_delta_claset ctxt


207 
val d_ss_thms = Simplifier.get_delta_simpset ctxt


208 
in


209 
isar_local_thms (d_cs, d_ss_thms);


210 
isar_atp' (prems, thm)


211 
end;

15347

212 

15603

213 
end (* local *)

15452

214 

15347

215 
end;


216 


217 
Proof.atp_hook := ResAtp.isar_atp;
