author  wenzelm 
Wed, 09 Aug 2006 00:12:33 +0200  
changeset 20363  f34c5dbe74d5 
parent 20341  41e77e688886 
child 20872  528054ca23e3 
permissions  rwrr 
5820  1 
(* Title: Pure/Isar/proof.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

19000  5 
The Isar/VM proof language interpreter: maintains a structured flow of 
6 
context elements, goals, refinements, and facts. 

5820  7 
*) 
8 

9 
signature PROOF = 

10 
sig 

17756  11 
type context (*= Context.proof*) 
12 
type method (*= Method.method*) 

5820  13 
type state 
17359  14 
val init: context > state 
15 
val level: state > int 

16 
val assert_bottom: bool > state > state 

5820  17 
val context_of: state > context 
18 
val theory_of: state > theory 

13377  19 
val map_context: (context > context) > state > state 
17976  20 
val add_binds_i: (indexname * term option) list > state > state 
19078  21 
val put_thms: bool > string * thm list option > state > state 
22 
val put_thms_internal: string * thm list option > state > state 

6091  23 
val the_facts: state > thm list 
9469  24 
val the_fact: state > thm 
17450  25 
val put_facts: thm list option > state > state 
6891  26 
val assert_forward: state > state 
17359  27 
val assert_chain: state > state 
9469  28 
val assert_forward_or_chain: state > state 
5820  29 
val assert_backward: state > state 
8206  30 
val assert_no_chain: state > state 
5820  31 
val enter_forward: state > state 
17359  32 
val get_goal: state > context * (thm list * thm) 
19995  33 
val schematic_goal: state > bool 
16539  34 
val show_main_goal: bool ref 
6529  35 
val verbose: bool ref 
12423  36 
val pretty_state: int > state > Pretty.T list 
10360  37 
val pretty_goals: bool > state > Pretty.T list 
17112  38 
val refine: Method.text > state > state Seq.seq 
39 
val refine_end: Method.text > state > state Seq.seq 

18908  40 
val refine_insert: thm list > state > state 
20208  41 
val goal_tac: thm > int > tactic 
17359  42 
val refine_goals: (context > thm > unit) > context > thm list > state > state Seq.seq 
5936  43 
val match_bind: (string list * string) list > state > state 
44 
val match_bind_i: (term list * term) list > state > state 

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

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

46 
val let_bind_i: (term list * term) list > state > state 
19846  47 
val fix: (string * string option * mixfix) list > state > state 
48 
val fix_i: (string * typ option * mixfix) list > state > state 

20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

49 
val assm: Assumption.export > 
19585  50 
((string * Attrib.src list) * (string * string list) list) list > state > state 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

51 
val assm_i: Assumption.export > 
19585  52 
((string * attribute list) * (term * term list) list) list > state > state 
53 
val assume: ((string * Attrib.src list) * (string * string list) list) list > state > state 

54 
val assume_i: ((string * attribute list) * (term * term list) list) list > state > state 

55 
val presume: ((string * Attrib.src list) * (string * string list) list) list > state > state 

56 
val presume_i: ((string * attribute list) * (term * term list) list) list > state > state 

19846  57 
val def: ((string * Attrib.src list) * 
58 
((string * mixfix) * (string * string list))) list > state > state 

59 
val def_i: ((string * attribute list) * 

60 
((string * mixfix) * (term * term list))) list > state > state 

17359  61 
val chain: state > state 
62 
val chain_facts: thm list > state > state 

63 
val get_thmss: state > (thmref * Attrib.src list) list > thm list 

14564  64 
val simple_note_thms: string > thm list > state > state 
17359  65 
val note_thmss: ((string * Attrib.src list) * 
17112  66 
(thmref * Attrib.src list) list) list > state > state 
18728  67 
val note_thmss_i: ((string * attribute list) * 
68 
(thm list * attribute list) list) list > state > state 

17112  69 
val from_thmss: ((thmref * Attrib.src list) list) list > state > state 
18728  70 
val from_thmss_i: ((thm list * attribute list) list) list > state > state 
17112  71 
val with_thmss: ((thmref * Attrib.src list) list) list > state > state 
18728  72 
val with_thmss_i: ((thm list * attribute list) list) list > state > state 
18548  73 
val using: ((thmref * Attrib.src list) list) list > state > state 
18728  74 
val using_i: ((thm list * attribute list) list) list > state > state 
18548  75 
val unfolding: ((thmref * Attrib.src list) list) list > state > state 
18728  76 
val unfolding_i: ((thm list * attribute list) list) list > state > state 
17112  77 
val invoke_case: string * string option list * Attrib.src list > state > state 
18728  78 
val invoke_case_i: string * string option list * attribute list > state > state 
17359  79 
val begin_block: state > state 
80 
val next_block: state > state 

20309  81 
val end_block: state > state 
17112  82 
val proof: Method.text option > state > state Seq.seq 
83 
val defer: int option > state > state Seq.seq 

84 
val prefer: int > state > state Seq.seq 

85 
val apply: Method.text > state > state Seq.seq 

86 
val apply_end: Method.text > state > state Seq.seq 

17359  87 
val goal_names: string option > string > string list > string 
88 
val local_goal: (context > ((string * string) * (string * thm list) list) > unit) > 

