author  wenzelm 
Fri, 09 May 2014 22:14:06 +0200  
changeset 56933  b47193851dc6 
parent 56932  11a4001b06c6 
child 57486  2131b6633529 
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 
52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

35 
val pretty_goal_messages: state > Pretty.T list 
12423  36 
val pretty_state: int > state > Pretty.T list 
17112  37 
val refine: Method.text > state > state Seq.seq 
38 
val refine_end: Method.text > state > state Seq.seq 

18908  39 
val refine_insert: thm list > state > state 
17359  40 
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

41 
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

42 
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

43 
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

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

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

46 
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

47 
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

48 
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

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

50 
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

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

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

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

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

55 
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

56 
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

57 
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

58 
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

59 
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

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

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

63 
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

64 
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

65 
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

66 
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

67 
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

68 
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

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

70 
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

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

72 
val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list > state > state 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

73 
val invoke_case: (string * Position.T) * binding option list * attribute list > 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

74 
state > state 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

75 
val invoke_case_cmd: (string * Position.T) * binding option list * Attrib.src list > 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

76 
state > state 
17359  77 
val begin_block: state > state 
78 
val next_block: state > state 

20309  79 
val end_block: state > state 
49042  80 
val begin_notepad: context > state 
81 
val end_notepad: state > context 

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

83 
val proof_results: Method.text_range option > state > state Seq.result Seq.seq 
49865  84 
val defer: int > state > state 
85 
val prefer: int > state > state 

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

88 
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

