author  wenzelm 
Sun, 24 Feb 2002 21:47:33 +0100  
changeset 12930  c1f3ff5feff1 
parent 12808  a529b4b91888 
child 12959  bf48fd86a732 
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 
12423  41 
val pretty_state: int > state > Pretty.T list 
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 
12714  54 
val have_thmss: ((bstring * context attribute list) * 
55 
(xstring * context attribute list) list) list > state > state 

56 
val have_thmss_i: ((bstring * context attribute list) * 

9196  57 
(thm list * context attribute list) list) list > state > state 
12714  58 
val with_thmss: ((bstring * context attribute list) * 
59 
(xstring * context attribute list) list) list > state > state 

60 
val with_thmss_i: ((bstring * context attribute list) * 

9196  61 
(thm list * context attribute list) list) list > state > state 
12930  62 
val using_thmss: ((xstring * context attribute list) list) list > state > state 
63 
val using_thmss_i: ((thm list * context attribute list) list) list > state > state 

7412  64 
val fix: (string list * string option) list > state > state 
7665  65 
val fix_i: (string list * typ option) list > state > state 
9469  66 
val assm: ProofContext.exporter 
10464  67 
> ((string * context attribute list) * (string * (string list * string list)) list) list 
7271  68 
> state > state 
9469  69 
val assm_i: ProofContext.exporter 
10464  70 
> ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  71 
> state > state 
10464  72 
val assume: 
73 
((string * context attribute list) * (string * (string list * string list)) list) list 

7271  74 
> state > state 
10464  75 
val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  76 
> state > state 
10464  77 
val presume: 
78 
((string * context attribute list) * (string * (string list * string list)) list) list 

6932  79 
> state > state 
10464  80 
val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list 
6932  81 
> state > state 
11891  82 
val def: string > context attribute list > string * (string * string list) > state > state 
83 
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

84 
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

85 
val multi_theorem: string > bstring * theory attribute list 
12698  86 
> (xstring * context attribute list list) option > context attribute Locale.element list 
12146  87 
> ((bstring * theory attribute list) * (string * (string list * string list)) list) list 
88 
> theory > state 

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

89 
val multi_theorem_i: string > bstring * theory attribute list 
12698  90 
> (string * context attribute list list) option > context attribute Locale.element_i list 
12146  91 
> ((bstring * theory attribute list) * (term * (term list * term list)) list) list 
92 
> 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 
12244  112 
> (theory * ((string * 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 = 

12698  136 
Theorem of string * (*theorem kind*) 
137 
(bstring * theory attribute list) * (*common result binding*) 

138 
(string * context attribute list list) option * (*target locale and attributes*) 

139 
theory attribute list list  (*attributes of individual result binding*) 

140 
Show of context attribute list list  (*intermediate result, solving subgoal*) 

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 

12423  326 
(** pretty_state **) 
5820  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 

12423  337 
fun pretty_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 [] => "" 
12308  351 
 nms => " " ^ enclose "(" ")" (space_implode " and " (take (7, nms) @ 
352 
(if length nms > 7 then ["..."] else [])))); 

12146  353 

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

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

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

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

7575  364 
else []; 
8462  365 

366 
val prts = 

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

12146  372 
(pretty_facts "" ctxt facts @ prt_goal (find_goal state)) 
12085  373 
else if mode = ForwardChain then pretty_facts "picking " ctxt facts 
12146  374 
else prt_goal (find_goal state)) 
12423  375 
in prts end; 
5820  376 

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

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

10320  380 

5820  381 

382 

383 
(** proof steps **) 

384 

385 
(* datatype method *) 

386 

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

389 

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

391 
val method_cases = Method; 

5820  392 

393 

394 
(* refine goal *) 

395 

8234  396 
local 
397 

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

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

401 

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

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

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

8234  413 
in 
414 

415 
val refine = gen_refine true; 

416 
val refine_end = gen_refine false; 

417 

418 
end; 

419 

5820  420 

11917  421 
(* goal addressing *) 
6932  422 

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

8152  426 

8166  427 
fun HEADGOAL tac = tac 1; 
428 

9469  429 

430 
(* export results *) 

431 

11816  432 
fun refine_tac rule = 
12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

433 
Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) => 
11816  434 
if can Logic.dest_goal (Logic.strip_assums_concl goal) then 
435 
Tactic.etac Drule.triv_goal i 

