author  paulson 
Thu, 27 Oct 2005 18:25:33 +0200  
changeset 17997  6c0fe78624d9 
parent 17775  2679ba74411f 
child 18700  f04a8755d6ca 
permissions  rwrr 
15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

1 
(* ID: $Id$ 
16259  2 
Author: Claire Quigley 
3 
Copyright 2004 University of Cambridge 

15789
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

4 
*) 
4cb16144c81b
added hearder lines and deleted some redundant material
paulson
parents:
15787
diff
changeset

5 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

6 
structure Recon_Transfer = 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

7 
struct 
16803  8 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

9 
open Recon_Parse 
16803  10 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

11 
infixr 8 ++; infixr 7 >>; infixr 6 ; 
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

12 

17718  13 
val trace_path = Path.basic "transfer_trace"; 
14 

15 
fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 

16 
else (); 

17 

15642  18 

19 
(* Versions that include type information *) 

20 

16803  21 
(* FIXME rename to str_of_thm *) 
16157  22 
fun string_of_thm thm = 
16803  23 
setmp show_sorts true (Pretty.str_of o Display.pretty_thm) thm; 
15642  24 

25 

26 
(* check separate args in the watcher program for separating strings with a * or ; or something *) 

27 

28 
fun clause_strs_to_string [] str = str 

29 
 clause_strs_to_string (x::xs) str = clause_strs_to_string xs (str^x^"%") 

30 

31 
fun thmvars_to_string [] str = str 

32 
 thmvars_to_string (x::xs) str = thmvars_to_string xs (str^x^"%") 

33 

34 

35 
fun proofstep_to_string Axiom = "Axiom()" 

16091  36 
 proofstep_to_string (Binary ((a,b), (c,d)))= 
37 
"Binary(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

38 
 proofstep_to_string (Factor (a,b,c)) = 

39 
"Factor("^(string_of_int a)^","^(string_of_int b)^","^(string_of_int c)^")" 

40 
 proofstep_to_string (Para ((a,b), (c,d)))= 

41 
"Para(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

42 
 proofstep_to_string (MRR ((a,b), (c,d))) = 

43 
"MRR(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))" 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

44 
(* proofstep_to_string (Rewrite((a,b),(c,d))) = 
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

45 
"Rewrite(("^(string_of_int a)^","^(string_of_int b)^"),("^(string_of_int c)^","^(string_of_int d)^"))"*) 
15642  46 

47 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

48 
fun proof_to_string (num,(step,clause_strs, thmvars)) = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

49 
(string_of_int num)^(proofstep_to_string step)^ 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

50 
"["^(clause_strs_to_string clause_strs "")^"]["^(thmvars_to_string thmvars "")^"]" 
15642  51 

52 

53 
fun proofs_to_string [] str = str 

54 
 proofs_to_string (x::xs) str = let val newstr = proof_to_string x 

55 
in 

56 
proofs_to_string xs (str^newstr) 

57 
end 

58 

59 

60 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

61 
fun init_proofstep_to_string (num, step, clause_strs) = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

62 
(string_of_int num)^" "^(proofstep_to_string step)^" "^ 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

63 
(clause_strs_to_string clause_strs "")^" " 
15642  64 

65 
fun init_proofsteps_to_string [] str = str 

66 
 init_proofsteps_to_string (x::xs) str = let val newstr = init_proofstep_to_string x 

67 
in 

68 
init_proofsteps_to_string xs (str^newstr) 

69 
end 

70 

71 

72 

73 
(*** get a string representing the Isabelle ordered axioms ***) 

74 

16061  75 
fun origAx_to_string (num,(meta,thmvars)) = 
76 
let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta 

77 
in 

16091  78 
(string_of_int num)^"OrigAxiom()["^ 
79 
(clause_strs_to_string clause_strs "")^"]["^ 

16061  80 
(thmvars_to_string thmvars "")^"]" 
81 
end 

15642  82 

83 

84 
fun origAxs_to_string [] str = str 

85 
 origAxs_to_string (x::xs) str = let val newstr = origAx_to_string x 

86 
in 

87 
origAxs_to_string xs (str^newstr) 

88 
end 

89 

90 

91 
(*** get a string representing the Isabelle ordered axioms not used in the spass proof***) 

92 

16061  93 
fun extraAx_to_string (num, (meta,thmvars)) = 
94 
let val clause_strs = ReconOrderClauses.get_meta_lits_bracket meta 

