author  quigley 
Fri, 10 Jun 2005 16:15:36 +0200  
changeset 16357  f1275d2a1dee 
parent 16259  aed1a8ae4b23 
child 16475  8f3ba52a7937 
permissions  rwrr 
15608  1 
(* Author: Jia Meng, Cambridge University Computer Laboratory 
2 
ID: $Id$ 

3 
Copyright 2004 University of Cambridge 

15347  4 

5 
ATPs with TPTP format input. 

6 
*) 

15452  7 

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

15644  9 
(*Claire: changed: added actual watcher calls *) 
15452  10 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

11 

15347  12 
signature RES_ATP = 
13 
sig 

15608  14 
val trace_res : bool ref 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

15 
val subgoals: Thm.thm list 
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

16 
val traceflag : bool ref 
15608  17 
val axiom_file : Path.T 
18 
val hyps_file : Path.T 

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

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

20 
val prob_file : Path.T; 
15644  21 
(*val atp_ax_tac : Thm.thm list > int > Tactical.tactic*) 
22 
(*val atp_tac : int > Tactical.tactic*) 

15608  23 
val debug: bool ref 
16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16089
diff
changeset

24 
val full_spass: bool ref 
15347  25 
end; 
26 

27 
structure ResAtp : RES_ATP = 

15608  28 

15347  29 
struct 
30 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

31 
val subgoals = []; 
15644  32 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

33 
val traceflag = ref true; 
16357  34 
(* used for debug *) 
35 
val debug = ref false; 

16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

36 

15608  37 
fun debug_tac tac = (warning "testing";tac); 
16357  38 
(* default value is false *) 
39 
val full_spass = ref false; 

15608  40 
val trace_res = ref false; 
15347  41 

15608  42 
val skolem_tac = skolemize_tac; 
43 

15644  44 
val num_of_clauses = ref 0; 
45 
val clause_arr = Array.array(3500, ("empty", 0)); 

46 

15347  47 

15608  48 
val atomize_tac = 
49 
SUBGOAL 

50 
(fn (prop,_) => 

51 
let val ts = Logic.strip_assums_hyp prop 

52 
in EVERY1 

53 
[METAHYPS 

54 
(fn hyps => (cut_facts_tac (map (ObjectLogic.atomize_thm o forall_intr_vars) hyps) 1)), 

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

56 
end); 

15347  57 

15608  58 
(* temporarily use these files, which will be loaded by Vampire *) 
15644  59 
val file_id_num =ref 0; 
15608  60 

15644  61 
fun new_prob_file () = (file_id_num := (!file_id_num) + 1;"prob"^(string_of_int (!file_id_num))); 
15608  62 

15347  63 

15644  64 
val axiom_file = File.tmp_path (Path.basic "axioms"); 
65 
val clasimp_file = File.tmp_path (Path.basic "clasimp"); 

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

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

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

69 

70 

15347  71 
(**** for Isabelle/ML interface ****) 
72 

16357  73 
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126) andalso (not ((ord ch ) = 63))) orelse (ch = " ") 
15608  74 

16357  75 
fun proofstring x = let val exp = explode x 
76 
in 

77 
List.filter (is_proof_char ) exp 

78 
end 

79 

15608  80 

15452  81 

15644  82 
(* 
83 
fun call_atp_tac thms n = (tptp_inputs thms ; dummy_tac); 

15347  84 

15644  85 
*) 
15347  86 

87 
(**** For running in Isar ****) 

88 

15608  89 
(* same function as that in res_axioms.ML *) 
90 
fun repeat_RS thm1 thm2 = 

91 
let val thm1' = thm1 RS thm2 handle THM _ => thm1 

92 
in 

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

94 
end; 

95 

96 
(* a special version of repeat_RS *) 

97 
fun repeat_someI_ex thm = repeat_RS thm someI_ex; 

98 

15644  99 
(*********************************************************************) 
15608  100 
(* convert clauses from "assume" to conjecture. write to file "hyps" *) 
15644  101 
(* hypotheses of the goal currently being proved *) 
102 
(*********************************************************************) 

