author  wenzelm 
Wed, 10 Jun 2015 11:14:04 +0200  
changeset 60411  8f7e1279251d 
parent 60409  240ad53041c9 
child 60414  f25f2f2ba48c 
permissions  rwrr 
5820  1 
(* Title: Pure/Isar/proof.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

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

5820  6 
*) 
7 

8 
signature PROOF = 

9 
sig 

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

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

15 
val assert_bottom: bool > state > state 

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

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

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

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

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

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

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

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

35 
val has_bottom_goal: state > bool 
60403  36 
val pretty_state: 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 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

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

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

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

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

68 
val with_thmss_cmd: ((Facts.ref * Token.src list) list) list > state > state 
60371  69 
val supply: (Thm.binding * (thm list * attribute list) list) list > state > state 
70 
val supply_cmd: (Attrib.binding * (Facts.ref * Token.src list) list) list > state > state 

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

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

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

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

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

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

76 
state > state 
58011
bc6bced136e5
tuned signature  moved type src to Token, without aliases;
wenzelm
parents:
58007
diff
changeset

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

78 
state > state 
17359  79 
val begin_block: state > state 
80 
val next_block: state > state 

20309  81 
val end_block: state > state 
49042  82 
val begin_notepad: context > state 
83 
val end_notepad: state > context 

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

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

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

90 
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

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

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

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

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

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

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

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

101 
val local_skip_proof: bool > state > state 

102 
val local_done_proof: state > state 

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

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

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

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

107 
val global_done_proof: state > context 
60406  108 
val internal_goal: (context > (string * string) * (string * thm list) list > unit) > 
109 
Proof_Context.mode > string > Method.text option > (thm list list > state > state) > 

110 
(binding * typ option * mixfix) list > 

111 
(Thm.binding * (term * term list) list) list > state > state 

29383  112 
val have: Method.text option > (thm list list > state > state) > 
60406  113 
(binding * typ option * mixfix) list > 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

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

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

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

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

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

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

