author  smolkas 
Wed, 02 Jan 2013 20:52:39 +0100  
changeset 50679  e409d9f8ec75 
parent 50677  f5c217474eca 
child 50705  0e943b33d907 
permissions  rwrr 
49883  1 
(* Title: HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML 
2 
Author: Jasmin Blanchette, TU Muenchen 

3 
Author: Steffen Juilf Smolka, TU Muenchen 

4 

49914  5 
Isar proof reconstruction from ATP proofs. 
49883  6 
*) 
7 

8 
signature SLEDGEHAMMER_PROOF_RECONSTRUCT = 

9 
sig 

49914  10 
type 'a proof = 'a ATP_Proof.proof 
11 
type stature = ATP_Problem_Generate.stature 

12 

13 
datatype reconstructor = 

14 
Metis of string * string  

15 
SMT 

16 

17 
datatype play = 

18 
Played of reconstructor * Time.time  

19 
Trust_Playable of reconstructor * Time.time option  

20 
Failed_to_Play of reconstructor 

21 

22 
type minimize_command = string list > string 

23 
type one_line_params = 

24 
play * string * (string * stature) list * minimize_command * int * int 

25 
type isar_params = 

50557  26 
bool * bool * Time.time option * real * string Symtab.table 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

27 
* (string * stature) list vector * int Symtab.table * string proof * thm 
49914  28 

29 
val smtN : string 

30 
val string_for_reconstructor : reconstructor > string 

31 
val lam_trans_from_atp_proof : string proof > string > string 

32 
val is_typed_helper_used_in_atp_proof : string proof > bool 

33 
val used_facts_in_atp_proof : 

34 
Proof.context > (string * stature) list vector > string proof > 

35 
(string * stature) list 

36 
val used_facts_in_unsound_atp_proof : 

37 
Proof.context > (string * stature) list vector > 'a proof > 

38 
string list option 

39 
val one_line_proof_text : int > one_line_params > string 

49883  40 
val isar_proof_text : 
49913  41 
Proof.context > bool > isar_params > one_line_params > string 
49883  42 
val proof_text : 
49913  43 
Proof.context > bool > isar_params > int > one_line_params > string 
49883  44 
end; 
45 

46 
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = 

47 
struct 

48 

49 
open ATP_Util 

49914  50 
open ATP_Problem 
49883  51 
open ATP_Proof 
52 
open ATP_Problem_Generate 

53 
open ATP_Proof_Reconstruct 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

54 
open Sledgehammer_Util 
50264
a9ec48b98734
renamed sledgehammer_isar_reconstruct to sledgehammer_proof
smolkas
parents:
50262
diff
changeset

55 
open Sledgehammer_Proof 
50258  56 
open Sledgehammer_Annotate 
50259  57 
open Sledgehammer_Shrink 
49914  58 

59 
structure String_Redirect = ATP_Proof_Redirect( 

60 
type key = step_name 

61 
val ord = fn ((s, _ : string list), (s', _)) => fast_string_ord (s, s') 

62 
val string_of = fst) 

63 

49883  64 
open String_Redirect 
65 

49916
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

66 

49914  67 
(** reconstructors **) 
68 

69 
datatype reconstructor = 

70 
Metis of string * string  

71 
SMT 

72 

73 
datatype play = 

74 
Played of reconstructor * Time.time  

75 
Trust_Playable of reconstructor * Time.time option  

76 
Failed_to_Play of reconstructor 

77 

78 
val smtN = "smt" 

79 

80 
fun string_for_reconstructor (Metis (type_enc, lam_trans)) = 

81 
metis_call type_enc lam_trans 

82 
 string_for_reconstructor SMT = smtN 

83 

84 

85 
(** fact extraction from ATP proofs **) 

86 

87 
fun find_first_in_list_vector vec key = 

88 
Vector.foldl (fn (ps, NONE) => AList.lookup (op =) ps key 

89 
 (_, value) => value) NONE vec 

90 

91 
val unprefix_fact_number = space_implode "_" o tl o space_explode "_" 

92 

93 
fun resolve_one_named_fact fact_names s = 

94 
case try (unprefix fact_prefix) s of 

95 
SOME s' => 

96 
let val s' = s' > unprefix_fact_number > unascii_of in 

97 
s' > find_first_in_list_vector fact_names > Option.map (pair s') 

98 
end 

99 
 NONE => NONE 

100 
fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) 

101 
fun is_fact fact_names = not o null o resolve_fact fact_names 

102 

103 
fun resolve_one_named_conjecture s = 

104 
case try (unprefix conjecture_prefix) s of 

105 
SOME s' => Int.fromString s' 

106 
 NONE => NONE 

107 

108 
val resolve_conjecture = map_filter resolve_one_named_conjecture 

109 
val is_conjecture = not o null o resolve_conjecture 

110 

111 
val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix 

112 

113 
(* overapproximation (good enough) *) 

114 
fun is_lam_lifted s = 

115 
String.isPrefix fact_prefix s andalso 

116 
String.isSubstring ascii_of_lam_fact_prefix s 

117 

118 
val is_combinator_def = String.isPrefix (helper_prefix ^ combinator_prefix) 