18728  89 
(theory > 'a > attribute) > 
17359  90 
(context * 'b list > context * (term list list * (context > context))) > 
18124  91 
string > Method.text option > (thm list list > state > state Seq.seq) > 
17359  92 
((string * 'a list) * 'b) list > state > state 
93 
val local_qed: Method.text option * bool > state > state Seq.seq 

94 
val global_goal: (context > (string * string) * (string * thm list) list > unit) > 

18728  95 
(theory > 'a > attribute) > 
17450  96 
(context * 'b list > context * (term list list * (context > context))) > 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

97 
string > Method.text option > (thm list list > context > context) > 
17859  98 
string option > string * 'a list > ((string * 'a list) * 'b) list > context > state 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

99 
val global_qed: Method.text option * bool > state > context 
17359  100 
val local_terminal_proof: Method.text * Method.text option > state > state Seq.seq 
101 
val local_default_proof: state > state Seq.seq 

102 
val local_immediate_proof: state > state Seq.seq 

103 
val local_done_proof: state > state Seq.seq 

104 
val local_skip_proof: bool > state > state Seq.seq 

20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

105 
val global_terminal_proof: Method.text * Method.text option > state > context 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

106 
val global_default_proof: state > context 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

107 
val global_immediate_proof: state > context 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

108 
val global_done_proof: state > context 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

109 
val global_skip_proof: bool > state > context 
18124  110 
val have: Method.text option > (thm list list > state > state Seq.seq) > 
19585  111 
((string * Attrib.src list) * (string * string list) list) list > bool > state > state 
18124  112 
val have_i: Method.text option > (thm list list > state > state Seq.seq) > 
19585  113 
((string * attribute list) * (term * term list) list) list > bool > state > state 
18124  114 
val show: Method.text option > (thm list list > state > state Seq.seq) > 
19585  115 
((string * Attrib.src list) * (string * string list) list) list > bool > state > state 
18124  116 
val show_i: Method.text option > (thm list list > state > state Seq.seq) > 
19585  117 
((string * attribute list) * (term * term list) list) list > bool > state > state 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

118 
val theorem: string > Method.text option > (thm list list > context > context) > 
17359  119 
string option > string * Attrib.src list > 
19585  120 
((string * Attrib.src list) * (string * string list) list) list > context > state 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

121 
val theorem_i: string > Method.text option > (thm list list > context > context) > 
18728  122 
string option > string * attribute list > 
19585  123 
((string * attribute list) * (term * term list) list) list > context > state 
5820  124 
end; 
125 

13377  126 
structure Proof: PROOF = 
5820  127 
struct 
128 

20309  129 
type context = Context.proof; 
17112  130 
type method = Method.method; 
16813  131 

5820  132 

133 
(** proof state **) 

134 

17359  135 
(* datatype state *) 
5820  136 

17112  137 
datatype mode = Forward  Chain  Backward; 
5820  138 

17359  139 
datatype state = 
140 
State of node Stack.T 

141 
and node = 

7176  142 
Node of 
143 
{context: context, 

144 
facts: thm list option, 

145 
mode: mode, 

17359  146 
goal: goal option} 
147 
and goal = 

148 
Goal of 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

149 
{statement: string * term list list, (*goal kind and statement, starting with vars*) 
17359  150 
using: thm list, (*goal facts*) 
151 
goal: thm, (*subgoals ==> statement*) 

17859  152 
before_qed: Method.text option, 
18124  153 
after_qed: 
154 
(thm list list > state > state Seq.seq) * 

20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

155 
(thm list list > context > context)}; 
17359  156 

17859  157 
fun make_goal (statement, using, goal, before_qed, after_qed) = 
158 
Goal {statement = statement, using = using, goal = goal, 

159 
before_qed = before_qed, after_qed = after_qed}; 

5820  160 

7176  161 
fun make_node (context, facts, mode, goal) = 
162 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

163 

17359  164 
fun map_node f (Node {context, facts, mode, goal}) = 
165 
make_node (f (context, facts, mode, goal)); 

5820  166 

17359  167 
fun init ctxt = State (Stack.init (make_node (ctxt, NONE, Forward, NONE))); 
5820  168 

17359  169 
fun current (State st) = Stack.top st > (fn Node node => node); 
170 
fun map_current f (State st) = State (Stack.map (map_node f) st); 

12045  171 

5820  172 

173 

174 
(** basic proof state operations **) 

175 

17359  176 
(* block structure *) 
177 

178 
fun open_block (State st) = State (Stack.push st); 

179 

18678  180 
fun close_block (State st) = State (Stack.pop st) 
181 
handle Empty => error "Unbalanced block parentheses"; 

17359  182 

183 
fun level (State st) = Stack.level st; 

184 

185 
fun assert_bottom b state = 

186 
let val b' = (level state <= 2) in 

18678  187 
if b andalso not b' then error "Not at bottom of proof!" 
188 
else if not b andalso b' then error "Already at bottom of proof!" 

17359  189 
else state 
190 
end; 

191 

192 

5820  193 
(* context *) 
194 

17359  195 
val context_of = #context o current; 
5820  196 
val theory_of = ProofContext.theory_of o context_of; 
197 

17359  198 
fun map_context f = 
199 
map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 

5820  200 

17359  201 
fun map_context_result f state = 
17859  202 
f (context_of state) > (fn ctxt => map_context (K ctxt) state); 
5820  203 

10809  204 
val add_binds_i = map_context o ProofContext.add_binds_i; 
19078  205 
val put_thms = map_context oo ProofContext.put_thms; 
206 
val put_thms_internal = map_context o ProofContext.put_thms_internal; 

5820  207 

208 

209 
(* facts *) 

210 

17359  211 
val get_facts = #facts o current; 
212 

213 
fun the_facts state = 

214 
(case get_facts state of SOME facts => facts 

18678  215 
 NONE => error "No current facts available"); 
5820  216 

9469  217 
fun the_fact state = 
17359  218 
(case the_facts state of [thm] => thm 
18678  219 
 _ => error "Single theorem expected"); 
7605  220 

17359  221 
fun put_facts facts = 
19078  222 
map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> 
223 
put_thms_internal (AutoBind.thisN, facts); 

5820  224 

17359  225 
fun these_factss more_facts (named_factss, state) = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

226 
(named_factss, state > put_facts (SOME (maps snd named_factss @ more_facts))); 
5820  227 

17359  228 
fun export_facts inner outer = 
229 
(case get_facts inner of 

20309  230 
NONE => put_facts NONE outer 
17359  231 
 SOME thms => 
232 
thms 

20309  233 
> ProofContext.export (context_of inner) (context_of outer) 
234 
> (fn ths => put_facts (SOME ths) outer)); 

5820  235 

236 

237 
(* mode *) 

238 

17359  239 
val get_mode = #mode o current; 
5820  240 
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); 
241 

17359  242 
val mode_name = (fn Forward => "state"  Chain => "chain"  Backward => "prove"); 
5820  243 

244 
fun assert_mode pred state = 

245 
let val mode = get_mode state in 

246 
if pred mode then state 

18678  247 
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode") 
5820  248 
end; 
249 

19308  250 
val assert_forward = assert_mode (fn mode => mode = Forward); 
251 
val assert_chain = assert_mode (fn mode => mode = Chain); 

252 
val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain); 

253 
val assert_backward = assert_mode (fn mode => mode = Backward); 

254 
val assert_no_chain = assert_mode (fn mode => mode <> Chain); 

5820  255 

17359  256 
val enter_forward = put_mode Forward; 
257 
val enter_chain = put_mode Chain; 

258 
val enter_backward = put_mode Backward; 

5820  259 

17359  260 

261 
(* current goal *) 

262 

263 
fun current_goal state = 

264 
(case current state of 

265 
{context, goal = SOME (Goal goal), ...} => (context, goal) 

18678  266 
 _ => error "No current goal!"); 
5820  267 

17359  268 
fun assert_current_goal g state = 
269 
let val g' = can current_goal state in 

18678  270 
if g andalso not g' then error "No goal in this block!" 
271 
else if not g andalso g' then error "Goal present in this block!" 

17359  272 
else state 
273 
end; 

6776  274 

17359  275 
fun put_goal goal = map_current (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal)); 
276 

17859  277 
val before_qed = #before_qed o #2 o current_goal; 
278 

17359  279 

280 
(* nested goal *) 

5820  281 

17359  282 
fun map_goal f g (State (Node {context, facts, mode, goal = SOME goal}, nodes)) = 
283 
let 

17859  284 
val Goal {statement, using, goal, before_qed, after_qed} = goal; 
285 
val goal' = make_goal (g (statement, using, goal, before_qed, after_qed)); 

17359  286 
in State (make_node (f context, facts, mode, SOME goal'), nodes) end 
287 
 map_goal f g (State (nd, node :: nodes)) = 

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

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

290 
 map_goal _ _ state = state; 

5820  291 

19188  292 
fun set_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) => 
293 
(statement, using, goal, before_qed, after_qed)); 

294 

17859  295 
fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) => 
296 
(statement, using, goal, before_qed, after_qed)); 

