author  wenzelm 
Mon, 19 Nov 2001 20:47:39 +0100  
changeset 12242  282a92bc5655 
parent 12223  d5e76c2e335c 
child 12244  179f142ffb03 
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 
12045  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 
9469  29 
val the_fact: state > thm 
11079
a378479996f7
val get_goal: state > context * (thm list * thm);
wenzelm
parents:
10938
diff
changeset

30 
val get_goal: state > context * (thm list * thm) 
6091  31 
val goal_facts: (state > thm list) > state > state 
5820  32 
val use_facts: state > state 
33 
val reset_facts: state > state 

9469  34 
val is_chain: state > bool 
6891  35 
val assert_forward: state > state 
9469  36 
val assert_forward_or_chain: state > state 
5820  37 
val assert_backward: state > state 
8206  38 
val assert_no_chain: state > state 
5820  39 
val enter_forward: state > state 
6529  40 
val verbose: bool ref 
7201  41 
val print_state: int > state > unit 
10360  42 
val pretty_goals: bool > state > Pretty.T list 
6776  43 
val level: state > int 
5820  44 
type method 
6848  45 
val method: (thm list > tactic) > method 
8374  46 
val method_cases: (thm list > thm > (thm * (string * RuleCases.T) list) Seq.seq) > method 
5820  47 
val refine: (context > method) > state > state Seq.seq 
8234  48 
val refine_end: (context > method) > state > state Seq.seq 
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 simple_have_thms: string > thm list > state > state 
9196  54 
val have_thmss: ((string * context attribute list) * 
55 
(thm list * context attribute list) list) list > state > state 

56 
val with_thmss: ((string * context attribute list) * 

57 
(thm list * context attribute list) list) list > state > state 

7412  58 
val fix: (string list * string option) list > state > state 
7665  59 
val fix_i: (string list * typ option) list > state > state 
9469  60 
val assm: ProofContext.exporter 
10464  61 
> ((string * context attribute list) * (string * (string list * string list)) list) list 
7271  62 
> state > state 
9469  63 
val assm_i: ProofContext.exporter 
10464  64 
> ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  65 
> state > state 
10464  66 
val assume: 
67 
((string * context attribute list) * (string * (string list * string list)) list) list 

7271  68 
> state > state 
10464  69 
val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  70 
> state > state 
10464  71 
val presume: 
72 
((string * context attribute list) * (string * (string list * string list)) list) list 

6932  73 
> state > state 
10464  74 
val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  75 
> state > state 
11891  76 
val def: string > context attribute list > string * (string * string list) > state > state 
77 
val def_i: string > context attribute list > string * (term * term list) > state > state 

11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

78 
val invoke_case: string * string option list * context attribute list > state > state 
12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

79 
val multi_theorem: string > bstring * theory attribute list 
12146  80 
> (xstring * context attribute list) option > context attribute Locale.element list 
81 
> ((bstring * theory attribute list) * (string * (string list * string list)) list) list 

82 
> theory > state 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

83 
val multi_theorem_i: string > bstring * theory attribute list 
12146  84 
> (string * context attribute list) option > context attribute Locale.element_i list 
85 
> ((bstring * theory attribute list) * (term * (term list * term list)) list) list 

86 
> theory > state 

12065  87 
val theorem: string 
88 
> (xstring * context attribute list) option > context attribute Locale.element list 

89 
> bstring > theory attribute list > string * (string list * string list) > theory > state 

90 
val theorem_i: string 

91 
> (string * context attribute list) option > context attribute Locale.element_i list 

92 
> bstring > theory attribute list > term * (term list * term list) > theory > state 

5820  93 
val chain: state > state 
6091  94 
val from_facts: thm list > state > state 
12146  95 
val show: (bool > state > state) > (state > state Seq.seq) 
96 
> ((string * context attribute list) * (string * (string list * string list)) list) list 

97 
> bool > state > state 

98 
val show_i: (bool > state > state) > (state > state Seq.seq) 

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