89 
val apply_end_results: Method.text_range > state > state Seq.result Seq.seq 
17359  90 
val local_goal: (context > ((string * string) * (string * thm list) list) > unit) > 
49042  91 
(context > 'a > attribute) > 
45327  92 
('b list > context > (term list list * (context > context)) * context) > 
29383  93 
string > Method.text option > (thm list list > state > state) > 
29581  94 
((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

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

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

98 
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

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

100 
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

101 
val local_terminal_proof: Method.text_range * Method.text_range option > state > state 
29383  102 
val local_default_proof: state > state 
103 
val local_immediate_proof: state > state 

104 
val local_skip_proof: bool > state > state 

105 
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

106 
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

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

108 
val global_immediate_proof: state > context 
29383  109 
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

110 
val global_done_proof: state > context 
29383  111 
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

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

113 
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

114 
(Attrib.binding * (string * string list) list) list > bool > state > state 
29383  115 
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

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

117 
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

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

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

120 
val is_relevant: state > bool 
51318  121 
val future_proof: (state > ('a * context) future) > state > 'a future * state 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

124 
val global_future_terminal_proof: Method.text_range * Method.text_range option > bool > 
49866  125 
state > context 
5820  126 
end; 
127 

13377  128 
structure Proof: PROOF = 
5820  129 
struct 
130 

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

131 
type context = Proof.context; 
17112  132 
type method = Method.method; 
16813  133 

5820  134 

135 
(** proof state **) 

136 

17359  137 
(* datatype state *) 
5820  138 

17112  139 
datatype mode = Forward  Chain  Backward; 
5820  140 

17359  141 
datatype state = 
142 
State of node Stack.T 

143 
and node = 

7176  144 
Node of 
145 
{context: context, 

146 
facts: thm list option, 

147 
mode: mode, 

17359  148 
goal: goal option} 
149 
and goal = 

150 
Goal of 

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

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

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

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

159 
(thm list list > context > context)}; 
17359  160 

24543  161 
fun make_goal (statement, messages, using, goal, before_qed, after_qed) = 
162 
Goal {statement = statement, messages = messages, using = using, goal = goal, 

17859  163 
before_qed = before_qed, after_qed = after_qed}; 
5820  164 

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

167 

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

5820  170 

21727  171 
val init_context = 
42360  172 
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

173 
Proof_Context.map_naming (K Name_Space.local_naming); 
21727  174 

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

175 
fun init ctxt = 
21727  176 
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); 
5820  177 

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

178 
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

179 
fun map_top f (State st) = State (Stack.map_top (map_node f) st); 
28278  180 
fun map_all f (State st) = State (Stack.map_all (map_node f) st); 
12045  181 

5820  182 

183 

184 
(** basic proof state operations **) 

185 

17359  186 
(* block structure *) 
187 

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

189 

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

191 
handle List.Empty => error "Unbalanced block parentheses"; 
17359  192 

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

194 

195 
fun assert_bottom b state = 

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

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

17359  199 
else state 
200 
end; 

201 

202 

5820  203 
(* context *) 
204 

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

205 
val context_of = #context o top; 
42360  206 
val theory_of = Proof_Context.theory_of o context_of; 
5820  207 

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

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

209 
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

210 

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

212 
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
5820  213 

17359  214 
fun map_context_result f state = 
17859  215 
f (context_of state) > (fn ctxt => map_context (K ctxt) state); 
5820  216 

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

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

219 
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

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

221 

42360  222 
val bind_terms = map_context o Proof_Context.bind_terms; 
223 
val put_thms = map_context oo Proof_Context.put_thms; 

5820  224 

225 

226 
(* facts *) 

227 

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

228 
val get_facts = #facts o top; 
17359  229 

230 
fun the_facts state = 

231 
(case get_facts state of SOME facts => facts 

18678  232 
 NONE => error "No current facts available"); 
5820  233 

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

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

239 
map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> 
33386  240 
put_thms true (Auto_Bind.thisN, facts); 
5820  241 

47068  242 
val set_facts = put_facts o SOME; 
243 
val reset_facts = put_facts NONE; 

244 

17359  245 
fun these_factss more_facts (named_factss, state) = 
47068  246 
(named_factss, state > set_facts (maps snd named_factss @ more_facts)); 
5820  247 

17359  248 
fun export_facts inner outer = 
249 
(case get_facts inner of 

47068  250 
NONE => reset_facts outer 
17359  251 
 SOME thms => 
252 
thms 

42360  253 
> Proof_Context.export (context_of inner) (context_of outer) 
47068  254 
> (fn ths => set_facts ths outer)); 
5820  255 

256 

257 
(* mode *) 

258 

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

259 
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

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

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

264 
fun assert_mode pred state = 

265 
let val mode = get_mode state in 

266 
if pred mode then state 

18678  267 
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode") 
5820  268 
end; 
269 

19308  270 
val assert_forward = assert_mode (fn mode => mode = Forward); 
271 
val assert_chain = assert_mode (fn mode => mode = Chain); 

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

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

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

5820  275 

17359  276 
val enter_forward = put_mode Forward; 
277 
val enter_chain = put_mode Chain; 

278 
val enter_backward = put_mode Backward; 

5820  279 

17359  280 

281 
(* current goal *) 

282 

283 
fun current_goal state = 

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

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

17359  288 
fun assert_current_goal g state = 
289 
let val g' = can current_goal state in 

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

17359  292 
else state 
293 
end; 

6776  294 

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

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

47068  297 
val set_goal = put_goal o SOME; 
298 
val reset_goal = put_goal NONE; 

299 

17859  300 
val before_qed = #before_qed o #2 o current_goal; 
301 

17359  302 

303 
(* nested goal *) 

5820  304 

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

305 
fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) = 
17359  306 
let 
24543  307 
val Goal {statement, messages, using, goal, before_qed, after_qed} = goal; 
308 
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

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

310 
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

311 
 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

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

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

314 
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

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

316 
 map_goal _ _ _ state = state; 
5820  317 

47068  318 
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

319 
(statement, [], using, goal, before_qed, after_qed)) I; 
19188  320 

24543  321 
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

322 
(statement, msg :: messages, using, goal, before_qed, after_qed)) I; 
24543  323 

24556  324 
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

325 
(statement, [], using, goal, before_qed, after_qed)) I; 
17359  326 

327 
local 

328 
fun find i state = 

329 
(case try current_goal state of 

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

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

334 
fun get_goal state = 

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

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

5820  337 

338 

339 

12423  340 
(** pretty_state **) 
5820  341 

52641
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

342 
fun pretty_goal_messages state = 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

343 
(case try find_goal state of 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

344 
SOME (_, (_, {messages, ...})) => map (fn msg => msg ()) (rev messages) 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

345 
 NONE => []); 
c56b6fa636e8
hybrid "auto" tool setup, for TTY (within theory) and PIDE (global print function);
wenzelm
parents:
52458
diff
changeset

346 

15531  347 
fun pretty_facts _ _ NONE = [] 
51584  348 
 pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""]; 
6756  349 

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

352 
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

