author  wenzelm 
Thu, 15 Jul 1999 17:53:28 +0200  
changeset 7011  7e8e9a26ba2c 
parent 6996  1a28d968c5aa 
child 7176  a329a37ed91a 
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 
7011  14 
val init_state: theory > state 
5820  15 
val context_of: state > context 
16 
val theory_of: state > theory 

17 
val sign_of: state > Sign.sg 

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

6891  23 
val assert_forward: state > state 
5820  24 
val assert_backward: state > state 
25 
val enter_forward: state > state 

6982  26 
val show_hyps: bool ref 
27 
val pretty_thm: thm > Pretty.T 

6529  28 
val verbose: bool ref 
5820  29 
val print_state: state > unit 
6776  30 
val level: state > int 
5820  31 
type method 
6848  32 
val method: (thm list > tactic) > method 
5820  33 
val refine: (context > method) > state > state Seq.seq 
6932  34 
val export_thm: context > thm > thm 
5820  35 
val bind: (indexname * string) list > state > state 
36 
val bind_i: (indexname * term) list > state > state 

5936  37 
val match_bind: (string list * string) list > state > state 
38 
val match_bind_i: (term list * term) list > state > state 

6876  39 
val have_thmss: thm list > string > context attribute list > 
6091  40 
(thm list * context attribute list) list > state > state 
6876  41 
val simple_have_thms: string > thm list > state > state 
5820  42 
val fix: (string * string option) list > state > state 
43 
val fix_i: (string * typ) list > state > state 

6932  44 
val assm: (int > tactic) * (int > tactic) > string > context attribute list 
45 
> (string * (string list * string list)) list > state > state 

46 
val assm_i: (int > tactic) * (int > tactic) > string > context attribute list 

47 
> (term * (term list * term list)) list > state > state 

48 
val assume: string > context attribute list > (string * (string list * string list)) list 

49 
> state > state 

50 
val assume_i: string > context attribute list > (term * (term list * term list)) list 

51 
> state > state 

52 
val presume: string > context attribute list > (string * (string list * string list)) list 

53 
> state > state 

54 
val presume_i: string > context attribute list > (term * (term list * term list)) list 

55 
> state > state 

56 
val theorem: bstring > theory attribute list > string * (string list * string list) 

57 
> theory > state 

58 
val theorem_i: bstring > theory attribute list > term * (term list * term list) 

59 
> theory > state 

60 
val lemma: bstring > theory attribute list > string * (string list * string list) 

61 
> theory > state 

62 
val lemma_i: bstring > theory attribute list > term * (term list * term list) 

63 
> theory > state 

5820  64 
val chain: state > state 
6932  65 
val export_chain: state > state Seq.seq 
6091  66 
val from_facts: thm list > state > state 
6932  67 
val show: string > context attribute list > string * (string list * string list) 
68 
> state > state 

69 
val show_i: string > context attribute list > term * (term list * term list) 

70 
> state > state 

71 
val have: string > context attribute list > string * (string list * string list) 

72 
> state > state 

73 
val have_i: string > context attribute list > term * (term list * term list) 

74 
> state > state 

6404  75 
val at_bottom: state > bool 
6982  76 
val local_qed: (state > state Seq.seq) 
77 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) > state > state Seq.seq 

6950  78 
val global_qed: (state > state Seq.seq) > state 
79 
> (theory * {kind: string, name: string, thm: thm}) Seq.seq 

6896  80 
val begin_block: state > state 
6932  81 
val end_block: state > state Seq.seq 
6896  82 
val next_block: state > state 
5820  83 
end; 
84 

85 
signature PROOF_PRIVATE = 

86 
sig 

87 
include PROOF 

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

89 
end; 

90 

91 
structure Proof: PROOF_PRIVATE = 

92 
struct 

93 

94 

95 
(** proof state **) 

96 

97 
type context = ProofContext.context; 

98 

99 

100 
(* type goal *) 

101 

102 
datatype kind = 

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

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

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

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

107 

108 
val kind_name = 

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