100 
> bool > state > state 

101 
val have: (state > state Seq.seq) 

102 
> ((string * context attribute list) * (string * (string list * string list)) list) list 

103 
> state > state 

104 
val have_i: (state > state Seq.seq) 

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

106 
> state > state 

6404  107 
val at_bottom: state > bool 
6982  108 
val local_qed: (state > state Seq.seq) 
12146  109 
> (context > string * (string * thm list) list > unit) * (context > thm > unit) 
110 
> state > state Seq.seq 

6950  111 
val global_qed: (state > state Seq.seq) > state 
12146  112 
> (theory * (string * (string * thm list) list)) Seq.seq 
6896  113 
val begin_block: state > state 
6932  114 
val end_block: state > state Seq.seq 
6896  115 
val next_block: state > state 
5820  116 
end; 
117 

8152  118 
signature PRIVATE_PROOF = 
5820  119 
sig 
120 
include PROOF 

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

122 
end; 

123 

8152  124 
structure Proof: PRIVATE_PROOF = 
5820  125 
struct 
126 

127 

128 
(** proof state **) 

129 

130 
type context = ProofContext.context; 

131 

132 

133 
(* type goal *) 

134 

135 
datatype kind = 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

136 
Theorem of string * (*theorem kind*) 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

137 
(bstring * theory attribute list) * (*common result binding*) 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

138 
(string * context attribute list) option * (*target locale*) 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

139 
theory attribute list list  (*attributes of individual result binding*) 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

140 
Show of context attribute list list  (*intermediate result, solving subgoal*) 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

141 
Have of context attribute list list; (*intermediate result*) 
5820  142 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

143 
fun common_name "" = ""  common_name a = " " ^ a; 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

144 

282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

145 
fun kind_name _ (Theorem (s, (a, _), None, _)) = s ^ common_name a 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

146 
 kind_name sg (Theorem (s, (a, _), Some (name, _), _)) = 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

147 
s ^ common_name a ^ " (in " ^ Locale.cond_extern sg name ^ ")" 
12015  148 
 kind_name _ (Show _) = "show" 
149 
 kind_name _ (Have _) = "have"; 

5820  150 

151 
type goal = 

12146  152 
(kind * (*result kind*) 
153 
string list * (*result names*) 

154 
term list list) * (*result statements*) 

