author  wenzelm 
Wed, 08 Mar 2000 18:02:36 +0100  
changeset 8374  ffb2eb084078 
parent 8239  07f25f7d2218 
child 8383  2dd4823c744f 
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 

8152  8 
signature BASIC_PROOF = 
9 
sig 

8374  10 
val FINDGOAL: (int > thm > 'a Seq.seq) > thm > 'a Seq.seq 
11 
val HEADGOAL: (int > thm > 'a Seq.seq) > thm > 'a Seq.seq 

8152  12 
end; 
13 

5820  14 
signature PROOF = 
15 
sig 

8152  16 
include BASIC_PROOF 
5820  17 
type context 
18 
type state 

19 
exception STATE of string * state 

6871  20 
val check_result: string > state > 'a Seq.seq > 'a Seq.seq 
7011  21 
val init_state: theory > state 
5820  22 
val context_of: state > context 
23 
val theory_of: state > theory 

24 
val sign_of: state > Sign.sg 

7924  25 
val warn_extra_tfrees: state > state > state 
7605  26 
val reset_thms: string > state > state 
6091  27 
val the_facts: state > thm list 
7665  28 
val get_goal: state > term * (thm list * thm) 
6091  29 
val goal_facts: (state > thm list) > state > state 
5820  30 
val use_facts: state > state 
31 
val reset_facts: state > state 

6891  32 
val assert_forward: state > state 
5820  33 
val assert_backward: state > state 
8206  34 
val assert_no_chain: state > state 
5820  35 
val enter_forward: state > state 
6982  36 
val show_hyps: bool ref 
37 
val pretty_thm: thm > Pretty.T 

7412  38 
val pretty_thms: thm list > Pretty.T 
6529  39 
val verbose: bool ref 
7201  40 
val print_state: int > state > unit 
6776  41 
val level: state > int 
5820  42 
type method 
6848  43 
val method: (thm list > tactic) > method 
8374  44 
val method_cases: (thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq) > method 
5820  45 
val refine: (context > method) > state > state Seq.seq 
8234  46 
val refine_end: (context > method) > state > state Seq.seq 
7669  47 
val find_free: term > string > term option 
6932  48 
val export_thm: context > thm > thm 
5936  49 
val match_bind: (string list * string) list > state > state 
50 
val match_bind_i: (term list * term) list > state > state 

6876  51 
val have_thmss: thm list > string > context attribute list > 
6091  52 
(thm list * context attribute list) list > state > state 
6876  53 
val simple_have_thms: string > thm list > state > state 
7412  54 
val fix: (string list * string option) list > state > state 
7665  55 
val fix_i: (string list * typ option) list > state > state 
7271  56 
val assm: (int > tactic) * (int > tactic) 
57 
> (string * context attribute list * (string * (string list * string list)) list) list 

58 
> state > state 

59 
val assm_i: (int > tactic) * (int > tactic) 

60 
> (string * context attribute list * (term * (term list * term list)) list) list 

6932  61 
> state > state 
7271  62 
val assume: (string * context attribute list * (string * (string list * string list)) list) list 
63 
> state > state 

64 
val assume_i: (string * context attribute list * (term * (term list * term list)) list) list 

6932  65 
> state > state 
7271  66 
val presume: (string * context attribute list * (string * (string list * string list)) list) list 
6932  67 
> state > state 
7271  68 
val presume_i: (string * context attribute list * (term * (term list * term list)) list) list 
6932  69 
> state > state 
8374  70 
val invoke_case: string > state > state 
6932  71 
val theorem: bstring > theory attribute list > string * (string list * string list) 
72 
> theory > state 

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

74 
> theory > state 

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

76 
> theory > state 

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

78 
> theory > state 

5820  79 
val chain: state > state 
6932  80 
val export_chain: state > state Seq.seq 
6091  81 
val from_facts: thm list > state > state 
7176  82 
val show: (state > state Seq.seq) > string > context attribute list 
83 
> string * (string list * string list) > state > state 

84 
val show_i: (state > state Seq.seq) > string > context attribute list 

85 
> term * (term list * term list) > state > state 

86 
val have: (state > state Seq.seq) > string > context attribute list 

87 
> string * (string list * string list) > state > state 

88 
val have_i: (state > state Seq.seq) > string > context attribute list 

89 
> term * (term list * term list) > state > state 

6404  90 
val at_bottom: state > bool 
6982  91 
val local_qed: (state > state Seq.seq) 
92 
> ({kind: string, name: string, thm: thm} > unit) * (thm > unit) > state > state Seq.seq 

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

6896  95 
val begin_block: state > state 
6932  96 
val end_block: state > state Seq.seq 
6896  97 
val next_block: state > state 
5820  98 
end; 
99 

8152  100 
signature PRIVATE_PROOF = 
5820  101 
sig 
102 
include PROOF 

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

104 
end; 

105 

8152  106 
structure Proof: PRIVATE_PROOF = 
5820  107 
struct 
108 

109 

110 
(** proof state **) 

111 

112 
type context = ProofContext.context; 

113 

114 

115 
(* type goal *) 

116 

117 
datatype kind = 

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

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

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

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

122 

123 
val kind_name = 

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

126 
type goal = 

6932  127 
(kind * (*result kind*) 
128 
string * (*result name*) 

129 
term) * (*result statement*) 

130 
(thm list * (*use facts*) 

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

5820  132 

133 

134 
(* type mode *) 

135 

136 
datatype mode = Forward  ForwardChain  Backward; 

7201  137 
val mode_name = (fn Forward => "state"  ForwardChain => "chain"  Backward => "prove"); 
5820  138 

139 

140 
(* datatype state *) 

141 

7176  142 
datatype node = 
143 
Node of 

144 
{context: context, 

145 
facts: thm list option, 

146 
mode: mode, 

147 
goal: (goal * (state > state Seq.seq)) option} 

148 
and state = 

5820  149 
State of 
150 
node * (*current*) 

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

152 

7176  153 
fun make_node (context, facts, mode, goal) = 
154 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

155 

156 

5820  157 
exception STATE of string * state; 
158 

159 
fun err_malformed name state = 

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

161 

6871  162 
fun check_result msg state sq = 
163 
(case Seq.pull sq of 

164 
None => raise STATE (msg, state) 

165 
 Some s_sq => Seq.cons s_sq); 

166 

5820  167 

7176  168 
fun map_current f (State (Node {context, facts, mode, goal}, nodes)) = 
5820  169 
State (make_node (f (context, facts, mode, goal)), nodes); 
170 

171 
fun init_state thy = 

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

174 

175 

176 
(** basic proof state operations **) 

177 

178 
(* context *) 

179 

7176  180 
fun context_of (State (Node {context, ...}, _)) = context; 
5820  181 
val theory_of = ProofContext.theory_of o context_of; 
182 
val sign_of = ProofContext.sign_of o context_of; 

183 

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

185 

7176  186 
fun map_context_result f (state as State (Node {context, facts, mode, goal}, nodes)) = 
5820  187 
let val (context', result) = f context 
188 
in (State (make_node (context', facts, mode, goal), nodes), result) end; 

189 

190 

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

7924  192 
val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of; 
6790  193 
val auto_bind_goal = map_context o ProofContext.auto_bind_goal; 
6798  194 
val auto_bind_facts = map_context oo ProofContext.auto_bind_facts; 
6091  195 
val put_thms = map_context o ProofContext.put_thms; 
196 
val put_thmss = map_context o ProofContext.put_thmss; 

7605  197 
val reset_thms = map_context o ProofContext.reset_thms; 
6932  198 
val assumptions = ProofContext.assumptions o context_of; 
8374  199 
val get_case = ProofContext.get_case o context_of; 
5820  200 

201 

202 
(* facts *) 

203 

7176  204 
fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts 
5820  205 
 the_facts state = raise STATE ("No current facts available", state); 
206 

6848  207 
fun assert_facts state = (the_facts state; state); 
7176  208 
fun get_facts (State (Node {facts, ...}, _)) = facts; 
6848  209 

7605  210 

211 
val thisN = "this"; 

212 

5820  213 
fun put_facts facts state = 
214 
state 

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

7605  216 
> (case facts of None => reset_thms thisN  Some ths => put_thms (thisN, ths)); 
5820  217 

218 
val reset_facts = put_facts None; 

219 

220 
fun have_facts (name, facts) state = 

221 
state 

222 
> put_facts (Some facts) 

6798  223 
> put_thms (name, facts); 
5820  224 

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

226 

227 

228 
(* goal *) 

229 

7176  230 
fun find_goal i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) 
231 
 find_goal i (State (Node {goal = None, ...}, node :: nodes)) = 

5820  232 
find_goal (i + 1) (State (node, nodes)) 
233 
 find_goal _ (state as State (_, [])) = err_malformed "find_goal" state; 

234 

7176  235 
fun get_goal state = 
7665  236 
let val (_, (_, (((_, _, t), goal), _))) = find_goal 0 state 
237 
in (t, goal) end; 

7176  238 

5820  239 
fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); 
240 

8374  241 
fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) = 
242 
State (make_node (f context, facts, mode, Some (g goal)), nodes) 

243 
 map_goal f g (State (nd, node :: nodes)) = 

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

245 
in map_context f (State (nd, node' :: nodes')) end 

246 
 map_goal _ _ state = state; 

5820  247 

248 
fun goal_facts get state = 

249 
state 

8374  250 
> map_goal I (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f)); 
5820  251 

252 
fun use_facts state = 

253 
state 

254 
> goal_facts the_facts 

255 
> reset_facts; 

256 

257 

258 
(* mode *) 

259 

7176  260 
fun get_mode (State (Node {mode, ...}, _)) = mode; 
5820  261 
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); 
262 

263 
val enter_forward = put_mode Forward; 

264 
val enter_forward_chain = put_mode ForwardChain; 

265 
val enter_backward = put_mode Backward; 

266 

267 
fun assert_mode pred state = 

268 
let val mode = get_mode state in 

269 
if pred mode then state 

8239  270 
else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state) 
5820  271 
end; 
272 

273 
fun is_chain state = get_mode state = ForwardChain; 

274 
val assert_forward = assert_mode (equal Forward); 

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

276 
val assert_backward = assert_mode (equal Backward); 

8206  277 
val assert_no_chain = assert_mode (not_equal ForwardChain); 
5820  278 

279 

280 
(* blocks *) 

281 

6776  282 
fun level (State (_, nodes)) = length nodes; 
283 

5820  284 
fun open_block (State (node, nodes)) = State (node, node :: nodes); 
285 

286 
fun new_block state = 

287 
state 

288 
> open_block 

289 
> put_goal None; 

290 

7487
c0f9b956a3e7
close_block: removed ProofContext.transfer_used_names;
wenzelm
parents:
7478
diff
changeset

291 
fun close_block (state as State (_, node :: nodes)) = State (node, nodes) 
5820  292 
 close_block state = raise STATE ("Unbalanced block parentheses", state); 
293 

294 

295 

296 
(** print_state **) 

297 

6982  298 
val show_hyps = ProofContext.show_hyps; 
299 
val pretty_thm = ProofContext.pretty_thm; 

300 

7412  301 
fun pretty_thms [th] = pretty_thm th 
7580  302 
 pretty_thms ths = Pretty.blk (0, Pretty.fbreaks (map pretty_thm ths)); 
7412  303 

304 

6529  305 
val verbose = ProofContext.verbose; 
306 

6756  307 
fun print_facts _ None = () 
6982  308 
 print_facts s (Some ths) = 
7575  309 
(Pretty.writeln (Pretty.big_list (s ^ "this:") (map pretty_thm ths)); writeln ""); 
6756  310 

7201  311 
fun print_state nr (state as State (Node {context, facts, mode, goal = _}, nodes)) = 
5820  312 
let 
5945
63184e276c1d
print_state: use begin_goal from Goals.current_goals_markers;
wenzelm
parents:
5936
diff
changeset

313 
val ref (_, _, begin_goal) = Goals.current_goals_markers; 
5820  314 

315 
fun levels_up 0 = "" 

7575  316 
 levels_up 1 = ", 1 level up" 
317 
 levels_up i = ", " ^ string_of_int i ^ " levels up"; 

5820  318 

7176  319 
fun print_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = 
7575  320 
(print_facts "using " 
7412  321 
(if mode <> Backward orelse null goal_facts then None else Some goal_facts); 
7575  322 
writeln ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^ 
323 
levels_up (i div 2) ^ "):"); 

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

324 
Locale.print_goals_marker begin_goal (! goals_limit) thm); 
6848  325 