95 
in 

16091  96 
(string_of_int num)^"ExtraAxiom()["^ 
16061  97 
(clause_strs_to_string clause_strs "")^"]"^ 
98 
"["^(thmvars_to_string thmvars "")^"]" 

99 
end; 

15642  100 

16061  101 
fun extraAxs_to_string [] str = str 
102 
 extraAxs_to_string (x::xs) str = 

103 
let val newstr = extraAx_to_string x 

104 
in 

105 
extraAxs_to_string xs (str^newstr) 

106 
end; 

15642  107 

17312  108 
fun is_axiom (_,Axiom,str) = true 
109 
 is_axiom (_,_,_) = false 

15642  110 

111 
fun get_step_nums [] nums = nums 

112 
 get_step_nums (( num:int,Axiom, str)::xs) nums = get_step_nums xs (nums@[num]) 

113 

15774  114 
exception Noassoc; 
115 

116 
fun assoc_snd a [] = raise Noassoc 

15642  117 
 assoc_snd a ((x, y)::t) = if a = y then x else assoc_snd a t; 
118 

119 
(* change to be something using check_order instead of a = y > returns true if ASSERTION not raised in checkorder, false otherwise *) 

120 

121 
(*fun get_assoc_snds [] xs assocs= assocs 

122 
 get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_snd x ys))]) 

123 
*) 

124 
(*FIX  should this have vars in it? *) 

16061  125 
fun there_out_of_order xs ys = (ReconOrderClauses.checkorder xs ys [] ([],[],[]); true) 
15774  126 
handle _ => false 
15642  127 

15774  128 
fun assoc_out_of_order a [] = raise Noassoc 
15642  129 
 assoc_out_of_order a ((b,c)::t) = if there_out_of_order a c then b else assoc_out_of_order a t; 
130 

131 
fun get_assoc_snds [] xs assocs= assocs 

132 
 get_assoc_snds (x::xs) ys assocs = get_assoc_snds xs ys (assocs@[((assoc_out_of_order x ys))]) 

133 

134 
fun add_if_not_inlist [] xs newlist = newlist 

16157  135 
 add_if_not_inlist (y::ys) xs newlist = if (not (y mem xs)) then 
15642  136 
add_if_not_inlist ys xs (y::newlist) 
137 
else add_if_not_inlist ys xs (newlist) 

138 

15700  139 
(*Flattens a list of list of strings to one string*) 
140 
fun onestr ls = String.concat (map String.concat ls); 

15642  141 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

142 
fun is_clasimp_ax clasimp_num n = n <= clasimp_num 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

143 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

144 
fun subone x = x  1 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

145 

2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

146 
fun numstr [] = "" 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

147 
 numstr (x::xs) = (string_of_int x)^"%"^(numstr xs) 
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

148 

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

149 

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

150 
(* retrieve the axioms that were obtained from the clasimpset *) 
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

151 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

152 
fun get_clasimp_cls (clause_arr: (ResClause.clause * thm) array) step_nums = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

153 
let val clasimp_nums = List.filter (is_clasimp_ax (Array.length clause_arr  1)) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

154 
(map subone step_nums) 
16157  155 
in 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

156 
map (fn x => Array.sub(clause_arr, x)) clasimp_nums 
16157  157 
end 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

158 