155 
(thm list * (*use facts*) 

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

5820  157 

158 

159 
(* type mode *) 

160 

161 
datatype mode = Forward  ForwardChain  Backward; 

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

164 

165 
(* datatype state *) 

166 

7176  167 
datatype node = 
168 
Node of 

169 
{context: context, 

170 
facts: thm list option, 

171 
mode: mode, 

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

173 
and state = 

5820  174 
State of 
175 
node * (*current*) 

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

177 

7176  178 
fun make_node (context, facts, mode, goal) = 
179 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

180 

181 

5820  182 
exception STATE of string * state; 
183 

184 
fun err_malformed name state = 

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

186 

6871  187 
fun check_result msg state sq = 
188 
(case Seq.pull sq of 

189 
None => raise STATE (msg, state) 

190 
 Some s_sq => Seq.cons s_sq); 

191 

5820  192 

7176  193 
fun map_current f (State (Node {context, facts, mode, goal}, nodes)) = 
5820  194 
State (make_node (f (context, facts, mode, goal)), nodes); 
195 

12045  196 
fun init_state thy = 
197 
State (make_node (ProofContext.init thy, None, Forward, None), []); 

198 

5820  199 

200 

201 
(** basic proof state operations **) 

202 

203 
(* context *) 

204 

7176  205 
fun context_of (State (Node {context, ...}, _)) = context; 
5820  206 
val theory_of = ProofContext.theory_of o context_of; 
207 
val sign_of = ProofContext.sign_of o context_of; 

208 

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

210 

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

214 

215 

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

7924  217 
val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of; 
10809  218 
val add_binds_i = map_context o ProofContext.add_binds_i; 
6790  219 
val auto_bind_goal = map_context o ProofContext.auto_bind_goal; 
12146  220 
val auto_bind_facts = map_context o ProofContext.auto_bind_facts; 
6091  221 
val put_thms = map_context o ProofContext.put_thms; 
222 
val put_thmss = map_context o ProofContext.put_thmss; 

7605  223 
val reset_thms = map_context o ProofContext.reset_thms; 
8374  224 
val get_case = ProofContext.get_case o context_of; 
5820  225 

226 

227 
(* facts *) 

228 

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

9469  232 
fun the_fact state = 
233 
(case the_facts state of 

234 
[thm] => thm 

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

236 

6848  237 
fun assert_facts state = (the_facts state; state); 
7176  238 
fun get_facts (State (Node {facts, ...}, _)) = facts; 
6848  239 

7605  240 

241 
val thisN = "this"; 

242 

5820  243 
fun put_facts facts state = 
244 
state 

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

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

248 
val reset_facts = put_facts None; 

249 

9196  250 
fun these_factss (state, named_factss) = 
5820  251 
state 
9196  252 
> put_thmss named_factss 
253 
> put_facts (Some (flat (map #2 named_factss))); 

5820  254 

255 

256 
(* goal *) 

257 

10553  258 
local 
259 
fun find i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal)) 

260 
 find i (State (Node {goal = None, ...}, node :: nodes)) = find (i + 1) (State (node, nodes)) 

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

262 
in val find_goal = find 0 end; 

7176  263 

11079
a378479996f7
val get_goal: state > context * (thm list * thm);
wenzelm
parents:
10938
diff
changeset

264 
fun get_goal state = 
a378479996f7
val get_goal: state > context * (thm list * thm);
wenzelm
parents:
10938
diff
changeset

265 
let val (ctxt, (_, ((_, x), _))) = find_goal state 
a378479996f7
val get_goal: state > context * (thm list * thm);
wenzelm
parents:
10938
diff
changeset

266 
in (ctxt, x) end; 
a378479996f7
val get_goal: state > context * (thm list * thm);
wenzelm
parents:
10938
diff
changeset

267 

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

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

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

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

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

275 
 map_goal _ _ state = state; 

5820  276 

277 
fun goal_facts get state = 

278 
state 

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

281 
fun use_facts state = 

282 
state 

283 
> goal_facts the_facts 

284 
> reset_facts; 

285 

286 

287 
(* mode *) 

288 

7176  289 
fun get_mode (State (Node {mode, ...}, _)) = mode; 
5820  290 
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); 
291 

292 
val enter_forward = put_mode Forward; 

293 
val enter_forward_chain = put_mode ForwardChain; 

294 
val enter_backward = put_mode Backward; 

295 

296 
fun assert_mode pred state = 

297 
let val mode = get_mode state in 

298 
if pred mode then state 

12010  299 
else raise STATE ("Illegal application of proof command in " 
300 
^ quote (mode_name mode) ^ " mode", state) 

5820  301 
end; 
302 

303 
fun is_chain state = get_mode state = ForwardChain; 

304 
val assert_forward = assert_mode (equal Forward); 

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

306 
val assert_backward = assert_mode (equal Backward); 

8206  307 
val assert_no_chain = assert_mode (not_equal ForwardChain); 
5820  308 

309 

310 
(* blocks *) 

311 

6776  312 
fun level (State (_, nodes)) = length nodes; 
313 

5820  314 
fun open_block (State (node, nodes)) = State (node, node :: nodes); 
315 

316 
fun new_block state = 

317 
state 

318 
> open_block 

319 
> put_goal None; 

320 

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

321 
fun close_block (state as State (_, node :: nodes)) = State (node, nodes) 
5820  322 
 close_block state = raise STATE ("Unbalanced block parentheses", state); 
323 

324 

325 

326 
(** print_state **) 

327 

6529  328 
val verbose = ProofContext.verbose; 
329 

12085  330 
fun pretty_goals_local ctxt = Display.pretty_goals_aux 
331 
(ProofContext.pretty_sort ctxt, ProofContext.pretty_typ ctxt, ProofContext.pretty_term ctxt); 

332 

12055  333 
fun pretty_facts _ _ None = [] 
334 
 pretty_facts s ctxt (Some ths) = 

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

6756  336 

12085  337 
fun print_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) = 
5820  338 
let 
11891  339 
val ref (_, _, begin_goal) = Display.current_goals_markers; 
5820  340 

341 
fun levels_up 0 = "" 

7575  342 
 levels_up 1 = ", 1 level up" 
343 
 levels_up i = ", " ^ string_of_int i ^ " levels up"; 

5820  344 

11556  345 
fun subgoals 0 = "" 
346 
 subgoals 1 = ", 1 subgoal" 

347 
 subgoals n = ", " ^ string_of_int n ^ " subgoals"; 

12146  348 

349 
fun prt_names names = 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

350 
(case filter_out (equal "") names of [] => "" 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

351 
 nms => " " ^ enclose "(" ")" (space_implode " and " nms)); 
12146  352 

353 
fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) = 

12085  354 
pretty_facts "using " ctxt 
8462  355 
(if mode <> Backward orelse null goal_facts then None else Some goal_facts) @ 
12146  356 
[Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^ 
357 
levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @ 

12085  358 
pretty_goals_local ctxt begin_goal (true, true) (! Display.goals_limit) thm; 
6848  359 

8462  360 
val ctxt_prts = 
12085  361 
if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt 
362 
else if mode = Backward then ProofContext.pretty_asms ctxt 

7575  363 
else []; 
8462  364 

365 
val prts = 

8582  366 
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ 
12010  367 
(if ! verbose then ", depth " ^ string_of_int (length nodes div 2  1) 
8561  368 
else "")), Pretty.str ""] @ 
8462  369 
(if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @ 
370 
(if ! verbose orelse mode = Forward then 

12146  371 
(pretty_facts "" ctxt facts @ prt_goal (find_goal state)) 
12085  372 
else if mode = ForwardChain then pretty_facts "picking " ctxt facts 
12146  373 
else prt_goal (find_goal state)) 
8462  374 
in Pretty.writeln (Pretty.chunks prts) end; 
5820  375 

12085  376 
fun pretty_goals main state = 
377 
let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state 

378 
in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) thm end; 

