author  wenzelm 
Wed, 07 May 2014 14:05:17 +0200  
changeset 56898  ba507cc96473 
parent 56897  c668735fb8b5 
child 56912  293cd4dcfebc 
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 []; 
17359  367 
in 
56898
ba507cc96473
tuned message: "step" goes back to TTY mode before Proof General, while "depth" is more informative but sometimes confusing due to implementation details;
wenzelm
parents:
56897
diff
changeset

368 
[Pretty.str ("proof (" ^ mode_name mode ^ "): depth " ^ string_of_int (level state div 2  1)), 
17359  369 
Pretty.str ""] @ 
370 
(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

371 
(if verbose orelse mode = Forward then 
51584  372 
pretty_facts ctxt "" facts @ prt_goal (try find_goal state) 
373 
else if mode = Chain then pretty_facts ctxt "picking" facts 

17359  374 
else prt_goal (try find_goal state)) 
375 
end; 

5820  376 

377 

378 

379 
(** proof steps **) 

380 

17359  381 
(* refine via method *) 
5820  382 

8234  383 
local 
384 

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

387 

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

389 

390 
fun goal_cases st = 

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

16146  393 

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

394 
fun apply_method current_context method state = 
6848  395 
let 
24556  396 
val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) = 
24543  397 
find_goal state; 
25958  398 
val ctxt = if current_context then context_of state else goal_ctxt; 
16146  399 
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

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

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

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

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

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

412 
> Seq.lift provide_goal ((PRIMITIVE (Goal.restrict 1 n) THEN Goal.conjunction_tac 1) goal) 
19188  413 
> Seq.maps meth 
414 
> 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

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

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

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

418 
fun apply_text current_context text state = 
17112  419 
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

420 
val ctxt = context_of state; 
17112  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 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

423 
 eval (Method.Source src) = apply_method current_context (Method.method_cmd ctxt src) 
55765  424 
 eval (Method.Then (_, txts)) = Seq.EVERY (map eval txts) 
425 
 eval (Method.Orelse (_, txts)) = Seq.FIRST (map eval txts) 

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

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

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

17112  429 
in eval text state end; 
430 

8234  431 
in 
432 

17112  433 
val refine = apply_text true; 
434 
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

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

8234  437 
end; 
438 

5820  439 

17359  440 
(* refine via subproof *) 
441 

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

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

443 

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

444 
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

445 
 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

446 
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

447 
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

448 
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

449 
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

450 
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

451 

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

452 
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

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

455 
finish_tac ctxt (Thm.nprems_of rule); 
11816  456 

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

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

458 
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

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

460 

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

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

462 

19915  463 
fun refine_goals print_rule inner raw_rules state = 
464 
let 

465 
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

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

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

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

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

474 

6932  475 

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

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

477 

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

478 
fun conclude_goal ctxt goal propss = 
5820  479 
let 
42360  480 
val thy = Proof_Context.theory_of ctxt; 
5820  481 

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

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

485 

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

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

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

488 
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

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

490 
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

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

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

493 
> Thm.check_hyps (Context.Proof ctxt); 
23418  494 

495 
val goal_propss = filter_out null propss; 

496 
val results = 

497 
Conjunction.elim_balanced (length goal_propss) th 

498 
> map2 Conjunction.elim_balanced (map length goal_propss) 

499 
handle THM _ => lost_structure (); 

500 
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

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

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

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

505 
 recover_result [] [] = [] 

506 
 recover_result _ _ = lost_structure (); 

507 
in recover_result propss results end; 

5820  508 

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

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

510 

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

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

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

513 
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

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

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

516 
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

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

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

519 

5820  520 

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

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

522 

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

523 
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

524 
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

525 
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

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

528 

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

529 
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

530 
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

531 
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

532 
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

533 
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

534 

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

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

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

537 
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

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

539 

49866  540 
fun method_error kind pos state = 
541 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  542 

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

543 

5820  544 

545 
(*** structured proof commands ***) 

546 

17112  547 
(** context elements **) 
5820  548 

36324  549 
(* let bindings *) 
5820  550 

16813  551 
local 
552 

17359  553 
fun gen_bind bind args state = 
5820  554 
state 
555 
> assert_forward 