111 
type goal = 

6932  112 
(kind * (*result kind*) 
113 
string * (*result name*) 

114 
term) * (*result statement*) 

115 
(thm list * (*use facts*) 

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

5820  117 

118 

119 
(* type mode *) 

120 

121 
datatype mode = Forward  ForwardChain  Backward; 

122 

123 
val mode_name = 

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

5820  126 

127 

128 
(* type node *) 

129 

130 
type node = 

131 
{context: context, 

6091  132 
facts: thm list option, 
5820  133 
mode: mode, 
134 
goal: goal option}; 

135 

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

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

138 

139 

140 
(* datatype state *) 

141 

142 
datatype state = 

143 
State of 

144 
node * (*current*) 

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

146 

147 
exception STATE of string * state; 

148 

149 
fun err_malformed name state = 

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

151 

6871  152 
fun check_result msg state sq = 
153 
(case Seq.pull sq of 

154 
None => raise STATE (msg, state) 

155 
 Some s_sq => Seq.cons s_sq); 

156 

5820  157 

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

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

160 

161 
fun init_state thy = 

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

164 

165 

166 
(** basic proof state operations **) 

167 

168 
(* context *) 

169 

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

171 
val theory_of = ProofContext.theory_of o context_of; 

172 
val sign_of = ProofContext.sign_of o context_of; 

173 

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

175 

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

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

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

179 

180 

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

182 
val declare_term = map_context o ProofContext.declare_term; 

183 
val add_binds = map_context o ProofContext.add_binds_i; 

6790  184 
val auto_bind_goal = map_context o ProofContext.auto_bind_goal; 
6798  185 
val auto_bind_facts = map_context oo ProofContext.auto_bind_facts; 
6091  186 
val put_thms = map_context o ProofContext.put_thms; 
187 
val put_thmss = map_context o ProofContext.put_thmss; 

6932  188 
val assumptions = ProofContext.assumptions o context_of; 
5820  189 

190 

191 
(* facts *) 

192 

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

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

195 

6776  196 
fun the_fact state = 
197 
(case the_facts state of 

198 
[fact] => fact 

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

200 

6848  201 
fun assert_facts state = (the_facts state; state); 
6932  202 
fun get_facts (State ({facts, ...}, _)) = facts; 
6848  203 

5820  204 
fun put_facts facts state = 
205 
state 

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

6798  207 
> put_thms ("facts", if_none facts []); 
5820  208 

209 
val reset_facts = put_facts None; 

210 

211 
fun have_facts (name, facts) state = 

212 
state 

213 
> put_facts (Some facts) 

6798  214 
> put_thms (name, facts); 
5820  215 

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

217 

218 

219 
(* goal *) 

220 

6932  221 
fun find_goal i (state as State ({goal = Some goal, ...}, _)) = (context_of state, (i, goal)) 
5820  222 
 find_goal i (State ({goal = None, ...}, node :: nodes)) = 
223 
find_goal (i + 1) (State (node, nodes)) 

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

225 

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

227 

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

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

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

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

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

233 
 map_goal _ state = state; 

234 

235 
fun goal_facts get state = 

236 
state 

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

238 

239 
fun use_facts state = 

240 
state 

241 
> goal_facts the_facts 

242 
> reset_facts; 

243 

244 

245 
(* mode *) 

246 

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

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

249 

250 
val enter_forward = put_mode Forward; 

251 
val enter_forward_chain = put_mode ForwardChain; 

252 
val enter_backward = put_mode Backward; 

253 

254 
fun assert_mode pred state = 

255 
let val mode = get_mode state in 

256 
if pred mode then state 

6731  257 
else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state) 
5820  258 
end; 
259 

260 
fun is_chain state = get_mode state = ForwardChain; 

261 
val assert_forward = assert_mode (equal Forward); 

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

263 
val assert_backward = assert_mode (equal Backward); 

264 

265 

266 
(* blocks *) 

267 

6776  268 
fun level (State (_, nodes)) = length nodes; 
269 

5820  270 
fun open_block (State (node, nodes)) = State (node, node :: nodes); 
271 

272 
fun new_block state = 

273 
state 

274 
> open_block 

275 
> put_goal None; 

276 

6896  277 
fun close_block (state as State (_, node :: nodes)) = 
278 
State (node, nodes) 

279 
> map_context (ProofContext.transfer_used_names (context_of state)) 

5820  280 
 close_block state = raise STATE ("Unbalanced block parentheses", state); 
281 

282 

283 

284 
(** print_state **) 

285 

6982  286 
val show_hyps = ProofContext.show_hyps; 
287 
val pretty_thm = ProofContext.pretty_thm; 

288 

6529  289 
val verbose = ProofContext.verbose; 
290 

6756  291 
fun print_facts _ None = () 
6982  292 
 print_facts s (Some ths) = 
293 
Pretty.writeln (Pretty.big_list (s ^ " facts:") (map pretty_thm ths)); 

6756  294 

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

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

297 
val ref (_, _, begin_goal) = Goals.current_goals_markers; 
5820  298 

299 
fun levels_up 0 = "" 

6932  300 
 levels_up 1 = " (1 level up)" 
5820  301 
 levels_up i = " (" ^ string_of_int i ^ " levels up)"; 
302 

6932  303 
fun print_goal (_, (i, ((kind, name, _), (goal_facts, thm)))) = 
6756  304 
(print_facts "Using" (if null goal_facts then None else Some goal_facts); 
305 
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

306 
Locale.print_goals_marker begin_goal (! goals_limit) thm); 
6848  307 

308 
val ctxt_strings = ProofContext.strings_of_context context; 

5820  309 
in 
6891  310 
if ! verbose then writeln ("Nesting level: " ^ string_of_int (length nodes div 2)) else (); 
5820  311 
writeln ""; 
6798  312 
writeln (mode_name mode ^ " mode"); 
5993  313 
writeln ""; 
6529  314 
if ! verbose orelse mode = Forward then 
6848  315 
(if null ctxt_strings then () else (seq writeln ctxt_strings; writeln ""); 
6756  316 
print_facts "Current" facts; 
6529  317 
print_goal (find_goal 0 state)) 
6756  318 
else if mode = ForwardChain then print_facts "Picking" facts 
6529  319 
else print_goal (find_goal 0 state) 
5820  320 
end; 
321 

322 

323 

324 
(** proof steps **) 

325 

326 
(* datatype method *) 

327 

6848  328 
datatype method = Method of thm list > tactic; 
5820  329 
val method = Method; 
330 

331 

332 
(* refine goal *) 

333 

334 
fun check_sign sg state = 

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

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

337 

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

6848  339 
let 
340 
val Method meth = meth_fun context; 

6932  341 
val (_, (_, (result, (facts, thm)))) = find_goal 0 state; 
5820  342 

6848  343 
fun refn thm' = 
344 
state 

345 
> check_sign (Thm.sign_of_thm thm') 

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

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

5820  348 

349 

6932  350 
(* export *) 
5820  351 

6932  352 
local 
353 

354 
fun varify_frees fixes thm = 

5820  355 
let 
356 
fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None 

357 
 get_free _ (opt, _) = opt; 

358 

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

360 

6887  361 
val {sign, prop, ...} = Thm.rep_thm thm; 
6932  362 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes); 
5820  363 
in 
364 
thm 

365 
> Drule.forall_intr_list frees 

6887  366 
> Drule.forall_elim_vars 0 
5820  367 
end; 
368 

6932  369 
fun most_general_varify_tfrees thm = 
6790  370 
let 
371 
val {hyps, prop, ...} = Thm.rep_thm thm; 

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

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

374 
in thm > Thm.varifyT' leave_tfrees end; 

375 

6932  376 
fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner) 
377 
 diff_context inner (Some outer) = 