353 
val verbose = Config.get ctxt Proof_Context.verbose; 
5820  354 

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

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

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

367 

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

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

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

371 
[Pretty.mark_str (position_markup, "proof"), 
293cd4dcfebc
some position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56898
diff
changeset

372 
Pretty.str (" (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2  1))], 
17359  373 
Pretty.str ""] @ 
374 
(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

375 
(if verbose orelse mode = Forward then 
51584  376 
pretty_facts ctxt "" facts @ prt_goal (try find_goal state) 
377 
else if mode = Chain then pretty_facts ctxt "picking" facts 

17359  378 
else prt_goal (try find_goal state)) 
379 
end; 

5820  380 

381 

382 

383 
(** proof steps **) 

384 

17359  385 
(* refine via method *) 
5820  386 

8234  387 
local 
388 

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

391 

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

393 

394 
fun goal_cases st = 

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

16146  397 

55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

398 
fun apply_method current_context method state = 
6848  399 
let 
24556  400 
val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = 
24543  401 
find_goal state; 
25958  402 
val ctxt = if current_context then context_of state else goal_ctxt; 
16146  403 
in 
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

404 
Method.apply method ctxt using goal > Seq.map (fn (meth_cases, goal') => 
6848  405 
state 
16146  406 
> map_goal 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

407 
(Proof_Context.update_cases false (no_goal_cases goal @ goal_cases goal') #> 
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

408 
Proof_Context.update_cases true meth_cases) 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

409 
(K (statement, [], using, goal', before_qed, after_qed)) I) 
16146  410 
end; 
5820  411 

19188  412 
fun select_goals n meth state = 
51383  413 
ALLGOALS Goal.conjunction_tac (#2 (#2 (get_goal state))) 
19224  414 
> Seq.maps (fn goal => 
19188  415 
state 
52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

416 
> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal) 
19188  417 
> Seq.maps meth 
418 
> Seq.maps (fn state' => state' 

52458
210bca64b894
less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context;
wenzelm
parents:
52456
diff
changeset

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

420 
> Seq.maps (apply_method true (K Method.succeed))); 
19188  421 

55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

422 
fun apply_text current_context text state = 
17112  423 
let 
55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

424 
val ctxt = context_of state; 
17112  425 

55742
a989bdaf8121
modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion;
wenzelm
parents:
55709
diff
changeset

426 
fun eval (Method.Basic m) = apply_method current_context m 
55997
9dc5ce83202c
modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121);
wenzelm
parents:
55955
diff
changeset

427 
 eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src) 
55765  428 
 eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts) 
429 
 eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts) 

430 
 eval (Method.Try (_, txt)) = Seq.TRY (eval txt) 

431 
 eval (Method.Repeat1 (_, txt)) = Seq.REPEAT1 (eval txt) 

432 
 eval (Method.Select_Goals (_, n, txt)) = select_goals n (eval txt); 

17112  433 
in eval text state end; 
434 

8234  435 
in 
436 

17112  437 
val refine = apply_text true; 
438 
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

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

8234  441 
end; 
442 

5820  443 

17359  444 
(* refine via subproof *) 
445 

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

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

447 

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

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

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

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

451 
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

452 
if can Logic.unprotect (Logic.strip_assums_concl goal) then 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

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

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

455 

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

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

457 
Goal.norm_hhf_tac ctxt THEN' 
52732  458 
rtac rule THEN' 
54742
7a86358a3c0b
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
wenzelm
parents:
54567
diff
changeset

459 
finish_tac ctxt (Thm.nprems_of rule); 
11816  460 

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

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

462 
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

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

464 

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

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

466 

19915  467 
fun refine_goals print_rule inner raw_rules state = 
468 
let 

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

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

470 
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st); 
19915  471 
in 
472 
raw_rules 

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

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

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

478 

6932  479 

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

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

481 

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

482 
fun conclude_goal ctxt goal propss = 
5820  483 
let 
42360  484 
val thy = Proof_Context.theory_of ctxt; 
5820  485 

54981  486 
val _ = 
487 
Theory.subthy (theory_of_thm goal, thy) orelse error "Bad background theory of goal state"; 

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

489 

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

490 
fun lost_structure () = error ("Lost goal structure:\n" ^ Display.string_of_thm ctxt goal); 
5820  491 

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

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

493 
(Goal.conclude (if length (flat propss) > 1 then Thm.norm_proof goal else goal) 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
53380
diff
changeset

494 
handle THM _ => lost_structure ()) 
cfe53047dc16
more uniform / rigid checking of Goal.prove_common vs. Proof.conclude_goal  NB: Goal.prove_common cannot check hyps right now, e.g. due to undeclared Simplifier prems;
wenzelm
parents:
53380
diff
changeset

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

496 
> Thm.check_shyps (Variable.sorts_of ctxt) 
54993
625370769fc0
check_hyps for attribute application (still inactive, due to noncompliant tools);
wenzelm
parents:
54984
diff
changeset

497 
> Thm.check_hyps (Context.Proof ctxt); 
23418  498 

499 
val goal_propss = filter_out null propss; 

500 
val results = 

501 
Conjunction.elim_balanced (length goal_propss) th 

502 
> map2 Conjunction.elim_balanced (map length goal_propss) 

503 
handle THM _ => lost_structure (); 

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

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

505 
error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th); 
23418  506 

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

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

509 
 recover_result [] [] = [] 

510 
 recover_result _ _ = lost_structure (); 

511 
in recover_result propss results end; 

5820  512 

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

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

514 

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

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

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

517 
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

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

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

520 
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

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

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

523 

5820  524 

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

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

526 

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

528 
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

529 
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

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

532 

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

534 
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

535 
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

536 
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

537 
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

538 

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

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

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

541 
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

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

543 

49866  544 
fun method_error kind pos state = 
545 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  546 

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

547 

5820  548 

549 
(*** structured proof commands ***) 

550 

17112  551 
(** context elements **) 
5820  552 

36324  553 
(* let bindings *) 
5820  554 

16813  555 
local 
556 

17359  557 
fun gen_bind bind args state = 
5820  558 
state 
559 
> assert_forward 

36324  560 
> map_context (bind true args #> snd) 
47068  561 
> reset_facts; 
5820  562 

16813  563 
in 
564 

42360  565 
val let_bind = gen_bind Proof_Context.match_bind_i; 
566 
val let_bind_cmd = gen_bind Proof_Context.match_bind; 

5820  567 

16813  568 
end; 
569 

5820  570 

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

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

572 

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

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

574 

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

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

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

579 

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

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

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

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

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

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

586 

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

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

588 

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

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

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

591 

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

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

593 

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

594 

17359  595 
(* fix *) 
9196  596 

12714  597 
local 
598 

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

599 
fun gen_fix prep_vars args = 
17359  600 
assert_forward 
45597  601 
#> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt)) 
47068  602 
#> reset_facts; 
5820  603 

16813  604 
in 
605 

45597  606 
val fix = gen_fix Proof_Context.cert_vars; 
607 
val fix_cmd = gen_fix Proof_Context.read_vars; 

5820  608 

16813  609 
end; 
610 

5820  611 

17359  612 
(* assume etc. *) 
5820  613 

16813  614 
local 
615 

17112  616 
fun gen_assume asm prep_att exp args state = 
5820  617 
state 
618 
> assert_forward 

47815  619 
> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args)) 
17359  620 
> these_factss [] > #2; 
6932  621 

16813  622 
in 
623 

42360  624 
val assm = gen_assume Proof_Context.add_assms_i (K I); 
47815  625 
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

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

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

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

629 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  630 

16813  631 
end; 
632 

7271  633 

17359  634 
(* def *) 
11891  635 

16813  636 
local 
637 

20913  638 
fun gen_def prep_att prep_vars prep_binds args state = 
11891  639 
let 
640 
val _ = assert_forward state; 

20913  641 
val (raw_name_atts, (raw_vars, raw_rhss)) = args > split_list > split_list; 
47815  642 
val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts; 
11891  643 
in 
20913  644 
state 
645 
> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars)) 

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