17775  159 
(* get names of clasimp axioms used*) 
17997  160 
fun get_axiom_names step_nums clause_arr = 
161 
distinct (sort_strings 

162 
(map (ResClause.get_axiomName o #1) 

163 
(get_clasimp_cls clause_arr step_nums))); 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

164 

17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
17484
diff
changeset

165 
fun get_axiom_names_spass proofstr clause_arr = 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

166 
let (* parse spass proof into datatype *) 
17718  167 
val _ = trace ("\nStarted parsing:\n" ^ proofstr) 
168 
val proof_steps = parse (#1(lex proofstr)) 

169 
val _ = trace "\nParsing finished!" 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

170 
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

171 
in 
17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
17484
diff
changeset

172 
get_axiom_names (get_step_nums (List.filter is_axiom proof_steps) []) clause_arr 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

173 
end; 
16357  174 

17569  175 
(*String contains multiple lines. 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

176 
A list consisting of the first number in each line is returned. *) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

177 
fun get_linenums proofstr = 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

178 
let val numerics = String.tokens (not o Char.isDigit) 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

179 
fun firstno [] = NONE 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

180 
 firstno (x::xs) = Int.fromString x 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

181 
val lines = String.tokens (fn c => c = #"\n") proofstr 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

182 
in List.mapPartial (firstno o numerics) lines end 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

183 

17569  184 
fun get_axiom_names_e proofstr clause_arr = 
17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
17484
diff
changeset

185 
get_axiom_names (get_linenums proofstr) clause_arr; 
17306  186 

17569  187 
(*String contains multiple lines. We want those of the form 
188 
"*********** [448, input] ***********". 

189 
A list consisting of the first number in each line is returned. *) 

190 
fun get_vamp_linenums proofstr = 

191 
let val toks = String.tokens (not o Char.isAlphaNum) 

192 
fun inputno [n,"input"] = Int.fromString n 

193 
 inputno _ = NONE 

194 
val lines = String.tokens (fn c => c = #"\n") proofstr 

195 
in List.mapPartial (inputno o toks) lines end 

196 

197 
fun get_axiom_names_vamp proofstr clause_arr = 

198 
get_axiom_names (get_vamp_linenums proofstr) clause_arr; 

199 

17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17122
diff
changeset

200 

16357  201 
(***********************************************) 
202 
(* get axioms for reconstruction *) 

203 
(***********************************************) 

16156
2f6fc19aba1e
Fixed array containing clasimpset rules. Added flags to turn on and off reconstruction and full spass
quigley
parents:
16091
diff
changeset

204 
fun numclstr (vars, []) str = str 
16157  205 
 numclstr ( vars, ((num, thm)::rest)) str = 
206 
let val newstr = str^(string_of_int num)^" "^(string_of_thm thm)^" " 

207 
in 

208 
numclstr (vars,rest) newstr 

209 
end 

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

210 

16157  211 
fun addvars c (a,b) = (a,b,c) 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

212 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

213 
fun get_axioms_used proof_steps thms clause_arr = 
17775  214 
let val axioms = (List.filter is_axiom) proof_steps 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

215 
val step_nums = get_step_nums axioms [] 
15919
b30a35432f5a
Replaced reference to SPASS with general one  set SPASS_HOME in settings file.
quigley
parents:
15817
diff
changeset

216 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

217 
val clauses = make_clauses thms (*FIXME: must this be repeated??*) 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

218 

5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

219 
val vars = map thm_vars clauses 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

220 

5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

221 
val distvars = distinct (fold append vars []) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

222 
val clause_terms = map prop_of clauses 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

223 
val clause_frees = List.concat (map term_frees clause_terms) 
15642  224 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

225 
val frees = map lit_string_with_nums clause_frees; 
15642  226 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

227 
val distfrees = distinct frees 
15642  228 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

229 
val metas = map Meson.make_meta_clause clauses 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

230 
val ax_strs = map #3 axioms 
15642  231 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

232 
(* literals of all axioms, not just those used by spass *) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

233 
val meta_strs = map ReconOrderClauses.get_meta_lits metas 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

234 

5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

235 
val metas_and_strs = ListPair.zip (metas,meta_strs) 
17718  236 
val _ = trace ("\nAxioms: " ^ onestr ax_strs) 
237 
val _ = trace ("\nMeta_strs: " ^ onestr meta_strs) 

15642  238 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

239 
(* get list of axioms as thms with their variables *) 
15642  240 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

241 
val ax_metas = get_assoc_snds ax_strs metas_and_strs [] 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

242 
val ax_vars = map thm_vars ax_metas 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

243 
val ax_with_vars = ListPair.zip (ax_metas,ax_vars) 
15642  244 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

245 
(* get list of extra axioms as thms with their variables *) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

246 
val extra_metas = add_if_not_inlist metas ax_metas [] 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

247 
val extra_vars = map thm_vars extra_metas 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

248 
val extra_with_vars = if (not (extra_metas = []) ) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

249 
then ListPair.zip (extra_metas,extra_vars) 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

250 
else [] 
17775  251 
in 
252 
(distfrees,distvars, extra_with_vars,ax_with_vars, ListPair.zip (step_nums,ax_metas)) 

253 
end; 

16905  254 

15642  255 

256 
(*********************************************************************) 

257 
(* Pass in spass string of proof and string version of isabelle goal *) 

258 
(* Get out reconstruction steps as a string to be sent to Isabelle *) 

259 
(*********************************************************************) 

260 

17122  261 
fun rules_to_string [] = "NONE" 
17775  262 
 rules_to_string xs = space_implode " " xs 
16357  263 

16478  264 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

265 
(*The signal handler in watcher.ML must be able to read the output of this.*) 
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

266 
fun prover_lemma_list_aux getax proofstr probfile toParent ppid clause_arr = 
17718  267 
let val _ = trace 
268 
("\nGetting lemma names. proofstr is " ^ proofstr ^ 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

269 
"\nprobfile is " ^ probfile ^ 
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

270 
" num of clauses is " ^ string_of_int (Array.length clause_arr)) 
17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
17484
diff
changeset

271 
val axiom_names = getax proofstr clause_arr 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

272 
val ax_str = rules_to_string axiom_names 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17122
diff
changeset

273 
in 
17718  274 
trace ("\nDone. Lemma list is " ^ ax_str); 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

275 
TextIO.output (toParent, "Success. Lemmas used in automatic proof: " ^ 
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

276 
ax_str ^ "\n"); 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

277 
TextIO.output (toParent, probfile ^ "\n"); 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17122
diff
changeset

278 
TextIO.flushOut toParent; 
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17569
diff
changeset

279 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2) 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17122
diff
changeset

280 
end 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

281 
handle exn => (*FIXME: exn handler is too general!*) 
17718  282 
(trace ("\nprover_lemma_list_aux: In exception handler: " ^ 
283 
Toplevel.exn_message exn); 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

284 
TextIO.output (toParent, "Translation failed for the proof: " ^ 
17746  285 
String.toString proofstr ^ "\n"); 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

286 
TextIO.output (toParent, probfile); 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

287 
TextIO.flushOut toParent; 
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17569
diff
changeset

288 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2)); 
17235
8e55ad29b690
Added ECommunication.ML and modified res_atp.ML, Reconstruction.thy, and
quigley
parents:
17122
diff
changeset

289 

17569  290 
val e_lemma_list = prover_lemma_list_aux get_axiom_names_e; 
291 

292 
val vamp_lemma_list = prover_lemma_list_aux get_axiom_names_vamp; 

17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

293 

17488
67376a311a2b
further simplification of the IsabelleATP linkup
paulson
parents:
17484
diff
changeset

294 
val spass_lemma_list = prover_lemma_list_aux get_axiom_names_spass; 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

295 

5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

296 

5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

297 
(**** Full proof reconstruction for SPASS (not really working) ****) 
15642  298 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

299 
fun spass_reconstruct proofstr probfile toParent ppid thms clause_arr = 
17718  300 
let val _ = trace ("\nspass_reconstruct. Proofstr is "^proofstr) 
16905  301 
val tokens = #1(lex proofstr) 
15782  302 

16905  303 
(* parse spass proof into datatype *) 
304 
(***********************************) 

17306  305 
val proof_steps = parse tokens 
17718  306 
val _ = trace "\nParsing finished" 
16905  307 

308 
(************************************) 

309 
(* recreate original subgoal as thm *) 

310 
(************************************) 

311 
(* get axioms as correctly numbered clauses w.r.t. the Spass proof *) 

312 
(* need to get prems_of thm, then get right one of the prems, relating to whichever*) 

313 
(* subgoal this is, and turn it into meta_clauses *) 

314 
(* should prob add array and table here, so that we can get axioms*) 

315 
(* produced from the clasimpset rather than the problem *) 

17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

316 
val (frees,vars,extra_with_vars ,ax_with_vars,numcls) = get_axioms_used proof_steps thms clause_arr 
16905  317 

318 
(*val numcls_string = numclstr ( vars, numcls) ""*) 

17718  319 
val _ = trace "\ngot axioms" 
16061  320 

16905  321 
(************************************) 
322 
(* translate proof *) 

323 
(************************************) 

17718  324 
val _ = trace ("\nabout to translate proof, steps: " 
325 
^ (init_proofsteps_to_string proof_steps "")) 

16905  326 
val (newthm,proof) = translate_proof numcls proof_steps vars 
17718  327 
val _ = trace ("translated proof, steps: "^(init_proofsteps_to_string proof_steps "")) 
16905  328 
(***************************************************) 
329 
(* transfer necessary steps as strings to Isabelle *) 

330 
(***************************************************) 

331 
(* turn the proof into a string *) 

332 
val reconProofStr = proofs_to_string proof "" 

333 
(* do the bit for the Isabelle ordered axioms at the top *) 

334 
val ax_nums = map #1 numcls 

335 
val ax_strs = map ReconOrderClauses.get_meta_lits_bracket (map #2 numcls) 

336 
val numcls_strs = ListPair.zip (ax_nums,ax_strs) 

337 
val num_cls_vars = map (addvars vars) numcls_strs; 

338 
val reconIsaAxStr = origAxs_to_string (ListPair.zip (ax_nums,ax_with_vars)) "" 

339 

340 
val extra_nums = if (not (extra_with_vars = [])) then (1 upto (length extra_with_vars)) 

341 
else [] 

342 
val reconExtraAxStr = extraAxs_to_string ( ListPair.zip (extra_nums,extra_with_vars)) "" 

343 
val frees_str = "["^(thmvars_to_string frees "")^"]" 

344 
val reconstr = (frees_str^reconExtraAxStr^reconIsaAxStr^reconProofStr) 

17718  345 
val _ = trace ("\nReconstruction:\n" ^ reconstr) 
16905  346 
in 
347 
TextIO.output (toParent, reconstr^"\n"); 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

348 
TextIO.output (toParent, probfile ^ "\n"); 
16905  349 
TextIO.flushOut toParent; 
350 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); 

17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17569
diff
changeset

351 
all_tac 
16905  352 
end 
17484
f6a225f97f0a
simplification of the IsabelleATP code; hooks for batch generation of problems
paulson
parents:
17422
diff
changeset

353 
handle exn => (*FIXME: exn handler is too general!*) 
17718  354 
(trace ("\nspass_reconstruct. In exception handler: " ^ Toplevel.exn_message exn); 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

355 
TextIO.output (toParent,"Translation failed for SPASS proof:"^ 
17746  356 
String.toString proofstr ^"\n"); 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

357 
TextIO.output (toParent, probfile ^ "\n"); 
17422  358 
TextIO.flushOut toParent; 
17583
c272b91b619f
removal of "sleep" to stop looping in Poly/ML, and replacement of funny codes by tracing statements
paulson
parents:
17569
diff
changeset

359 
Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr2); all_tac) 
15642  360 

361 
(**********************************************************************************) 

362 
(* At other end, want to turn back into datatype so can apply reconstruct_proof. *) 

363 
(* This will be done by the signal handler *) 

364 
(**********************************************************************************) 

365 

366 
(* Parse in the string version of the proof steps for reconstruction *) 

367 
(* Isar format: cl1 [BINARY 0 cl2 0];cl1 [PARAMOD 0 cl2 0]; cl1 [DEMOD 0 cl2];cl1 [FACTOR 1 2];*) 

368 

369 

370 
val term_numstep = 

371 
(number ++ (a (Other ",")) ++ number) >> (fn (a, (_, c)) => (a, c)) 

372 

373 
val extraaxiomstep = (a (Word "ExtraAxiom"))++ (a (Other "(")) ++(a (Other ")")) 

374 
>> (fn (_) => ExtraAxiom) 

375 

376 

377 

378 
val origaxiomstep = (a (Word "OrigAxiom"))++ (a (Other "(")) ++(a (Other ")")) 

379 
>> (fn (_) => OrigAxiom) 

380 

381 

382 
val axiomstep = (a (Word "Axiom"))++ (a (Other "(")) ++(a (Other ")")) 

383 
>> (fn (_) => Axiom) 

384 

385 

386 

387 

388 
val binarystep = (a (Word "Binary")) ++ (a (Other "(")) ++ (a (Other "(")) 

389 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

390 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

391 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Binary (c,e)) 