378 
(ProofContext.fixed_names inner \\ ProofContext.fixed_names outer, 

379 
Library.drop (length (ProofContext.assumptions outer), ProofContext.assumptions inner)); 

380 

381 
in 

382 

383 
fun export fixes casms thm = 

384 
thm 

385 
> Drule.implies_intr_list casms 

386 
> varify_frees fixes 

387 
> most_general_varify_tfrees; 

388 

389 
fun export_wrt inner opt_outer = 

390 
let 

391 
val (fixes, asms) = diff_context inner opt_outer; 

6996  392 
val casms = map (Drule.mk_cgoal o #1) asms; 
6932  393 
val tacs = map #2 asms; 
394 
in (export fixes casms, tacs) end; 

395 

396 
end; 

5820  397 

6848  398 

6932  399 
(* export results *) 
400 

401 
fun RANGE [] _ = all_tac 

402 
 RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; 

403 

6982  404 
fun export_goal print_rule raw_rule inner state = 
6932  405 
let 
406 
val (outer, (_, (result, (facts, thm)))) = find_goal 0 state; 

6950  407 
val (exp, tacs) = export_wrt inner (Some outer); 
6932  408 
val rule = exp raw_rule; 
6982  409 
val _ = print_rule rule; 
6932  410 
val thmq = FIRSTGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm; 
411 
in Seq.map (fn th => map_goal (K (result, (facts, th))) state) thmq end; 

412 

413 

414 
fun export_thm inner thm = 

415 
let val (exp, tacs) = export_wrt inner None in 

416 
(case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of 

417 
([thm'], _) => thm' 

418 
 ([], _) => raise THM ("export: failed", 0, [thm]) 

419 
 _ => raise THM ("export: more than one result", 0, [thm])) 

420 
end; 

421 

422 

423 
fun export_facts inner_state opt_outer_state state = 

424 
let 

425 
val thms = the_facts inner_state; 

426 
val (exp, tacs) = export_wrt (context_of inner_state) (apsome context_of opt_outer_state); 

427 
val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms; 

428 
in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end; 

429 

430 
fun transfer_facts inner_state state = 

431 
(case get_facts inner_state of 

432 
None => Seq.single (reset_facts state) 

433 
 Some ths => export_facts inner_state (Some state) state); 

434 

435 

436 
(* prepare result *) 

437 

438 
fun prep_result state t raw_thm = 

5820  439 
let 
440 
val ctxt = context_of state; 

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

442 

443 
val ngoals = Thm.nprems_of raw_thm; 

444 
val _ = 

445 
if ngoals = 0 then () 

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

447 

6932  448 
val thm = raw_thm RS Drule.rev_triv_goal; 
449 
val {hyps, prop, sign, maxidx, ...} = Thm.rep_thm thm; 

5820  450 
val tsig = Sign.tsig_of sign; 
6932  451 

452 
val casms = map #1 (assumptions state); 

6996  453 
val bad_hyps = Library.gen_rems Term.aconv (hyps, map (Thm.term_of o Drule.mk_cgoal) casms); 
5820  454 
in 
6932  455 
if not (null bad_hyps) then 
456 
err ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) bad_hyps)) 