7575  326 
val ctxt_strings = 
327 
if ! verbose orelse mode = Forward then ProofContext.strings_of_context context 

328 
else if mode = Backward then ProofContext.strings_of_prems context 

329 
else []; 

5820  330 
in 
7201  331 
writeln ("Proof(" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ 
332 
", depth " ^ string_of_int (length nodes div 2)); 

5993  333 
writeln ""; 
7575  334 
if null ctxt_strings then () else (seq writeln ctxt_strings; writeln ""); 
6529  335 
if ! verbose orelse mode = Forward then 
7575  336 
(print_facts "" facts; print_goal (find_goal 0 state)) 
337 
else if mode = ForwardChain then print_facts "picking " facts 

6529  338 
else print_goal (find_goal 0 state) 
5820  339 
end; 
340 

341 

342 

343 
(** proof steps **) 

344 

345 
(* datatype method *) 

346 

8374  347 
datatype method = 
348 
Method of thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq; 

349 

350 
fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st)); 

351 
val method_cases = Method; 

5820  352 

353 

354 
(* refine goal *) 

355 

8234  356 
local 
357 

5820  358 
fun check_sign sg state = 
359 
if Sign.subsig (sg, sign_of state) then state 

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

361 

8234  362 
fun gen_refine current_context meth_fun state = 
6848  363 
let 
8234  364 
val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal 0 state; 
365 
val Method meth = meth_fun (if current_context then context_of state else goal_ctxt); 