103 

15608  104 
fun isar_atp_h thms = 
15644  105 

15608  106 
let val prems = map (skolemize o make_nnf o ObjectLogic.atomize_thm) thms 
15644  107 
val prems' = map repeat_someI_ex prems 
108 
val prems'' = make_clauses prems' 

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

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

15774  111 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15608  112 
val tfree_lits = ResLib.flat_noDup tfree_litss 
113 
val tfree_clss = map ResClause.tfree_clause tfree_lits 

16259  114 
val hypsfile = File.platform_path hyps_file 
15608  115 
val out = TextIO.openOut(hypsfile) 
116 
in 

117 
((ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; if !trace_res then (warning hypsfile) else ());tfree_lits) 

118 
end; 

15347  119 

15644  120 

121 
(*********************************************************************) 

122 
(* write out a subgoal as tptp clauses to the file "probN" *) 

123 
(* where N is the number of this subgoal *) 

124 
(*********************************************************************) 

125 

15608  126 
fun tptp_inputs_tfrees thms n tfrees = 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

127 
let val _ = (warning ("in tptp_inputs_tfrees 0")) 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

128 
val clss = map (ResClause.make_conjecture_clause_thm) thms 
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

129 
val _ = (warning ("in tptp_inputs_tfrees 1")) 
15774  130 
val (tptp_clss,tfree_litss) = ListPair.unzip (map ResClause.clause2tptp clss) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

131 
val _ = (warning ("in tptp_inputs_tfrees 2")) 
15608  132 
val tfree_clss = map ResClause.tfree_clause ((ResLib.flat_noDup tfree_litss) \\ tfrees) 
15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

133 
val _ = (warning ("in tptp_inputs_tfrees 3")) 
16259  134 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
15608  135 
val out = TextIO.openOut(probfile) 
136 
in 

16357  137 
(ResLib.writeln_strs out (tfree_clss @ tptp_clss); TextIO.closeOut out; (if !trace_res then (warning probfile) else ())) 
15608  138 
end; 
15452  139 

15608  140 

16357  141 

15644  142 
(*********************************************************************) 
143 
(* call SPASS with settings and problem file for the current subgoal *) 

144 
(* should be modified to allow other provers to be called *) 

145 
(*********************************************************************) 

16357  146 
(* now passing in list of skolemized thms and list of sgterms to go with them *) 
147 
fun call_resolve_tac (thms: Thm.thm list list) sign (sg_terms: Term.term list) (childin, childout,pid) n = let 

148 
val axfile = (File.platform_path axiom_file) 

149 
val hypsfile = (File.platform_path hyps_file) 

150 
val clasimpfile = (File.platform_path clasimp_file) 

151 
val spass_home = getenv "SPASS_HOME" 

152 

153 
fun make_atp_list [] sign n = [] 

154 
 make_atp_list ((sko_thm, sg_term)::xs) sign n = 

155 
let 

156 
val skothmstr = Meson.concat_with_and (map string_of_thm sko_thm) 

157 
val thmproofstr = proofstring ( skothmstr) 

158 
val no_returns =List.filter not_newline ( thmproofstr) 

159 
val thmstr = implode no_returns 

160 
val _ = warning ("thmstring in make_atp_lists is: "^thmstr) 

15608  161 

16357  162 
val sgstr = Sign.string_of_term sign sg_term 
163 
val goalproofstring = proofstring sgstr 

16089
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

164 
val no_returns =List.filter not_newline ( goalproofstring) 
9169bdf930f8
trying to set up portable calling sequences for SPASS and tptp2X
paulson
parents:
16061
diff
changeset

165 
val goalstring = implode no_returns 
16357  166 
val _ = warning ("goalstring in make_atp_lists is: "^goalstring) 
167 

16259  168 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int n) 
16357  169 
val _ = (warning ("prob file in cal_res_tac is: "^probfile)) 
170 
in 

171 
if !full_spass 

172 
then 