119 

120 
fun is_axiom_used_in_proof pred = 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

121 
exists (fn Inference_Step ((_, ss), _, _, _, []) => exists pred ss 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

122 
 _ => false) 
49914  123 

124 
fun lam_trans_from_atp_proof atp_proof default = 

125 
case (is_axiom_used_in_proof is_combinator_def atp_proof, 

126 
is_axiom_used_in_proof is_lam_lifted atp_proof) of 

127 
(false, false) => default 

128 
 (false, true) => liftingN 

129 
(*  (true, true) => combs_and_liftingN  not supported by "metis" *) 

130 
 (true, _) => combsN 

131 

132 
val is_typed_helper_name = 

133 
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix 

134 
fun is_typed_helper_used_in_atp_proof atp_proof = 

135 
is_axiom_used_in_proof is_typed_helper_name atp_proof 

136 

137 
fun add_non_rec_defs fact_names accum = 

138 
Vector.foldl (fn (facts, facts') => 

139 
union (op =) (filter (fn (_, (_, status)) => status = Non_Rec_Def) facts) 

140 
facts') 

141 
accum fact_names 

142 

143 
val isa_ext = Thm.get_name_hint @{thm ext} 

144 
val isa_short_ext = Long_Name.base_name isa_ext 

145 

146 
fun ext_name ctxt = 

147 
if Thm.eq_thm_prop (@{thm ext}, 

148 
singleton (Attrib.eval_thms ctxt) (Facts.named isa_short_ext, [])) then 

149 
isa_short_ext 

150 
else 

151 
isa_ext 

152 

50675  153 
val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg" 
154 
val leo2_unfold_def_rule = "unfold_def" 

49914  155 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

156 
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, _, rule, deps)) = 
50675  157 
(if rule = leo2_extcnf_equal_neg_rule then 
49914  158 
insert (op =) (ext_name ctxt, (Global, General)) 
50675  159 
else if rule = leo2_unfold_def_rule then 
49914  160 
(* LEO 1.3.3 does not record definitions properly, leading to missing 
161 
dependencies in the TSTP proof. Remove the next line once this is 

162 
fixed. *) 

163 
add_non_rec_defs fact_names 

164 
else if rule = satallax_coreN then 

165 
(fn [] => 

166 
(* Satallax doesn't include definitions in its unsatisfiable cores, 

167 
so we assume the worst and include them all here. *) 

168 
[(ext_name ctxt, (Global, General))] > add_non_rec_defs fact_names 

169 
 facts => facts) 

170 
else 

171 
I) 

172 
#> (if null deps then union (op =) (resolve_fact fact_names ss) 

173 
else I) 

174 
 add_fact _ _ _ = I 

175 

176 
fun used_facts_in_atp_proof ctxt fact_names atp_proof = 

177 
if null atp_proof then Vector.foldl (uncurry (union (op =))) [] fact_names 

178 
else fold (add_fact ctxt fact_names) atp_proof [] 

179 

180 
fun used_facts_in_unsound_atp_proof _ _ [] = NONE 

181 
 used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = 

182 
let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in 

183 
if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso 

184 
not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then 

185 
SOME (map fst used_facts) 

186 
else 

187 
NONE 

188 
end 

189 

190 

191 
(** oneliner reconstructor proofs **) 

192 

193 
fun show_time NONE = "" 

194 
 show_time (SOME ext_time) = " (" ^ string_from_ext_time ext_time ^ ")" 

195 

49986
90e7be285b49
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
blanchet
parents:
49983
diff
changeset

196 
(* FIXME: Various bugs, esp. with "unfolding" 
49914  197 
fun unusing_chained_facts _ 0 = "" 
198 
 unusing_chained_facts used_chaineds num_chained = 

199 
if length used_chaineds = num_chained then "" 

200 
else if null used_chaineds then "(* using no facts *) " 

201 
else "(* using only " ^ space_implode " " used_chaineds ^ " *) " 

49986
90e7be285b49
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
blanchet
parents:
49983
diff
changeset

202 
*) 
49914  203 

204 
fun apply_on_subgoal _ 1 = "by " 

205 
 apply_on_subgoal 1 _ = "apply " 

206 
 apply_on_subgoal i n = 

207 
"prefer " ^ string_of_int i ^ " " ^ apply_on_subgoal 1 n 

208 

209 
fun using_labels [] = "" 

210 
 using_labels ls = 

211 
"using " ^ space_implode " " (map string_for_label ls) ^ " " 

212 

213 
fun command_call name [] = 

50239  214 
name > not (Symbol_Pos.is_identifier name) ? enclose "(" ")" 
49914  215 
 command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" 
216 

217 
fun reconstructor_command reconstr i n used_chaineds num_chained (ls, ss) = 

49986
90e7be285b49
took out "using only ..." comments in Sledgehammer generated metis/smt calls, until these can be generated soundly
blanchet
parents:
49983
diff
changeset

218 
(* unusing_chained_facts used_chaineds num_chained ^ *) 
49914  219 
using_labels ls ^ apply_on_subgoal i n ^ 
220 
command_call (string_for_reconstructor reconstr) ss 

