author  wenzelm 
Fri, 02 Jul 1999 15:05:16 +0200  
changeset 6887  12b5fb35a688 
parent 6876  4ae9c47f2b6b 
child 6891  7bb02d03035d 
permissions  rwrr 
5820  1 
(* Title: Pure/Isar/proof.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Proof states and methods. 

6 
*) 

7 

8 
signature PROOF = 

9 
sig 

10 
type context 

11 
type state 

12 
exception STATE of string * state 

6871  13 
val check_result: string > state > 'a Seq.seq > 'a Seq.seq 
5820  14 
val context_of: state > context 
15 
val theory_of: state > theory 

16 
val sign_of: state > Sign.sg 

6091  17 
val the_facts: state > thm list 
6776  18 
val the_fact: state > thm 
6091  19 
val goal_facts: (state > thm list) > state > state 
5820  20 
val use_facts: state > state 
21 
val reset_facts: state > state 

22 
val assert_backward: state > state 

23 
val enter_forward: state > state 

6529  24 
val verbose: bool ref 
5820  25 
val print_state: state > unit 
6776  26 
val level: state > int 
5820  27 
type method 
6848  28 
val method: (thm list > tactic) > method 
5820  29 
val refine: (context > method) > state > state Seq.seq 
30 
val bind: (indexname * string) list > state > state 

31 
val bind_i: (indexname * term) list > state > state 

5936  32 
val match_bind: (string list * string) list > state > state 
33 
val match_bind_i: (term list * term) list > state > state 

6876  34 
val have_thmss: thm list > string > context attribute list > 
6091  35 
(thm list * context attribute list) list > state > state 
6876  36 
val simple_have_thms: string > thm list > state > state 
6848  37 
val assume: (int > tactic) > string > context attribute list > (string * string list) list 
38 
> state > state 

39 
val assume_i: (int > tactic) > string > context attribute list > (term * term list) list 

40 
> state > state 

5820  41 
val fix: (string * string option) list > state > state 
42 
val fix_i: (string * typ) list > state > state 

5936  43 
val theorem: bstring > theory attribute list > string * string list > theory > state 
44 
val theorem_i: bstring > theory attribute list > term * term list > theory > state 

45 
val lemma: bstring > theory attribute list > string * string list > theory > state 

46 
val lemma_i: bstring > theory attribute list > term * term list > theory > state 

5820  47 
val chain: state > state 
6091  48 
val from_facts: thm list > state > state 
5936  49 
val show: string > context attribute list > string * string list > state > state 
50 
val show_i: string > context attribute list > term * term list > state > state 

51 
val have: string > context attribute list > string * string list > state > state 

52 
val have_i: string > context attribute list > term * term list > state > state 

5820  53 
val begin_block: state > state 
54 
val next_block: state > state 

6404  55 
val end_block: state > state 
56 
val at_bottom: state > bool 

6731  57 
val local_qed: (state > state Seq.seq) > ({kind: string, name: string, thm: thm} > unit) 
58 
> state > state Seq.seq 

6404  59 
val global_qed: (state > state Seq.seq) > bstring option 
6871  60 
> theory attribute list option > state > (theory * {kind: string, name: string, thm: thm}) Seq.seq 
5820  61 
end; 
62 

63 
signature PROOF_PRIVATE = 

64 
sig 

65 
include PROOF 