436 
else all_tac)); 

437 

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

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

6932  448 

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

451 

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

454 
None => Seq.single (reset_facts state) 

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

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

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

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

461 

462 
(* prepare result *) 

463 

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

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

468 

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

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

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

481 
val th = raw_th RS Drule.rev_triv_goal; 

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

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

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))); 

12808
a529b4b91888
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12760
diff
changeset

487 
conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () => 
12146  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 

12714  512 
(* have_thmss *) 
5820  513 

12714  514 
local 
515 

516 
fun gen_have_thmss f args state = 

5820  517 
state 
518 
> assert_forward 

12714  519 
> map_context_result (f args) 
9196  520 
> these_factss; 
5820  521 

12714  522 
in 
523 

524 
val have_thmss = gen_have_thmss ProofContext.have_thmss; 

525 
val have_thmss_i = gen_have_thmss ProofContext.have_thmss_i; 

526 

527 
fun simple_have_thms name thms = have_thmss_i [((name, []), [(thms, [])])]; 

528 

529 
end; 

530 

531 

532 
(* with_thmss *) 

9196  533 

12714  534 
local 
535 

536 
fun gen_with_thmss f args state = 

537 
let val state' = state > f args 

9196  538 
in state' > simple_have_thms "" (the_facts state' @ the_facts state) end; 
6876  539 

12714  540 
in 
541 

542 
val with_thmss = gen_with_thmss have_thmss; 

543 
val with_thmss_i = gen_with_thmss have_thmss_i; 

544 

545 
end; 

546 

5820  547 

12930  548 
(* using_thmss *) 
549 

550 
local 

551 

552 
fun gen_using_thmss f args state = 

553 
state 

554 
> assert_backward 

555 
> map_context_result (f (map (pair ("", [])) args)) 

556 
> (fn (st, named_facts) => 

557 
let val (_, (_, ((result, (facts, thm)), f))) = find_goal st; 

558 
in st > map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), f)) end); 

559 

560 
in 

561 

562 
val using_thmss = gen_using_thmss ProofContext.have_thmss; 

563 
val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i; 

564 

565 
end; 

566 

567 

5820  568 
(* fix *) 
569 

570 
fun gen_fix f xs state = 

571 
state 

572 
> assert_forward 

573 
> map_context (f xs) 

574 
> reset_facts; 

575 

576 
val fix = gen_fix ProofContext.fix; 

577 
val fix_i = gen_fix ProofContext.fix_i; 

578 

579 

11891  580 
(* assume and presume *) 
5820  581 

9469  582 
fun gen_assume f exp args state = 
5820  583 
state 
584 
> assert_forward 

9469  585 
> map_context_result (f exp args) 
11924  586 
> these_factss; 
6932  587 

7271  588 
val assm = gen_assume ProofContext.assume; 
589 
val assm_i = gen_assume ProofContext.assume_i; 

11917  590 
val assume = assm ProofContext.export_assume; 
591 
val assume_i = assm_i ProofContext.export_assume; 

592 
val presume = assm ProofContext.export_presume; 

593 
val presume_i = assm_i ProofContext.export_presume; 

5820  594 

7271  595 

5820  596 

11891  597 
(** local definitions **) 
598 

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

600 
let 

601 
val _ = assert_forward state; 

602 
val ctxt = context_of state; 

603 

604 
(*rhs*) 

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

606 
val rhs = prep_term ctxt raw_rhs; 

607 
val T = Term.fastype_of rhs; 

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

609 

610 
(*lhs*) 

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

612 
in 

613 
state 

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

615 
> match_bind_i [(pats, rhs)] 

11917  616 
> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])] 
11891  617 
end; 
618 

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

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

621 

622 

8374  623 
(* invoke_case *) 
624 

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

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

628 
map_context_result (ProofContext.apply_case (get_case state name xs)) state; 
9292  629 
in 
10830  630 
state' 
10809  631 
> add_binds_i lets 
10830  632 
> assume_i [((name, atts), map (rpair ([], [])) asms)] 
8374  633 
end; 
634 

635 

5820  636 

637 
(** goals **) 

638 

639 
(* forward chaining *) 

640 

641 
fun chain state = 