5820  366 

8374  367 
fun refn (thm', cases) = 
6848  368 
state 
369 
> check_sign (Thm.sign_of_thm thm') 

8374  370 
> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), f)); 
6848  371 
in Seq.map refn (meth facts thm) end; 
5820  372 

8234  373 
in 
374 

375 
val refine = gen_refine true; 

376 
val refine_end = gen_refine false; 

377 

378 
end; 

379 

5820  380 

6932  381 
(* export *) 
5820  382 

7669  383 
fun get_free x (None, t as Free (y, _)) = if x = y then Some t else None 
384 
 get_free _ (opt, _) = opt; 

385 

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

387 

388 

6932  389 
local 
390 

391 
fun varify_frees fixes thm = 

5820  392 
let 
6887  393 
val {sign, prop, ...} = Thm.rep_thm thm; 
6932  394 
val frees = map (Thm.cterm_of sign) (mapfilter (find_free prop) fixes); 
5820  395 
in 
396 
thm 

397 
> Drule.forall_intr_list frees 

6887  398 
> Drule.forall_elim_vars 0 
5820  399 
end; 
400 

8152  401 
fun export fixes casms thm = 
402 
thm 

403 
> Drule.implies_intr_list casms 

404 
> varify_frees fixes 

8186  405 
> ProofContext.most_general_varify_tfrees; 
8152  406 

