author  wenzelm 
Sun, 28 May 2000 21:55:50 +0200  
changeset 8991  dc70b797827f 
parent 8807  0046be1769f9 
child 9196  1f6f66fe777a 
permissions  rwrr 
5820  1 
(* Title: Pure/Isar/proof.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

8807  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
5820  5 

6 
Proof states and methods. 

7 
*) 

8 

8152  9 
signature BASIC_PROOF = 
10 
sig 

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

8152  13 
end; 
14 

5820  15 
signature PROOF = 
16 
sig 

8152  17 
include BASIC_PROOF 
5820  18 
type context 
19 
type state 

20 
exception STATE of string * state 

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

25 
val sign_of: state > Sign.sg 

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

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

7412  39 
val pretty_thms: thm list > Pretty.T 
6529  40 
val verbose: bool ref 
7201  41 
val print_state: int > state > unit 
6776  42 
val level: state > int 
5820  43 
type method 
6848  44 
val method: (thm list > tactic) > method 
8374  45 
val method_cases: (thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq) > method 
5820  46 
val refine: (context > method) > state > state Seq.seq 
8234  47 
val refine_end: (context > method) > state > state Seq.seq 
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 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

51 
val let_bind: (string list * string) list > state > state 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

60 
> state > state 

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

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

6932  63 
> state > state 
7271  64 
val assume: (string * context attribute list * (string * (string list * string list)) list) list 
65 
> state > state 

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

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

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

76 
> theory > state 

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

78 
> theory > state 

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

80 
> theory > state 

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

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

86 
> term * (term list * term list) > state > state 

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

88 
> string * (string list * string list) > state > state 

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

90 
> term * (term list * term list) > state > state 

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

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

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

8152  101 
signature PRIVATE_PROOF = 
5820  102 
sig 
103 
include PROOF 

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

105 
end; 

106 

8152  107 
structure Proof: PRIVATE_PROOF = 
5820  108 
struct 
109 

110 

111 
(** proof state **) 

112 

113 
type context = ProofContext.context; 

114 

115 

116 
(* type goal *) 

117 

118 
datatype kind = 

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

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

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

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

123 

124 
val kind_name = 

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

127 
type goal = 

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

130 
term) * (*result statement*) 

131 
(thm list * (*use facts*) 

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

5820  133 

134 

135 
(* type mode *) 

136 

137 
datatype mode = Forward  ForwardChain  Backward; 

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

140 

141 
(* datatype state *) 

142 

7176  143 
datatype node = 
144 
Node of 

145 
{context: context, 

146 
facts: thm list option, 

147 
mode: mode, 

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

149 
and state = 

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

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

153 

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

156 

157 

5820  158 
exception STATE of string * state; 
159 

160 
fun err_malformed name state = 

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

162 

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

165 
None => raise STATE (msg, state) 

166 
 Some s_sq => Seq.cons s_sq); 

167 

5820  168 

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

172 
fun init_state thy = 

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

175 

176 

177 
(** basic proof state operations **) 

178 

179 
(* context *) 

180 

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

184 

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

186 

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

190 

191 

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

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

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

202 

203 
(* facts *) 

204 

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

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

7605  211 

212 
val thisN = "this"; 

213 

5820  214 
fun put_facts facts state = 
215 
state 

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

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

219 
val reset_facts = put_facts None; 

220 

221 
fun have_facts (name, facts) state = 

222 
state 

223 
> put_facts (Some facts) 

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

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

227 

228 

229 
(* goal *) 

230 

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

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

235 

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

7176  239 

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

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

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

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

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

247 
 map_goal _ _ state = state; 

5820  248 

249 
fun goal_facts get state = 

250 
state 

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

253 
fun use_facts state = 

254 
state 

255 
> goal_facts the_facts 

256 
> reset_facts; 

257 

258 

259 
(* mode *) 

260 

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

264 
val enter_forward = put_mode Forward; 

265 
val enter_forward_chain = put_mode ForwardChain; 

266 
val enter_backward = put_mode Backward; 

267 

268 
fun assert_mode pred state = 

269 
let val mode = get_mode state in 

270 
if pred mode then state 

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

274 
fun is_chain state = get_mode state = ForwardChain; 

275 
val assert_forward = assert_mode (equal Forward); 

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

277 
val assert_backward = assert_mode (equal Backward); 

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

280 

281 
(* blocks *) 

282 

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

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

287 
fun new_block state = 

288 
state 

289 
> open_block 

290 
> put_goal None; 

291 

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

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

295 

296 

297 
(** print_state **) 

298 

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

301 

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

305 

6529  306 
val verbose = ProofContext.verbose; 
307 

8462  308 
fun pretty_facts _ None = [] 
309 
 pretty_facts s (Some ths) = 

310 
[Pretty.big_list (s ^ "this:") (map pretty_thm ths), Pretty.str ""]; 

6756  311 

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

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

316 
fun levels_up 0 = "" 

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

5820  319 

8462  320 
fun pretty_goal (_, (i, (((kind, name, _), (goal_facts, thm)), _))) = 
321 
pretty_facts "using " 

322 
(if mode <> Backward orelse null goal_facts then None else Some goal_facts) @ 

323 
[Pretty.str ("goal (" ^ kind_name kind ^ (if name = "" then "" else " " ^ name) ^ 

324 
levels_up (i div 2) ^ "):")] @ 

325 
Locale.pretty_goals_marker begin_goal (! goals_limit) thm; 

6848  326 

8462  327 
val ctxt_prts = 
328 
if ! verbose orelse mode = Forward then ProofContext.pretty_context context 

329 
else if mode = Backward then ProofContext.pretty_prems context 

7575  330 
else []; 
8462  331 

332 
val prts = 

8582  333 
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ 
8561  334 
(if ! verbose then ", depth " ^ string_of_int (length nodes div 2) 
335 
else "")), Pretty.str ""] @ 