17359  297 

298 
local 

299 
fun find i state = 

300 
(case try current_goal state of 

301 
SOME (ctxt, goal) => (ctxt, (i, goal)) 

18678  302 
 NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present")); 
17359  303 
in val find_goal = find 0 end; 
304 

305 
fun get_goal state = 

306 
let val (ctxt, (_, {using, goal, ...})) = find_goal state 

307 
in (ctxt, (using, goal)) end; 

5820  308 

19995  309 
fun schematic_goal state = 
310 
let 

311 
val (_, (_, {statement = (_, propss), ...})) = find_goal state; 

312 
val tvars = fold (fold Term.add_tvars) propss []; 

313 
val vars = fold (fold Term.add_vars) propss []; 

314 
in not (null tvars andalso null vars) end; 

315 

5820  316 

317 

12423  318 
(** pretty_state **) 
5820  319 

13869  320 
val show_main_goal = ref false; 
16539  321 
val verbose = ProofContext.verbose; 
13698  322 

14876  323 
val pretty_goals_local = Display.pretty_goals_aux o ProofContext.pp; 
12085  324 

15531  325 
fun pretty_facts _ _ NONE = [] 
326 
 pretty_facts s ctxt (SOME ths) = 

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

17359  329 
fun pretty_state nr state = 
5820  330 
let 
17359  331 
val {context, facts, mode, goal = _} = current state; 
332 
val ref (_, _, bg) = Display.current_goals_markers; 

5820  333 

334 
fun levels_up 0 = "" 

17359  335 
 levels_up 1 = "1 level up" 
336 
 levels_up i = string_of_int i ^ " levels up"; 

5820  337 

11556  338 
fun subgoals 0 = "" 
17359  339 
 subgoals 1 = "1 subgoal" 
340 
 subgoals n = string_of_int n ^ " subgoals"; 

341 

342 
fun description strs = 

343 
(case filter_out (equal "") strs of [] => "" 

344 
 strs' => enclose " (" ")" (commas strs')); 

12146  345 

17859  346 
fun prt_goal (SOME (ctxt, (i, {statement = (kind, _), using, goal, before_qed, after_qed}))) = 
17359  347 
pretty_facts "using " ctxt 
348 
(if mode <> Backward orelse null using then NONE else SOME using) @ 

349 
[Pretty.str ("goal" ^ description [kind, levels_up (i div 2), 

350 
subgoals (Thm.nprems_of goal)] ^ ":")] @ 

