author  wenzelm 
Thu, 06 Dec 2012 23:01:49 +0100  
changeset 50410  6ab3fadf43af 
parent 50277  e0a4d8404c76 
child 50450  358b6020f8b6 
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 = 

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

26 
bool * bool * Time.time * real * string Symtab.table 
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 

153 
val leo2_ext = "extcnf_equal_neg" 

154 
val leo2_unfold_def = "unfold_def" 

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)) = 
49914  157 
(if rule = leo2_ext then 
158 
insert (op =) (ext_name ctxt, (Global, General)) 

159 
else if rule = leo2_unfold_def then 

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 = 

50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50102
diff
changeset

223 
banner ^ ": " ^ 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 => 

50163
c62ce309dc26
more abstract Sendback operations, with explicit id/exec_id properties;
wenzelm
parents:
50102
diff
changeset

230 
"\nTo minimize: " ^ 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 

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

392 
 add_line _ (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 

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

395 
Inference_Step (name, role, t, rule, deps) :: 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? *) 

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

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

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

402 
Inference_Step (name, role, t', rule, deps) :: 
49914  403 
pre @ map (replace_dependencies_in_line (name', [name])) post 
404 
 _ => raise Fail "unexpected inference" 

405 

406 
val waldmeister_conjecture_num = "1.0.0.0" 

407 

408 
val repair_waldmeister_endgame = 

409 
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

410 
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

411 
Inference_Step (name, role, s_not t, rule, deps) 
49914  412 
 do_tail line = line 
413 
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

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

417 
 do_body (line :: lines) = line :: do_body lines 

418 
in do_body end 

419 

420 
(* 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

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

424 
 add_nontrivial_line line lines = line :: lines 

425 
and delete_dependency name lines = 

426 
fold_rev add_nontrivial_line 

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

428 

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

430 
offending lines often does the trick. *) 

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

432 
 is_bad_free _ _ = false 

433 

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

434 
fun add_desired_line _ _ (line as Definition_Step (name, _, _)) (j, lines) = 
49914  435 
(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

436 
 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

437 
(Inference_Step (name as (_, ss), role, t, rule, deps)) (j, lines) = 
49914  438 
(j + 1, 
439 
if is_fact fact_names ss orelse 

440 
is_conjecture ss orelse 

441 
(* the last line must be kept *) 

442 
j = 0 orelse 

443 
(not (is_only_type_information t) andalso 

444 
null (Term.add_tvars t []) andalso 

445 
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

446 
length deps >= 2 andalso 
49914  447 
(* kill next to last line, which usually results in a trivial step *) 
448 
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

449 
Inference_Step (name, role, t, rule, deps) :: lines (* keep line *) 
49914  450 
else 
451 
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) 

452 

453 
val indent_size = 2 

454 
val no_label = ("", ~1) 

455 

49883  456 
fun string_for_proof ctxt type_enc lam_trans i n = 
457 
let 

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

459 
fun do_free (s, T) = 

460 
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

461 
maybe_quote (simplify_spaces (with_vanilla_print_mode 
50048  462 
(Syntax.string_of_typ ctxt) T)) 
49883  463 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": " 
464 
fun do_have qs = 

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

466 
(if member (op =) qs Then then 

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

468 
else 

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

470 
val do_term = 

50048  471 
annotate_types ctxt 
472 
#> 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

473 
#> simplify_spaces 
50048  474 
#> maybe_quote 
49883  475 
val reconstr = Metis (type_enc, lam_trans) 
49921  476 
fun do_facts ind (ls, ss) = 
477 
"\n" ^ do_indent (ind + 1) ^ 

49883  478 
reconstructor_command reconstr 1 1 [] 0 
479 
(ls > sort_distinct (prod_ord string_ord int_ord), 

480 
ss > sort_distinct string_ord) 

481 
and do_step ind (Fix xs) = 

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

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

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

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

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

487 
 do_step ind (Prove (qs, l, t, By_Metis facts)) = 

488 
do_indent ind ^ do_have qs ^ " " ^ 

49921  489 
do_label l ^ do_term t ^ do_facts ind facts ^ "\n" 
49883  490 
 do_step ind (Prove (qs, l, t, Case_Split (proofs, facts))) = 
491 
implode (map (prefix (do_indent ind ^ "moreover\n") o do_block ind) 

492 
proofs) ^ 

49921  493 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ 
494 
do_facts ind facts ^ "\n" 

49883  495 
and do_steps prefix suffix ind steps = 
496 
let val s = implode (map (do_step ind) steps) in 

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

498 
String.extract (s, ind * indent_size, 

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

500 
suffix ^ "\n" 

501 
end 

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

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

504 
directly. *) 

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

506 
 do_proof proof = 

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

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

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

510 
in do_proof end 

511 

49914  512 
fun used_labels_of_step (Prove (_, _, _, by)) = 
513 
(case by of 

514 
By_Metis (ls, _) => ls 

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

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

517 
 used_labels_of_step _ = [] 

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

519 

520 
fun kill_useless_labels_in_proof proof = 

521 
let 

522 
val used_ls = used_labels_of proof 

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

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

525 
 do_step (Prove (qs, l, t, by)) = 

526 
Prove (qs, do_label l, t, 

527 
case by of 

528 
Case_Split (proofs, facts) => 

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

530 
 _ => by) 

531 
 do_step step = step 

532 
in map do_step proof end 

533 

534 
fun prefix_for_depth n = replicate_string (n + 1) 

535 

536 
val relabel_proof = 

537 
let 

538 
fun aux _ _ _ [] = [] 

50017  539 
 aux subst depth (next_assum, next_have) (Assume (l, t) :: proof) = 
49914  540 
if l = no_label then 
50017  541 
Assume (l, t) :: aux subst depth (next_assum, next_have) proof 
49914  542 
else 
50017  543 
let val l' = (prefix_for_depth depth assume_prefix, next_assum) in 
49914  544 
Assume (l', t) :: 
50017  545 
aux ((l, l') :: subst) depth (next_assum + 1, next_have) proof 
49914  546 
end 
50017  547 
 aux subst depth (next_assum, next_have) 
49914  548 
(Prove (qs, l, t, by) :: proof) = 
549 
let 

50017  550 
val (l', subst, next_have) = 
49914  551 
if l = no_label then 
50017  552 
(l, subst, next_have) 
49914  553 
else 
50017  554 
let val l' = (prefix_for_depth depth have_prefix, next_have) in 
555 
(l', (l, l') :: subst, next_have + 1) 

556 
end 

49914  557 
val relabel_facts = 
558 
apfst (maps (the_list o AList.lookup (op =) subst)) 

559 
val by = 

560 
case by of 

561 
By_Metis facts => By_Metis (relabel_facts facts) 

562 
 Case_Split (proofs, facts) => 

563 
Case_Split (map (aux subst (depth + 1) (1, 1)) proofs, 

564 
relabel_facts facts) 

565 
in 

50017  566 
Prove (qs, l', t, by) :: aux subst depth (next_assum, next_have) proof 
49914  567 
end 
568 
 aux subst depth nextp (step :: proof) = 

569 
step :: aux subst depth nextp proof 

570 
in aux [] 0 (1, 1) end 

571 

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

572 
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

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

574 
fun succedent_of_step (Prove (_, label, _, _)) = SOME label 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

575 
 succedent_of_step (Assume (label, _)) = SOME label 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

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

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

578 
(step as Prove (qs, label, t, By_Metis (lfs, gfs))) = 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

579 
if member (op =) lfs label0 then 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

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

581 
By_Metis (filter_out (curry (op =) label0) lfs, gfs)) 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

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

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

584 
 chain_inf _ (Prove (qs, label, t, Case_Split (proofs, facts))) = 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

585 
Prove (qs, label, t, Case_Split ((map (chain_proof NONE) proofs), facts)) 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

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

587 
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

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

589 
chain_inf prev i :: chain_proof (succedent_of_step i) is 
c96e8e40d789
several improvements to Isar proof reconstruction, by Steffen Smolka (step merging in case splits, time measurements, etc.)
blanchet
parents:
49994
diff
changeset

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

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

592 
in chain_proof NONE end 
49883  593 

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

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

596 
* (string * stature) list vector * int Symtab.table * string proof * thm 
49914  597 

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

598 
fun isar_proof_text ctxt isar_proofs 
50020  599 
(debug, verbose, preplay_timeout, isar_shrink, pool, fact_names, sym_tab, 
600 
atp_proof, goal) 

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

601 
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = 
49883  602 
let 
603 
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal 

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

605 
val one_line_proof = one_line_proof_text 0 one_line_params 

606 
val type_enc = 

607 
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN 

608 
else partial_typesN 

609 
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans 

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

610 
val preplay = preplay_timeout <> seconds 0.0 
49883  611 

612 
fun isar_proof_of () = 

613 
let 

614 
val atp_proof = 

615 
atp_proof 

616 
> clean_up_atp_proof_dependencies 

617 
> nasty_atp_proof pool 

618 
> map_term_names_in_atp_proof repair_name 

619 
> decode_lines ctxt sym_tab 

620 
> rpair [] > fold_rev (add_line fact_names) 

621 
> repair_waldmeister_endgame 

622 
> rpair [] > fold_rev add_nontrivial_line 

623 
> rpair (0, []) 

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

624 
> fold_rev (add_desired_line fact_names frees) 
49883  625 
> snd 
626 
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) 

627 
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

628 
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

629 
(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

630 
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

631 
 _ => 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

632 
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

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

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

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

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

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

638 
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

639 
 _ => 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

640 
 _ => NONE) 
49883  641 
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

642 
 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

643 
SOME (from, name) 
49883  644 
val ref_graph = atp_proof > map_filter dep_of_step > make_ref_graph 
645 
val axioms = axioms_of_ref_graph ref_graph conjs 

646 
val tainted = tainted_atoms_of_ref_graph ref_graph conjs 

647 
val props = 

648 
Symtab.empty 

649 
> fold (fn Definition_Step _ => I (* FIXME *) 

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

650 
 Inference_Step (name as (s, ss), role, t, _, _) => 
49883  651 
Symtab.update_new (s, 
50016  652 
if member (op = o apsnd fst) tainted s then 
653 
t > role <> Conjecture ? s_not 

654 
> fold exists_of (map Var (Term.add_vars t [])) 

655 
else 

656 
t)) 

49883  657 
atp_proof 
50013
cceec179bdca
use original formulas for hypotheses and conclusion to avoid mismatches
blanchet
parents:
50012
diff
changeset

658 
(* The assumptions and conjecture are props; the rest are bools. *) 
50016  659 
fun prop_of_clause [name as (s, ss)] = 
660 
(case resolve_conjecture ss of 

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

662 
 _ => the_default @{term False} (Symtab.lookup props s) 

663 
> HOLogic.mk_Trueprop > close_form) 

664 
 prop_of_clause names = 

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

665 
let val lits = map_filter (Symtab.lookup props o fst) names in 
4ea26c74d7ea
use implications rather than disjunctions to improve readability
blanchet
parents:
50017
diff
changeset

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

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

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

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

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

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

672 
end 
50016  673 
> HOLogic.mk_Trueprop > close_form 
49883  674 
fun maybe_show outer c = 
675 
(outer andalso length c = 1 andalso subset (op =) (c, conjs)) 

676 
? cons Show 

677 
fun do_have outer qs (gamma, c) = 

678 
Prove (maybe_show outer c qs, label_of_clause c, prop_of_clause c, 

50005  679 
By_Metis (fold (add_fact_from_dependencies fact_names) gamma 
680 
([], []))) 

49883  681 
fun do_inf outer (Have z) = do_have outer [] z 
682 
 do_inf outer (Cases cases) = 

683 
let val c = succedent_of_cases cases in 

684 
Prove (maybe_show outer c [Ultimately], label_of_clause c, 

685 
prop_of_clause c, 

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

687 
end 

688 
and do_case outer (c, infs) = 

689 
Assume (label_of_clause c, prop_of_clause c) :: 

690 
map (do_inf outer) infs 

50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50269
diff
changeset

691 
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

692 
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

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

694 
> map (do_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

695 
> append assms 
50257  696 
> (if not preplay andalso isar_shrink <= 1.0 
50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50269
diff
changeset

697 
then pair (false, (true, seconds 0.0)) #> swap 
50257  698 
else shrink_proof debug ctxt type_enc lam_trans preplay 
699 
preplay_timeout (if isar_proofs then isar_shrink else 1000.0)) 

700 
(* >> reorder_proof_to_minimize_jumps (* ? *) *) 

701 
>> chain_direct_proof 

702 
>> kill_useless_labels_in_proof 

703 
>> relabel_proof 

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

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

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

706 
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

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

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

711 
if isar_proofs then 
49883  712 
"\nNo structured proof available (proof too short)." 
713 
else 

714 
"" 

715 
 _ => 

50271
2be84eaf7ebb
deal with the case that metis does not time out, but fails instead
smolkas
parents:
50269
diff
changeset

716 
let 
50277  717 
val msg = 
718 
(if preplay then 

719 
[if preplay_fail 

720 
then "may fail" 

721 
else string_from_ext_time ext_time] 

722 
else []) 

723 
@ 

724 
(if verbose then 

725 
[let val num_steps = metis_steps_total isar_proof 

726 
in string_of_int num_steps ^ plural_s num_steps end] 

727 
else []) 

728 
in 

729 
"\n\nStructured proof " 

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

50410
6ab3fadf43af
proper Sendback.markup, as required for standard Prover IDE protocol (see also c62ce309dc26);
wenzelm
parents:
50277
diff
changeset

731 
^ ":\n" ^ Sendback.markup isar_text 
50277  732 
end 
49883  733 
end 
734 
val isar_proof = 

735 
if debug then 

736 
isar_proof_of () 

737 
else case try isar_proof_of () of 

738 
SOME s => s 

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

739 
 NONE => if isar_proofs then 
49883  740 
"\nWarning: The Isar proof construction failed." 
741 
else 

742 
"" 

743 
in one_line_proof ^ isar_proof end 

744 

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

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

747 
(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

748 
isar_proof_text ctxt isar_proofs isar_params 
49883  749 
else 
750 
one_line_proof_text num_chained) one_line_params 

751 

752 
end; 