66 
val put_data: Object.kind > ('a > Object.T) > 'a > state > state 

67 
end; 

68 

69 
structure Proof: PROOF_PRIVATE = 

70 
struct 

71 

72 

73 
(** proof state **) 

74 

75 
type context = ProofContext.context; 

76 

77 

78 
(* type goal *) 

79 

80 
datatype kind = 

81 
Theorem of theory attribute list  (*toplevel theorem*) 

82 
Lemma of theory attribute list  (*toplevel lemma*) 

83 
Goal of context attribute list  (*intermediate result, solving subgoal*) 

84 
Aux of context attribute list ; (*intermediate result*) 

85 

86 
val kind_name = 

6001  87 
fn Theorem _ => "theorem"  Lemma _ => "lemma"  Goal _ => "show"  Aux _ => "have"; 
5820  88 

89 
type goal = 

6848  90 
(kind * (*result kind*) 
91 
string * (*result name*) 

92 
cterm list * (*result assumptions*) 

93 
(int > tactic) list * (*tactics to solve result assumptions*) 

94 
term) * (*result statement*) 

95 
(thm list * (*use facts*) 

96 
thm); (*goal: subgoals ==> statement*) 

5820  97 

98 

99 
(* type mode *) 

100 

101 
datatype mode = Forward  ForwardChain  Backward; 

102 

103 
val mode_name = 

6798  104 
enclose "`" "'" o 
105 
(fn Forward => "state"  ForwardChain => "chain"  Backward => "prove"); 

5820  106 

107 

108 
(* type node *) 

109 

110 
type node = 

111 
{context: context, 

6091  112 
facts: thm list option, 
5820  113 
mode: mode, 
114 
goal: goal option}; 

115 

116 
fun make_node (context, facts, mode, goal) = 

117 
{context = context, facts = facts, mode = mode, goal = goal}: node; 

118 

119 

120 
(* datatype state *) 

121 

122 
datatype state = 

123 
State of 

124 
node * (*current*) 

125 
node list; (*parents wrt. block structure*) 

126 

127 
exception STATE of string * state; 

128 

129 
fun err_malformed name state = 

130 
raise STATE (name ^ ": internal error  malformed proof state", state); 

131 

6871  132 
fun check_result msg state sq = 
133 
(case Seq.pull sq of 

134 
None => raise STATE (msg, state) 

135 
 Some s_sq => Seq.cons s_sq); 

136 

5820  137 

138 
fun map_current f (State ({context, facts, mode, goal}, nodes)) = 

139 
State (make_node (f (context, facts, mode, goal)), nodes); 

140 

141 
fun init_state thy = 

5875  142 
State (make_node (ProofContext.init thy, None, Forward, None), []); 
5820  143 

144 

145 

146 
(** basic proof state operations **) 

147 

148 
(* context *) 

149 

150 
fun context_of (State ({context, ...}, _)) = context; 

151 
val theory_of = ProofContext.theory_of o context_of; 

152 
val sign_of = ProofContext.sign_of o context_of; 

153 

154 
fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 

155 

156 
fun map_context_result f (state as State ({context, facts, mode, goal}, nodes)) = 

157 
let val (context', result) = f context 

158 
in (State (make_node (context', facts, mode, goal), nodes), result) end; 

159 

160 

161 
fun put_data kind f = map_context o ProofContext.put_data kind f; 

162 
val declare_term = map_context o ProofContext.declare_term; 

163 
val add_binds = map_context o ProofContext.add_binds_i; 

6790  164 
val auto_bind_goal = map_context o ProofContext.auto_bind_goal; 
6798  165 
val auto_bind_facts = map_context oo ProofContext.auto_bind_facts; 
6091  166 
val put_thms = map_context o ProofContext.put_thms; 
167 
val put_thmss = map_context o ProofContext.put_thmss; 

5820  168 

169 

170 
(* facts *) 

171 

172 
fun the_facts (State ({facts = Some facts, ...}, _)) = facts 

173 
 the_facts state = raise STATE ("No current facts available", state); 

174 

6776  175 
fun the_fact state = 
176 
(case the_facts state of 

177 
[fact] => fact 

178 
 _ => raise STATE ("Single fact expected", state)); 

179 

6848  180 
fun assert_facts state = (the_facts state; state); 
181 

5820  182 
fun put_facts facts state = 
183 
state 

184 
> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) 

6798  185 
> put_thms ("facts", if_none facts []); 
5820  186 

187 
val reset_facts = put_facts None; 

188 

189 
fun have_facts (name, facts) state = 

190 
state 

191 
> put_facts (Some facts) 

6798  192 
> put_thms (name, facts); 
5820  193 

194 
fun these_facts (state, ths) = have_facts ths state; 

195 
fun fetch_facts (State ({facts, ...}, _)) = put_facts facts; 

196 

197 

198 
(* goal *) 

199 

200 
fun find_goal i (State ({goal = Some goal, ...}, _)) = (i, goal) 

201 
 find_goal i (State ({goal = None, ...}, node :: nodes)) = 

202 
find_goal (i + 1) (State (node, nodes)) 

203 
 find_goal _ (state as State (_, [])) = err_malformed "find_goal" state; 

204 

205 
fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); 

206 

207 
fun map_goal f (State ({context, facts, mode, goal = Some goal}, nodes)) = 

208 
State (make_node (context, facts, mode, Some (f goal)), nodes) 

209 
 map_goal f (State (nd, node :: nodes)) = 

210 
let val State (node', nodes') = map_goal f (State (node, nodes)) 

211 
in State (nd, node' :: nodes') end 

212 
 map_goal _ state = state; 

213 

214 
fun goal_facts get state = 

215 
state 

216 
> map_goal (fn (result, (_, thm)) => (result, (get state, thm))); 

217 

218 
fun use_facts state = 

219 
state 

220 
> goal_facts the_facts 

221 
> reset_facts; 

222 

223 

224 
(* mode *) 

225 

226 
fun get_mode (State ({mode, ...}, _)) = mode; 

227 
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); 

228 

229 
val enter_forward = put_mode Forward; 

230 
val enter_forward_chain = put_mode ForwardChain; 

231 
val enter_backward = put_mode Backward; 

232 

233 
fun assert_mode pred state = 

234 
let val mode = get_mode state in 

235 
if pred mode then state 

6731  236 
else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state) 
5820  237 
end; 
238 

239 
fun is_chain state = get_mode state = ForwardChain; 

240 
val assert_forward = assert_mode (equal Forward); 

241 
val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain); 