5820  457 
(* FIXME else if not (Pattern.matches tsig (t, Logic.skip_flexpairs prop)) then 
458 
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) *) 

6932  459 
else Drule.forall_elim_vars (maxidx + 1) thm 
5820  460 
end; 
461 

462 

463 
(* prepare final result *) 

464 

465 
fun strip_flexflex thm = 

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

467 

468 
fun final_result state pre_thm = 

469 
let 

470 
val thm = 

471 
pre_thm 

472 
> strip_flexflex 

473 
> Thm.strip_shyps 

474 
> Drule.standard; 

475 

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

477 
val xshyps = Thm.extra_shyps thm; 

478 
in 

479 
if not (null xshyps) then 

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

481 
else thm 

482 
end; 

483 

484 

485 

486 
(*** structured proof commands ***) 

487 

488 
(** context **) 

489 

490 
(* bind *) 

491 

492 
fun gen_bind f x state = 

493 
state 

494 
> assert_forward 

495 
> map_context (f x) 

496 
> reset_facts; 

497 

498 
val bind = gen_bind ProofContext.add_binds; 

499 
val bind_i = gen_bind ProofContext.add_binds_i; 

500 

501 
val match_bind = gen_bind ProofContext.match_binds; 

502 
val match_bind_i = gen_bind ProofContext.match_binds_i; 