392 

393 

394 
val parastep = (a (Word "Para")) ++ (a (Other "(")) ++ (a (Other "(")) 

395 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

396 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

397 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Para(c, e)) 

398 

399 
val mrrstep = (a (Word "MRR")) ++ (a (Other "(")) ++ (a (Other "(")) 

400 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 

401 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

402 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => MRR(c, e)) 

403 

404 

405 
val factorstep = (a (Word "Factor")) ++ (a (Other "(")) 

406 
++ number ++ (a (Other ",")) 

407 
++ number ++ (a (Other ",")) 

408 
++ number ++ (a (Other ")")) 

409 

410 
>> (fn (_, (_, (c, (_, (e,(_,(f,_))))))) => Factor (c,e,f)) 

411 

412 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

413 
(*val rewritestep = (a (Word "Rewrite")) ++ (a (Other "(")) ++ (a (Other "(")) 
15642  414 
++ term_numstep ++ (a (Other ")")) ++ (a (Other ",")) 
415 
++ (a (Other "(")) ++ term_numstep ++ (a (Other ")")) ++ (a (Other ")")) 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

416 
>> (fn (_, (_, (_, (c, (_,(_,(_, (e,(_,_))))))))) => Rewrite (c,e))*) 
15642  417 

418 
val obviousstep = (a (Word "Obvious")) ++ (a (Other "(")) 