647 
> (fn vars => 

648 
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

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

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

651 
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

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

653 
in map_context_result (Local_Defs.add_defs defs) end)) 
47068  654 
> (set_facts o map (#2 o #2)) 
11891  655 
end; 
656 

16813  657 
in 
658 

42360  659 
val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i; 
47815  660 
val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind; 
11891  661 

16813  662 
end; 
663 

11891  664 

8374  665 

17112  666 
(** facts **) 
5820  667 

17359  668 
(* chain *) 
5820  669 

24011  670 
fun clean_facts ctxt = 
47068  671 
set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt; 
24011  672 

17359  673 
val chain = 
674 
assert_forward 

24011  675 
#> clean_facts 
17359  676 
#> enter_chain; 
5820  677 

17359  678 
fun chain_facts facts = 
47068  679 
set_facts facts 
17359  680 
#> chain; 
5820  681 

682 

17359  683 
(* note etc. *) 
17112  684 

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

687 
local 

688 

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

689 
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state = 
17112  690 
state 
691 
> assert_forward 

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

17112  694 
> these_factss (more_facts state) 
17359  695 
> opt_chain 
696 
> opt_result; 

17112  697 

698 
in 

699 

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

700 
val note_thmss = gen_thmss (K []) I #2 (K I) (K I); 
47815  701 
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact; 
17112  702 

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

703 
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding; 
47815  704 
val from_thmss_cmd = 
705 
gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding; 

17359  706 

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

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

710 

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

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

17112  713 
end; 
714 

715 

18548  716 
(* using/unfolding *) 
17112  717 

718 
local 

719 

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

720 
fun gen_using f g prep_att prep_fact args state = 
17112  721 
state 
722 
> assert_backward 

21442  723 
> map_context_result 
47815  724 
(fn ctxt => ctxt > Proof_Context.note_thmss "" 
725 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args))) 