642 
state 

643 
> assert_forward 

6848  644 
> assert_facts 
5820  645 
> enter_forward_chain; 
646 

647 
fun from_facts facts state = 

648 
state 

649 
> put_facts (Some facts) 

650 
> chain; 

651 

652 

653 
(* setup goals *) 

654 

11549  655 
val rule_contextN = "rule_context"; 
8991  656 

12534  657 
fun setup_goal opt_block prepp autofix kind after_qed names raw_propp state = 
5820  658 
let 
12146  659 
val (state', (propss, gen_binds)) = 
5936  660 
state 
661 
> assert_forward_or_chain 

662 
> enter_forward 

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

663 
> opt_block 
12534  664 
> map_context_result (fn ctxt => prepp (ctxt, raw_propp)); 
12808
a529b4b91888
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12760
diff
changeset

665 
val sign' = sign_of state'; 
12146  666 

667 
val props = flat propss; 

12808
a529b4b91888
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12760
diff
changeset

668 
val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props); 
7556  669 
val goal = Drule.mk_triv_goal cprop; 
10553  670 

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

5820  673 
in 
10553  674 
if null tvars then () 
675 
else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^ 

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

677 
if null vars then () 

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

12055  679 
commas (map (ProofContext.string_of_term (context_of state')) vars)); 
5936  680 
state' 
12146  681 
> map_context (autofix props) 
682 
> put_goal (Some (((kind, names, propss), ([], goal)), after_qed o map_context gen_binds)) 

12167  683 
> map_context (ProofContext.add_cases 
12808
a529b4b91888
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12760
diff
changeset

684 
(if length props = 1 then 
a529b4b91888
RuleCases.make interface based on term instead of thm;
wenzelm
parents:
12760
diff
changeset

685 
RuleCases.make true (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN] 
12167  686 
else [(rule_contextN, RuleCases.empty)])) 
12146  687 
> auto_bind_goal props 
5820  688 
> (if is_chain state then use_facts else reset_facts) 
689 
> new_block 

690 
> enter_backward 

691 
end; 

692 

693 
(*global goals*) 

12534  694 
fun global_goal prep kind a raw_locale elems args thy = 
12503  695 
let 
12549  696 
val init = init_state thy; 
12534  697 
val (opt_name, locale_ctxt, elems_ctxt, propp) = 
12549  698 
prep (apsome fst raw_locale) elems (map snd args) (context_of init); 
12534  699 
val locale = (case raw_locale of None => None  Some (_, atts) => Some (the opt_name, atts)); 
12503  700 
in 
12549  701 
init 
702 
> open_block 

12511  703 
> map_context (K locale_ctxt) 
12065  704 
> open_block 
12511  705 
> map_context (K elems_ctxt) 
12534  706 
> setup_goal I ProofContext.bind_propp_schematic_i 
707 
ProofContext.fix_frees (Theorem (kind, a, locale, map (snd o fst) args)) 

708 
Seq.single (map (fst o fst) args) propp 

12065  709 
end; 
5820  710 

12534  711 
val multi_theorem = global_goal Locale.read_context_statement; 
712 
val multi_theorem_i = global_goal Locale.cert_context_statement; 

12146  713 

5820  714 

715 
(*local goals*) 

12146  716 
fun local_goal' prepp kind (check: bool > state > state) f args int state = 
7928  717 
state 
12146  718 
> setup_goal open_block prepp (K I) (kind (map (snd o fst) args)) 
719 
f (map (fst o fst) args) (map snd args) 

10936  720 
> warn_extra_tfrees state 
721 
> check int; 

5820  722 

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

725 
val show = local_goal' ProofContext.bind_propp Show; 

726 
val show_i = local_goal' ProofContext.bind_propp_i Show; 

727 
val have = local_goal ProofContext.bind_propp Have; 

10380  728 
val have_i = local_goal ProofContext.bind_propp_i Have; 
5820  729 

730 

731 

732 
(** conclusions **) 

733 

734 
(* current goal *) 

735 

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

7176  739 
fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) = 
6404  740 
raise STATE ("No goal in this block!", state) 
7176  741 
 assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) = 
6404  742 
raise STATE ("Goal present in this block!", state) 
743 
 assert_current_goal _ state = state; 

5820  744 

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

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

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

749 
else state 

750 
end; 

5820  751 

6404  752 
val at_bottom = can (assert_bottom true o close_block); 
753 

6932  754 
fun end_proof bot state = 
5820  755 
state 
756 
> assert_forward 

757 
> close_block 

758 
> assert_bottom bot 

7011  759 
> assert_current_goal true 
760 
> goal_facts (K []); 

5820  761 

762 

6404  763 
(* local_qed *) 
5820  764 

6982  765 
fun finish_local (print_result, print_rule) state = 
5820  766 
let 
12146  767 
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

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

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

770 

12146  771 
val ts = flat tss; 
772 
val results = prep_result state ts raw_thm; 

773 
val resultq = 

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

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

9469  776 

12146  777 
val (attss, opt_solve) = 
5820  778 
(case kind of 
12146  779 
Show attss => (attss, export_goals goal_ctxt print_rule results) 
780 
 Have attss => (attss, Seq.single) 

6932  781 
 _ => err_malformed "finish_local" state); 
5820  782 
in 
12146  783 
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

784 
outer_state 
12549  785 
> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts) 
9469  786 
> (fn st => Seq.map (fn res => 
12714  787 
have_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq) 
9469  788 
> (Seq.flat o Seq.map opt_solve) 
7176  789 
> (Seq.flat o Seq.map after_qed) 
5820  790 
end; 
791 

6982  792 
fun local_qed finalize print state = 
6404  793 
state 
6932  794 
> end_proof false 
6871  795 
> finalize 
6982  796 
> (Seq.flat o Seq.map (finish_local print)); 
5820  797 

798 

12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

799 
(* global_qed *) 
12065  800 

6950  801 
fun finish_global state = 
5820  802 
let 
12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

803 
val export = Drule.local_standard ooo ProofContext.export_single; 
12146  804 
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state; 
12065  805 
val locale_ctxt = context_of (state > close_block); 
806 
val theory_ctxt = context_of (state > close_block > close_block); 

5820  807 

12146  808 
val ts = flat tss; 
12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

809 
val locale_results = map (export goal_ctxt locale_ctxt) (prep_result state ts raw_thm); 
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

810 
val results = map (Drule.strip_shyps_warning o export locale_ctxt theory_ctxt) locale_results; 
12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

811 
val (k, (cname, catts), locale, attss) = 
12146  812 
(case kind of Theorem x => x  _ => err_malformed "finish_global" state); 
12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

813 

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

814 
val (thy1, res') = 
12703
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

815 
theory_of state > Locale.add_thmss_hybrid k 
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

816 
((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results)) 
af5fec8a418f
refine_tac: Tactic.norm_hhf_tac before trying rule;
wenzelm
parents:
12698
diff
changeset

817 
locale (Library.unflat tss locale_results); 
12242
282a92bc5655
multi_theorem: common statement header (covers *all* results);
wenzelm
parents:
12223
diff
changeset

818 
val thy2 = thy1 > PureThy.add_thmss [((cname, flat (map #2 res')), catts)] > #1; 
12244  819 
in (thy2, ((k, cname), res')) end; 
5820  820 

10553  821 
(*note: clients should inspect first result only, as backtracking may destroy theory*) 
6950  822 
fun global_qed finalize state = 
5820  823 
state 
6932  824 
> end_proof true 
6871  825 
> finalize 
12065  826 
> Seq.map finish_global; 
5820  827 

828 

6896  829 

830 
(** blocks **) 

831 

832 
(* begin_block *) 

833 

834 
fun begin_block state = 

835 
state 

836 
> assert_forward 

837 
> new_block 

838 
> open_block; 

839 

840 

841 
(* end_block *) 

842 

843 
fun end_block state = 

844 
state 

845 
> assert_forward 

846 
> close_block 

847 
> assert_current_goal false 

848 
> close_block 

6932  849 
> transfer_facts state; 
6896  850 

851 

852 
(* next_block *) 

853 

854 
fun next_block state = 

855 
state 

856 
> assert_forward 

857 
> close_block 

8718  858 
> new_block 
859 
> reset_facts; 

6896  860 

861 

5820  862 
end; 
8152  863 

864 
structure BasicProof: BASIC_PROOF = Proof; 

865 
open BasicProof; 