36324  556 
> map_context (bind true args #> snd) 
47068  557 
> reset_facts; 
5820  558 

16813  559 
in 
560 

42360  561 
val let_bind = gen_bind Proof_Context.match_bind_i; 
562 
val let_bind_cmd = gen_bind Proof_Context.match_bind; 

5820  563 

16813  564 
end; 
565 

5820  566 

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

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

568 

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

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

570 

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

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

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

575 

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

576 
fun read_arg ctxt (c, mx) = 
56002  577 
(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

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

579 
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

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

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

582 

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

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

584 

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

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

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

587 

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

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

589 

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

590 

17359  591 
(* fix *) 
9196  592 

12714  593 
local 
594 

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

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

16813  600 
in 
601 

45597  602 
val fix = gen_fix Proof_Context.cert_vars; 
603 
val fix_cmd = gen_fix Proof_Context.read_vars; 

5820  604 

16813  605 
end; 
606 

5820  607 

17359  608 
(* assume etc. *) 
5820  609 

16813  610 
local 
611 

17112  612 
fun gen_assume asm prep_att exp args state = 
5820  613 
state 
614 
> assert_forward 

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

16813  618 
in 
619 

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

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

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

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

625 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  626 

16813  627 
end; 
628 

7271  629 

17359  630 
(* def *) 
11891  631 

16813  632 
local 
633 

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

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

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

643 
> (fn vars => 

644 
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

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

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

647 
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

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

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

16813  653 
in 
654 

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

16813  658 
end; 
659 

11891  660 

8374  661 

17112  662 
(** facts **) 
5820  663 

17359  664 
(* chain *) 
5820  665 

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

17359  669 
val chain = 
670 
assert_forward 

24011  671 
#> clean_facts 
17359  672 
#> enter_chain; 
5820  673 

17359  674 
fun chain_facts facts = 
47068  675 
set_facts facts 
17359  676 
#> chain; 
5820  677 

678 

17359  679 
(* note etc. *) 
17112  680 

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

683 
local 

684 

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

685 
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state = 
17112  686 
state 
687 
> assert_forward 

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

17112  690 
> these_factss (more_facts state) 
17359  691 
> opt_chain 
692 
> opt_result; 

17112  693 

694 
in 

695 

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

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

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

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

17359  702 

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

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

706 

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

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

17112  709 
end; 
710 

711 

18548  712 
(* using/unfolding *) 
17112  713 

714 
local 

715 

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

716 
fun gen_using f g prep_att prep_fact args state = 
17112  717 
state 
718 
> assert_backward 

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

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

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

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

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

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

17112  732 

733 
in 

734 

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

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

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

740 
end; 

741 

742 

743 
(* case *) 

744 

745 
local 

746 

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

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

751 
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

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

753 
asms > map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts)); 
17112  754 
in 
755 
state' 

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

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

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

761 
in 

762 

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

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

766 
end; 

767 

768 

769 

17359  770 
(** proof structure **) 
771 

772 
(* blocks *) 

773 

774 
val begin_block = 

775 
assert_forward 

776 
#> open_block 

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

780 
val next_block = 

781 
assert_forward 

782 
#> close_block 

783 
#> open_block 

47068  784 
#> reset_goal 
785 
#> reset_facts; 

17359  786 

787 
fun end_block state = 

788 
state 

789 
> assert_forward 

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

793 
> close_block 

794 
> export_facts state; 

795 

796 

40960  797 
(* global notepad *) 
798 

799 
val begin_notepad = 

800 
init 

801 
#> open_block 

802 
#> map_context (Variable.set_body true) 

803 
#> open_block; 

804 

805 
val end_notepad = 

806 
assert_forward 

807 
#> assert_bottom true 

808 
#> close_block 

809 
#> assert_current_goal false 

810 
#> close_block 

811 
#> context_of; 

812 

813 

17359  814 
(* subproofs *) 
815 

816 
fun proof opt_text = 

817 
assert_backward 

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

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

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

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

824 

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

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

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

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

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

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

830 
 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

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

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

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

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

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

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

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

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

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

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

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

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

843 
end; 
17359  844 

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

847 
NONE => error msg 

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

849 

17359  850 

851 
(* unstructured refinement *) 

852 

49865  853 
fun defer i = 
854 
assert_no_chain #> 

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

856 

857 
fun prefer i = 

858 
assert_no_chain #> 

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

17359  860 

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

49866  862 

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

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

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

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

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

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

869 
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

870 

17359  871 

872 

17112  873 
(** goals **) 
874 

17359  875 
(* generic goals *) 
876 

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

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

878 

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

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

880 
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

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

882 

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

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

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

887 
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

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

889 

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

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

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

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

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

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

895 

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

896 
in 
17359  897 

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

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

5936  906 
state 
907 
> assert_forward_or_chain 

908 
> enter_forward 

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

911 
val props = flat propss; 
15703  912 

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

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

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

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

917 
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

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

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

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

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

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

936 
fun generic_qed after_ctxt state = 
12503  937 
let 
36354  938 
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

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

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

941 

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

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

943 
flat (tl stmt) 
19915  944 
> Variable.exportT_terms goal_ctxt outer_ctxt; 
17359  945 
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

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

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

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

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

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

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

955 

9469  956 

17359  957 
(* local goals *) 
958 

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

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

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

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

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

49866  974 
fun local_qeds arg = 
975 
end_proof false arg 

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

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

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

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

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

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

5820  982 

17359  983 
(* global goals *) 
984 

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

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

988 

989 
fun global_goal prepp before_qed after_qed propp = 

990 
init #> 

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

17359  992 

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

12065  995 

49866  996 
fun global_qeds arg = 
997 
end_proof true arg 

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

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

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

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

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

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

5820  1004 

49907  1005 
(* terminal proof steps *) 
17112  1006 

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

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

1008 

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

1009 
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

1010 
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

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

1012 

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

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

1014 

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

1016 
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

1017 
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

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

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

1021 
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

1022 
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

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

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

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

1026 

6896  1027 

49907  1028 
(* skip proofs *) 
1029 

1030 
fun local_skip_proof int state = 

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

51551  1032 
Skip_Proof.report (context_of state); 
49907  1033 

1034 
fun global_skip_proof int state = 

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

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

1038 

17359  1039 
(* common goal statements *) 
1040 

1041 
local 

1042 

17859  1043 
fun gen_have prep_att prepp before_qed after_qed stmt int = 
56897
c668735fb8b5
print results as "state", to avoid intrusion into the source text;
wenzelm
parents:
56002
diff
changeset

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

1045 
prep_att prepp "have" before_qed after_qed stmt; 
6896  1046 

17859  1047 
fun gen_show prep_att prepp before_qed after_qed stmt int state = 
17359  1048 
let 
32738  1049 
val testing = Unsynchronized.ref false; 
1050 
val rule = Unsynchronized.ref (NONE: thm option); 

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

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

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

1057 
if ! testing then () 
56897
c668735fb8b5
print results as "state", to avoid intrusion into the source text;
wenzelm
parents:
56002
diff
changeset

1058 
else Proof_Display.print_results int ctxt res; 
17359  1059 
fun print_rule ctxt th = 
1060 
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

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

1062 
writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th)) 
17359  1063 
else (); 
1064 
val test_proof = 

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

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