18843  726 
> (fn (named_facts, state') => 
24556  727 
state' > map_goal I (fn (statement, _, using, goal, before_qed, after_qed) => 
18843  728 
let 
729 
val ctxt = context_of state'; 

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

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

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

24050  733 
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 
35624  734 
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 
735 
val unfold_goals = Local_Defs.unfold_goals; 

17112  736 

737 
in 

738 

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

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

741 
val unfolding = gen_using unfold_using unfold_goals (K I) (K I); 
47815  742 
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact; 
17112  743 

744 
end; 

745 

746 

747 
(* case *) 

748 

749 
local 

750 

53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

751 
fun gen_invoke_case prep_att ((name, pos), xs, raw_atts) state = 
17112  752 
let 
47815  753 
val atts = map (prep_att (context_of state)) raw_atts; 
19078  754 
val (asms, state') = state > map_context_result (fn ctxt => 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

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

756 
val assumptions = 
08f3491c50bf
cases: formal binding of 'assumes', with position provided via invoke_case;
wenzelm
parents:
53378
diff
changeset

757 
asms > map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts)); 
17112  758 
in 
759 
state' 

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

760 
> assume assumptions 
33386  761 
> bind_terms Auto_Bind.no_facts 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

762 
> `the_facts > (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])]) 
17112  763 
end; 
764 

765 
in 

766 

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

767 
val invoke_case = gen_invoke_case (K I); 
47815  768 
val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd; 
17112  769 

770 
end; 

771 

772 

773 

17359  774 
(** proof structure **) 
775 

776 
(* blocks *) 

777 

778 
val begin_block = 

779 
assert_forward 

780 
#> open_block 

47068  781 
#> reset_goal 
17359  782 
#> open_block; 
783 

784 
val next_block = 

785 
assert_forward 

786 
#> close_block 

787 
#> open_block 

47068  788 
#> reset_goal 
789 
#> reset_facts; 

17359  790 

791 
fun end_block state = 

792 
state 

793 
> assert_forward 

40960  794 
> assert_bottom false 
17359  795 
> close_block 
796 
> assert_current_goal false 

797 
> close_block 

798 
> export_facts state; 

799 

800 

40960  801 
(* global notepad *) 
802 

803 
val begin_notepad = 

804 
init 

805 
#> open_block 

806 
#> map_context (Variable.set_body true) 

807 
#> open_block; 

808 

809 
val end_notepad = 

810 
assert_forward 

811 
#> assert_bottom true 

812 
#> close_block 

813 
#> assert_current_goal false 

814 
#> close_block 

815 
#> context_of; 

816 

817 

17359  818 
(* subproofs *) 
819 

820 
fun proof opt_text = 

821 
assert_backward 

17859  822 
#> refine (the_default Method.default_text opt_text) 
17359  823 
#> Seq.map (using_facts [] #> enter_forward); 
824 

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

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

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

828 

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

829 
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

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

831 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

847 
end; 
17359  848 

29383  849 
fun check_result msg sq = 
850 
(case Seq.pull sq of 

851 
NONE => error msg 

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

853 

17359  854 

855 
(* unstructured refinement *) 

856 

49865  857 
fun defer i = 
858 
assert_no_chain #> 

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

860 

861 
fun prefer i = 

862 
assert_no_chain #> 

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

17359  864 

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

49866  866 

17359  867 
fun apply_end text = assert_forward #> refine_end text; 
868 

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

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

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

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

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

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

874 

17359  875 

876 

17112  877 
(** goals **) 
878 

17359  879 
(* generic goals *) 
880 

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

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

882 

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

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

884 
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

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

886 

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

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

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

891 
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

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

893 

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

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

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

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

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

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

899 

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

900 
in 
17359  901 

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

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

5936  910 
state 
911 
> assert_forward_or_chain 

912 
> enter_forward 

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

915 
val props = flat propss; 
15703  916 

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

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

918 
val propss' = vars :: propss; 
23418  919 
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

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

921 
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

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

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

5820  926 
in 
17359  927 
goal_state 
21727  928 
> map_context (init_context #> Variable.set_body true) 
47068  929 
> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed')) 
42360  930 
> map_context (Proof_Context.auto_bind_goal props) 
21565  931 
> chaining ? (`the_facts #> using_facts) 
47068  932 
> reset_facts 
17359  933 
> open_block 
47068  934 
> reset_goal 
5820  935 
> enter_backward 
23418  936 
> 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

937 
> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd) 
5820  938 
end; 
939 

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

