author  wenzelm 
Fri, 08 Dec 2017 14:39:52 +0100  
changeset 67161  b762ed417ed9 
parent 67157  d0657c8b7616 
child 67522  9e712280cc37 
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 
63541  22 
val report_improper: state > unit 
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 

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

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

35 
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

36 
val has_bottom_goal: state > bool 
60623  37 
val using_facts: thm list > state > state 
60403  38 
val pretty_state: state > Pretty.T list 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

39 
val refine: Method.text > state > state Seq.result Seq.seq 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

40 
val refine_end: Method.text > state > state Seq.result Seq.seq 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

41 
val refine_singleton: Method.text > state > state 
18908  42 
val refine_insert: thm list > state > state 
60623  43 
val refine_primitive: (Proof.context > thm > thm) > state > state 
33288
bd3f30da7bc1
replaced slightly odd get_goal/flat_goal by explicit goal views that correspond to the usual method categories;
wenzelm
parents:
33165
diff
changeset

44 
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

45 
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

46 
val simple_goal: state > {context: context, goal: thm} 
36323
655e2d74de3a
modernized naming conventions of main Isar proof elements;
wenzelm
parents:
36322
diff
changeset

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

48 
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

49 
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

50 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

70 
state > state 
17359  71 
val chain: state > state 
72 
val chain_facts: thm list > state > state 

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

73 
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

74 
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

75 
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

76 
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

77 
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

78 
val with_thmss_cmd: ((Facts.ref * Token.src list) list) list > state > state 
60371  79 
val supply: (Thm.binding * (thm list * attribute list) list) list > state > state 
80 
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

81 
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

82 
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

83 
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

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

63039  87 
val define: (binding * typ option * mixfix) list > 
88 
(binding * typ option * mixfix) list > 

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

90 
val define_cmd: (binding * string option * mixfix) list > 

91 
(binding * string option * mixfix) list > 

92 
(Attrib.binding * (string * string list) list) list > state > state 

17359  93 
val begin_block: state > state 
94 
val next_block: state > state 

20309  95 
val end_block: state > state 
49042  96 
val begin_notepad: context > state 
97 
val end_notepad: state > context 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

98 
val proof: Method.text_range option > state > state Seq.result Seq.seq 
49865  99 
val defer: int > state > state 
100 
val prefer: int > state > state 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

101 
val apply: Method.text_range > state > state Seq.result Seq.seq 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

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

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

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

106 
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

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

108 
val global_qed: Method.text_range option * bool > state > context 
67157  109 
val schematic_goal: state > bool 
110 
val is_relevant: state > bool 

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

111 
val local_terminal_proof: Method.text_range * Method.text_range option > state > state 
29383  112 
val local_default_proof: state > state 
113 
val local_immediate_proof: state > state 

114 
val local_skip_proof: bool > state > state 

115 
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

116 
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

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

118 
val global_immediate_proof: state > context 
29383  119 
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

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

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

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

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

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

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

139 
val show_cmd: bool > Method.text option > (context * thm list list > state > state) > 
60406  140 
(binding * string option * mixfix) list > 
60414  141 
(Attrib.binding * (string * string list) list) list > 
60461  142 
(Attrib.binding * (string * string list) list) list > bool > state > thm list * state 
51318  143 
val future_proof: (state > ('a * context) future) > state > 'a future * state 
60403  144 
val local_future_terminal_proof: Method.text_range * Method.text_range option > state > state 
145 
val global_future_terminal_proof: Method.text_range * Method.text_range option > state > context 

5820  146 
end; 
147 

13377  148 
structure Proof: PROOF = 
5820  149 
struct 
150 

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

151 
type context = Proof.context; 
17112  152 
type method = Method.method; 
16813  153 

5820  154 

155 
(** proof state **) 

156 

17359  157 
(* datatype state *) 
5820  158 

17112  159 
datatype mode = Forward  Chain  Backward; 
5820  160 

17359  161 
datatype state = 
162 
State of node Stack.T 

163 
and node = 

7176  164 
Node of 
165 
{context: context, 

63541  166 
facts: (thm list * bool) option, 
7176  167 
mode: mode, 
17359  168 
goal: goal option} 
169 
and goal = 

170 
Goal of 

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

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

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

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

17359  179 

62663  180 
val _ = 
62819
d3ff367a16a0
careful export of typedependent functions, without losing their special status;
wenzelm
parents:
62773
diff
changeset

181 
ML_system_pp (fn _ => fn _ => fn _: state => 
62663  182 
Pretty.to_polyml (Pretty.str "<Proof.state>")); 
183 

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

184 
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

185 
Goal {statement = statement, using = using, goal = goal, 
17859  186 
before_qed = before_qed, after_qed = after_qed}; 
5820  187 

7176  188 
fun make_node (context, facts, mode, goal) = 
189 
Node {context = context, facts = facts, mode = mode, goal = goal}; 

190 

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

5820  193 

21727  194 
val init_context = 
42360  195 
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

196 
Proof_Context.map_naming (K Name_Space.local_naming); 
21727  197 

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

198 
fun init ctxt = 
21727  199 
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE))); 
5820  200 

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

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