351 
pretty_goals_local ctxt bg (true, ! show_main_goal) (! Display.goals_limit) goal 

352 
 prt_goal NONE = []; 

6848  353 

17359  354 
val prt_ctxt = 
355 
if ! verbose orelse mode = Forward then ProofContext.pretty_context context 

18670  356 
else if mode = Backward then ProofContext.pretty_ctxt context 
7575  357 
else []; 
17359  358 
in 
359 
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ 

360 
(if ! verbose then ", depth " ^ string_of_int (level state div 2  1) else "")), 

361 
Pretty.str ""] @ 

362 
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ 

363 
(if ! verbose orelse mode = Forward then 

364 
pretty_facts "" context facts @ prt_goal (try find_goal state) 

365 
else if mode = Chain then pretty_facts "picking " context facts 

366 
else prt_goal (try find_goal state)) 

367 
end; 

5820  368 

12085  369 
fun pretty_goals main state = 
19188  370 
let val (ctxt, (_, goal)) = get_goal state 
17359  371 
in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) goal end; 
10320  372 

5820  373 

374 

375 
(** proof steps **) 

376 

17359  377 
(* refine via method *) 
5820  378 

8234  379 
local 
380 

16146  381 
fun goalN i = "goal" ^ string_of_int i; 
382 
fun goals st = map goalN (1 upto Thm.nprems_of st); 

383 

384 
fun no_goal_cases st = map (rpair NONE) (goals st); 

385 

386 
fun goal_cases st = 

18607  387 
RuleCases.make_common true (Thm.theory_of_thm st, Thm.prop_of st) (map (rpair []) (goals st)); 
16146  388 

17112  389 
fun apply_method current_context meth_fun state = 
6848  390 
let 
17859  391 
val (goal_ctxt, (_, {statement, using, goal, before_qed, after_qed})) = find_goal state; 
17112  392 
val meth = meth_fun (if current_context then context_of state else goal_ctxt); 
16146  393 
in 
18228  394 
Method.apply meth using goal > Seq.map (fn (meth_cases, goal') => 
6848  395 
state 
16146  396 
> map_goal 
18475  397 
(ProofContext.add_cases false (no_goal_cases goal @ goal_cases goal') #> 
398 
ProofContext.add_cases true meth_cases) 

17859  399 
(K (statement, using, goal', before_qed, after_qed))) 
16146  400 
end; 
5820  401 

19188  402 
fun select_goals n meth state = 
19224  403 
state 
404 
> (#2 o #2 o get_goal) 

405 
> ALLGOALS Tactic.conjunction_tac 

406 
> Seq.maps (fn goal => 

19188  407 
state 
19224  408 
> Seq.lift set_goal (Goal.extract 1 n goal > Seq.maps (Tactic.conjunction_tac 1)) 
19188  409 
> Seq.maps meth 
410 
> Seq.maps (fn state' => state' 

411 
> Seq.lift set_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal)) 

19224  412 
> Seq.maps (apply_method true (K Method.succeed))); 
19188  413 

17112  414 
fun apply_text cc text state = 
415 
let 

416 
val thy = theory_of state; 

417 

418 
fun eval (Method.Basic m) = apply_method cc m 

419 
 eval (Method.Source src) = apply_method cc (Method.method thy src) 

20031  420 
 eval (Method.Source_i src) = apply_method cc (Method.method_i thy src) 
17112  421 
 eval (Method.Then txts) = Seq.EVERY (map eval txts) 
422 
 eval (Method.Orelse txts) = Seq.FIRST (map eval txts) 

423 
 eval (Method.Try txt) = Seq.TRY (eval txt) 

19188  424 
 eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt) 
425 
 eval (Method.SelectGoals (n, txt)) = select_goals n (eval txt); 

17112  426 
in eval text state end; 
427 

8234  428 
in 
429 

17112  430 
val refine = apply_text true; 
431 
val refine_end = apply_text false; 

8234  432 

18908  433 
fun refine_insert [] = I 
434 
 refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths))); 

435 

8234  436 
end; 
437 

5820  438 

17359  439 
(* refine via subproof *) 
440 

20208  441 
fun goal_tac rule = 
18186  442 
Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW 
443 
(Tactic.norm_hhf_tac THEN' (SUBGOAL (fn (goal, i) => 

444 
if can Logic.unprotect (Logic.strip_assums_concl goal) then 

445 
Tactic.etac Drule.protectI i 

446 
else all_tac))); 

11816  447 

19915  448 
fun refine_goals print_rule inner raw_rules state = 
449 
let 

450 
val (outer, (_, goal)) = get_goal state; 

20208  451 
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st); 
19915  452 
in 
453 
raw_rules 

20309  454 
> ProofContext.goal_export inner outer 
455 
> (fn rules => Seq.lift set_goal (EVERY (map refine rules) goal) state) 

19915  456 
end; 
17359  457 

6932  458 

17359  459 
(* conclude_goal *) 
6932  460 

18503
841137f20307
goal/qed: proper treatment of two levels of conjunctions;
wenzelm
parents:
18475
diff
changeset

461 
fun conclude_goal state goal propss = 
5820  462 
let 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

463 
val thy = theory_of state; 
5820  464 
val ctxt = context_of state; 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

465 
val string_of_term = ProofContext.string_of_term ctxt; 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

466 
val string_of_thm = ProofContext.string_of_thm ctxt; 
5820  467 

17359  468 
val ngoals = Thm.nprems_of goal; 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

