author  wenzelm 
Thu, 17 Dec 1998 17:45:51 +0100  
changeset 6030  f29d4e507564 
parent 6001  28b0a9891852 
child 6091  e3cdbd929a24 
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 

25 
val the_facts: state > tthm list 

26 
val goal_facts: (state > tthm list) > state > state 

27 
val use_facts: state > state 

28 
val reset_facts: state > state 

29 
val assert_backward: state > state 

30 
val enter_forward: state > state 

31 
val print_state: state > unit 

32 
type method 

33 
val method: (tthm list > thm > 

34 
(thm * (indexname * term) list * (string * tthm list) list) Seq.seq) > method 

35 
val refine: (context > method) > state > state Seq.seq 

36 
val bind: (indexname * string) list > state > state 

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

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

5918  40 
val have_tthmss: string > context attribute list > 
41 
(tthm list * context attribute list) list > state > state 

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

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

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

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

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

5820  50 
val chain: state > state 
51 
val from_facts: tthm list > state > state 

5936  52 
val show: string > context attribute list > string * string list > state > state 
53 
val show_i: string > context attribute list > term * term list > state > state 

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

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

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

58 
val end_block: (context > method) > state > state Seq.seq 

59 
val qed: (context > method) > bstring option > theory attribute list option > state 

60 
> theory * (string * string * tthm) 

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 = 

90 
(kind * (*result kind*) 

91 
string * (*result name*) 

92 
cterm list * (*result assumptions*) 

93 
term) * (*result statement*) 