419 
++ term_numstep ++ (a (Other ")")) 

420 
>> (fn (_, (_, (c,_))) => Obvious (c)) 

421 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

422 
val methodstep = extraaxiomstep  origaxiomstep  axiomstep binarystep  factorstep parastep  mrrstep  (*rewritestep *) obviousstep 
15642  423 

424 

425 
val number_list_step = 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

426 
( number ++ many ((a (Other ",") ++ number)>> #2)) 
15642  427 
>> (fn (a,b) => (a::b)) 
428 

429 
val numberlist_step = a (Other "[") ++ a (Other "]") 

430 
>>(fn (_,_) => ([]:int list)) 

431 
 a (Other "[") ++ number_list_step ++ a (Other "]") 

432 
>>(fn (_,(a,_)) => a) 

433 

434 

435 

436 
(** change this to allow P (x U) *) 

17306  437 
fun arglist_step input = 
438 
( word ++ many word >> (fn (a, b) => (a^" "^(space_implode " " b))) 

439 
word >> (fn (a) => (a)))input 

15642  440 

441 

442 
fun literal_step input = (word ++ a (Other "(") ++ arglist_step ++ a (Other ")") 

443 
>>(fn (a, (b, (c,d))) => (a^" ("^(c)^")")) 

444 
 arglist_step >> (fn (a) => (a)))input 

445 

446 

447 

448 
(* fun term_step input = (a (Other "~") ++ arglist_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b)) 

449 
 arglist_step ++ a (Other "%")>> (fn (a,b) => a ))input 

450 
*) 