221 

222 
fun try_command_line banner time command = 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50410
diff
changeset

223 
banner ^ ": " ^ Active.sendback_markup command ^ show_time time ^ "." 
49914  224 

225 
fun minimize_line _ [] = "" 

226 
 minimize_line minimize_command ss = 

227 
case minimize_command ss of 

228 
"" => "" 

229 
 command => 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50410
diff
changeset

230 
"\nTo minimize: " ^ Active.sendback_markup command ^ "." 
49914  231 

232 
fun split_used_facts facts = 

233 
facts > List.partition (fn (_, (sc, _)) => sc = Chained) 

234 
> pairself (sort_distinct (string_ord o pairself fst)) 

235 

236 
type minimize_command = string list > string 

237 
type one_line_params = 

238 
play * string * (string * stature) list * minimize_command * int * int 

239 

240 
fun one_line_proof_text num_chained 

241 
(preplay, banner, used_facts, minimize_command, subgoal, 

242 
subgoal_count) = 

243 
let 

244 
val (chained, extra) = split_used_facts used_facts 

245 
val (failed, reconstr, ext_time) = 

246 
case preplay of 

247 
Played (reconstr, time) => (false, reconstr, (SOME (false, time))) 

248 
 Trust_Playable (reconstr, time) => 

249 
(false, reconstr, 

250 
case time of 

251 
NONE => NONE 

252 
 SOME time => 

253 
if time = Time.zeroTime then NONE else SOME (true, time)) 

254 
 Failed_to_Play reconstr => (true, reconstr, NONE) 

255 
val try_line = 

256 
([], map fst extra) 

257 
> reconstructor_command reconstr subgoal subgoal_count (map fst chained) 

258 
num_chained 

259 
> (if failed then 

260 
enclose "Oneline proof reconstruction failed: " 

261 
".\n(Invoking \"sledgehammer\" with \"[strict]\" might \ 

262 
\solve this.)" 

263 
else 

264 
try_command_line banner ext_time) 

265 
in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end 

266 

267 

268 
(** Isar proof construction and manipulation **) 

269 

50017  270 
val assume_prefix = "a" 
49914  271 
val have_prefix = "f" 
272 
val raw_prefix = "x" 

273 

274 
fun raw_label_for_name (num, ss) = 

275 
case resolve_conjecture ss of 

276 
[j] => (conjecture_prefix, j) 

277 
 _ => (raw_prefix ^ ascii_of num, 0) 

278 

50005  279 
fun label_of_clause [name] = raw_label_for_name name 
50262  280 
 label_of_clause c = (space_implode "___" (map (fst o raw_label_for_name) c), 0) 
50005  281 

282 
fun add_fact_from_dependencies fact_names (names as [(_, ss)]) = 

283 
if is_fact fact_names ss then 

284 
apsnd (union (op =) (map fst (resolve_fact fact_names ss))) 

285 
else 

286 
apfst (insert (op =) (label_of_clause names)) 

287 
 add_fact_from_dependencies fact_names names = 

288 
apfst (insert (op =) (label_of_clause names)) 

49914  289 

290 
fun repair_name "$true" = "c_True" 

291 
 repair_name "$false" = "c_False" 

292 
 repair_name "$$e" = tptp_equal (* seen in Vampire proofs *) 

293 
 repair_name s = 

294 
if is_tptp_equal s orelse 

295 
(* seen in Vampire proofs *) 

296 
(String.isPrefix "sQ" s andalso String.isSuffix "_eqProxy" s) then 

297 
tptp_equal 

298 
else 

299 
s 

300 

301 
fun unvarify_term (Var ((s, 0), T)) = Free (s, T) 

302 
 unvarify_term t = raise TERM ("unvarify_term: nonVar", [t]) 

303 

304 
fun infer_formula_types ctxt = 

305 
Type.constraint HOLogic.boolT 

306 
#> Syntax.check_term 

307 
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt) 

308 

309 
val combinator_table = 

310 
[(@{const_name Meson.COMBI}, @{thm Meson.COMBI_def [abs_def]}), 

311 
(@{const_name Meson.COMBK}, @{thm Meson.COMBK_def [abs_def]}), 

312 
(@{const_name Meson.COMBB}, @{thm Meson.COMBB_def [abs_def]}), 

313 
(@{const_name Meson.COMBC}, @{thm Meson.COMBC_def [abs_def]}), 

314 
(@{const_name Meson.COMBS}, @{thm Meson.COMBS_def [abs_def]})] 

315 

316 
fun uncombine_term thy = 

317 
let 

318 
fun aux (t1 $ t2) = betapply (pairself aux (t1, t2)) 