242 
val assert_backward = assert_mode (equal Backward); 

243 

244 

245 
(* blocks *) 

246 

6776  247 
fun level (State (_, nodes)) = length nodes; 
248 

5820  249 
fun open_block (State (node, nodes)) = State (node, node :: nodes); 
250 

251 
fun new_block state = 

252 
state 

253 
> open_block 

254 
> put_goal None; 

255 

256 
fun close_block (State (_, node :: nodes)) = State (node, nodes) 

257 
 close_block state = raise STATE ("Unbalanced block parentheses", state); 

258 

259 

260 

261 
(** print_state **) 

262 

6529  263 
val verbose = ProofContext.verbose; 
264 

6756  265 
fun print_facts _ None = () 
6871  266 
 print_facts s (Some ths) = Pretty.writeln (Pretty.big_list (s ^ " facts:") 
267 
(map (setmp Display.show_hyps false Display.pretty_thm) ths)); 

6756  268 

5820  269 
fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = 
270 
let 

5945
63184e276c1d
print_state: use begin_goal from Goals.current_goals_markers;
wenzelm
parents:
5936
diff
changeset

271 
val ref (_, _, begin_goal) = Goals.current_goals_markers; 
5820  272 

273 
fun levels_up 0 = "" 

274 
 levels_up i = " (" ^ string_of_int i ^ " levels up)"; 

275 

6848  276 
fun print_goal (i, ((kind, name, _, _, _), (goal_facts, thm))) = 
6756  277 
(print_facts "Using" (if null goal_facts then None else Some goal_facts); 
278 
writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 2) ^ ":"); 

5945
63184e276c1d
print_state: use begin_goal from Goals.current_goals_markers;
wenzelm
parents:
5936
diff
changeset

279 
Locale.print_goals_marker begin_goal (! goals_limit) thm); 
6848  280 

281 
val ctxt_strings = ProofContext.strings_of_context context; 

5820  282 
in 
6262  283 
writeln ("Nesting level: " ^ string_of_int (length nodes div 2)); 
5820  284 
writeln ""; 
6798  285 
writeln (mode_name mode ^ " mode"); 
5993  286 
writeln ""; 
6529  287 
if ! verbose orelse mode = Forward then 
6848  288 
(if null ctxt_strings then () else (seq writeln ctxt_strings; writeln ""); 
6756  289 
print_facts "Current" facts; 
6529  290 
print_goal (find_goal 0 state)) 
6756  291 
else if mode = ForwardChain then print_facts "Picking" facts 
6529  292 
else print_goal (find_goal 0 state) 
5820  293 
end; 
294 

295 

296 

297 
(** proof steps **) 

298 

299 
(* datatype method *) 

300 

6848  301 
datatype method = Method of thm list > tactic; 
5820  302 
val method = Method; 
303 

304 

305 
(* refine goal *) 

306 

307 
fun check_sign sg state = 

308 
if Sign.subsig (sg, sign_of state) then state 

309 
else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state); 

310 

