author  wenzelm 
Tue, 27 Apr 1999 15:13:35 +0200  
changeset 6529  0f4c2ebc5018 
parent 6404  2daaf2943c79 
child 6683  b7293047b0f4 
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 
TODO: 

8 
 assume: improve schematic Vars handling (!?); 

5918  9 
 warn_vars; 
5820  10 
 bind: check rhs (extra (T)Vars etc.) (How to handle these anyway?); 
11 
 prep_result: avoid duplicate asms; 

12 
 prep_result error: use error channel (!); 

5918  13 
 check_finished: trace results (!?); 
5820  14 
 next_block: fetch_facts (!?); 
15 
*) 

16 

17 
signature PROOF = 

18 
sig 

19 
type context 

20 
type state 

21 
exception STATE of string * state 

22 
val context_of: state > context 

23 
val theory_of: state > theory 

24 
val sign_of: state > Sign.sg 

6091  25 
val the_facts: state > thm list 
26 
val goal_facts: (state > thm list) > state > state 

5820  27 
val use_facts: state > state 
28 
val reset_facts: state > state 

29 
val assert_backward: state > state 

30 
val enter_forward: state > state 

6529  31 
val verbose: bool ref 
5820  32 
val print_state: state > unit 
33 
type method 

6091  34 
val method: (thm list > thm > 
35 
(thm * (indexname * term) list * (string * thm list) list) Seq.seq) > method 

5820  36 
val refine: (context > method) > state > state Seq.seq 
37 
val bind: (indexname * string) list > state > state 

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

5936  39 
val match_bind: (string list * string) list > state > state 
40 
val match_bind_i: (term list * term) list > state > state 

6091  41 
val have_thmss: string > context attribute list > 
42 
(thm list * context attribute list) list > state > state 

5936  43 
val assume: string > context attribute list > (string * string list) list > state > state 
44 
val assume_i: string > context attribute list > (term * term list) list > state > state 

5820  45 
val fix: (string * string option) list > state > state 
46 
val fix_i: (string * typ) list > state > state 

5936  47 
val theorem: bstring > theory attribute list > string * string list > theory > state 
48 
val theorem_i: bstring > theory attribute list > term * term list > theory > state 

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

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

5820  51 
val chain: state > state 
6091  52 
val from_facts: thm list > state > state 
5936  53 
val show: string > context attribute list > string * string list > state > state 
54 
val show_i: string > context attribute list > term * term list > state > state 

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

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

5820  57 
val begin_block: state > state 
58 
val next_block: state > state 

6404  59 
val end_block: state > state 
60 
val at_bottom: state > bool 

61 
val local_qed: (state > state Seq.seq) > state > state Seq.seq 

62 
val global_qed: (state > state Seq.seq) > bstring option 

6529  63 
> theory attribute list option > state > theory * {kind: string, name: string, thm: thm} 
5820  64 
end; 
65 

66 
signature PROOF_PRIVATE = 

67 
sig 

68 
include PROOF 

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

70 
end; 

71 

72 
structure Proof: PROOF_PRIVATE = 

73 
struct 

74 

75 

76 
(** proof state **) 

77 

78 
type context = ProofContext.context; 

79 

80 

81 
(* type goal *) 

82 

83 
datatype kind = 

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

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

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

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

88 

89 
val kind_name = 

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

92 
type goal = 

6091  93 
(kind * (*result kind*) 
5820  94 
string * (*result name*) 
95 
cterm list * (*result assumptions*) 

96 
term) * (*result statement*) 

6091  97 
(thm list * (*use facts*) 
5820  98 
thm); (*goal: subgoals ==> statement*) 
99 

100 

101 
(* type mode *) 

102 

103 
datatype mode = Forward  ForwardChain  Backward; 

104 

105 
val mode_name = 

6030  106 
fn Forward => "state"  ForwardChain => "chain"  Backward => "prove"; 
5820  107 

108 

109 
(* type node *) 

110 

111 
type node = 