319 
 aux (Abs (s, T, t')) = Abs (s, T, aux t') 

320 
 aux (t as Const (x as (s, _))) = 

321 
(case AList.lookup (op =) combinator_table s of 

322 
SOME thm => thm > prop_of > specialize_type thy x 

323 
> Logic.dest_equals > snd 

324 
 NONE => t) 

325 
 aux t = t 

326 
in aux end 

327 

328 
fun decode_line sym_tab (Definition_Step (name, phi1, phi2)) ctxt = 

329 
let 

330 
val thy = Proof_Context.theory_of ctxt 

331 
val t1 = prop_from_atp ctxt true sym_tab phi1 

332 
val vars = snd (strip_comb t1) 

333 
val frees = map unvarify_term vars 

334 
val unvarify_args = subst_atomic (vars ~~ frees) 

335 
val t2 = prop_from_atp ctxt true sym_tab phi2 

336 
val (t1, t2) = 

337 
HOLogic.eq_const HOLogic.typeT $ t1 $ t2 

338 
> unvarify_args > uncombine_term thy > infer_formula_types ctxt 

339 
> HOLogic.dest_eq 

340 
in 

341 
(Definition_Step (name, t1, t2), 

342 
fold Variable.declare_term (maps Misc_Legacy.term_frees [t1, t2]) ctxt) 

343 
end 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

344 
 decode_line sym_tab (Inference_Step (name, role, u, rule, deps)) ctxt = 
49914  345 
let 
346 
val thy = Proof_Context.theory_of ctxt 

347 
val t = u > prop_from_atp ctxt true sym_tab 

348 
> uncombine_term thy > infer_formula_types ctxt 

349 
in 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

350 
(Inference_Step (name, role, t, rule, deps), 
49914  351 
fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) 
352 
end 

353 
fun decode_lines ctxt sym_tab lines = 

354 
fst (fold_map (decode_line sym_tab) lines ctxt) 

355 

356 
fun replace_one_dependency (old, new) dep = 

357 
if is_same_atp_step dep old then new else [dep] 

358 
fun replace_dependencies_in_line _ (line as Definition_Step _) = line 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

359 
 replace_dependencies_in_line p 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

360 
(Inference_Step (name, role, t, rule, deps)) = 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

361 
Inference_Step (name, role, t, rule, 
49914  362 
fold (union (op =) o replace_one_dependency p) deps []) 
363 

364 
(* No "real" literals means only type information (tfree_tcs, clsrel, or 

365 
clsarity). *) 

366 
fun is_only_type_information t = t aconv @{term True} 

367 

368 
fun is_same_inference _ (Definition_Step _) = false 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

369 
 is_same_inference t (Inference_Step (_, _, t', _, _)) = t aconv t' 
49914  370 

371 
(* Discard facts; consolidate adjacent lines that prove the same formula, since 

372 
they differ only in type information.*) 

373 
fun add_line _ (line as Definition_Step _) lines = line :: lines 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

374 
 add_line fact_names (Inference_Step (name as (_, ss), role, t, rule, [])) 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

375 
lines = 
49914  376 
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or 
377 
definitions. *) 

378 
if is_fact fact_names ss then 

379 
(* Facts are not proof lines. *) 

380 
if is_only_type_information t then 

381 
map (replace_dependencies_in_line (name, [])) lines 

382 
(* Is there a repetition? If so, replace later line by earlier one. *) 

383 
else case take_prefix (not o is_same_inference t) lines of 

384 
(_, []) => lines (* no repetition of proof line *) 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

385 
 (pre, Inference_Step (name', _, _, _, _) :: post) => 
49914  386 
pre @ map (replace_dependencies_in_line (name', [name])) post 
387 
 _ => raise Fail "unexpected inference" 

388 
else if is_conjecture ss then 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

389 
Inference_Step (name, role, t, rule, []) :: lines 
49914  390 
else 
391 
map (replace_dependencies_in_line (name, [])) lines 

50675  392 
 add_line _ (line as Inference_Step (name, role, t, rule, deps)) lines = 
49914  393 
(* Type information will be deleted later; skip repetition test. *) 
394 
if is_only_type_information t then 

50675  395 
line :: lines 
49914  396 
(* Is there a repetition? If so, replace later line by earlier one. *) 
397 
else case take_prefix (not o is_same_inference t) lines of 

398 
(* FIXME: Doesn't this code risk conflating proofs involving different 

399 
types? *) 

50675  400 
(_, []) => line :: lines 
401 
 (pre, Inference_Step (name', _, _, _, _) :: post) => 

402 
line :: pre @ map (replace_dependencies_in_line (name', [name])) post 

403 
 _ => raise Fail "unexpected inference" 

49914  404 

405 
val waldmeister_conjecture_num = "1.0.0.0" 

406 

407 
val repair_waldmeister_endgame = 

408 
let 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

409 
fun do_tail (Inference_Step (name, role, t, rule, deps)) = 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

410 
Inference_Step (name, role, s_not t, rule, deps) 
49914  411 
 do_tail line = line 
412 
fun do_body [] = [] 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

413 
 do_body ((line as Inference_Step ((num, _), _, _, _, _)) :: lines) = 
49914  414 
if num = waldmeister_conjecture_num then map do_tail (line :: lines) 
415 
else line :: do_body lines 

416 
 do_body (line :: lines) = line :: do_body lines 

417 
in do_body end 

418 

419 
(* Recursively delete empty lines (type information) from the proof. *) 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

420 
fun add_nontrivial_line (line as Inference_Step (name, _, t, _, [])) lines = 
49914  421 
if is_only_type_information t then delete_dependency name lines 
422 
else line :: lines 

423 
 add_nontrivial_line line lines = line :: lines 

424 
and delete_dependency name lines = 

425 
fold_rev add_nontrivial_line 

426 
(map (replace_dependencies_in_line (name, [])) lines) [] 

427 

428 
(* ATPs sometimes reuse free variable names in the strangest ways. Removing 

429 
offending lines often does the trick. *) 

430 
fun is_bad_free frees (Free x) = not (member (op =) frees x) 

431 
 is_bad_free _ _ = false 

432 

50675  433 
val e_skolemize_rule = "skolemize" 
434 
val vampire_skolemisation_rule = "skolemisation" 

435 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

436 
val is_skolemize_rule = 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

437 
member (op =) [e_skolemize_rule, vampire_skolemisation_rule] 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

438 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

439 
fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = 
49914  440 
(j, line :: map (replace_dependencies_in_line (name, [])) lines) 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

441 
 add_desired_line fact_names frees 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

442 
(Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) = 
49914  443 
(j + 1, 
444 
if is_fact fact_names ss orelse 

445 
is_conjecture ss orelse 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

446 
is_skolemize_rule rule orelse 
49914  447 
(* the last line must be kept *) 
448 
j = 0 orelse 

449 
(not (is_only_type_information t) andalso 

450 
null (Term.add_tvars t []) andalso 

451 
not (exists_subterm (is_bad_free frees) t) andalso 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

452 
length deps >= 2 andalso 
49914  453 
(* kill next to last line, which usually results in a trivial step *) 
454 
j <> 1) then 

50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

455 
Inference_Step (name, role, t, rule, deps) :: lines (* keep line *) 
49914  456 
else 
457 
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) 

458 

459 
val indent_size = 2 

460 
val no_label = ("", ~1) 

461 

49883  462 
fun string_for_proof ctxt type_enc lam_trans i n = 
463 
let 

464 
fun do_indent ind = replicate_string (ind * indent_size) " " 

465 
fun do_free (s, T) = 

466 
maybe_quote s ^ " :: " ^ 

50049
dd6a4655cd72
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
blanchet
parents:
50048
diff
changeset

467 
maybe_quote (simplify_spaces (with_vanilla_print_mode 
50048  468 
(Syntax.string_of_typ ctxt) T)) 
49883  469 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": " 
470 
fun do_have qs = 

471 
(if member (op =) qs Ultimately then "ultimately " else "") ^ 

472 
(if member (op =) qs Then then 

473 
if member (op =) qs Show then "thus" else "hence" 

474 
else 

475 
if member (op =) qs Show then "show" else "have") 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

476 
fun do_obtain qs xs = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

477 
(if member (op =) qs Then then "then " else "") ^ "obtain " ^ 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

478 
(space_implode " " (map fst xs)) ^ " where" 
49883  479 
val do_term = 
50048  480 
annotate_types ctxt 
481 
#> with_vanilla_print_mode (Syntax.string_of_term ctxt) 

50049
dd6a4655cd72
avoid messing too much with output of "string_of_term", so that it doesn't break the yxml encoding for jEdit
blanchet
parents:
50048
diff
changeset

482 
#> simplify_spaces 
50048  483 
#> maybe_quote 
49883  484 
val reconstr = Metis (type_enc, lam_trans) 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

485 
fun do_metis ind (ls, ss) = 
49921  486 
"\n" ^ do_indent (ind + 1) ^ 
49883  487 
reconstructor_command reconstr 1 1 [] 0 
488 
(ls > sort_distinct (prod_ord string_ord int_ord), 

489 
ss > sort_distinct string_ord) 

490 
and do_step ind (Fix xs) = 

491 
do_indent ind ^ "fix " ^ space_implode " and " (map do_free xs) ^ "\n" 

492 
 do_step ind (Let (t1, t2)) = 

493 
do_indent ind ^ "let " ^ do_term t1 ^ " = " ^ do_term t2 ^ "\n" 

494 
 do_step ind (Assume (l, t)) = 

495 
do_indent ind ^ "assume " ^ do_label l ^ do_term t ^ "\n" 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

496 
 do_step ind (Obtain (qs, xs, l, t, By_Metis facts)) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

497 
do_indent ind ^ do_obtain qs xs ^ " " ^ 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

498 
do_label l ^ do_term t ^ do_metis ind facts ^ "\n" 
49883  499 
 do_step ind (Prove (qs, l, t, By_Metis facts)) = 
500 
do_indent ind ^ do_have qs ^ " " ^ 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

501 
do_label l ^ do_term t ^ do_metis ind facts ^ "\n" 
49883  502 
 do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = 
503 
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) 

504 
proofs) ^ 

49921  505 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

506 
do_metis ind facts ^ "\n" 
49883  507 
and do_steps prefix suffix ind steps = 
508 
let val s = implode (map (do_step ind) steps) in 

509 
replicate_string (ind * indent_size  size prefix) " " ^ prefix ^ 

510 
String.extract (s, ind * indent_size, 

511 
SOME (size s  ind * indent_size  1)) ^ 

512 
suffix ^ "\n" 

513 
end 

514 
and do_block ind proof = do_steps "{ " " }" (ind + 1) proof 

515 
(* Onestep proofs are pointless; better use the Metis oneliner 

516 
directly. *) 

517 
and do_proof [Prove (_, _, _, By_Metis _)] = "" 

518 
 do_proof proof = 

519 
(if i <> 1 then "prefer " ^ string_of_int i ^ "\n" else "") ^ 

520 
do_indent 0 ^ "proof \n" ^ do_steps "" "" 1 proof ^ do_indent 0 ^ 

521 
(if n <> 1 then "next" else "qed") 

522 
in do_proof end 

523 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

524 
fun used_labels_of_step (Obtain (_, _, _, _, By_Metis (ls, _))) = ls 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

525 
 used_labels_of_step (Prove (_, _, _, by)) = 
49914  526 
(case by of 
527 
By_Metis (ls, _) => ls 

528 
 Case_Split (proofs, (ls, _)) => 

529 
fold (union (op =) o used_labels_of) proofs ls) 

530 
 used_labels_of_step _ = [] 

531 
and used_labels_of proof = fold (union (op =) o used_labels_of_step) proof [] 

532 

533 
fun kill_useless_labels_in_proof proof = 

534 
let 

535 
val used_ls = used_labels_of proof 

536 
fun do_label l = if member (op =) used_ls l then l else no_label 

537 
fun do_step (Assume (l, t)) = Assume (do_label l, t) 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

538 
 do_step (Obtain (qs, xs, l, t, by)) = Obtain (qs, xs, do_label l, t, by) 
49914  539 
 do_step (Prove (qs, l, t, by)) = 
540 
Prove (qs, do_label l, t, 

541 
case by of 

542 
Case_Split (proofs, facts) => 

543 
Case_Split (map (map do_step) proofs, facts) 

544 
 _ => by) 

545 
 do_step step = step 

546 
in map do_step proof end 

547 

548 
fun prefix_for_depth n = replicate_string (n + 1) 

549 

550 
val relabel_proof = 

551 
let 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

552 
fun fresh_label depth (old as (l, subst, next_have)) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

553 
if l = no_label then 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

554 
old 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

555 
else 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

556 
let val l' = (prefix_for_depth depth have_prefix, next_have) in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

557 
(l', (l, l') :: subst, next_have + 1) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

558 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

559 
fun do_facts subst = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

560 
apfst (maps (the_list o AList.lookup (op =) subst)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

561 
fun do_byline subst depth by = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

562 
case by of 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

563 
By_Metis facts => By_Metis (do_facts subst facts) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

564 
 Case_Split (proofs, facts) => 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

565 
Case_Split (map (do_proof subst (depth + 1) (1, 1)) proofs, 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

566 
do_facts subst facts) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

567 
and do_proof _ _ _ [] = [] 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

568 
 do_proof subst depth (next_assum, next_have) (Assume (l, t) :: proof) = 
49914  569 
if l = no_label then 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

570 
Assume (l, t) :: do_proof subst depth (next_assum, next_have) proof 
49914  571 
else 
50017  572 
let val l' = (prefix_for_depth depth assume_prefix, next_assum) in 
49914  573 
Assume (l', t) :: 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

574 
do_proof ((l, l') :: subst) depth (next_assum + 1, next_have) proof 
49914  575 
end 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

576 
 do_proof subst depth (next_assum, next_have) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

577 
(Obtain (qs, xs, l, t, by) :: proof) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

578 
let 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

579 
val (l, subst, next_have) = (l, subst, next_have) > fresh_label depth 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

580 
val by = by > do_byline subst depth 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

581 
in 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

582 
Obtain (qs, xs, l, t, by) :: 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

583 
do_proof subst depth (next_assum, next_have) proof 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

584 
end 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

585 
 do_proof subst depth (next_assum, next_have) 
49914  586 
(Prove (qs, l, t, by) :: proof) = 
587 
let 

50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

588 
val (l, subst, next_have) = (l, subst, next_have) > fresh_label depth 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

589 
val by = by > do_byline subst depth 
49914  590 
in 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

591 
Prove (qs, l, t, by) :: 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

592 
do_proof subst depth (next_assum, next_have) proof 
49914  593 
end 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

594 
 do_proof subst depth nextp (step :: proof) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

595 
step :: do_proof subst depth nextp proof 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

596 
in do_proof [] 0 (1, 1) end 
49914  597 

50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

598 
val chain_direct_proof = 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

599 
let 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

600 
fun label_of (Assume (l, _)) = SOME l 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

601 
 label_of (Obtain (_, _, l, _, _)) = SOME l 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

602 
 label_of (Prove (_, l, _, _)) = SOME l 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

603 
 label_of _ = NONE 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

604 
fun chain_step (SOME l0) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

605 
(step as Obtain (qs, xs, l, t, By_Metis (lfs, gfs))) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

606 
if member (op =) lfs l0 then 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

607 
Obtain (Then :: qs, xs, l, t, By_Metis (lfs > remove (op =) l0, gfs)) 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

608 
else 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

609 
step 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

610 
 chain_step (SOME l0) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

611 
(step as Prove (qs, l, t, By_Metis (lfs, gfs))) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

612 
if member (op =) lfs l0 then 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

613 
Prove (Then :: qs, l, t, By_Metis (lfs > remove (op =) l0, gfs)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

614 
else 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

615 
step 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

616 
 chain_step _ (Prove (qs, l, t, Case_Split (proofs, facts))) = 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

617 
Prove (qs, l, t, Case_Split ((map (chain_proof NONE) proofs), facts)) 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

618 
 chain_step _ step = step 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

619 
and chain_proof _ [] = [] 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

620 
 chain_proof (prev as SOME _) (i :: is) = 
50672
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

621 
chain_step prev i :: chain_proof (label_of i) is 
ab5b8b5c9cbe
added "obtain" to Isar proof construction data structure
blanchet
parents:
50671
diff
changeset

622 
 chain_proof _ (i :: is) = i :: chain_proof (label_of i) is 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

623 
in chain_proof NONE end 
49883  624 

49914  625 
type isar_params = 
50557  626 
bool * bool * Time.time option * real * string Symtab.table 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

627 
* (string * stature) list vector * int Symtab.table * string proof * thm 
49914  628 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

629 
fun isar_proof_text ctxt isar_proofs 
50020  630 
(debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab, 
631 
atp_proof, goal) 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

632 
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = 
49883  633 
let 
634 
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal 

635 
val frees = fold Term.add_frees (concl_t :: hyp_ts) [] 

636 
val one_line_proof = one_line_proof_text 0 one_line_params 

637 
val type_enc = 

638 
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN 

639 
else partial_typesN 

640 
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans 

50557  641 
val preplay = preplay_timeout <> SOME Time.zeroTime 
49883  642 

643 
fun isar_proof_of () = 

644 
let 

645 
val atp_proof = 

646 
atp_proof 

647 
> clean_up_atp_proof_dependencies 

648 
> nasty_atp_proof pool 

649 
> map_term_names_in_atp_proof repair_name 

650 
> decode_lines ctxt sym_tab 

651 
> rpair [] > fold_rev (add_line fact_names) 

652 
> repair_waldmeister_endgame 

653 
> rpair [] > fold_rev add_nontrivial_line 

654 
> rpair (0, []) 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

655 
> fold_rev (add_desired_line fact_names frees) 
49883  656 
> snd 
657 
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) 

658 
val conjs = 

50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

659 
atp_proof > map_filter 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

660 
(fn Inference_Step (name as (_, ss), _, _, _, []) => 
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

661 
if member (op =) ss conj_name then SOME name else NONE 
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

662 
 _ => NONE) 
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

663 
val assms = 
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

664 
atp_proof > map_filter 
50013
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

665 
(fn Inference_Step (name as (_, ss), _, _, _, []) => 
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

666 
(case resolve_conjecture ss of 
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

667 
[j] => 
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

668 
if j = length hyp_ts then NONE 
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

669 
else SOME (Assume (raw_label_for_name name, nth hyp_ts j)) 
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

670 
 _ => NONE) 
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

671 
 _ => NONE) 
49883  672 
fun dep_of_step (Definition_Step _) = NONE 
50012
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

673 
 dep_of_step (Inference_Step (name, _, _, _, from)) = 
01cb92151a53
track formula roles in proofs and use that to determine whether the conjecture should be negated or not
blanchet
parents:
50010
diff
changeset

674 
SOME (from, name) 
49883  675 
val ref_graph = atp_proof > map_filter dep_of_step > make_ref_graph 
676 
val axioms = axioms_of_ref_graph ref_graph conjs 

677 
val tainted = tainted_atoms_of_ref_graph ref_graph conjs 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

678 
val steps = 
49883  679 
Symtab.empty 
680 
> fold (fn Definition_Step _ => I (* FIXME *) 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

681 
 Inference_Step (name as (s, ss), role, t, rule, _) => 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

682 
Symtab.update_new (s, (rule, 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

683 
t > (if member (op = o apsnd fst) tainted s then 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

684 
(role <> Conjecture ? s_not) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

685 
#> fold exists_of (map Var (Term.add_vars t [])) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

686 
else 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

687 
I)))) 
49883  688 
atp_proof 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

689 
fun is_clause_skolemize_rule [(s, _)] = 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

690 
Option.map (is_skolemize_rule o fst) (Symtab.lookup steps s) = 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

691 
SOME true 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

692 
 is_clause_skolemize_rule _ = false 
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

693 
(* The assumptions and conjecture are "prop"s; the other formulas are 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

694 
"bool"s. *) 
50016  695 
fun prop_of_clause [name as (s, ss)] = 
696 
(case resolve_conjecture ss of 

697 
[j] => if j = length hyp_ts then concl_t else nth hyp_ts j 

50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

698 
 _ => the_default ("", @{term False}) (Symtab.lookup steps s) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

699 
> snd > HOLogic.mk_Trueprop > close_form) 
50016  700 
 prop_of_clause names = 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

701 
let 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

702 
val lits = map snd (map_filter (Symtab.lookup steps o fst) names) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

703 
in 
50018
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

704 
case List.partition (can HOLogic.dest_not) lits of 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

705 
(negs as _ :: _, pos as _ :: _) => 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

706 
HOLogic.mk_imp 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

707 
(Library.foldr1 s_conj (map HOLogic.dest_not negs), 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

708 
Library.foldr1 s_disj pos) 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

709 
 _ => fold (curry s_disj) lits @{term False} 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

710 
end 
50016  711 
> HOLogic.mk_Trueprop > close_form 
49883  712 
fun maybe_show outer c = 
713 
(outer andalso length c = 1 andalso subset (op =) (c, conjs)) 

714 
? cons Show 

50674  715 
fun isar_step_of_direct_inf outer (Have (gamma, c)) = 
50676
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

716 
let 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

717 
val l = label_of_clause c 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

718 
val t = prop_of_clause c 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

719 
val by = 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

720 
By_Metis (fold (add_fact_from_dependencies fact_names) gamma 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

721 
([], [])) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

722 
in 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

723 
if is_clause_skolemize_rule c then 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

724 
let 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

725 
val xs = 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

726 
Term.add_frees t [] 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

727 
> filter_out (Variable.is_declared ctxt o fst) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

728 
in Obtain ([], xs, l, t, by) end 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

729 
else 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

730 
Prove (maybe_show outer c [], l, t, by) 
83b8a5a39709
generate "obtain" steps corresponding to skolemization inferences
blanchet
parents:
50675
diff
changeset

731 
end 
50674  732 
 isar_step_of_direct_inf outer (Cases cases) = 
49883  733 
let val c = succedent_of_cases cases in 
734 
Prove (maybe_show outer c [Ultimately], label_of_clause c, 

735 
prop_of_clause c, 

736 
Case_Split (map (do_case false) cases, ([], []))) 

737 
end 

738 
and do_case outer (c, infs) = 

739 
Assume (label_of_clause c, prop_of_clause c) :: 

50674  740 
map (isar_step_of_direct_inf outer) infs 
50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50269
diff
changeset

741 
val (isar_proof, (preplay_fail, ext_time)) = 
50004
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

742 
ref_graph 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

743 
> redirect_graph axioms tainted 
50674  744 
> map (isar_step_of_direct_inf true) 
50010
17488e45eb5a
proper handling of assumptions arising from the goal's being expressed in rule format, for Isar proof construction
blanchet
parents:
50005
diff
changeset

745 
> append assms 
50557  746 
> (if not preplay andalso isar_shrink <= 1.0 then 
50677  747 
rpair (false, (true, seconds 0.0)) 
50557  748 
else 
749 
shrink_proof debug ctxt type_enc lam_trans preplay 

50679  750 
preplay_timeout 
751 
(if isar_proofs then isar_shrink else 1000.0)) 

50257  752 
(* >> reorder_proof_to_minimize_jumps (* ? *) *) 
753 
>> chain_direct_proof 

754 
>> kill_useless_labels_in_proof 

755 
>> relabel_proof 

756 
>> not (null params) ? cons (Fix params) 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

757 
val isar_text = 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

758 
string_for_proof ctxt type_enc lam_trans subgoal subgoal_count 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

759 
isar_proof 
49883  760 
in 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

761 
case isar_text of 
49883  762 
"" => 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

763 
if isar_proofs then 
50671  764 
"\nNo structured proof available (proof too simple)." 
49883  765 
else 
766 
"" 

767 
 _ => 

50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

768 
let 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

769 
val msg = 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

770 
(if preplay then 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

771 
[if preplay_fail then "may fail" 
50277  772 
else string_from_ext_time ext_time] 
50670
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

773 
else 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

774 
[]) @ 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

775 
(if verbose then 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

776 
let val num_steps = metis_steps_total isar_proof in 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

777 
[string_of_int num_steps ^ " step" ^ plural_s num_steps] 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

778 
end 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

779 
else 
eaa540986291
properly take the existential closure of skolems
blanchet
parents:
50557
diff
changeset

780 
[]) 
50277  781 
in 
782 
"\n\nStructured proof " 

783 
^ (commas msg > not (null msg) ? enclose "(" ")") 

50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50410
diff
changeset

784 
^ ":\n" ^ Active.sendback_markup isar_text 
50277  785 
end 
49883  786 
end 
787 
val isar_proof = 

788 
if debug then 

789 
isar_proof_of () 

790 
else case try isar_proof_of () of 

791 
SOME s => s 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

792 
 NONE => if isar_proofs then 
49883  793 
"\nWarning: The Isar proof construction failed." 
794 
else 

795 
"" 

796 
in one_line_proof ^ isar_proof end 

797 

49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

798 
fun proof_text ctxt isar_proofs isar_params num_chained 
49883  799 
(one_line_params as (preplay, _, _, _, _, _)) = 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

800 
(if case preplay of Failed_to_Play _ => true  _ => isar_proofs then 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

801 
isar_proof_text ctxt isar_proofs isar_params 
49883  802 
else 
803 
one_line_proof_text num_chained) one_line_params 

804 

805 
end; 