469 
val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks 
17359  470 
(pretty_goals_local ctxt "" (true, ! show_main_goal) (! Display.goals_limit) goal @ 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

471 
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

472 

9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

473 
val extra_hyps = Assumption.extra_hyps ctxt goal; 
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

474 
val _ = null extra_hyps orelse 
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

475 
error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps)); 
5820  476 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

477 
val (results, th) = `(Conjunction.elim_precise (map length propss)) (Goal.conclude goal) 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

478 
handle THM _ => error ("Lost goal structure:\n" ^ string_of_thm goal); 
19862  479 
val _ = Unify.matches_list thy (flat propss) (map Thm.prop_of (flat results)) orelse 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

480 
error ("Proved a different theorem:\n" ^ string_of_thm th); 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

481 
in results end; 
5820  482 

483 

484 

485 
(*** structured proof commands ***) 

486 

17112  487 
(** context elements **) 
5820  488 

17112  489 
(* bindings *) 
5820  490 

16813  491 
local 
492 

17359  493 
fun gen_bind bind args state = 
5820  494 
state 
495 
> assert_forward 

18308  496 
> map_context (bind args #> snd) 
17359  497 
> put_facts NONE; 
5820  498 

16813  499 
in 
500 

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

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

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

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

504 
val let_bind_i = gen_bind (ProofContext.match_bind_i true); 
5820  505 

16813  506 
end; 
507 

5820  508 

17359  509 
(* fix *) 
9196  510 

12714  511 
local 
512 

18670  513 
fun gen_fix add_fixes args = 
17359  514 
assert_forward 
19846  515 
#> map_context (snd o add_fixes args) 
17359  516 
#> put_facts NONE; 
5820  517 

16813  518 
in 
519 

18670  520 
val fix = gen_fix ProofContext.add_fixes; 
521 
val fix_i = gen_fix ProofContext.add_fixes_i; 

5820  522 

16813  523 
end; 
524 

5820  525 

17359  526 
(* assume etc. *) 
5820  527 

16813  528 
local 
529 

17112  530 
fun gen_assume asm prep_att exp args state = 
5820  531 
state 
532 
> assert_forward 

17112  533 
> map_context_result (asm exp (Attrib.map_specs (prep_att (theory_of state)) args)) 
17359  534 
> these_factss [] > #2; 
6932  535 

16813  536 
in 
537 

18728  538 
val assm = gen_assume ProofContext.add_assms Attrib.attribute; 
18670  539 
val assm_i = gen_assume ProofContext.add_assms_i (K I); 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

540 
val assume = assm Assumption.assume_export; 
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

541 
val assume_i = assm_i Assumption.assume_export; 
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

542 
val presume = assm Assumption.presume_export; 
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

543 
val presume_i = assm_i Assumption.presume_export; 
5820  544 

16813  545 
end; 
546 

7271  547 

17359  548 
(* def *) 
11891  549 

16813  550 
local 
551 

19846  552 
fun gen_def gen_fix prep_att prep_binds args state = 
11891  553 
let 
554 
val _ = assert_forward state; 

17112  555 
val thy = theory_of state; 
11891  556 

19846  557 
val ((raw_names, raw_atts), (vars, raw_rhss)) = 
558 
args > split_list >> split_list > split_list; 

559 
val xs = map #1 vars; 

18308  560 
val names = map (fn ("", x) => Thm.def_name x  (name, _) => name) (raw_names ~~ xs); 
561 
val atts = map (map (prep_att thy)) raw_atts; 

562 
val (rhss, state') = state > map_context_result (prep_binds false (map swap raw_rhss)); 

18826  563 
val eqs = LocalDefs.mk_def (context_of state') (xs ~~ rhss); 
11891  564 
in 
18308  565 
state' 
19846  566 
> gen_fix (map (fn (x, mx) => (x, NONE, mx)) vars) 
19585  567 
> assm_i LocalDefs.def_export ((names ~~ atts) ~~ map (fn eq => [(eq, [])]) eqs) 
11891  568 
end; 
569 

16813  570 
in 
571 

18728  572 
val def = gen_def fix Attrib.attribute ProofContext.match_bind; 
18308  573 
val def_i = gen_def fix_i (K I) ProofContext.match_bind_i; 
11891  574 

16813  575 
end; 
576 

11891  577 

8374  578 

17112  579 
(** facts **) 
5820  580 

17359  581 
(* chain *) 
5820  582 

17359  583 
val chain = 
584 
assert_forward 

585 
#> tap the_facts 

586 
#> enter_chain; 

5820  587 

17359  588 
fun chain_facts facts = 
589 
put_facts (SOME facts) 

590 
#> chain; 

5820  591 

592 

17359  593 
(* note etc. *) 
17112  594 

17166  595 
fun no_binding args = map (pair ("", [])) args; 
17112  596 

597 
local 

598 

17359  599 
fun gen_thmss note_ctxt more_facts opt_chain opt_result prep_atts args state = 
17112  600 
state 
601 
> assert_forward 

602 
> map_context_result (note_ctxt (Attrib.map_facts (prep_atts (theory_of state)) args)) 

603 
> these_factss (more_facts state) 

17359  604 
> opt_chain 
605 
> opt_result; 

17112  606 

607 
in 

608 

18728  609 
val note_thmss = gen_thmss ProofContext.note_thmss (K []) I #2 Attrib.attribute; 
17359  610 
val note_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) I #2 (K I); 
17112  611 

612 
val from_thmss = 

18728  613 
gen_thmss ProofContext.note_thmss (K []) chain #2 Attrib.attribute o no_binding; 
17359  614 
val from_thmss_i = gen_thmss ProofContext.note_thmss_i (K []) chain #2 (K I) o no_binding; 
17112  615 

616 
val with_thmss = 

18728  617 
gen_thmss ProofContext.note_thmss the_facts chain #2 Attrib.attribute o no_binding; 
17359  618 
val with_thmss_i = gen_thmss ProofContext.note_thmss_i the_facts chain #2 (K I) o no_binding; 
619 

18808  620 
val local_results = 
621 
gen_thmss ProofContext.note_thmss_i (K []) I I (K I) o map (apsnd Thm.simple_fact); 

622 
fun global_results kind = PureThy.note_thmss_i kind o map (apsnd Thm.simple_fact); 

17359  623 

624 
fun get_thmss state srcs = the_facts (note_thmss [(("", []), srcs)] state); 

625 
fun simple_note_thms name thms = note_thmss_i [((name, []), [(thms, [])])]; 

17112  626 

627 
end; 

628 

629 

18548  630 
(* using/unfolding *) 
17112  631 

632 
local 

633 

18548  634 
fun gen_using f g note prep_atts args state = 
17112  635 
state 
636 
> assert_backward 

17166  637 
> map_context_result (note (Attrib.map_facts (prep_atts (theory_of state)) (no_binding args))) 
18843  638 
> (fn (named_facts, state') => 
639 
state' > map_goal I (fn (statement, using, goal, before_qed, after_qed) => 

640 
let 

641 
val ctxt = context_of state'; 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

642 
val ths = maps snd named_facts; 
18843  643 
in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); 
18548  644 

18843  645 
fun append_using _ ths using = using @ ths; 
18878  646 
fun unfold_using ctxt ths = map (LocalDefs.unfold ctxt ths); 
647 
val unfold_goals = LocalDefs.unfold_goals; 

17112  648 

649 
in 

650 

18843  651 
val using = gen_using append_using (K (K I)) ProofContext.note_thmss Attrib.attribute; 
652 
val using_i = gen_using append_using (K (K I)) ProofContext.note_thmss_i (K I); 

18826  653 
val unfolding = gen_using unfold_using unfold_goals ProofContext.note_thmss Attrib.attribute; 
654 
val unfolding_i = gen_using unfold_using unfold_goals ProofContext.note_thmss_i (K I); 

17112  655 

656 
end; 

657 

658 

659 
(* case *) 

660 

661 
local 

662 

663 
fun gen_invoke_case prep_att (name, xs, raw_atts) state = 

664 
let 

665 
val atts = map (prep_att (theory_of state)) raw_atts; 

19078  666 
val (asms, state') = state > map_context_result (fn ctxt => 
667 
ctxt > ProofContext.apply_case (ProofContext.get_case ctxt name xs)); 

19585  668 
val assumptions = asms > map (fn (a, ts) => ((a, atts), map (rpair []) ts)); 
17112  669 
in 
670 
state' 

17359  671 
> map_context (ProofContext.qualified_names #> ProofContext.no_base_names) 
17112  672 
> assume_i assumptions 
17976  673 
> add_binds_i AutoBind.no_facts 
17112  674 
> map_context (ProofContext.restore_naming (context_of state)) 
675 
> `the_facts > simple_note_thms name 

