author  wenzelm 
Fri, 19 Oct 2012 17:52:21 +0200  
changeset 49936  3e7522664453 
parent 49921  073d69478207 
child 49981  e12b4e9794fd 
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 = 

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

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

29 
val smtN : string 

30 
val string_for_reconstructor : reconstructor > string 

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

31 
val thms_of_name : Proof.context > string > thm list 
49914  32 
val lam_trans_from_atp_proof : string proof > string > string 
33 
val is_typed_helper_used_in_atp_proof : string proof > bool 

34 
val used_facts_in_atp_proof : 

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

36 
(string * stature) list 

37 
val used_facts_in_unsound_atp_proof : 

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

39 
string list option 

40 
val one_line_proof_text : int > one_line_params > string 

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

47 
structure Sledgehammer_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT = 

48 
struct 

49 

50 
open ATP_Util 

49914  51 
open ATP_Problem 
49883  52 
open ATP_Proof 
53 
open ATP_Problem_Generate 

54 
open ATP_Proof_Reconstruct 

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

55 
open Sledgehammer_Util 
49914  56 

57 
structure String_Redirect = ATP_Proof_Redirect( 

58 
type key = step_name 

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

60 
val string_of = fst) 

61 

49883  62 
open String_Redirect 
63 

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

64 

49914  65 
(** reconstructors **) 
66 

67 
datatype reconstructor = 

68 
Metis of string * string  

69 
SMT 

70 

71 
datatype play = 

72 
Played of reconstructor * Time.time  

73 
Trust_Playable of reconstructor * Time.time option  

74 
Failed_to_Play of reconstructor 

75 

76 
val smtN = "smt" 

77 

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

79 
metis_call type_enc lam_trans 

80 
 string_for_reconstructor SMT = smtN 

81 

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

82 
fun thms_of_name ctxt name = 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

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

84 
val lex = Keyword.get_lexicons 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

85 
val get = maps (Proof_Context.get_fact ctxt o fst) 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

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

87 
Source.of_string name 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

88 
> Symbol.source 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

89 
> Token.source {do_recover=SOME false} lex Position.start 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

90 
> Token.source_proper 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

91 
> Source.source Token.stopper (Parse_Spec.xthms1 >> get) NONE 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

92 
> Source.exhaust 
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

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

94 

49914  95 

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

97 

98 
fun find_first_in_list_vector vec key = 

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

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

101 

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

103 

104 
fun resolve_one_named_fact fact_names s = 

105 
case try (unprefix fact_prefix) s of 

106 
SOME s' => 

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

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

109 
end 

110 
 NONE => NONE 

111 
fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names) 

112 
fun is_fact fact_names = not o null o resolve_fact fact_names 

113 

114 
fun resolve_one_named_conjecture s = 

115 
case try (unprefix conjecture_prefix) s of 

116 
SOME s' => Int.fromString s' 

117 
 NONE => NONE 

118 

119 
val resolve_conjecture = map_filter resolve_one_named_conjecture 

120 
val is_conjecture = not o null o resolve_conjecture 

121 

122 
val ascii_of_lam_fact_prefix = ascii_of lam_fact_prefix 

123 

124 
(* overapproximation (good enough) *) 

125 
fun is_lam_lifted s = 

126 
String.isPrefix fact_prefix s andalso 

127 
String.isSubstring ascii_of_lam_fact_prefix s 

128 

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

130 

131 
fun is_axiom_used_in_proof pred = 

132 
exists (fn Inference_Step ((_, ss), _, _, []) => exists pred ss  _ => false) 

133 

134 
fun lam_trans_from_atp_proof atp_proof default = 

135 
case (is_axiom_used_in_proof is_combinator_def atp_proof, 

136 
is_axiom_used_in_proof is_lam_lifted atp_proof) of 

137 
(false, false) => default 

138 
 (false, true) => liftingN 

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

140 
 (true, _) => combsN 

141 

142 
val is_typed_helper_name = 

143 
String.isPrefix helper_prefix andf String.isSuffix typed_helper_suffix 

144 
fun is_typed_helper_used_in_atp_proof atp_proof = 

145 
is_axiom_used_in_proof is_typed_helper_name atp_proof 

146 

147 
fun add_non_rec_defs fact_names accum = 

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

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

150 
facts') 

151 
accum fact_names 

152 

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

154 
val isa_short_ext = Long_Name.base_name isa_ext 

155 

156 
fun ext_name ctxt = 

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

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

159 
isa_short_ext 

160 
else 

161 
isa_ext 

162 

163 
val leo2_ext = "extcnf_equal_neg" 

164 
val leo2_unfold_def = "unfold_def" 

165 

166 
fun add_fact ctxt fact_names (Inference_Step ((_, ss), _, rule, deps)) = 