125 
val is_relevant: state > bool 
51318  126 
val future_proof: (state > ('a * context) future) > state > 'a future * state 
60403  127 
val local_future_terminal_proof: Method.text_range * Method.text_range option > state > state 
128 
val global_future_terminal_proof: Method.text_range * Method.text_range option > state > context 

5820  129 
end; 
130 

13377  131 
structure Proof: PROOF = 
5820  132 
struct 
133 

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

134 
type context = Proof.context; 
17112  135 
type method = Method.method; 
16813  136 

5820  137 

138 
(** proof state **) 

139 

17359  140 
(* datatype state *) 
5820  141 

17112  142 
datatype mode = Forward  Chain  Backward; 
5820  143 

17359  144 
datatype state = 
145 
State of node Stack.T 

146 
and node = 

7176  147 
Node of 
148 
{context: context, 

149 
facts: thm list option, 

150 
mode: mode, 

17359  151 
goal: goal option} 
152 
and goal = 

153 
Goal of 

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

154 
{statement: bool * (string * Position.T) * term list list * term, 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

155 
(*regular export, goal kind and statement (starting with vars), initial proposition*) 
25958  156 
using: thm list, (*goal facts*) 
157 
goal: thm, (*subgoals ==> statement*) 

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

161 
(thm list list > context > context)}; 
17359  162 

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

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

164 
Goal {statement = statement, using = using, goal = goal, 
17859  165 
before_qed = before_qed, after_qed = after_qed}; 
5820  166 

7176  167 
fun make_node (context, facts, mode, goal) = 
168 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

169 

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

5820  172 

21727  173 
val init_context = 
42360  174 
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

175 
Proof_Context.map_naming (K Name_Space.local_naming); 
21727  176 

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

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

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

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

12045  183 

5820  184 

185 

186 
(** basic proof state operations **) 

187 

17359  188 
(* block structure *) 
189 

58796  190 
fun open_block (State stack) = State (Stack.push stack); 
17359  191 

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

193 
handle List.Empty => error "Unbalanced block parentheses"; 
17359  194 

58796  195 
fun level (State stack) = Stack.level stack; 
17359  196 

197 
fun assert_bottom b state = 

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

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

17359  201 
else state 
202 
end; 

203 

204 

5820  205 
(* context *) 
206 

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

207 
val context_of = #context o top; 
42360  208 
val theory_of = Proof_Context.theory_of o context_of; 
5820  209 

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

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

211 
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

212 

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

214 
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
5820  215 

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

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

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

221 
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

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

223 

42360  224 
val put_thms = map_context oo Proof_Context.put_thms; 
5820  225 

226 

227 
(* facts *) 

228 

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

229 
val get_facts = #facts o top; 
17359  230 

231 
fun the_facts state = 

232 
(case get_facts state of SOME facts => facts 

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

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

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

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

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

245 

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

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

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

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

257 

258 
(* mode *) 

259 

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

260 
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

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

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

265 
fun assert_mode pred state = 

266 
let val mode = get_mode state in 

267 
if pred mode then state 

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

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

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

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

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

5820  276 

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

279 
val enter_backward = put_mode Backward; 

5820  280 

17359  281 

282 
(* current goal *) 

283 

284 
fun current_goal state = 

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

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

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

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

17359  293 
else state 
294 
end; 

6776  295 

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

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

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

300 

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

17359  303 

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

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

305 

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

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

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

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

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

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

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

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

313 

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

314 

17359  315 
(* nested goal *) 
5820  316 

58797  317 
fun map_goal f g h (State stack) = 
318 
(case Stack.dest stack of 

319 
(Node {context, facts, mode, goal = SOME goal}, node :: nodes) => 

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

321 
val Goal {statement, using, goal, before_qed, after_qed} = goal; 
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

322 
val goal' = make_goal (g (statement, using, goal, before_qed, after_qed)); 
47431
d9dd4a9f18fc
more precise declaration of goal_tfrees in forked proof state;
wenzelm
parents:
47416
diff
changeset

323 
val node' = map_node_context h node; 
58797  324 
val stack' = Stack.make (make_node (f context, facts, mode, SOME goal')) (node' :: nodes); 
325 
in State stack' end 

326 
 (nd, node :: nodes) => 

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

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

328 
val nd' = map_node_context f nd; 
58797  329 
val State stack' = map_goal f g h (State (Stack.make node nodes)); 
330 
val (node', nodes') = Stack.dest stack'; 

331 
in State (Stack.make nd' (node' :: nodes')) end 

332 
 _ => State stack); 

5820  333 

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

334 
fun provide_goal goal = map_goal I (fn (statement, using, _, before_qed, after_qed) => 
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

335 
(statement, using, goal, before_qed, after_qed)) I; 
19188  336 

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

337 
fun using_facts using = map_goal I (fn (statement, _, goal, before_qed, after_qed) => 
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

338 
(statement, using, goal, before_qed, after_qed)) I; 
17359  339 

340 
local 

341 
fun find i state = 

342 
(case try current_goal state of 

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

60094  344 
 NONE => find (i + 1) (close_block state handle ERROR _ => error "No proof goal")); 
17359  345 
in val find_goal = find 0 end; 
346 

347 
fun get_goal state = 

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

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

5820  350 

351 

352 

12423  353 
(** pretty_state **) 
5820  354 

59185  355 
local 
356 

15531  357 
fun pretty_facts _ _ NONE = [] 
59185  358 
 pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths]; 
359 

360 
fun pretty_sep prts [] = prts 

361 
 pretty_sep [] prts = prts 

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

363 

364 
in 

6756  365 

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

368 
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

369 
val verbose = Config.get ctxt Proof_Context.verbose; 
5820  370 

60403  371 
fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) = 
59185  372 
pretty_sep 
373 
(pretty_facts ctxt "using" 

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

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

17359  376 
 prt_goal NONE = []; 
6848  377 

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

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

382 

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

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

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

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

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

390 
(if verbose orelse mode = Forward then 
59185  391 
pretty_sep (pretty_facts ctxt "" facts) (prt_goal (try find_goal state)) 
51584  392 
else if mode = Chain then pretty_facts ctxt "picking" facts 
17359  393 
else prt_goal (try find_goal state)) 
394 
end; 

5820  395 

59185  396 
end; 
397 

5820  398 

399 

400 
(** proof steps **) 

401 

17359  402 
(* refine via method *) 
5820  403 

8234  404 
local 
405 

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

408 

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

410 

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

16146  413 

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

414 
fun apply_method text ctxt state = 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

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

416 
Method.evaluate text ctxt using goal 
58004  417 
> Seq.map (fn (meth_cases, goal') => 
6848  418 
state 
16146  419 
> map_goal 
59970  420 
(Proof_Context.update_cases false (no_goal_cases goal @ goal_cases ctxt goal') #> 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

421 
Proof_Context.update_cases true meth_cases) 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

422 
(K (statement, using, goal', before_qed, after_qed)) I)); 
5820  423 

8234  424 
in 
425 

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

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

427 
fun refine_end text state = apply_method text (#1 (find_goal state)) state; 
58004  428 

429 
fun refine_insert ths = 

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

18908  431 

8234  432 
end; 
433 

5820  434 

17359  435 
(* refine via subproof *) 
436 

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

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

438 

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

439 
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

440 
 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

441 
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

442 
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

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

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

445 
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

446 

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

447 
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

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

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

450 
finish_tac ctxt (Thm.nprems_of rule); 
11816  451 

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

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

453 
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

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

455 

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

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

457 

19915  458 
fun refine_goals print_rule inner raw_rules state = 
459 
let 

460 
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

461 
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac outer rule) st); 
19915  462 
in 
463 
raw_rules 

42360  464 
> Proof_Context.goal_export inner outer 
47068  465 
> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state) 
19915  466 
end; 
17359  467 

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

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

469 

6932  470 

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

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

472 

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

473 
fun conclude_goal ctxt goal propss = 
5820  474 
let 
42360  475 
val thy = Proof_Context.theory_of ctxt; 
5820  476 

54981  477 
val _ = 
59582  478 
Theory.subthy (Thm.theory_of_thm goal, thy) orelse 
479 
error "Bad background theory of goal state"; 

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

481 

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

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

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

484 
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

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

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

487 
> Drule.flexflex_unique (SOME ctxt) 
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 
> 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

489 
> Thm.check_hyps (Context.Proof ctxt); 
23418  490 

491 
val goal_propss = filter_out null propss; 

492 
val results = 

493 
Conjunction.elim_balanced (length goal_propss) th 

494 
> map2 Conjunction.elim_balanced (map length goal_propss) 

495 
handle THM _ => lost_structure (); 

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

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

497 
Unify.matches_list (Context.Proof ctxt) (flat goal_propss) (map Thm.prop_of (flat results)) 
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58892
diff
changeset

498 
orelse error ("Proved a different theorem:\n" ^ Display.string_of_thm ctxt th); 
23418  499 

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

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

502 
 recover_result [] [] = [] 

503 
 recover_result _ _ = lost_structure (); 

504 
in recover_result propss results end; 

5820  505 

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

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

507 

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

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

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

510 
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

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

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

513 
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

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

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

516 

5820  517 

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

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

519 

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

520 
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

521 
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

522 
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

523 

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

525 

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

527 
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

528 
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

529 
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

530 
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

531 

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

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

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

534 
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

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

536 

49866  537 
fun method_error kind pos state = 
538 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  539 

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

540 

5820  541 

542 
(*** structured proof commands ***) 

543 

17112  544 
(** context elements **) 
5820  545 

36324  546 
(* let bindings *) 
5820  547 

16813  548 
local 
549 

17359  550 
fun gen_bind bind args state = 
5820  551 
state 
552 
> assert_forward 

36324  553 
> map_context (bind true args #> snd) 
47068  554 
> reset_facts; 
5820  555 

16813  556 
in 
557 

60377  558 
val let_bind = gen_bind Proof_Context.match_bind; 
559 
val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd; 

5820  560 

16813  561 
end; 
562 

5820  563 

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

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

565 

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

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

567 

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

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

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

572 

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

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

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

576 
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

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

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

579 

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

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

581 

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

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

583 
val write_cmd = gen_write read_arg; 
36505
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 
end; 
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

586 

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

587 

17359  588 
(* fix *) 
9196  589 

12714  590 
local 
591 

60379  592 
fun gen_fix prep_var args = 
17359  593 
assert_forward 
60379  594 
#> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (fold_map prep_var args ctxt)) ctxt)) 
47068  595 
#> reset_facts; 
5820  596 

16813  597 
in 
598 

60379  599 
val fix = gen_fix Proof_Context.cert_var; 
600 
val fix_cmd = gen_fix Proof_Context.read_var; 

5820  601 

16813  602 
end; 
603 

5820  604 

17359  605 
(* assume etc. *) 
5820  606 

16813  607 
local 
608 

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

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

16813  615 
in 
616 

60377  617 
val assm = gen_assume Proof_Context.add_assms (K I); 
618 
val assm_cmd = gen_assume Proof_Context.add_assms_cmd Attrib.attribute_cmd; 

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

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

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

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

622 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  623 

16813  624 
end; 
625 

7271  626 

17359  627 
(* def *) 
11891  628 

16813  629 
local 
630 

60379  631 
fun gen_def prep_att prep_var prep_binds args state = 
11891  632 
let 
633 
val _ = assert_forward state; 

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

641 
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

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

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

644 
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

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

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

16813  650 
in 
651 

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

11891  654 

16813  655 
end; 
656 

11891  657 

8374  658 

17112  659 
(** facts **) 
5820  660 

17359  661 
(* chain *) 
5820  662 

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

17359  666 
val chain = 
667 
assert_forward 

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

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

675 

17359  676 
(* note etc. *) 
17112  677 

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

680 
local 

681 

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

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

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

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

17112  690 

691 
in 

692 

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

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

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

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

17359  699 

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

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

703 

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

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

17112  706 
end; 
707 

708 

60371  709 
(* facts during goal refinement *) 
710 

711 
local 

712 

713 
fun gen_supply prep_att prep_fact args state = 

714 
state 

715 
> assert_backward 

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

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

718 

719 
in 

720 

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

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

723 

724 
end; 

725 

726 

18548  727 
(* using/unfolding *) 
17112  728 

729 
local 

730 

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

731 
fun gen_using f g prep_att prep_fact args state = 
17112  732 
state 
733 
> assert_backward 

21442  734 
> map_context_result 
47815  735 
(fn ctxt => ctxt > Proof_Context.note_thmss "" 
736 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args))) 

18843  737 
> (fn (named_facts, state') => 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

738 
state' > map_goal I (fn (statement, using, goal, before_qed, after_qed) => 
18843  739 
let 
740 
val ctxt = context_of state'; 

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

741 
val ths = maps snd named_facts; 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

742 
in (statement, f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I); 
18548  743 

24050  744 
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 
35624  745 
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 
746 
val unfold_goals = Local_Defs.unfold_goals; 

17112  747 

748 
in 

749 

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

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

752 
val unfolding = gen_using unfold_using unfold_goals (K I) (K I); 
47815  753 
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact; 
17112  754 

755 
end; 

756 

757 

758 
(* case *) 

759 

760 
local 

761 

57486
2131b6633529
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
wenzelm
parents:
56933
diff
changeset

762 
fun gen_invoke_case internal prep_att ((name, pos), xs, raw_atts) state = 
17112  763 
let 
47815  764 
val atts = map (prep_att (context_of state)) raw_atts; 
19078  765 
val (asms, state') = state > map_context_result (fn ctxt => 
57486
2131b6633529
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
wenzelm
parents:
56933
diff
changeset

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

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

768 
asms > map (fn (b, ts) => ((Binding.set_pos pos b, atts), map (rpair []) ts)); 
17112  769 
in 
770 
state' 

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

771 
> assume assumptions 
60401  772 
> map_context (fold Variable.unbind_term Auto_Bind.no_facts) 
53378
07990ba8c0ea
cases: more position information and PIDE markup;
wenzelm
parents:
53192
diff
changeset

773 
> `the_facts > (fn thms => note_thmss [((Binding.make (name, pos), []), [(thms, [])])]) 
17112  774 
end; 
775 

776 
in 

777 

57486
2131b6633529
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
wenzelm
parents:
56933
diff
changeset

778 
val invoke_case = gen_invoke_case true (K I); 
2131b6633529
check 'case' variable bindings as for 'fix', which means internal names are rejected as usual;
wenzelm
parents:
56933
diff
changeset

779 
val invoke_case_cmd = gen_invoke_case false Attrib.attribute_cmd; 
17112  780 

781 
end; 

782 

783 

784 

17359  785 
(** proof structure **) 
786 

787 
(* blocks *) 

788 

789 
val begin_block = 

790 
assert_forward 

791 
#> open_block 

47068  792 
#> reset_goal 
17359  793 
#> open_block; 
794 

795 
val next_block = 

796 
assert_forward 

797 
#> close_block 

798 
#> open_block 

47068  799 
#> reset_goal 
800 
#> reset_facts; 

17359  801 

802 
fun end_block state = 

803 
state 

804 
> assert_forward 

40960  805 
> assert_bottom false 
17359  806 
> close_block 
807 
> assert_current_goal false 

808 
> close_block 

809 
> export_facts state; 

810 

811 

40960  812 
(* global notepad *) 
813 

814 
val begin_notepad = 

815 
init 

816 
#> open_block 

817 
#> map_context (Variable.set_body true) 

818 
#> open_block; 

819 

820 
val end_notepad = 

821 
assert_forward 

822 
#> assert_bottom true 

823 
#> close_block 

824 
#> assert_current_goal false 

825 
#> close_block 

826 
#> context_of; 

827 

828 

17359  829 
(* subproofs *) 
830 

831 
fun proof opt_text = 

832 
assert_backward 

17859  833 
#> refine (the_default Method.default_text opt_text) 
17359  834 
#> Seq.map (using_facts [] #> enter_forward); 
835 

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

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

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

839 

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

840 
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

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

842 
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

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

844 
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

845 
 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

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

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

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

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

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

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

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

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

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

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

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

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

858 
end; 
17359  859 

29383  860 
fun check_result msg sq = 
861 
(case Seq.pull sq of 

862 
NONE => error msg 

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

864 

17359  865 

866 
(* unstructured refinement *) 

867 

49865  868 
fun defer i = 
869 
assert_no_chain #> 

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

871 

872 
fun prefer i = 

873 
assert_no_chain #> 

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

17359  875 

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

49866  877 

17359  878 
fun apply_end text = assert_forward #> refine_end text; 
879 

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

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

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

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

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

884 
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

885 

17359  886 

887 

17112  888 
(** goals **) 
889 

17359  890 
(* generic goals *) 
891 

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

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

893 

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

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

895 
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

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

897 

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

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

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

902 
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

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

904 

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

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

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

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

910 

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

911 
in 
17359  912 

60406  913 
fun generic_goal kind before_qed after_qed make_statement state = 
5820  914 
let 
17359  915 
val chaining = can assert_chain state; 
25958  916 
val pos = Position.thread_data (); 
17359  917 

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

918 
val ((propss, result_binds), goal_state) = 
5936  919 
state 
920 
> assert_forward_or_chain 

921 
> enter_forward 

17359  922 
> open_block 
60406  923 
> map_context_result make_statement; 
60402  924 
val props = flat propss; 
60383  925 
val goal_ctxt = context_of goal_state; 
15703  926 

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

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

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

930 
val goal = 
59616  931 
Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss) 
60406  932 
> Thm.cterm_of goal_ctxt 
60383  933 
> Thm.weaken_sorts (Variable.sorts_of goal_ctxt); 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

934 
val statement = (true, (kind, pos), propss', Thm.term_of goal); 
60402  935 

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

937 
map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); 
5820  938 
in 
17359  939 
goal_state 
21727  940 
> map_context (init_context #> Variable.set_body true) 
58892
20aa19ecf2cc
eliminated obsolete Proof.goal_message  print outcome more directly;
wenzelm
parents:
58837
diff
changeset

941 
> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed')) 
42360  942 
> map_context (Proof_Context.auto_bind_goal props) 
21565  943 
> chaining ? (`the_facts #> using_facts) 
47068  944 
> reset_facts 
17359  945 
> open_block 
47068  946 
> reset_goal 
5820  947 
> enter_backward 
23418  948 
> 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

949 
> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd) 
5820  950 
end; 
951 

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

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

953 
let 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

954 
val (goal_ctxt, {statement, goal, after_qed, ...}) = current_goal state; 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

955 
val (regular_export, _, propss, _) = statement; 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

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

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

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

959 
> `(fn outer_state => 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

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

961 
val results = 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

962 
tl (conclude_goal goal_ctxt goal propss) 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

963 
> regular_export ? burrow (Proof_Context.export goal_ctxt (context_of outer_state)); 
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

964 
in (after_qed, results) end) 
17359  965 
end; 
966 

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

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

968 

9469  969 

17359  970 
(* local goals *) 
971 

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

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

973 

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

974 
fun export_binds ctxt' ctxt binds = 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

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

976 
val rhss = 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

977 
map (the_list o snd) binds 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

978 
> burrow (Variable.export_terms ctxt' ctxt) 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

979 
> map (try the_single); 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

980 
in map fst binds ~~ rhss end; 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

981 

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

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

983 

60406  984 
fun local_goal print_results prep_att prep_propp prep_var 
985 
kind before_qed after_qed fixes stmt state = 

17359  986 
let 
21362
3a2ab1dce297
simplified Proof.theorem(_i) interface  removed target support;
wenzelm
parents:
21274
diff
changeset

987 
val ((names, attss), propp) = 
47815  988 
Attrib.map_specs (map (prep_att (context_of state))) stmt > split_list >> split_list; 
17359  989 

60406  990 
fun make_statement ctxt = 
60402  991 
let 
60406  992 
val ((xs', vars), fix_ctxt) = ctxt 
993 
> fold_map prep_var fixes 

994 
> (fn vars => Proof_Context.add_fixes vars ##>> pair vars); 

995 

996 
val (propss, binds) = prep_propp fix_ctxt propp; 

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

997 
val props = flat propss; 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

998 

60407  999 
val (ps, params_ctxt) = fix_ctxt 
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1000 
> fold Variable.declare_term props 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1001 
> fold Variable.bind_term binds 
60406  1002 
> fold_map Proof_Context.inferred_param xs'; 
1003 

1004 
val xs = map (Variable.check_name o #1) vars; 

60407  1005 
val params = xs ~~ map Free ps; 
60406  1006 

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

1007 
val binds' = 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1008 
(case try List.last props of 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1009 
NONE => [] 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1010 
 SOME prop => map (apsnd (SOME o Auto_Bind.abs_params prop)) binds); 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1011 
val result_binds = 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1012 
(Auto_Bind.facts params_ctxt props @ binds') 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1013 
> (map o apsnd o Option.map) (fold_rev Term.dependent_lambda_name params) 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1014 
> export_binds params_ctxt ctxt; 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1015 

60406  1016 
val _ = Variable.warn_extra_tfrees fix_ctxt params_ctxt; 
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1017 

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

1018 
in ((propss, result_binds), params_ctxt) end; 
60402  1019 

18124  1020 
fun after_qed' results = 
18808  1021 
local_results ((names ~~ attss) ~~ results) 
17359  1022 
#> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) 
18124  1023 
#> after_qed results; 
60406  1024 
in generic_goal kind before_qed (after_qed', K I) make_statement state end; 
5820  1025 

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

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

1027 

49866  1028 
fun local_qeds arg = 
1029 
end_proof false arg 

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

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

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

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

1033 
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
29383  1034 

5820  1035 

17359  1036 
(* global goals *) 
1037 

60388  1038 
fun global_goal prep_propp before_qed after_qed propp = 
60402  1039 
let 
60406  1040 
fun make_statement ctxt = 
60402  1041 
let 
1042 
val (propss, binds) = 

60406  1043 
prep_propp (Proof_Context.set_mode Proof_Context.mode_schematic ctxt) propp; 
1044 
val ctxt' = ctxt 

60402  1045 
> (fold o fold) Variable.auto_fixes propss 
60408
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1046 
> fold Variable.bind_term binds; 
1fd46ced2fa8
more uniform treatment of auto bindings vs. explicit user bindings;
wenzelm
parents:
60407
diff
changeset

1047 
in ((propss, []), ctxt') end; 
60406  1048 
in init #> generic_goal "" before_qed (K I, after_qed) make_statement end; 
45327  1049 

60388  1050 
val theorem = global_goal Proof_Context.cert_propp; 
1051 
val theorem_cmd = global_goal Proof_Context.read_propp; 

12065  1052 

49866  1053 
fun global_qeds arg = 
1054 
end_proof true arg 

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

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

1056 
after_qed results (context_of state))); 
17112  1057 

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

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

1059 
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
12959  1060 

5820  1061 

49907  1062 
(* terminal proof steps *) 
17112  1063 

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

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

1065 

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

1066 
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

1067 
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

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

1069 

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

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

1071 

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

1073 
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

1074 
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

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

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

1078 
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

1079 
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

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

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

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

1083 

6896  1084 

49907  1085 
(* skip proofs *) 
1086 

1087 
fun local_skip_proof int state = 

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

51551  1089 
Skip_Proof.report (context_of state); 
49907  1090 

1091 
fun global_skip_proof int state = 

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

51551  1093 
Skip_Proof.report (context_of state); 
49907  1094 

1095 

17359  1096 
(* common goal statements *) 
1097 

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

1100 
Proof_Context.cert_var; 

1101 

17359  1102 
local 
1103 

60406  1104 
fun gen_have prep_att prep_propp prep_var 
1105 
before_qed after_qed fixes stmt int = 

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

1106 
local_goal (Proof_Display.print_results int (Position.thread_data ())) 
60406  1107 
prep_att prep_propp prep_var "have" before_qed after_qed fixes stmt; 
6896  1108 

60406  1109 
fun gen_show prep_att prep_propp prep_var 
1110 
before_qed after_qed fixes stmt int state = 

17359  1111 
let 
32738  1112 
val testing = Unsynchronized.ref false; 
1113 
val rule = Unsynchronized.ref (NONE: thm option); 

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

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

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

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

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

1122 
else Proof_Display.print_results int pos ctxt res; 
17359  1123 
fun print_rule ctxt th = 
1124 
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

1125 
else if int then 
56933  1126 
Proof_Display.string_of_rule ctxt "Successful" th 
1127 
> Markup.markup Markup.text_fold 

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

1128 
> Output.state 
17359  1129 
else (); 
1130 
val test_proof = 

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

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

1132 
> Unsynchronized.setmp testing true 
42042  1133 
> Exn.interruptible_capture; 
6896  1134 

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

1136 
refine_goals print_rule (context_of state) (flat results) 
29383  1137 
#> check_result "Failed to refine any pending goal" 
1138 
#> after_qed results; 

17359  1139 
in 
1140 
state 

60406  1141 
> local_goal print_results prep_att prep_propp prep_var 
1142 
"show" before_qed after_qed' fixes stmt 

21565  1143 
> int ? (fn goal_state => 
49907  1144 
(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

1145 
Exn.Res _ => goal_state 
42042  1146 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1147 
end; 
1148 

1149 
in 

1150 

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

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

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

6896  1155 

5820  1156 
end; 
17359  1157 

28410  1158 

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

1159 

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

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

1161 

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

1162 
(* relevant proof states *) 
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 
fun schematic_goal state = 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

1165 
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

1166 
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

1167 

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

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

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

1170 
NONE => true 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

1171 
 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

1172 
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

1173 

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

1174 

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

1175 
(* full proofs *) 
28410  1176 

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

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

1178 

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

1179 
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

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

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

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

1184 

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

1185 
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

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

1187 
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

1188 
 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

1189 

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

1190 
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

1191 
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

1192 

51318  1193 
in 
1194 

1195 
fun future_proof fork_proof state = 

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

1197 
val _ = assert_backward state; 
60409
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

1198 
val (goal_ctxt, (_, goal_info)) = find_goal state; 
240ad53041c9
prevent export of future result  avoid interference with goal fixes;
wenzelm
parents:
60408
diff
changeset

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

29383  1201 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1202 

60411  1203 
val statement' = (false, kind, [[], [prop]], prop); 
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

1204 
val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th); 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

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

1206 
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

1207 
> map_context reset_result 
60411  1208 
> map_goal I (K (statement', using, goal, before_qed, after_qed')) I 
29346
fe6843aa4f5f
more precise is_relevant: requires original main goal, not initial goal state;
wenzelm
parents:
29090
diff
changeset

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

1210 

51318  1211 
val future_thm = Future.map (the_result o snd) result_ctxt; 
60411  1212 
val finished_goal = Goal.protect 0 (Goal.future_result goal_ctxt future_thm prop); 
28973
c549650d1442
future proofs: pass actual futures to facilitate composite computations;
wenzelm
parents:
28627
diff
changeset

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

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

1215 
> map_goal I (K (statement, using, finished_goal, NONE, after_qed)) I; 
51318  1216 
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

1217 

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

1219 

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

1220 

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

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

1222 

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

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

1224 

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

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

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

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

1230 
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

1231 
in 
53192  1232 
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

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

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

1236 

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

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

1238 

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

1240 
future_terminal_proof 
51318  1241 
(local_terminal_proof meths) 
1242 
(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

1243 

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

1245 
future_terminal_proof 
51318  1246 
(global_terminal_proof meths) 
1247 
(global_terminal_proof meths) global_done_proof; 

29350  1248 

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

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

1250 

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

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

1252 