112 
{context: context, 

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

116 

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

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

119 

120 

121 
(* datatype state *) 

122 

123 
datatype state = 

124 
State of 

125 
node * (*current*) 

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

127 

128 
exception STATE of string * state; 

129 

130 
fun err_malformed name state = 

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

132 

133 

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

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

136 

137 
fun init_state thy = 

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

140 

141 

142 
(** basic proof state operations **) 

143 

144 
(* context *) 

145 

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

147 
val theory_of = ProofContext.theory_of o context_of; 

148 
val sign_of = ProofContext.sign_of o context_of; 

149 

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

151 

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

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

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

155 

156 

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

158 
val declare_term = map_context o ProofContext.declare_term; 

159 
val add_binds = map_context o ProofContext.add_binds_i; 

6091  160 
val put_thms = map_context o ProofContext.put_thms; 
161 
val put_thmss = map_context o ProofContext.put_thmss; 

5820  162 

163 

164 
(* bind statements *) 

165 

166 
fun bind_props bs state = 

167 
let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement 

168 
in state > add_binds (flat (map mk_bind bs)) end; 

169 

6091  170 
fun bind_thms (name, thms) state = 
5820  171 
let 
6091  172 
val props = map (#prop o Thm.rep_thm) thms; 
5820  173 
val named_props = 
174 
(case props of 

175 
[prop] => [(name, prop)] 

176 
 props => map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props)); 

177 
in state > bind_props named_props end; 

178 

6091  179 
fun let_thms name_thms state = 
5820  180 
state 
6091  181 
> put_thms name_thms 
182 
> bind_thms name_thms; 

5820  183 

184 

185 
(* facts *) 

186 

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

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

189 

190 
fun put_facts facts state = 

191 
state 

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

6091  193 
> let_thms ("facts", if_none facts []); 
5820  194 

195 
val reset_facts = put_facts None; 

196 

197 
fun have_facts (name, facts) state = 

198 
state 

199 
> put_facts (Some facts) 

6091  200 
> let_thms (name, facts); 
5820  201 

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

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

204 

205 

206 
(* goal *) 

207 

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

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

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

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

212 

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

214 

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

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

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

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

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

220 
 map_goal _ state = state; 

221 

222 
fun goal_facts get state = 

223 
state 

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

225 

226 
fun use_facts state = 

227 
state 

228 
> goal_facts the_facts 

229 
> reset_facts; 

230 

231 

232 
(* mode *) 

233 

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

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

236 

237 
val enter_forward = put_mode Forward; 

238 
val enter_forward_chain = put_mode ForwardChain; 

239 
val enter_backward = put_mode Backward; 

240 

241 
fun assert_mode pred state = 

242 
let val mode = get_mode state in 

243 
if pred mode then state 

244 
else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state) 

245 
end; 

246 

247 
fun is_chain state = get_mode state = ForwardChain; 

248 
val assert_forward = assert_mode (equal Forward); 

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

250 
val assert_backward = assert_mode (equal Backward); 

251 

252 

253 
(* blocks *) 

254 

255 
fun open_block (State (node, nodes)) = State (node, node :: nodes); 

256 

257 
fun new_block state = 

258 
state 

259 
> open_block 

260 
> put_goal None; 

261 

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

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

264 

265 

266 

267 
(** print_state **) 

268 

6529  269 
val verbose = ProofContext.verbose; 
270 

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

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

273 
val ref (_, _, begin_goal) = Goals.current_goals_markers; 
5820  274 

275 
fun print_facts None = () 

276 
 print_facts (Some ths) = 

6091  277 
Pretty.writeln (Pretty.big_list "Current facts:" (map Display.pretty_thm ths)); 
5820  278 

279 
fun levels_up 0 = "" 

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

281 

282 
fun print_goal (i, ((kind, name, _, _), (_, thm))) = 

6262  283 
(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

284 
Locale.print_goals_marker begin_goal (! goals_limit) thm); 
5820  285 
in 
6262  286 
writeln ("Nesting level: " ^ string_of_int (length nodes div 2)); 
5820  287 
writeln ""; 
6529  288 
writeln (enclose "`" "'" (mode_name mode) ^ " mode"); 
5993  289 
writeln ""; 
6529  290 
if ! verbose orelse mode = Forward then 
291 
(ProofContext.print_context context; 

292 
writeln ""; 

293 
print_facts facts; 

294 
print_goal (find_goal 0 state)) 

295 
else if mode = ForwardChain then print_facts facts 

296 
else print_goal (find_goal 0 state) 

5820  297 
end; 
298 

299 

300 

301 
(** proof steps **) 

302 

303 
(* datatype method *) 

304 

305 
datatype method = Method of 

6091  306 
thm list > (*use facts*) 
5820  307 
thm (*goal: subgoals ==> statement*) 
308 
> (thm * (*refined goal*) 

309 
(indexname * term) list * (*new bindings*) 

6091  310 
(string * thm list) list) (*new thms*) 
5820  311 
Seq.seq; 
312 

313 
val method = Method; 

314 

315 

316 
(* refine goal *) 

317 

318 
fun check_sign sg state = 

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

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

321 

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

