author  wenzelm 
Wed, 16 Jan 2013 18:43:59 +0100  
changeset 50912  8d391f185cac 
parent 50885  f3588e59aeaa 
child 51048  123be08eed88 
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 
30757
2d2076300185
replaced add_binds(_i) by bind_terms  internal version only;
wenzelm
parents:
30557
diff
changeset

22 
val bind_terms: (indexname * term option) list > state > state 
26251
b8c6259d366b
put_facts: do_props, i.e. facts are indexed by proposition again;
wenzelm
parents:
25958
diff
changeset

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

6891  28 
val assert_forward: state > state 
17359  29 
val assert_chain: state > state 
9469  30 
val assert_forward_or_chain: state > state 
5820  31 
val assert_backward: state > state 
8206  32 
val assert_no_chain: state > state 
5820  33 
val enter_forward: state > state 
24543  34 
val goal_message: (unit > Pretty.T) > state > state 
12423  35 
val pretty_state: int > state > Pretty.T list 
17112  36 
val refine: Method.text > state > state Seq.seq 
37 
val refine_end: Method.text > state > state Seq.seq 

18908  38 
val refine_insert: thm list > state > state 
17359  39 
val refine_goals: (context > thm > unit) > context > thm list > state > state Seq.seq 
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

40 
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

41 
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

42 
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

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

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

45 
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

46 
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

47 
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

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

49 
val fix_cmd: (binding * string option * mixfix) list > state > state 
20224
9c40a144ee0e
moved basic assumption operations from structure ProofContext to Assumption;
wenzelm
parents:
20208
diff
changeset

50 
val assm: Assumption.export > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

52 
val assm_cmd: Assumption.export > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

53 
(Attrib.binding * (string * string list) list) list > state > state 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