94 
(tthm list * (*use facts*) 

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

96 

97 

98 
(* type mode *) 

99 

100 
datatype mode = Forward  ForwardChain  Backward; 

101 

102 
val mode_name = 

6030  103 
fn Forward => "state"  ForwardChain => "chain"  Backward => "prove"; 
5820  104 

105 

106 
(* type node *) 

107 

108 
type node = 

109 
{context: context, 

110 
facts: tthm list option, 

111 
mode: mode, 

112 
goal: goal option}; 

113 

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

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

116 

117 

118 
(* datatype state *) 

119 

120 
datatype state = 

121 
State of 

122 
node * (*current*) 

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

124 

125 
exception STATE of string * state; 

126 

127 
fun err_malformed name state = 

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

129 

130 

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

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

133 

134 
fun init_state thy = 

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

137 

138 

139 
(** basic proof state operations **) 

140 

141 
(* context *) 

142 

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

144 
val theory_of = ProofContext.theory_of o context_of; 

145 
val sign_of = ProofContext.sign_of o context_of; 

146 

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

148 

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

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

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

152 

153 

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

155 
val declare_term = map_context o ProofContext.declare_term; 

156 
val add_binds = map_context o ProofContext.add_binds_i; 

157 
val put_tthms = map_context o ProofContext.put_tthms; 

158 
val put_tthmss = map_context o ProofContext.put_tthmss; 

159 

160 

161 
(* bind statements *) 

162 

163 
fun bind_props bs state = 

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

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

166 

167 
fun bind_tthms (name, tthms) state = 

168 
let 

169 
val props = map (#prop o Thm.rep_thm o Attribute.thm_of) tthms; 

170 
val named_props = 

171 
(case props of 

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

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

174 
in state > bind_props named_props end; 

175 

176 
fun let_tthms name_tthms state = 

177 
state 

178 
> put_tthms name_tthms 

179 
> bind_tthms name_tthms; 

180 

181 

182 
(* facts *) 

183 

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

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

186 

187 
fun put_facts facts state = 

188 
state 

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

190 
> let_tthms ("facts", if_none facts []); 

191 

192 
val reset_facts = put_facts None; 

193 

194 
fun have_facts (name, facts) state = 

195 
state 

196 
> put_facts (Some facts) 

197 
> let_tthms (name, facts); 

198 

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

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

201 

202 

203 
(* goal *) 

204 

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

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

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

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

209 

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

211 

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

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

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

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

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

217 
 map_goal _ state = state; 

218 

219 
fun goal_facts get state = 

220 
state 

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

222 

223 
fun use_facts state = 

224 
state 

225 
> goal_facts the_facts 

226 
> reset_facts; 

227 

228 

229 
(* mode *) 

230 

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

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

233 

234 
val enter_forward = put_mode Forward; 

235 
val enter_forward_chain = put_mode ForwardChain; 

236 
val enter_backward = put_mode Backward; 

237 

238 
fun assert_mode pred state = 

239 
let val mode = get_mode state in 

240 
if pred mode then state 

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

242 
end; 

243 

244 
fun is_chain state = get_mode state = ForwardChain; 

245 
val assert_forward = assert_mode (equal Forward); 

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

247 
val assert_backward = assert_mode (equal Backward); 

248 

249 

250 
(* blocks *) 

251 

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

253 

254 
fun new_block state = 

255 
state 

256 
> open_block 

257 
> put_goal None; 

258 

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

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

261 

262 

263 

264 
(** print_state **) 

265 

266 
fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) = 

267 
let 

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

268 
val ref (_, _, begin_goal) = Goals.current_goals_markers; 
5820  269 
val prt_tthm = Attribute.pretty_tthm; 
270 

271 
fun print_facts None = () 

272 
 print_facts (Some ths) = 

273 
Pretty.writeln (Pretty.big_list "Current facts:" (map prt_tthm ths)); 

274 

275 
fun levels_up 0 = "" 

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

277 

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

279 
(writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *) 

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

280 
Locale.print_goals_marker begin_goal (! goals_limit) thm); 
5820  281 
in 
282 
writeln ("Nesting level: " ^ string_of_int (length nodes div 1)); (* FIXME *) 

283 
writeln ""; 

5993  284 
writeln (mode_name mode ^ " mode"); 
285 
writeln ""; 

5820  286 
ProofContext.print_context context; 
287 
writeln ""; 

288 
print_facts facts; 

5993  289 
print_goal (find_goal 0 state) 
5820  290 
end; 
291 

292 

293 

294 
(** proof steps **) 

295 

296 
(* datatype method *) 

297 

298 
datatype method = Method of 

299 
tthm list > (*use facts*) 

300 
thm (*goal: subgoals ==> statement*) 

301 
> (thm * (*refined goal*) 

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

303 
(string * tthm list) list) (*new thms*) 

304 
Seq.seq; 

305 

306 
val method = Method; 

307 

308 

309 
(* refine goal *) 

310 

311 
fun check_sign sg state = 

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

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

314 

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

316 
let 

317 
val Method meth = meth_fun context; 

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

319 

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

321 
state 

322 
> check_sign (sign_of_thm thm') 

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

324 
> add_binds new_binds 

325 
> put_tthmss new_thms; 

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

327 

328 

329 
(* prepare result *) 

330 

331 
fun varify_frees names thm = 

332 
let 

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

334 
 get_free _ (opt, _) = opt; 

335 

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

337 

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

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

340 
in 

341 
thm 

342 
> Drule.forall_intr_list frees 

343 
> Drule.forall_elim_vars (maxidx + 1) 

344 
end; 

345 

346 
fun implies_elim_hyps thm = 

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

348 

349 
fun prep_result state asms t raw_thm = 

350 
let 

351 
val ctxt = context_of state; 

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

353 

354 
val ngoals = Thm.nprems_of raw_thm; 

355 
val _ = 

356 
if ngoals = 0 then () 

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

358 

359 
val thm = 

360 
raw_thm RS Drule.rev_triv_goal 

361 
> implies_elim_hyps 

362 
> Drule.implies_intr_list asms 

363 
> varify_frees (ProofContext.fixed_names ctxt); 

364 

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

366 
val tsig = Sign.tsig_of sign; 

367 
in 

368 
(* FIXME 

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

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

371 
else (); 

372 
*) 

373 
if not (null hyps) then 

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

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

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

377 
else thm 

378 
end; 

379 

380 

381 
(* prepare final result *) 

382 

383 
fun strip_flexflex thm = 

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

385 

386 
fun final_result state pre_thm = 

387 
let 

388 
val thm = 

389 
pre_thm 

390 
> strip_flexflex 

391 
> Thm.strip_shyps 

392 
> Drule.standard; 

393 

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

395 
val xshyps = Thm.extra_shyps thm; 

396 
in 

397 
if not (null xshyps) then 

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

399 
else thm 

400 
end; 

401 

402 

403 
(* solve goal *) 

404 

405 
fun solve_goal rule state = 

406 
let 

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

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

411 

412 

413 
(*** structured proof commands ***) 

414 

415 
(** context **) 

416 

417 
(* bind *) 

418 

419 
fun gen_bind f x state = 

420 
state 

421 
> assert_forward 

422 
> map_context (f x) 

423 
> reset_facts; 

424 

425 
val bind = gen_bind ProofContext.add_binds; 

426 
val bind_i = gen_bind ProofContext.add_binds_i; 

427 

428 
val match_bind = gen_bind ProofContext.match_binds; 

429 
val match_bind_i = gen_bind ProofContext.match_binds_i; 

430 

431 

5918  432 
(* have_tthmss *) 
5820  433 

5918  434 
fun have_tthmss name atts ths_atts state = 
5820  435 
state 
436 
> assert_forward 

5918  437 
> map_context_result (ProofContext.have_tthmss (PureThy.default_name name) atts ths_atts) 
5820  438 
> these_facts; 
439 

440 

441 
(* fix *) 

442 

443 
fun gen_fix f xs state = 

444 
state 

445 
> assert_forward 

446 
> map_context (f xs) 

447 
> reset_facts; 

448 

449 
val fix = gen_fix ProofContext.fix; 

450 
val fix_i = gen_fix ProofContext.fix_i; 

451 

452 

453 
(* assume *) 

454 

455 
fun gen_assume f name atts props state = 

456 
state 

457 
> assert_forward 

5918  458 
> map_context_result (f (PureThy.default_name name) atts props) 
5820  459 
> these_facts 
460 
> (fn st => let_tthms ("prems", ProofContext.assumptions (context_of st)) st); 

461 

462 
val assume = gen_assume ProofContext.assume; 

463 
val assume_i = gen_assume ProofContext.assume_i; 

464 

465 

466 

467 
(** goals **) 

468 

469 
(* forward chaining *) 

470 

471 
fun chain state = 

472 
state 

473 
> assert_forward 

474 
> enter_forward_chain; 

475 

476 
fun from_facts facts state = 

477 
state 

478 
> put_facts (Some facts) 

479 
> chain; 

480 

481 

482 
(* setup goals *) 

483 

5936  484 
fun setup_goal opt_block prepp kind name atts raw_propp state = 
5820  485 
let 
5936  486 
val (state', concl) = 
487 
state 

488 
> assert_forward_or_chain 

489 
> enter_forward 

490 
> opt_block 

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

5820  492 

5936  493 
val casms = map (#prop o Thm.crep_thm o Attribute.thm_of) 
494 
(ProofContext.assumptions (context_of state')); 

5820  495 
val asms = map Thm.term_of casms; 
496 

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

5820  499 
val thm = Drule.mk_triv_goal cprop; 
500 
in 

5936  501 
state' 
5918  502 
> put_goal (Some ((kind atts, (PureThy.default_name name), casms, prop), ([], thm))) 
5820  503 
> bind_props [("thesis", prop)] 
504 
> (if is_chain state then use_facts else reset_facts) 

505 
> new_block 

506 
> enter_backward 

507 
end; 

508 

509 

510 
(*global goals*) 

511 
fun global_goal prep kind name atts x thy = 

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

513 

5936  514 
val theorem = global_goal ProofContext.bind_propp Theorem; 
515 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

516 
val lemma = global_goal ProofContext.bind_propp Lemma; 

517 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  518 

519 

520 
(*local goals*) 

521 
fun local_goal prep kind name atts x = 

522 
setup_goal open_block prep kind name atts x; 

523 

5936  524 
val show = local_goal ProofContext.bind_propp Goal; 
525 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

526 
val have = local_goal ProofContext.bind_propp Aux; 

527 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  528 

529 

530 

531 
(** blocks **) 

532 

533 
(* begin_block *) 

534 

535 
fun begin_block state = 

536 
state 

537 
> assert_forward 

538 
> new_block 

539 
> reset_facts 

540 
> open_block; 

541 

542 

543 
(* next_block *) 

544 

545 
fun next_block state = 

546 
state 

547 
> assert_forward 

548 
> close_block 

549 
> new_block; 

550 

551 

552 

553 
(** conclusions **) 

554 

555 
(* current goal *) 

556 

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

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

559 

560 
fun assert_current_goal state = (current_goal state; state); 

561 

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

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

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

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

566 
 assert_bottom _ state = state; 

567 

568 

569 
(* finish proof *) 

570 

571 
fun check_finished state states = 

572 
(case Seq.pull states of 

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

574 
 Some s_sq => Seq.cons s_sq); 

575 

576 
fun finish_proof bot meth_fun state = 

577 
state 

578 
> assert_forward 

579 
> close_block 

580 
> assert_bottom bot 

581 
> assert_current_goal 

582 
> refine meth_fun 

583 
> check_finished state; 

584 

585 

586 
(* conclude local proof *) 

587 

588 
fun finish_local state = 

589 
let 

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

591 
val result = prep_result state asms t raw_thm; 

592 
val (atts, opt_solve) = 

593 
(case kind of 

594 
Goal atts => (atts, solve_goal result) 

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

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

597 
in 

598 
state 

599 
> close_block 

5918  600 
> have_tthmss name atts [([(result, [])], [])] 
5820  601 
> opt_solve 
602 
end; 

603 

604 
fun end_block meth_fun state = 

605 
if can assert_current_goal (close_block state) then 

606 
state 

607 
> finish_proof false meth_fun 

608 
> (Seq.flat o Seq.map finish_local) 

609 
else 

610 
state 

611 
> assert_forward 

612 
> close_block 

613 
> close_block 

614 
> fetch_facts state 

615 
> Seq.single; 

616 

617 

618 
(* conclude global proof *) 

619 

620 
fun finish_global alt_name alt_atts state = 

621 
let 

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

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

624 

625 
val name = if_none alt_name def_name; 

626 
val atts = 

627 
(case kind of 

628 
Theorem atts => if_none alt_atts atts 

5918  629 
 Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma] 
5820  630 
 _ => raise STATE ("No global goal!", state)); 
631 

632 
val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state); 

6001  633 
in (thy', (kind_name kind, name, result')) end; 
5820  634 

635 
fun qed meth_fun alt_name alt_atts state = 

636 
state 

637 
> finish_proof true meth_fun 

638 
> Seq.hd 

639 
> finish_global alt_name alt_atts; 

640 

641 

642 
end; 