940 
fun generic_qed after_ctxt state = 
12503  941 
let 
36354  942 
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

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

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

945 

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

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

947 
flat (tl stmt) 
19915  948 
> Variable.exportT_terms goal_ctxt outer_ctxt; 
17359  949 
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

950 
tl (conclude_goal goal_ctxt goal stmt) 
42360  951 
> burrow (Proof_Context.export goal_ctxt outer_ctxt); 
17359  952 
in 
953 
outer_state 

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

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

955 
> pair (after_qed, results) 
17359  956 
end; 
957 

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

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

959 

9469  960 

17359  961 
(* local goals *) 
962 

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

965 
val ((names, attss), propp) = 
47815  966 
Attrib.map_specs (map (prep_att (context_of state))) stmt > split_list >> split_list; 
17359  967 

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

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

975 
> tap (Variable.warn_extra_tfrees (context_of state) o context_of) 
5820  976 
end; 
977 

49866  978 
fun local_qeds arg = 
979 
end_proof false arg 

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

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

981 
(fn ((after_qed, _), results) => after_qed results)); 
5820  982 

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

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

984 
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
29383  985 

5820  986 

17359  987 
(* global goals *) 
988 

45327  989 
fun prepp_auto_fixes prepp args = 
990 
prepp args #> 

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

992 

993 
fun global_goal prepp before_qed after_qed propp = 

994 
init #> 

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

17359  996 

42360  997 
val theorem = global_goal Proof_Context.bind_propp_schematic_i; 
998 
val theorem_cmd = global_goal Proof_Context.bind_propp_schematic; 

12065  999 

49866  1000 
fun global_qeds arg = 
1001 
end_proof true arg 

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

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

1003 
after_qed results (context_of state))); 
17112  1004 

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

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

1006 
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
12959  1007 

5820  1008 

49907  1009 
(* terminal proof steps *) 
17112  1010 

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

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

1012 

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

1013 
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

1014 
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

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

1016 

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

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

1018 

29383  1019 
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

1020 
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

1021 
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

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

29383  1024 
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

1025 
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

1026 
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

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

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

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

1030 

6896  1031 

49907  1032 
(* skip proofs *) 
1033 

1034 
fun local_skip_proof int state = 

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

51551  1036 
Skip_Proof.report (context_of state); 
49907  1037 

1038 
fun global_skip_proof int state = 

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

51551  1040 
Skip_Proof.report (context_of state); 
49907  1041 

1042 

17359  1043 
(* common goal statements *) 
1044 

1045 
local 

1046 

17859  1047 
fun gen_have prep_att prepp before_qed after_qed stmt int = 
56932
11a4001b06c6
more position markup to help locating the query context, e.g. from "Info" dockable;
wenzelm
parents:
56912
diff
changeset

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

1049 
prep_att prepp "have" before_qed after_qed stmt; 
6896  1050 