173 
([("spass", thmstr, goalstring (*,spass_home*), 

174 
getenv "ISABELLE_HOME" ^ "/src/HOL/Tools/ATP/spassshell"(*( getenv "SPASS_HOME")^"/SPASS"*), 

175 
"DocProof%TimeLimit=60", 

176 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 

177 
else 

178 
([("spass", thmstr, goalstring (*,spass_home*), 

179 
getenv "ISABELLE_HOME" ^"/src/HOL/Tools/ATP/spassshell"(* (getenv "SPASS_HOME")^"/SPASS"*), 

180 
"Auto=0%ISRe%ISFc%RTaut%RFSub%RBSub%DocProof%TimeLimit=60", 

181 
clasimpfile, axfile, hypsfile, probfile)]@(make_atp_list xs sign (n+1))) 

182 
end 

15452  183 

16357  184 
val thms_goals = ListPair.zip( thms, sg_terms) 
185 
val atp_list = make_atp_list thms_goals sign 1 

186 
in 

187 
Watcher.callResProvers(childout,atp_list); 

188 
warning("Sent commands to watcher!"); 

189 
dummy_tac 

190 
end 

191 
(* 

192 
val axfile = (File.platform_path axiom_file) 

193 
val hypsfile = (File.platform_path hyps_file) 

194 
val clasimpfile = (File.platform_path clasimp_file) 

195 
val spass_home = getenv "SPASS_HOME" 

196 
val probfile = (File.platform_path prob_file) ^ "_" ^ (string_of_int 1) 

197 

198 
val (clause_arr, num_of_clauses) = ResClasimp.write_out_clasimp_small (File.platform_path clasimp_file) ; 

199 
val (childin,childout,pid) = Watcher.createWatcher(mp, clause_arr, num_of_clauses); 

200 
Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", spass_home, "DocProof", clasimpfile, axfile, hypsfile,probfile)]); 

201 

202 
Watcher.callResProvers(childout, [("spass", "thmstring", "goalstr", "/homes/clq20/spassshell", "", clasimpfile, axfile, hypsfile,probfile)]); 

203 

204 

205 
*) 

15644  206 
(**********************************************************) 
207 
(* write out the current subgoal as a tptp file, probN, *) 

208 
(* then call dummy_tac  should be call_res_tac *) 

209 
(**********************************************************) 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

210 

15657
bd946fbc7c2b
Current version of res_atp.ML  causes an error when I run it. C.Q.
quigley
parents:
15653
diff
changeset

211 

16357  212 
fun get_sko_thms tfrees sign sg_terms (childin, childout,pid) thm n sko_thms = 
213 
if (equal n 0) then 

214 
(call_resolve_tac (rev sko_thms) sign sg_terms (childin, childout, pid) (List.length sg_terms);dummy_tac thm) 

215 
else 

216 

217 
( SELECT_GOAL 

218 
(EVERY1 [rtac ccontr,atomize_tac, skolemize_tac, 

219 
METAHYPS(fn negs => (tptp_inputs_tfrees (make_clauses negs) n tfrees; 

220 
get_sko_thms tfrees sign sg_terms (childin, childout, pid) thm (n 1) (negs::sko_thms);dummy_tac))]) n thm ) 

15644  221 

222 

223 

224 
(**********************************************) 

225 
(* recursively call atp_tac_g on all subgoals *) 

226 
(* sg_term is the nth subgoal as a term  used*) 

227 
(* in proof reconstruction *) 

228 
(**********************************************) 

229 

16357  230 
fun isar_atp_goal' thm n tfree_lits (childin, childout, pid) = 
231 

232 
(let val prems = prems_of thm 

233 
(*val sg_term = get_nth k prems*) 

234 
val sign = sign_of_thm thm 

235 
val thmstring = string_of_thm thm 

236 
in 

237 

238 
(warning("in isar_atp_goal'")); 

239 
(warning("thmstring in isar_atp_goal': "^thmstring)); 

240 
(* go and call callResProvers with this subgoal *) 

241 
(* isar_atp_g tfree_lits sg_term (childin, childout, pid) k thm; *) 

242 
(* recursive call to pick up the remaining subgoals *) 

243 
(* isar_atp_goal' thm (k+1) n tfree_lits (childin, childout, pid) *) 

244 
get_sko_thms tfree_lits sign prems (childin, childout, pid) thm n [] 

245 
end); 

15644  246 

16357  247 
(*fun isar_atp_goal thm n_subgoals tfree_lits (childin, childout, pid) = 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

248 
(if (!debug) then warning (string_of_thm thm) 
16357  249 
else (isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) ));*) 
15644  250 

251 
(**************************************************) 

252 
(* convert clauses from "assume" to conjecture. *) 

253 
(* i.e. apply make_clauses and then get tptp for *) 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

254 
(* any hypotheses in the goal produced by assume *) 
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

255 
(* statements; *) 
15644  256 
(* write to file "hyps" *) 
257 
(**************************************************) 

258 

259 

260 
fun isar_atp_aux thms thm n_subgoals (childin, childout, pid) = 

15608  261 
let val tfree_lits = isar_atp_h thms 
16357  262 
in 
263 
(warning("in isar_atp_aux")); 

264 
isar_atp_goal' thm n_subgoals tfree_lits (childin, childout, pid) 

15608  265 
end; 
15644  266 

267 
(******************************************************************) 

268 
(* called in Isar automatically *) 

269 
(* writes out the current clasimpset to a tptp file *) 

270 
(* passes all subgoals on to isar_atp_aux for further processing *) 

271 
(* turns off xsymbol at start of function, restoring it at end *) 

272 
(******************************************************************) 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

273 
(*FIX changed to clasimp_file *) 
16357  274 
fun isar_atp' (ctxt,thms, thm) = 
275 
let 

276 
val _= (print_mode := (Library.gen_rems (op =) (! print_mode, ["xsymbols", "symbols"]))) 

15644  277 
val _= (warning ("in isar_atp'")) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

278 
val prems = prems_of thm 
15697  279 
val sign = sign_of_thm thm 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

280 
val thms_string = Meson.concat_with_and (map string_of_thm thms) 
15644  281 
val thmstring = string_of_thm thm 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

282 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

283 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

284 
(* set up variables for writing out the clasimps to a tptp file *) 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

285 
val (clause_arr, num_of_clauses) = 
16357  286 
ResClasimp.write_out_clasimp(*_small*) (File.platform_path clasimp_file) 
16172
629ba53a072f
small tweaks; also now write_out_clasimp takes the current theory as argument
paulson
parents:
16156
diff
changeset

287 
(ProofContext.theory_of ctxt) 
16357  288 
val _ = (warning ("clasimp_file is this: "^(File.platform_path clasimp_file)) ) 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

289 

15644  290 
(* cq: add write out clasimps to file *) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

291 
(* cq:create watcher and pass to isar_atp_aux *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

292 
(* tracing *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

293 
(*val tenth_ax = fst( Array.sub(clause_arr, 1)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

294 
val tenth_ax_thms = Recon_Transfer.memo_find_clause (tenth_ax, clause_tab) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

295 
val clause_str = Meson.concat_with_and (map string_of_thm tenth_ax_thms) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

296 
val _ = (warning ("tenth axiom in array is: "^tenth_ax)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

297 
val _ = (warning ("tenth axiom in table is: "^clause_str)) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

298 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

299 
val _ = (warning ("num_of_clauses is: "^(string_of_int (num_of_clauses))) ) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

300 
*) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

301 

b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15782
diff
changeset

302 
val (childin,childout,pid) = Watcher.createWatcher(thm,clause_arr, num_of_clauses) 
15644  303 
val pidstring = string_of_int(Word.toInt (Word.fromLargeWord ( Posix.Process.pidToWord pid ))) 
15608  304 
in 
15644  305 
case prems of [] => () 
306 
 _ => ((warning ("initial thms: "^thms_string)); 

307 
(warning ("initial thm: "^thmstring)); 

308 
(warning ("subgoals: "^prems_string)); 

309 
(warning ("pid: "^ pidstring))); 

310 
isar_atp_aux thms thm (length prems) (childin, childout, pid) ; 

16357  311 
(warning("turning xsymbol back on!")); 
15644  312 
print_mode := (["xsymbols", "symbols"] @ ! print_mode) 
15608  313 
end; 
314 

15452  315 

15608  316 

317 

318 
local 

319 

320 
fun get_thms_cs claset = 

321 
let val clsset = rep_cs claset 

322 
val safeEs = #safeEs clsset 

323 
val safeIs = #safeIs clsset 

324 
val hazEs = #hazEs clsset 

325 
val hazIs = #hazIs clsset 

326 
in 

327 
safeEs @ safeIs @ hazEs @ hazIs 

328 
end; 

329 

16357  330 

331 

15608  332 
fun append_name name [] _ = [] 
333 
 append_name name (thm::thms) k = (Thm.name_thm ((name ^ "_" ^ (string_of_int k)),thm)) :: (append_name name thms (k+1)); 

334 

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

336 
let val thms' = append_name name thms 0 

337 
in 

338 
thms'::(append_names names thmss) 

339 
end; 

340 

16357  341 

15608  342 
fun get_thms_ss [] = [] 
343 
 get_thms_ss thms = 

344 
let val names = map Thm.name_of_thm thms 

345 
val thms' = map (mksimps mksimps_pairs) thms 

346 
val thms'' = append_names names thms' 

347 
in 

348 
ResLib.flat_noDup thms'' 

349 
end; 

350 

16357  351 

352 

353 

15608  354 
in 
355 

15452  356 

15608  357 
(* convert locally declared rules to axiom clauses *) 
358 
(* write axiom clauses to ax_file *) 

15644  359 
(* what about clasimpset  it should already be in the ax file  perhaps append to ax file rather than just *) 
360 
(* write out ? Or keep as a separate file and then cat them all together in the watcher, like we do with the *) 

361 
(*claset file and prob file*) 

16357  362 
(* FIX*) 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

363 
(*fun isar_local_thms (delta_cs, delta_ss_thms) = 
15608  364 
let val thms_cs = get_thms_cs delta_cs 
365 
val thms_ss = get_thms_ss delta_ss_thms 

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

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

16259  368 
val ax_file = File.platform_path axiom_file 
15608  369 
val out = TextIO.openOut ax_file 
370 
in 

15644  371 
(ResLib.writeln_strs out clauses_strs; (warning ("axiom file is: "^ax_file));TextIO.closeOut out) 
15608  372 
end; 
16039
dfe264950511
Moved some of the clausify functions from ATP/res_clasimpset.ML to res_axioms.ML.
quigley
parents:
15919
diff
changeset

373 
*) 
15608  374 

375 

16357  376 

377 

15608  378 
(* called in Isar automatically *) 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

379 

15608  380 
fun isar_atp (ctxt,thm) = 
381 
let val prems = ProofContext.prems_of ctxt 

15644  382 
val d_cs = Classical.get_delta_claset ctxt 
383 
val d_ss_thms = Simplifier.get_delta_simpset ctxt 

384 
val thmstring = string_of_thm thm 

15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

385 
val sg_prems = prems_of thm 
15697  386 
val sign = sign_of_thm thm 
15679
28eb0fe50533
Integrating the reconstruction files into the building of HOL
quigley
parents:
15657
diff
changeset

387 
val prem_no = length sg_prems 
15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

388 
val prems_string = Meson.concat_with_and (map (Sign.string_of_term sign) sg_prems) 
15608  389 
in 
15644  390 
(warning ("initial thm in isar_atp: "^thmstring)); 
391 
(warning ("subgoals in isar_atp: "^prems_string)); 

15779
aed221aff642
Removed remaining references to Main.thy in reconstruction code.
quigley
parents:
15774
diff
changeset

392 
(warning ("number of subgoals in isar_atp: "^(string_of_int prem_no))); 
16357  393 
(*isar_local_thms (d_cs,d_ss_thms);*) 
394 
isar_atp' (ctxt,prems, thm) 

15608  395 
end; 
15347  396 

15608  397 
end 
398 

399 

16357  400 

401 

15347  402 
end; 
403 

404 
Proof.atp_hook := ResAtp.isar_atp; 