10320  379 

5820  380 

381 

382 
(** proof steps **) 

383 

384 
(* datatype method *) 

385 

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

388 

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

390 
val method_cases = Method; 

5820  391 

392 

393 
(* refine goal *) 

394 

8234  395 
local 
396 

5820  397 
fun check_sign sg state = 
398 
if Sign.subsig (sg, sign_of state) then state 

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

400 

8234  401 
fun gen_refine current_context meth_fun state = 
6848  402 
let 
10553  403 
val (goal_ctxt, (_, ((result, (facts, thm)), f))) = find_goal state; 
8234  404 
val Method meth = meth_fun (if current_context then context_of state else goal_ctxt); 
5820  405 

8374  406 
fun refn (thm', cases) = 
6848  407 
state 
408 
> check_sign (Thm.sign_of_thm thm') 

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

8234  412 
in 
413 

414 
val refine = gen_refine true; 

415 
val refine_end = gen_refine false; 

416 

417 
end; 

418 

5820  419 

11917  420 
(* goal addressing *) 
6932  421 

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

8152  425 

8166  426 
fun HEADGOAL tac = tac 1; 
427 

9469  428 

429 
(* export results *) 

430 

11816  431 
fun refine_tac rule = 
432 
Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) => 

433 
if can Logic.dest_goal (Logic.strip_assums_concl goal) then 

434 
Tactic.etac Drule.triv_goal i 

435 
else all_tac)); 

436 

