wenzelm@5820
|
1 |
(* Title: Pure/Isar/proof.ML
|
wenzelm@5820
|
2 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@5820
|
3 |
|
wenzelm@19000
|
4 |
The Isar/VM proof language interpreter: maintains a structured flow of
|
wenzelm@19000
|
5 |
context elements, goals, refinements, and facts.
|
wenzelm@5820
|
6 |
*)
|
wenzelm@5820
|
7 |
|
wenzelm@5820
|
8 |
signature PROOF =
|
wenzelm@5820
|
9 |
sig
|
wenzelm@33031
|
10 |
type context = Proof.context
|
wenzelm@23639
|
11 |
type method = Method.method
|
wenzelm@5820
|
12 |
type state
|
wenzelm@17359
|
13 |
val init: context -> state
|
wenzelm@17359
|
14 |
val level: state -> int
|
wenzelm@17359
|
15 |
val assert_bottom: bool -> state -> state
|
wenzelm@5820
|
16 |
val context_of: state -> context
|
wenzelm@5820
|
17 |
val theory_of: state -> theory
|
wenzelm@13377
|
18 |
val map_context: (context -> context) -> state -> state
|
bulwahn@40890
|
19 |
val map_context_result : (context -> 'a * context) -> state -> 'a * state
|
wenzelm@28278
|
20 |
val map_contexts: (context -> context) -> state -> state
|
wenzelm@38212
|
21 |
val propagate_ml_env: state -> state
|
wenzelm@30764
|
22 |
val bind_terms: (indexname * term option) list -> state -> state
|
wenzelm@26251
|
23 |
val put_thms: bool -> string * thm list option -> state -> state
|
wenzelm@6091
|
24 |
val the_facts: state -> thm list
|
wenzelm@9469
|
25 |
val the_fact: state -> thm
|
wenzelm@47945
|
26 |
val set_facts: thm list -> state -> state
|
wenzelm@47945
|
27 |
val reset_facts: state -> state
|
wenzelm@6891
|
28 |
val assert_forward: state -> state
|
wenzelm@17359
|
29 |
val assert_chain: state -> state
|
wenzelm@9469
|
30 |
val assert_forward_or_chain: state -> state
|
wenzelm@5820
|
31 |
val assert_backward: state -> state
|
wenzelm@8206
|
32 |
val assert_no_chain: state -> state
|
wenzelm@5820
|
33 |
val enter_forward: state -> state
|
wenzelm@24543
|
34 |
val goal_message: (unit -> Pretty.T) -> state -> state
|
wenzelm@12423
|
35 |
val pretty_state: int -> state -> Pretty.T list
|
wenzelm@17112
|
36 |
val refine: Method.text -> state -> state Seq.seq
|
wenzelm@17112
|
37 |
val refine_end: Method.text -> state -> state Seq.seq
|
wenzelm@18908
|
38 |
val refine_insert: thm list -> state -> state
|
wenzelm@17359
|
39 |
val refine_goals: (context -> thm -> unit) -> context -> thm list -> state -> state Seq.seq
|
wenzelm@33288
|
40 |
val raw_goal: state -> {context: context, facts: thm list, goal: thm}
|
wenzelm@33288
|
41 |
val goal: state -> {context: context, facts: thm list, goal: thm}
|
wenzelm@33288
|
42 |
val simple_goal: state -> {context: context, goal: thm}
|
wenzelm@38994
|
43 |
val status_markup: state -> Markup.T
|
wenzelm@36334
|
44 |
val let_bind: (term list * term) list -> state -> state
|
wenzelm@36334
|
45 |
val let_bind_cmd: (string list * string) list -> state -> state
|
wenzelm@36521
|
46 |
val write: Syntax.mode -> (term * mixfix) list -> state -> state
|
wenzelm@36521
|
47 |
val write_cmd: Syntax.mode -> (string * mixfix) list -> state -> state
|
wenzelm@36334
|
48 |
val fix: (binding * typ option * mixfix) list -> state -> state
|
wenzelm@36334
|
49 |
val fix_cmd: (binding * string option * mixfix) list -> state -> state
|
wenzelm@20224
|
50 |
val assm: Assumption.export ->
|
wenzelm@36334
|
51 |
(Thm.binding * (term * term list) list) list -> state -> state
|
wenzelm@36334
|
52 |
val assm_cmd: Assumption.export ->
|
wenzelm@28084
|
53 |
(Attrib.binding * (string * string list) list) list -> state -> state
|
wenzelm@36334
|
54 |
val assume: (Thm.binding * (term * term list) list) list -> state -> state
|
wenzelm@36334
|
55 |
val assume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
|
wenzelm@36334
|
56 |
val presume: (Thm.binding * (term * term list) list) list -> state -> state
|
wenzelm@36334
|
57 |
val presume_cmd: (Attrib.binding * (string * string list) list) list -> state -> state
|
wenzelm@36334
|
58 |
val def: (Thm.binding * ((binding * mixfix) * (term * term list))) list -> state -> state
|
wenzelm@36334
|
59 |
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
|
wenzelm@17359
|
60 |
val chain: state -> state
|
wenzelm@17359
|
61 |
val chain_facts: thm list -> state -> state
|
wenzelm@36334
|
62 |
val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
|
wenzelm@36334
|
63 |
val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
|
wenzelm@36334
|
64 |
val from_thmss: ((thm list * attribute list) list) list -> state -> state
|
wenzelm@36334
|
65 |
val from_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
|
wenzelm@36334
|
66 |
val with_thmss: ((thm list * attribute list) list) list -> state -> state
|
wenzelm@36334
|
67 |
val with_thmss_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
|
wenzelm@36334
|
68 |
val using: ((thm list * attribute list) list) list -> state -> state
|
wenzelm@36334
|
69 |
val using_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
|
wenzelm@36334
|
70 |
val unfolding: ((thm list * attribute list) list) list -> state -> state
|
wenzelm@36334
|
71 |
val unfolding_cmd: ((Facts.ref * Attrib.src list) list) list -> state -> state
|
wenzelm@43368
|
72 |
val invoke_case: string * binding option list * attribute list -> state -> state
|
wenzelm@43368
|
73 |
val invoke_case_cmd: string * binding option list * Attrib.src list -> state -> state
|
wenzelm@17359
|
74 |
val begin_block: state -> state
|
wenzelm@17359
|
75 |
val next_block: state -> state
|
wenzelm@20309
|
76 |
val end_block: state -> state
|
wenzelm@50057
|
77 |
val begin_notepad: context -> state
|
wenzelm@50057
|
78 |
val end_notepad: state -> context
|
wenzelm@17112
|
79 |
val proof: Method.text option -> state -> state Seq.seq
|
wenzelm@50904
|
80 |
val proof_results: Method.text_range option -> state -> state Seq.result Seq.seq
|
wenzelm@50880
|
81 |
val defer: int -> state -> state
|
wenzelm@50880
|
82 |
val prefer: int -> state -> state
|
wenzelm@17112
|
83 |
val apply: Method.text -> state -> state Seq.seq
|
wenzelm@17112
|
84 |
val apply_end: Method.text -> state -> state Seq.seq
|
wenzelm@50904
|
85 |
val apply_results: Method.text_range -> state -> state Seq.result Seq.seq
|
wenzelm@50904
|
86 |
val apply_end_results: Method.text_range -> state -> state Seq.result Seq.seq
|
wenzelm@17359
|
87 |
val local_goal: (context -> ((string * string) * (string * thm list) list) -> unit) ->
|
wenzelm@50057
|
88 |
(context -> 'a -> attribute) ->
|
wenzelm@46203
|
89 |
('b list -> context -> (term list list * (context -> context)) * context) ->
|
wenzelm@29383
|
90 |
string -> Method.text option -> (thm list list -> state -> state) ->
|
haftmann@29581
|
91 |
((binding * 'a list) * 'b) list -> state -> state
|
wenzelm@50904
|
92 |
val local_qed: Method.text_range option * bool -> state -> state
|
wenzelm@21442
|
93 |
val theorem: Method.text option -> (thm list list -> context -> context) ->
|
wenzelm@36334
|
94 |
(term * term list) list list -> context -> state
|
wenzelm@36334
|
95 |
val theorem_cmd: Method.text option -> (thm list list -> context -> context) ->
|
wenzelm@21362
|
96 |
(string * string list) list list -> context -> state
|
wenzelm@50904
|
97 |
val global_qed: Method.text_range option * bool -> state -> context
|
wenzelm@50904
|
98 |
val local_terminal_proof: Method.text_range * Method.text_range option -> state -> state
|
wenzelm@29383
|
99 |
val local_default_proof: state -> state
|
wenzelm@29383
|
100 |
val local_immediate_proof: state -> state
|
wenzelm@29383
|
101 |
val local_skip_proof: bool -> state -> state
|
wenzelm@29383
|
102 |
val local_done_proof: state -> state
|
wenzelm@50904
|
103 |
val global_terminal_proof: Method.text_range * Method.text_range option -> state -> context
|
wenzelm@20363
|
104 |
val global_default_proof: state -> context
|
wenzelm@20363
|
105 |
val global_immediate_proof: state -> context
|
wenzelm@29383
|
106 |
val global_skip_proof: bool -> state -> context
|
wenzelm@20363
|
107 |
val global_done_proof: state -> context
|
wenzelm@29383
|
108 |
val have: Method.text option -> (thm list list -> state -> state) ->
|
wenzelm@36334
|
109 |
(Thm.binding * (term * term list) list) list -> bool -> state -> state
|
wenzelm@36334
|
110 |
val have_cmd: Method.text option -> (thm list list -> state -> state) ->
|
wenzelm@28084
|
111 |
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
|
wenzelm@36334
|
112 |
val show: Method.text option -> (thm list list -> state -> state) ->
|
wenzelm@30215
|
113 |
(Thm.binding * (term * term list) list) list -> bool -> state -> state
|
wenzelm@36334
|
114 |
val show_cmd: Method.text option -> (thm list list -> state -> state) ->
|
wenzelm@28084
|
115 |
(Attrib.binding * (string * string list) list) list -> bool -> state -> state
|
wenzelm@29385
|
116 |
val schematic_goal: state -> bool
|
wenzelm@52363
|
117 |
val is_relevant: state -> bool
|
wenzelm@48288
|
118 |
val local_future_proof: (state -> ('a * state) future) -> state -> 'a future * state
|
wenzelm@50057
|
119 |
val global_future_proof: (state -> ('a * context) future) -> state -> 'a future * context
|
wenzelm@50904
|
120 |
val local_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
|
wenzelm@50881
|
121 |
state -> state
|
wenzelm@50904
|
122 |
val global_future_terminal_proof: Method.text_range * Method.text_range option -> bool ->
|
wenzelm@50881
|
123 |
state -> context
|
wenzelm@5820
|
124 |
end;
|
wenzelm@5820
|
125 |
|
wenzelm@13377
|
126 |
structure Proof: PROOF =
|
wenzelm@5820
|
127 |
struct
|
wenzelm@5820
|
128 |
|
wenzelm@33031
|
129 |
type context = Proof.context;
|
wenzelm@17112
|
130 |
type method = Method.method;
|
wenzelm@16813
|
131 |
|
wenzelm@5820
|
132 |
|
wenzelm@5820
|
133 |
(** proof state **)
|
wenzelm@5820
|
134 |
|
wenzelm@17359
|
135 |
(* datatype state *)
|
wenzelm@5820
|
136 |
|
wenzelm@17112
|
137 |
datatype mode = Forward | Chain | Backward;
|
wenzelm@5820
|
138 |
|
wenzelm@17359
|
139 |
datatype state =
|
wenzelm@17359
|
140 |
State of node Stack.T
|
wenzelm@17359
|
141 |
and node =
|
wenzelm@7176
|
142 |
Node of
|
wenzelm@7176
|
143 |
{context: context,
|
wenzelm@7176
|
144 |
facts: thm list option,
|
wenzelm@7176
|
145 |
mode: mode,
|
wenzelm@17359
|
146 |
goal: goal option}
|
wenzelm@17359
|
147 |
and goal =
|
wenzelm@17359
|
148 |
Goal of
|
wenzelm@29346
|
149 |
{statement: (string * Position.T) * term list list * term,
|
wenzelm@28410
|
150 |
(*goal kind and statement (starting with vars), initial proposition*)
|
wenzelm@25958
|
151 |
messages: (unit -> Pretty.T) list, (*persistent messages (hints etc.)*)
|
wenzelm@25958
|
152 |
using: thm list, (*goal facts*)
|
wenzelm@25958
|
153 |
goal: thm, (*subgoals ==> statement*)
|
wenzelm@17859
|
154 |
before_qed: Method.text option,
|
wenzelm@18124
|
155 |
after_qed:
|
wenzelm@29383
|
156 |
(thm list list -> state -> state) *
|
wenzelm@20363
|
157 |
(thm list list -> context -> context)};
|
wenzelm@17359
|
158 |
|
wenzelm@24543
|
159 |
fun make_goal (statement, messages, using, goal, before_qed, after_qed) =
|
wenzelm@24543
|
160 |
Goal {statement = statement, messages = messages, using = using, goal = goal,
|
wenzelm@17859
|
161 |
before_qed = before_qed, after_qed = after_qed};
|
wenzelm@5820
|
162 |
|
wenzelm@7176
|
163 |
fun make_node (context, facts, mode, goal) =
|
wenzelm@7176
|
164 |
Node {context = context, facts = facts, mode = mode, goal = goal};
|
wenzelm@7176
|
165 |
|
wenzelm@17359
|
166 |
fun map_node f (Node {context, facts, mode, goal}) =
|
wenzelm@17359
|
167 |
make_node (f (context, facts, mode, goal));
|
wenzelm@7176
|
168 |
|
wenzelm@21727
|
169 |
val init_context =
|
wenzelm@43231
|
170 |
Proof_Context.set_stmt true #>
|
wenzelm@47876
|
171 |
Proof_Context.map_naming (K Name_Space.local_naming);
|
wenzelm@21727
|
172 |
|
wenzelm@21466
|
173 |
fun init ctxt =
|
wenzelm@21727
|
174 |
State (Stack.init (make_node (init_context ctxt, NONE, Forward, NONE)));
|
wenzelm@5820
|
175 |
|
wenzelm@50026
|
176 |
fun top (State st) = Stack.top st |> (fn Node node => node);
|
wenzelm@50026
|
177 |
fun map_top f (State st) = State (Stack.map_top (map_node f) st);
|
wenzelm@28278
|
178 |
fun map_all f (State st) = State (Stack.map_all (map_node f) st);
|
wenzelm@12045
|
179 |
|
wenzelm@5820
|
180 |
|
wenzelm@5820
|
181 |
|
wenzelm@5820
|
182 |
(** basic proof state operations **)
|
wenzelm@5820
|
183 |
|
wenzelm@17359
|
184 |
(* block structure *)
|
wenzelm@17359
|
185 |
|
wenzelm@17359
|
186 |
fun open_block (State st) = State (Stack.push st);
|
wenzelm@17359
|
187 |
|
wenzelm@18678
|
188 |
fun close_block (State st) = State (Stack.pop st)
|
wenzelm@47937
|
189 |
handle List.Empty => error "Unbalanced block parentheses";
|
wenzelm@17359
|
190 |
|
wenzelm@17359
|
191 |
fun level (State st) = Stack.level st;
|
wenzelm@17359
|
192 |
|
wenzelm@17359
|
193 |
fun assert_bottom b state =
|
wenzelm@47942
|
194 |
let val b' = level state <= 2 in
|
wenzelm@47942
|
195 |
if b andalso not b' then error "Not at bottom of proof"
|
wenzelm@47942
|
196 |
else if not b andalso b' then error "Already at bottom of proof"
|
wenzelm@17359
|
197 |
else state
|
wenzelm@17359
|
198 |
end;
|
wenzelm@17359
|
199 |
|
wenzelm@17359
|
200 |
|
wenzelm@5820
|
201 |
(* context *)
|
wenzelm@5820
|
202 |
|
wenzelm@50026
|
203 |
val context_of = #context o top;
|
wenzelm@43231
|
204 |
val theory_of = Proof_Context.theory_of o context_of;
|
wenzelm@5820
|
205 |
|
wenzelm@48308
|
206 |
fun map_node_context f =
|
wenzelm@48308
|
207 |
map_node (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
|
wenzelm@48308
|
208 |
|
wenzelm@17359
|
209 |
fun map_context f =
|
wenzelm@50026
|
210 |
map_top (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
|
wenzelm@5820
|
211 |
|
wenzelm@17359
|
212 |
fun map_context_result f state =
|
wenzelm@17859
|
213 |
f (context_of state) ||> (fn ctxt => map_context (K ctxt) state);
|
wenzelm@5820
|
214 |
|
wenzelm@28278
|
215 |
fun map_contexts f = map_all (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
|
wenzelm@28278
|
216 |
|
wenzelm@38212
|
217 |
fun propagate_ml_env state = map_contexts
|
wenzelm@38212
|
218 |
(Context.proof_map (ML_Env.inherit (Context.Proof (context_of state)))) state;
|
wenzelm@38212
|
219 |
|
wenzelm@43231
|
220 |
val bind_terms = map_context o Proof_Context.bind_terms;
|
wenzelm@43231
|
221 |
val put_thms = map_context oo Proof_Context.put_thms;
|
wenzelm@5820
|
222 |
|
wenzelm@5820
|
223 |
|
wenzelm@5820
|
224 |
(* facts *)
|
wenzelm@5820
|
225 |
|
wenzelm@50026
|
226 |
val get_facts = #facts o top;
|
wenzelm@17359
|
227 |
|
wenzelm@17359
|
228 |
fun the_facts state =
|
wenzelm@17359
|
229 |
(case get_facts state of SOME facts => facts
|
wenzelm@18678
|
230 |
| NONE => error "No current facts available");
|
wenzelm@5820
|
231 |
|
wenzelm@9469
|
232 |
fun the_fact state =
|
wenzelm@17359
|
233 |
(case the_facts state of [thm] => thm
|
wenzelm@18678
|
234 |
| _ => error "Single theorem expected");
|
wenzelm@9469
|
235 |
|
wenzelm@17359
|
236 |
fun put_facts facts =
|
wenzelm@50026
|
237 |
map_top (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal)) #>
|
wenzelm@33386
|
238 |
put_thms true (Auto_Bind.thisN, facts);
|
wenzelm@6848
|
239 |
|
wenzelm@47945
|
240 |
val set_facts = put_facts o SOME;
|
wenzelm@47945
|
241 |
val reset_facts = put_facts NONE;
|
wenzelm@47945
|
242 |
|
wenzelm@17359
|
243 |
fun these_factss more_facts (named_factss, state) =
|
wenzelm@47945
|
244 |
(named_factss, state |> set_facts (maps snd named_factss @ more_facts));
|
wenzelm@7605
|
245 |
|
wenzelm@17359
|
246 |
fun export_facts inner outer =
|
wenzelm@17359
|
247 |
(case get_facts inner of
|
wenzelm@47945
|
248 |
NONE => reset_facts outer
|
wenzelm@17359
|
249 |
| SOME thms =>
|
wenzelm@17359
|
250 |
thms
|
wenzelm@43231
|
251 |
|> Proof_Context.export (context_of inner) (context_of outer)
|
wenzelm@47945
|
252 |
|> (fn ths => set_facts ths outer));
|
wenzelm@5820
|
253 |
|
wenzelm@5820
|
254 |
|
wenzelm@5820
|
255 |
(* mode *)
|
wenzelm@5820
|
256 |
|
wenzelm@50026
|
257 |
val get_mode = #mode o top;
|
wenzelm@50026
|
258 |
fun put_mode mode = map_top (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
|
wenzelm@5820
|
259 |
|
wenzelm@17359
|
260 |
val mode_name = (fn Forward => "state" | Chain => "chain" | Backward => "prove");
|
wenzelm@5820
|
261 |
|
wenzelm@5820
|
262 |
fun assert_mode pred state =
|
wenzelm@5820
|
263 |
let val mode = get_mode state in
|
wenzelm@5820
|
264 |
if pred mode then state
|
wenzelm@18678
|
265 |
else error ("Illegal application of proof command in " ^ quote (mode_name mode) ^ " mode")
|
wenzelm@5820
|
266 |
end;
|
wenzelm@5820
|
267 |
|
wenzelm@19308
|
268 |
val assert_forward = assert_mode (fn mode => mode = Forward);
|
wenzelm@19308
|
269 |
val assert_chain = assert_mode (fn mode => mode = Chain);
|
wenzelm@19308
|
270 |
val assert_forward_or_chain = assert_mode (fn mode => mode = Forward orelse mode = Chain);
|
wenzelm@19308
|
271 |
val assert_backward = assert_mode (fn mode => mode = Backward);
|
wenzelm@19308
|
272 |
val assert_no_chain = assert_mode (fn mode => mode <> Chain);
|
wenzelm@5820
|
273 |
|
wenzelm@17359
|
274 |
val enter_forward = put_mode Forward;
|
wenzelm@17359
|
275 |
val enter_chain = put_mode Chain;
|
wenzelm@17359
|
276 |
val enter_backward = put_mode Backward;
|
wenzelm@5820
|
277 |
|
wenzelm@5820
|
278 |
|
wenzelm@17359
|
279 |
(* current goal *)
|
wenzelm@6776
|
280 |
|
wenzelm@17359
|
281 |
fun current_goal state =
|
wenzelm@50026
|
282 |
(case top state of
|
wenzelm@17359
|
283 |
{context, goal = SOME (Goal goal), ...} => (context, goal)
|
wenzelm@47942
|
284 |
| _ => error "No current goal");
|
wenzelm@5820
|
285 |
|
wenzelm@17359
|
286 |
fun assert_current_goal g state =
|
wenzelm@17359
|
287 |
let val g' = can current_goal state in
|
wenzelm@47942
|
288 |
if g andalso not g' then error "No goal in this block"
|
wenzelm@47942
|
289 |
else if not g andalso g' then error "Goal present in this block"
|
wenzelm@17359
|
290 |
else state
|
wenzelm@17359
|
291 |
end;
|
wenzelm@5820
|
292 |
|
wenzelm@50026
|
293 |
fun put_goal goal = map_top (fn (ctxt, using, mode, _) => (ctxt, using, mode, goal));
|
wenzelm@17359
|
294 |
|
wenzelm@47945
|
295 |
val set_goal = put_goal o SOME;
|
wenzelm@47945
|
296 |
val reset_goal = put_goal NONE;
|
wenzelm@47945
|
297 |
|
wenzelm@17859
|
298 |
val before_qed = #before_qed o #2 o current_goal;
|
wenzelm@17859
|
299 |
|
wenzelm@17359
|
300 |
|
wenzelm@17359
|
301 |
(* nested goal *)
|
wenzelm@17359
|
302 |
|
wenzelm@48308
|
303 |
fun map_goal f g h (State (Node {context, facts, mode, goal = SOME goal}, node :: nodes)) =
|
wenzelm@17359
|
304 |
let
|
wenzelm@24543
|
305 |
val Goal {statement, messages, using, goal, before_qed, after_qed} = goal;
|
wenzelm@24543
|
306 |
val goal' = make_goal (g (statement, messages, using, goal, before_qed, after_qed));
|
wenzelm@48308
|
307 |
val node' = map_node_context h node;
|
wenzelm@48308
|
308 |
in State (make_node (f context, facts, mode, SOME goal'), node' :: nodes) end
|
wenzelm@48308
|
309 |
| map_goal f g h (State (nd, node :: nodes)) =
|
wenzelm@48308
|
310 |
let
|
wenzelm@48308
|
311 |
val nd' = map_node_context f nd;
|
wenzelm@48308
|
312 |
val State (node', nodes') = map_goal f g h (State (node, nodes));
|
wenzelm@48308
|
313 |
in State (nd', node' :: nodes') end
|
wenzelm@48308
|
314 |
| map_goal _ _ _ state = state;
|
wenzelm@17359
|
315 |
|
wenzelm@47945
|
316 |
fun provide_goal goal = map_goal I (fn (statement, _, using, _, before_qed, after_qed) =>
|
wenzelm@48308
|
317 |
(statement, [], using, goal, before_qed, after_qed)) I;
|
wenzelm@19188
|
318 |
|
wenzelm@24543
|
319 |
fun goal_message msg = map_goal I (fn (statement, messages, using, goal, before_qed, after_qed) =>
|
wenzelm@48308
|
320 |
(statement, msg :: messages, using, goal, before_qed, after_qed)) I;
|
wenzelm@24543
|
321 |
|
wenzelm@24556
|
322 |
fun using_facts using = map_goal I (fn (statement, _, _, goal, before_qed, after_qed) =>
|
wenzelm@48308
|
323 |
(statement, [], using, goal, before_qed, after_qed)) I;
|
wenzelm@17359
|
324 |
|
wenzelm@17359
|
325 |
local
|
wenzelm@17359
|
326 |
fun find i state =
|
wenzelm@17359
|
327 |
(case try current_goal state of
|
wenzelm@17359
|
328 |
SOME (ctxt, goal) => (ctxt, (i, goal))
|
wenzelm@18678
|
329 |
| NONE => find (i + 1) (close_block state handle ERROR _ => error "No goal present"));
|
wenzelm@17359
|
330 |
in val find_goal = find 0 end;
|
wenzelm@17359
|
331 |
|
wenzelm@17359
|
332 |
fun get_goal state =
|
wenzelm@17359
|
333 |
let val (ctxt, (_, {using, goal, ...})) = find_goal state
|
wenzelm@17359
|
334 |
in (ctxt, (using, goal)) end;
|
wenzelm@5820
|
335 |
|
wenzelm@5820
|
336 |
|
wenzelm@5820
|
337 |
|
wenzelm@12423
|
338 |
(** pretty_state **)
|
wenzelm@5820
|
339 |
|
skalberg@15531
|
340 |
fun pretty_facts _ _ NONE = []
|
skalberg@15531
|
341 |
| pretty_facts s ctxt (SOME ths) =
|
wenzelm@50882
|
342 |
[(Pretty.block o Pretty.fbreaks)
|
wenzelm@50924
|
343 |
((if s = "" then Pretty.str "this:"
|
wenzelm@50924
|
344 |
else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
|
wenzelm@50924
|
345 |
map (Display.pretty_thm ctxt) ths),
|
wenzelm@50924
|
346 |
Pretty.str ""];
|
wenzelm@6756
|
347 |
|
wenzelm@17359
|
348 |
fun pretty_state nr state =
|
wenzelm@5820
|
349 |
let
|
wenzelm@50026
|
350 |
val {context = ctxt, facts, mode, goal = _} = top state;
|
wenzelm@43630
|
351 |
val verbose = Config.get ctxt Proof_Context.verbose;
|
wenzelm@5820
|
352 |
|
wenzelm@50875
|
353 |
fun prt_goal (SOME (_, (_,
|
wenzelm@29417
|
354 |
{statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
|
wenzelm@50924
|
355 |
pretty_facts "using" ctxt
|
wenzelm@17359
|
356 |
(if mode <> Backward orelse null using then NONE else SOME using) @
|
wenzelm@50875
|
357 |
[Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
|
wenzelm@25958
|
358 |
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
|
wenzelm@17359
|
359 |
| prt_goal NONE = [];
|
wenzelm@6848
|
360 |
|
wenzelm@17359
|
361 |
val prt_ctxt =
|
wenzelm@43630
|
362 |
if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt
|
wenzelm@43231
|
363 |
else if mode = Backward then Proof_Context.pretty_ctxt ctxt
|
wenzelm@7575
|
364 |
else [];
|
wenzelm@17359
|
365 |
in
|
wenzelm@17359
|
366 |
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
|
wenzelm@43630
|
367 |
(if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")),
|
wenzelm@17359
|
368 |
Pretty.str ""] @
|
wenzelm@17359
|
369 |
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
|
wenzelm@43630
|
370 |
(if verbose orelse mode = Forward then
|
wenzelm@39349
|
371 |
pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
|
wenzelm@50924
|
372 |
else if mode = Chain then pretty_facts "picking" ctxt facts
|
wenzelm@17359
|
373 |
else prt_goal (try find_goal state))
|
wenzelm@17359
|
374 |
end;
|
wenzelm@5820
|
375 |
|
wenzelm@5820
|
376 |
|
wenzelm@5820
|
377 |
|
wenzelm@5820
|
378 |
(** proof steps **)
|
wenzelm@5820
|
379 |
|
wenzelm@17359
|
380 |
(* refine via method *)
|
wenzelm@5820
|
381 |
|
wenzelm@8234
|
382 |
local
|
wenzelm@8234
|
383 |
|
wenzelm@16146
|
384 |
fun goalN i = "goal" ^ string_of_int i;
|
wenzelm@16146
|
385 |
fun goals st = map goalN (1 upto Thm.nprems_of st);
|
wenzelm@16146
|
386 |
|
wenzelm@16146
|
387 |
fun no_goal_cases st = map (rpair NONE) (goals st);
|
wenzelm@16146
|
388 |
|
wenzelm@16146
|
389 |
fun goal_cases st =
|
wenzelm@48686
|
390 |
Rule_Cases.make_common
|
wenzelm@48686
|
391 |
(Thm.theory_of_thm st, Thm.prop_of st) (map (rpair [] o rpair []) (goals st));
|
wenzelm@16146
|
392 |
|
wenzelm@32193
|
393 |
fun apply_method current_context meth state =
|
wenzelm@6848
|
394 |
let
|
wenzelm@24556
|
395 |
val (goal_ctxt, (_, {statement, messages = _, using, goal, before_qed, after_qed})) =
|
wenzelm@24543
|
396 |
find_goal state;
|
wenzelm@25958
|
397 |
val ctxt = if current_context then context_of state else goal_ctxt;
|
wenzelm@16146
|
398 |
in
|
wenzelm@32193
|
399 |
Method.apply meth ctxt using goal |> Seq.map (fn (meth_cases, goal') =>
|
wenzelm@6848
|
400 |
state
|
wenzelm@16146
|
401 |
|> map_goal
|
wenzelm@43231
|
402 |
(Proof_Context.add_cases false (no_goal_cases goal @ goal_cases goal') #>
|
wenzelm@43231
|
403 |
Proof_Context.add_cases true meth_cases)
|
wenzelm@48308
|
404 |
(K (statement, [], using, goal', before_qed, after_qed)) I)
|
wenzelm@16146
|
405 |
end;
|
wenzelm@5820
|
406 |
|
wenzelm@19188
|
407 |
fun select_goals n meth state =
|
wenzelm@19224
|
408 |
state
|
wenzelm@19224
|
409 |
|> (#2 o #2 o get_goal)
|
wenzelm@21687
|
410 |
|> ALLGOALS Goal.conjunction_tac
|
wenzelm@19224
|
411 |
|> Seq.maps (fn goal =>
|
wenzelm@19188
|
412 |
state
|
wenzelm@47945
|
413 |
|> Seq.lift provide_goal (Goal.extract 1 n goal |> Seq.maps (Goal.conjunction_tac 1))
|
wenzelm@19188
|
414 |
|> Seq.maps meth
|
wenzelm@19188
|
415 |
|> Seq.maps (fn state' => state'
|
wenzelm@47945
|
416 |
|> Seq.lift provide_goal (Goal.retrofit 1 n (#2 (#2 (get_goal state'))) goal))
|
wenzelm@32193
|
417 |
|> Seq.maps (apply_method true (K Method.succeed)));
|
wenzelm@19188
|
418 |
|
wenzelm@17112
|
419 |
fun apply_text cc text state =
|
wenzelm@17112
|
420 |
let
|
wenzelm@17112
|
421 |
val thy = theory_of state;
|
wenzelm@17112
|
422 |
|
wenzelm@32193
|
423 |
fun eval (Method.Basic m) = apply_method cc m
|
wenzelm@32193
|
424 |
| eval (Method.Source src) = apply_method cc (Method.method thy src)
|
wenzelm@32193
|
425 |
| eval (Method.Source_i src) = apply_method cc (Method.method_i thy src)
|
wenzelm@17112
|
426 |
| eval (Method.Then txts) = Seq.EVERY (map eval txts)
|
wenzelm@17112
|
427 |
| eval (Method.Orelse txts) = Seq.FIRST (map eval txts)
|
wenzelm@17112
|
428 |
| eval (Method.Try txt) = Seq.TRY (eval txt)
|
wenzelm@19188
|
429 |
| eval (Method.Repeat1 txt) = Seq.REPEAT1 (eval txt)
|
wenzelm@19188
|
430 |
| eval (Method.SelectGoals (n, txt)) = select_goals n (eval txt);
|
wenzelm@17112
|
431 |
in eval text state end;
|
wenzelm@17112
|
432 |
|
wenzelm@8234
|
433 |
in
|
wenzelm@8234
|
434 |
|
wenzelm@17112
|
435 |
val refine = apply_text true;
|
wenzelm@17112
|
436 |
val refine_end = apply_text false;
|
wenzelm@32856
|
437 |
fun refine_insert ths = Seq.hd o refine (Method.Basic (K (Method.insert ths)));
|
wenzelm@18908
|
438 |
|
wenzelm@8234
|
439 |
end;
|
wenzelm@8234
|
440 |
|
wenzelm@5820
|
441 |
|
wenzelm@17359
|
442 |
(* refine via sub-proof *)
|
wenzelm@17359
|
443 |
|
wenzelm@47342
|
444 |
local
|
wenzelm@47342
|
445 |
|
wenzelm@30559
|
446 |
fun finish_tac 0 = K all_tac
|
wenzelm@30559
|
447 |
| finish_tac n =
|
wenzelm@30559
|
448 |
Goal.norm_hhf_tac THEN'
|
wenzelm@30559
|
449 |
SUBGOAL (fn (goal, i) =>
|
wenzelm@30559
|
450 |
if can Logic.unprotect (Logic.strip_assums_concl goal) then
|
wenzelm@30559
|
451 |
Tactic.etac Drule.protectI i THEN finish_tac (n - 1) i
|
wenzelm@30559
|
452 |
else finish_tac (n - 1) (i + 1));
|
wenzelm@30559
|
453 |
|
wenzelm@20208
|
454 |
fun goal_tac rule =
|
wenzelm@30559
|
455 |
Goal.norm_hhf_tac THEN'
|
wenzelm@30559
|
456 |
Tactic.rtac rule THEN'
|
wenzelm@30559
|
457 |
finish_tac (Thm.nprems_of rule);
|
wenzelm@11816
|
458 |
|
wenzelm@47342
|
459 |
fun FINDGOAL tac st =
|
wenzelm@47342
|
460 |
let fun find i n = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1) n)
|
wenzelm@47342
|
461 |
in find 1 (Thm.nprems_of st) st end;
|
wenzelm@47342
|
462 |
|
wenzelm@47342
|
463 |
in
|
wenzelm@47342
|
464 |
|
wenzelm@19915
|
465 |
fun refine_goals print_rule inner raw_rules state =
|
wenzelm@19915
|
466 |
let
|
wenzelm@19915
|
467 |
val (outer, (_, goal)) = get_goal state;
|
wenzelm@20208
|
468 |
fun refine rule st = (print_rule outer rule; FINDGOAL (goal_tac rule) st);
|
wenzelm@19915
|
469 |
in
|
wenzelm@19915
|
470 |
raw_rules
|
wenzelm@43231
|
471 |
|> Proof_Context.goal_export inner outer
|
wenzelm@47945
|
472 |
|> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
|
wenzelm@19915
|
473 |
end;
|
wenzelm@6932
|
474 |
|
wenzelm@47342
|
475 |
end;
|
wenzelm@47342
|
476 |
|
wenzelm@6932
|
477 |
|
wenzelm@50861
|
478 |
(* conclude goal *)
|
wenzelm@50861
|
479 |
|
wenzelm@28627
|
480 |
fun conclude_goal ctxt goal propss =
|
wenzelm@5820
|
481 |
let
|
wenzelm@43231
|
482 |
val thy = Proof_Context.theory_of ctxt;
|
wenzelm@24920
|
483 |
val string_of_term = Syntax.string_of_term ctxt;
|
wenzelm@32111
|
484 |
val string_of_thm = Display.string_of_thm ctxt;
|
wenzelm@5820
|
485 |
|
wenzelm@50875
|
486 |
val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
|
wenzelm@20224
|
487 |
|
wenzelm@20224
|
488 |
val extra_hyps = Assumption.extra_hyps ctxt goal;
|
wenzelm@20224
|
489 |
val _ = null extra_hyps orelse
|
wenzelm@20224
|
490 |
error ("Additional hypotheses:\n" ^ cat_lines (map string_of_term extra_hyps));
|
wenzelm@5820
|
491 |
|
wenzelm@23418
|
492 |
fun lost_structure () = error ("Lost goal structure:\n" ^ string_of_thm goal);
|
wenzelm@23418
|
493 |
|
berghofe@23782
|
494 |
val th = Goal.conclude
|
wenzelm@23806
|
495 |
(if length (flat propss) > 1 then Thm.norm_proof goal else goal)
|
berghofe@23782
|
496 |
handle THM _ => lost_structure ();
|
wenzelm@23418
|
497 |
val goal_propss = filter_out null propss;
|
wenzelm@23418
|
498 |
val results =
|
wenzelm@23418
|
499 |
Conjunction.elim_balanced (length goal_propss) th
|
wenzelm@23418
|
500 |
|> map2 Conjunction.elim_balanced (map length goal_propss)
|
wenzelm@23418
|
501 |
handle THM _ => lost_structure ();
|
wenzelm@23418
|
502 |
val _ = Unify.matches_list thy (flat goal_propss) (map Thm.prop_of (flat results)) orelse
|
wenzelm@19774
|
503 |
error ("Proved a different theorem:\n" ^ string_of_thm th);
|
wenzelm@28627
|
504 |
val _ = Thm.check_shyps (Variable.sorts_of ctxt) th;
|
wenzelm@23418
|
505 |
|
wenzelm@23418
|
506 |
fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
|
wenzelm@23418
|
507 |
| recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
|
wenzelm@23418
|
508 |
| recover_result [] [] = []
|
wenzelm@23418
|
509 |
| recover_result _ _ = lost_structure ();
|
wenzelm@23418
|
510 |
in recover_result propss results end;
|
wenzelm@5820
|
511 |
|
wenzelm@50874
|
512 |
val finished_goal_error = "Failed to finish proof";
|
wenzelm@50874
|
513 |
|
wenzelm@50904
|
514 |
fun finished_goal pos state =
|
wenzelm@50874
|
515 |
let val (ctxt, (_, goal)) = get_goal state in
|
wenzelm@50874
|
516 |
if Thm.no_prems goal then Seq.Result state
|
wenzelm@50904
|
517 |
else
|
wenzelm@50904
|
518 |
Seq.Error (fn () =>
|
wenzelm@50904
|
519 |
finished_goal_error ^ Position.here pos ^ ":\n" ^
|
wenzelm@50904
|
520 |
Proof_Display.string_of_goal ctxt goal)
|
wenzelm@50874
|
521 |
end;
|
wenzelm@50861
|
522 |
|
wenzelm@5820
|
523 |
|
wenzelm@33288
|
524 |
(* goal views -- corresponding to methods *)
|
wenzelm@33288
|
525 |
|
wenzelm@33288
|
526 |
fun raw_goal state =
|
wenzelm@33288
|
527 |
let val (ctxt, (facts, goal)) = get_goal state
|
wenzelm@33288
|
528 |
in {context = ctxt, facts = facts, goal = goal} end;
|
wenzelm@33288
|
529 |
|
wenzelm@33288
|
530 |
val goal = raw_goal o refine_insert [];
|
wenzelm@33288
|
531 |
|
wenzelm@33288
|
532 |
fun simple_goal state =
|
wenzelm@33288
|
533 |
let
|
wenzelm@33288
|
534 |
val (_, (facts, _)) = get_goal state;
|
wenzelm@33288
|
535 |
val (ctxt, (_, goal)) = get_goal (refine_insert facts state);
|
wenzelm@33288
|
536 |
in {context = ctxt, goal = goal} end;
|
wenzelm@33288
|
537 |
|
wenzelm@38994
|
538 |
fun status_markup state =
|
wenzelm@38994
|
539 |
(case try goal state of
|
wenzelm@51216
|
540 |
SOME {goal, ...} => Markup.proof_state (Thm.nprems_of goal)
|
wenzelm@38994
|
541 |
| NONE => Markup.empty);
|
wenzelm@38994
|
542 |
|
wenzelm@50881
|
543 |
fun method_error kind pos state =
|
wenzelm@50881
|
544 |
Seq.single (Proof_Display.method_error kind pos (raw_goal state));
|
wenzelm@50876
|
545 |
|
wenzelm@33288
|
546 |
|
wenzelm@5820
|
547 |
|
wenzelm@5820
|
548 |
(*** structured proof commands ***)
|
wenzelm@5820
|
549 |
|
wenzelm@17112
|
550 |
(** context elements **)
|
wenzelm@5820
|
551 |
|
wenzelm@36335
|
552 |
(* let bindings *)
|
wenzelm@5820
|
553 |
|
wenzelm@16813
|
554 |
local
|
wenzelm@16813
|
555 |
|
wenzelm@17359
|
556 |
fun gen_bind bind args state =
|
wenzelm@5820
|
557 |
state
|
wenzelm@5820
|
558 |
|> assert_forward
|
wenzelm@36335
|
559 |
|> map_context (bind true args #> snd)
|
wenzelm@47945
|
560 |
|> reset_facts;
|
wenzelm@5820
|
561 |
|
wenzelm@16813
|
562 |
in
|
wenzelm@16813
|
563 |
|
wenzelm@43231
|
564 |
val let_bind = gen_bind Proof_Context.match_bind_i;
|
wenzelm@43231
|
565 |
val let_bind_cmd = gen_bind Proof_Context.match_bind;
|
wenzelm@5820
|
566 |
|
wenzelm@16813
|
567 |
end;
|
wenzelm@16813
|
568 |
|
wenzelm@5820
|
569 |
|
wenzelm@36521
|
570 |
(* concrete syntax *)
|
wenzelm@36521
|
571 |
|
wenzelm@36521
|
572 |
local
|
wenzelm@36521
|
573 |
|
wenzelm@36523
|
574 |
fun gen_write prep_arg mode args =
|
wenzelm@36523
|
575 |
assert_forward
|
wenzelm@43231
|
576 |
#> map_context (fn ctxt => ctxt |> Proof_Context.notation true mode (map (prep_arg ctxt) args))
|
wenzelm@47945
|
577 |
#> reset_facts;
|
wenzelm@36521
|
578 |
|
wenzelm@36521
|
579 |
in
|
wenzelm@36521
|
580 |
|
wenzelm@36521
|
581 |
val write = gen_write (K I);
|
wenzelm@36521
|
582 |
|
wenzelm@36521
|
583 |
val write_cmd =
|
wenzelm@36521
|
584 |
gen_write (fn ctxt => fn (c, mx) =>
|
wenzelm@43231
|
585 |
(Proof_Context.read_const ctxt false (Mixfix.mixfixT mx) c, mx));
|
wenzelm@36521
|
586 |
|
wenzelm@36521
|
587 |
end;
|
wenzelm@36521
|
588 |
|
wenzelm@36521
|
589 |
|
wenzelm@17359
|
590 |
(* fix *)
|
wenzelm@5820
|
591 |
|
wenzelm@12714
|
592 |
local
|
wenzelm@12714
|
593 |
|
wenzelm@30770
|
594 |
fun gen_fix prep_vars args =
|
wenzelm@17359
|
595 |
assert_forward
|
wenzelm@46468
|
596 |
#> map_context (fn ctxt => snd (Proof_Context.add_fixes (fst (prep_vars args ctxt)) ctxt))
|
wenzelm@47945
|
597 |
#> reset_facts;
|
wenzelm@5820
|
598 |
|
wenzelm@16813
|
599 |
in
|
wenzelm@16813
|
600 |
|
wenzelm@46468
|
601 |
val fix = gen_fix Proof_Context.cert_vars;
|
wenzelm@46468
|
602 |
val fix_cmd = gen_fix Proof_Context.read_vars;
|
wenzelm@5820
|
603 |
|
wenzelm@16813
|
604 |
end;
|
wenzelm@16813
|
605 |
|
wenzelm@5820
|
606 |
|
wenzelm@17359
|
607 |
(* assume etc. *)
|
wenzelm@5820
|
608 |
|
wenzelm@16813
|
609 |
local
|
wenzelm@16813
|
610 |
|
wenzelm@17112
|
611 |
fun gen_assume asm prep_att exp args state =
|
wenzelm@5820
|
612 |
state
|
wenzelm@5820
|
613 |
|> assert_forward
|
wenzelm@48686
|
614 |
|> map_context_result (asm exp (Attrib.map_specs (map (prep_att (context_of state))) args))
|
wenzelm@17359
|
615 |
|> these_factss [] |> #2;
|
wenzelm@6932
|
616 |
|
wenzelm@16813
|
617 |
in
|
wenzelm@16813
|
618 |
|
wenzelm@43231
|
619 |
val assm = gen_assume Proof_Context.add_assms_i (K I);
|
wenzelm@48686
|
620 |
val assm_cmd = gen_assume Proof_Context.add_assms Attrib.attribute_cmd;
|
wenzelm@36334
|
621 |
val assume = assm Assumption.assume_export;
|
wenzelm@36334
|
622 |
val assume_cmd = assm_cmd Assumption.assume_export;
|
wenzelm@36334
|
623 |
val presume = assm Assumption.presume_export;
|
wenzelm@36334
|
624 |
val presume_cmd = assm_cmd Assumption.presume_export;
|
wenzelm@5820
|
625 |
|
wenzelm@16813
|
626 |
end;
|
wenzelm@16813
|
627 |
|
wenzelm@7271
|
628 |
|
wenzelm@17359
|
629 |
(* def *)
|
wenzelm@11891
|
630 |
|
wenzelm@16813
|
631 |
local
|
wenzelm@16813
|
632 |
|
wenzelm@20913
|
633 |
fun gen_def prep_att prep_vars prep_binds args state =
|
wenzelm@11891
|
634 |
let
|
wenzelm@11891
|
635 |
val _ = assert_forward state;
|
wenzelm@20913
|
636 |
val (raw_name_atts, (raw_vars, raw_rhss)) = args |> split_list ||> split_list;
|
wenzelm@48686
|
637 |
val name_atts = map (apsnd (map (prep_att (context_of state)))) raw_name_atts;
|
wenzelm@11891
|
638 |
in
|
wenzelm@20913
|
639 |
state
|
wenzelm@20913
|
640 |
|> map_context_result (prep_vars (map (fn (x, mx) => (x, NONE, mx)) raw_vars))
|
wenzelm@20913
|
641 |
|>> map (fn (x, _, mx) => (x, mx))
|
wenzelm@20913
|
642 |
|-> (fn vars =>
|
wenzelm@20913
|
643 |
map_context_result (prep_binds false (map swap raw_rhss))
|
wenzelm@50763
|
644 |
#-> (fn rhss =>
|
wenzelm@50763
|
645 |
let
|
wenzelm@50763
|
646 |
val defs = (vars ~~ (name_atts ~~ rhss)) |> map (fn ((x, mx), ((a, atts), rhs)) =>
|
wenzelm@50763
|
647 |
((x, mx), ((Thm.def_binding_optional x a, atts), rhs)));
|
wenzelm@50763
|
648 |
in map_context_result (Local_Defs.add_defs defs) end))
|
wenzelm@47945
|
649 |
|-> (set_facts o map (#2 o #2))
|
wenzelm@11891
|
650 |
end;
|
wenzelm@11891
|
651 |
|
wenzelm@16813
|
652 |
in
|
wenzelm@16813
|
653 |
|
wenzelm@43231
|
654 |
val def = gen_def (K I) Proof_Context.cert_vars Proof_Context.match_bind_i;
|
wenzelm@48686
|
655 |
val def_cmd = gen_def Attrib.attribute_cmd Proof_Context.read_vars Proof_Context.match_bind;
|
wenzelm@11891
|
656 |
|
wenzelm@16813
|
657 |
end;
|
wenzelm@16813
|
658 |
|
wenzelm@11891
|
659 |
|
wenzelm@8374
|
660 |
|
wenzelm@17112
|
661 |
(** facts **)
|
wenzelm@5820
|
662 |
|
wenzelm@17359
|
663 |
(* chain *)
|
wenzelm@5820
|
664 |
|
wenzelm@24011
|
665 |
fun clean_facts ctxt =
|
wenzelm@47945
|
666 |
set_facts (filter_out Thm.is_dummy (the_facts ctxt)) ctxt;
|
wenzelm@24011
|
667 |
|
wenzelm@17359
|
668 |
val chain =
|
wenzelm@17359
|
669 |
assert_forward
|
wenzelm@24011
|
670 |
#> clean_facts
|
wenzelm@17359
|
671 |
#> enter_chain;
|
wenzelm@5820
|
672 |
|
wenzelm@17359
|
673 |
fun chain_facts facts =
|
wenzelm@47945
|
674 |
set_facts facts
|
wenzelm@17359
|
675 |
#> chain;
|
wenzelm@5820
|
676 |
|
wenzelm@5820
|
677 |
|
wenzelm@17359
|
678 |
(* note etc. *)
|
wenzelm@17112
|
679 |
|
haftmann@28965
|
680 |
fun no_binding args = map (pair (Binding.empty, [])) args;
|
wenzelm@17112
|
681 |
|
wenzelm@17112
|
682 |
local
|
wenzelm@17112
|
683 |
|
wenzelm@30767
|
684 |
fun gen_thmss more_facts opt_chain opt_result prep_atts prep_fact args state =
|
wenzelm@17112
|
685 |
state
|
wenzelm@17112
|
686 |
|> assert_forward
|
wenzelm@48686
|
687 |
|> map_context_result (fn ctxt => ctxt |> Proof_Context.note_thmss ""
|
wenzelm@48686
|
688 |
(Attrib.map_facts_refs (map (prep_atts ctxt)) (prep_fact ctxt) args))
|
wenzelm@17112
|
689 |
|> these_factss (more_facts state)
|
wenzelm@17359
|
690 |
||> opt_chain
|
wenzelm@17359
|
691 |
|> opt_result;
|
wenzelm@17112
|
692 |
|
wenzelm@17112
|
693 |
in
|
wenzelm@17112
|
694 |
|
wenzelm@36334
|
695 |
val note_thmss = gen_thmss (K []) I #2 (K I) (K I);
|
wenzelm@48686
|
696 |
val note_thmss_cmd = gen_thmss (K []) I #2 Attrib.attribute_cmd Proof_Context.get_fact;
|
wenzelm@17112
|
697 |
|
wenzelm@36334
|
698 |
val from_thmss = gen_thmss (K []) chain #2 (K I) (K I) o no_binding;
|
wenzelm@48686
|
699 |
val from_thmss_cmd =
|
wenzelm@48686
|
700 |
gen_thmss (K []) chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
|
wenzelm@17112
|
701 |
|
wenzelm@36334
|
702 |
val with_thmss = gen_thmss the_facts chain #2 (K I) (K I) o no_binding;
|
wenzelm@48686
|
703 |
val with_thmss_cmd =
|
wenzelm@48686
|
704 |
gen_thmss the_facts chain #2 Attrib.attribute_cmd Proof_Context.get_fact o no_binding;
|
wenzelm@17359
|
705 |
|
wenzelm@30767
|
706 |
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
|
wenzelm@17359
|
707 |
|
wenzelm@17112
|
708 |
end;
|
wenzelm@17112
|
709 |
|
wenzelm@17112
|
710 |
|
wenzelm@18548
|
711 |
(* using/unfolding *)
|
wenzelm@17112
|
712 |
|
wenzelm@17112
|
713 |
local
|
wenzelm@17112
|
714 |
|
wenzelm@46261
|
715 |
fun gen_using f g prep_att prep_fact args state =
|
wenzelm@17112
|
716 |
state
|
wenzelm@17112
|
717 |
|> assert_backward
|
wenzelm@21442
|
718 |
|> map_context_result
|
wenzelm@48686
|
719 |
(fn ctxt => ctxt |> Proof_Context.note_thmss ""
|
wenzelm@48686
|
720 |
(Attrib.map_facts_refs (map (prep_att ctxt)) (prep_fact ctxt) (no_binding args)))
|
wenzelm@18843
|
721 |
|> (fn (named_facts, state') =>
|
wenzelm@24556
|
722 |
state' |> map_goal I (fn (statement, _, using, goal, before_qed, after_qed) =>
|
wenzelm@18843
|
723 |
let
|
wenzelm@18843
|
724 |
val ctxt = context_of state';
|
wenzelm@19482
|
725 |
val ths = maps snd named_facts;
|
wenzelm@48308
|
726 |
in (statement, [], f ctxt ths using, g ctxt ths goal, before_qed, after_qed) end) I);
|
wenzelm@18548
|
727 |
|
wenzelm@24050
|
728 |
fun append_using _ ths using = using @ filter_out Thm.is_dummy ths;
|
wenzelm@35624
|
729 |
fun unfold_using ctxt ths = map (Local_Defs.unfold ctxt ths);
|
wenzelm@35624
|
730 |
val unfold_goals = Local_Defs.unfold_goals;
|
wenzelm@17112
|
731 |
|
wenzelm@17112
|
732 |
in
|
wenzelm@17112
|
733 |
|
wenzelm@36334
|
734 |
val using = gen_using append_using (K (K I)) (K I) (K I);
|
wenzelm@48686
|
735 |
val using_cmd = gen_using append_using (K (K I)) Attrib.attribute_cmd Proof_Context.get_fact;
|
wenzelm@36334
|
736 |
val unfolding = gen_using unfold_using unfold_goals (K I) (K I);
|
wenzelm@48686
|
737 |
val unfolding_cmd = gen_using unfold_using unfold_goals Attrib.attribute_cmd Proof_Context.get_fact;
|
wenzelm@17112
|
738 |
|
wenzelm@17112
|
739 |
end;
|
wenzelm@17112
|
740 |
|
wenzelm@17112
|
741 |
|
wenzelm@17112
|
742 |
(* case *)
|
wenzelm@17112
|
743 |
|
wenzelm@17112
|
744 |
local
|
wenzelm@17112
|
745 |
|
wenzelm@30420
|
746 |
fun qualified_binding a =
|
wenzelm@30420
|
747 |
Binding.qualify true (Long_Name.qualifier a) (Binding.name (Long_Name.base_name a));
|
wenzelm@30420
|
748 |
|
wenzelm@17112
|
749 |
fun gen_invoke_case prep_att (name, xs, raw_atts) state =
|
wenzelm@17112
|
750 |
let
|
wenzelm@48686
|
751 |
val atts = map (prep_att (context_of state)) raw_atts;
|
wenzelm@19078
|
752 |
val (asms, state') = state |> map_context_result (fn ctxt =>
|
wenzelm@43231
|
753 |
ctxt |> Proof_Context.apply_case (Proof_Context.get_case ctxt name xs));
|
wenzelm@30420
|
754 |
val assumptions = asms |> map (fn (a, ts) => ((qualified_binding a, atts), map (rpair []) ts));
|
wenzelm@17112
|
755 |
in
|
wenzelm@17112
|
756 |
state'
|
wenzelm@36334
|
757 |
|> assume assumptions
|
wenzelm@33386
|
758 |
|> bind_terms Auto_Bind.no_facts
|
wenzelm@36334
|
759 |
|> `the_facts |-> (fn thms => note_thmss [((Binding.name name, []), [(thms, [])])])
|
wenzelm@17112
|
760 |
end;
|
wenzelm@17112
|
761 |
|
wenzelm@17112
|
762 |
in
|
wenzelm@17112
|
763 |
|
wenzelm@36334
|
764 |
val invoke_case = gen_invoke_case (K I);
|
wenzelm@48686
|
765 |
val invoke_case_cmd = gen_invoke_case Attrib.attribute_cmd;
|
wenzelm@17112
|
766 |
|
wenzelm@17112
|
767 |
end;
|
wenzelm@17112
|
768 |
|
wenzelm@17112
|
769 |
|
wenzelm@17112
|
770 |
|
wenzelm@17359
|
771 |
(** proof structure **)
|
wenzelm@17359
|
772 |
|
wenzelm@17359
|
773 |
(* blocks *)
|
wenzelm@17359
|
774 |
|
wenzelm@17359
|
775 |
val begin_block =
|
wenzelm@17359
|
776 |
assert_forward
|
wenzelm@17359
|
777 |
#> open_block
|
wenzelm@47945
|
778 |
#> reset_goal
|
wenzelm@17359
|
779 |
#> open_block;
|
wenzelm@17359
|
780 |
|
wenzelm@17359
|
781 |
val next_block =
|
wenzelm@17359
|
782 |
assert_forward
|
wenzelm@17359
|
783 |
#> close_block
|
wenzelm@17359
|
784 |
#> open_block
|
wenzelm@47945
|
785 |
#> reset_goal
|
wenzelm@47945
|
786 |
#> reset_facts;
|
wenzelm@17359
|
787 |
|
wenzelm@17359
|
788 |
fun end_block state =
|
wenzelm@17359
|
789 |
state
|
wenzelm@17359
|
790 |
|> assert_forward
|
wenzelm@41208
|
791 |
|> assert_bottom false
|
wenzelm@17359
|
792 |
|> close_block
|
wenzelm@17359
|
793 |
|> assert_current_goal false
|
wenzelm@17359
|
794 |
|> close_block
|
wenzelm@17359
|
795 |
|> export_facts state;
|
wenzelm@17359
|
796 |
|
wenzelm@17359
|
797 |
|
wenzelm@41208
|
798 |
(* global notepad *)
|
wenzelm@41208
|
799 |
|
wenzelm@41208
|
800 |
val begin_notepad =
|
wenzelm@41208
|
801 |
init
|
wenzelm@41208
|
802 |
#> open_block
|
wenzelm@41208
|
803 |
#> map_context (Variable.set_body true)
|
wenzelm@41208
|
804 |
#> open_block;
|
wenzelm@41208
|
805 |
|
wenzelm@41208
|
806 |
val end_notepad =
|
wenzelm@41208
|
807 |
assert_forward
|
wenzelm@41208
|
808 |
#> assert_bottom true
|
wenzelm@41208
|
809 |
#> close_block
|
wenzelm@41208
|
810 |
#> assert_current_goal false
|
wenzelm@41208
|
811 |
#> close_block
|
wenzelm@41208
|
812 |
#> context_of;
|
wenzelm@41208
|
813 |
|
wenzelm@41208
|
814 |
|
wenzelm@17359
|
815 |
(* sub-proofs *)
|
wenzelm@17359
|
816 |
|
wenzelm@17359
|
817 |
fun proof opt_text =
|
wenzelm@17359
|
818 |
assert_backward
|
wenzelm@17859
|
819 |
#> refine (the_default Method.default_text opt_text)
|
wenzelm@17359
|
820 |
#> Seq.map (using_facts [] #> enter_forward);
|
wenzelm@17359
|
821 |
|
wenzelm@50881
|
822 |
fun proof_results arg =
|
wenzelm@50881
|
823 |
Seq.APPEND (proof (Method.text arg) #> Seq.make_results,
|
wenzelm@50881
|
824 |
method_error "initial" (Method.position arg));
|
wenzelm@50878
|
825 |
|
wenzelm@50904
|
826 |
fun end_proof bot (prev_pos, (opt_text, immed)) =
|
wenzelm@50904
|
827 |
let
|
wenzelm@50904
|
828 |
val (finish_text, terminal_pos, finished_pos) =
|
wenzelm@50904
|
829 |
(case opt_text of
|
wenzelm@50904
|
830 |
NONE => (Method.finish_text (NONE, immed), Position.none, prev_pos)
|
wenzelm@51927
|
831 |
| SOME (text, (pos, end_pos)) =>
|
wenzelm@51927
|
832 |
(Method.finish_text (SOME text, immed), Position.set_range (pos, end_pos), end_pos));
|
wenzelm@50904
|
833 |
in
|
wenzelm@50904
|
834 |
Seq.APPEND (fn state =>
|
wenzelm@50904
|
835 |
state
|
wenzelm@50904
|
836 |
|> assert_forward
|
wenzelm@50904
|
837 |
|> assert_bottom bot
|
wenzelm@50904
|
838 |
|> close_block
|
wenzelm@50904
|
839 |
|> assert_current_goal true
|
wenzelm@50904
|
840 |
|> using_facts []
|
wenzelm@50904
|
841 |
|> `before_qed |-> (refine o the_default Method.succeed_text)
|
wenzelm@50904
|
842 |
|> Seq.maps (refine finish_text)
|
wenzelm@50904
|
843 |
|> Seq.make_results, method_error "terminal" terminal_pos)
|
wenzelm@50904
|
844 |
#> Seq.maps_results (Seq.single o finished_goal finished_pos)
|
wenzelm@50904
|
845 |
end;
|
wenzelm@17359
|
846 |
|
wenzelm@29383
|
847 |
fun check_result msg sq =
|
wenzelm@29383
|
848 |
(case Seq.pull sq of
|
wenzelm@29383
|
849 |
NONE => error msg
|
wenzelm@29383
|
850 |
| SOME (s, _) => s);
|
wenzelm@29383
|
851 |
|
wenzelm@17359
|
852 |
|
wenzelm@17359
|
853 |
(* unstructured refinement *)
|
wenzelm@17359
|
854 |
|
wenzelm@50880
|
855 |
fun defer i =
|
wenzelm@50880
|
856 |
assert_no_chain #>
|
wenzelm@50880
|
857 |
refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL defer_tac i))) #> Seq.hd;
|
wenzelm@50880
|
858 |
|
wenzelm@50880
|
859 |
fun prefer i =
|
wenzelm@50880
|
860 |
assert_no_chain #>
|
wenzelm@50880
|
861 |
refine (Method.Basic (fn _ => METHOD (fn _ => ASSERT_SUBGOAL prefer_tac i))) #> Seq.hd;
|
wenzelm@17359
|
862 |
|
wenzelm@17359
|
863 |
fun apply text = assert_backward #> refine text #> Seq.map (using_facts []);
|
wenzelm@50881
|
864 |
|
wenzelm@17359
|
865 |
fun apply_end text = assert_forward #> refine_end text;
|
wenzelm@17359
|
866 |
|
wenzelm@50904
|
867 |
fun apply_results (text, range) =
|
wenzelm@50904
|
868 |
Seq.APPEND (apply text #> Seq.make_results, method_error "" (Position.set_range range));
|
wenzelm@50881
|
869 |
|
wenzelm@50904
|
870 |
fun apply_end_results (text, range) =
|
wenzelm@50904
|
871 |
Seq.APPEND (apply_end text #> Seq.make_results, method_error "" (Position.set_range range));
|
wenzelm@50878
|
872 |
|
wenzelm@17359
|
873 |
|
wenzelm@17359
|
874 |
|
wenzelm@17112
|
875 |
(** goals **)
|
wenzelm@17112
|
876 |
|
wenzelm@17359
|
877 |
(* generic goals *)
|
wenzelm@17359
|
878 |
|
wenzelm@19774
|
879 |
local
|
wenzelm@17359
|
880 |
|
wenzelm@36333
|
881 |
val is_var =
|
wenzelm@36333
|
882 |
can (dest_TVar o Logic.dest_type o Logic.dest_term) orf
|
wenzelm@36333
|
883 |
can (dest_Var o Logic.dest_term);
|
wenzelm@36333
|
884 |
|
wenzelm@36333
|
885 |
fun implicit_vars props =
|
wenzelm@19846
|
886 |
let
|
wenzelm@36364
|
887 |
val (var_props, _) = take_prefix is_var props;
|
wenzelm@36333
|
888 |
val explicit_vars = fold Term.add_vars var_props [];
|
wenzelm@36333
|
889 |
val vars = filter_out (member (op =) explicit_vars) (fold Term.add_vars props []);
|
wenzelm@36333
|
890 |
in map (Logic.mk_term o Var) vars end;
|
wenzelm@19774
|
891 |
|
wenzelm@19774
|
892 |
fun refine_terms n =
|
wenzelm@30515
|
893 |
refine (Method.Basic (K (RAW_METHOD
|
wenzelm@19774
|
894 |
(K (HEADGOAL (PRECISE_CONJUNCTS n
|
wenzelm@32193
|
895 |
(HEADGOAL (CONJUNCTS (ALLGOALS (rtac Drule.termI))))))))))
|
wenzelm@19774
|
896 |
#> Seq.hd;
|
wenzelm@19774
|
897 |
|
wenzelm@19774
|
898 |
in
|
wenzelm@17359
|
899 |
|
wenzelm@17859
|
900 |
fun generic_goal prepp kind before_qed after_qed raw_propp state =
|
wenzelm@5936
|
901 |
let
|
wenzelm@17359
|
902 |
val thy = theory_of state;
|
wenzelm@23418
|
903 |
val cert = Thm.cterm_of thy;
|
wenzelm@17359
|
904 |
val chaining = can assert_chain state;
|
wenzelm@25958
|
905 |
val pos = Position.thread_data ();
|
wenzelm@17359
|
906 |
|
wenzelm@17359
|
907 |
val ((propss, after_ctxt), goal_state) =
|
wenzelm@5936
|
908 |
state
|
wenzelm@5936
|
909 |
|> assert_forward_or_chain
|
wenzelm@5936
|
910 |
|> enter_forward
|
wenzelm@17359
|
911 |
|> open_block
|
wenzelm@46203
|
912 |
|> map_context_result (prepp raw_propp);
|
wenzelm@19482
|
913 |
val props = flat propss;
|
wenzelm@15703
|
914 |
|
wenzelm@36333
|
915 |
val vars = implicit_vars props;
|
wenzelm@36333
|
916 |
val propss' = vars :: propss;
|
wenzelm@23418
|
917 |
val goal_propss = filter_out null propss';
|
wenzelm@29346
|
918 |
val goal =
|
wenzelm@29346
|
919 |
cert (Logic.mk_conjunction_balanced (map Logic.mk_conjunction_balanced goal_propss))
|
wenzelm@28627
|
920 |
|> Thm.weaken_sorts (Variable.sorts_of (context_of goal_state));
|
wenzelm@29346
|
921 |
val statement = ((kind, pos), propss', Thm.term_of goal);
|
wenzelm@18124
|
922 |
val after_qed' = after_qed |>> (fn after_local =>
|
wenzelm@18124
|
923 |
fn results => map_context after_ctxt #> after_local results);
|
wenzelm@5820
|
924 |
in
|
wenzelm@17359
|
925 |
goal_state
|
wenzelm@21727
|
926 |
|> map_context (init_context #> Variable.set_body true)
|
wenzelm@47945
|
927 |
|> set_goal (make_goal (statement, [], [], Goal.init goal, before_qed, after_qed'))
|
wenzelm@43231
|
928 |
|> map_context (Proof_Context.auto_bind_goal props)
|
wenzelm@21565
|
929 |
|> chaining ? (`the_facts #-> using_facts)
|
wenzelm@47945
|
930 |
|> reset_facts
|
wenzelm@17359
|
931 |
|> open_block
|
wenzelm@47945
|
932 |
|> reset_goal
|
wenzelm@5820
|
933 |
|> enter_backward
|
wenzelm@23418
|
934 |
|> not (null vars) ? refine_terms (length goal_propss)
|
wenzelm@32193
|
935 |
|> null props ? (refine (Method.Basic Method.assumption) #> Seq.hd)
|
wenzelm@5820
|
936 |
end;
|
wenzelm@5820
|
937 |
|
wenzelm@29090
|
938 |
fun generic_qed after_ctxt state =
|
wenzelm@12503
|
939 |
let
|
wenzelm@36364
|
940 |
val (goal_ctxt, {statement = (_, stmt, _), goal, after_qed, ...}) = current_goal state;
|
wenzelm@8617
|
941 |
val outer_state = state |> close_block;
|
wenzelm@8617
|
942 |
val outer_ctxt = context_of outer_state;
|
wenzelm@8617
|
943 |
|
wenzelm@18503
|
944 |
val props =
|
wenzelm@19774
|
945 |
flat (tl stmt)
|
wenzelm@19915
|
946 |
|> Variable.exportT_terms goal_ctxt outer_ctxt;
|
wenzelm@17359
|
947 |
val results =
|
wenzelm@28627
|
948 |
tl (conclude_goal goal_ctxt goal stmt)
|
wenzelm@43231
|
949 |
|> burrow (Proof_Context.export goal_ctxt outer_ctxt);
|
wenzelm@5820
|
950 |
in
|
wenzelm@8617
|
951 |
outer_state
|
wenzelm@29090
|
952 |
|> map_context (after_ctxt props)
|
wenzelm@34247
|
953 |
|> pair (after_qed, results)
|
wenzelm@5820
|
954 |
end;
|
wenzelm@5820
|
955 |
|
wenzelm@19774
|
956 |
end;
|
wenzelm@19774
|
957 |
|
wenzelm@5820
|
958 |
|
wenzelm@17359
|
959 |
(* local goals *)
|
wenzelm@5820
|
960 |
|
wenzelm@17859
|
961 |
fun local_goal print_results prep_att prepp kind before_qed after_qed stmt state =
|
wenzelm@17359
|
962 |
let
|
wenzelm@21362
|
963 |
val ((names, attss), propp) =
|
wenzelm@48686
|
964 |
Attrib.map_specs (map (prep_att (context_of state))) stmt |> split_list |>> split_list;
|
wenzelm@17359
|
965 |
|
wenzelm@18124
|
966 |
fun after_qed' results =
|
wenzelm@18808
|
967 |
local_results ((names ~~ attss) ~~ results)
|
wenzelm@17359
|
968 |
#-> (fn res => tap (fn st => print_results (context_of st) ((kind, ""), res) : unit))
|
wenzelm@18124
|
969 |
#> after_qed results;
|
wenzelm@17359
|
970 |
in
|
wenzelm@17359
|
971 |
state
|
wenzelm@21362
|
972 |
|> generic_goal prepp kind before_qed (after_qed', K I) propp
|
wenzelm@19900
|
973 |
|> tap (Variable.warn_extra_tfrees (context_of state) o context_of)
|
wenzelm@17359
|
974 |
end;
|
wenzelm@17359
|
975 |
|
wenzelm@50881
|
976 |
fun local_qeds arg =
|
wenzelm@50881
|
977 |
end_proof false arg
|
wenzelm@50874
|
978 |
#> Seq.map_result (generic_qed Proof_Context.auto_bind_facts #->
|
wenzelm@50874
|
979 |
(fn ((after_qed, _), results) => after_qed results));
|
wenzelm@17359
|
980 |
|
wenzelm@50904
|
981 |
fun local_qed arg =
|
wenzelm@50904
|
982 |
local_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
|
wenzelm@29383
|
983 |
|
wenzelm@17359
|
984 |
|
wenzelm@17359
|
985 |
(* global goals *)
|
wenzelm@17359
|
986 |
|
wenzelm@46203
|
987 |
fun prepp_auto_fixes prepp args =
|
wenzelm@46203
|
988 |
prepp args #>
|
wenzelm@46203
|
989 |
(fn ((propss, a), ctxt) => ((propss, a), (fold o fold) Variable.auto_fixes propss ctxt));
|
wenzelm@46203
|
990 |
|
wenzelm@46203
|
991 |
fun global_goal prepp before_qed after_qed propp =
|
wenzelm@46203
|
992 |
init #>
|
wenzelm@46203
|
993 |
generic_goal (prepp_auto_fixes prepp) "" before_qed (K I, after_qed) propp;
|
wenzelm@17359
|
994 |
|
wenzelm@43231
|
995 |
val theorem = global_goal Proof_Context.bind_propp_schematic_i;
|
wenzelm@43231
|
996 |
val theorem_cmd = global_goal Proof_Context.bind_propp_schematic;
|
wenzelm@12065
|
997 |
|
wenzelm@50881
|
998 |
fun global_qeds arg =
|
wenzelm@50881
|
999 |
end_proof true arg
|
wenzelm@50874
|
1000 |
#> Seq.map_result (generic_qed (K I) #> (fn (((_, after_qed), results), state) =>
|
wenzelm@50874
|
1001 |
after_qed results (context_of state)));
|
wenzelm@5820
|
1002 |
|
wenzelm@50904
|
1003 |
fun global_qed arg =
|
wenzelm@50904
|
1004 |
global_qeds (Position.none, arg) #> Seq.the_result finished_goal_error;
|
wenzelm@17112
|
1005 |
|
wenzelm@17112
|
1006 |
|
wenzelm@50922
|
1007 |
(* terminal proof steps *)
|
wenzelm@17112
|
1008 |
|
wenzelm@50905
|
1009 |
local
|
wenzelm@50905
|
1010 |
|
wenzelm@50861
|
1011 |
fun terminal_proof qeds initial terminal =
|
wenzelm@50904
|
1012 |
proof_results (SOME initial) #> Seq.maps_results (qeds (#2 (#2 initial), terminal))
|
wenzelm@50878
|
1013 |
#> Seq.the_result "";
|
wenzelm@50863
|
1014 |
|
wenzelm@50905
|
1015 |
in
|
wenzelm@50905
|
1016 |
|
wenzelm@29383
|
1017 |
fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
|
wenzelm@50904
|
1018 |
val local_default_proof = local_terminal_proof ((Method.default_text, Position.no_range), NONE);
|
wenzelm@50904
|
1019 |
val local_immediate_proof = local_terminal_proof ((Method.this_text, Position.no_range), NONE);
|
wenzelm@50904
|
1020 |
val local_done_proof = terminal_proof local_qeds (Method.done_text, Position.no_range) (NONE, false);
|
wenzelm@17112
|
1021 |
|
wenzelm@29383
|
1022 |
fun global_terminal_proof (text, opt_text) = terminal_proof global_qeds text (opt_text, true);
|
wenzelm@50904
|
1023 |
val global_default_proof = global_terminal_proof ((Method.default_text, Position.no_range), NONE);
|
wenzelm@50904
|
1024 |
val global_immediate_proof = global_terminal_proof ((Method.this_text, Position.no_range), NONE);
|
wenzelm@50904
|
1025 |
val global_done_proof = terminal_proof global_qeds (Method.done_text, Position.no_range) (NONE, false);
|
wenzelm@17112
|
1026 |
|
wenzelm@50905
|
1027 |
end;
|
wenzelm@50905
|
1028 |
|
wenzelm@17112
|
1029 |
|
wenzelm@50922
|
1030 |
(* skip proofs *)
|
wenzelm@50922
|
1031 |
|
wenzelm@50922
|
1032 |
local
|
wenzelm@50922
|
1033 |
|
wenzelm@50922
|
1034 |
fun skipped_proof state =
|
wenzelm@52016
|
1035 |
Context_Position.if_visible (context_of state) Output.report
|
wenzelm@52016
|
1036 |
(Markup.markup Markup.bad "Skipped proof");
|
wenzelm@50922
|
1037 |
|
wenzelm@50922
|
1038 |
in
|
wenzelm@50922
|
1039 |
|
wenzelm@50922
|
1040 |
fun local_skip_proof int state =
|
wenzelm@50922
|
1041 |
local_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
|
wenzelm@50922
|
1042 |
skipped_proof state;
|
wenzelm@50922
|
1043 |
|
wenzelm@50922
|
1044 |
fun global_skip_proof int state =
|
wenzelm@50922
|
1045 |
global_terminal_proof ((Method.sorry_text int, Position.no_range), NONE) state before
|
wenzelm@50922
|
1046 |
skipped_proof state;
|
wenzelm@50922
|
1047 |
|
wenzelm@50922
|
1048 |
end;
|
wenzelm@50922
|
1049 |
|
wenzelm@50922
|
1050 |
|
wenzelm@17359
|
1051 |
(* common goal statements *)
|
wenzelm@17112
|
1052 |
|
wenzelm@17359
|
1053 |
local
|
wenzelm@17112
|
1054 |
|
wenzelm@17859
|
1055 |
fun gen_have prep_att prepp before_qed after_qed stmt int =
|
wenzelm@51216
|
1056 |
local_goal (Proof_Display.print_results Markup.state int)
|
wenzelm@47602
|
1057 |
prep_att prepp "have" before_qed after_qed stmt;
|
wenzelm@5820
|
1058 |
|
wenzelm@17859
|
1059 |
fun gen_show prep_att prepp before_qed after_qed stmt int state =
|
wenzelm@17359
|
1060 |
let
|
wenzelm@32738
|
1061 |
val testing = Unsynchronized.ref false;
|
wenzelm@32738
|
1062 |
val rule = Unsynchronized.ref (NONE: thm option);
|
wenzelm@17359
|
1063 |
fun fail_msg ctxt =
|
wenzelm@51330
|
1064 |
"Local statement fails to refine any pending goal" ::
|
wenzelm@33389
|
1065 |
(case ! rule of NONE => [] | SOME th => [Proof_Display.string_of_rule ctxt "Failed" th])
|
wenzelm@17359
|
1066 |
|> cat_lines;
|
wenzelm@5820
|
1067 |
|
wenzelm@17359
|
1068 |
fun print_results ctxt res =
|
wenzelm@47602
|
1069 |
if ! testing then ()
|
wenzelm@51216
|
1070 |
else Proof_Display.print_results Markup.state int ctxt res;
|
wenzelm@17359
|
1071 |
fun print_rule ctxt th =
|
wenzelm@17359
|
1072 |
if ! testing then rule := SOME th
|
wenzelm@41429
|
1073 |
else if int then
|
wenzelm@51216
|
1074 |
writeln (Markup.markup Markup.state (Proof_Display.string_of_rule ctxt "Successful" th))
|
wenzelm@17359
|
1075 |
else ();
|
wenzelm@17359
|
1076 |
val test_proof =
|
wenzelm@51330
|
1077 |
local_skip_proof true
|
wenzelm@39862
|
1078 |
|> Unsynchronized.setmp testing true
|
wenzelm@42923
|
1079 |
|> Exn.interruptible_capture;
|
wenzelm@6896
|
1080 |
|
wenzelm@18124
|
1081 |
fun after_qed' results =
|
wenzelm@19482
|
1082 |
refine_goals print_rule (context_of state) (flat results)
|
wenzelm@29383
|
1083 |
#> check_result "Failed to refine any pending goal"
|
wenzelm@29383
|
1084 |
#> after_qed results;
|
wenzelm@17359
|
1085 |
in
|
wenzelm@17359
|
1086 |
state
|
wenzelm@17859
|
1087 |
|> local_goal print_results prep_att prepp "show" before_qed after_qed' stmt
|
wenzelm@21565
|
1088 |
|> int ? (fn goal_state =>
|
wenzelm@50922
|
1089 |
(case test_proof (map_context (Context_Position.set_visible false) goal_state) of
|
wenzelm@51330
|
1090 |
Exn.Res _ => goal_state
|
wenzelm@42923
|
1091 |
| Exn.Exn exn => raise Exn.EXCEPTIONS ([exn, ERROR (fail_msg (context_of goal_state))])))
|
wenzelm@17359
|
1092 |
end;
|
wenzelm@6896
|
1093 |
|
wenzelm@17359
|
1094 |
in
|
wenzelm@6896
|
1095 |
|
wenzelm@43231
|
1096 |
val have = gen_have (K I) Proof_Context.bind_propp_i;
|
wenzelm@48686
|
1097 |
val have_cmd = gen_have Attrib.attribute_cmd Proof_Context.bind_propp;
|
wenzelm@43231
|
1098 |
val show = gen_show (K I) Proof_Context.bind_propp_i;
|
wenzelm@48686
|
1099 |
val show_cmd = gen_show Attrib.attribute_cmd Proof_Context.bind_propp;
|
wenzelm@6896
|
1100 |
|
wenzelm@5820
|
1101 |
end;
|
wenzelm@17359
|
1102 |
|
wenzelm@28410
|
1103 |
|
wenzelm@29385
|
1104 |
|
wenzelm@29385
|
1105 |
(** future proofs **)
|
wenzelm@29385
|
1106 |
|
wenzelm@29385
|
1107 |
(* relevant proof states *)
|
wenzelm@29385
|
1108 |
|
wenzelm@29385
|
1109 |
fun is_schematic t =
|
wenzelm@29385
|
1110 |
Term.exists_subterm Term.is_Var t orelse
|
wenzelm@29385
|
1111 |
Term.exists_type (Term.exists_subtype Term.is_TVar) t;
|
wenzelm@29385
|
1112 |
|
wenzelm@29385
|
1113 |
fun schematic_goal state =
|
wenzelm@29385
|
1114 |
let val (_, (_, {statement = (_, _, prop), ...})) = find_goal state
|
wenzelm@29385
|
1115 |
in is_schematic prop end;
|
wenzelm@29385
|
1116 |
|
wenzelm@29385
|
1117 |
fun is_relevant state =
|
wenzelm@29385
|
1118 |
(case try find_goal state of
|
wenzelm@29385
|
1119 |
NONE => true
|
wenzelm@29385
|
1120 |
| SOME (_, (_, {statement = (_, _, prop), goal, ...})) =>
|
wenzelm@29385
|
1121 |
is_schematic prop orelse not (Logic.protect prop aconv Thm.concl_of goal));
|
wenzelm@29385
|
1122 |
|
wenzelm@29385
|
1123 |
|
wenzelm@29385
|
1124 |
(* full proofs *)
|
wenzelm@28410
|
1125 |
|
wenzelm@29346
|
1126 |
local
|
wenzelm@29346
|
1127 |
|
wenzelm@50927
|
1128 |
structure Result = Proof_Data
|
wenzelm@50927
|
1129 |
(
|
wenzelm@50927
|
1130 |
type T = thm option;
|
wenzelm@50927
|
1131 |
val empty = NONE;
|
wenzelm@50927
|
1132 |
fun init _ = empty;
|
wenzelm@50927
|
1133 |
);
|
wenzelm@50927
|
1134 |
|
wenzelm@50927
|
1135 |
fun the_result ctxt =
|
wenzelm@50927
|
1136 |
(case Result.get ctxt of
|
wenzelm@50927
|
1137 |
NONE => error "No result of forked proof"
|
wenzelm@50927
|
1138 |
| SOME th => th);
|
wenzelm@50927
|
1139 |
|
wenzelm@50927
|
1140 |
val set_result = Result.put o SOME;
|
wenzelm@50927
|
1141 |
val reset_result = Result.put NONE;
|
wenzelm@50927
|
1142 |
|
wenzelm@29385
|
1143 |
fun future_proof done get_context fork_proof state =
|
wenzelm@28410
|
1144 |
let
|
wenzelm@29381
|
1145 |
val _ = assert_backward state;
|
wenzelm@28410
|
1146 |
val (goal_ctxt, (_, goal)) = find_goal state;
|
wenzelm@32793
|
1147 |
val {statement as (kind, _, prop), messages, using, goal, before_qed, after_qed} = goal;
|
wenzelm@48308
|
1148 |
val goal_tfrees =
|
wenzelm@48308
|
1149 |
fold Term.add_tfrees
|
wenzelm@48308
|
1150 |
(prop :: map Thm.term_of (Assumption.all_assms_of goal_ctxt)) [];
|
wenzelm@28410
|
1151 |
|
wenzelm@29383
|
1152 |
val _ = is_relevant state andalso error "Cannot fork relevant proof";
|
wenzelm@29383
|
1153 |
|
wenzelm@29346
|
1154 |
val prop' = Logic.protect prop;
|
wenzelm@29346
|
1155 |
val statement' = (kind, [[], [prop']], prop');
|
wenzelm@29346
|
1156 |
val goal' = Thm.adjust_maxidx_thm (Thm.maxidx_of goal)
|
wenzelm@29346
|
1157 |
(Drule.comp_no_flatten (goal, Thm.nprems_of goal) 1 Drule.protectI);
|
wenzelm@50927
|
1158 |
val after_qed' = (fn [[th]] => map_context (set_result th), fn [[th]] => set_result th);
|
wenzelm@28410
|
1159 |
|
wenzelm@28973
|
1160 |
val result_ctxt =
|
wenzelm@28973
|
1161 |
state
|
wenzelm@50927
|
1162 |
|> map_context reset_result
|
wenzelm@29385
|
1163 |
|> map_goal I (K (statement', messages, using, goal', before_qed, after_qed'))
|
wenzelm@48308
|
1164 |
(fold (Variable.declare_typ o TFree) goal_tfrees)
|
wenzelm@29346
|
1165 |
|> fork_proof;
|
wenzelm@28973
|
1166 |
|
wenzelm@50927
|
1167 |
val future_thm = result_ctxt |> Future.map (fn (_, x) => the_result (get_context x));
|
wenzelm@32078
|
1168 |
val finished_goal = Goal.future_result goal_ctxt future_thm prop';
|
wenzelm@28973
|
1169 |
val state' =
|
wenzelm@28973
|
1170 |
state
|
wenzelm@48308
|
1171 |
|> map_goal I (K (statement, messages, using, finished_goal, NONE, after_qed)) I
|
wenzelm@29385
|
1172 |
|> done;
|
wenzelm@28973
|
1173 |
in (Future.map #1 result_ctxt, state') end;
|
wenzelm@28410
|
1174 |
|
wenzelm@29385
|
1175 |
in
|
wenzelm@29385
|
1176 |
|
wenzelm@29385
|
1177 |
fun local_future_proof x = future_proof local_done_proof context_of x;
|
wenzelm@29385
|
1178 |
fun global_future_proof x = future_proof global_done_proof I x;
|
wenzelm@29385
|
1179 |
|
wenzelm@17359
|
1180 |
end;
|
wenzelm@29346
|
1181 |
|
wenzelm@29385
|
1182 |
|
wenzelm@29385
|
1183 |
(* terminal proofs *)
|
wenzelm@29385
|
1184 |
|
wenzelm@29385
|
1185 |
local
|
wenzelm@29385
|
1186 |
|
wenzelm@50027
|
1187 |
fun future_terminal_proof n proof1 proof2 meths int state =
|
wenzelm@50027
|
1188 |
if (Goal.future_enabled_level 4 orelse Goal.future_enabled_nested n andalso not int)
|
wenzelm@50027
|
1189 |
andalso not (is_relevant state)
|
wenzelm@50027
|
1190 |
then
|
wenzelm@50027
|
1191 |
snd (proof2 (fn state' =>
|
wenzelm@52359
|
1192 |
Goal.fork_name "Proof.future_terminal_proof" ~1 (fn () => ((), proof1 meths state'))) state)
|
wenzelm@50027
|
1193 |
else proof1 meths state;
|
wenzelm@29385
|
1194 |
|
wenzelm@29385
|
1195 |
in
|
wenzelm@29385
|
1196 |
|
wenzelm@29385
|
1197 |
fun local_future_terminal_proof x =
|
wenzelm@50027
|
1198 |
future_terminal_proof 2 local_terminal_proof local_future_proof x;
|
wenzelm@29385
|
1199 |
|
wenzelm@29385
|
1200 |
fun global_future_terminal_proof x =
|
wenzelm@50027
|
1201 |
future_terminal_proof 3 global_terminal_proof global_future_proof x;
|
wenzelm@29350
|
1202 |
|
wenzelm@29346
|
1203 |
end;
|
wenzelm@29346
|
1204 |
|
wenzelm@29385
|
1205 |
end;
|
wenzelm@29385
|
1206 |
|