12045  204 

5820  205 

206 

207 
(** basic proof state operations **) 

208 

17359  209 
(* block structure *) 
210 

58796  211 
fun open_block (State stack) = State (Stack.push stack); 
17359  212 

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

214 
handle List.Empty => error "Unbalanced block parentheses"; 
17359  215 

58796  216 
fun level (State stack) = Stack.level stack; 
17359  217 

218 
fun assert_bottom b state = 

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

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

17359  222 
else state 
223 
end; 

224 

225 

5820  226 
(* context *) 
227 

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

228 
val context_of = #context o top; 
42360  229 
val theory_of = Proof_Context.theory_of o context_of; 
5820  230 

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

232 
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal)); 
5820  233 

17359  234 
fun map_context_result f state = 
17859  235 
f (context_of state) > (fn ctxt => map_context (K ctxt) state); 
5820  236 

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

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

239 
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

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

241 

5820  242 

243 
(* facts *) 

244 

63541  245 
fun report_improper state = 
246 
Context_Position.report (context_of state) (Position.thread_data ()) Markup.improper; 

247 

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

248 
val get_facts = #facts o top; 
17359  249 

250 
fun the_facts state = 

60550  251 
(case get_facts state of 
63541  252 
SOME (facts, proper) => (if proper then () else report_improper state; facts) 
18678  253 
 NONE => error "No current facts available"); 
5820  254 

9469  255 
fun the_fact state = 
60550  256 
(case the_facts state of 
257 
[thm] => thm 

18678  258 
 _ => error "Single theorem expected"); 
7605  259 

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

261 
map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #> 
63541  262 
map_context (Proof_Context.put_thms index (Auto_Bind.thisN, Option.map #1 facts)); 
263 

264 
fun set_facts thms = put_facts false (SOME (thms, true)); 

265 
val reset_facts = put_facts false NONE; 

5820  266 

63541  267 
fun improper_reset_facts state = 
268 
(case get_facts state of 

269 
SOME (thms, _) => put_facts false (SOME (thms, false)) state 

270 
 NONE => state); 

47068  271 

17359  272 
fun these_factss more_facts (named_factss, state) = 
47068  273 
(named_factss, state > set_facts (maps snd named_factss @ more_facts)); 
5820  274 

17359  275 
fun export_facts inner outer = 
276 
(case get_facts inner of 

47068  277 
NONE => reset_facts outer 
63541  278 
 SOME (thms, proper) => 
279 
let val thms' = Proof_Context.export (context_of inner) (context_of outer) thms 

280 
in put_facts true (SOME (thms', proper)) outer end); 

5820  281 

282 

283 
(* mode *) 

284 

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

285 
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

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

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

290 
fun assert_mode pred state = 

291 
let val mode = get_mode state in 

292 
if pred mode then state 

18678  293 
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode") 
5820  294 
end; 
295 

19308  296 
val assert_forward = assert_mode (fn mode => mode = Forward); 
297 
val assert_chain = assert_mode (fn mode => mode = Chain); 

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

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

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

5820  301 

17359  302 
val enter_forward = put_mode Forward; 
303 
val enter_chain = put_mode Chain; 

304 
val enter_backward = put_mode Backward; 

5820  305 

17359  306 

307 
(* current goal *) 

308 

309 
fun current_goal state = 

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

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

311 
{context = ctxt, goal = SOME (Goal goal), ...} => (ctxt, goal) 
47065  312 
 _ => error "No current goal"); 
5820  313 

17359  314 
fun assert_current_goal g state = 
315 
let val g' = can current_goal state in 

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

17359  318 
else state 
319 
end; 

6776  320 

63249  321 
fun put_goal goal = map_top (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal)); 
17359  322 

47068  323 
val set_goal = put_goal o SOME; 
324 
val reset_goal = put_goal NONE; 

325 

17859  326 
val before_qed = #before_qed o #2 o current_goal; 
327 

17359  328 

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

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

330 

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

331 
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

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

333 
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

334 
 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

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

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

337 
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

338 

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

339 

17359  340 
(* nested goal *) 
5820  341 

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

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

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

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

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

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

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

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

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

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

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

355 
in State (Stack.make top_node (node' :: nodes')) end 
58797  356 
 _ => State stack); 
5820  357 

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

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

360 
(ctxt, statement, using, goal, before_qed, after_qed)); 
19188  361 

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

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

364 
(ctxt, statement, using, goal, before_qed, after_qed)); 
17359  365 

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

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

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

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

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

371 
fun get_goal state = 

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