12146  437 
fun export_goal inner print_rule raw_rule state = 
6932  438 
let 
10553  439 
val (outer, (_, ((result, (facts, thm)), f))) = find_goal state; 
12010  440 
val exp_tac = ProofContext.export true inner outer; 
9469  441 
fun exp_rule rule = 
442 
let 

12055  443 
val _ = print_rule outer rule; 
11816  444 
val thmq = FINDGOAL (refine_tac rule) thm; 
9469  445 
in Seq.map (fn th => map_goal I (K ((result, (facts, th)), f)) state) thmq end; 
446 
in raw_rule > exp_tac > (Seq.flat o Seq.map exp_rule) end; 

6932  447 

12146  448 
fun export_goals inner print_rule raw_rules = 
449 
Seq.EVERY (map (export_goal inner print_rule) raw_rules); 

450 

6932  451 
fun transfer_facts inner_state state = 
452 
(case get_facts inner_state of 

453 
None => Seq.single (reset_facts state) 

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

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

455 
let 
12010  456 
val exp_tac = ProofContext.export false (context_of inner_state) (context_of state); 
11816  457 
val thmqs = map exp_tac thms; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

460 

461 
(* prepare result *) 

462 

12146  463 
fun prep_result state ts raw_th = 
5820  464 
let 
465 
val ctxt = context_of state; 

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

467 

12146  468 
val ngoals = Thm.nprems_of raw_th; 
5820  469 
val _ = 
470 
if ngoals = 0 then () 

12085  471 
else (err (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, true) 
12146  472 
(! Display.goals_limit) raw_th @ 
12085  473 
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")])))); 
5820  474 

12146  475 
val {hyps, sign, ...} = Thm.rep_thm raw_th; 
5820  476 
val tsig = Sign.tsig_of sign; 
12055  477 
val casms = flat (map #1 (ProofContext.assumptions_of (context_of state))); 
11816  478 
val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms); 
12146  479 

480 
val th = raw_th RS Drule.rev_triv_goal; 

481 
val ths = Drule.conj_elim_precise (length ts) th 

482 
handle THM _ => err "Main goal structure corrupted"; 

483 
val props = map (#prop o Thm.rep_thm) ths; 

5820  484 
in 
12146  485 
conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^ 
486 
cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps))); 

487 
conditional (exists (not o Pattern.matches tsig) (ts ~~ props)) (fn () => 

488 
err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th))); 

489 
ths 

5820  490 
end; 
491 

492 

493 

494 
(*** structured proof commands ***) 

495 

496 
(** context **) 

497 

498 
(* bind *) 

499 

500 
fun gen_bind f x state = 

501 
state 

502 
> assert_forward 

503 
> map_context (f x) 

504 
> reset_facts; 

505 

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

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

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

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

509 
val let_bind_i = gen_bind (ProofContext.match_bind_i true); 
5820  510 

511 

9196  512 
(* have_thmss etc. *) 
5820  513 

9196  514 
fun have_thmss args state = 
5820  515 
state 
516 
> assert_forward 

9196  517 
> map_context_result (ProofContext.have_thmss args) 
518 
> these_factss; 

5820  519 

9196  520 
fun simple_have_thms name thms = have_thmss [((name, []), [(thms, [])])]; 
521 

522 
fun with_thmss args state = 

523 
let val state' = state > have_thmss args 

524 
in state' > simple_have_thms "" (the_facts state' @ the_facts state) end; 

6876  525 

5820  526 

527 
(* fix *) 

528 

529 
fun gen_fix f xs state = 

530 
state 

531 
> assert_forward 

532 
> map_context (f xs) 

533 
> reset_facts; 

534 

535 
val fix = gen_fix ProofContext.fix; 

536 
val fix_i = gen_fix ProofContext.fix_i; 

537 

538 

11891  539 
(* assume and presume *) 
5820  540 

9469  541 
fun gen_assume f exp args state = 
5820  542 
state 
543 
> assert_forward 

9469  544 
> map_context_result (f exp args) 
11924  545 
> these_factss; 
6932  546 