451 

452 

453 
fun term_step input = (a (Other "~") ++ literal_step ++ a (Other "%")>> (fn (a,(b,c)) => ("~ "^b)) 

454 
 literal_step ++ a (Other "%")>> (fn (a,b) => a ))input 

455 

456 

457 

458 

459 
val term_list_step = 

460 
( term_step ++ many ( term_step)) 

461 
>> (fn (a,b) => (a::b)) 

462 

463 

464 
val term_lists_step = a (Other "[") ++ a (Other "]") 

465 
>>(fn (_,_) => ([]:string list)) 

466 
 a (Other "[") ++ term_list_step ++ a (Other "]") 

467 
>>(fn (_,(a,_)) => a) 

468 

469 

470 
val linestep = number ++ methodstep ++ term_lists_step ++ term_lists_step 

471 
>> (fn (a, (b, (c,d))) => (a,(b,c,d))) 

472 

473 
val lines_step = many linestep 

474 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

475 
val alllines_step = (term_lists_step ++ lines_step ) ++ finished >> #1 
15642  476 

15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15700
diff
changeset

477 
val parse_step = #1 o alllines_step 
15642  478 

479 

480 
(* 

481 
val reconstr ="[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]%(EX x::'a::type. ALL y::'a::type. (P::'a::type => bool) x = P y) >(EX x::'a::type. P x) = (ALL y::'a::type. P y)" 

482 
*) 

483 

484 
(************************************************************) 

485 
(* Construct an Isar style proof from a list of proof steps *) 

486 
(************************************************************) 

487 
(* want to assume all axioms, then do haves for the other clauses*) 

488 
(* then show for the last step *) 

489 

490 
(* replace ~ by not here *) 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