167 
(if rule = leo2_ext then 

168 
insert (op =) (ext_name ctxt, (Global, General)) 

169 
else if rule = leo2_unfold_def then 

170 
(* LEO 1.3.3 does not record definitions properly, leading to missing 

171 
dependencies in the TSTP proof. Remove the next line once this is 

172 
fixed. *) 

173 
add_non_rec_defs fact_names 

174 
else if rule = satallax_coreN then 

175 
(fn [] => 

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

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

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

179 
 facts => facts) 

180 
else 

181 
I) 

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

183 
else I) 

184 
 add_fact _ _ _ = I 

185 

186 
fun used_facts_in_atp_proof ctxt fact_names atp_proof = 

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

188 
else fold (add_fact ctxt fact_names) atp_proof [] 

189 

190 
fun used_facts_in_unsound_atp_proof _ _ [] = NONE 

191 
 used_facts_in_unsound_atp_proof ctxt fact_names atp_proof = 

192 
let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in 

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

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

195 
SOME (map fst used_facts) 

196 
else 

197 
NONE 

198 
end 

199 

200 

201 
(** oneliner reconstructor proofs **) 

202 

203 
fun string_for_label (s, num) = s ^ string_of_int num 

204 

205 
fun show_time NONE = "" 

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

207 

208 
fun unusing_chained_facts _ 0 = "" 

209 
 unusing_chained_facts used_chaineds num_chained = 

210 
if length used_chaineds = num_chained then "" 

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

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

213 

214 
fun apply_on_subgoal _ 1 = "by " 

215 
 apply_on_subgoal 1 _ = "apply " 

216 
 apply_on_subgoal i n = 

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

218 

219 
fun using_labels [] = "" 

220 
 using_labels ls = 

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

222 

223 
fun command_call name [] = 

224 
name > not (Lexicon.is_identifier name) ? enclose "(" ")" 

225 
 command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")" 

226 

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

228 
unusing_chained_facts used_chaineds num_chained ^ 

229 
using_labels ls ^ apply_on_subgoal i n ^ 

230 
command_call (string_for_reconstructor reconstr) ss 

231 

232 
fun try_command_line banner time command = 

233 
banner ^ ": " ^ Markup.markup Isabelle_Markup.sendback command ^ 

234 
show_time time ^ "." 

235 

236 
fun minimize_line _ [] = "" 

237 
 minimize_line minimize_command ss = 

238 
case minimize_command ss of 

239 
"" => "" 

240 
 command => 

241 
"\nTo minimize: " ^ Markup.markup Isabelle_Markup.sendback command ^ "." 

242 

243 
fun split_used_facts facts = 

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

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

246 

247 
type minimize_command = string list > string 

248 
type one_line_params = 

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

250 

251 
fun one_line_proof_text num_chained 

252 
(preplay, banner, used_facts, minimize_command, subgoal, 

253 
subgoal_count) = 

254 
let 

255 
val (chained, extra) = split_used_facts used_facts 

256 
val (failed, reconstr, ext_time) = 

257 
case preplay of 

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

259 
 Trust_Playable (reconstr, time) => 

260 
(false, reconstr, 

261 
case time of 

262 
NONE => NONE 

263 
 SOME time => 

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

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

266 
val try_line = 

267 
([], map fst extra) 

268 
> reconstructor_command reconstr subgoal subgoal_count (map fst chained) 

269 
num_chained 

270 
> (if failed then 

271 
enclose "Oneline proof reconstruction failed: " 

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

273 
\solve this.)" 

274 
else 

275 
try_command_line banner ext_time) 

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

277 

278 

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

280 

281 
type label = string * int 

282 
type facts = label list * string list 

283 

284 
datatype isar_qualifier = Show  Then  Moreover  Ultimately 

285 

286 
datatype isar_step = 

287 
Fix of (string * typ) list  

288 
Let of term * term  

289 
Assume of label * term  

290 
Prove of isar_qualifier list * label * term * byline 

291 
and byline = 

292 
By_Metis of facts  

293 
Case_Split of isar_step list list * facts 

294 

295 
val assum_prefix = "a" 

296 
val have_prefix = "f" 

297 
val raw_prefix = "x" 

298 

299 
fun raw_label_for_name (num, ss) = 

300 
case resolve_conjecture ss of 

301 
[j] => (conjecture_prefix, j) 

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

303 

304 
fun add_fact_from_dependency fact_names (name as (_, ss)) = 

305 
if is_fact fact_names ss then 

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

307 
else 

308 
apfst (insert (op =) (raw_label_for_name name)) 

309 

310 
fun repair_name "$true" = "c_True" 

311 
 repair_name "$false" = "c_False" 

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

313 
 repair_name s = 

314 
if is_tptp_equal s orelse 

315 
(* seen in Vampire proofs *) 

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