6932  407 
fun diff_context inner None = (ProofContext.fixed_names inner, ProofContext.assumptions inner) 
408 
 diff_context inner (Some outer) = 

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

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

411 

412 
in 

413 

414 
fun export_wrt inner opt_outer = 

415 
let 

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

6996  417 
val casms = map (Drule.mk_cgoal o #1) asms; 
6932  418 
val tacs = map #2 asms; 
419 
in (export fixes casms, tacs) end; 

420 

421 
end; 

5820  422 

6848  423 

6932  424 
(* export results *) 
425 

426 
fun RANGE [] _ = all_tac 

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

428 

8152  429 
fun FINDGOAL tac st = 
8374  430 
let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n)) 
431 
in find (1, Thm.nprems_of st) st end; 

8152  432 

8166  433 
fun HEADGOAL tac = tac 1; 
434 

6982  435 
fun export_goal print_rule raw_rule inner state = 
6932  436 
let 
7176  437 
val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state; 
6950  438 
val (exp, tacs) = export_wrt inner (Some outer); 
6932  439 
val rule = exp raw_rule; 
6982  440 
val _ = print_rule rule; 
8152  441 
val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm; 
8374  442 
in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; 
6932  443 

444 

445 
fun export_thm inner thm = 

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

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

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

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

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

451 
end; 

452 

453 

454 
fun export_facts inner_state opt_outer_state state = 

455 
let 

456 
val thms = the_facts inner_state; 

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

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

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

460 

461 
fun transfer_facts inner_state state = 