323 
let 

324 
val Method meth = meth_fun context; 

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

326 

327 
fun refn (thm', new_binds, new_thms) = 

328 
state 

329 
> check_sign (sign_of_thm thm') 

330 
> map_goal (K (result, (facts, thm'))) 

331 
> add_binds new_binds 

6091  332 
> put_thmss new_thms; 
5820  333 
in Seq.map refn (meth facts thm) end; 
334 

335 

336 
(* prepare result *) 

337 

338 
fun varify_frees names thm = 

339 
let 

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

341 
 get_free _ (opt, _) = opt; 

342 

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

344 

345 
val {sign, maxidx, prop, ...} = Thm.rep_thm thm; 

346 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) names); 

347 
in 

348 
thm 

349 
> Drule.forall_intr_list frees 

350 
> Drule.forall_elim_vars (maxidx + 1) 

351 
end; 

352 

353 
fun implies_elim_hyps thm = 

354 
foldl (uncurry Thm.implies_elim) (thm, map Thm.assume (Drule.cprems_of thm)); 

355 

356 
fun prep_result state asms t raw_thm = 

357 
let 

358 
val ctxt = context_of state; 

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

360 

361 
val ngoals = Thm.nprems_of raw_thm; 

362 
val _ = 

363 
if ngoals = 0 then () 

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

365 

366 
val thm = 

367 
raw_thm RS Drule.rev_triv_goal 

368 
> implies_elim_hyps 

369 
> Drule.implies_intr_list asms 

370 
> varify_frees (ProofContext.fixed_names ctxt); 

371 

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

373 
val tsig = Sign.tsig_of sign; 

374 
in 

375 
(* FIXME 

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

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

378 
else (); 

379 
*) 

380 
if not (null hyps) then 

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

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

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

384 
else thm 

385 
end; 

386 

387 

388 
(* prepare final result *) 

389 

390 
fun strip_flexflex thm = 

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

392 

393 
fun final_result state pre_thm = 

394 
let 

395 
val thm = 

396 
pre_thm 

397 
> strip_flexflex 

398 
> Thm.strip_shyps 

399 
> Drule.standard; 

400 

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

402 
val xshyps = Thm.extra_shyps thm; 

403 
in 

404 
if not (null xshyps) then 

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

406 
else thm 

407 
end; 

408 

409 

410 
(* solve goal *) 

411 

412 
fun solve_goal rule state = 

413 
let 

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

5993  415 
val thms' = FIRSTGOAL (rtac rule THEN_ALL_NEW (TRY o assume_tac)) thm; 
5820  416 
in Seq.map (fn thm' => map_goal (K (result, (facts, thm'))) state) thms' end; 
417 

418 

419 

420 
(*** structured proof commands ***) 

421 

422 
(** context **) 

423 

424 
(* bind *) 

425 

426 
fun gen_bind f x state = 

427 
state 

428 
> assert_forward 

429 
> map_context (f x) 

430 
> reset_facts; 

431 

432 
val bind = gen_bind ProofContext.add_binds; 

433 
val bind_i = gen_bind ProofContext.add_binds_i; 

434 

435 
val match_bind = gen_bind ProofContext.match_binds; 

436 
val match_bind_i = gen_bind ProofContext.match_binds_i; 

437 

438 

6091  439 
(* have_thmss *) 
5820  440 

6091  441 
fun have_thmss name atts ths_atts state = 
5820  442 
state 
443 
> assert_forward 

6091  444 
> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts) 
5820  445 
> these_facts; 
446 

447 

448 
(* fix *) 

449 

450 
fun gen_fix f xs state = 

451 
state 

452 
> assert_forward 

453 
> map_context (f xs) 

454 
> reset_facts; 

455 

456 
val fix = gen_fix ProofContext.fix; 

457 
val fix_i = gen_fix ProofContext.fix_i; 

458 

459 

460 
(* assume *) 

461 

462 
fun gen_assume f name atts props state = 

463 
state 

464 
> assert_forward 

5918  465 
> map_context_result (f (PureThy.default_name name) atts props) 
5820  466 
> these_facts 
6091  467 
> (fn st => let_thms ("prems", ProofContext.assumptions (context_of st)) st); 
5820  468 

469 
val assume = gen_assume ProofContext.assume; 

470 
val assume_i = gen_assume ProofContext.assume_i; 

471 

472 

473 

474 
(** goals **) 

475 

476 
(* forward chaining *) 

477 

478 
fun chain state = 

479 
state 

480 
> assert_forward 

481 
> enter_forward_chain; 