311 
fun refine meth_fun (state as State ({context, ...}, _)) = 

6848  312 
let 
313 
val Method meth = meth_fun context; 

314 
val (_, (result, (facts, thm))) = find_goal 0 state; 

5820  315 

6848  316 
fun refn thm' = 
317 
state 

318 
> check_sign (Thm.sign_of_thm thm') 

319 
> map_goal (K (result, (facts, thm'))); 

320 
in Seq.map refn (meth facts thm) end; 

5820  321 

322 

323 
(* prepare result *) 

324 

325 
fun varify_frees names thm = 

326 
let 

327 
fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None 

328 
 get_free _ (opt, _) = opt; 

329 

330 
fun find_free t x = foldl_aterms (get_free x) (None, t); 

331 

6887  332 
val {sign, prop, ...} = Thm.rep_thm thm; 
5820  333 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names); 
334 
in 

335 
thm 

336 
> Drule.forall_intr_list frees 

6887  337 
> Drule.forall_elim_vars 0 
5820  338 
end; 
339 

6790  340 
fun varify_tfrees thm = 
341 
let 

342 
val {hyps, prop, ...} = Thm.rep_thm thm; 

343 
val frees = foldr Term.add_term_frees (prop :: hyps, []); 

344 
val leave_tfrees = foldr Term.add_term_tfree_names (frees, []); 

345 
in thm > Thm.varifyT' leave_tfrees end; 

346 

5820  347 
fun implies_elim_hyps thm = 
348 
foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm)); 

349 

6848  350 

5820  351 
fun prep_result state asms t raw_thm = 
352 
let 

353 
val ctxt = context_of state; 

354 
fun err msg = raise STATE (msg, state); 

355 

356 
val ngoals = Thm.nprems_of raw_thm; 

357 
val _ = 

358 
if ngoals = 0 then () 

359 
else (Locale.print_goals ngoals raw_thm; err (string_of_int ngoals ^ " unsolved goal(s)!")); 

360 

361 
val thm = 

362 
raw_thm RS Drule.rev_triv_goal 

363 
> implies_elim_hyps 

364 
> Drule.implies_intr_list asms 

6731  365 
> varify_frees (ProofContext.fixed_names ctxt) 
6790  366 
> varify_tfrees; 
5820  367 

368 
val {hyps, prop, sign, ...} = Thm.rep_thm thm; 

369 
val tsig = Sign.tsig_of sign; 

370 
in 

371 
(* FIXME 

372 
if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then 

373 
warning ("Proved a different theorem: " ^ Sign.string_of_term sign prop) 

374 
else (); 

375 
*) 

376 
if not (null hyps) then 

377 
err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps)) 

378 
(* FIXME else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then 

379 
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *) 

6871  380 
else thm 
5820  381 
end; 
382 

383 

384 
(* prepare final result *) 

385 

386 
fun strip_flexflex thm = 

387 
Seq.hd (Thm.flexflex_rule thm) handle THM _ => thm; 

388 

389 
fun final_result state pre_thm = 

390 
let 

391 
val thm = 

392 
pre_thm 

393 
> strip_flexflex 

394 
> Thm.strip_shyps 

395 
> Drule.standard; 

396 

397 
val str_of_sort = Sign.str_of_sort (Thm.sign_of_thm thm); 

398 
val xshyps = Thm.extra_shyps thm; 

399 
in 

400 
if not (null xshyps) then 

401 
raise STATE ("Extra sort hypotheses: " ^ commas (map str_of_sort xshyps), state) 

402 
else thm 

403 
end; 

404 

405 

406 
(* solve goal *) 

407 

6853  408 
fun RANGE [] _ = all_tac 
409 
 RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; 

6848  410 

411 
fun solve_goal rule tacs state = 

5820  412 
let 
413 
val (_, (result, (facts, thm))) = find_goal 0 state; 

6853  414 
val thms' = FIRSTGOAL (rtac rule THEN' RANGE tacs) thm; 
5820  415 
in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end; 
416 

417 

418 

419 
(*** structured proof commands ***) 

420 

421 
(** context **) 

422 

423 
(* bind *) 

424 

425 
fun gen_bind f x state = 

426 
state 

427 
> assert_forward 

428 
> map_context (f x) 

429 
> reset_facts; 

430 

431 
val bind = gen_bind ProofContext.add_binds; 