462 
(case get_facts inner_state of 

463 
None => Seq.single (reset_facts state) 

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

465 

466 

467 
(* prepare result *) 

468 

469 
fun prep_result state t raw_thm = 

5820  470 
let 
471 
val ctxt = context_of state; 

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

473 

474 
val ngoals = Thm.nprems_of raw_thm; 

475 
val _ = 

476 
if ngoals = 0 then () 

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

478 

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

5820  481 
val tsig = Sign.tsig_of sign; 
6932  482 

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

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

7605  488 
else if not (t aconv prop) then 
489 
err ("Proved a different theorem: " ^ Sign.string_of_term sign prop) 

8186  490 
else thm > Drule.forall_elim_vars (maxidx + 1) > ProofContext.most_general_varify_tfrees 
5820  491 
end; 
492 

493 

494 

495 
(*** structured proof commands ***) 

496 

497 
(** context **) 

498 

499 
(* bind *) 

500 

501 
fun gen_bind f x state = 

502 
state 

503 
> assert_forward 

504 
> map_context (f x) 

505 
> reset_facts; 

506 

8095  507 
val match_bind = gen_bind ProofContext.match_bind; 
508 
val match_bind_i = gen_bind ProofContext.match_bind_i; 

5820  509 

510 

6091  511 
(* have_thmss *) 
5820  512 

6876  513 
fun have_thmss ths name atts ths_atts state = 
5820  514 
state 
515 
> assert_forward 

7478  516 
> map_context_result (ProofContext.have_thmss ths name atts ths_atts) 
5820  517 
> these_facts; 
518 

6876  519 
fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])]; 
520 

5820  521 

522 
(* fix *) 

523 

524 
fun gen_fix f xs state = 

525 
state 

526 
> assert_forward 

527 
> map_context (f xs) 

528 
> reset_facts; 

529 

530 
val fix = gen_fix ProofContext.fix; 

531 
val fix_i = gen_fix ProofContext.fix_i; 

532 

533 

534 
(* assume *) 

535 

7271  536 
local 
537 

538 
fun gen_assume f tac args state = 

5820  539 
state 
540 
> assert_forward 