8462  336 
(if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ 
337 
(if ! verbose orelse mode = Forward then 

338 
(pretty_facts "" facts @ pretty_goal (find_goal 0 state)) 

339 
else if mode = ForwardChain then pretty_facts "picking " facts 

340 
else pretty_goal (find_goal 0 state)) 

341 
in Pretty.writeln (Pretty.chunks prts) end; 

5820  342 

343 

344 

345 
(** proof steps **) 

346 

347 
(* datatype method *) 

348 

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

351 

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

353 
val method_cases = Method; 

5820  354 

355 

356 
(* refine goal *) 

357 

8234  358 
local 
359 

5820  360 
fun check_sign sg state = 
361 
if Sign.subsig (sg, sign_of state) then state 

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

363 

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

5820  368 

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

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

8234  375 
in 
376 

377 
val refine = gen_refine true; 

378 
val refine_end = gen_refine false; 

379 

380 
end; 

381 

5820  382 

6932  383 
(* export results *) 
384 

385 
fun RANGE [] _ = all_tac 

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

387 

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

8152  391 

8166  392 
fun HEADGOAL tac = tac 1; 
393 

6982  394 
fun export_goal print_rule raw_rule inner state = 
6932  395 
let 
7176  396 
val (outer, (_, ((result, (facts, thm)), f))) = find_goal 0 state; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

397 
val (exp, tacs) = ProofContext.export_wrt inner (Some outer); 
6932  398 
val rule = exp raw_rule; 
6982  399 
val _ = print_rule rule; 
8152  400 
val thmq = FINDGOAL (Tactic.rtac rule THEN' RANGE (map #1 tacs)) thm; 
8374  401 
in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; 
6932  402 

403 

404 
fun export_thm inner thm = 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

405 
let val (exp, tacs) = ProofContext.export_wrt inner None in 
6932  406 
(case Seq.chop (2, RANGE (map #2 tacs) 1 (exp thm)) of 
407 
([thm'], _) => thm' 

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

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

410 
end; 

411 

412 
fun transfer_facts inner_state state = 

413 
(case get_facts inner_state of 

414 
None => Seq.single (reset_facts state) 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

415 
 Some thms => 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

416 
let 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

417 
val (exp, tacs) = 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

418 
ProofContext.export_wrt (context_of inner_state) (Some (context_of state)); 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

419 
val thmqs = map (RANGE (map #2 tacs) 1 o exp) thms; 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

422 

423 
(* prepare result *) 

424 

425 
fun prep_result state t raw_thm = 

5820  426 
let 
427 
val ctxt = context_of state; 

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

429 

430 
val ngoals = Thm.nprems_of raw_thm; 

431 
val _ = 

432 
if ngoals = 0 then () 

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

434 

6932  435 
val thm = raw_thm RS Drule.rev_triv_goal; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

436 
val {hyps, prop, sign, ...} = Thm.rep_thm thm; 
5820  437 
val tsig = Sign.tsig_of sign; 
6932  438 

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

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

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

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

446 
else thm 
5820  447 
end; 
448 

449 

450 

451 
(*** structured proof commands ***) 

452 

453 
(** context **) 

454 

455 
(* bind *) 

456 

457 
fun gen_bind f x state = 

458 
state 

459 
> assert_forward 

460 
> map_context (f x) 

461 
> reset_facts; 

462 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

463 
val match_bind = gen_bind (ProofContext.match_bind false); 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

464 
val match_bind_i = gen_bind (ProofContext.match_bind_i false); 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

465 
val let_bind = gen_bind (ProofContext.match_bind true); 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

466 
val let_bind_i = gen_bind (ProofContext.match_bind_i true); 
5820  467 

468 

6091  469 
(* have_thmss *) 
5820  470 

6876  471 
fun have_thmss ths name atts ths_atts state = 
5820  472 
state 
473 
> assert_forward 

7478  474 
> map_context_result (ProofContext.have_thmss ths name atts ths_atts) 
5820  475 
> these_facts; 
476 

6876  477 
fun simple_have_thms name thms = have_thmss [] name [] [(thms, [])]; 
478 

5820  479 

480 
(* fix *) 

481 

482 
fun gen_fix f xs state = 

483 
state 

484 
> assert_forward 

485 
> map_context (f xs) 

486 
> reset_facts; 

487 

488 
val fix = gen_fix ProofContext.fix; 

489 
val fix_i = gen_fix ProofContext.fix_i; 

490 

491 

492 
(* assume *) 

493 

7271  494 
local 
495 

496 
fun gen_assume f tac args state = 

5820  497 
state 
498 
> assert_forward 

7478  499 
> map_context_result (f tac args) 
7271  500 
> (fn (st, (factss, prems)) => 
501 
foldl these_facts (st, factss) 

502 
> put_thms ("prems", prems) 

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

6932  504 

6996  505 
val hard_asm_tac = Tactic.etac Drule.triv_goal; 
8542  506 
val soft_asm_tac = Tactic.rtac Drule.triv_goal 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

507 
THEN' Tactic.rtac asm_rl; (* FIXME hack to norm goal *) 
6996  508 

7271  509 
in 
510 

511 
val assm = gen_assume ProofContext.assume; 

512 
val assm_i = gen_assume ProofContext.assume_i; 

6996  513 
val assume = assm (hard_asm_tac, soft_asm_tac); 
514 
val assume_i = assm_i (hard_asm_tac, soft_asm_tac); 

515 
val presume = assm (soft_asm_tac, soft_asm_tac); 

516 
val presume_i = assm_i (soft_asm_tac, soft_asm_tac); 

5820  517 

7271  518 
end; 
519 

5820  520 

8374  521 
(* invoke_case *) 
522 

8450  523 
fun invoke_case (name, atts) state = 
8374  524 
let val (vars, props) = get_case state name in 
525 
state 

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

8450  527 
> assume_i [(name, atts, map (fn t => (t, ([], []))) props)] 
8374  528 
end; 
529 

530 

5820  531 

532 
(** goals **) 

533 

534 
(* forward chaining *) 

535 

536 
fun chain state = 

537 
state 

538 
> assert_forward 

6848  539 
> assert_facts 
5820  540 
> enter_forward_chain; 
541 

542 
fun from_facts facts state = 

543 
state 

544 
> put_facts (Some facts) 

545 
> chain; 

546 

547 

548 
(* setup goals *) 

549 

8991  550 
val antN = "antecedent"; 
551 

7176  552 
fun setup_goal opt_block prepp kind after_qed name atts raw_propp state = 
5820  553 
let 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

554 
val (state', (prop, gen_binds)) = 
5936  555 
state 
556 
> assert_forward_or_chain 

557 
> enter_forward 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

558 
> opt_block 
8095  559 
> map_context_result (fn ct => prepp (ct, raw_propp)); 
6932  560 
val cprop = Thm.cterm_of (sign_of state') prop; 
7556  561 
val goal = Drule.mk_triv_goal cprop; 
5820  562 
in 
5936  563 
state' 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

564 
> put_goal (Some (((kind atts, name, prop), ([], goal)), after_qed o map_context gen_binds)) 
8991  565 
> map_context (ProofContext.add_cases (RuleCases.make goal [antN])) 
6790  566 
> auto_bind_goal prop 
5820  567 
> (if is_chain state then use_facts else reset_facts) 
568 
> new_block 

569 
> enter_backward 

570 
end; 

571 

572 

573 
(*global goals*) 

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

5820  576 

7928  577 
val theorem = global_goal ProofContext.bind_propp Theorem; 
578 
val theorem_i = global_goal ProofContext.bind_propp_i Theorem; 

579 
val lemma = global_goal ProofContext.bind_propp Lemma; 

580 
val lemma_i = global_goal ProofContext.bind_propp_i Lemma; 

5820  581 

582 

583 
(*local goals*) 

8095  584 
fun local_goal prepp kind f name atts args state = 
7928  585 
state 
8095  586 
> setup_goal open_block prepp kind f name atts args 
7928  587 
> warn_extra_tfrees state; 
5820  588 

7928  589 
val show = local_goal ProofContext.bind_propp Goal; 
590 
val show_i = local_goal ProofContext.bind_propp_i Goal; 

591 
val have = local_goal ProofContext.bind_propp Aux; 

592 
val have_i = local_goal ProofContext.bind_propp_i Aux; 

5820  593 

594 

595 

596 
(** conclusions **) 

597 

598 
(* current goal *) 

599 

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

7176  603 
fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) = 
6404  604 
raise STATE ("No goal in this block!", state) 
7176  605 
 assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) = 
6404  606 
raise STATE ("Goal present in this block!", state) 
607 
 assert_current_goal _ state = state; 

5820  608 

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

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

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

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

613 
 assert_bottom _ state = state; 

614 

6404  615 
val at_bottom = can (assert_bottom true o close_block); 
616 

6932  617 
fun end_proof bot state = 
5820  618 
state 
619 
> assert_forward 

620 
> close_block 

621 
> assert_bottom bot 

7011  622 
> assert_current_goal true 
623 
> goal_facts (K []); 

5820  624 

625 

6404  626 
(* local_qed *) 
5820  627 

6982  628 
fun finish_local (print_result, print_rule) state = 
5820  629 
let 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

630 
val (goal_ctxt, (((kind, name, t), (_, raw_thm)), after_qed)) = current_goal state; 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

631 
val outer_state = state > close_block; 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

632 
val outer_ctxt = context_of outer_state; 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

633 

6932  634 
val result = prep_result state t raw_thm; 
5820  635 
val (atts, opt_solve) = 
636 
(case kind of 

8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

637 
Goal atts => (atts, export_goal print_rule result goal_ctxt) 
5820  638 
 Aux atts => (atts, Seq.single) 
6932  639 
 _ => err_malformed "finish_local" state); 
5820  640 
in 
6731  641 
print_result {kind = kind_name kind, name = name, thm = result}; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

642 
outer_state 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

643 
> auto_bind_facts name [ProofContext.generalize goal_ctxt outer_ctxt t] 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

644 
> have_thmss [] name atts [Thm.no_attributes 
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

645 
[#1 (ProofContext.export_wrt goal_ctxt (Some outer_ctxt)) result]] 
5820  646 
> opt_solve 
7176  647 
> (Seq.flat o Seq.map after_qed) 
5820  648 
end; 
649 

6982  650 
fun local_qed finalize print state = 
6404  651 
state 
6932  652 
> end_proof false 
6871  653 
> finalize 
6982  654 
> (Seq.flat o Seq.map (finish_local print)); 
5820  655 

656 

6404  657 
(* global_qed *) 
5820  658 

6950  659 
fun finish_global state = 
5820  660 
let 
7176  661 
val (_, (((kind, name, t), (_, raw_thm)), _)) = current_goal state; (*ignores after_qed!*) 
8152  662 
val result = Drule.standard (prep_result state t raw_thm); 
5820  663 

664 
val atts = 

665 
(case kind of 

6950  666 
Theorem atts => atts 
667 
 Lemma atts => atts @ [Drule.tag_lemma] 

6932  668 
 _ => err_malformed "finish_global" state); 
5820  669 

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

6871  673 
(*Note: should inspect first result only, backtracking may destroy theory*) 
6950  674 
fun global_qed finalize state = 
5820  675 
state 
6932  676 
> end_proof true 
6871  677 
> finalize 
6950  678 
> Seq.map finish_global; 
5820  679 

680 

6896  681 

682 
(** blocks **) 

683 

684 
(* begin_block *) 

685 

686 
fun begin_block state = 

687 
state 

688 
> assert_forward 

689 
> new_block 

690 
> open_block; 

691 

692 

693 
(* end_block *) 

694 

695 
fun end_block state = 

696 
state 

697 
> assert_forward 

698 
> close_block 

699 
> assert_current_goal false 

700 
> close_block 

6932  701 
> transfer_facts state; 
6896  702 

703 

704 
(* next_block *) 

705 

706 
fun next_block state = 

707 
state 

708 
> assert_forward 

709 
> close_block 

8718  710 
> new_block 
711 
> reset_facts; 

6896  712 

713 

5820  714 
end; 
8152  715 

716 

717 
structure BasicProof: BASIC_PROOF = Proof; 

718 
open BasicProof; 