482 

483 
fun from_facts facts state = 

484 
state 

485 
> put_facts (Some facts) 

486 
> chain; 

487 

488 

489 
(* setup goals *) 

490 

5936  491 
fun setup_goal opt_block prepp kind name atts raw_propp state = 
5820  492 
let 
5936  493 
val (state', concl) = 
494 
state 

495 
> assert_forward_or_chain 

496 
> enter_forward 

497 
> opt_block 

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

5820  499 

6091  500 
val casms = map (#prop o Thm.crep_thm) (ProofContext.assumptions (context_of state')); 
5820  501 
val asms = map Thm.term_of casms; 
502 

5936  503 
val prop = Logic.list_implies (asms, concl); 
504 
val cprop = Thm.cterm_of (sign_of state') prop; 

5820  505 
val thm = Drule.mk_triv_goal cprop; 
506 
in 

5936  507 
state' 
5918  508 
> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm))) 
5820  509 
> bind_props [("thesis", prop)] 
510 
> (if is_chain state then use_facts else reset_facts) 

511 
> new_block 

512 
> enter_backward 

513 
end; 

514 

515 

516 
(*global goals*) 

517 
fun global_goal prep kind name atts x thy = 

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

519 

5936  520 
val theorem = global_goal ProofContext.bind_propp Theorem; 
521 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

522 
val lemma = global_goal ProofContext.bind_propp Lemma; 

523 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  524 

525 

526 
(*local goals*) 

527 
fun local_goal prep kind name atts x = 

528 
setup_goal open_block prep kind name atts x; 

529 

5936  530 
val show = local_goal ProofContext.bind_propp Goal; 
531 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

532 
val have = local_goal ProofContext.bind_propp Aux; 

533 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  534 

535 

536 

537 
(** blocks **) 

538 

539 
(* begin_block *) 

540 

541 
fun begin_block state = 

542 
state 

543 
> assert_forward 

544 
> new_block 

545 
> reset_facts 

546 
> open_block; 

547 

548 

549 
(* next_block *) 

550 

551 
fun next_block state = 

552 
state 

553 
> assert_forward 

554 
> close_block 

555 
> new_block; 

556 

557 

558 

559 
(** conclusions **) 

560 

561 
(* current goal *) 

562 

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

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

565 

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

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

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

570 
 assert_current_goal _ state = state; 

5820  571 

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

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

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

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

576 
 assert_bottom _ state = state; 

577 

6404  578 
val at_bottom = can (assert_bottom true o close_block); 
579 

5820  580 

581 
(* finish proof *) 

582 

583 
fun check_finished state states = 

584 
(case Seq.pull states of 

585 
None => raise STATE ("Failed to finish proof", state) 

586 
 Some s_sq => Seq.cons s_sq); 

587 

6404  588 
fun finish_proof bot finalize state = 
5820  589 
state 
590 
> assert_forward 

591 
> close_block 

592 
> assert_bottom bot 

6404  593 
> assert_current_goal true 
594 
> finalize 

5820  595 
> check_finished state; 
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 

611 
fun finish_local state = 

612 
let 

613 
val ((kind, name, asms, t), (_, raw_thm)) = current_goal state; 

614 
val result = prep_result state asms t raw_thm; 

615 
val (atts, opt_solve) = 

616 
(case kind of 

617 
Goal atts => (atts, solve_goal result) 

618 
 Aux atts => (atts, Seq.single) 

619 
 _ => raise STATE ("No local goal!", state)); 

620 
in 

621 
state 

622 
> close_block 

6091  623 
> have_thmss name atts [Thm.no_attributes [result]] 
5820  624 
> opt_solve 
625 
end; 

626 

6404  627 
fun local_qed finalize state = 
628 
state 

629 
> finish_proof false finalize 

630 
> (Seq.flat o Seq.map finish_local); 

5820  631 

632 

6404  633 
(* global_qed *) 
5820  634 

635 
fun finish_global alt_name alt_atts state = 

636 
let 

637 
val ((kind, def_name, asms, t), (_, raw_thm)) = current_goal state; 

638 
val result = final_result state (prep_result state asms t raw_thm); 

639 

640 
val name = if_none alt_name def_name; 

641 
val atts = 

642 
(case kind of 

643 
Theorem atts => if_none alt_atts atts 

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

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

6404  650 
fun global_qed finalize alt_name alt_atts state = 
5820  651 
state 
6404  652 
> finish_proof true finalize 
5820  653 
> Seq.hd 
654 
> finish_global alt_name alt_atts; 

655 

656 

657 
end; 