1066 
> Unsynchronized.setmp testing true 
42042  1067 
> Exn.interruptible_capture; 
6896  1068 

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

1070 
refine_goals print_rule (context_of state) (flat results) 
29383  1071 
#> check_result "Failed to refine any pending goal" 
1072 
#> after_qed results; 

17359  1073 
in 
1074 
state 

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

1078 
Exn.Res _ => goal_state 
42042  1079 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1080 
end; 
1081 

1082 
in 

1083 

42360  1084 
val have = gen_have (K I) Proof_Context.bind_propp_i; 
47815  1085 
val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp; 
42360  1086 
val show = gen_show (K I) Proof_Context.bind_propp_i; 
47815  1087 
val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp; 
6896  1088 

5820  1089 
end; 
17359  1090 

28410  1091 

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

1092 

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

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

1094 

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

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

1096 

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

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

1098 
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

1099 
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

1100 

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

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

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

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

1104 
 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

1105 
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

1106 

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

1107 

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

1108 
(* full proofs *) 
28410  1109 

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

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

1111 

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

1112 
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

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

1114 
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

1115 
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

1116 
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

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

1118 

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

1119 
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

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

1121 
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

1122 
 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

1123 

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

1125 
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

1126 

51318  1127 
in 
1128 

1129 
fun future_proof fork_proof state = 

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

1131 
val _ = assert_backward state; 
28410  1132 
val (goal_ctxt, (_, goal)) = find_goal state; 
32786  1133 
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

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

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

1136 
(prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) []; 
28410  1137 

29383  1138 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1139 

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

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

1141 
val statement' = (kind, [[], [prop']], prop'); 
52456  1142 
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

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

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

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

1146 
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

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

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

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

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

1151 

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

1153 
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

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

1155 
state 
51318  1156 
> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I; 
1157 
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

1158 

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

1160 

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

1161 

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

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

1163 

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

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

1165 

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

1166 
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

1167 
if Goal.future_enabled 3 andalso not (is_relevant state) then 
51318  1168 
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

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

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

1171 
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

1172 
in 
53192  1173 
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

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

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

1177 

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

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

1179 

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

1181 
future_terminal_proof 
51318  1182 
(local_terminal_proof meths) 
1183 
(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

1184 

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

1186 
future_terminal_proof 
51318  1187 
(global_terminal_proof meths) 
1188 
(global_terminal_proof meths) global_done_proof; 

29350  1189 

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

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

1191 

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

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

1193 