432 
val bind_i = gen_bind ProofContext.add_binds_i; 

433 

434 
val match_bind = gen_bind ProofContext.match_binds; 

435 
val match_bind_i = gen_bind ProofContext.match_binds_i; 

436 

437 

6091  438 
(* have_thmss *) 
5820  439 

6876  440 
fun have_thmss ths name atts ths_atts state = 
5820  441 
state 
442 
> assert_forward 

6876  443 
> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts) 
5820  444 
> these_facts; 
445 

6876  446 
fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])]; 
447 

5820  448 

449 
(* fix *) 

450 

451 
fun gen_fix f xs state = 

452 
state 

453 
> assert_forward 

454 
> map_context (f xs) 

455 
> reset_facts; 

456 

457 
val fix = gen_fix ProofContext.fix; 

458 
val fix_i = gen_fix ProofContext.fix_i; 

459 

460 

461 
(* assume *) 

462 

6848  463 
fun gen_assume f tac name atts props state = 
5820  464 
state 
465 
> assert_forward 

6848  466 
> map_context_result (f tac (PureThy.default_name name) atts props) 
6798  467 
> (fn (st, (facts, prems)) => 
468 
(st, facts) 

469 
> these_facts 

470 
> put_thms ("prems", prems)); 

5820  471 

472 
val assume = gen_assume ProofContext.assume; 

473 
val assume_i = gen_assume ProofContext.assume_i; 

474 

475 

476 

477 
(** goals **) 

478 

479 
(* forward chaining *) 

480 

481 
fun chain state = 

482 
state 

483 
> assert_forward 

6848  484 
> assert_facts 
5820  485 
> enter_forward_chain; 
486 

487 
fun from_facts facts state = 

488 
state 

489 
> put_facts (Some facts) 

490 
> chain; 

491 

492 

493 
(* setup goals *) 

494 