503 

504 

6091  505 
(* have_thmss *) 
5820  506 

6876  507 
fun have_thmss ths name atts ths_atts state = 
5820  508 
state 
509 
> assert_forward 

6876  510 
> map_context_result (ProofContext.have_thmss ths (PureThy.default_name name) atts ths_atts) 
5820  511 
> these_facts; 
512 

6876  513 
fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])]; 
514 

5820  515 

516 
(* fix *) 

517 

518 
fun gen_fix f xs state = 

519 
state 

520 
> assert_forward 

521 
> map_context (f xs) 

522 
> reset_facts; 

523 

524 
val fix = gen_fix ProofContext.fix; 

525 
val fix_i = gen_fix ProofContext.fix_i; 

526 

527 

528 
(* assume *) 

529 

6932  530 
fun gen_assume f tacs name atts props state = 
5820  531 
state 
532 
> assert_forward 

6932  533 
> map_context_result (f tacs (PureThy.default_name name) atts props) 
6798  534 
> (fn (st, (facts, prems)) => 
535 
(st, facts) 

536 
> these_facts 

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

5820  538 

6932  539 
val assm = gen_assume ProofContext.assume; 
540 
val assm_i = gen_assume ProofContext.assume_i; 

541 

6996  542 
val hard_asm_tac = Tactic.etac Drule.triv_goal; 
543 
val soft_asm_tac = Tactic.rtac Drule.triv_goal; 

544 

545 
val assume = assm (hard_asm_tac, soft_asm_tac); 

546 
val assume_i = assm_i (hard_asm_tac, soft_asm_tac); 

547 
val presume = assm (soft_asm_tac, soft_asm_tac); 

548 
val presume_i = assm_i (soft_asm_tac, soft_asm_tac); 

5820  549 

550 

551 

552 
(** goals **) 

553 

554 
(* forward chaining *) 

555 

556 
fun chain state = 

557 
state 

558 
> assert_forward 

6848  559 
> assert_facts 
5820  560 
> enter_forward_chain; 
561 

6932  562 
fun export_chain state = 
563 
state 

564 
> assert_forward 

565 
> export_facts state None 

566 
> Seq.map chain; 

567 

5820  568 
fun from_facts facts state = 
569 
state 

570 
> put_facts (Some facts) 

571 
> chain; 

572 

573 

574 
(* setup goals *) 

575 

5936  576 
fun setup_goal opt_block prepp kind name atts raw_propp state = 
5820  577 
let 
6932  578 
val (state', prop) = 
5936  579 
state 
580 
> assert_forward_or_chain 

581 
> enter_forward 

582 
> opt_block 

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

6932  584 
val cprop = Thm.cterm_of (sign_of state') prop; 
585 
val casms = map #1 (assumptions state'); 

5820  586 

6932  587 
val revcut_rl = Drule.incr_indexes_wrt [] [] (cprop :: casms) [] Drule.revcut_rl; 
6996  588 
fun cut_asm (casm, thm) = Thm.rotate_rule ~1 1 ((Drule.assume_goal casm COMP revcut_rl) RS thm); 
6932  589 
val goal = foldr cut_asm (casms, Drule.mk_triv_goal cprop); 
5820  590 
in 
5936  591 
state' 
6932  592 
> put_goal (Some ((kind atts, (PureThy.default_name name), prop), ([], goal))) 
6790  593 
> auto_bind_goal prop 
5820  594 
> (if is_chain state then use_facts else reset_facts) 
595 
> new_block 

596 
> enter_backward 

597 
end; 

598 

599 

600 
(*global goals*) 

601 
fun global_goal prep kind name atts x thy = 

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

603 

5936  604 
val theorem = global_goal ProofContext.bind_propp Theorem; 
605 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

606 
val lemma = global_goal ProofContext.bind_propp Lemma; 

607 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  608 

609 

610 
(*local goals*) 

611 
fun local_goal prep kind name atts x = 

612 
setup_goal open_block prep kind name atts x; 

613 

5936  614 
val show = local_goal ProofContext.bind_propp Goal; 
615 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

616 
val have = local_goal ProofContext.bind_propp Aux; 

617 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  618 

619 

620 

621 
(** conclusions **) 

622 

623 
(* current goal *) 

624 

6950  625 
fun current_goal (State ({context, goal = Some goal, ...}, _)) = (context, goal) 
5820  626 
 current_goal state = raise STATE ("No current goal!", state); 
627 

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

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

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

632 
 assert_current_goal _ state = state; 

5820  633 

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

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

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

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

638 
 assert_bottom _ state = state; 

639 

6404  640 
val at_bottom = can (assert_bottom true o close_block); 
641 

6932  642 
fun end_proof bot state = 
5820  643 
state 
644 
> assert_forward 

645 
> close_block 

646 
> assert_bottom bot 

7011  647 
> assert_current_goal true 
648 
> goal_facts (K []); 

5820  649 

650 

6404  651 
(* local_qed *) 
5820  652 

6982  653 
fun finish_local (print_result, print_rule) state = 
5820  654 
let 
6950  655 
val (ctxt, ((kind, name, t), (_, raw_thm))) = current_goal state; 
6932  656 
val result = prep_result state t raw_thm; 
5820  657 
val (atts, opt_solve) = 
658 
(case kind of 

6982  659 
Goal atts => (atts, export_goal print_rule result ctxt) 
5820  660 
 Aux atts => (atts, Seq.single) 
6932  661 
 _ => err_malformed "finish_local" state); 
5820  662 
in 
6731  663 
print_result {kind = kind_name kind, name = name, thm = result}; 
5820  664 
state 
665 
> close_block 

6871  666 
> auto_bind_facts name [t] 
6876  667 
> have_thmss [] name atts [Thm.no_attributes [result]] 
5820  668 
> opt_solve 
669 
end; 

670 

6982  671 
fun local_qed finalize print state = 
6404  672 
state 
6932  673 
> end_proof false 
6871  674 
> finalize 
6982  675 
> (Seq.flat o Seq.map (finish_local print)); 
5820  676 

677 

6404  678 
(* global_qed *) 
5820  679 

6950  680 
fun finish_global state = 
5820  681 
let 
6950  682 
val (_, ((kind, name, t), (_, raw_thm))) = current_goal state; 
6932  683 
val result = final_result state (prep_result state t raw_thm); 
5820  684 

685 
val atts = 

686 
(case kind of 

6950  687 
Theorem atts => atts 
688 
 Lemma atts => atts @ [Drule.tag_lemma] 

6932  689 
 _ => err_malformed "finish_global" state); 
5820  690 

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

6871  694 
(*Note: should inspect first result only, backtracking may destroy theory*) 
6950  695 
fun global_qed finalize state = 
5820  696 
state 
6932  697 
> end_proof true 
6871  698 
> finalize 
6950  699 
> Seq.map finish_global; 
5820  700 

701 

6896  702 

703 
(** blocks **) 

704 

705 
(* begin_block *) 

706 

707 
fun begin_block state = 

708 
state 

709 
> assert_forward 

710 
> new_block 

711 
> open_block; 

712 

713 

714 
(* end_block *) 

715 

716 
fun end_block state = 

717 
state 

718 
> assert_forward 

719 
> close_block 

720 
> assert_current_goal false 

721 
> close_block 

6932  722 
> transfer_facts state; 
6896  723 

724 

725 
(* next_block *) 

726 

727 
fun next_block state = 

728 
state 

729 
> assert_forward 

730 
> close_block 

6932  731 
> assert_current_goal true 
6896  732 
> new_block; 
733 

734 

5820  735 
end; 