7271  547 
val assm = gen_assume ProofContext.assume; 
548 
val assm_i = gen_assume ProofContext.assume_i; 

11917  549 
val assume = assm ProofContext.export_assume; 
550 
val assume_i = assm_i ProofContext.export_assume; 

551 
val presume = assm ProofContext.export_presume; 

552 
val presume_i = assm_i ProofContext.export_presume; 

5820  553 

7271  554 

5820  555 

11891  556 
(** local definitions **) 
557 

558 
fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state = 

559 
let 

560 
val _ = assert_forward state; 

561 
val ctxt = context_of state; 

562 

563 
(*rhs*) 

564 
val name = if raw_name = "" then Thm.def_name x else raw_name; 

565 
val rhs = prep_term ctxt raw_rhs; 

566 
val T = Term.fastype_of rhs; 

567 
val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats; 

568 

569 
(*lhs*) 

570 
val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T)); 

571 
in 

572 
state 

573 
> fix [([x], None)] 

574 
> match_bind_i [(pats, rhs)] 

11917  575 
> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] 
11891  576 
end; 
577 

578 
val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats; 

579 
val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats; 

580 

581 

8374  582 
(* invoke_case *) 
583 

11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

584 
fun invoke_case (name, xs, atts) state = 
9292  585 
let 
10830  586 
val (state', (lets, asms)) = 
11793
5f0ab6f5c280
support impromptu terminology of cases parameters;
wenzelm
parents:
11742
diff
changeset

587 
map_context_result (ProofContext.apply_case (get_case state name xs)) state; 
9292  588 
in 
10830  589 
state' 
10809  590 
> add_binds_i lets 
10830  591 
> assume_i [((name, atts), map (rpair ([], [])) asms)] 
8374  592 
end; 
593 

594 

5820  595 

596 
(** goals **) 

597 

598 
(* forward chaining *) 

599 

600 
fun chain state = 

601 
state 

602 
> assert_forward 

6848  603 
> assert_facts 
5820  604 
> enter_forward_chain; 
605 

606 
fun from_facts facts state = 

607 
state 

608 
> put_facts (Some facts) 

609 
> chain; 

610 

611 

612 
(* setup goals *) 

613 

11549  614 
val rule_contextN = "rule_context"; 
8991  615 

12146  616 
fun setup_goal opt_block prepp autofix kind after_qed names raw_propss state = 
5820  617 
let 
12146  618 
val (state', (propss, gen_binds)) = 
5936  619 
state 
620 
> assert_forward_or_chain 

621 
> enter_forward 

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

622 
> opt_block 
12146  623 
> map_context_result (fn ctxt => prepp (ctxt, raw_propss)); 
624 

625 
val props = flat propss; 

626 
val cprop = Thm.cterm_of (sign_of state') (foldr1 Logic.mk_conjunction props); 

7556  627 
val goal = Drule.mk_triv_goal cprop; 
10553  628 

12146  629 
val tvars = foldr Term.add_term_tvars (props, []); 
630 
val vars = foldr Term.add_term_vars (props, []); 

5820  631 
in 
10553  632 
if null tvars then () 
633 
else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^ 

634 
commas (map (Syntax.string_of_vname o #1) tvars), state); 

635 
if null vars then () 

636 
else warning ("Goal statement contains unbound schematic variable(s): " ^ 

12055  637 
commas (map (ProofContext.string_of_term (context_of state')) vars)); 
5936  638 
state' 
12146  639 
> map_context (autofix props) 
640 
> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds)) 

12167  641 
> map_context (ProofContext.add_cases 
642 
(if length props = 1 then RuleCases.make true goal [rule_contextN] 

643 
else [(rule_contextN, RuleCases.empty)])) 

12146  644 
> auto_bind_goal props 
5820  645 
> (if is_chain state then use_facts else reset_facts) 
646 
> new_block 

647 
> enter_backward 

648 
end; 

649 

650 
(*global goals*) 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

651 
fun global_goal prepp prep_locale activate kind a raw_locale elems args thy = 
12065  652 
let val locale = apsome (apfst (prep_locale (Theory.sign_of thy))) raw_locale in 
653 
thy 

654 
> init_state 

655 
> open_block 

656 
> (case locale of Some (name, _) => map_context (Locale.activate_locale_i name)  None => I) 

657 
> open_block 

658 
> map_context (activate elems) 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

659 
> setup_goal I prepp ProofContext.fix_frees (Theorem (kind, a, locale, map (snd o fst) args)) 
12146  660 
Seq.single (map (fst o fst) args) (map snd args) 
12065  661 
end; 
5820  662 

12146  663 
val multi_theorem = 
664 
global_goal ProofContext.bind_propp_schematic Locale.intern Locale.activate_elements; 

665 
val multi_theorem_i = 

666 
global_goal ProofContext.bind_propp_schematic_i (K I) Locale.activate_elements_i; 

667 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

668 
fun theorem k locale elems name atts p = 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

669 
multi_theorem k (name, atts) locale elems [(("", []), [p])]; 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

670 
fun theorem_i k locale elems name atts p = 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

671 
multi_theorem_i k (name, atts) locale elems [(("", []), [p])]; 
5820  672 

673 

674 
(*local goals*) 

12146  675 
fun local_goal' prepp kind (check: bool > state > state) f args int state = 
7928  676 
state 
12146  677 
> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) 
678 
f (map (fst o fst) args) (map snd args) 

10936  679 
> warn_extra_tfrees state 
680 
> check int; 

5820  681 

12146  682 
fun local_goal prepp kind f args = local_goal' prepp kind (K I) f args false; 
10936  683 

684 
val show = local_goal' ProofContext.bind_propp Show; 

685 
val show_i = local_goal' ProofContext.bind_propp_i Show; 

686 
val have = local_goal ProofContext.bind_propp Have; 

10380  687 
val have_i = local_goal ProofContext.bind_propp_i Have; 
5820  688 

689 

690 

691 
(** conclusions **) 

692 

693 
(* current goal *) 

694 

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

7176  698 
fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) = 
6404  699 
raise STATE ("No goal in this block!", state) 
7176  700 
 assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) = 
6404  701 
raise STATE ("Goal present in this block!", state) 
702 
 assert_current_goal _ state = state; 

5820  703 

12010  704 
fun assert_bottom b (state as State (_, nodes)) = 
705 
let val bot = (length nodes <= 2) in 

706 
if b andalso not bot then raise STATE ("Not at bottom of proof!", state) 

707 
else if not b andalso bot then raise STATE ("Already at bottom of proof!", state) 

708 
else state 

709 
end; 

5820  710 

6404  711 
val at_bottom = can (assert_bottom true o close_block); 
712 

6932  713 
fun end_proof bot state = 
5820  714 
state 
715 
> assert_forward 

716 
> close_block 

717 
> assert_bottom bot 

7011  718 
> assert_current_goal true 
719 
> goal_facts (K []); 

5820  720 

721 

6404  722 
(* local_qed *) 
5820  723 

6982  724 
fun finish_local (print_result, print_rule) state = 
5820  725 
let 
12146  726 
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), after_qed)) = current_goal state; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

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

729 

12146  730 
val ts = flat tss; 
731 
val results = prep_result state ts raw_thm; 

732 
val resultq = 

733 
results > map (ProofContext.export false goal_ctxt outer_ctxt) 

734 
> Seq.commute > Seq.map (Library.unflat tss); 

9469  735 

12146  736 
val (attss, opt_solve) = 
5820  737 
(case kind of 
12146  738 
Show attss => (attss, export_goals goal_ctxt print_rule results) 
739 
 Have attss => (attss, Seq.single) 

6932  740 
 _ => err_malformed "finish_local" state); 
5820  741 
in 
12146  742 
print_result goal_ctxt (kind_name (sign_of state) kind, names ~~ Library.unflat tss results); 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

743 
outer_state 
12146  744 
> auto_bind_facts (map (ProofContext.generalize goal_ctxt outer_ctxt) ts) 
9469  745 
> (fn st => Seq.map (fn res => 
12146  746 
have_thmss ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq) 
9469  747 
> (Seq.flat o Seq.map opt_solve) 
7176  748 
> (Seq.flat o Seq.map after_qed) 
5820  749 
end; 
750 

6982  751 
fun local_qed finalize print state = 
6404  752 
state 
6932  753 
> end_proof false 
6871  754 
> finalize 
6982  755 
> (Seq.flat o Seq.map (finish_local print)); 
5820  756 

757 

6404  758 
(* global_qed *) 
5820  759 

12085  760 
fun locale_prefix None f thy = f thy 
12096  761 
 locale_prefix (Some (loc, _)) f thy = 
762 
thy > Theory.add_path (Sign.base_name loc) > f >> Theory.parent_path; 

12085  763 

12146  764 
fun locale_add_thmss None _ = I 
765 
 locale_add_thmss (Some (loc, atts)) ths = Locale.add_thmss loc (map (rpair atts) ths); 

12065  766 

6950  767 
fun finish_global state = 
5820  768 
let 
12065  769 
fun export inner outer th = 
770 
(case Seq.pull (ProofContext.export false inner outer th) of 

771 
Some (th', _) => th' > Drule.local_standard 

772 
 None => raise STATE ("Internal failure of theorem export", state)); 

12010  773 

12146  774 
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state; 
12065  775 
val locale_ctxt = context_of (state > close_block); 
776 
val theory_ctxt = context_of (state > close_block > close_block); 

5820  777 

12146  778 
val ts = flat tss; 
779 
val locale_results = 

780 
prep_result state ts raw_thm > map (export goal_ctxt locale_ctxt); 

12223
d5e76c2e335c
finish_global: Drule.strip_shyps_warning (just for warning);
wenzelm
parents:
12167
diff
changeset

781 
val results = locale_results 
d5e76c2e335c
finish_global: Drule.strip_shyps_warning (just for warning);
wenzelm
parents:
12167
diff
changeset

782 
> map (Drule.strip_shyps_warning o export locale_ctxt theory_ctxt); 
12065  783 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

784 
val (k, (cname, catts), locale, attss) = 
12146  785 
(case kind of Theorem x => x  _ => err_malformed "finish_global" state); 
12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

786 
val (thy1, res') = 
12065  787 
theory_of state 
12146  788 
> locale_prefix locale (PureThy.have_thmss [Drule.kind k] 
789 
((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))) 

790 
>> locale_add_thmss locale (names ~~ Library.unflat tss locale_results); 

12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

791 
val thy2 = thy1 > PureThy.add_thmss [((cname, flat (map #2 res')), catts)] > #1; 
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

792 
in (thy2, (k, res')) end; 
5820  793 

10553  794 
(*note: clients should inspect first result only, as backtracking may destroy theory*) 
6950  795 
fun global_qed finalize state = 
5820  796 
state 
6932  797 
> end_proof true 
6871  798 
> finalize 
12065  799 
> Seq.map finish_global; 
5820  800 

801 

6896  802 

803 
(** blocks **) 

804 

805 
(* begin_block *) 

806 

807 
fun begin_block state = 

808 
state 

809 
> assert_forward 

810 
> new_block 

811 
> open_block; 

812 

813 

814 
(* end_block *) 

815 

816 
fun end_block state = 

817 
state 

818 
> assert_forward 

819 
> close_block 

820 
> assert_current_goal false 

821 
> close_block 

6932  822 
> transfer_facts state; 
6896  823 

824 

825 
(* next_block *) 

826 

827 
fun next_block state = 

828 
state 

829 
> assert_forward 

830 
> close_block 

8718  831 
> new_block 
832 
> reset_facts; 

6896  833 

834 

5820  835 
end; 
8152  836 

837 
structure BasicProof: BASIC_PROOF = Proof; 

838 
open BasicProof; 