5936  495 
fun setup_goal opt_block prepp kind name atts raw_propp state = 
5820  496 
let 
5936  497 
val (state', concl) = 
498 
state 

499 
> assert_forward_or_chain 

500 
> enter_forward 

501 
> opt_block 

502 
> map_context_result (fn c => prepp (c, raw_propp)); 

6752
0545b77f864e
setup_goal: proper handling of nonatomic goals (include cprems into asms);
wenzelm
parents:
6731
diff
changeset

503 
val cterm_of = Thm.cterm_of (sign_of state); 
5820  504 

6848  505 
val (casms, asm_tacs) = Library.split_list (ProofContext.assumptions (context_of state')); 
6752
0545b77f864e
setup_goal: proper handling of nonatomic goals (include cprems into asms);
wenzelm
parents:
6731
diff
changeset

506 
val cprems = map cterm_of (Logic.strip_imp_prems concl); 
6848  507 
val prem_tacs = replicate (length cprems) (K all_tac); 
508 

6752
0545b77f864e
setup_goal: proper handling of nonatomic goals (include cprems into asms);
wenzelm
parents:
6731
diff
changeset

509 
val prop = Logic.list_implies (map Thm.term_of casms, concl); 
0545b77f864e
setup_goal: proper handling of nonatomic goals (include cprems into asms);
wenzelm
parents:
6731
diff
changeset

510 
val cprop = cterm_of prop; 
5820  511 
val thm = Drule.mk_triv_goal cprop; 
512 
in 

5936  513 
state' 
6848  514 
> put_goal (Some ((kind atts, (PureThy.default_name name), casms @ cprems, 
515 
asm_tacs @ prem_tacs, prop), ([], thm))) 

6790  516 
> auto_bind_goal prop 
5820  517 
> (if is_chain state then use_facts else reset_facts) 
518 
> new_block 

519 
> enter_backward 

520 
end; 

521 

522 

523 
(*global goals*) 

524 
fun global_goal prep kind name atts x thy = 

525 
setup_goal I prep kind name atts x (init_state thy); 

526 

5936  527 
val theorem = global_goal ProofContext.bind_propp Theorem; 
528 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

529 
val lemma = global_goal ProofContext.bind_propp Lemma; 

530 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  531 

532 

533 
(*local goals*) 

534 
fun local_goal prep kind name atts x = 

535 
setup_goal open_block prep kind name atts x; 

536 

5936  537 
val show = local_goal ProofContext.bind_propp Goal; 
538 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

539 
val have = local_goal ProofContext.bind_propp Aux; 

540 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  541 

542 

543 

544 
(** blocks **) 

545 

546 
(* begin_block *) 

547 

548 
fun begin_block state = 

549 
state 

550 
> assert_forward 

551 
> new_block 

552 
> reset_facts 

553 
> open_block; 

554 

555 

556 
(* next_block *) 

557 

558 
fun next_block state = 

559 
state 

560 
> assert_forward 

561 
> close_block 

562 
> new_block; 

563 

564 

565 

566 
(** conclusions **) 

567 

568 
(* current goal *) 

569 

570 
fun current_goal (State ({goal = Some goal, ...}, _)) = goal 

571 
 current_goal state = raise STATE ("No current goal!", state); 

572 

6404  573 
fun assert_current_goal true (state as State ({goal = None, ...}, _)) = 
574 
raise STATE ("No goal in this block!", state) 

575 
 assert_current_goal false (state as State ({goal = Some _, ...}, _)) = 

576 
raise STATE ("Goal present in this block!", state) 

577 
 assert_current_goal _ state = state; 

5820  578 

579 
fun assert_bottom true (state as State (_, _ :: _)) = 

580 
raise STATE ("Not at bottom of proof!", state) 

581 
 assert_bottom false (state as State (_, [])) = 

582 
raise STATE ("Already at bottom of proof!", state) 

583 
 assert_bottom _ state = state; 

584 

6404  585 
val at_bottom = can (assert_bottom true o close_block); 
586 

5820  587 

588 
(* finish proof *) 

589 

6871  590 
fun finish_proof bot state = 
5820  591 
state 
592 
> assert_forward 

593 
> close_block 

594 
> assert_bottom bot 

6871  595 
> assert_current_goal true; 
5820  596 

597 

6404  598 
(* end_block *) 
599 

600 
fun end_block state = 

601 
state 

602 
> assert_forward 

603 
> close_block 

604 
> assert_current_goal false 

605 
> close_block 

606 
> fetch_facts state; 

607 

608 

609 
(* local_qed *) 

5820  610 

6731  611 
fun finish_local print_result state = 
5820  612 
let 
6848  613 
val ((kind, name, asms, tacs, t), (_, raw_thm)) = current_goal state; 
6871  614 
val result = prep_result state asms t raw_thm; 
5820  615 
val (atts, opt_solve) = 
616 
(case kind of 

6848  617 
Goal atts => (atts, solve_goal result tacs) 
5820  618 
 Aux atts => (atts, Seq.single) 
619 
 _ => raise STATE ("No local goal!", state)); 

620 
in 

6731  621 
print_result {kind = kind_name kind, name = name, thm = result}; 
5820  622 
state 
623 
> close_block 

6871  624 
> auto_bind_facts name [t] 
6876  625 
> have_thmss [] name atts [Thm.no_attributes [result]] 
5820  626 
> opt_solve 
627 
end; 

628 

6731  629 
fun local_qed finalize print_result state = 
6404  630 
state 
6871  631 
> finish_proof false 
632 
> finalize 

6731  633 
> (Seq.flat o Seq.map (finish_local print_result)); 
5820  634 

635 

6404  636 
(* global_qed *) 
5820  637 

638 
fun finish_global alt_name alt_atts state = 

639 
let 

6848  640 
val ((kind, def_name, asms, _, t), (_, raw_thm)) = current_goal state; 
6871  641 
val result = final_result state (prep_result state asms t raw_thm); 
5820  642 

643 
val name = if_none alt_name def_name; 

644 
val atts = 

645 
(case kind of 

646 
Theorem atts => if_none alt_atts atts 

6091  647 
 Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma] 
5820  648 
 _ => raise STATE ("No global goal!", state)); 
649 

6091  650 
val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state); 
6529  651 
in (thy', {kind = kind_name kind, name = name, thm = result'}) end; 
5820  652 

6871  653 
(*Note: should inspect first result only, backtracking may destroy theory*) 
6404  654 
fun global_qed finalize alt_name alt_atts state = 
5820  655 
state 
6871  656 
> finish_proof true 
657 
> finalize 

658 
> Seq.map (finish_global alt_name alt_atts); 

5820  659 

660 

661 
end; 