676 
end; 

677 

678 
in 

679 

18728  680 
val invoke_case = gen_invoke_case Attrib.attribute; 
17112  681 
val invoke_case_i = gen_invoke_case (K I); 
682 

683 
end; 

684 

685 

686 

17359  687 
(** proof structure **) 
688 

689 
(* blocks *) 

690 

691 
val begin_block = 

692 
assert_forward 

693 
#> open_block 

694 
#> put_goal NONE 

695 
#> open_block; 

696 

697 
val next_block = 

698 
assert_forward 

699 
#> close_block 

700 
#> open_block 

701 
#> put_goal NONE 

702 
#> put_facts NONE; 

703 

704 
fun end_block state = 

705 
state 

706 
> assert_forward 

707 
> close_block 

708 
> assert_current_goal false 

709 
> close_block 

710 
> export_facts state; 

711 

712 

713 
(* subproofs *) 

714 

715 
fun proof opt_text = 

716 
assert_backward 

17859  717 
#> refine (the_default Method.default_text opt_text) 
17359  718 
#> Seq.map (using_facts [] #> enter_forward); 
719 

720 
fun end_proof bot txt = 

721 
assert_forward 

722 
#> assert_bottom bot 

723 
#> close_block 

724 
#> assert_current_goal true 

725 
#> using_facts [] 

17859  726 
#> `before_qed #> (refine o the_default Method.succeed_text) 
727 
#> Seq.maps (refine (Method.finish_text txt)); 

17359  728 

729 

730 
(* unstructured refinement *) 

731 

732 
fun defer i = assert_no_chain #> refine (Method.Basic (K (Method.defer i))); 

733 
fun prefer i = assert_no_chain #> refine (Method.Basic (K (Method.prefer i))); 

734 

735 
fun apply text = assert_backward #> refine text #> Seq.map (using_facts []); 

736 
fun apply_end text = assert_forward #> refine_end text; 

737 

738 

739 

17112  740 
(** goals **) 
741 

17359  742 
(* goal names *) 
743 

744 
fun prep_names prep_att stmt = 

745 
let 

746 
val (names_attss, propp) = split_list (Attrib.map_specs prep_att stmt); 

747 
val (names, attss) = split_list names_attss; 

748 
in ((names, attss), propp) end; 

5820  749 

17359  750 
fun goal_names target name names = 
17450  751 
(case target of NONE => ""  SOME "" => ""  SOME loc => " (in " ^ loc ^ ")") ^ 
17359  752 
(if name = "" then "" else " " ^ name) ^ 
753 
(case filter_out (equal "") names of [] => "" 

754 
 nms => " " ^ enclose "(" ")" (space_implode " and " (Library.take (7, nms) @ 

755 
(if length nms > 7 then ["..."] else [])))); 