55 
val assume_cmd: (Attrib.binding * (string * string list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

57 
val presume_cmd: (Attrib.binding * (string * string list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

58 
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

59 
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list > state > state 
17359  60 
val chain: state > state 
61 
val chain_facts: thm list > state > state 

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

62 
val note_thmss: (Thm.binding * (thm list * attribute list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

64 
val from_thmss: ((thm list * attribute list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

66 
val with_thmss: ((thm list * attribute list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

68 
val using: ((thm list * attribute list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

70 
val unfolding: ((thm list * attribute list) list) list > state > state 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

71 
val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list > state > state 
42496  72 
val invoke_case: string * binding option list * attribute list > state > state 
73 
val invoke_case_cmd: string * binding option list * Attrib.src list > state > state 

17359  74 
val begin_block: state > state 
75 
val next_block: state > state 

20309  76 
val end_block: state > state 
49042  77 
val begin_notepad: context > state 
78 
val end_notepad: state > context 

17112  79 
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

80 
val proof_results: Method.text_range option > state > state Seq.result Seq.seq 
49865  81 
val defer: int > state > state 
82 
val prefer: int > state > state 

17112  83 
val apply: Method.text > state > state Seq.seq 
84 
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

85 
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

86 
val apply_end_results: Method.text_range > state > state Seq.result Seq.seq 
17359  87 
val local_goal: (context > ((string * string) * (string * thm list) list) > unit) > 
49042  88 
(context > 'a > attribute) > 
45327  89 
('b list > context > (term list list * (context > context)) * context) > 
29383  90 
string > Method.text option > (thm list list > state > state) > 
29581  91 
((binding * 'a list) * 'b) list > state > state 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

92 
val local_qed: Method.text_range option * bool > state > state 
21442  93 
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

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

95 
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

96 
(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

97 
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

98 
val local_terminal_proof: Method.text_range * Method.text_range option > state > state 
29383  99 
val local_default_proof: state > state 
100 
val local_immediate_proof: state > state 

101 
val local_skip_proof: bool > state > state 

102 
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

103 
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

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

105 
val global_immediate_proof: state > context 
29383  106 
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

107 
val global_done_proof: state > context 
29383  108 
val have: Method.text option > (thm list list > state > state) > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

110 
val have_cmd: Method.text option > (thm list list > state > state) > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

111 
(Attrib.binding * (string * string list) list) list > bool > state > state 
29383  112 
val show: Method.text option > (thm list list > state > state) > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

114 
val show_cmd: Method.text option > (thm list list > state > state) > 
28084
a05ca48ef263
type Attrib.binding abbreviates Name.binding without attributes;
wenzelm
parents:
28083
diff
changeset

115 
(Attrib.binding * (string * string list) list) list > bool > state > state 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

116 
val schematic_goal: state > bool 
47416  117 
val local_future_proof: (state > ('a * state) future) > state > 'a future * state 
49042  118 
val global_future_proof: (state > ('a * context) future) > state > 'a future * context 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

119 
val local_future_terminal_proof: Method.text_range * Method.text_range option > bool > 
49866  120 
state > state 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

121 
val global_future_terminal_proof: Method.text_range * Method.text_range option > bool > 
49866  122 
state > context 
5820  123 
end; 
124 

13377  125 
structure Proof: PROOF = 
5820  126 
struct 
127 

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

128 
type context = Proof.context; 
17112  129 
type method = Method.method; 
16813  130 

5820  131 

132 
(** proof state **) 

133 

17359  134 
(* datatype state *) 
5820  135 

17112  136 
datatype mode = Forward  Chain  Backward; 
5820  137 

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

140 
and node = 

7176  141 
Node of 
142 
{context: context, 

143 
facts: thm list option, 

144 
mode: mode, 

17359  145 
goal: goal option} 
146 
and goal = 

147 
Goal of 

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

148 
{statement: (string * Position.T) * term list list * term, 
28410  149 
(*goal kind and statement (starting with vars), initial proposition*) 
25958  150 
messages: (unit > Pretty.T) list, (*persistent messages (hints etc.)*) 
151 
using: thm list, (*goal facts*) 

152 
goal: thm, (*subgoals ==> statement*) 

17859  153 
before_qed: Method.text option, 
18124  154 
after_qed: 
29383  155 
(thm list list > state > state) * 
20363
f34c5dbe74d5
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
wenzelm
parents:
20341
diff
changeset

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

24543  158 
fun make_goal (statement, messages, using, goal, before_qed, after_qed) = 
159 
Goal {statement = statement, messages = messages, using = using, goal = goal, 

17859  160 
before_qed = before_qed, after_qed = after_qed}; 
5820  161 

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

164 

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

5820  167 

21727  168 
val init_context = 
42360  169 
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

170 
Proof_Context.map_naming (K Name_Space.local_naming); 
21727  171 

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

172 
fun init ctxt = 
21727  173 
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); 
5820  174 

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

175 
fun top (State st) = Stack.top st > (fn Node node => node); 
9c68e43502ce
some support for registering forked proofs within Proof.state, using its bottom context;
wenzelm
parents:
47815
diff
changeset

176 
fun map_top f (State st) = State (Stack.map_top (map_node f) st); 
28278  177 
fun map_all f (State st) = State (Stack.map_all (map_node f) st); 
12045  178 

5820  179 

180 

181 
(** basic proof state operations **) 

182 

17359  183 
(* block structure *) 
184 

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

186 

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

188 
handle List.Empty => error "Unbalanced block parentheses"; 
17359  189 

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

191 

192 
fun assert_bottom b state = 

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

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

17359  196 
else state 
197 
end; 

198 

199 

5820  200 
(* context *) 
201 

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

202 
val context_of = #context o top; 
42360  203 
val theory_of = Proof_Context.theory_of o context_of; 
5820  204 

47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

205 
fun map_node_context f = 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

206 
map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

207 

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

209 
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
5820  210 

17359  211 
fun map_context_result f state = 
17859  212 
f (context_of state) > (fn ctxt => map_context (K ctxt) state); 
5820  213 

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

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

216 
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

217 
(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

218 

42360  219 
val bind_terms = map_context o Proof_Context.bind_terms; 
220 
val put_thms = map_context oo Proof_Context.put_thms; 

5820  221 

222 

223 
(* facts *) 

224 

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

225 
val get_facts = #facts o top; 
17359  226 

227 
fun the_facts state = 

228 
(case get_facts state of SOME facts => facts 

18678  229 
 NONE => error "No current facts available"); 
5820  230 

9469  231 
fun the_fact state = 
17359  232 
(case the_facts state of [thm] => thm 
18678  233 
 _ => error "Single theorem expected"); 
7605  234 

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

236 
map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> 
33386  237 
put_thms true (Auto_Bind.thisN, facts); 
5820  238 

47068  239 
val set_facts = put_facts o SOME; 
240 
val reset_facts = put_facts NONE; 

241 

17359  242 
fun these_factss more_facts (named_factss, state) = 
47068  243 
(named_factss, state > set_facts (maps snd named_factss @ more_facts)); 
5820  244 

17359  245 
fun export_facts inner outer = 
246 
(case get_facts inner of 

47068  247 
NONE => reset_facts outer 
17359  248 
 SOME thms => 
249 
thms 

42360  250 
> Proof_Context.export (context_of inner) (context_of outer) 
47068  251 
> (fn ths => set_facts ths outer)); 
5820  252 

253 

254 
(* mode *) 

255 

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

256 
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

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

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

261 
fun assert_mode pred state = 

262 
let val mode = get_mode state in 

263 
if pred mode then state 

18678  264 
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode") 
5820  265 
end; 
266 

19308  267 
val assert_forward = assert_mode (fn mode => mode = Forward); 
268 
val assert_chain = assert_mode (fn mode => mode = Chain); 

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

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

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

5820  272 

17359  273 
val enter_forward = put_mode Forward; 
274 
val enter_chain = put_mode Chain; 

275 
val enter_backward = put_mode Backward; 

5820  276 

17359  277 

278 
(* current goal *) 

279 

280 
fun current_goal state = 

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

281 
(case top state of 
17359  282 
{context, goal = SOME (Goal goal), ...} => (context, goal) 
47065  283 
 _ => error "No current goal"); 
5820  284 

17359  285 
fun assert_current_goal g state = 
286 
let val g' = can current_goal state in 

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

17359  289 
else state 
290 
end; 

6776  291 

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

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

47068  294 
val set_goal = put_goal o SOME; 
295 
val reset_goal = put_goal NONE; 

296 

17859  297 
val before_qed = #before_qed o #2 o current_goal; 
298 

17359  299 

300 
(* nested goal *) 

5820  301 

47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

302 
fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = 
17359  303 
let 
24543  304 
val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; 
305 
val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed)); 

47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

306 
val node' = map_node_context h node; 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

307 
in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

308 
 map_goal f g h (State (nd, node :: nodes)) = 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

309 
let 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

310 
val nd' = map_node_context f nd; 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

311 
val State (node', nodes') = map_goal f g h (State (node, nodes)); 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

312 
in State (nd', node' :: nodes') end 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

313 
 map_goal _ _ _ state = state; 
5820  314 

47068  315 
fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) => 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

316 
(statement, [], using, goal, before_qed, after_qed)) I; 
19188  317 

24543  318 
fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) => 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

319 
(statement, msg :: messages, using, goal, before_qed, after_qed)) I; 
24543  320 

24556  321 
fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) => 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

322 
(statement, [], using, goal, before_qed, after_qed)) I; 
17359  323 

324 
local 

325 
fun find i state = 

326 
(case try current_goal state of 

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

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

331 
fun get_goal state = 

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

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

5820  334 

335 

336 

12423  337 
(** pretty_state **) 
5820  338 

15531  339 
fun pretty_facts _ _ NONE = [] 
340 
 pretty_facts s ctxt (SOME ths) = 

49867  341 
[(Pretty.block o Pretty.fbreaks) 
49909  342 
((if s = "" then Pretty.str "this:" 
343 
else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) :: 

344 
map (Display.pretty_thm ctxt) ths), 

345 
Pretty.str ""]; 

6756  346 

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

349 
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

350 
val verbose = Config.get ctxt Proof_Context.verbose; 
5820  351 

49860  352 
fun prt_goal (SOME (_, (_, 
29416  353 
{statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) = 
49909  354 
pretty_facts "using" ctxt 
17359  355 
(if mode <> Backward orelse null using then NONE else SOME using) @ 
49860  356 
[Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @ 
25958  357 
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) 
17359  358 
 prt_goal NONE = []; 
6848  359 

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

361 
if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt 
42360  362 
else if mode = Backward then Proof_Context.pretty_ctxt ctxt 
7575  363 
else []; 
17359  364 
in 
365 
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ 

42717
0bbb56867091
proper configuration options Proof_Context.debug and Proof_Context.verbose;
wenzelm
parents:
42496
diff
changeset

366 
(if verbose then ", depth " ^ string_of_int (level state div 2  1) else "")), 
17359  367 
Pretty.str ""] @ 
368 
(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

369 
(if verbose orelse mode = Forward then 
39051
45facd8f358e
Proof.pretty_state: print everything in the foreground context to give users a chance to configure options, e.g. via "using [[show_consts]]";
wenzelm
parents:
38721
diff
changeset

370 
pretty_facts "" ctxt facts @ prt_goal (try find_goal state) 
49909  371 
else if mode = Chain then pretty_facts "picking" ctxt facts 
17359  372 
else prt_goal (try find_goal state)) 
373 
end; 

5820  374 

375 

376 

377 
(** proof steps **) 

378 

17359  379 
(* refine via method *) 
5820  380 

8234  381 
local 
382 

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

385 

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

387 

388 
fun goal_cases st = 

47815  389 
Rule_Cases.make_common 
390 
(Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st)); 

16146  391 

32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

392 
fun apply_method current_context meth state = 
6848  393 
let 
24556  394 
val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = 
24543  395 
find_goal state; 
25958  396 
val ctxt = if current_context then context_of state else goal_ctxt; 
16146  397 
in 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

398 
Method.apply meth ctxt using goal > Seq.map (fn (meth_cases, goal') => 
6848  399 
state 
16146  400 
> map_goal 
42360  401 
(Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #> 
402 
Proof_Context.add_cases true meth_cases) 

47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

403 
(K (statement, [], using, goal', before_qed, after_qed)) I) 
16146  404 
end; 
5820  405 

19188  406 
fun select_goals n meth state = 
19224  407 
state 
408 
> (#2 o #2 o get_goal) 

21687  409 
> ALLGOALS Goal.conjunction_tac 
19224  410 
> Seq.maps (fn goal => 
19188  411 
state 
47068  412 
> Seq.lift provide_goal (Goal.extract 1 n goal > Seq.maps (Goal.conjunction_tac 1)) 
19188  413 
> Seq.maps meth 
414 
> Seq.maps (fn state' => state' 

47068  415 
> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal)) 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

416 
> Seq.maps (apply_method true (K Method.succeed))); 
19188  417 

17112  418 
fun apply_text cc text state = 
419 
let 

420 
val thy = theory_of state; 

421 

32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

422 
fun eval (Method.Basic m) = apply_method cc m 
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

423 
 eval (Method.Source src) = apply_method cc (Method.method thy src) 
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

424 
 eval (Method.Source_i src) = apply_method cc (Method.method_i thy src) 
17112  425 
 eval (Method.Then txts) = Seq.EVERY (map eval txts) 
426 
 eval (Method.Orelse txts) = Seq.FIRST (map eval txts) 

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

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

17112  430 
in eval text state end; 
431 

8234  432 
in 
433 

17112  434 
val refine = apply_text true; 
435 
val refine_end = apply_text false; 

32856
92d9555ac790
clarified Proof.refine_insert  always "refine" to apply standard method treatment (of conjunctions);
wenzelm
parents:
32786
diff
changeset

436 
fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths))); 
18908  437 

8234  438 
end; 
439 

5820  440 

17359  441 
(* refine via subproof *) 
442 

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

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

444 

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

445 
fun finish_tac 0 = K all_tac 
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

446 
 finish_tac n = 
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

447 
Goal.norm_hhf_tac THEN' 
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

448 
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

449 
if can Logic.unprotect (Logic.strip_assums_concl goal) then 
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

450 
Tactic.etac Drule.protectI i THEN finish_tac (n  1) 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

451 
else finish_tac (n  1) (i + 1)); 
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

452 

20208  453 
fun goal_tac rule = 
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

454 
Goal.norm_hhf_tac THEN' 
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

455 
Tactic.rtac rule THEN' 
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

456 
finish_tac (Thm.nprems_of rule); 
11816  457 

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

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

459 
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

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

461 

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

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

463 

19915  464 
fun refine_goals print_rule inner raw_rules state = 
465 
let 

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

20208  467 
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st); 
19915  468 
in 
469 
raw_rules 

42360  470 
> Proof_Context.goal_export inner outer 
47068  471 
> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state) 
19915  472 
end; 
17359  473 

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

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

475 

6932  476 

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

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

478 

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

479 
fun conclude_goal ctxt goal propss = 
5820  480 
let 
42360  481 
val thy = Proof_Context.theory_of ctxt; 
24920  482 
val string_of_term = Syntax.string_of_term ctxt; 
32091
30e2ffbba718
proper context for Display.pretty_thm etc. or oldstyle versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
wenzelm
parents:
32089
diff
changeset

483 
val string_of_thm = Display.string_of_thm ctxt; 
5820  484 

49860  485 
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

486 

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

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

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

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

23418  491 
fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal); 
492 

23782
4dd0ba632e40
Proof terms for metaconjunctions are now normalized before
berghofe
parents:
23639
diff
changeset

493 
val th = Goal.conclude 
23806  494 
(if length (flat propss) > 1 then Thm.norm_proof goal else goal) 
23782
4dd0ba632e40
Proof terms for metaconjunctions are now normalized before
berghofe
parents:
23639
diff
changeset

495 
handle THM _ => lost_structure (); 
23418  496 
val goal_propss = filter_out null propss; 
497 
val results = 

498 
Conjunction.elim_balanced (length goal_propss) th 

499 
> map2 Conjunction.elim_balanced (map length goal_propss) 

500 
handle THM _ => lost_structure (); 

501 
val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse 

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

502 
error ("Proved a different theorem:\n" ^ string_of_thm th); 
28627
63663cfa297c
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28458
diff
changeset

503 
val _ = Thm.check_shyps (Variable.sorts_of ctxt) th; 
23418  504 

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

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

507 
 recover_result [] [] = [] 

508 
 recover_result _ _ = lost_structure (); 

509 
in recover_result propss results end; 

5820  510 

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

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

512 

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

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

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

515 
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

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

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

518 
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

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

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

521 

5820  522 

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

523 
(* 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

524 

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

525 
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

526 
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

527 
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

528 

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

529 
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

530 

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

531 
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

532 
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

533 
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

534 
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

535 
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

536 

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

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

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

539 
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

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

541 

49866  542 
fun method_error kind pos state = 
543 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  544 

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

545 

5820  546 

547 
(*** structured proof commands ***) 

548 

17112  549 
(** context elements **) 
5820  550 

36324  551 
(* let bindings *) 
5820  552 

16813  553 
local 
554 

17359  555 
fun gen_bind bind args state = 
5820  556 
state 
557 
> assert_forward 

36324  558 
> map_context (bind true args #> snd) 
47068  559 
> reset_facts; 
5820  560 

16813  561 
in 
562 

42360  563 
val let_bind = gen_bind Proof_Context.match_bind_i; 
564 
val let_bind_cmd = gen_bind Proof_Context.match_bind; 

5820  565 

16813  566 
end; 
567 

5820  568 

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

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

570 

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

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

572 

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

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

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

577 

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

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

579 

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

580 
val write = gen_write (K I); 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

581 

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

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

583 
gen_write (fn ctxt => fn (c, mx) => 
42360  584 
(Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx)); 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

585 

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

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

587 

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

588 

17359  589 
(* fix *) 
9196  590 

12714  591 
local 
592 

30763
6976521b4263
renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;
wenzelm
parents:
30761
diff
changeset

593 
fun gen_fix prep_vars args = 
17359  594 
assert_forward 
45597  595 
#> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt)) 
47068  596 
#> reset_facts; 
5820  597 

16813  598 
in 
599 

45597  600 
val fix = gen_fix Proof_Context.cert_vars; 
601 
val fix_cmd = gen_fix Proof_Context.read_vars; 

5820  602 

16813  603 
end; 
604 

5820  605 

17359  606 
(* assume etc. *) 
5820  607 

16813  608 
local 
609 

17112  610 
fun gen_assume asm prep_att exp args state = 
5820  611 
state 
612 
> assert_forward 

47815  613 
> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args)) 
17359  614 
> these_factss [] > #2; 
6932  615 

16813  616 
in 
617 

42360  618 
val assm = gen_assume Proof_Context.add_assms_i (K I); 
47815  619 
val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd; 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

621 
val assume_cmd = assm_cmd Assumption.assume_export; 
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

623 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  624 

16813  625 
end; 
626 

7271  627 

17359  628 
(* def *) 
11891  629 

16813  630 
local 
631 

20913  632 
fun gen_def prep_att prep_vars prep_binds args state = 
11891  633 
let 
634 
val _ = assert_forward state; 

20913  635 
val (raw_name_atts, (raw_vars, raw_rhss)) = args > split_list > split_list; 
47815  636 
val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts; 
11891  637 
in 
20913  638 
state 
639 
> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars)) 

640 
>> map (fn (x, _, mx) => (x, mx)) 

641 
> (fn vars => 

642 
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

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

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

645 
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

646 
((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

647 
in map_context_result (Local_Defs.add_defs defs) end)) 
47068  648 
> (set_facts o map (#2 o #2)) 
11891  649 
end; 
650 

16813  651 
in 
652 

42360  653 
val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i; 
47815  654 
val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind; 
11891  655 

16813  656 
end; 
657 

11891  658 

8374  659 

17112  660 
(** facts **) 
5820  661 

17359  662 
(* chain *) 
5820  663 

24011  664 
fun clean_facts ctxt = 
47068  665 
set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt; 
24011  666 

17359  667 
val chain = 
668 
assert_forward 

24011  669 
#> clean_facts 
17359  670 
#> enter_chain; 
5820  671 

17359  672 
fun chain_facts facts = 
47068  673 
set_facts facts 
17359  674 
#> chain; 
5820  675 

676 

17359  677 
(* note etc. *) 
17112  678 

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

681 
local 

682 

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

683 
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state = 
17112  684 
state 
685 
> assert_forward 

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

17112  688 
> these_factss (more_facts state) 
17359  689 
> opt_chain 
690 
> opt_result; 

17112  691 

692 
in 

693 

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

694 
val note_thmss = gen_thmss (K []) I #2 (K I) (K I); 
47815  695 
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact; 
17112  696 

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

697 
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding; 
47815  698 
val from_thmss_cmd = 
699 
gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding; 

17359  700 

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

701 
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding; 
47815  702 
val with_thmss_cmd = 
703 
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

704 

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

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

17112  707 
end; 
708 

709 

18548  710 
(* using/unfolding *) 
17112  711 

712 
local 

713 

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

714 
fun gen_using f g prep_att prep_fact args state = 
17112  715 
state 
716 
> assert_backward 

21442  717 
> map_context_result 
47815  718 
(fn ctxt => ctxt > Proof_Context.note_thmss "" 
719 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args))) 

18843  720 
> (fn (named_facts, state') => 
24556  721 
state' > map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => 
18843  722 
let 
723 
val ctxt = context_of state'; 

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

724 
val ths = maps snd named_facts; 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

725 
in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); 
18548  726 

24050  727 
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 
35624  728 
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 
729 
val unfold_goals = Local_Defs.unfold_goals; 

17112  730 

731 
in 

732 

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

733 
val using = gen_using append_using (K (K I)) (K I) (K I); 
47815  734 
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

735 
val unfolding = gen_using unfold_using unfold_goals (K I) (K I); 
47815  736 
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact; 
17112  737 

738 
end; 

739 

740 

741 
(* case *) 

742 

743 
local 

744 

30419
c944e299eaf9
invoke_case: proper qualification of name binding, avoiding old no_base_names;
wenzelm
parents:
30279
diff
changeset

745 
fun qualified_binding a = 
c944e299eaf9
invoke_case: proper qualification of name binding, avoiding old no_base_names;
wenzelm
parents:
30279
diff
changeset

746 
Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a)); 
c944e299eaf9
invoke_case: proper qualification of name binding, avoiding old no_base_names;
wenzelm
parents:
30279
diff
changeset

747 

17112  748 
fun gen_invoke_case prep_att (name, xs, raw_atts) state = 
749 
let 

47815  750 
val atts = map (prep_att (context_of state)) raw_atts; 
19078  751 
val (asms, state') = state > map_context_result (fn ctxt => 
42360  752 
ctxt > Proof_Context.apply_case (Proof_Context.get_case ctxt name xs)); 
30419
c944e299eaf9
invoke_case: proper qualification of name binding, avoiding old no_base_names;
wenzelm
parents:
30279
diff
changeset

753 
val assumptions = asms > map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts)); 
17112  754 
in 
755 
state' 

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

756 
> assume assumptions 
33386  757 
> bind_terms Auto_Bind.no_facts 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

758 
> `the_facts > (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])]) 
17112  759 
end; 
760 

761 
in 

762 

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

763 
val invoke_case = gen_invoke_case (K I); 
47815  764 
val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd; 
17112  765 

766 
end; 

767 

768 

769 

17359  770 
(** proof structure **) 
771 

772 
(* blocks *) 

773 

774 
val begin_block = 

775 
assert_forward 

776 
#> open_block 

47068  777 
#> reset_goal 
17359  778 
#> open_block; 
779 

780 
val next_block = 

781 
assert_forward 

782 
#> close_block 

783 
#> open_block 

47068  784 
#> reset_goal 
785 
#> reset_facts; 

17359  786 

787 
fun end_block state = 

788 
state 

789 
> assert_forward 

40960  790 
> assert_bottom false 
17359  791 
> close_block 
792 
> assert_current_goal false 

793 
> close_block 

794 
> export_facts state; 

795 

796 

40960  797 
(* global notepad *) 
798 

799 
val begin_notepad = 

800 
init 

801 
#> open_block 

802 
#> map_context (Variable.set_body true) 

803 
#> open_block; 

804 

805 
val end_notepad = 

806 
assert_forward 

807 
#> assert_bottom true 

808 
#> close_block 

809 
#> assert_current_goal false 

810 
#> close_block 

811 
#> context_of; 

812 

813 

17359  814 
(* subproofs *) 
815 

816 
fun proof opt_text = 

817 
assert_backward 

17859  818 
#> refine (the_default Method.default_text opt_text) 
17359  819 
#> Seq.map (using_facts [] #> enter_forward); 
820 

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

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

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

824 

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

825 
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

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

827 
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

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

829 
NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos) 
50912  830 
 SOME (text, (pos, end_pos)) => 
831 
(Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos)); 

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

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

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

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

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

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

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

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

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

840 
> `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

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

842 
> 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

843 
#> 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

844 
end; 
17359  845 

29383  846 
fun check_result msg sq = 
847 
(case Seq.pull sq of 

848 
NONE => error msg 

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

850 

17359  851 

852 
(* unstructured refinement *) 

853 

49865  854 
fun defer i = 
855 
assert_no_chain #> 

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

857 

858 
fun prefer i = 

859 
assert_no_chain #> 

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

17359  861 

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

49866  863 

17359  864 
fun apply_end text = assert_forward #> refine_end text; 
865 

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

866 
fun apply_results (text, range) = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

867 
Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range)); 
49866  868 

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

869 
fun apply_end_results (text, range) = 
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

871 

17359  872 

873 

17112  874 
(** goals **) 
875 

17359  876 
(* generic goals *) 
877 

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

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

879 

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

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

881 
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

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

883 

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

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

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

888 
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

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

890 

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

891 
fun refine_terms n = 
30510
4120fc59dd85
unified type Proof.method and pervasive METHOD combinators;
wenzelm
parents:
30419
diff
changeset

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

893 
(K (HEADGOAL (PRECISE_CONJUNCTS n 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

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

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

896 

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

897 
in 
17359  898 

17859  899 
fun generic_goal prepp kind before_qed after_qed raw_propp state = 
5820  900 
let 
17359  901 
val thy = theory_of state; 
23418  902 
val cert = Thm.cterm_of thy; 
17359  903 
val chaining = can assert_chain state; 
25958  904 
val pos = Position.thread_data (); 
17359  905 

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

5936  907 
state 
908 
> assert_forward_or_chain 

909 
> enter_forward 

17359  910 
> open_block 
45327  911 
> map_context_result (prepp raw_propp); 
19482
9f11af8f7ef9
tuned basic list operators (flat, maps, map_filter);
wenzelm
parents:
19475
diff
changeset

912 
val props = flat propss; 
15703  913 

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

914 
val vars = implicit_vars props; 
81cba3921ba5
goals: simplified handling of implicit variables  removed obsolete warning;
wenzelm
parents:
35624
diff
changeset

915 
val propss' = vars :: propss; 
23418  916 
val goal_propss = filter_out null propss'; 
29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

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

918 
cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss)) 
28627
63663cfa297c
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28458
diff
changeset

919 
> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state)); 
29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

920 
val statement = ((kind, pos), propss', Thm.term_of goal); 
18124  921 
val after_qed' = after_qed >> (fn after_local => 
922 
fn results => map_context after_ctxt #> after_local results); 

5820  923 
in 
17359  924 
goal_state 
21727  925 
> map_context (init_context #> Variable.set_body true) 
47068  926 
> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')) 
42360  927 
> map_context (Proof_Context.auto_bind_goal props) 
21565  928 
> chaining ? (`the_facts #> using_facts) 
47068  929 
> reset_facts 
17359  930 
> open_block 
47068  931 
> reset_goal 
5820  932 
> enter_backward 
23418  933 
> not (null vars) ? refine_terms (length goal_propss) 
32193
c314b4836031
basic method application: avoid Position.setmp_thread_data_seq, which destroys transaction context;
wenzelm
parents:
32187
diff
changeset

934 
> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd) 
5820  935 
end; 
936 

29090
bbfac5fd8d78
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
wenzelm
parents:
28981
diff
changeset

937 
fun generic_qed after_ctxt state = 
12503  938 
let 
36354  939 
val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state; 
8617
33e2bd53aec3
support HindleyMilner polymorphisms in binds and facts;
wenzelm
parents:
8582
diff
changeset

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

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

942 

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

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

944 
flat (tl stmt) 
19915  945 
> Variable.exportT_terms goal_ctxt outer_ctxt; 
17359  946 
val results = 
28627
63663cfa297c
conclude_goal: precise goal context, include all sorts from context into statement, check shyps of result;
wenzelm
parents:
28458
diff
changeset

947 
tl (conclude_goal goal_ctxt goal stmt) 
42360  948 
> burrow (Proof_Context.export goal_ctxt outer_ctxt); 
17359  949 
in 
950 
outer_state 

29090
bbfac5fd8d78
global_qed: refrain from ProofContext.auto_bind_facts, to avoid
wenzelm
parents:
28981
diff
changeset

951 
> map_context (after_ctxt props) 
34239
e18b0f7b9902
after_qed: refrain from Position.setmp_thread_data, which causes duplication of results with several independent proof attempts;
wenzelm
parents:
33389
diff
changeset

952 
> pair (after_qed, results) 
17359  953 
end; 
954 

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

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

956 

9469  957 

17359  958 
(* local goals *) 
959 

17859  960 
fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state = 
17359  961 
let 
21362
3a2ab1dce297
simplified Proof.theorem(_i) interface  removed target support;
wenzelm
parents:
21274
diff
changeset

962 
val ((names, attss), propp) = 
47815  963 
Attrib.map_specs (map (prep_att (context_of state))) stmt > split_list >> split_list; 
17359  964 

18124  965 
fun after_qed' results = 
18808  966 
local_results ((names ~~ attss) ~~ results) 
17359  967 
#> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) 
18124  968 
#> after_qed results; 
5820  969 
in 
17359  970 
state 
21362
3a2ab1dce297
simplified Proof.theorem(_i) interface  removed target support;
wenzelm
parents:
21274
diff
changeset

971 
> generic_goal prepp kind before_qed (after_qed', K I) propp 
19900
21a99d88d925
ProofContext: moved variable operations to struct Variable;
wenzelm
parents:
19862
diff
changeset

972 
> tap (Variable.warn_extra_tfrees (context_of state) o context_of) 
5820  973 
end; 
974 

49866  975 
fun local_qeds arg = 
976 
end_proof false arg 

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

977 
#> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #> 
52da6a736c32
more informative error messages of initial/terminal proof methods;
wenzelm
parents:
49848
diff
changeset

978 
(fn ((after_qed, _), results) => after_qed results)); 
5820  979 

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

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

981 
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
29383  982 

5820  983 

17359  984 
(* global goals *) 
985 

45327  986 
fun prepp_auto_fixes prepp args = 
987 
prepp args #> 

988 
(fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt)); 

989 

990 
fun global_goal prepp before_qed after_qed propp = 

991 
init #> 

992 
generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp; 

17359  993 

42360  994 
val theorem = global_goal Proof_Context.bind_propp_schematic_i; 
995 
val theorem_cmd = global_goal Proof_Context.bind_propp_schematic; 

12065  996 

49866  997 
fun global_qeds arg = 
998 
end_proof true arg 

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

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

1000 
after_qed results (context_of state))); 
17112  1001 

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

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

1003 
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
12959  1004 

5820  1005 

49907  1006 
(* terminal proof steps *) 
17112  1007 

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

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

1009 

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

1010 
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

1011 
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

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

1013 

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

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

1015 

29383  1016 
fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true); 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

1018 
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

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

29383  1021 
fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true); 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

1023 
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

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

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

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

1027 

6896  1028 

49907  1029 
(* skip proofs *) 
1030 

1031 
local 

1032 

1033 
fun skipped_proof state = 

50885
f3588e59aeaa
restrict "bad" markup to command keyword, notably excluding subsequent comments;
wenzelm
parents:
50315
diff
changeset

1034 
Context_Position.report_text (context_of state) (Position.thread_data ()) 
f3588e59aeaa
restrict "bad" markup to command keyword, notably excluding subsequent comments;
wenzelm
parents:
50315
diff
changeset

1035 
Markup.bad "Skipped proof"; 
49907  1036 

1037 
in 

1038 

1039 
fun local_skip_proof int state = 

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

1041 
skipped_proof state; 

1042 

1043 
fun global_skip_proof int state = 

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

1045 
skipped_proof state; 

1046 

1047 
end; 

1048 

1049 

17359  1050 
(* common goal statements *) 
1051 

1052 
local 

1053 

17859  1054 
fun gen_have prep_att prepp before_qed after_qed stmt int = 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49912
diff
changeset

1055 
local_goal (Proof_Display.print_results Markup.state int) 
46728
85f8e3932712
display proof results as "state", to suppress odd squiggles in the Prover IDE (see also 9240be8c8c69);
wenzelm
parents:
46466
diff
changeset

1056 
prep_att prepp "have" before_qed after_qed stmt; 
6896  1057 

17859  1058 
fun gen_show prep_att prepp before_qed after_qed stmt int state = 
17359  1059 
let 
32738  1060 
val testing = Unsynchronized.ref false; 
1061 
val rule = Unsynchronized.ref (NONE: thm option); 

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

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

17359  1067 
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

1068 
if ! testing then () 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49912
diff
changeset

1069 
else Proof_Display.print_results Markup.state int ctxt res; 
17359  1070 
fun print_rule ctxt th = 
1071 
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

1072 
else if int then 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49912
diff
changeset

1073 
writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th)) 
17359  1074 
else (); 
1075 
val test_proof = 

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

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

1077 
> Unsynchronized.setmp testing true 
42042  1078 
> Exn.interruptible_capture; 
6896  1079 

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

1081 
refine_goals print_rule (context_of state) (flat results) 
29383  1082 
#> check_result "Failed to refine any pending goal" 
1083 
#> after_qed results; 

17359  1084 
in 
1085 
state 

17859  1086 
> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt 
21565  1087 
> int ? (fn goal_state => 
49907  1088 
(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

1089 
Exn.Res _ => goal_state 
42042  1090 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1091 
end; 
1092 

1093 
in 

1094 

42360  1095 
val have = gen_have (K I) Proof_Context.bind_propp_i; 
47815  1096 
val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp; 
42360  1097 
val show = gen_show (K I) Proof_Context.bind_propp_i; 
47815  1098 
val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp; 
6896  1099 

5820  1100 
end; 
17359  1101 

28410  1102 

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

1103 

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

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

1105 

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

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

1107 

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

1108 
fun is_schematic t = 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1109 
Term.exists_subterm Term.is_Var t orelse 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1110 
Term.exists_type (Term.exists_subtype Term.is_TVar) t; 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1111 

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

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

1113 
let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1114 
in is_schematic prop end; 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1115 

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

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

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

1118 
NONE => true 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1119 
 SOME (_, (_, {statement = (_, _, prop), goal, ...})) => 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

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

1121 

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

1122 

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

1123 
(* full proofs *) 
28410  1124 

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

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

1126 

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

1127 
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

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

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

1130 
val empty = 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

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

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

1133 

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

1134 
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

1135 
(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

1136 
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

1137 
 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

1138 

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

1139 
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

1140 
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

1141 

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

1142 
fun future_proof done get_context fork_proof state = 
28410  1143 
let 
29381
45d77aeb1608
future_terminal_proof: no fork for interactive mode, assert_backward;
wenzelm
parents:
29364
diff
changeset

1144 
val _ = assert_backward state; 
28410  1145 
val (goal_ctxt, (_, goal)) = find_goal state; 
32786  1146 
val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal; 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

1147 
val goal_tfrees = 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

1148 
fold Term.add_tfrees 
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

1149 
(prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; 
28410  1150 

29383  1151 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1152 

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

1153 
val prop' = Logic.protect prop; 
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1154 
val statement' = (kind, [[], [prop']], prop'); 
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1155 
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) 
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1156 
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI); 
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

1157 
val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th); 
28410  1158 

28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1159 
val result_ctxt = 
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1160 
state 
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

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

1162 
> map_goal I (K (statement', messages, using, goal', before_qed, after_qed')) 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

1163 
(fold (Variable.declare_typ o TFree) goal_tfrees) 
29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

1164 
> fork_proof; 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1165 

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

1166 
val future_thm = result_ctxt > Future.map (fn (_, x) => the_result (get_context x)); 
32062
457f5bcd3d76
Proof.future_proof: declare all assumptions as well;
wenzelm
parents:
32061
diff
changeset

1167 
val finished_goal = Goal.future_result goal_ctxt future_thm prop'; 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1168 
val state' = 
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1169 
state 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

1170 
> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1171 
> done; 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

1172 
in (Future.map #1 result_ctxt, state') end; 
28410  1173 

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

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

1175 

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

1176 
fun local_future_proof x = future_proof local_done_proof context_of x; 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1177 
fun global_future_proof x = future_proof global_done_proof I x; 
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1178 

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

1180 

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

1181 

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

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

1183 

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

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

1185 

49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1186 
fun future_terminal_proof n proof1 proof2 meths int state = 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1187 
if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int) 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1188 
andalso not (is_relevant state) 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1189 
then 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1190 
snd (proof2 (fn state' => 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1191 
Goal.fork_name "Proof.future_terminal_proof" (fn () => ((), proof1 meths state'))) state) 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1192 
else proof1 meths state; 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1193 

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

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

1195 

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

1196 
fun local_future_terminal_proof x = 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1197 
future_terminal_proof 2 local_terminal_proof local_future_proof x; 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1198 

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

1199 
fun global_future_terminal_proof x = 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

1200 
future_terminal_proof 3 global_terminal_proof global_future_proof x; 
29350  1201 

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

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

1203 

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

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

1205 