author  wenzelm 
Fri, 13 Nov 2015 11:41:11 +0100  
changeset 61654  4a28eec739e9 
parent 61508  2c7e2ae6173d 
child 61655  f217bbe4e93e 
permissions  rwrr 
5820  1 
(* Title: Pure/Isar/proof.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

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

5820  6 
*) 
7 

8 
signature PROOF = 

9 
sig 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32856
diff
changeset

10 
type context = Proof.context 
23639  11 
type method = Method.method 
5820  12 
type state 
17359  13 
val init: context > state 
14 
val level: state > int 

15 
val assert_bottom: bool > state > state 

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

13377  18 
val map_context: (context > context) > state > state 
40642
99c6ce92669b
added useful function map_context_result to signature
bulwahn
parents:
40132
diff
changeset

19 
val map_context_result : (context > 'a * context) > state > 'a * state 
28278  20 
val map_contexts: (context > context) > state > state 
37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37186
diff
changeset

21 
val propagate_ml_env: state > state 
26251
b8c6259d366b
put_facts: do_props, i.e. facts are indexed by proposition again;
wenzelm
parents:
25958
diff
changeset

22 
val put_thms: bool > string * thm list option > state > state 
6091  23 
val the_facts: state > thm list 
9469  24 
val the_fact: state > thm 
47068  25 
val set_facts: thm list > state > state 
26 
val reset_facts: state > state 

6891  27 
val assert_forward: state > state 
17359  28 
val assert_chain: state > state 
9469  29 
val assert_forward_or_chain: state > state 
5820  30 
val assert_backward: state > state 
8206  31 
val assert_no_chain: state > state 
5820  32 
val enter_forward: state > state 
60369
f393a3fe884c
clarified signature  better support for Isar commands outside of Pure;
wenzelm
parents:
60094
diff
changeset

33 
val enter_chain: state > state 
f393a3fe884c
clarified signature  better support for Isar commands outside of Pure;
wenzelm
parents:
60094
diff
changeset

34 
val enter_backward: state > state 
58798
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

35 
val has_bottom_goal: state > bool 
60623  36 
val using_facts: thm list > state > state 
60403  37 
val pretty_state: 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 
60623  41 
val refine_primitive: (Proof.context > thm > thm) > state > state 
33288
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

42 
val raw_goal: state > {context: context, facts: thm list, goal: thm} 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

43 
val goal: state > {context: context, facts: thm list, goal: thm} 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

44 
val simple_goal: state > {context: context, goal: thm} 
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38333
diff
changeset

45 
val status_markup: state > Markup.T 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

46 
val let_bind: (term list * term) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

47 
val let_bind_cmd: (string list * string) list > state > state 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

48 
val write: Syntax.mode > (term * mixfix) list > state > state 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

49 
val write_cmd: Syntax.mode > (string * mixfix) list > state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

50 
val fix: (binding * typ option * mixfix) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

51 
val fix_cmd: (binding * string option * mixfix) list > state > state 
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

52 
val assm: Assumption.export > (binding * typ option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

53 
(term * term list) list list > (Thm.binding * (term * term list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

54 
state > state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

55 
val assm_cmd: Assumption.export > (binding * string option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

56 
(string * string list) list list > (Attrib.binding * (string * string list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

57 
state > state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

58 
val assume: (binding * typ option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

59 
(term * term list) list list > (Thm.binding * (term * term list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

60 
state > state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

61 
val assume_cmd: (binding * string option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

62 
(string * string list) list list > (Attrib.binding * (string * string list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

63 
state > state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

64 
val presume: (binding * typ option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

65 
(term * term list) list list > (Thm.binding * (term * term list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

66 
state > state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

67 
val presume_cmd: (binding * string option * mixfix) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

68 
(string * string list) list list > (Attrib.binding * (string * string list) list) list > 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

69 
state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

70 
val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

71 
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list > state > state 
17359  72 
val chain: state > state 
73 
val chain_facts: thm list > state > state 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

74 
val note_thmss: (Thm.binding * (thm list * attribute list) list) list > state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

75 
val note_thmss_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list > state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

76 
val from_thmss: ((thm list * attribute list) list) list > state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

77 
val from_thmss_cmd: ((Facts.ref * Token.src list) list) list > state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

78 
val with_thmss: ((thm list * attribute list) list) list > state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

79 
val with_thmss_cmd: ((Facts.ref * Token.src list) list) list > state > state 
60371  80 
val supply: (Thm.binding * (thm list * attribute list) list) list > state > state 
81 
val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list > state > state 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

82 
val using: ((thm list * attribute list) list) list > state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

83 
val using_cmd: ((Facts.ref * Token.src list) list) list > state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

84 
val unfolding: ((thm list * attribute list) list) list > state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

85 
val unfolding_cmd: ((Facts.ref * Token.src list) list) list > state > state 
60565  86 
val case_: Thm.binding * ((string * Position.T) * binding option list) > state > state 
87 
val case_cmd: Attrib.binding * ((string * Position.T) * binding option list) > state > state 

17359  88 
val begin_block: state > state 
89 
val next_block: state > state 

20309  90 
val end_block: state > state 
49042  91 
val begin_notepad: context > state 
92 
val end_notepad: state > context 

17112  93 
val proof: Method.text option > state > state Seq.seq 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

94 
val proof_results: Method.text_range option > state > state Seq.result Seq.seq 
49865  95 
val defer: int > state > state 
96 
val prefer: int > state > state 

17112  97 
val apply: Method.text > state > state Seq.seq 
98 
val apply_end: Method.text > state > state Seq.seq 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

99 
val apply_results: Method.text_range > state > state Seq.result Seq.seq 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

100 
val apply_end_results: Method.text_range > state > state Seq.result Seq.seq 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

101 
val local_qed: Method.text_range option * bool > state > state 
21442  102 
val theorem: Method.text option > (thm list list > context > context) > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

103 
(term * term list) list list > context > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

104 
val theorem_cmd: Method.text option > (thm list list > context > context) > 
21362
3a2ab1dce297
simplified Proof.theorem(_i) interface  removed target support;
wenzelm
parents:
21274
diff
changeset

105 
(string * string list) list list > context > state 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

106 
val global_qed: Method.text_range option * bool > state > context 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

107 
val local_terminal_proof: Method.text_range * Method.text_range option > state > state 
29383  108 
val local_default_proof: state > state 
109 
val local_immediate_proof: state > state 

110 
val local_skip_proof: bool > state > state 

111 
val local_done_proof: state > state 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

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

114 
val global_immediate_proof: state > context 
29383  115 
val global_skip_proof: bool > state > context 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

116 
val global_done_proof: state > context 
60406  117 
val internal_goal: (context > (string * string) * (string * thm list) list > unit) > 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

118 
Proof_Context.mode > bool > string > Method.text option > 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

119 
(context * thm list list > state > state) > 
60406  120 
(binding * typ option * mixfix) list > 
60414  121 
(Thm.binding * (term * term list) list) list > 
60461  122 
(Thm.binding * (term * term list) list) list > state > thm list * state 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

123 
val have: bool > Method.text option > (context * thm list list > state > state) > 
60406  124 
(binding * typ option * mixfix) list > 
60414  125 
(Thm.binding * (term * term list) list) list > 
60461  126 
(Thm.binding * (term * term list) list) list > bool > state > thm list * state 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

127 
val have_cmd: bool > Method.text option > (context * thm list list > state > state) > 
60406  128 
(binding * string option * mixfix) list > 
60414  129 
(Attrib.binding * (string * string list) list) list > 
60461  130 
(Attrib.binding * (string * string list) list) list > bool > state > thm list * state 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

131 
val show: bool > Method.text option > (context * thm list list > state > state) > 
60406  132 
(binding * typ option * mixfix) list > 
60414  133 
(Thm.binding * (term * term list) list) list > 
60461  134 
(Thm.binding * (term * term list) list) list > bool > state > thm list * state 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

135 
val show_cmd: bool > Method.text option > (context * thm list list > state > state) > 
60406  136 
(binding * string option * mixfix) list > 
60414  137 
(Attrib.binding * (string * string list) list) list > 
60461  138 
(Attrib.binding * (string * string list) list) list > bool > state > thm list * state 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

139 
val schematic_goal: state > bool 
51226
1973089f1dba
proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);
wenzelm
parents:
51222
diff
changeset

140 
val is_relevant: state > bool 
51318  141 
val future_proof: (state > ('a * context) future) > state > 'a future * state 
60403  142 
val local_future_terminal_proof: Method.text_range * Method.text_range option > state > state 
143 
val global_future_terminal_proof: Method.text_range * Method.text_range option > state > context 

5820  144 
end; 
145 

13377  146 
structure Proof: PROOF = 
5820  147 
struct 
148 

33031
b75c35574e04
backpatching of structure Proof and ProofContext  avoid odd aliases;
wenzelm
parents:
32856
diff
changeset

149 
type context = Proof.context; 
17112  150 
type method = Method.method; 
16813  151 

5820  152 

153 
(** proof state **) 

154 

17359  155 
(* datatype state *) 
5820  156 

17112  157 
datatype mode = Forward  Chain  Backward; 
5820  158 

17359  159 
datatype state = 
160 
State of node Stack.T 

161 
and node = 

7176  162 
Node of 
163 
{context: context, 

164 
facts: thm list option, 

165 
mode: mode, 

17359  166 
goal: goal option} 
167 
and goal = 

168 
Goal of 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

169 
{statement: (string * Position.T) * term list list * term, 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

170 
(*goal kind and statement (starting with vars), initial proposition*) 
25958  171 
using: thm list, (*goal facts*) 
172 
goal: thm, (*subgoals ==> statement*) 

17859  173 
before_qed: Method.text option, 
18124  174 
after_qed: 
60550  175 
(context * thm list list > state > state) * 
176 
(context * thm list list > context > context)}; 

17359  177 

58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

178 
fun make_goal (statement, using, goal, before_qed, after_qed) = 
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

179 
Goal {statement = statement, using = using, goal = goal, 
17859  180 
before_qed = before_qed, after_qed = after_qed}; 
5820  181 

7176  182 
fun make_node (context, facts, mode, goal) = 
183 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

184 

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

5820  187 

21727  188 
val init_context = 
42360  189 
Proof_Context.set_stmt true #> 
47005
421760a1efe7
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
wenzelm
parents:
46728
diff
changeset

190 
Proof_Context.map_naming (K Name_Space.local_naming); 
21727  191 

21466
6ffb8f455b84
init: enter inner statement mode, which prevents local notes from being named internally;
wenzelm
parents:
21451
diff
changeset

192 
fun init ctxt = 
21727  193 
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); 
5820  194 

58796  195 
fun top (State stack) = Stack.top stack > (fn Node node => node); 
196 
fun map_top f (State stack) = State (Stack.map_top (map_node f) stack); 

197 
fun map_all f (State stack) = State (Stack.map_all (map_node f) stack); 

12045  198 

5820  199 

200 

201 
(** basic proof state operations **) 

202 

17359  203 
(* block structure *) 
204 

58796  205 
fun open_block (State stack) = State (Stack.push stack); 
17359  206 

58796  207 
fun close_block (State stack) = State (Stack.pop stack) 
47060
e2741ec9ae36
prefer explicitly qualified exception List.Empty;
wenzelm
parents:
47005
diff
changeset

208 
handle List.Empty => error "Unbalanced block parentheses"; 
17359  209 

58796  210 
fun level (State stack) = Stack.level stack; 
17359  211 

212 
fun assert_bottom b state = 

47065  213 
let val b' = level state <= 2 in 
214 
if b andalso not b' then error "Not at bottom of proof" 

215 
else if not b andalso b' then error "Already at bottom of proof" 

17359  216 
else state 
217 
end; 

218 

219 

5820  220 
(* context *) 
221 

49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

222 
val context_of = #context o top; 
42360  223 
val theory_of = Proof_Context.theory_of o context_of; 
5820  224 

17359  225 
fun map_context f = 
49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

226 
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
5820  227 

17359  228 
fun map_context_result f state = 
17859  229 
f (context_of state) > (fn ctxt => map_context (K ctxt) state); 
5820  230 

28278  231 
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
232 

37949
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37186
diff
changeset

233 
fun propagate_ml_env state = map_contexts 
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37186
diff
changeset

234 
(Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state; 
48a874444164
moved management of auxiliary theory source files to Thy_Load  as theory data instead of accidental loader state;
wenzelm
parents:
37186
diff
changeset

235 

42360  236 
val put_thms = map_context oo Proof_Context.put_thms; 
5820  237 

238 

239 
(* facts *) 

240 

49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

241 
val get_facts = #facts o top; 
17359  242 

243 
fun the_facts state = 

60550  244 
(case get_facts state of 
245 
SOME facts => facts 

18678  246 
 NONE => error "No current facts available"); 
5820  247 

9469  248 
fun the_fact state = 
60550  249 
(case the_facts state of 
250 
[thm] => thm 

18678  251 
 _ => error "Single theorem expected"); 
7605  252 

17359  253 
fun put_facts facts = 
49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

254 
map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> 
33386  255 
put_thms true (Auto_Bind.thisN, facts); 
5820  256 

47068  257 
val set_facts = put_facts o SOME; 
258 
val reset_facts = put_facts NONE; 

259 

17359  260 
fun these_factss more_facts (named_factss, state) = 
47068  261 
(named_factss, state > set_facts (maps snd named_factss @ more_facts)); 
5820  262 

17359  263 
fun export_facts inner outer = 
264 
(case get_facts inner of 

47068  265 
NONE => reset_facts outer 
17359  266 
 SOME thms => 
267 
thms 

42360  268 
> Proof_Context.export (context_of inner) (context_of outer) 
47068  269 
> (fn ths => set_facts ths outer)); 
5820  270 

271 

272 
(* mode *) 

273 

49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

274 
val get_mode = #mode o top; 
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

275 
fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal)); 
5820  276 

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

279 
fun assert_mode pred state = 

280 
let val mode = get_mode state in 

281 
if pred mode then state 

18678  282 
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode") 
5820  283 
end; 
284 

19308  285 
val assert_forward = assert_mode (fn mode => mode = Forward); 
286 
val assert_chain = assert_mode (fn mode => mode = Chain); 

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

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

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

5820  290 

17359  291 
val enter_forward = put_mode Forward; 
292 
val enter_chain = put_mode Chain; 

293 
val enter_backward = put_mode Backward; 

5820  294 

17359  295 

296 
(* current goal *) 

297 

298 
fun current_goal state = 

49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

299 
(case top state of 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

300 
{context = ctxt, goal = SOME (Goal goal), ...} => (ctxt, goal) 
47065  301 
 _ => error "No current goal"); 
5820  302 

17359  303 
fun assert_current_goal g state = 
304 
let val g' = can current_goal state in 

47065  305 
if g andalso not g' then error "No goal in this block" 
306 
else if not g andalso g' then error "Goal present in this block" 

17359  307 
else state 
308 
end; 

6776  309 

49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

310 
fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal)); 
17359  311 

47068  312 
val set_goal = put_goal o SOME; 
313 
val reset_goal = put_goal NONE; 

314 

17859  315 
val before_qed = #before_qed o #2 o current_goal; 
316 

17359  317 

58798
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

318 
(* bottom goal *) 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

319 

49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

320 
fun has_bottom_goal (State stack) = 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

321 
let 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

322 
fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

323 
 bottom [Node {goal, ...}] = is_some goal 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

324 
 bottom [] = false 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

325 
 bottom (_ :: rest) = bottom rest; 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

326 
in bottom (op :: (Stack.dest stack)) end; 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

327 

49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58797
diff
changeset

328 

17359  329 
(* nested goal *) 
5820  330 

60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

331 
fun map_goal f (State stack) = 
58797  332 
(case Stack.dest stack of 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

333 
(Node {context = ctxt, facts, mode, goal = SOME goal}, node :: nodes) => 
17359  334 
let 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

335 
val Goal {statement, using, goal, before_qed, after_qed} = goal; 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

336 
val (ctxt', statement', using', goal', before_qed', after_qed') = 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

337 
f (ctxt, statement, using, goal, before_qed, after_qed); 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

338 
val goal' = make_goal (statement', using', goal', before_qed', after_qed'); 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

339 
in State (Stack.make (make_node (ctxt', facts, mode, SOME goal')) (node :: nodes)) end 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

340 
 (top_node, node :: nodes) => 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

341 
let 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

342 
val State stack' = map_goal f (State (Stack.make node nodes)); 
58797  343 
val (node', nodes') = Stack.dest stack'; 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

344 
in State (Stack.make top_node (node' :: nodes')) end 
58797  345 
 _ => State stack); 
5820  346 

60550  347 
fun provide_goal goal = 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

348 
map_goal (fn (ctxt, statement, using, _, before_qed, after_qed) => 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

349 
(ctxt, statement, using, goal, before_qed, after_qed)); 
19188  350 

60550  351 
fun using_facts using = 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

352 
map_goal (fn (ctxt, statement, _, goal, before_qed, after_qed) => 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

353 
(ctxt, statement, using, goal, before_qed, after_qed)); 
17359  354 

60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

355 
fun find_goal state = 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

356 
(case try current_goal state of 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

357 
SOME ctxt_goal => ctxt_goal 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

358 
 NONE => find_goal (close_block state handle ERROR _ => error "No proof goal")); 
17359  359 

360 
fun get_goal state = 

60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

361 
let val (ctxt, {using, goal, ...}) = find_goal state 
17359  362 
in (ctxt, (using, goal)) end; 
5820  363 

364 

365 

12423  366 
(** pretty_state **) 
5820  367 

59185  368 
local 
369 

15531  370 
fun pretty_facts _ _ NONE = [] 
59185  371 
 pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths]; 
372 

373 
fun pretty_sep prts [] = prts 

374 
 pretty_sep [] prts = prts 

375 
 pretty_sep prts1 prts2 = prts1 @ [Pretty.str ""] @ prts2; 

376 

377 
in 

6756  378 

60403  379 
fun pretty_state state = 
5820  380 
let 
49011
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

381 
val {context = ctxt, facts, mode, goal = _} = top state; 
42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42496
diff
changeset

382 
val verbose = Config.get ctxt Proof_Context.verbose; 
5820  383 

60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

384 
fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) = 
59185  385 
pretty_sep 
386 
(pretty_facts ctxt "using" 

387 
(if mode <> Backward orelse null using then NONE else SOME using)) 

388 
([Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal) 

17359  389 
 prt_goal NONE = []; 
6848  390 

17359  391 
val prt_ctxt = 
42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42496
diff
changeset

392 
if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt 
42360  393 
else if mode = Backward then Proof_Context.pretty_ctxt ctxt 
7575  394 
else []; 
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56898
diff
changeset

395 

293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56898
diff
changeset

396 
val position_markup = Position.markup (Position.thread_data ()) Markup.position; 
17359  397 
in 
56912
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56898
diff
changeset

398 
[Pretty.block 
60551  399 
[Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @ 
17359  400 
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ 
42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42496
diff
changeset

401 
(if verbose orelse mode = Forward then 
59185  402 
pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state)) 
51584  403 
else if mode = Chain then pretty_facts ctxt "picking" facts 
17359  404 
else prt_goal (try find_goal state)) 
405 
end; 

5820  406 

59185  407 
end; 
408 

5820  409 

410 

411 
(** proof steps **) 

412 

17359  413 
(* refine via method *) 
5820  414 

8234  415 
local 
416 

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

419 

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

421 

59970  422 
fun goal_cases ctxt st = 
423 
Rule_Cases.make_common ctxt (Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); 

16146  424 

58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58004
diff
changeset

425 
fun apply_method text ctxt state = 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

426 
find_goal state > (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) => 
58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58004
diff
changeset

427 
Method.evaluate text ctxt using goal 
58004  428 
> Seq.map (fn (meth_cases, goal') => 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

429 
let 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

430 
val goal_ctxt' = goal_ctxt 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

431 
> Proof_Context.update_cases_legacy (no_goal_cases goal @ goal_cases ctxt goal') 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

432 
> Proof_Context.update_cases meth_cases; 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

433 
val state' = state 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

434 
> map_goal (K (goal_ctxt', statement, using, goal', before_qed, after_qed)); 
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

435 
in state' end)); 
5820  436 

8234  437 
in 
438 

58007
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58004
diff
changeset

439 
fun refine text state = apply_method text (context_of state) state; 
671c607fb4af
just one context for Method.evaluate (in contrast to a989bdaf8121, but in accordance to old global situation);
wenzelm
parents:
58004
diff
changeset

440 
fun refine_end text state = apply_method text (#1 (find_goal state)) state; 
58004  441 

442 
fun refine_insert ths = 

443 
Seq.hd o refine (Method.Basic (K (Method.insert ths))); 

18908  444 

60623  445 
fun refine_primitive r = (* FIXME Seq.Error!? *) 
446 
Seq.hd o refine (Method.Basic (fn ctxt => fn _ => EMPTY_CASES (PRIMITIVE (r ctxt)))); 

447 

8234  448 
end; 
449 

5820  450 

17359  451 
(* refine via subproof *) 
452 

46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

453 
local 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

454 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

455 
fun finish_tac _ 0 = K all_tac 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

456 
 finish_tac ctxt n = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

457 
Goal.norm_hhf_tac ctxt THEN' 
30557
a28d83e903ce
goal_tac: finish marked assumptions from left to right  corresponds better with the strategy of etac, with significant performance gains in some situations;
wenzelm
parents:
30510
diff
changeset

458 
SUBGOAL (fn (goal, i) => 
a28d83e903ce
goal_tac: finish marked assumptions from left to right  corresponds better with the strategy of etac, with significant performance gains in some situations;
wenzelm
parents:
30510
diff
changeset

459 
if can Logic.unprotect (Logic.strip_assums_concl goal) then 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59185
diff
changeset

460 
eresolve_tac ctxt [Drule.protectI] i THEN finish_tac ctxt (n  1) i 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

461 
else finish_tac ctxt (n  1) (i + 1)); 
30557
a28d83e903ce
goal_tac: finish marked assumptions from left to right  corresponds better with the strategy of etac, with significant performance gains in some situations;
wenzelm
parents:
30510
diff
changeset

462 

54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

463 
fun goal_tac ctxt rule = 
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

464 
Goal.norm_hhf_tac ctxt THEN' 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59185
diff
changeset

465 
resolve_tac ctxt [rule] THEN' 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

466 
finish_tac ctxt (Thm.nprems_of rule); 
11816  467 

46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

468 
fun FINDGOAL tac st = 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

469 
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n) 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

470 
in find 1 (Thm.nprems_of st) st end; 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

471 

60595  472 
fun protect_prem i th = 
473 
Thm.bicompose NONE {flatten = false, match = false, incremented = true} 

474 
(false, Drule.incr_indexes th Drule.protectD, 1) i th 

475 
> Seq.hd; 

476 

477 
fun protect_prems th = 

478 
fold_rev protect_prem (1 upto Thm.nprems_of th) th; 

479 

46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

480 
in 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

481 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

482 
fun refine_goals print_rule result_ctxt result state = 
19915  483 
let 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

484 
val (goal_ctxt, (_, goal)) = get_goal state; 
60550  485 
fun refine rule st = 
486 
(print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st); 

19915  487 
in 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

488 
result 
60595  489 
> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems) 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

490 
> Proof_Context.goal_export result_ctxt goal_ctxt 
47068  491 
> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state) 
19915  492 
end; 
17359  493 

46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

494 
end; 
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
45666
diff
changeset

495 

6932  496 

49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
49748
diff
changeset

497 
(* conclude goal *) 
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
49748
diff
changeset

498 

28627
63663cfa297c
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28458
diff
changeset

499 
fun conclude_goal ctxt goal propss = 
5820  500 
let 
42360  501 
val thy = Proof_Context.theory_of ctxt; 
5820  502 

54981  503 
val _ = 
60948  504 
Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse 
59582  505 
error "Bad background theory of goal state"; 
49860  506 
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal); 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

507 

61268  508 
fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal); 
5820  509 

54567
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
53380
diff
changeset

510 
val th = 
60723
757cad5a3fe9
more aggressive compaction of multigoal proof terms (see also a8babbb6d5ea, 4dd0ba632e40);
wenzelm
parents:
60623
diff
changeset

511 
(Goal.conclude (if length (flat propss) > 1 then Thm.close_derivation goal else goal) 
60550  512 
handle THM _ => err_lost ()) 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58892
diff
changeset

513 
> Drule.flexflex_unique (SOME ctxt) 
61508  514 
> Thm.check_shyps ctxt 
54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

515 
> Thm.check_hyps (Context.Proof ctxt); 
23418  516 

517 
val goal_propss = filter_out null propss; 

518 
val results = 

519 
Conjunction.elim_balanced (length goal_propss) th 

520 
> map2 Conjunction.elim_balanced (map length goal_propss) 

60550  521 
handle THM _ => err_lost (); 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58892
diff
changeset

522 
val _ = 
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58892
diff
changeset

523 
Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results)) 
61268  524 
orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th); 
23418  525 

526 
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss 

527 
 recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss 

528 
 recover_result [] [] = [] 

60550  529 
 recover_result _ _ = err_lost (); 
23418  530 
in recover_result propss results end; 
5820  531 

49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

532 
val finished_goal_error = "Failed to finish proof"; 
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

533 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

534 
fun finished_goal pos state = 
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

535 
let val (ctxt, (_, goal)) = get_goal state in 
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

536 
if Thm.no_prems goal then Seq.Result state 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

537 
else 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

538 
Seq.Error (fn () => 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

539 
finished_goal_error ^ Position.here pos ^ ":\n" ^ 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

540 
Proof_Display.string_of_goal ctxt goal) 
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

541 
end; 
49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
49748
diff
changeset

542 

5820  543 

33288
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

544 
(* goal views  corresponding to methods *) 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

545 

bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

546 
fun raw_goal state = 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

547 
let val (ctxt, (facts, goal)) = get_goal state 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

548 
in {context = ctxt, facts = facts, goal = goal} end; 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

549 

bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

550 
val goal = raw_goal o refine_insert []; 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

551 

bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

552 
fun simple_goal state = 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

553 
let 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

554 
val (_, (facts, _)) = get_goal state; 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

555 
val (ctxt, (_, goal)) = get_goal (refine_insert facts state); 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

556 
in {context = ctxt, goal = goal} end; 
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

557 

38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38333
diff
changeset

558 
fun status_markup state = 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38333
diff
changeset

559 
(case try goal state of 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49912
diff
changeset

560 
SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal) 
38721
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38333
diff
changeset

561 
 NONE => Markup.empty); 
ca8b14fa0d0d
added some proof state markup, notably number of subgoals (e.g. for indentation);
wenzelm
parents:
38333
diff
changeset

562 

49866  563 
fun method_error kind pos state = 
564 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  565 

33288
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

566 

5820  567 

568 
(*** structured proof commands ***) 

569 

17112  570 
(** context elements **) 
5820  571 

36324  572 
(* let bindings *) 
5820  573 

16813  574 
local 
575 

17359  576 
fun gen_bind bind args state = 
5820  577 
state 
578 
> assert_forward 

36324  579 
> map_context (bind true args #> snd) 
47068  580 
> reset_facts; 
5820  581 

16813  582 
in 
583 

60377  584 
val let_bind = gen_bind Proof_Context.match_bind; 
585 
val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd; 

5820  586 

16813  587 
end; 
588 

5820  589 

36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

590 
(* concrete syntax *) 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

591 

79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

592 
local 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

593 

36507
c966a1aab860
'write': actually observe the proof structure (like 'let' or 'fix');
wenzelm
parents:
36505
diff
changeset

594 
fun gen_write prep_arg mode args = 
c966a1aab860
'write': actually observe the proof structure (like 'let' or 'fix');
wenzelm
parents:
36505
diff
changeset

595 
assert_forward 
42360  596 
#> map_context (fn ctxt => ctxt > Proof_Context.notation true mode (map (prep_arg ctxt) args)) 
47068  597 
#> reset_facts; 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

598 

55955
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

599 
fun read_arg ctxt (c, mx) = 
56002  600 
(case Proof_Context.read_const {proper = false, strict = false} ctxt c of 
55955
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

601 
Free (x, _) => 
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

602 
let val T = Proof_Context.infer_type ctxt (x, Mixfix.mixfixT mx) 
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

603 
in (Free (x, T), mx) end 
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

604 
 t => (t, mx)); 
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

605 

36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

606 
in 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

607 

79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

608 
val write = gen_write (K I); 
55955
e8f1bf005661
eliminated odd type constraint for read_const (see also 79c1d2bbe5a9);
wenzelm
parents:
55954
diff
changeset

609 
val write_cmd = gen_write read_arg; 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

610 

79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

611 
end; 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

612 

79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

613 

17359  614 
(* fix *) 
9196  615 

12714  616 
local 
617 

60469  618 
fun gen_fix add_fixes raw_fixes = 
17359  619 
assert_forward 
60469  620 
#> map_context (snd o add_fixes raw_fixes) 
47068  621 
#> reset_facts; 
5820  622 

16813  623 
in 
624 

60469  625 
val fix = gen_fix Proof_Context.add_fixes; 
626 
val fix_cmd = gen_fix Proof_Context.add_fixes_cmd; 

5820  627 

16813  628 
end; 
629 

5820  630 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

631 
(* structured clause *) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

632 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

633 
fun export_binds ctxt' ctxt binds = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

634 
let 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

635 
val rhss = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

636 
map (the_list o snd) binds 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

637 
> burrow (Variable.export_terms ctxt' ctxt) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

638 
> map (try the_single); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

639 
in map fst binds ~~ rhss end; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

640 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

641 
fun prep_clause prep_var prep_propp raw_fixes raw_assumes raw_shows ctxt = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

642 
let 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

643 
(*fixed variables*) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

644 
val ((xs', vars), fix_ctxt) = ctxt 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

645 
> fold_map prep_var raw_fixes 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

646 
> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

647 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

648 
(*propositions with term bindings*) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

649 
val (all_propss, binds) = prep_propp fix_ctxt (raw_assumes @ raw_shows); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

650 
val (assumes_propss, shows_propss) = chop (length raw_assumes) all_propss; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

651 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

652 
(*params*) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

653 
val (ps, params_ctxt) = fix_ctxt 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

654 
> (fold o fold) Variable.declare_term all_propss 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

655 
> fold Variable.bind_term binds 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

656 
> fold_map Proof_Context.inferred_param xs'; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

657 
val xs = map (Variable.check_name o #1) vars; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

658 
val params = xs ~~ map Free ps; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

659 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

660 
val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

661 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

662 
(*result term bindings*) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

663 
val shows_props = flat shows_propss; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

664 
val binds' = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

665 
(case try List.last shows_props of 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

666 
NONE => [] 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

667 
 SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

668 
val result_binds = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

669 
(Auto_Bind.facts params_ctxt shows_props @ binds') 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

670 
> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

671 
> export_binds params_ctxt ctxt; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

672 
in ((params, assumes_propss, shows_propss, result_binds), params_ctxt) end; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

673 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

674 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

675 
(* assume *) 
5820  676 

16813  677 
local 
678 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

679 
fun gen_assume prep_var prep_propp prep_att export raw_fixes raw_prems raw_concls state = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

680 
let 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

681 
val ctxt = context_of state; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

682 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

683 
val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

684 
val (params, prems_propss, concl_propss, result_binds) = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

685 
#1 (prep_clause prep_var prep_propp raw_fixes raw_prems (map snd raw_concls) ctxt); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

686 

4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

687 
fun close prop = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

688 
fold_rev Logic.all_name params (Logic.list_implies (flat prems_propss, prop)); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

689 
val propss = (map o map) close concl_propss; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

690 
in 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

691 
state 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

692 
> assert_forward 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

693 
> map_context_result (fn ctxt => 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

694 
ctxt 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

695 
> (fold o fold) Variable.declare_term propss 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

696 
> fold Variable.maybe_bind_term result_binds 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

697 
> fold_burrow (Assumption.add_assms export o map (Thm.cterm_of ctxt)) propss 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

698 
> (fn premss => 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

699 
Proof_Context.note_thmss "" (bindings ~~ (map o map) (fn th => ([th], [])) premss))) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

700 
> these_factss [] > #2 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

701 
end; 
6932  702 

16813  703 
in 
704 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

705 
val assm = gen_assume Proof_Context.cert_var Proof_Context.cert_propp (K I); 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

706 
val assm_cmd = gen_assume Proof_Context.read_var Proof_Context.read_propp Attrib.attribute_cmd; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

707 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

708 
val assume = assm Assumption.assume_export; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

709 
val assume_cmd = assm_cmd Assumption.assume_export; 
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

710 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

711 
val presume = assm Assumption.presume_export; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

712 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  713 

16813  714 
end; 
715 

7271  716 

17359  717 
(* def *) 
11891  718 

16813  719 
local 
720 

60379  721 
fun gen_def prep_att prep_var prep_binds args state = 
11891  722 
let 
723 
val _ = assert_forward state; 

20913  724 
val (raw_name_atts, (raw_vars, raw_rhss)) = args > split_list > split_list; 
47815  725 
val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts; 
11891  726 
in 
20913  727 
state 
60379  728 
> map_context_result (fold_map (fn (x, mx) => prep_var (x, NONE, mx)) raw_vars) 
20913  729 
>> map (fn (x, _, mx) => (x, mx)) 
730 
> (fn vars => 

731 
map_context_result (prep_binds false (map swap raw_rhss)) 

49748
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49063
diff
changeset

732 
#> (fn rhss => 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49063
diff
changeset

733 
let 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49063
diff
changeset

734 
val defs = (vars ~~ (name_atts ~~ rhss)) > map (fn ((x, mx), ((a, atts), rhs)) => 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49063
diff
changeset

735 
((x, mx), ((Thm.def_binding_optional x a, atts), rhs))); 
a346daa8a1f4
clarified Local_Defs.add_def(s): refrain from hardwiring Thm.def_binding_optional;
wenzelm
parents:
49063
diff
changeset

736 
in map_context_result (Local_Defs.add_defs defs) end)) 
47068  737 
> (set_facts o map (#2 o #2)) 
11891  738 
end; 
739 

16813  740 
in 
741 

60379  742 
val def = gen_def (K I) Proof_Context.cert_var Proof_Context.match_bind; 
743 
val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_var Proof_Context.match_bind_cmd; 

11891  744 

16813  745 
end; 
746 

11891  747 

8374  748 

17112  749 
(** facts **) 
5820  750 

17359  751 
(* chain *) 
5820  752 

24011  753 
fun clean_facts ctxt = 
47068  754 
set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt; 
24011  755 

17359  756 
val chain = 
757 
assert_forward 

24011  758 
#> clean_facts 
17359  759 
#> enter_chain; 
5820  760 

17359  761 
fun chain_facts facts = 
47068  762 
set_facts facts 
17359  763 
#> chain; 
5820  764 

765 

17359  766 
(* note etc. *) 
17112  767 

28965  768 
fun no_binding args = map (pair (Binding.empty, [])) args; 
17112  769 

770 
local 

771 

30760
0fffc66b10d7
simplified references to facts, eliminated external note_thmss;
wenzelm
parents:
30757
diff
changeset

772 
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state = 
17112  773 
state 
774 
> assert_forward 

47815  775 
> map_context_result (fn ctxt => ctxt > Proof_Context.note_thmss "" 
776 
(Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args)) 

17112  777 
> these_factss (more_facts state) 
17359  778 
> opt_chain 
779 
> opt_result; 

17112  780 

781 
in 

782 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

783 
val note_thmss = gen_thmss (K []) I #2 (K I) (K I); 
47815  784 
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact; 
17112  785 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

786 
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding; 
47815  787 
val from_thmss_cmd = 
788 
gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding; 

17359  789 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

790 
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding; 
47815  791 
val with_thmss_cmd = 
792 
gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding; 

30760
0fffc66b10d7
simplified references to facts, eliminated external note_thmss;
wenzelm
parents:
30757
diff
changeset

793 

0fffc66b10d7
simplified references to facts, eliminated external note_thmss;
wenzelm
parents:
30757
diff
changeset

794 
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact); 
17359  795 

17112  796 
end; 
797 

798 

60371  799 
(* facts during goal refinement *) 
800 

801 
local 

802 

803 
fun gen_supply prep_att prep_fact args state = 

804 
state 

805 
> assert_backward 

806 
> map_context (fn ctxt => ctxt > Proof_Context.note_thmss "" 

807 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) args) > snd); 

808 

809 
in 

810 

811 
val supply = gen_supply (K I) (K I); 

812 
val supply_cmd = gen_supply Attrib.attribute_cmd Proof_Context.get_fact; 

813 

814 
end; 

815 

816 

18548  817 
(* using/unfolding *) 
17112  818 

819 
local 

820 

45390
e29521ef9059
tuned signature  avoid spurious Thm.mixed_attribute;
wenzelm
parents:
45327
diff
changeset

821 
fun gen_using f g prep_att prep_fact args state = 
17112  822 
state 
823 
> assert_backward 

21442  824 
> map_context_result 
47815  825 
(fn ctxt => ctxt > Proof_Context.note_thmss "" 
826 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args))) 

18843  827 
> (fn (named_facts, state') => 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

828 
state' > map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) => 
18843  829 
let 
830 
val ctxt = context_of state'; 

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

831 
val ths = maps snd named_facts; 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

832 
in (goal_ctxt, statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end)); 
18548  833 

24050  834 
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 
35624  835 
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 
836 
val unfold_goals = Local_Defs.unfold_goals; 

17112  837 

838 
in 

839 

36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

840 
val using = gen_using append_using (K (K I)) (K I) (K I); 
47815  841 
val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact; 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

842 
val unfolding = gen_using unfold_using unfold_goals (K I) (K I); 
47815  843 
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact; 
17112  844 

845 
end; 

846 

847 

848 
(* case *) 

849 

850 
local 

851 

60565  852 
fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state = 
17112  853 
let 
60565  854 
val ctxt = context_of state; 
855 

856 
val binding = if Binding.is_empty raw_binding then Binding.make (name, pos) else raw_binding; 

857 
val atts = map (prep_att ctxt) raw_atts; 

858 

19078  859 
val (asms, state') = state > map_context_result (fn ctxt => 
57486
2131b6633529
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
wenzelm
parents:
56933
diff
changeset

860 
ctxt > Proof_Context.apply_case (Proof_Context.check_case ctxt internal (name, pos) xs)); 
53380
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
53378
diff
changeset

861 
val assumptions = 
60565  862 
asms > map (fn (a, ts) => ((Binding.qualified true a binding, []), map (rpair []) ts)); 
17112  863 
in 
864 
state' 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

865 
> assume [] [] assumptions 
60401  866 
> map_context (fold Variable.unbind_term Auto_Bind.no_facts) 
60565  867 
> `the_facts > (fn thms => note_thmss [((binding, atts), [(thms, [])])]) 
17112  868 
end; 
869 

870 
in 

871 

60565  872 
val case_ = gen_case true (K I); 
873 
val case_cmd = gen_case false Attrib.attribute_cmd; 

17112  874 

875 
end; 

876 

877 

878 

17359  879 
(** proof structure **) 
880 

881 
(* blocks *) 

882 

883 
val begin_block = 

884 
assert_forward 

885 
#> open_block 

47068  886 
#> reset_goal 
17359  887 
#> open_block; 
888 

889 
val next_block = 

890 
assert_forward 

891 
#> close_block 

892 
#> open_block 

47068  893 
#> reset_goal 
894 
#> reset_facts; 

17359  895 

896 
fun end_block state = 

897 
state 

898 
> assert_forward 

40960  899 
> assert_bottom false 
17359  900 
> close_block 
901 
> assert_current_goal false 

902 
> close_block 

903 
> export_facts state; 

904 

905 

40960  906 
(* global notepad *) 
907 

908 
val begin_notepad = 

909 
init 

910 
#> open_block 

911 
#> map_context (Variable.set_body true) 

912 
#> open_block; 

913 

914 
val end_notepad = 

915 
assert_forward 

916 
#> assert_bottom true 

917 
#> close_block 

918 
#> assert_current_goal false 

919 
#> close_block 

920 
#> context_of; 

921 

922 

17359  923 
(* subproofs *) 
924 

925 
fun proof opt_text = 

926 
assert_backward 

60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60611
diff
changeset

927 
#> refine (the_default Method.standard_text opt_text) 
60551  928 
#> Seq.map 
929 
(using_facts [] 

930 
#> enter_forward 

931 
#> open_block 

932 
#> reset_goal); 

17359  933 

49866  934 
fun proof_results arg = 
935 
Seq.APPEND (proof (Method.text arg) #> Seq.make_results, 

936 
method_error "initial" (Method.position arg)); 

49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49861
diff
changeset

937 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

938 
fun end_proof bot (prev_pos, (opt_text, immed)) = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

939 
let 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

940 
val (finish_text, terminal_pos, finished_pos) = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

941 
(case opt_text of 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

942 
NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos) 
55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
54993
diff
changeset

943 
 SOME (text, (pos, end_pos)) => (Method.finish_text (SOME text, immed), pos, end_pos)); 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

944 
in 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

945 
Seq.APPEND (fn state => 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

946 
state 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

947 
> assert_forward 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

948 
> assert_bottom bot 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

949 
> close_block 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

950 
> assert_current_goal true 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

951 
> using_facts [] 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

952 
> `before_qed > (refine o the_default Method.succeed_text) 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

953 
> Seq.maps (refine finish_text) 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

954 
> Seq.make_results, method_error "terminal" terminal_pos) 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

955 
#> Seq.maps_results (Seq.single o finished_goal finished_pos) 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

956 
end; 
17359  957 

29383  958 
fun check_result msg sq = 
959 
(case Seq.pull sq of 

960 
NONE => error msg 

961 
 SOME (s, _) => s); 

962 

17359  963 

964 
(* unstructured refinement *) 

965 

49865  966 
fun defer i = 
967 
assert_no_chain #> 

968 
refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd; 

969 

970 
fun prefer i = 

971 
assert_no_chain #> 

972 
refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd; 

17359  973 

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

49866  975 

17359  976 
fun apply_end text = assert_forward #> refine_end text; 
977 

55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
54993
diff
changeset

978 
fun apply_results (text, (pos, _)) = 
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
54993
diff
changeset

979 
Seq.APPEND (apply text #> Seq.make_results, method_error "" pos); 
49866  980 

55709
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
54993
diff
changeset

981 
fun apply_end_results (text, (pos, _)) = 
4e5a83a46ded
clarified Token.range_of in accordance to Symbol_Pos.range;
wenzelm
parents:
54993
diff
changeset

982 
Seq.APPEND (apply_end text #> Seq.make_results, method_error "" pos); 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49861
diff
changeset

983 

17359  984 

985 

17112  986 
(** goals **) 
987 

17359  988 
(* generic goals *) 
989 

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

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

991 

36322
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

992 
val is_var = 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

993 
can (dest_TVar o Logic.dest_type o Logic.dest_term) orf 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

994 
can (dest_Var o Logic.dest_term); 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

995 

81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

996 
fun implicit_vars props = 
19846  997 
let 
36354  998 
val (var_props, _) = take_prefix is_var props; 
36322
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

999 
val explicit_vars = fold Term.add_vars var_props []; 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

1000 
val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []); 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

1001 
in map (Logic.mk_term o Var) vars end; 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

1002 

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

1003 
fun refine_terms n = 
59953  1004 
refine (Method.Basic (fn ctxt => EMPTY_CASES o 
58002  1005 
K (HEADGOAL (PRECISE_CONJUNCTS n 
59498
50b60f501b05
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
wenzelm
parents:
59185
diff
changeset

1006 
(HEADGOAL (CONJUNCTS (ALLGOALS (resolve_tac ctxt [Drule.termI])))))))) 
19774
5fe7731d0836
allow nontrivial schematic goals (via embedded term vars);
wenzelm
parents:
19585
diff
changeset

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

1008 

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

1009 
in 
17359  1010 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1011 
fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state = 
5820  1012 
let 
17359  1013 
val chaining = can assert_chain state; 
25958  1014 
val pos = Position.thread_data (); 
17359  1015 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1016 
val goal_props = flat goal_propss; 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1017 
val vars = implicit_vars goal_props; 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1018 
val propss' = vars :: goal_propss; 
23418  1019 
val goal_propss = filter_out null propss'; 
60551  1020 

29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1021 
val goal = 
59616  1022 
Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) 
60406  1023 
> Thm.cterm_of goal_ctxt 
61508  1024 
> Thm.weaken_sorts' goal_ctxt; 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1025 
val statement = ((kind, pos), propss', Thm.term_of goal); 
60402  1026 

60383  1027 
val after_qed' = after_qed >> (fn after_local => fn results => 
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1028 
map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); 
5820  1029 
in 
60551  1030 
state 
1031 
> assert_forward_or_chain 

1032 
> enter_forward 

1033 
> open_block 

1034 
> enter_backward 

1035 
> map_context 

1036 
(K goal_ctxt 

1037 
#> init_context 

1038 
#> Variable.set_body true 

1039 
#> Proof_Context.auto_bind_goal goal_props) 

58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

1040 
> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed')) 
21565  1041 
> chaining ? (`the_facts #> using_facts) 
47068  1042 
> reset_facts 
23418  1043 
> not (null vars) ? refine_terms (length goal_propss) 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1044 
> null goal_props ? (refine (Method.Basic Method.assumption) #> Seq.hd) 
5820  1045 
end; 
1046 

60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1047 
fun generic_qed state = 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

1048 
let 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1049 
val (goal_ctxt, {statement = (_, propss, _), goal, after_qed, ...}) = 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1050 
current_goal state; 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1051 
val results = tl (conclude_goal goal_ctxt goal propss); 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1052 
in state > close_block > pair (after_qed, (goal_ctxt, results)) end; 
17359  1053 

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

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

1055 

9469  1056 

17359  1057 
(* local goals *) 
1058 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1059 
fun local_goal print_results prep_att prep_propp prep_var strict_asm 
60414  1060 
kind before_qed after_qed raw_fixes raw_assumes raw_shows state = 
17359  1061 
let 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1062 
val ctxt = context_of state; 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1063 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1064 
val add_assumes = 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1065 
Assumption.add_assms 
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1066 
(if strict_asm then Assumption.assume_export else Assumption.presume_export); 
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1067 

60414  1068 
val (assumes_bindings, shows_bindings) = 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1069 
apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows); 
17359  1070 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1071 
val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1072 
> prep_clause prep_var prep_propp raw_fixes (map snd raw_assumes) (map snd raw_shows); 
60406  1073 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1074 
val (that_fact, goal_ctxt) = params_ctxt 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1075 
> fold_burrow add_assumes ((map o map) (Thm.cterm_of params_ctxt) assumes_propss) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1076 
> (fn (premss, ctxt') => 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1077 
let 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1078 
val prems = Assumption.local_prems_of ctxt' ctxt; 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1079 
val ctxt'' = 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1080 
ctxt' 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1081 
> not (null assumes_propss) ? 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1082 
(snd o Proof_Context.note_thmss "" 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1083 
[((Binding.name Auto_Bind.thatN, []), [(prems, [])])]) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1084 
> (snd o Proof_Context.note_thmss "" 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1085 
(assumes_bindings ~~ map (map (fn th => ([th], []))) premss)) 
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1086 
in (prems, ctxt'') end); 
60402  1087 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1088 
fun after_qed' (result_ctxt, results) state' = state' 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1089 
> local_results (shows_bindings ~~ burrow (Proof_Context.export result_ctxt ctxt) results) 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1090 
> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1091 
> after_qed (result_ctxt, results); 
60461  1092 
in 
1093 
state 

61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

1094 
> generic_goal kind before_qed (after_qed', K I) goal_ctxt shows_propss result_binds 
60461  1095 
> pair that_fact 
1096 
end; 

5820  1097 

49866  1098 
fun local_qeds arg = 
1099 
end_proof false arg 

60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1100 
#> Seq.map_result (generic_qed #> (fn ((after_qed, _), results) => after_qed results)); 
5820  1101 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1102 
fun local_qed arg = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1103 
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
29383  1104 

5820  1105 

17359  1106 
(* global goals *) 
1107 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1108 
fun global_goal prep_propp before_qed after_qed propp ctxt = 
60402  1109 
let 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1110 
val (propss, binds) = 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1111 
prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp; 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1112 
val goal_ctxt = ctxt 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1113 
> (fold o fold) Variable.auto_fixes propss 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1114 
> fold Variable.bind_term binds; 
61109
1c98bfc5d743
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
wenzelm
parents:
60948
diff
changeset

1115 
fun after_qed' (result_ctxt, results) ctxt' = ctxt' 
1c98bfc5d743
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
wenzelm
parents:
60948
diff
changeset

1116 
> Proof_Context.restore_naming ctxt 
1c98bfc5d743
proper restore_naming after global qed, which is important to make Name_Space.transform_naming work properly, e.g. for "private typedef";
wenzelm
parents:
60948
diff
changeset

1117 
> after_qed (burrow (Proof_Context.export result_ctxt ctxt') results); 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1118 
in 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1119 
ctxt 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1120 
> init 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1121 
> generic_goal "" before_qed (K I, after_qed') goal_ctxt propss [] 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1122 
end; 
45327  1123 

60388  1124 
val theorem = global_goal Proof_Context.cert_propp; 
1125 
val theorem_cmd = global_goal Proof_Context.read_propp; 

12065  1126 

49866  1127 
fun global_qeds arg = 
1128 
end_proof true arg 

60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1129 
#> Seq.map_result (generic_qed #> (fn (((_, after_qed), results), state) => 
49859
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

1130 
after_qed results (context_of state))); 
17112  1131 

49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1132 
fun global_qed arg = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1133 
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
12959  1134 

5820  1135 

49907  1136 
(* terminal proof steps *) 
17112  1137 

49890
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1138 
local 
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1139 

49846
8fae089f5a0c
refined Proof.the_finished_goal with more informative error;
wenzelm
parents:
49748
diff
changeset

1140 
fun terminal_proof qeds initial terminal = 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1141 
proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal)) 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49861
diff
changeset

1142 
#> Seq.the_result ""; 
49848
f222a054342e
more informative error of initial/terminal proof steps;
wenzelm
parents:
49847
diff
changeset

1143 

49890
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1144 
in 
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1145 

29383  1146 
fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true); 
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60611
diff
changeset

1147 
val local_default_proof = local_terminal_proof ((Method.standard_text, Position.no_range), NONE); 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1148 
val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE); 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1149 
val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false); 
17112  1150 

29383  1151 
fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true); 
60618
4c79543cc376
renamed "default" to "standard", to make semantically clear what it is;
wenzelm
parents:
60611
diff
changeset

1152 
val global_default_proof = global_terminal_proof ((Method.standard_text, Position.no_range), NONE); 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1153 
val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE); 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

1154 
val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false); 
5820  1155 

49890
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1156 
end; 
89eff795f757
skipped proofs appear as "bad" without counting as error;
wenzelm
parents:
49889
diff
changeset

1157 

6896  1158 

49907  1159 
(* skip proofs *) 
1160 

1161 
fun local_skip_proof int state = 

1162 
local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before 

51551  1163 
Skip_Proof.report (context_of state); 
49907  1164 

1165 
fun global_skip_proof int state = 

1166 
global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before 

51551  1167 
Skip_Proof.report (context_of state); 
49907  1168 

1169 

17359  1170 
(* common goal statements *) 
1171 

60406  1172 
fun internal_goal print_results mode = 
1173 
local_goal print_results (K I) (Proof_Context.cert_propp o Proof_Context.set_mode mode) 

1174 
Proof_Context.cert_var; 

1175 

17359  1176 
local 
1177 

60406  1178 
fun gen_have prep_att prep_propp prep_var 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1179 
strict_asm before_qed after_qed fixes assumes shows int = 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56912
diff
changeset

1180 
local_goal (Proof_Display.print_results int (Position.thread_data ())) 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1181 
prep_att prep_propp prep_var strict_asm "have" before_qed after_qed fixes assumes shows; 
6896  1182 

60406  1183 
fun gen_show prep_att prep_propp prep_var 
60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1184 
strict_asm before_qed after_qed fixes assumes shows int state = 
17359  1185 
let 
32738  1186 
val testing = Unsynchronized.ref false; 
1187 
val rule = Unsynchronized.ref (NONE: thm option); 

17359  1188 
fun fail_msg ctxt = 
50315
cf9002ac1018
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
wenzelm
parents:
50201
diff
changeset

1189 
"Local statement fails to refine any pending goal" :: 
33389  1190 
(case ! rule of NONE => []  SOME th => [Proof_Display.string_of_rule ctxt "Failed" th]) 
17359  1191 
> cat_lines; 
6896  1192 

56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56912
diff
changeset

1193 
val pos = Position.thread_data (); 
17359  1194 
fun print_results ctxt res = 
46728
85f8e3932712
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents:
46466
diff
changeset

1195 
if ! testing then () 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56912
diff
changeset

1196 
else Proof_Display.print_results int pos ctxt res; 
17359  1197 
fun print_rule ctxt th = 
1198 
if ! testing then rule := SOME th 

41181
9240be8c8c69
show: display goal refinement rule as "state", to avoid odd Output.urgent_message and make its association with the goal more explicit;
wenzelm
parents:
40960
diff
changeset

1199 
else if int then 
56933  1200 
Proof_Display.string_of_rule ctxt "Successful" th 
1201 
> Markup.markup Markup.text_fold 

59184
830bb7ddb3ab
explicit message channels for "state", "information";
wenzelm
parents:
59150
diff
changeset

1202 
> Output.state 
17359  1203 
else (); 
1204 
val test_proof = 

50315
cf9002ac1018
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
wenzelm
parents:
50201
diff
changeset

1205 
local_skip_proof true 
39616
8052101883c3
renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
wenzelm
parents:
39232
diff
changeset

1206 
> Unsynchronized.setmp testing true 
42042  1207 
> Exn.interruptible_capture; 
6896  1208 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1209 
fun after_qed' (result_ctxt, results) state' = state' 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1210 
> refine_goals print_rule result_ctxt (flat results) 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1211 
> check_result "Failed to refine any pending goal" 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1212 
> after_qed (result_ctxt, results); 
17359  1213 
in 
1214 
state 

60555
51a6997b1384
support 'when' statement, which corresponds to 'presume';
wenzelm
parents:
60551
diff
changeset

1215 
> local_goal print_results prep_att prep_propp prep_var strict_asm 
60414  1216 
"show" before_qed after_qed' fixes assumes shows 
60461  1217 
> int ? (fn goal_state => 
49907  1218 
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of 
50315
cf9002ac1018
recovered error to finish proof (e.g. bad obtain export) from 223f18cfbb32;
wenzelm
parents:
50201
diff
changeset

1219 
Exn.Res _ => goal_state 
42042  1220 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1221 
end; 
1222 

1223 
in 

1224 

60406  1225 
val have = gen_have (K I) Proof_Context.cert_propp Proof_Context.cert_var; 
1226 
val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var; 

1227 
val show = gen_show (K I) Proof_Context.cert_propp Proof_Context.cert_var; 

1228 
val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.read_propp Proof_Context.read_var; 

6896  1229 

5820  1230 
end; 
17359  1231 

28410  1232 

29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1233 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1234 
(** future proofs **) 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1235 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1236 
(* relevant proof states *) 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1237 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1238 
fun schematic_goal state = 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

1239 
let val (_, {statement = (_, _, prop), ...}) = find_goal state 
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51551
diff
changeset

1240 
in Goal.is_schematic prop end; 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1241 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1242 
fun is_relevant state = 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1243 
(case try find_goal state of 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1244 
NONE => true 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

1245 
 SOME (_, {statement = (_, _, prop), goal, ...}) => 
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51551
diff
changeset

1246 
Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal)); 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1247 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1248 

c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1249 
(* full proofs *) 
28410  1250 

29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1251 
local 
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1252 

49912
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1253 
structure Result = Proof_Data 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1254 
( 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1255 
type T = thm option; 
59150  1256 
fun init _ = NONE; 
49912
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1257 
); 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1258 

c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1259 
fun the_result ctxt = 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1260 
(case Result.get ctxt of 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1261 
NONE => error "No result of forked proof" 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1262 
 SOME th => th); 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1263 

c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1264 
val set_result = Result.put o SOME; 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1265 
val reset_result = Result.put NONE; 
c6307ee2665d
more robust future_proof result with specific error message (e.g. relevant for incomplete proof of nonregistered theorem);
wenzelm
parents:
49909
diff
changeset

1266 

51318  1267 
in 
1268 

1269 
fun future_proof fork_proof state = 

28410  1270 
let 
29381
45d77aeb1608
future_terminal_proof: no fork for interactive mode, assert_backward;
wenzelm
parents:
29364
diff
changeset

1271 
val _ = assert_backward state; 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

1272 
val (goal_ctxt, goal_info) = find_goal state; 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1273 
val {statement as (kind, _, prop), using, goal, before_qed, after_qed} = goal_info; 
28410  1274 

29383  1275 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1276 

60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1277 
val after_qed' = 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1278 
(fn (_, [[th]]) => map_context (set_result th), 
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

1279 
fn (_, [[th]]) => set_result th); 