372 
let val (ctxt, {using, goal, ...}) = find_goal state 
17359  373 
in (ctxt, (using, goal)) end; 
5820  374 

375 

376 

12423  377 
(** pretty_state **) 
5820  378 

59185  379 
local 
380 

15531  381 
fun pretty_facts _ _ NONE = [] 
59185  382 
 pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths]; 
383 

384 
fun pretty_sep prts [] = prts 

385 
 pretty_sep [] prts = prts 

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

387 

388 
in 

6756  389 

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

392 
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

393 
val verbose = Config.get ctxt Proof_Context.verbose; 
5820  394 

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

395 
fun prt_goal (SOME (_, {statement = _, using, goal, before_qed = _, after_qed = _})) = 
59185  396 
pretty_sep 
397 
(pretty_facts ctxt "using" 

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

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

17359  400 
 prt_goal NONE = []; 
6848  401 

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

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

406 

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

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

409 
[Pretty.block 
60551  410 
[Pretty.mark_str (position_markup, "proof"), Pretty.str (" (" ^ mode_name mode ^ ")")]] @ 
17359  411 
(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

412 
(if verbose orelse mode = Forward then 
63541  413 
pretty_sep (pretty_facts ctxt "" (Option.map #1 facts)) (prt_goal (try find_goal state)) 
414 
else if mode = Chain then pretty_facts ctxt "picking" (Option.map #1 facts) 

17359  415 
else prt_goal (try find_goal state)) 
416 
end; 

5820  417 

59185  418 
end; 
419 

5820  420 

421 

422 
(** proof steps **) 

423 

17359  424 
(* refine via method *) 
5820  425 

8234  426 
local 
427 

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

430 

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

432 

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

16146  435 

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

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

437 
find_goal state > (fn (goal_ctxt, {statement, using, goal, before_qed, after_qed}) => 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

438 
Method.evaluate text ctxt using (goal_ctxt, goal) 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

439 
> Seq.map_result (fn (goal_ctxt', goal') => 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

440 
let 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

441 
val goal_ctxt'' = goal_ctxt' 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

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

443 
val state' = state 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

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

445 
in state' end)); 
5820  446 

8234  447 
in 
448 

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

449 
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

450 
fun refine_end text state = apply_method text (#1 (find_goal state)) state; 
58004  451 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

452 
fun refine_singleton text = refine text #> Seq.the_result ""; 
18908  453 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

454 
fun refine_insert ths = 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

455 
refine_singleton (Method.Basic (K (Method.insert ths))); 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

456 

4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

457 
fun refine_primitive r = 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

458 
refine_singleton (Method.Basic (fn ctxt => fn _ => Method.CONTEXT_TACTIC (PRIMITIVE (r ctxt)))); 
60623  459 

8234  460 
end; 
461 

5820  462 

17359  463 
(* refine via subproof *) 
464 

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

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

466 

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

467 
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

468 
 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

469 
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

470 
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

471 
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

472 
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

473 
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

474 

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

475 
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

476 
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

477 
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

478 
finish_tac ctxt (Thm.nprems_of rule); 
11816  479 

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

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

481 
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

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

483 

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

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

487 
> Seq.hd; 

488 

489 
fun protect_prems th = 

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

491 

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

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

493 

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

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

496 
val (goal_ctxt, (_, goal)) = get_goal state; 
60550  497 
fun refine rule st = 
498 
(print_rule goal_ctxt rule; FINDGOAL (goal_tac goal_ctxt rule) st); 

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

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

502 
> Proof_Context.goal_export result_ctxt goal_ctxt 
47068  503 
> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state) 
19915  504 
end; 
17359  505 

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

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

507 

6932  508 

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

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

510 

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

511 
fun conclude_goal ctxt goal propss = 
5820  512 
let 
42360  513 
val thy = Proof_Context.theory_of ctxt; 
5820  514 

54981  515 
val _ = 
65458  516 
Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse 
59582  517 
error "Bad background theory of goal state"; 
49860  518 
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

519 

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

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

522 
val th = 
64567
7141a3a4dc83
always close derivation, for significantly improved performance without parallel proofs;
wenzelm
parents:
64420
diff
changeset

523 
(Goal.conclude (Thm.close_derivation goal) handle THM _ => err_lost ()) 
58950
d07464875dd4
optional proof context for unify operations, for the sake of proper local options;
wenzelm
parents:
58892
diff
changeset

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

526 
> Thm.check_hyps (Context.Proof ctxt); 
23418  527 

528 
val goal_propss = filter_out null propss; 

529 
val results = 

530 
Conjunction.elim_balanced (length goal_propss) th 

531 
> map2 Conjunction.elim_balanced (map length goal_propss) 

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

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

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

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

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

539 
 recover_result [] [] = [] 

60550  540 
 recover_result _ _ = err_lost (); 
23418  541 
in recover_result propss results end; 
5820  542 

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

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

544 

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

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

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

547 
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

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

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

550 
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

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

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

553 

5820  554 

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

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

556 

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

557 
fun raw_goal state = 
63249  558 
let val (ctxt, (using, goal)) = get_goal state 
559 
in {context = ctxt, facts = using, goal = goal} end; 

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

560 

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

561 
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

562 

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

563 
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

564 
let 
63249  565 
val (_, (using, _)) = get_goal state; 
566 
val (ctxt, (_, goal)) = get_goal (refine_insert using state); 

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

567 
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

568 

49866  569 
fun method_error kind pos state = 
570 
Seq.single (Proof_Display.method_error kind pos (raw_goal state)); 

49861  571 

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

572 

5820  573 

574 
(*** structured proof commands ***) 

575 

17112  576 
(** context elements **) 
5820  577 

36324  578 
(* let bindings *) 
5820  579 

16813  580 
local 
581 

17359  582 
fun gen_bind bind args state = 
5820  583 
state 
584 
> assert_forward 

36324  585 
> map_context (bind true args #> snd) 
47068  586 
> reset_facts; 
5820  587 

16813  588 
in 
589 

60377  590 
val let_bind = gen_bind Proof_Context.match_bind; 
591 
val let_bind_cmd = gen_bind Proof_Context.match_bind_cmd; 

5820  592 

16813  593 
end; 
594 

5820  595 

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

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

597 

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

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

599 

62771  600 
fun read_arg (c, mx) ctxt = 
601 
(case Proof_Context.read_const {proper = false, strict = false} ctxt c of 

602 
Free (x, _) => 

603 
let 

604 
val ctxt' = 

605 
ctxt > is_none (Variable.default_type ctxt x) ? 

62959
19c2a58623ed
back to static Mixfix.default_constraint without any special tricks (reverting e6443edaebff);
wenzelm
parents:
62819
diff
changeset

606 
Variable.declare_constraints (Free (x, Mixfix.default_constraint mx)); 
62771  607 
val t = Free (#1 (Proof_Context.inferred_param x ctxt')); 
608 
in ((t, mx), ctxt') end 

609 
 t => ((t, mx), ctxt)); 

610 

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

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

612 
assert_forward 
62771  613 
#> map_context (fold_map prep_arg args #> Proof_Context.notation true mode) 
47068  614 
#> reset_facts; 
36505
79c1d2bbe5a9
ProofContext.read_const: allow for type constraint (for fixed variable);
wenzelm
parents:
36354
diff
changeset

615 

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

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

617 

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

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

620 

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

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

622 

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

623 

17359  624 
(* fix *) 
9196  625 

12714  626 
local 
627 

60469  628 
fun gen_fix add_fixes raw_fixes = 
17359  629 
assert_forward 
60469  630 
#> map_context (snd o add_fixes raw_fixes) 
47068  631 
#> reset_facts; 
5820  632 

16813  633 
in 
634 

60469  635 
val fix = gen_fix Proof_Context.add_fixes; 
636 
val fix_cmd = gen_fix Proof_Context.add_fixes_cmd; 

5820  637 

16813  638 
end; 
639 

5820  640 

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

641 
(* assume *) 
5820  642 

16813  643 
local 
644 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

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

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

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

648 

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

649 
val bindings = map (apsnd (map (prep_att ctxt)) o fst) raw_concls; 
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

650 
val ((params, prems_propss, concl_propss, result_binds), _) = 
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

651 
prep_statement raw_fixes raw_prems (map snd raw_concls) ctxt; 
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

652 
val propss = (map o map) (Logic.close_prop params (flat prems_propss)) concl_propss; 
61654
4a28eec739e9
support for structure statements in 'assume', 'presume';
wenzelm
parents:
61508
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

664 
end; 
6932  665 

16813  666 
in 
667 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

668 
val assm = gen_assume Proof_Context.cert_statement (K I); 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

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

670 

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

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

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

673 

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

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

675 
val presume_cmd = assm_cmd Assumption.presume_export; 
5820  676 

16813  677 
end; 
678 

7271  679 

8374  680 

17112  681 
(** facts **) 
5820  682 

17359  683 
(* chain *) 
5820  684 

17359  685 
val chain = 
686 
assert_forward 

63251  687 
#> (fn state => set_facts (Method.clean_facts (the_facts state)) state) 
17359  688 
#> enter_chain; 
5820  689 

17359  690 
fun chain_facts facts = 
47068  691 
set_facts facts 
17359  692 
#> chain; 
5820  693 

694 

17359  695 
(* note etc. *) 
17112  696 

63352  697 
fun empty_bindings args = map (pair Binding.empty_atts) args; 
17112  698 

699 
local 

700 

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

701 
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state = 
17112  702 
state 
703 
> assert_forward 

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

17112  706 
> these_factss (more_facts state) 
17359  707 
> opt_chain 
708 
> opt_result; 

17112  709 

710 
in 

711 

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

712 
val note_thmss = gen_thmss (K []) I #2 (K I) (K I); 
47815  713 
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact; 
17112  714 

63352  715 
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o empty_bindings; 
47815  716 
val from_thmss_cmd = 
63352  717 
gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings; 
17359  718 

63352  719 
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o empty_bindings; 
47815  720 
val with_thmss_cmd = 
63352  721 
gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o empty_bindings; 
30760
0fffc66b10d7
simplified references to facts, eliminated external note_thmss;
wenzelm
parents:
30757
diff
changeset

722 

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

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

17112  725 
end; 
726 

727 

60371  728 
(* facts during goal refinement *) 
729 

730 
local 

731 

732 
fun gen_supply prep_att prep_fact args state = 

733 
state 

734 
> assert_backward 

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

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

737 

738 
in 

739 

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

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

742 

743 
end; 

744 

745 

18548  746 
(* using/unfolding *) 
17112  747 

748 
local 

749 

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

750 
fun gen_using f g prep_att prep_fact args state = 
17112  751 
state 
752 
> assert_backward 

21442  753 
> map_context_result 
47815  754 
(fn ctxt => ctxt > Proof_Context.note_thmss "" 
63352  755 
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (empty_bindings args))) 
18843  756 
> (fn (named_facts, state') => 
60611
27255d1fbe1a
clarified map_node: operate precisely on goal context and goal info (see also 2b8342b0d98c);
wenzelm
parents:
60595
diff
changeset

757 
state' > map_goal (fn (goal_ctxt, statement, using, goal, before_qed, after_qed) => 
18843  758 
let 
759 
val ctxt = context_of state'; 

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

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

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

24050  763 
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths; 
35624  764 
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths); 
765 
val unfold_goals = Local_Defs.unfold_goals; 

17112  766 

767 
in 

768 

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

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

771 
val unfolding = gen_using unfold_using unfold_goals (K I) (K I); 
47815  772 
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact; 
17112  773 

774 
end; 

775 

776 

777 
(* case *) 

778 

779 
local 

780 

60565  781 
fun gen_case internal prep_att ((raw_binding, raw_atts), ((name, pos), xs)) state = 
17112  782 
let 
60565  783 
val ctxt = context_of state; 
784 

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

786 
val atts = map (prep_att ctxt) raw_atts; 

787 

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

789 
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

790 
val assumptions = 
63003  791 
asms > map (fn (a, ts) => ((Binding.qualify_name true binding a, []), map (rpair []) ts)); 
17112  792 
in 
793 
state' 

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

794 
> assume [] [] assumptions 
60401  795 
> map_context (fold Variable.unbind_term Auto_Bind.no_facts) 
60565  796 
> `the_facts > (fn thms => note_thmss [((binding, atts), [(thms, [])])]) 
17112  797 
end; 
798 

799 
in 

800 

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

17112  803 

804 
end; 

805 

806 

63039  807 
(* define *) 
808 

809 
local 

810 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

811 
fun gen_define prep_stmt prep_att raw_decls raw_fixes raw_defs state = 
63039  812 
let 
813 
val _ = assert_forward state; 

814 
val ctxt = context_of state; 

815 

816 
(*vars*) 

63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

817 
val ((vars, propss, _, binds'), vars_ctxt) = 
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

818 
prep_stmt (raw_decls @ raw_fixes) (map snd raw_defs) ctxt; 
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

819 
val (decls, fixes) = chop (length raw_decls) vars; 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

820 
val show_term = Syntax.string_of_term vars_ctxt; 
63039  821 

822 
(*defs*) 

63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

823 
fun match_defs (((b, _, mx), (_, Free (x, T))) :: more_decls) ((((y, U), t), _) :: more_defs) = 
63352  824 
if x = y then ((b, mx), (Binding.empty_atts, t)) :: match_defs more_decls more_defs 
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

825 
else 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

826 
error ("Mismatch of declaration " ^ show_term (Free (x, T)) ^ " wrt. definition " ^ 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

827 
show_term (Free (y, U))) 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

828 
 match_defs [] [] = [] 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

829 
 match_defs more_decls more_defs = 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

830 
error ("Mismatch of declarations " ^ commas (map (show_term o #2 o #2) more_decls) ^ 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

831 
(if null more_decls then "" else " ") ^ 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

832 
"wrt. definitions " ^ commas (map (show_term o Free o #1 o #1) more_defs)); 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

833 

63395  834 
val derived_def = Local_Defs.derived_def ctxt (K []) {conditional = false}; 
63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

835 
val defs1 = map (derived_def o Logic.close_prop (map #2 fixes) []) (flat propss); 
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

836 
val defs2 = match_defs decls defs1; 
63344  837 
val (defs3, defs_ctxt) = Local_Defs.define defs2 ctxt; 
63039  838 

839 
(*notes*) 

840 
val def_thmss = 

63056
9b95ae9ec671
defs are closed, which leads to proper auto_bind_facts;
wenzelm
parents:
63041
diff
changeset

841 
map (fn (((_, prove), ((b, _), _)), (_, (_, th))) => (b, prove defs_ctxt th)) 
63039  842 
(defs1 ~~ defs2 ~~ defs3) 
843 
> unflat (map snd raw_defs); 

844 
val notes = 

845 
map2 (fn ((a, raw_atts), _) => fn def_thms => 

63041
cb495c4807b3
clarified def binding position: reset for implicit/derived binding, keep for explicit binding;
wenzelm
parents:
63039
diff
changeset

846 
((Thm.def_binding_optional (Binding.conglomerate (map #1 def_thms)) a, 
63039  847 
map (prep_att defs_ctxt) raw_atts), map (fn (_, th) => ([th], [])) def_thms)) 
848 
raw_defs def_thmss; 

849 
in 

850 
state 

851 
> map_context (K defs_ctxt #> fold Variable.bind_term binds') 

852 
> note_thmss notes 

853 
end; 

854 

855 
in 

856 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

857 
val define = gen_define Proof_Context.cert_stmt (K I); 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

858 
val define_cmd = gen_define Proof_Context.read_stmt Attrib.attribute_cmd; 
63039  859 

860 
end; 

861 

862 

17112  863 

17359  864 
(** proof structure **) 
865 

866 
(* blocks *) 

867 

868 
val begin_block = 

869 
assert_forward 

870 
#> open_block 

47068  871 
#> reset_goal 
17359  872 
#> open_block; 
873 

874 
val next_block = 

875 
assert_forward 

876 
#> close_block 

877 
#> open_block 

47068  878 
#> reset_goal 
879 
#> reset_facts; 

17359  880 

881 
fun end_block state = 

882 
state 

883 
> assert_forward 

40960  884 
> assert_bottom false 
17359  885 
> close_block 
886 
> assert_current_goal false 

887 
> close_block 

888 
> export_facts state; 

889 

890 

40960  891 
(* global notepad *) 
892 

893 
val begin_notepad = 

894 
init 

895 
#> open_block 

896 
#> map_context (Variable.set_body true) 

897 
#> open_block; 

898 

899 
val end_notepad = 

900 
assert_forward 

901 
#> assert_bottom true 

902 
#> close_block 

903 
#> assert_current_goal false 

904 
#> close_block 

905 
#> context_of; 

906 

907 

17359  908 
(* subproofs *) 
909 

910 
fun proof opt_text = 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

911 
Seq.APPEND 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

912 
(assert_backward 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

913 
#> refine (the_default Method.standard_text (Method.text opt_text)) 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

914 
#> Seq.map_result 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

915 
(using_facts [] 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

916 
#> enter_forward 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

917 
#> open_block 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

918 
#> reset_goal), 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

919 
method_error "initial" (Method.position opt_text)); 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49861
diff
changeset

920 

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

921 
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

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

923 
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

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

925 
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

926 
 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

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

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

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

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

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

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

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

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

935 
> `before_qed > (refine o the_default Method.succeed_text) 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

936 
> Seq.maps_results (refine finish_text), 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

937 
method_error "terminal" terminal_pos) 
49889
00ea087e83d8
more method position information, notably finished_pos after end of previous text;
wenzelm
parents:
49867
diff
changeset

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

939 
end; 
17359  940 

29383  941 
fun check_result msg sq = 
942 
(case Seq.pull sq of 

943 
NONE => error msg 

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

945 

17359  946 

947 
(* unstructured refinement *) 

948 

49865  949 
fun defer i = 
950 
assert_no_chain #> 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

951 
refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))); 
49865  952 

953 
fun prefer i = 

954 
assert_no_chain #> 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

955 
refine_singleton (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))); 
17359  956 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

957 
fun apply (text, (pos, _)) = 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

958 
Seq.APPEND (assert_backward #> refine text #> Seq.map_result (using_facts []), 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

959 
method_error "" pos); 
49866  960 

61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

961 
fun apply_end (text, (pos, _)) = 
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

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

963 

17359  964 

965 

17112  966 
(** goals **) 
967 

17359  968 
(* generic goals *) 
969 

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

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

971 

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

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

973 
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

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

975 

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

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

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

980 
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

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

982 

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

983 
fun refine_terms n = 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

984 
refine_singleton (Method.Basic (fn ctxt => Method.CONTEXT_TACTIC o 
58002  985 
K (HEADGOAL (PRECISE_CONJUNCTS n 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

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

987 

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

988 
in 
17359  989 

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

990 
fun generic_goal kind before_qed after_qed goal_ctxt goal_propss result_binds state = 
5820  991 
let 
17359  992 
val chaining = can assert_chain state; 
25958  993 
val pos = Position.thread_data (); 
17359  994 

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

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

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

997 
val propss' = vars :: goal_propss; 
23418  998 
val goal_propss = filter_out null propss'; 
60551  999 

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

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

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

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

1007 
map_context (fold Variable.maybe_bind_term result_binds) #> after_local results); 
5820  1008 
in 
60551  1009 
state 
1010 
> assert_forward_or_chain 

1011 
> enter_forward 

1012 
> open_block 

1013 
> enter_backward 

1014 
> map_context 

1015 
(K goal_ctxt 

1016 
#> init_context 

1017 
#> Variable.set_body true 

1018 
#> Proof_Context.auto_bind_goal goal_props) 

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

1019 
> set_goal (make_goal (statement, [], Goal.init goal, before_qed, after_qed')) 
21565  1020 
> chaining ? (`the_facts #> using_facts) 
47068  1021 
> reset_facts 
23418  1022 
> not (null vars) ? refine_terms (length goal_propss) 
61841
4d3527b94f2a
more general types Proof.method / context_tactic;
wenzelm
parents:
61659
diff
changeset

1023 
> null goal_props ? refine_singleton (Method.Basic Method.assumption) 
5820  1024 
end; 
1025 

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

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

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

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

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

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

1031 
in state > close_block > pair (after_qed, (goal_ctxt, results)) end; 
17359  1032 

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

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

1034 

9469  1035 

17359  1036 
(* local goals *) 
1037 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1038 
fun local_goal print_results prep_statement prep_att strict_asm 
60414  1039 
kind before_qed after_qed raw_fixes raw_assumes raw_shows state = 
17359  1040 
let 
60415
9d37b2330ee3
clarified local after_qed: result is not exported yet;
wenzelm
parents:
60414
diff
changeset

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

1042 

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

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

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

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

1046 

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

1048 
val ((params, assumes_propss, shows_propss, result_binds), params_ctxt) = ctxt 
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1049 
> prep_statement raw_fixes (map snd raw_assumes) (map snd raw_shows); 
60406  1050 

61659  1051 
(*prems*) 
1052 
val (assumes_bindings, shows_bindings) = 

1053 
apply2 (map (apsnd (map (prep_att ctxt)) o fst)) (raw_assumes, raw_shows); 

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

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

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

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

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

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

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

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

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

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

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

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

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

1066 
in (prems, ctxt'') end); 
60402  1067 

61659  1068 
(*result*) 
63371
3c7c9f726cc3
clarified fact position, notably for reports on literal facts;
wenzelm
parents:
63370
diff
changeset

1069 
val results_bindings = map (apfst Binding.default_pos) shows_bindings; 
61659  1070 
fun after_qed' (result_ctxt, results) state' = 
1071 
let 

1072 
val ctxt' = context_of state'; 

1073 
val export0 = 

1074 
Assumption.export false result_ctxt ctxt' #> 

1075 
fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #> 

1076 
Raw_Simplifier.norm_hhf_protect ctxt'; 

1077 
val export = map export0 #> Variable.export result_ctxt ctxt'; 

1078 
in 

1079 
state' 

63371
3c7c9f726cc3
clarified fact position, notably for reports on literal facts;
wenzelm
parents:
63370
diff
changeset

1080 
> local_results (results_bindings ~~ burrow export results) 
61659  1081 
> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit)) 
1082 
> after_qed (result_ctxt, results) 

1083 
end; 

60461  1084 
in 
1085 
state 

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

1086 
> generic_goal kind before_qed (after_qed', K I) goal_ctxt shows_propss result_binds 
60461  1087 
> pair that_fact 
1088 
end; 

5820  1089 

49866  1090 
fun local_qeds arg = 
1091 
end_proof false arg 

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

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

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

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

1095 
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
29383  1096 

5820  1097 

17359  1098 
(* global goals *) 
1099 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1114 
end; 
45327  1115 

60388  1116 
val theorem = global_goal Proof_Context.cert_propp; 
1117 
val theorem_cmd = global_goal Proof_Context.read_propp; 

12065  1118 

49866  1119 
fun global_qeds arg = 
1120 
end_proof true arg 

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

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

1122 
after_qed results (context_of state))); 
17112  1123 

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

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

1125 
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error; 
12959  1126 

5820  1127 

67157  1128 
(* relevant proof states *) 
1129 

1130 
fun schematic_goal state = 

1131 
let val (_, {statement = (_, _, prop), ...}) = find_goal state 

1132 
in Goal.is_schematic prop end; 

1133 

1134 
fun is_relevant state = 

1135 
(case try find_goal state of 

1136 
NONE => true 

1137 
 SOME (_, {statement = (_, _, prop), goal, ...}) => 

1138 
Goal.is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal)); 

1139 

1140 

49907  1141 
(* terminal proof steps *) 
17112  1142 

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

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

1144 

64420
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1145 
fun terminal_proof qeds initial terminal state = 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1146 
let 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1147 
val ctxt = context_of state; 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1148 
val check_closure = Method.check_text ctxt #> Method.map_source (Method.method_closure ctxt); 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1149 
val initial' = apfst check_closure initial; 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1150 
val terminal' = (apfst o Option.map o apfst) check_closure terminal; 
2efc128370fa
avoid multiple PIDE markup due to (potentially infinite) backtracking;
wenzelm
parents:
63541
diff
changeset

1151 
in 
67157  1152 
if Goal.skip_proofs_enabled () andalso not (is_relevant state) then 
1153 
state 

67161
b762ed417ed9
implicit quick_and_dirty as for Toplevel.begin_proof/Proof.global_skip_proof;
wenzelm
parents:
67157
diff
changeset

1154 
> proof (SOME (Method.sorry_text true, #2 initial')) 
67157  1155 
> Seq.maps_results (qeds (#2 (#2 initial), (NONE, #2 terminal))) 
1156 
else 

1157 
state 

1158 
> proof (SOME initial') 

1159 
> Seq.maps_results (qeds (#2 (#2 initial), terminal')) 

1160 
end > Seq.the_result ""; 

49848
f222a054342e
more informative error of initial/terminal proof steps;
wenzelm
parents:
49847
diff
changeset

1161 

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

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

1163 

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

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

1166 
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

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

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

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

1171 
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

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

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

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

1175 

6896  1176 

49907  1177 
(* skip proofs *) 
1178 

1179 
fun local_skip_proof int state = 

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

51551  1181 
Skip_Proof.report (context_of state); 
49907  1182 

1183 
fun global_skip_proof int state = 

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

51551  1185 
Skip_Proof.report (context_of state); 
49907  1186 

1187 

17359  1188 
(* common goal statements *) 
1189 

60406  1190 
fun internal_goal print_results mode = 
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1191 
local_goal print_results 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1192 
(fn a => fn b => fn c => Proof_Context.cert_statement a b c o Proof_Context.set_mode mode) (K I); 
60406  1193 

17359  1194 
local 
1195 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

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

1197 
local_goal (Proof_Display.print_results int (Position.thread_data ())) 
63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1198 
prep_statement prep_att strict_asm "have" before_qed after_qed fixes assumes shows; 
6896  1199 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1200 
fun gen_show prep_statement prep_att strict_asm before_qed after_qed fixes assumes shows int state = 
17359  1201 
let 
32738  1202 
val testing = Unsynchronized.ref false; 
1203 
val rule = Unsynchronized.ref (NONE: thm option); 

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

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

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

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

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

1212 
else Proof_Display.print_results int pos ctxt res; 
17359  1213 
fun print_rule ctxt th = 
1214 
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

1215 
else if int then 
56933  1216 
Proof_Display.string_of_rule ctxt "Successful" th 
1217 
> Markup.markup Markup.text_fold 

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

1218 
> Output.state 
17359  1219 
else (); 
1220 
val test_proof = 

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

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

1222 
> Unsynchronized.setmp testing true 
42042  1223 
> Exn.interruptible_capture; 
6896  1224 

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

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

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

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

1228 
> after_qed (result_ctxt, results); 
17359  1229 
in 
1230 
state 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1231 
> local_goal print_results prep_statement prep_att strict_asm 
60414  1232 
"show" before_qed after_qed' fixes assumes shows 
60461  1233 
> int ? (fn goal_state => 
49907  1234 
(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

1235 
Exn.Res _ => goal_state 
42042  1236 
 Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))]))) 
17359  1237 
end; 
1238 

1239 
in 

1240 

63057
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1241 
val have = gen_have Proof_Context.cert_statement (K I); 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1242 
val have_cmd = gen_have Proof_Context.read_statement Attrib.attribute_cmd; 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1243 
val show = gen_show Proof_Context.cert_statement (K I); 
50802acac277
more uniform operations for structured statements;
wenzelm
parents:
63056
diff
changeset

1244 
val show_cmd = gen_show Proof_Context.read_statement Attrib.attribute_cmd; 
6896  1245 

5820  1246 
end; 
17359  1247 

28410  1248 

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

1249 

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

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

1251 

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

1252 
(* full proofs *) 
28410  1253 

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

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

1255 

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

1256 
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

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

1258 
type T = thm option; 
59150  1259 
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

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

1261 

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

1262 
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

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

1264 
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

1265 
 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

1266 

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

1267 
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

1268 
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

1269 

51318  1270 
in 
1271 

1272 
fun future_proof fork_proof state = 

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

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

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

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

29383  1278 
val _ = is_relevant state andalso error "Cannot fork relevant proof"; 
1279 

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

1280 
val after_qed' = 