756 

16813  757 

17359  758 
(* generic goals *) 
759 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

760 
local 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

761 

19846  762 
fun implicit_vars dest add props = 
763 
let 

764 
val (explicit_vars, props') = take_prefix (can dest) props >> map dest; 

765 
val vars = rev (subtract (op =) explicit_vars (fold add props [])); 

766 
val _ = 

767 
if null vars then () 

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

769 
commas_quote (map (Term.string_of_vname o fst) vars)); 

770 
in (rev vars, props') end; 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

771 

5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

772 
fun refine_terms n = 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

773 
refine (Method.Basic (K (Method.RAW_METHOD 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

774 
(K (HEADGOAL (PRECISE_CONJUNCTS n 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

775 
(HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI)))))))))) 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

776 
#> Seq.hd; 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

777 

5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

778 
in 
17359  779 

17859  780 
fun generic_goal prepp kind before_qed after_qed raw_propp state = 
5820  781 
let 
17359  782 
val thy = theory_of state; 
783 
val chaining = can assert_chain state; 

784 

785 
val ((propss, after_ctxt), goal_state) = 

5936  786 
state 
787 
> assert_forward_or_chain 

788 
> enter_forward 

17359  789 
> open_block 
17859  790 
> map_context_result (fn ctxt => swap (prepp (ctxt, raw_propp))); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

791 
val props = flat propss; 
15703  792 