491 
val change_nots = String.translate (fn c => if c = #"~" then "\\<not>" else str c); 
15642  492 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

493 
fun clstrs_to_string xs = space_implode "; " (map change_nots xs); 
15642  494 

495 
fun thmvars_to_quantstring [] str = str 

496 
 thmvars_to_quantstring (x::[]) str =str^x^". " 

497 
 thmvars_to_quantstring (x::xs) str = thmvars_to_quantstring xs (str^(x^" ")) 

498 

499 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

500 
fun clause_strs_to_isar clstrs [] = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

501 
"\"\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\"" 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

502 
 clause_strs_to_isar clstrs thmvars = 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

503 
"\"\\<And>"^(thmvars_to_quantstring thmvars "")^ 
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

504 
"\\<lbrakk>"^(clstrs_to_string clstrs)^"\\<rbrakk> \\<Longrightarrow> False\"" 
15642  505 

17317
3f12de2e2e6e
IsabelleATP link: sortable axiom names; no spaces in switches; general tidying
paulson
parents:
17315
diff
changeset

506 
fun frees_to_isar_str clstrs = space_implode " " (map change_nots clstrs) 
15642  507 

508 

509 
(***********************************************************************) 

510 
(* functions for producing assumptions for the Isabelle ordered axioms *) 

511 
(***********************************************************************) 

512 
(*val str = "[P%x%xa%xb%]1OrigAxiom()[P x%~ P U%][U%]3OrigAxiom()[P U%~ P x%][U%]5OrigAxiom()[~ P xa%~ P U%][U%]7OrigAxiom()[P U%P xb%][U%]1Axiom()[P x%~ P U%][U%]3Axiom()[P U%~ P x%][U%]5Axiom()[~ P U%~ P xa%][U%]7Axiom()[P U%P xb%][U%]9Factor(5,0,1)[~ P xa%][]10Binary((9,0),(3,0))[~ P x%][]11Binary((10,0),(1,0))[~ P U%][U%]12Factor(7,0,1)[P xb%][]14Binary((11,0),(12,0))[][]"; 

513 
num, rule, clausestrs, vars*) 

514 

515 

516 
(* assume the extra clauses  not used in Spass proof *) 

517 

518 
fun is_extraaxiom_step ( num:int,(ExtraAxiom, str, tstr)) = true 

519 
 is_extraaxiom_step (num, _) = false 

520 

521 
fun get_extraaxioms xs = List.filter (is_extraaxiom_step) ( xs) 

522 

523 
fun assume_isar_extraaxiom [] str = str 

524 
 assume_isar_extraaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_extraaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " ) 

525 

526 

527 

528 
fun assume_isar_extraaxioms [] = "" 

529 
assume_isar_extraaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

530 
in 

531 
assume_isar_extraaxiom xs str 

532 
end 

533 

534 
(* assume the Isabelle ordered clauses *) 

535 

536 
fun is_origaxiom_step ( num:int,(OrigAxiom, str, tstr)) = true 

537 
 is_origaxiom_step (num, _) = false 

538 

539 
fun get_origaxioms xs = List.filter (is_origaxiom_step) ( xs) 

540 

541 
fun assume_isar_origaxiom [] str = str 

542 
 assume_isar_origaxiom ((numb,(step, clstr, thmvars))::xs) str = assume_isar_origaxiom xs (str^"and cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstr thmvars)^"\n " ) 

543 

544 

545 

546 
fun assume_isar_origaxioms ((numb,(step, clstrs, thmstrs))::xs) = let val str = "assume cl"^(string_of_int numb)^"': "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

547 
in 

548 
assume_isar_origaxiom xs str 

549 
end 

550 

551 

552 

553 
fun is_axiom_step ( num:int,(Axiom, str, tstr)) = true 

554 
 is_axiom_step (num, _) = false 

555 

556 
fun get_axioms xs = List.filter (is_axiom_step) ( xs) 

557 

558 
fun have_isar_axiomline (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

559 

560 
fun by_isar_axiomline (numb,(step, clstrs, thmstrs))="by (rule cl"^ (string_of_int numb)^"') \n" 

561 

562 

563 
fun isar_axiomline (numb, (step, clstrs, thmstrs)) = (have_isar_axiomline (numb,(step,clstrs, thmstrs )))^( by_isar_axiomline(numb,(step,clstrs, thmstrs )) ) 

564 

565 

566 
fun isar_axiomlines [] str = str 

567 
 isar_axiomlines (x::xs) str = isar_axiomlines xs (str^(isar_axiomline x)) 

568 

569 

570 
fun have_isar_line (numb,(step, clstrs, thmstrs))="have cl"^(string_of_int numb)^": "^(clause_strs_to_isar clstrs thmstrs)^"\n" 

16357  571 
(*FIX: ask Larry to add and mrr attribute *) 
15642  572 

16091  573 
fun by_isar_line ((Binary ((a,b), (c,d)))) = 
574 
"by(rule cl"^ 

575 
(string_of_int a)^" [binary "^(string_of_int b)^" cl"^ 

576 
(string_of_int c)^" "^(string_of_int d)^"])\n" 

16357  577 
by_isar_line ((MRR ((a,b), (c,d)))) = 
578 
"by(rule cl"^ 

579 
(string_of_int a)^" [binary "^(string_of_int b)^" cl"^ 

580 
(string_of_int c)^" "^(string_of_int d)^"])\n" 

16091  581 
 by_isar_line ( (Para ((a,b), (c,d)))) = 
582 
"by (rule cl"^ 

583 
(string_of_int a)^" [paramod "^(string_of_int b)^" cl"^ 

584 
(string_of_int c)^" "^(string_of_int d)^"])\n" 

585 
 by_isar_line ((Factor ((a,b,c)))) = 

586 
"by (rule cl"^(string_of_int a)^" [factor "^(string_of_int b)^" "^ 

587 
(string_of_int c)^" ])\n" 

16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

588 
(* by_isar_line ( (Rewrite ((a,b),(c,d)))) = 
16091  589 
"by (rule cl"^(string_of_int a)^" [demod "^(string_of_int b)^" "^ 
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16520
diff
changeset

590 
(string_of_int c)^" "^(string_of_int d)^" ])\n"*) 
16091  591 
 by_isar_line ( (Obvious ((a,b)))) = 
592 
"by (rule cl"^(string_of_int a)^" [obvious "^(string_of_int b)^" ])\n" 

15642  593 

594 
fun isar_line (numb, (step, clstrs, thmstrs)) = (have_isar_line (numb,(step,clstrs, thmstrs )))^( by_isar_line step) 

595 

596 

597 
fun isar_lines [] str = str 

598 
 isar_lines (x::xs) str = isar_lines xs (str^(isar_line x)) 

599 

600 
fun last_isar_line (numb,( step, clstrs,thmstrs)) = "show \"False\"\n"^(by_isar_line step) 

601 

602 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

603 
fun to_isar_proof (frees, xs) = 
16091  604 
let val extraaxioms = get_extraaxioms xs 
605 
val extraax_num = length extraaxioms 

606 
val origaxioms_and_steps = Library.drop (extraax_num, xs) 

607 

608 
val origaxioms = get_origaxioms origaxioms_and_steps 

609 
val origax_num = length origaxioms 

610 
val axioms_and_steps = Library.drop (origax_num + extraax_num, xs) 

611 
val axioms = get_axioms axioms_and_steps 

612 

613 
val steps = Library.drop (origax_num, axioms_and_steps) 

614 
val firststeps = ReconOrderClauses.butlast steps 

17312  615 
val laststep = List.last steps 
16091  616 

617 
val isar_proof = 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

618 
("show \"[your goal]\"\n")^ 
16091  619 
("proof (rule ccontr,skolemize, make_clauses) \n")^ 
620 
("fix "^(frees_to_isar_str frees)^"\n")^ 

621 
(assume_isar_extraaxioms extraaxioms)^ 

622 
(assume_isar_origaxioms origaxioms)^ 

623 
(isar_axiomlines axioms "")^ 

624 
(isar_lines firststeps "")^ 

625 
(last_isar_line laststep)^ 

626 
("qed") 

17718  627 
val _ = trace ("\nto_isar_proof returns " ^ isar_proof) 
16091  628 
in 
629 
isar_proof 

630 
end; 

15642  631 

632 
(* get fix vars from axioms  all Frees *) 

633 
(* check each clause for metavars and /\ over them at each step*) 

634 

635 
(*******************************************************) 

636 
(* This assumes the thm list "numcls" is still there *) 

637 
(* In reality, should probably label it with an *) 

638 
(* ID number identifying the subgoal. This could *) 

639 
(* be passed over to the watcher, e.g. numcls25 *) 

640 
(*******************************************************) 

641 

17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

642 
fun apply_res_thm str = 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

643 
let val tokens = #1 (lex str); 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

644 
val _ = trace ("\napply_res_thm. str is: "^str^"\n") 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

645 
val (frees,recon_steps) = parse_step tokens 
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

646 
in 
17772
818cec5f82a4
major simplification: removal of the goalstring argument
paulson
parents:
17746
diff
changeset

647 
to_isar_proof (frees, recon_steps) 
17315
5bf0e0aacc24
consolidation of duplicate code in IsabelleATP linkup
paulson
parents:
17312
diff
changeset

648 
end 
15642  649 

15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset

650 
end; 