7478  541 
> map_context_result (f tac args) 
7271  542 
> (fn (st, (factss, prems)) => 
543 
foldl these_facts (st, factss) 

544 
> put_thms ("prems", prems) 

545 
> put_facts (Some (flat (map #2 factss)))); 

6932  546 

6996  547 
val hard_asm_tac = Tactic.etac Drule.triv_goal; 
548 
val soft_asm_tac = Tactic.rtac Drule.triv_goal; 

549 

7271  550 
in 
551 

552 
val assm = gen_assume ProofContext.assume; 

553 
val assm_i = gen_assume ProofContext.assume_i; 

6996  554 
val assume = assm (hard_asm_tac, soft_asm_tac); 
555 
val assume_i = assm_i (hard_asm_tac, soft_asm_tac); 

556 
val presume = assm (soft_asm_tac, soft_asm_tac); 

557 
val presume_i = assm_i (soft_asm_tac, soft_asm_tac); 

5820  558 

7271  559 
end; 
560 

5820  561 

8374  562 
(* invoke_case *) 
563 

564 
fun invoke_case name state = 

565 
let val (vars, props) = get_case state name in 

566 
state 

567 
> fix_i (map (fn (x, T) => ([x], Some T)) vars) 

568 
> assume_i [("", [], map (fn t => (t, ([], []))) props)] 

569 
end; 

570 

571 

5820  572 

573 
(** goals **) 

574 

575 
(* forward chaining *) 

576 

577 
fun chain state = 

578 
state 

579 
> assert_forward 

6848  580 
> assert_facts 
5820  581 
> enter_forward_chain; 
582 

6932  583 
fun export_chain state = 
584 
state 

585 
> assert_forward 

586 
> export_facts state None 

587 
> Seq.map chain; 

588 

5820  589 
fun from_facts facts state = 
590 
state 

591 
> put_facts (Some facts) 

592 
> chain; 

593 

594 

595 
(* setup goals *) 

596 

7176  597 
fun setup_goal opt_block prepp kind after_qed name atts raw_propp state = 
5820  598 
let 
7928  599 
val (state', prop) = 
5936  600 
state 
601 
> assert_forward_or_chain 

602 
> enter_forward 

8095  603 
> map_context_result (fn ct => prepp (ct, raw_propp)); 
6932  604 
val cprop = Thm.cterm_of (sign_of state') prop; 
7556  605 
val goal = Drule.mk_triv_goal cprop; 
5820  606 
in 
5936  607 
state' 
7412  608 
> opt_block 
7478  609 
> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed)) 
6790  610 
> auto_bind_goal prop 
5820  611 
> (if is_chain state then use_facts else reset_facts) 
612 
> new_block 

613 
> enter_backward 

614 
end; 

615 

616 

617 
(*global goals*) 

8095  618 
fun global_goal prepp kind name atts x thy = 
619 
setup_goal I prepp kind Seq.single name atts x (init_state thy); 

5820  620 

7928  621 
val theorem = global_goal ProofContext.bind_propp Theorem; 
622 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

623 
val lemma = global_goal ProofContext.bind_propp Lemma; 

624 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  625 

626 

627 
(*local goals*) 

8095  628 
fun local_goal prepp kind f name atts args state = 
7928  629 
state 
8095  630 
> setup_goal open_block prepp kind f name atts args 
7928  631 
> warn_extra_tfrees state; 
5820  632 

7928  633 
val show = local_goal ProofContext.bind_propp Goal; 
634 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

635 
val have = local_goal ProofContext.bind_propp Aux; 

636 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  637 

638 

639 

640 
(** conclusions **) 

641 

642 
(* current goal *) 

643 

7176  644 
fun current_goal (State (Node {context, goal = Some goal, ...}, _)) = (context, goal) 
5820  645 
 current_goal state = raise STATE ("No current goal!", state); 
646 

7176  647 
fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) = 
6404  648 
raise STATE ("No goal in this block!", state) 
7176  649 
 assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) = 
6404  650 
raise STATE ("Goal present in this block!", state) 
651 
 assert_current_goal _ state = state; 

5820  652 

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

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

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

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

657 
 assert_bottom _ state = state; 

658 

6404  659 
val at_bottom = can (assert_bottom true o close_block); 
660 

6932  661 
fun end_proof bot state = 
5820  662 
state 
663 
> assert_forward 

664 
> close_block 

665 
> assert_bottom bot 

7011  666 
> assert_current_goal true 
667 
> goal_facts (K []); 

5820  668 

669 

6404  670 
(* local_qed *) 
5820  671 

6982  672 
fun finish_local (print_result, print_rule) state = 
5820  673 
let 
7176  674 
val (ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state; 
6932  675 
val result = prep_result state t raw_thm; 
5820  676 
val (atts, opt_solve) = 
677 
(case kind of 

6982  678 
Goal atts => (atts, export_goal print_rule result ctxt) 
5820  679 
 Aux atts => (atts, Seq.single) 
6932  680 
 _ => err_malformed "finish_local" state); 
5820  681 
in 
6731  682 
print_result {kind = kind_name kind, name = name, thm = result}; 
5820  683 
state 
684 
> close_block 

6871  685 
> auto_bind_facts name [t] 
6876  686 
> have_thmss [] name atts [Thm.no_attributes [result]] 
5820  687 
> opt_solve 
7176  688 
> (Seq.flat o Seq.map after_qed) 
5820  689 
end; 
690 

6982  691 
fun local_qed finalize print state = 
6404  692 
state 
6932  693 
> end_proof false 
6871  694 
> finalize 
6982  695 
> (Seq.flat o Seq.map (finish_local print)); 
5820  696 

697 

6404  698 
(* global_qed *) 
5820  699 

6950  700 
fun finish_global state = 
5820  701 
let 
7176  702 
val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*) 
8152  703 
val result = Drule.standard (prep_result state t raw_thm); 
5820  704 

705 
val atts = 

706 
(case kind of 

6950  707 
Theorem atts => atts 
708 
 Lemma atts => atts @ [Drule.tag_lemma] 

6932  709 
 _ => err_malformed "finish_global" state); 
5820  710 

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

6871  714 
(*Note: should inspect first result only, backtracking may destroy theory*) 
6950  715 
fun global_qed finalize state = 
5820  716 
state 
6932  717 
> end_proof true 
6871  718 
> finalize 
6950  719 
> Seq.map finish_global; 
5820  720 

721 

6896  722 

723 
(** blocks **) 

724 

725 
(* begin_block *) 

726 

727 
fun begin_block state = 

728 
state 

729 
> assert_forward 

730 
> new_block 

731 
> open_block; 

732 

733 

734 
(* end_block *) 

735 

736 
fun end_block state = 

737 
state 

738 
> assert_forward 

739 
> close_block 

740 
> assert_current_goal false 

741 
> close_block 

6932  742 
> transfer_facts state; 
6896  743 

744 

745 
(* next_block *) 

746 

747 
fun next_block state = 

748 
state 

749 
> assert_forward 

750 
> close_block 

6932  751 
> assert_current_goal true 
6896  752 
> new_block; 
753 

754 

5820  755 
end; 
8152  756 

757 

758 
structure BasicProof: BASIC_PROOF = Proof; 

759 
open BasicProof; 