317 
tptp_equal 

318 
else 

319 
s 

320 

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

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

323 

324 
fun infer_formula_types ctxt = 

325 
Type.constraint HOLogic.boolT 

326 
#> Syntax.check_term 

327 
(Proof_Context.set_mode Proof_Context.mode_schematic ctxt) 

328 

329 
val combinator_table = 

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

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

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

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

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

335 

336 
fun uncombine_term thy = 

337 
let 

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

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

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

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

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

343 
> Logic.dest_equals > snd 

344 
 NONE => t) 

345 
 aux t = t 

346 
in aux end 

347 

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

349 
let 

350 
val thy = Proof_Context.theory_of ctxt 

351 
val t1 = prop_from_atp ctxt true sym_tab phi1 

352 
val vars = snd (strip_comb t1) 

353 
val frees = map unvarify_term vars 

354 
val unvarify_args = subst_atomic (vars ~~ frees) 

355 
val t2 = prop_from_atp ctxt true sym_tab phi2 

356 
val (t1, t2) = 

357 
HOLogic.eq_const HOLogic.typeT $ t1 $ t2 

358 
> unvarify_args > uncombine_term thy > infer_formula_types ctxt 

359 
> HOLogic.dest_eq 

360 
in 

361 
(Definition_Step (name, t1, t2), 

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

363 
end 

364 
 decode_line sym_tab (Inference_Step (name, u, rule, deps)) ctxt = 

365 
let 

366 
val thy = Proof_Context.theory_of ctxt 

367 
val t = u > prop_from_atp ctxt true sym_tab 

368 
> uncombine_term thy > infer_formula_types ctxt 

369 
in 

370 
(Inference_Step (name, t, rule, deps), 

371 
fold Variable.declare_term (Misc_Legacy.term_frees t) ctxt) 

372 
end 

373 
fun decode_lines ctxt sym_tab lines = 

374 
fst (fold_map (decode_line sym_tab) lines ctxt) 

375 

376 
fun replace_one_dependency (old, new) dep = 

377 
if is_same_atp_step dep old then new else [dep] 

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

379 
 replace_dependencies_in_line p (Inference_Step (name, t, rule, deps)) = 

380 
Inference_Step (name, t, rule, 

381 
fold (union (op =) o replace_one_dependency p) deps []) 

382 

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

384 
clsarity). *) 

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

386 

387 
fun is_same_inference _ (Definition_Step _) = false 