19846  793 
val (_, props') = 
794 
implicit_vars (dest_TVar o Logic.dest_type o Logic.dest_term) Term.add_tvars props; 

795 
val (vars, _) = implicit_vars (dest_Var o Logic.dest_term) Term.add_vars props'; 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

796 

5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

797 
val propss' = map (Logic.mk_term o Var) vars :: propss; 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

798 
val goal = Goal.init (Thm.cterm_of thy (Logic.mk_conjunction_list2 propss')); 
18124  799 
val after_qed' = after_qed >> (fn after_local => 
800 
fn results => map_context after_ctxt #> after_local results); 

5820  801 
in 
17359  802 
goal_state 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19862
diff
changeset

803 
> map_context (Variable.set_body true) 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

804 
> put_goal (SOME (make_goal ((kind, propss'), [], goal, before_qed, after_qed'))) 
18475  805 
> map_context (ProofContext.add_cases false (AutoBind.cases thy props)) 
17359  806 
> map_context (ProofContext.auto_bind_goal props) 
807 
> K chaining ? (`the_facts #> using_facts) 

808 
> put_facts NONE 

809 
> open_block 

810 
> put_goal NONE 

5820  811 
> enter_backward 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

812 
> K (not (null vars)) ? refine_terms (length propss') 
17450  813 
> K (null props) ? (refine (Method.Basic Method.assumption) #> Seq.hd) 
5820  814 
end; 
815 

17359  816 
fun generic_qed state = 
12503  817 
let 
18548  818 
val (goal_ctxt, {statement = (_, stmt), using = _, goal, before_qed = _, after_qed}) = 
17859  819 
current_goal state; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

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

822 

18503
841137f20307
goal/qed: proper treatment of two levels of conjunctions;
wenzelm
parents:
18475
diff
changeset

823 
val props = 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

824 
flat (tl stmt) 
19915  825 
> Variable.exportT_terms goal_ctxt outer_ctxt; 
17359  826 
val results = 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

827 
tl (conclude_goal state goal stmt) 
20309  828 
> burrow (ProofContext.export goal_ctxt outer_ctxt); 
17359  829 
in 
830 
outer_state 

831 
> map_context (ProofContext.auto_bind_facts props) 

18124  832 
> pair (after_qed, results) 
17359  833 
end; 
834 

19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

835 
end; 
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

836 

9469  837 

17359  838 
(* local goals *) 
839 

17859  840 
fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state = 
17359  841 
let 
842 
val ((names, attss), propp) = prep_names (prep_att (theory_of state)) stmt; 

843 

18124  844 
fun after_qed' results = 
18808  845 
local_results ((names ~~ attss) ~~ results) 
17359  846 
#> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) 
18124  847 
#> after_qed results; 
5820  848 
in 
17359  849 
state 
18124  850 
> generic_goal prepp (kind ^ goal_names NONE "" names) before_qed (after_qed', K I) propp 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19862
diff
changeset

851 
> tap (Variable.warn_extra_tfrees (context_of state) o context_of) 
5820  852 
end; 
853 

17359  854 
fun local_qed txt = 
20309  855 
end_proof false txt #> 
856 
Seq.maps (generic_qed #> (fn ((after_qed, _), results) => after_qed results)); 

5820  857 

858 

17359  859 
(* global goals *) 
860 

861 
fun global_goal print_results prep_att prepp 

17859  862 
kind before_qed after_qed target (name, raw_atts) stmt ctxt = 
17359  863 
let 
864 
val thy = ProofContext.theory_of ctxt; 

865 
val thy_ctxt = ProofContext.init thy; 

866 

867 
val atts = map (prep_att thy) raw_atts; 

868 
val ((names, attss), propp) = prep_names (prep_att thy) stmt; 

869 

17450  870 
fun store_results prfx res = 
871 
K (prfx <> "") ? (Sign.add_path prfx #> Sign.no_base_names) 

872 
#> global_results kind ((names ~~ attss) ~~ res) 

17359  873 
#> (fn res' => 
874 
(print_results thy_ctxt ((kind, name), res') : unit; 

19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

875 
#2 o global_results kind [((name, atts), maps #2 res')])) 
17450  876 
#> Sign.restore_naming thy; 
17359  877 

18124  878 
fun after_qed' results = 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

879 
ProofContext.theory 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

880 
(case target of NONE => I 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

881 
 SOME prfx => store_results (NameSpace.base prfx) 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

882 
(map (ProofContext.export_standard ctxt thy_ctxt 
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

883 
#> map Drule.strip_shyps_warning) results)) 
18124  884 
#> after_qed results; 
17359  885 
in 
886 
init ctxt 

18670  887 
> generic_goal (prepp #> ProofContext.auto_fixes) (kind ^ goal_names target name names) 
18124  888 
before_qed (K Seq.single, after_qed') propp 
17359  889 
end; 
12065  890 

18678  891 
fun check_result msg sq = 
17112  892 
(case Seq.pull sq of 
18678  893 
NONE => error msg 
19475  894 
 SOME (s', sq') => Seq.cons s' sq'); 
17112  895 

17359  896 
fun global_qeds txt = 
897 
end_proof true txt 

20309  898 
#> Seq.map (generic_qed #> (fn (((_, after_qed), results), state) => 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

899 
after_qed results (context_of state))) 
17112  900 
> Seq.DETERM; (*backtracking may destroy theory!*) 
901 

18678  902 
fun global_qed txt = 
903 
global_qeds txt 

904 
#> check_result "Failed to finish proof" 

905 
#> Seq.hd; 

12959  906 

5820  907 

17359  908 
(* concluding steps *) 
17112  909 

17359  910 
fun local_terminal_proof (text, opt_text) = 
911 
proof (SOME text) #> Seq.maps (local_qed (opt_text, true)); 

17112  912 

913 
val local_default_proof = local_terminal_proof (Method.default_text, NONE); 

914 
val local_immediate_proof = local_terminal_proof (Method.this_text, NONE); 

17359  915 
val local_done_proof = proof (SOME Method.done_text) #> Seq.maps (local_qed (NONE, false)); 
916 
fun local_skip_proof int = local_terminal_proof (Method.sorry_text int, NONE); 

17112  917 

18678  918 
fun global_term_proof immed (text, opt_text) = 
919 
proof (SOME text) 

920 
#> check_result "Terminal proof method failed" 

921 
#> Seq.maps (global_qeds (opt_text, immed)) 

922 
#> check_result "Failed to finish proof (after successful terminal method)" 

923 
#> Seq.hd; 

17112  924 

925 
val global_terminal_proof = global_term_proof true; 

926 
val global_default_proof = global_terminal_proof (Method.default_text, NONE); 

927 
val global_immediate_proof = global_terminal_proof (Method.this_text, NONE); 

928 
val global_done_proof = global_term_proof false (Method.done_text, NONE); 

17359  929 
fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE); 
5820  930 

6896  931 

17359  932 
(* common goal statements *) 
933 

934 
local 

935 

17859  936 
fun gen_have prep_att prepp before_qed after_qed stmt int = 
937 
local_goal (ProofDisplay.print_results int) prep_att prepp "have" before_qed after_qed stmt; 

6896  938 

17859  939 
fun gen_show prep_att prepp before_qed after_qed stmt int state = 
17359  940 
let 
941 
val testing = ref false; 

942 
val rule = ref (NONE: thm option); 

943 
fun fail_msg ctxt = 

944 
"Local statement will fail to solve any pending goal" :: 

945 
(case ! rule of NONE => []  SOME th => [ProofDisplay.string_of_rule ctxt "Failed" th]) 

946 
> cat_lines; 

6896  947 

17359  948 
fun print_results ctxt res = 
949 
if ! testing then () else ProofDisplay.print_results int ctxt res; 

950 
fun print_rule ctxt th = 

951 
if ! testing then rule := SOME th 

952 
else if int then priority (ProofDisplay.string_of_rule ctxt "Successful" th) 

953 
else (); 

954 
val test_proof = 

955 
(Seq.pull oo local_skip_proof) true 

956 
> setmp testing true 

957 
> setmp proofs 0 

958 
> capture; 

6896  959 

18124  960 
fun after_qed' results = 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

961 
refine_goals print_rule (context_of state) (flat results) 
18124  962 
#> Seq.maps (after_qed results); 
17359  963 
in 
964 
state 

17859  965 
> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt 
17359  966 
> K int ? (fn goal_state => 
967 
(case test_proof goal_state of 

968 
Result (SOME _) => goal_state 

18678  969 
 Result NONE => error (fail_msg (context_of goal_state)) 
17359  970 
 Exn Interrupt => raise Interrupt 
971 
 Exn exn => raise EXCEPTION (exn, fail_msg (context_of goal_state)))) 

972 
end; 

973 

17859  974 
fun gen_theorem prep_att prepp kind before_qed after_qed target a = 
975 
global_goal ProofDisplay.present_results prep_att prepp kind before_qed after_qed target a; 

17359  976 

977 
in 

978 

18728  979 
val have = gen_have Attrib.attribute ProofContext.bind_propp; 
17359  980 
val have_i = gen_have (K I) ProofContext.bind_propp_i; 
18728  981 
val show = gen_show Attrib.attribute ProofContext.bind_propp; 
17359  982 
val show_i = gen_show (K I) ProofContext.bind_propp_i; 
18728  983 
val theorem = gen_theorem Attrib.attribute ProofContext.bind_propp_schematic; 
17359  984 
val theorem_i = gen_theorem (K I) ProofContext.bind_propp_schematic_i; 
6896  985 

5820  986 
end; 
17359  987 

988 
end; 