17859  1051 
fun gen_show prep_att prepp before_qed after_qed stmt int state = 
17359  1052 
let 
32738  1053 
val testing = Unsynchronized.ref false; 
1054 
val rule = Unsynchronized.ref (NONE: thm option); 

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

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

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

1060 
val pos = Position.thread_data (); 
17359  1061 
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

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

1063 
else Proof_Display.print_results int pos ctxt res; 
17359  1064 
fun print_rule ctxt th = 
1065 
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

1066 
else if int then 
56933  1067 
Proof_Display.string_of_rule ctxt "Successful" th 
1068 
> Markup.markup Markup.text_fold 

1069 
> Markup.markup Markup.state 

1070 
> writeln 

17359  1071 
else (); 
1072 
val test_proof = 

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

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

1074 
> Unsynchronized.setmp testing true 
42042  1075 
> Exn.interruptible_capture; 
6896  1076 

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

1078 
refine_goals print_rule (context_of state) (flat results) 
29383  1079 
#> check_result "Failed to refine any pending goal" 
1080 
#> after_qed results; 

17359  1081 
in 
1082 
state 

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

1086 
Exn.Res _ => goal_state 
42042  1087 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1088 
end; 
1089 

1090 
in 

1091 

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

5820  1097 
end; 
17359  1098 

28410  1099 

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

1100 

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

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

1102 

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

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

1104 

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

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

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

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

1108 

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

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

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

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

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

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

1114 

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 
(* full proofs *) 
28410  1117 

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

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

1119 

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

1120 
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

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

1122 
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

1123 
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

1124 
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

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

1126 

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

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

1129 
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

1130 
 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

1131 

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

1133 
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

1134 

51318  1135 
in 
1136 

1137 
fun future_proof fork_proof state = 

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

1139 
val _ = assert_backward state; 
28410  1140 
val (goal_ctxt, (_, goal)) = find_goal state; 
32786  1141 
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

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

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

1144 
(prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; 
28410  1145 

29383  1146 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1147 

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

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

1149 
val statement' = (kind, [[], [prop']], prop'); 
52456  1150 
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal) (Goal.protect (Thm.nprems_of goal) goal); 
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

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

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

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

1154 
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

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

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

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

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

1159 

51318  1160 
val future_thm = Future.map (the_result o snd) result_ctxt; 
32062
457f5bcd3d76
Proof.future_proof: declare all assumptions as well;
wenzelm
parents:
32061
diff
changeset

1161 
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

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

1163 
state 
51318  1164 
> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I; 
1165 
in (Future.map fst result_ctxt, state') end; 

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

1166 

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

1168 

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

1169 

51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1170 
(* terminal proofs *) (* FIXME avoid toplevel imitation  include in PIDE/document *) 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1171 

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

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

1173 

51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51584
diff
changeset

1174 
fun future_terminal_proof proof1 proof2 done int state = 
53189
ee8b8dafef0e
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents:
52732
diff
changeset

1175 
if Goal.future_enabled 3 andalso not (is_relevant state) then 
51318  1176 
state > future_proof (fn state' => 
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1177 
let 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1178 
val pos = Position.thread_data (); 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1179 
val props = Markup.command_timing :: (Markup.nameN, "by") :: Position.properties_of pos; 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1180 
in 
53192  1181 
Execution.fork {name = "Proof.future_terminal_proof", pos = pos, pri = ~1} 
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1182 
(fn () => ((), Timing.protocol props proof2 state')) 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51606
diff
changeset

1183 
end) > snd > done 
51318  1184 
else proof1 state; 
29385
c96b91bab2e6
future_proof: refined version covers local_future_proof and global_future_proof;
wenzelm
parents:
29383
diff
changeset

1185 

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

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

1187 

51318  1188 
fun local_future_terminal_proof meths = 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51584
diff
changeset

1189 
future_terminal_proof 
51318  1190 
(local_terminal_proof meths) 
1191 
(local_terminal_proof meths #> context_of) local_done_proof; 

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

1192 

51318  1193 
fun global_future_terminal_proof meths = 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51584
diff
changeset

1194 
future_terminal_proof 
51318  1195 
(global_terminal_proof meths) 
1196 
(global_terminal_proof meths) global_done_proof; 

29350  1197 

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

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

1199 

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

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

1201 