388 
 is_same_inference t (Inference_Step (_, t', _, _)) = t aconv t' 

389 

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

391 
they differ only in type information.*) 

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

393 
 add_line fact_names (Inference_Step (name as (_, ss), t, rule, [])) lines = 

394 
(* No dependencies: fact, conjecture, or (for Vampire) internal facts or 

395 
definitions. *) 

396 
if is_fact fact_names ss then 

397 
(* Facts are not proof lines. *) 

398 
if is_only_type_information t then 

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

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

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

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

403 
 (pre, Inference_Step (name', _, _, _) :: post) => 

404 
pre @ map (replace_dependencies_in_line (name', [name])) post 

405 
 _ => raise Fail "unexpected inference" 

406 
else if is_conjecture ss then 

407 
Inference_Step (name, t, rule, []) :: lines 

408 
else 

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

410 
 add_line _ (Inference_Step (name, t, rule, deps)) lines = 

411 
(* Type information will be deleted later; skip repetition test. *) 

412 
if is_only_type_information t then 

413 
Inference_Step (name, t, rule, deps) :: lines 

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

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

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

417 
types? *) 

418 
(_, []) => Inference_Step (name, t, rule, deps) :: lines 

419 
 (pre, Inference_Step (name', t', rule, _) :: post) => 

420 
Inference_Step (name, t', rule, deps) :: 

421 
pre @ map (replace_dependencies_in_line (name', [name])) post 

422 
 _ => raise Fail "unexpected inference" 

423 

424 
val waldmeister_conjecture_num = "1.0.0.0" 

425 

426 
val repair_waldmeister_endgame = 

427 
let 

428 
fun do_tail (Inference_Step (name, t, rule, deps)) = 

429 
Inference_Step (name, s_not t, rule, deps) 

430 
 do_tail line = line 

431 
fun do_body [] = [] 

432 
 do_body ((line as Inference_Step ((num, _), _, _, _)) :: lines) = 

433 
if num = waldmeister_conjecture_num then map do_tail (line :: lines) 

434 
else line :: do_body lines 

435 
 do_body (line :: lines) = line :: do_body lines 

436 
in do_body end 

437 

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

439 
fun add_nontrivial_line (line as Inference_Step (name, t, _, [])) lines = 

440 
if is_only_type_information t then delete_dependency name lines 

441 
else line :: lines 

442 
 add_nontrivial_line line lines = line :: lines 

443 
and delete_dependency name lines = 

444 
fold_rev add_nontrivial_line 

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

446 

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

448 
offending lines often does the trick. *) 

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

450 
 is_bad_free _ _ = false 

451 

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

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

454 
 add_desired_line fact_names frees 
49914  455 
(Inference_Step (name as (_, ss), t, rule, deps)) (j, lines) = 
456 
(j + 1, 

457 
if is_fact fact_names ss orelse 

458 
is_conjecture ss orelse 

459 
(* the last line must be kept *) 

460 
j = 0 orelse 

461 
(not (is_only_type_information t) andalso 

462 
null (Term.add_tvars t []) andalso 

463 
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

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

467 
Inference_Step (name, t, rule, deps) :: lines (* keep line *) 

468 
else 

469 
map (replace_dependencies_in_line (name, deps)) lines) (* drop line *) 

470 

49883  471 
(** Type annotations **) 
472 

473 
fun post_traverse_term_type' f _ (t as Const (_, T)) s = f t T s 

474 
 post_traverse_term_type' f _ (t as Free (_, T)) s = f t T s 

475 
 post_traverse_term_type' f _ (t as Var (_, T)) s = f t T s 

476 
 post_traverse_term_type' f env (t as Bound i) s = f t (nth env i) s 

477 
 post_traverse_term_type' f env (Abs (x, T1, b)) s = 

478 
let 

479 
val ((b', s'), T2) = post_traverse_term_type' f (T1 :: env) b s 

480 
in f (Abs (x, T1, b')) (T1 > T2) s' end 

481 
 post_traverse_term_type' f env (u $ v) s = 

482 
let 

483 
val ((u', s'), Type (_, [_, T])) = post_traverse_term_type' f env u s 

484 
val ((v', s''), _) = post_traverse_term_type' f env v s' 

485 
in f (u' $ v') T s'' end 

486 

487 
fun post_traverse_term_type f s t = 

488 
post_traverse_term_type' (fn t => fn T => fn s => (f t T s, T)) [] t s > fst 

489 
fun post_fold_term_type f s t = 

490 
post_traverse_term_type (fn t => fn T => fn s => (t, f t T s)) s t > snd 

491 

492 
(* Data structures, orders *) 

493 
val cost_ord = prod_ord int_ord (prod_ord int_ord int_ord) 

494 

495 
structure Var_Set_Tab = Table( 

496 
type key = indexname list 

497 
val ord = list_ord Term_Ord.fast_indexname_ord) 

498 

499 
(* (1) Generalize Types *) 

500 
fun generalize_types ctxt t = 

501 
t > map_types (fn _ => dummyT) 

502 
> Syntax.check_term 

503 
(Proof_Context.set_mode Proof_Context.mode_pattern ctxt) 

504 

505 
(* (2) Typingspot Table *) 

506 
local 

507 
fun key_of_atype (TVar (idxn, _)) = 

508 
Ord_List.insert Term_Ord.fast_indexname_ord idxn 

509 
 key_of_atype _ = I 

510 
fun key_of_type T = fold_atyps key_of_atype T [] 

511 
fun update_tab t T (tab, pos) = 

512 
(case key_of_type T of 

513 
[] => tab 

514 
 key => 

515 
let val cost = (size_of_typ T, (size_of_term t, pos)) in 

516 
case Var_Set_Tab.lookup tab key of 

517 
NONE => Var_Set_Tab.update_new (key, cost) tab 

518 
 SOME old_cost => 

519 
(case cost_ord (cost, old_cost) of 

520 
LESS => Var_Set_Tab.update (key, cost) tab 

521 
 _ => tab) 

522 
end, 

523 
pos + 1) 

524 
in 

525 
val typing_spot_table = 

526 
post_fold_term_type update_tab (Var_Set_Tab.empty, 0) #> fst 

527 
end 

528 

529 
(* (3) ReverseGreedy *) 

530 
fun reverse_greedy typing_spot_tab = 

531 
let 

532 
fun update_count z = 

533 
fold (fn tvar => fn tab => 

534 
let val c = Vartab.lookup tab tvar > the_default 0 in 

535 
Vartab.update (tvar, c + z) tab 

536 
end) 

537 
fun superfluous tcount = 

538 
forall (fn tvar => the (Vartab.lookup tcount tvar) > 1) 

539 
fun drop_superfluous (tvars, (_, (_, spot))) (spots, tcount) = 

540 
if superfluous tcount tvars then (spots, update_count ~1 tvars tcount) 

541 
else (spot :: spots, tcount) 

542 
val (typing_spots, tvar_count_tab) = 

543 
Var_Set_Tab.fold 

544 
(fn kv as (k, _) => apfst (cons kv) #> apsnd (update_count 1 k)) 

545 
typing_spot_tab ([], Vartab.empty) 

546 
>> sort_distinct (rev_order o cost_ord o pairself snd) 

547 
in fold drop_superfluous typing_spots ([], tvar_count_tab) > fst end 

548 

549 
(* (4) Introduce Annotations *) 

550 
fun introduce_annotations thy spots t t' = 

551 
let 

552 
val get_types = post_fold_term_type (K cons) [] 

553 
fun match_types tp = 

554 
fold (Sign.typ_match thy) (op ~~ (pairself get_types tp)) Vartab.empty 

555 
fun unica' b x [] = if b then [x] else [] 

556 
 unica' b x (y :: ys) = 

557 
if x = y then unica' false x ys 

558 
else unica' true y ys > b ? cons x 

559 
fun unica ord xs = 

560 
case sort ord xs of x :: ys => unica' true x ys  [] => [] 

561 
val add_all_tfree_namesT = fold_atyps (fn TFree (x, _) => cons x  _ => I) 

562 
fun erase_unica_tfrees env = 

563 
let 

564 
val unica = 

565 
Vartab.fold (add_all_tfree_namesT o snd o snd) env [] 

566 
> unica fast_string_ord 

567 
val erase_unica = map_atyps 

568 
(fn T as TFree (s, _) => 

569 
if Ord_List.member fast_string_ord unica s then dummyT else T 

570 
 T => T) 

571 
in Vartab.map (K (apsnd erase_unica)) env end 

572 
val env = match_types (t', t) > erase_unica_tfrees 

573 
fun get_annot env (TFree _) = (false, (env, dummyT)) 

574 
 get_annot env (T as TVar (v, S)) = 

575 
let val T' = Envir.subst_type env T in 

576 
if T' = dummyT then (false, (env, dummyT)) 

577 
else (true, (Vartab.update (v, (S, dummyT)) env, T')) 

578 
end 

579 
 get_annot env (Type (S, Ts)) = 

580 
(case fold_rev (fn T => fn (b, (env, Ts)) => 

581 
let 

582 
val (b', (env', T)) = get_annot env T 

583 
in (b orelse b', (env', T :: Ts)) end) 

584 
Ts (false, (env, [])) of 

585 
(true, (env', Ts)) => (true, (env', Type (S, Ts))) 

586 
 (false, (env', _)) => (false, (env', dummyT))) 

587 
fun post1 _ T (env, cp, ps as p :: ps', annots) = 

588 
if p <> cp then 

589 
(env, cp + 1, ps, annots) 

590 
else 

591 
let val (_, (env', T')) = get_annot env T in 

592 
(env', cp + 1, ps', (p, T') :: annots) 

593 
end 

594 
 post1 _ _ accum = accum 

595 
val (_, _, _, annots) = post_fold_term_type post1 (env, 0, spots, []) t' 

596 
fun post2 t _ (cp, annots as (p, T) :: annots') = 

597 
if p <> cp then (t, (cp + 1, annots)) 

598 
else (Type.constraint T t, (cp + 1, annots')) 

599 
 post2 t _ x = (t, x) 

600 
in post_traverse_term_type post2 (0, rev annots) t > fst end 

601 

602 
(* (5) Annotate *) 

603 
fun annotate_types ctxt t = 

604 
let 

605 
val thy = Proof_Context.theory_of ctxt 

606 
val t' = generalize_types ctxt t 

607 
val typing_spots = 

608 
t' > typing_spot_table 

609 
> reverse_greedy 

610 
> sort int_ord 

611 
in introduce_annotations thy typing_spots t t' end 

612 

49914  613 
val indent_size = 2 
614 
val no_label = ("", ~1) 

615 

49883  616 
fun string_for_proof ctxt type_enc lam_trans i n = 
617 
let 

618 
fun fix_print_mode f x = 

619 
Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN) 

620 
(print_mode_value ())) f x 

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

622 
fun do_free (s, T) = 

623 
maybe_quote s ^ " :: " ^ 

624 
maybe_quote (fix_print_mode (Syntax.string_of_typ ctxt) T) 

625 
fun do_label l = if l = no_label then "" else string_for_label l ^ ": " 

626 
fun do_have qs = 

627 
(if member (op =) qs Moreover then "moreover " else "") ^ 

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

629 
(if member (op =) qs Then then 

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

631 
else 

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

633 
val do_term = 

634 
maybe_quote o fix_print_mode (Syntax.string_of_term ctxt) 

635 
o annotate_types ctxt 

636 
val reconstr = Metis (type_enc, lam_trans) 

49921  637 
fun do_facts ind (ls, ss) = 
638 
"\n" ^ do_indent (ind + 1) ^ 

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

641 
ss > sort_distinct string_ord) 

642 
and do_step ind (Fix xs) = 

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

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

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

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

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

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

649 
do_indent ind ^ do_have qs ^ " " ^ 

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

653 
proofs) ^ 

49921  654 
do_indent ind ^ do_have qs ^ " " ^ do_label l ^ do_term t ^ 
655 
do_facts ind facts ^ "\n" 

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

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

659 
String.extract (s, ind * indent_size, 

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

661 
suffix ^ "\n" 

662 
end 

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

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

665 
directly. *) 

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

667 
 do_proof proof = 

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

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

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

671 
in do_proof end 

672 

49914  673 
(* FIXME: Still needed? Try with SPASS proofs perhaps. *) 
674 
val kill_duplicate_assumptions_in_proof = 

675 
let 

676 
fun relabel_facts subst = 

677 
apfst (map (fn l => AList.lookup (op =) subst l > the_default l)) 

678 
fun do_step (step as Assume (l, t)) (proof, subst, assums) = 

679 
(case AList.lookup (op aconv) assums t of 

680 
SOME l' => (proof, (l, l') :: subst, assums) 

681 
 NONE => (step :: proof, subst, (t, l) :: assums)) 

682 
 do_step (Prove (qs, l, t, by)) (proof, subst, assums) = 

683 
(Prove (qs, l, t, 

684 
case by of 

685 
By_Metis facts => By_Metis (relabel_facts subst facts) 

686 
 Case_Split (proofs, facts) => 

687 
Case_Split (map do_proof proofs, 

688 
relabel_facts subst facts)) :: 

689 
proof, subst, assums) 

690 
 do_step step (proof, subst, assums) = (step :: proof, subst, assums) 

691 
and do_proof proof = fold do_step proof ([], [], []) > #1 > rev 

692 
in do_proof end 

693 

694 
fun used_labels_of_step (Prove (_, _, _, by)) = 

695 
(case by of 

696 
By_Metis (ls, _) => ls 

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

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

699 
 used_labels_of_step _ = [] 

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

701 

702 
fun kill_useless_labels_in_proof proof = 

703 
let 

704 
val used_ls = used_labels_of proof 

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

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

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

708 
Prove (qs, do_label l, t, 

709 
case by of 

710 
Case_Split (proofs, facts) => 

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

712 
 _ => by) 

713 
 do_step step = step 

714 
in map do_step proof end 

715 

716 
fun prefix_for_depth n = replicate_string (n + 1) 

717 

718 
val relabel_proof = 

719 
let 

720 
fun aux _ _ _ [] = [] 

721 
 aux subst depth (next_assum, next_fact) (Assume (l, t) :: proof) = 

722 
if l = no_label then 

723 
Assume (l, t) :: aux subst depth (next_assum, next_fact) proof 

724 
else 

725 
let val l' = (prefix_for_depth depth assum_prefix, next_assum) in 

726 
Assume (l', t) :: 

727 
aux ((l, l') :: subst) depth (next_assum + 1, next_fact) proof 

728 
end 

729 
 aux subst depth (next_assum, next_fact) 

730 
(Prove (qs, l, t, by) :: proof) = 

731 
let 

732 
val (l', subst, next_fact) = 

733 
if l = no_label then 

734 
(l, subst, next_fact) 

735 
else 

736 
let 

737 
val l' = (prefix_for_depth depth have_prefix, next_fact) 

738 
in (l', (l, l') :: subst, next_fact + 1) end 

739 
val relabel_facts = 

740 
apfst (maps (the_list o AList.lookup (op =) subst)) 

741 
val by = 

742 
case by of 

743 
By_Metis facts => By_Metis (relabel_facts facts) 

744 
 Case_Split (proofs, facts) => 

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

746 
relabel_facts facts) 

747 
in 

748 
Prove (qs, l', t, by) :: aux subst depth (next_assum, next_fact) proof 

749 
end 

750 
 aux subst depth nextp (step :: proof) = 

751 
step :: aux subst depth nextp proof 

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

753 

49917  754 
val merge_timeout_slack = 1.2 
755 

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

756 
fun shrink_locally ctxt type_enc lam_trans isar_shrinkage proof = 
49883  757 
let 
758 
(* Merging spots, greedy algorithm *) 

759 
fun cost (Prove (_, _ , t, _)) = Term.size_of_term t 

760 
 cost _ = ~1 

49913  761 
fun can_merge (Prove (_, lbl, _, By_Metis _)) 
762 
(Prove (_, _, _, By_Metis _)) = 

763 
(lbl = no_label) 

49883  764 
 can_merge _ _ = false 
765 
val merge_spots = 

49913  766 
fold_index (fn (i, s2) => fn (s1, pile) => 
767 
(s2, pile > can_merge s1 s2 ? cons (i, cost s1))) 

49883  768 
(tl proof) (hd proof, []) 
49917  769 
> snd > sort (rev_order o int_ord o pairself snd) > map fst 
49883  770 

49917  771 
(* Enrich context with local facts *) 
49883  772 
val thy = Proof_Context.theory_of ctxt 
49915  773 
fun sorry t = Skip_Proof.make_thm thy (HOLogic.mk_Trueprop t) 
49883  774 
fun enrich_ctxt' (Prove (_, lbl, t, _)) ctxt = 
49913  775 
ctxt > lbl <> no_label 
776 
? Proof_Context.put_thms false (string_for_label lbl, SOME [sorry t]) 

49883  777 
 enrich_ctxt' _ ctxt = ctxt 
778 
val rich_ctxt = fold enrich_ctxt' proof ctxt 

779 

780 
(* Timing *) 

781 
fun take_time tac arg = 

49917  782 
let val timing = Timing.start () in 
783 
(tac arg; Timing.result timing > #cpu) 

49883  784 
end 
785 
fun try_metis (Prove (qs, _, t, By_Metis fact_names)) s0 = 

786 
let 

787 
fun thmify (Prove (_, _, t, _)) = sorry t 

49913  788 
val facts = 
789 
fact_names 

49915  790 
>> map string_for_label > op @ 
49916
412346127bfa
fixed theorem lookup code in Isar proof reconstruction
blanchet
parents:
49915
diff
changeset

791 
> map (the_single o thms_of_name rich_ctxt) 
49913  792 
> (if member (op =) qs Then then cons (the s0 > thmify) else I) 
49915  793 
val goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop t) 
49883  794 
fun tac {context = ctxt, prems = _} = 
795 
Metis_Tactic.metis_tac [type_enc] lam_trans ctxt facts 1 

796 
in 

797 
take_time (fn () => goal tac) 

798 
end 

799 

800 
(* Merging *) 

801 
fun merge (Prove (qs1, _, _, By_Metis (ls1, ss1))) 

802 
(Prove (qs2, lbl , t, By_Metis (ls2, ss2))) = 

803 
let 

49913  804 
val qs = 
805 
inter (op =) qs1 qs2 (* FIXME: Is this correct? *) 

806 
> member (op =) (union (op =) qs1 qs2) Ultimately ? cons Ultimately 

807 
> member (op =) qs2 Show ? cons Show 

808 
in Prove (qs, lbl, t, By_Metis (ls1 @ ls2, ss1 @ ss2)) end 

49883  809 
fun try_merge proof i = 
810 
let 

811 
val (front, s0, s1, s2, tail) = 

812 
case (proof, i) of 

49913  813 
((s1 :: s2 :: proof), 0) => ([], NONE, s1, s2, proof) 
814 
 _ => 

815 
let val (front, s0 :: s1 :: s2 :: tail) = chop (i  1) proof in 

816 
(front, SOME s0, s1, s2, tail) 

817 
end 

49883  818 
val s12 = merge s1 s2 
819 
val t1 = try_metis s1 s0 () 

820 
val t2 = try_metis s2 (SOME s1) () 

49917  821 
val timeout = 
49936  822 
Time.+ (t1, t2) > Time.toReal > curry Real.* merge_timeout_slack 
49917  823 
> Time.fromReal 
49883  824 
in 
49917  825 
(TimeLimit.timeLimit timeout (try_metis s12 s0) (); 
49915  826 
SOME (front @ (the_list s0 @ s12 :: tail))) 
49883  827 
handle _ => NONE 
828 
end 

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

829 
fun spill_shrinkage shrinkage = isar_shrinkage + shrinkage  1.0 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

830 
fun merge_steps _ proof [] = proof 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

831 
 merge_steps shrinkage proof (i :: is) = 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

832 
if shrinkage < 1.5 then 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

833 
merge_steps (spill_shrinkage shrinkage) proof is 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

834 
else case try_merge proof i of 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

835 
NONE => merge_steps (spill_shrinkage shrinkage) proof is 
49913  836 
 SOME proof' => 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

837 
merge_steps (shrinkage  1.0) proof' 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

838 
(map (fn j => if j > i then j  1 else j) is) 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

839 
in merge_steps isar_shrinkage proof merge_spots end 
49883  840 

49914  841 
type isar_params = 
49918
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

842 
bool * bool * real * string Symtab.table * (string * stature) list vector 
49914  843 
* int Symtab.table * string proof * thm 
844 

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

845 
fun isar_proof_text ctxt isar_proofs 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

846 
(debug, verbose, isar_shrinkage, pool, fact_names, sym_tab, atp_proof, goal) 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

847 
(one_line_params as (_, _, _, _, subgoal, subgoal_count)) = 
49883  848 
let 
849 
val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal 

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

851 
val one_line_proof = one_line_proof_text 0 one_line_params 

852 
val type_enc = 

853 
if is_typed_helper_used_in_atp_proof atp_proof then full_typesN 

854 
else partial_typesN 

855 
val lam_trans = lam_trans_from_atp_proof atp_proof metis_default_lam_trans 

856 

857 
fun isar_proof_of () = 

858 
let 

859 
val atp_proof = 

860 
atp_proof 

861 
> clean_up_atp_proof_dependencies 

862 
> nasty_atp_proof pool 

863 
> map_term_names_in_atp_proof repair_name 

864 
> decode_lines ctxt sym_tab 

865 
> rpair [] > fold_rev (add_line fact_names) 

866 
> repair_waldmeister_endgame 

867 
> rpair [] > fold_rev add_nontrivial_line 

868 
> rpair (0, []) 

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

869 
> fold_rev (add_desired_line fact_names frees) 
49883  870 
> snd 
871 
val conj_name = conjecture_prefix ^ string_of_int (length hyp_ts) 

872 
val conjs = 

873 
atp_proof 

874 
> map_filter (fn Inference_Step (name as (_, ss), _, _, []) => 

875 
if member (op =) ss conj_name then SOME name else NONE 

876 
 _ => NONE) 

877 
fun dep_of_step (Definition_Step _) = NONE 

878 
 dep_of_step (Inference_Step (name, _, _, from)) = SOME (from, name) 

879 
val ref_graph = atp_proof > map_filter dep_of_step > make_ref_graph 

880 
val axioms = axioms_of_ref_graph ref_graph conjs 

881 
val tainted = tainted_atoms_of_ref_graph ref_graph conjs 

882 
val props = 

883 
Symtab.empty 

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

885 
 Inference_Step ((s, _), t, _, _) => 

886 
Symtab.update_new (s, 

887 
t > fold forall_of (map Var (Term.add_vars t [])) 

888 
> member (op = o apsnd fst) tainted s ? s_not)) 

889 
atp_proof 

890 
fun prop_of_clause c = 

891 
fold (curry s_disj) (map_filter (Symtab.lookup props o fst) c) 

892 
@{term False} 

893 
fun label_of_clause [name] = raw_label_for_name name 

894 
 label_of_clause c = (space_implode "___" (map fst c), 0) 

895 
fun maybe_show outer c = 

896 
(outer andalso length c = 1 andalso subset (op =) (c, conjs)) 

897 
? cons Show 

898 
fun do_have outer qs (gamma, c) = 

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

900 
By_Metis (fold (add_fact_from_dependency fact_names 

901 
o the_single) gamma ([], []))) 

902 
fun do_inf outer (Have z) = do_have outer [] z 

903 
 do_inf outer (Hence z) = do_have outer [Then] z 

904 
 do_inf outer (Cases cases) = 

905 
let val c = succedent_of_cases cases in 

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

907 
prop_of_clause c, 

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

909 
end 

910 
and do_case outer (c, infs) = 

911 
Assume (label_of_clause c, prop_of_clause c) :: 

912 
map (do_inf outer) infs 

913 
val isar_proof = 

914 
(if null params then [] else [Fix params]) @ 

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

915 
(ref_graph 
49883  916 
> redirect_graph axioms tainted 
917 
> chain_direct_proof 

918 
> map (do_inf true) 

919 
> kill_duplicate_assumptions_in_proof 

920 
> kill_useless_labels_in_proof 

921 
> relabel_proof 

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

922 
> shrink_locally ctxt type_enc lam_trans 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

923 
(if isar_proofs then isar_shrinkage else 1000.0)) 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

924 
val num_steps = length isar_proof 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

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

926 
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

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

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

931 
if isar_proofs then 
49883  932 
"\nNo structured proof available (proof too short)." 
933 
else 

934 
"" 

935 
 _ => 

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

936 
"\n\n" ^ 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

937 
(if isar_proofs then 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

938 
"Structured proof" ^ 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

939 
(if verbose then 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

940 
" (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^ 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

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

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

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

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

945 
"Perhaps this will work") ^ 
cf441f4a358b
renamed Isarproof related options + changed semantics of Isar shrinking
blanchet
parents:
49917
diff
changeset

946 
":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text 
49883  947 
end 
948 
val isar_proof = 

949 
if debug then 

950 
isar_proof_of () 

951 
else case try isar_proof_of () of 

952 
SOME s => s 

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

953 
 NONE => if isar_proofs then 
49883  954 
"\nWarning: The Isar proof construction failed." 
955 
else 

956 
"" 

957 
in one_line_proof ^ isar_proof end 

958 

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

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

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

962 
isar_proof_text ctxt isar_proofs isar_params 
49883  963 
else 
964 
one_line_proof_text num_chained) one_line_params 

965 

966 
end; 