wenzelm@5820
|
1 |
(* Title: Pure/Isar/proof.ML
|
wenzelm@5820
|
2 |
ID: $Id$
|
wenzelm@5820
|
3 |
Author: Markus Wenzel, TU Muenchen
|
wenzelm@8807
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
wenzelm@5820
|
5 |
|
wenzelm@5820
|
6 |
Proof states and methods.
|
wenzelm@5820
|
7 |
*)
|
wenzelm@5820
|
8 |
|
wenzelm@8152
|
9 |
signature BASIC_PROOF =
|
wenzelm@8152
|
10 |
sig
|
wenzelm@8374
|
11 |
val FINDGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
|
wenzelm@8374
|
12 |
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq
|
wenzelm@8152
|
13 |
end;
|
wenzelm@8152
|
14 |
|
wenzelm@5820
|
15 |
signature PROOF =
|
wenzelm@5820
|
16 |
sig
|
wenzelm@8152
|
17 |
include BASIC_PROOF
|
wenzelm@5820
|
18 |
type context
|
wenzelm@5820
|
19 |
type state
|
wenzelm@5820
|
20 |
exception STATE of string * state
|
wenzelm@6871
|
21 |
val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
|
wenzelm@12045
|
22 |
val init_state: theory -> state
|
wenzelm@5820
|
23 |
val context_of: state -> context
|
wenzelm@5820
|
24 |
val theory_of: state -> theory
|
wenzelm@5820
|
25 |
val sign_of: state -> Sign.sg
|
wenzelm@13377
|
26 |
val map_context: (context -> context) -> state -> state
|
wenzelm@7924
|
27 |
val warn_extra_tfrees: state -> state -> state
|
wenzelm@7605
|
28 |
val reset_thms: string -> state -> state
|
wenzelm@6091
|
29 |
val the_facts: state -> thm list
|
wenzelm@9469
|
30 |
val the_fact: state -> thm
|
wenzelm@11079
|
31 |
val get_goal: state -> context * (thm list * thm)
|
wenzelm@6091
|
32 |
val goal_facts: (state -> thm list) -> state -> state
|
wenzelm@5820
|
33 |
val use_facts: state -> state
|
wenzelm@5820
|
34 |
val reset_facts: state -> state
|
wenzelm@9469
|
35 |
val is_chain: state -> bool
|
wenzelm@6891
|
36 |
val assert_forward: state -> state
|
wenzelm@9469
|
37 |
val assert_forward_or_chain: state -> state
|
wenzelm@5820
|
38 |
val assert_backward: state -> state
|
wenzelm@8206
|
39 |
val assert_no_chain: state -> state
|
wenzelm@5820
|
40 |
val enter_forward: state -> state
|
wenzelm@6529
|
41 |
val verbose: bool ref
|
nipkow@13698
|
42 |
val show_main_goal: bool ref
|
wenzelm@12423
|
43 |
val pretty_state: int -> state -> Pretty.T list
|
wenzelm@10360
|
44 |
val pretty_goals: bool -> state -> Pretty.T list
|
wenzelm@6776
|
45 |
val level: state -> int
|
wenzelm@5820
|
46 |
type method
|
wenzelm@6848
|
47 |
val method: (thm list -> tactic) -> method
|
wenzelm@8374
|
48 |
val method_cases: (thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq) -> method
|
wenzelm@5820
|
49 |
val refine: (context -> method) -> state -> state Seq.seq
|
wenzelm@8234
|
50 |
val refine_end: (context -> method) -> state -> state Seq.seq
|
wenzelm@5936
|
51 |
val match_bind: (string list * string) list -> state -> state
|
wenzelm@5936
|
52 |
val match_bind_i: (term list * term) list -> state -> state
|
wenzelm@8617
|
53 |
val let_bind: (string list * string) list -> state -> state
|
wenzelm@8617
|
54 |
val let_bind_i: (term list * term) list -> state -> state
|
wenzelm@6876
|
55 |
val simple_have_thms: string -> thm list -> state -> state
|
wenzelm@12714
|
56 |
val have_thmss: ((bstring * context attribute list) *
|
wenzelm@12714
|
57 |
(xstring * context attribute list) list) list -> state -> state
|
wenzelm@12714
|
58 |
val have_thmss_i: ((bstring * context attribute list) *
|
wenzelm@9196
|
59 |
(thm list * context attribute list) list) list -> state -> state
|
wenzelm@12714
|
60 |
val with_thmss: ((bstring * context attribute list) *
|
wenzelm@12714
|
61 |
(xstring * context attribute list) list) list -> state -> state
|
wenzelm@12714
|
62 |
val with_thmss_i: ((bstring * context attribute list) *
|
wenzelm@9196
|
63 |
(thm list * context attribute list) list) list -> state -> state
|
wenzelm@12930
|
64 |
val using_thmss: ((xstring * context attribute list) list) list -> state -> state
|
wenzelm@12930
|
65 |
val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state
|
wenzelm@7412
|
66 |
val fix: (string list * string option) list -> state -> state
|
wenzelm@7665
|
67 |
val fix_i: (string list * typ option) list -> state -> state
|
wenzelm@9469
|
68 |
val assm: ProofContext.exporter
|
wenzelm@10464
|
69 |
-> ((string * context attribute list) * (string * (string list * string list)) list) list
|
wenzelm@6932
|
70 |
-> state -> state
|
wenzelm@9469
|
71 |
val assm_i: ProofContext.exporter
|
wenzelm@10464
|
72 |
-> ((string * context attribute list) * (term * (term list * term list)) list) list
|
wenzelm@6932
|
73 |
-> state -> state
|
wenzelm@10464
|
74 |
val assume:
|
wenzelm@10464
|
75 |
((string * context attribute list) * (string * (string list * string list)) list) list
|
wenzelm@6932
|
76 |
-> state -> state
|
wenzelm@10464
|
77 |
val assume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
|
wenzelm@7271
|
78 |
-> state -> state
|
wenzelm@10464
|
79 |
val presume:
|
wenzelm@10464
|
80 |
((string * context attribute list) * (string * (string list * string list)) list) list
|
wenzelm@7271
|
81 |
-> state -> state
|
wenzelm@10464
|
82 |
val presume_i: ((string * context attribute list) * (term * (term list * term list)) list) list
|
wenzelm@6932
|
83 |
-> state -> state
|
wenzelm@11891
|
84 |
val def: string -> context attribute list -> string * (string * string list) -> state -> state
|
wenzelm@11891
|
85 |
val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
|
wenzelm@11793
|
86 |
val invoke_case: string * string option list * context attribute list -> state -> state
|
wenzelm@12959
|
87 |
val multi_theorem: string
|
wenzelm@12959
|
88 |
-> (xstring * (context attribute list * context attribute list list)) option
|
wenzelm@12959
|
89 |
-> bstring * theory attribute list -> context attribute Locale.element list
|
wenzelm@12146
|
90 |
-> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
|
wenzelm@12146
|
91 |
-> theory -> state
|
wenzelm@12959
|
92 |
val multi_theorem_i: string
|
wenzelm@12959
|
93 |
-> (string * (context attribute list * context attribute list list)) option
|
wenzelm@12959
|
94 |
-> bstring * theory attribute list
|
wenzelm@12959
|
95 |
-> context attribute Locale.element_i list
|
wenzelm@12146
|
96 |
-> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
|
wenzelm@12146
|
97 |
-> theory -> state
|
wenzelm@5820
|
98 |
val chain: state -> state
|
wenzelm@6091
|
99 |
val from_facts: thm list -> state -> state
|
wenzelm@12971
|
100 |
val show: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
|
wenzelm@12146
|
101 |
-> ((string * context attribute list) * (string * (string list * string list)) list) list
|
wenzelm@12146
|
102 |
-> bool -> state -> state
|
wenzelm@12971
|
103 |
val show_i: (bool -> state -> state) -> (state -> state Seq.seq) -> bool
|
wenzelm@12146
|
104 |
-> ((string * context attribute list) * (term * (term list * term list)) list) list
|
wenzelm@12146
|
105 |
-> bool -> state -> state
|
wenzelm@12971
|
106 |
val have: (state -> state Seq.seq) -> bool
|
wenzelm@12146
|
107 |
-> ((string * context attribute list) * (string * (string list * string list)) list) list
|
wenzelm@12146
|
108 |
-> state -> state
|
wenzelm@12971
|
109 |
val have_i: (state -> state Seq.seq) -> bool
|
wenzelm@12146
|
110 |
-> ((string * context attribute list) * (term * (term list * term list)) list) list
|
wenzelm@12146
|
111 |
-> state -> state
|
wenzelm@6404
|
112 |
val at_bottom: state -> bool
|
wenzelm@6982
|
113 |
val local_qed: (state -> state Seq.seq)
|
wenzelm@12146
|
114 |
-> (context -> string * (string * thm list) list -> unit) * (context -> thm -> unit)
|
wenzelm@12146
|
115 |
-> state -> state Seq.seq
|
wenzelm@6950
|
116 |
val global_qed: (state -> state Seq.seq) -> state
|
wenzelm@12244
|
117 |
-> (theory * ((string * string) * (string * thm list) list)) Seq.seq
|
wenzelm@6896
|
118 |
val begin_block: state -> state
|
wenzelm@6932
|
119 |
val end_block: state -> state Seq.seq
|
wenzelm@6896
|
120 |
val next_block: state -> state
|
wenzelm@5820
|
121 |
end;
|
wenzelm@5820
|
122 |
|
wenzelm@13377
|
123 |
structure Proof: PROOF =
|
wenzelm@5820
|
124 |
struct
|
wenzelm@5820
|
125 |
|
wenzelm@5820
|
126 |
|
wenzelm@5820
|
127 |
(** proof state **)
|
wenzelm@5820
|
128 |
|
wenzelm@5820
|
129 |
type context = ProofContext.context;
|
wenzelm@5820
|
130 |
|
wenzelm@5820
|
131 |
|
wenzelm@5820
|
132 |
(* type goal *)
|
wenzelm@5820
|
133 |
|
wenzelm@5820
|
134 |
datatype kind =
|
wenzelm@12959
|
135 |
Theorem of {kind: string,
|
wenzelm@12959
|
136 |
theory_spec: (bstring * theory attribute list) * theory attribute list list,
|
wenzelm@13415
|
137 |
locale_spec: (string * (context attribute list * context attribute list list)) option,
|
wenzelm@13415
|
138 |
view: cterm list} |
|
wenzelm@12959
|
139 |
Show of context attribute list list |
|
wenzelm@12959
|
140 |
Have of context attribute list list;
|
wenzelm@5820
|
141 |
|
wenzelm@13415
|
142 |
fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
|
wenzelm@13415
|
143 |
locale_spec = None, view = _}) = s ^ (if a = "" then "" else " " ^ a)
|
wenzelm@13399
|
144 |
| kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
|
wenzelm@13415
|
145 |
locale_spec = Some (name, _), view = _}) =
|
wenzelm@13415
|
146 |
s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
|
wenzelm@12015
|
147 |
| kind_name _ (Show _) = "show"
|
wenzelm@12015
|
148 |
| kind_name _ (Have _) = "have";
|
wenzelm@5820
|
149 |
|
wenzelm@5820
|
150 |
type goal =
|
wenzelm@12146
|
151 |
(kind * (*result kind*)
|
wenzelm@12146
|
152 |
string list * (*result names*)
|
wenzelm@12146
|
153 |
term list list) * (*result statements*)
|
wenzelm@12146
|
154 |
(thm list * (*use facts*)
|
wenzelm@12146
|
155 |
thm); (*goal: subgoals ==> statement*)
|
wenzelm@5820
|
156 |
|
wenzelm@5820
|
157 |
|
wenzelm@5820
|
158 |
(* type mode *)
|
wenzelm@5820
|
159 |
|
wenzelm@5820
|
160 |
datatype mode = Forward | ForwardChain | Backward;
|
wenzelm@7201
|
161 |
val mode_name = (fn Forward => "state" | ForwardChain => "chain" | Backward => "prove");
|
wenzelm@5820
|
162 |
|
wenzelm@5820
|
163 |
|
wenzelm@5820
|
164 |
(* datatype state *)
|
wenzelm@5820
|
165 |
|
wenzelm@7176
|
166 |
datatype node =
|
wenzelm@7176
|
167 |
Node of
|
wenzelm@7176
|
168 |
{context: context,
|
wenzelm@7176
|
169 |
facts: thm list option,
|
wenzelm@7176
|
170 |
mode: mode,
|
wenzelm@12971
|
171 |
goal: (goal * ((state -> state Seq.seq) * bool)) option}
|
wenzelm@7176
|
172 |
and state =
|
wenzelm@5820
|
173 |
State of
|
wenzelm@5820
|
174 |
node * (*current*)
|
wenzelm@5820
|
175 |
node list; (*parents wrt. block structure*)
|
wenzelm@5820
|
176 |
|
wenzelm@7176
|
177 |
fun make_node (context, facts, mode, goal) =
|
wenzelm@7176
|
178 |
Node {context = context, facts = facts, mode = mode, goal = goal};
|
wenzelm@7176
|
179 |
|
wenzelm@7176
|
180 |
|
wenzelm@5820
|
181 |
exception STATE of string * state;
|
wenzelm@5820
|
182 |
|
wenzelm@5820
|
183 |
fun err_malformed name state =
|
wenzelm@5820
|
184 |
raise STATE (name ^ ": internal error -- malformed proof state", state);
|
wenzelm@5820
|
185 |
|
wenzelm@6871
|
186 |
fun check_result msg state sq =
|
wenzelm@6871
|
187 |
(case Seq.pull sq of
|
wenzelm@6871
|
188 |
None => raise STATE (msg, state)
|
wenzelm@6871
|
189 |
| Some s_sq => Seq.cons s_sq);
|
wenzelm@6871
|
190 |
|
wenzelm@5820
|
191 |
|
wenzelm@7176
|
192 |
fun map_current f (State (Node {context, facts, mode, goal}, nodes)) =
|
wenzelm@5820
|
193 |
State (make_node (f (context, facts, mode, goal)), nodes);
|
wenzelm@5820
|
194 |
|
wenzelm@12045
|
195 |
fun init_state thy =
|
wenzelm@12045
|
196 |
State (make_node (ProofContext.init thy, None, Forward, None), []);
|
wenzelm@12045
|
197 |
|
wenzelm@5820
|
198 |
|
wenzelm@5820
|
199 |
|
wenzelm@5820
|
200 |
(** basic proof state operations **)
|
wenzelm@5820
|
201 |
|
wenzelm@5820
|
202 |
(* context *)
|
wenzelm@5820
|
203 |
|
wenzelm@7176
|
204 |
fun context_of (State (Node {context, ...}, _)) = context;
|
wenzelm@5820
|
205 |
val theory_of = ProofContext.theory_of o context_of;
|
wenzelm@5820
|
206 |
val sign_of = ProofContext.sign_of o context_of;
|
wenzelm@5820
|
207 |
|
wenzelm@5820
|
208 |
fun map_context f = map_current (fn (ctxt, facts, mode, goal) => (f ctxt, facts, mode, goal));
|
wenzelm@5820
|
209 |
|
wenzelm@7176
|
210 |
fun map_context_result f (state as State (Node {context, facts, mode, goal}, nodes)) =
|
wenzelm@5820
|
211 |
let val (context', result) = f context
|
wenzelm@5820
|
212 |
in (State (make_node (context', facts, mode, goal), nodes), result) end;
|
wenzelm@5820
|
213 |
|
wenzelm@5820
|
214 |
|
wenzelm@7924
|
215 |
val warn_extra_tfrees = map_context o ProofContext.warn_extra_tfrees o context_of;
|
wenzelm@10809
|
216 |
val add_binds_i = map_context o ProofContext.add_binds_i;
|
wenzelm@6790
|
217 |
val auto_bind_goal = map_context o ProofContext.auto_bind_goal;
|
wenzelm@12146
|
218 |
val auto_bind_facts = map_context o ProofContext.auto_bind_facts;
|
wenzelm@6091
|
219 |
val put_thms = map_context o ProofContext.put_thms;
|
wenzelm@6091
|
220 |
val put_thmss = map_context o ProofContext.put_thmss;
|
wenzelm@7605
|
221 |
val reset_thms = map_context o ProofContext.reset_thms;
|
wenzelm@8374
|
222 |
val get_case = ProofContext.get_case o context_of;
|
wenzelm@5820
|
223 |
|
wenzelm@5820
|
224 |
|
wenzelm@5820
|
225 |
(* facts *)
|
wenzelm@5820
|
226 |
|
wenzelm@7176
|
227 |
fun the_facts (State (Node {facts = Some facts, ...}, _)) = facts
|
wenzelm@5820
|
228 |
| the_facts state = raise STATE ("No current facts available", state);
|
wenzelm@5820
|
229 |
|
wenzelm@9469
|
230 |
fun the_fact state =
|
wenzelm@9469
|
231 |
(case the_facts state of
|
wenzelm@9469
|
232 |
[thm] => thm
|
wenzelm@9469
|
233 |
| _ => raise STATE ("Single fact expected", state));
|
wenzelm@9469
|
234 |
|
wenzelm@6848
|
235 |
fun assert_facts state = (the_facts state; state);
|
wenzelm@7176
|
236 |
fun get_facts (State (Node {facts, ...}, _)) = facts;
|
wenzelm@6848
|
237 |
|
wenzelm@7605
|
238 |
|
wenzelm@7605
|
239 |
val thisN = "this";
|
wenzelm@7605
|
240 |
|
wenzelm@5820
|
241 |
fun put_facts facts state =
|
wenzelm@5820
|
242 |
state
|
wenzelm@5820
|
243 |
|> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
|
wenzelm@7605
|
244 |
|> (case facts of None => reset_thms thisN | Some ths => put_thms (thisN, ths));
|
wenzelm@5820
|
245 |
|
wenzelm@5820
|
246 |
val reset_facts = put_facts None;
|
wenzelm@5820
|
247 |
|
wenzelm@9196
|
248 |
fun these_factss (state, named_factss) =
|
wenzelm@13297
|
249 |
state |> put_facts (Some (flat (map snd named_factss)));
|
wenzelm@5820
|
250 |
|
wenzelm@5820
|
251 |
|
wenzelm@5820
|
252 |
(* goal *)
|
wenzelm@5820
|
253 |
|
wenzelm@10553
|
254 |
local
|
wenzelm@10553
|
255 |
fun find i (state as State (Node {goal = Some goal, ...}, _)) = (context_of state, (i, goal))
|
wenzelm@10553
|
256 |
| find i (State (Node {goal = None, ...}, node :: nodes)) = find (i + 1) (State (node, nodes))
|
wenzelm@10553
|
257 |
| find _ (state as State (_, [])) = err_malformed "find_goal" state;
|
wenzelm@10553
|
258 |
in val find_goal = find 0 end;
|
wenzelm@7176
|
259 |
|
wenzelm@11079
|
260 |
fun get_goal state =
|
wenzelm@11079
|
261 |
let val (ctxt, (_, ((_, x), _))) = find_goal state
|
wenzelm@11079
|
262 |
in (ctxt, x) end;
|
wenzelm@11079
|
263 |
|
wenzelm@5820
|
264 |
fun put_goal goal = map_current (fn (ctxt, facts, mode, _) => (ctxt, facts, mode, goal));
|
wenzelm@5820
|
265 |
|
wenzelm@8374
|
266 |
fun map_goal f g (State (Node {context, facts, mode, goal = Some goal}, nodes)) =
|
wenzelm@8374
|
267 |
State (make_node (f context, facts, mode, Some (g goal)), nodes)
|
wenzelm@8374
|
268 |
| map_goal f g (State (nd, node :: nodes)) =
|
wenzelm@8374
|
269 |
let val State (node', nodes') = map_goal f g (State (node, nodes))
|
wenzelm@8374
|
270 |
in map_context f (State (nd, node' :: nodes')) end
|
wenzelm@8374
|
271 |
| map_goal _ _ state = state;
|
wenzelm@5820
|
272 |
|
wenzelm@5820
|
273 |
fun goal_facts get state =
|
wenzelm@5820
|
274 |
state
|
wenzelm@8374
|
275 |
|> map_goal I (fn ((result, (_, thm)), f) => ((result, (get state, thm)), f));
|
wenzelm@5820
|
276 |
|
wenzelm@5820
|
277 |
fun use_facts state =
|
wenzelm@5820
|
278 |
state
|
wenzelm@5820
|
279 |
|> goal_facts the_facts
|
wenzelm@5820
|
280 |
|> reset_facts;
|
wenzelm@5820
|
281 |
|
wenzelm@5820
|
282 |
|
wenzelm@5820
|
283 |
(* mode *)
|
wenzelm@5820
|
284 |
|
wenzelm@7176
|
285 |
fun get_mode (State (Node {mode, ...}, _)) = mode;
|
wenzelm@5820
|
286 |
fun put_mode mode = map_current (fn (ctxt, facts, _, goal) => (ctxt, facts, mode, goal));
|
wenzelm@5820
|
287 |
|
wenzelm@5820
|
288 |
val enter_forward = put_mode Forward;
|
wenzelm@5820
|
289 |
val enter_forward_chain = put_mode ForwardChain;
|
wenzelm@5820
|
290 |
val enter_backward = put_mode Backward;
|
wenzelm@5820
|
291 |
|
wenzelm@5820
|
292 |
fun assert_mode pred state =
|
wenzelm@5820
|
293 |
let val mode = get_mode state in
|
wenzelm@5820
|
294 |
if pred mode then state
|
wenzelm@12010
|
295 |
else raise STATE ("Illegal application of proof command in "
|
wenzelm@12010
|
296 |
^ quote (mode_name mode) ^ " mode", state)
|
wenzelm@5820
|
297 |
end;
|
wenzelm@5820
|
298 |
|
wenzelm@5820
|
299 |
fun is_chain state = get_mode state = ForwardChain;
|
wenzelm@5820
|
300 |
val assert_forward = assert_mode (equal Forward);
|
wenzelm@5820
|
301 |
val assert_forward_or_chain = assert_mode (equal Forward orf equal ForwardChain);
|
wenzelm@5820
|
302 |
val assert_backward = assert_mode (equal Backward);
|
wenzelm@8206
|
303 |
val assert_no_chain = assert_mode (not_equal ForwardChain);
|
wenzelm@5820
|
304 |
|
wenzelm@5820
|
305 |
|
wenzelm@5820
|
306 |
(* blocks *)
|
wenzelm@5820
|
307 |
|
wenzelm@6776
|
308 |
fun level (State (_, nodes)) = length nodes;
|
wenzelm@6776
|
309 |
|
wenzelm@5820
|
310 |
fun open_block (State (node, nodes)) = State (node, node :: nodes);
|
wenzelm@5820
|
311 |
|
wenzelm@5820
|
312 |
fun new_block state =
|
wenzelm@5820
|
313 |
state
|
wenzelm@5820
|
314 |
|> open_block
|
wenzelm@5820
|
315 |
|> put_goal None;
|
wenzelm@5820
|
316 |
|
wenzelm@7487
|
317 |
fun close_block (state as State (_, node :: nodes)) = State (node, nodes)
|
wenzelm@5820
|
318 |
| close_block state = raise STATE ("Unbalanced block parentheses", state);
|
wenzelm@5820
|
319 |
|
wenzelm@5820
|
320 |
|
wenzelm@5820
|
321 |
|
wenzelm@12423
|
322 |
(** pretty_state **)
|
wenzelm@5820
|
323 |
|
nipkow@13869
|
324 |
val show_main_goal = ref false;
|
nipkow@13698
|
325 |
|
wenzelm@6529
|
326 |
val verbose = ProofContext.verbose;
|
wenzelm@6529
|
327 |
|
wenzelm@12085
|
328 |
fun pretty_goals_local ctxt = Display.pretty_goals_aux
|
wenzelm@12085
|
329 |
(ProofContext.pretty_sort ctxt, ProofContext.pretty_typ ctxt, ProofContext.pretty_term ctxt);
|
wenzelm@12085
|
330 |
|
wenzelm@12055
|
331 |
fun pretty_facts _ _ None = []
|
wenzelm@12055
|
332 |
| pretty_facts s ctxt (Some ths) =
|
wenzelm@12055
|
333 |
[Pretty.big_list (s ^ "this:") (map (ProofContext.pretty_thm ctxt) ths), Pretty.str ""];
|
wenzelm@6756
|
334 |
|
wenzelm@12423
|
335 |
fun pretty_state nr (state as State (Node {context = ctxt, facts, mode, goal = _}, nodes)) =
|
wenzelm@5820
|
336 |
let
|
wenzelm@11891
|
337 |
val ref (_, _, begin_goal) = Display.current_goals_markers;
|
wenzelm@5820
|
338 |
|
wenzelm@5820
|
339 |
fun levels_up 0 = ""
|
wenzelm@7575
|
340 |
| levels_up 1 = ", 1 level up"
|
wenzelm@7575
|
341 |
| levels_up i = ", " ^ string_of_int i ^ " levels up";
|
wenzelm@5820
|
342 |
|
wenzelm@11556
|
343 |
fun subgoals 0 = ""
|
wenzelm@11556
|
344 |
| subgoals 1 = ", 1 subgoal"
|
wenzelm@11556
|
345 |
| subgoals n = ", " ^ string_of_int n ^ " subgoals";
|
wenzelm@12146
|
346 |
|
wenzelm@12146
|
347 |
fun prt_names names =
|
wenzelm@12242
|
348 |
(case filter_out (equal "") names of [] => ""
|
wenzelm@12308
|
349 |
| nms => " " ^ enclose "(" ")" (space_implode " and " (take (7, nms) @
|
wenzelm@12308
|
350 |
(if length nms > 7 then ["..."] else []))));
|
wenzelm@12146
|
351 |
|
wenzelm@12146
|
352 |
fun prt_goal (_, (i, (((kind, names, _), (goal_facts, thm)), _))) =
|
wenzelm@12085
|
353 |
pretty_facts "using " ctxt
|
wenzelm@8462
|
354 |
(if mode <> Backward orelse null goal_facts then None else Some goal_facts) @
|
wenzelm@12146
|
355 |
[Pretty.str ("goal (" ^ kind_name (sign_of state) kind ^ prt_names names ^
|
wenzelm@12146
|
356 |
levels_up (i div 2) ^ subgoals (Thm.nprems_of thm) ^ "):")] @
|
nipkow@13698
|
357 |
pretty_goals_local ctxt begin_goal (true, !show_main_goal) (! Display.goals_limit) thm;
|
wenzelm@6848
|
358 |
|
wenzelm@8462
|
359 |
val ctxt_prts =
|
wenzelm@12085
|
360 |
if ! verbose orelse mode = Forward then ProofContext.pretty_context ctxt
|
wenzelm@12085
|
361 |
else if mode = Backward then ProofContext.pretty_asms ctxt
|
wenzelm@7575
|
362 |
else [];
|
wenzelm@8462
|
363 |
|
wenzelm@8462
|
364 |
val prts =
|
wenzelm@8582
|
365 |
[Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^
|
wenzelm@12010
|
366 |
(if ! verbose then ", depth " ^ string_of_int (length nodes div 2 - 1)
|
wenzelm@8561
|
367 |
else "")), Pretty.str ""] @
|
wenzelm@8462
|
368 |
(if null ctxt_prts then [] else ctxt_prts @ [Pretty.str ""]) @
|
wenzelm@8462
|
369 |
(if ! verbose orelse mode = Forward then
|
wenzelm@12146
|
370 |
(pretty_facts "" ctxt facts @ prt_goal (find_goal state))
|
wenzelm@12085
|
371 |
else if mode = ForwardChain then pretty_facts "picking " ctxt facts
|
wenzelm@12146
|
372 |
else prt_goal (find_goal state))
|
wenzelm@12423
|
373 |
in prts end;
|
wenzelm@5820
|
374 |
|
wenzelm@12085
|
375 |
fun pretty_goals main state =
|
wenzelm@12085
|
376 |
let val (ctxt, (_, ((_, (_, thm)), _))) = find_goal state
|
wenzelm@12085
|
377 |
in pretty_goals_local ctxt "" (false, main) (! Display.goals_limit) thm end;
|
wenzelm@10320
|
378 |
|
wenzelm@5820
|
379 |
|
wenzelm@5820
|
380 |
|
wenzelm@5820
|
381 |
(** proof steps **)
|
wenzelm@5820
|
382 |
|
wenzelm@5820
|
383 |
(* datatype method *)
|
wenzelm@5820
|
384 |
|
wenzelm@8374
|
385 |
datatype method =
|
wenzelm@8374
|
386 |
Method of thm list -> thm -> (thm * (string * RuleCases.T) list) Seq.seq;
|
wenzelm@8374
|
387 |
|
wenzelm@8374
|
388 |
fun method tac = Method (fn facts => fn st => Seq.map (rpair []) (tac facts st));
|
wenzelm@8374
|
389 |
val method_cases = Method;
|
wenzelm@5820
|
390 |
|
wenzelm@5820
|
391 |
|
wenzelm@5820
|
392 |
(* refine goal *)
|
wenzelm@5820
|
393 |
|
wenzelm@8234
|
394 |
local
|
wenzelm@8234
|
395 |
|
wenzelm@5820
|
396 |
fun check_sign sg state =
|
wenzelm@5820
|
397 |
if Sign.subsig (sg, sign_of state) then state
|
wenzelm@5820
|
398 |
else raise STATE ("Bad signature of result: " ^ Sign.str_of_sg sg, state);
|
wenzelm@5820
|
399 |
|
wenzelm@8234
|
400 |
fun gen_refine current_context meth_fun state =
|
wenzelm@6848
|
401 |
let
|
wenzelm@12971
|
402 |
val (goal_ctxt, (_, ((result, (facts, thm)), x))) = find_goal state;
|
wenzelm@8234
|
403 |
val Method meth = meth_fun (if current_context then context_of state else goal_ctxt);
|
wenzelm@5820
|
404 |
|
wenzelm@8374
|
405 |
fun refn (thm', cases) =
|
wenzelm@6848
|
406 |
state
|
wenzelm@6848
|
407 |
|> check_sign (Thm.sign_of_thm thm')
|
wenzelm@12971
|
408 |
|> map_goal (ProofContext.add_cases cases) (K ((result, (facts, thm')), x));
|
wenzelm@6848
|
409 |
in Seq.map refn (meth facts thm) end;
|
wenzelm@5820
|
410 |
|
wenzelm@8234
|
411 |
in
|
wenzelm@8234
|
412 |
|
wenzelm@8234
|
413 |
val refine = gen_refine true;
|
wenzelm@8234
|
414 |
val refine_end = gen_refine false;
|
wenzelm@8234
|
415 |
|
wenzelm@8234
|
416 |
end;
|
wenzelm@8234
|
417 |
|
wenzelm@5820
|
418 |
|
wenzelm@11917
|
419 |
(* goal addressing *)
|
wenzelm@6932
|
420 |
|
wenzelm@8152
|
421 |
fun FINDGOAL tac st =
|
wenzelm@8374
|
422 |
let fun find (i, n) = if i > n then Seq.fail else Seq.APPEND (tac i, find (i + 1, n))
|
wenzelm@8374
|
423 |
in find (1, Thm.nprems_of st) st end;
|
wenzelm@8152
|
424 |
|
wenzelm@8166
|
425 |
fun HEADGOAL tac = tac 1;
|
wenzelm@8166
|
426 |
|
wenzelm@9469
|
427 |
|
wenzelm@9469
|
428 |
(* export results *)
|
wenzelm@9469
|
429 |
|
wenzelm@11816
|
430 |
fun refine_tac rule =
|
wenzelm@12703
|
431 |
Tactic.norm_hhf_tac THEN' Tactic.rtac rule THEN_ALL_NEW (SUBGOAL (fn (goal, i) =>
|
wenzelm@11816
|
432 |
if can Logic.dest_goal (Logic.strip_assums_concl goal) then
|
wenzelm@11816
|
433 |
Tactic.etac Drule.triv_goal i
|
wenzelm@11816
|
434 |
else all_tac));
|
wenzelm@11816
|
435 |
|
wenzelm@12146
|
436 |
fun export_goal inner print_rule raw_rule state =
|
wenzelm@6932
|
437 |
let
|
wenzelm@12971
|
438 |
val (outer, (_, ((result, (facts, thm)), x))) = find_goal state;
|
wenzelm@12010
|
439 |
val exp_tac = ProofContext.export true inner outer;
|
wenzelm@9469
|
440 |
fun exp_rule rule =
|
wenzelm@9469
|
441 |
let
|
wenzelm@12055
|
442 |
val _ = print_rule outer rule;
|
wenzelm@11816
|
443 |
val thmq = FINDGOAL (refine_tac rule) thm;
|
wenzelm@12971
|
444 |
in Seq.map (fn th => map_goal I (K ((result, (facts, th)), x)) state) thmq end;
|
wenzelm@9469
|
445 |
in raw_rule |> exp_tac |> (Seq.flat o Seq.map exp_rule) end;
|
wenzelm@6932
|
446 |
|
wenzelm@12146
|
447 |
fun export_goals inner print_rule raw_rules =
|
wenzelm@12146
|
448 |
Seq.EVERY (map (export_goal inner print_rule) raw_rules);
|
wenzelm@12146
|
449 |
|
wenzelm@6932
|
450 |
fun transfer_facts inner_state state =
|
wenzelm@6932
|
451 |
(case get_facts inner_state of
|
wenzelm@6932
|
452 |
None => Seq.single (reset_facts state)
|
wenzelm@8617
|
453 |
| Some thms =>
|
wenzelm@8617
|
454 |
let
|
wenzelm@12010
|
455 |
val exp_tac = ProofContext.export false (context_of inner_state) (context_of state);
|
wenzelm@11816
|
456 |
val thmqs = map exp_tac thms;
|
wenzelm@8617
|
457 |
in Seq.map (fn ths => put_facts (Some ths) state) (Seq.commute thmqs) end);
|
wenzelm@6932
|
458 |
|
wenzelm@6932
|
459 |
|
wenzelm@6932
|
460 |
(* prepare result *)
|
wenzelm@6932
|
461 |
|
wenzelm@12146
|
462 |
fun prep_result state ts raw_th =
|
wenzelm@5820
|
463 |
let
|
wenzelm@5820
|
464 |
val ctxt = context_of state;
|
wenzelm@5820
|
465 |
fun err msg = raise STATE (msg, state);
|
wenzelm@5820
|
466 |
|
wenzelm@12146
|
467 |
val ngoals = Thm.nprems_of raw_th;
|
wenzelm@5820
|
468 |
val _ =
|
wenzelm@5820
|
469 |
if ngoals = 0 then ()
|
nipkow@13698
|
470 |
else (err (Pretty.string_of (Pretty.chunks (pretty_goals_local ctxt "" (true, !show_main_goal)
|
wenzelm@12146
|
471 |
(! Display.goals_limit) raw_th @
|
wenzelm@12085
|
472 |
[Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))));
|
wenzelm@5820
|
473 |
|
wenzelm@12146
|
474 |
val {hyps, sign, ...} = Thm.rep_thm raw_th;
|
wenzelm@6932
|
475 |
val tsig = Sign.tsig_of sign;
|
wenzelm@12055
|
476 |
val casms = flat (map #1 (ProofContext.assumptions_of (context_of state)));
|
wenzelm@11816
|
477 |
val bad_hyps = Library.gen_rems Term.aconv (hyps, map Thm.term_of casms);
|
wenzelm@12146
|
478 |
|
wenzelm@12146
|
479 |
val th = raw_th RS Drule.rev_triv_goal;
|
wenzelm@12146
|
480 |
val ths = Drule.conj_elim_precise (length ts) th
|
wenzelm@12146
|
481 |
handle THM _ => err "Main goal structure corrupted";
|
wenzelm@5820
|
482 |
in
|
wenzelm@12146
|
483 |
conditional (not (null bad_hyps)) (fn () => err ("Additional hypotheses:\n" ^
|
wenzelm@12146
|
484 |
cat_lines (map (ProofContext.string_of_term ctxt) bad_hyps)));
|
wenzelm@12808
|
485 |
conditional (exists (not o Pattern.matches tsig) (ts ~~ map Thm.prop_of ths)) (fn () =>
|
wenzelm@12146
|
486 |
err ("Proved a different theorem: " ^ Pretty.string_of (ProofContext.pretty_thm ctxt th)));
|
wenzelm@12146
|
487 |
ths
|
wenzelm@5820
|
488 |
end;
|
wenzelm@5820
|
489 |
|
wenzelm@5820
|
490 |
|
wenzelm@5820
|
491 |
|
wenzelm@5820
|
492 |
(*** structured proof commands ***)
|
wenzelm@5820
|
493 |
|
wenzelm@5820
|
494 |
(** context **)
|
wenzelm@5820
|
495 |
|
wenzelm@5820
|
496 |
(* bind *)
|
wenzelm@5820
|
497 |
|
wenzelm@5820
|
498 |
fun gen_bind f x state =
|
wenzelm@5820
|
499 |
state
|
wenzelm@5820
|
500 |
|> assert_forward
|
wenzelm@5820
|
501 |
|> map_context (f x)
|
wenzelm@5820
|
502 |
|> reset_facts;
|
wenzelm@5820
|
503 |
|
wenzelm@8617
|
504 |
val match_bind = gen_bind (ProofContext.match_bind false);
|
wenzelm@8617
|
505 |
val match_bind_i = gen_bind (ProofContext.match_bind_i false);
|
wenzelm@8617
|
506 |
val let_bind = gen_bind (ProofContext.match_bind true);
|
wenzelm@8617
|
507 |
val let_bind_i = gen_bind (ProofContext.match_bind_i true);
|
wenzelm@5820
|
508 |
|
wenzelm@5820
|
509 |
|
wenzelm@12714
|
510 |
(* have_thmss *)
|
wenzelm@5820
|
511 |
|
wenzelm@12714
|
512 |
local
|
wenzelm@12714
|
513 |
|
wenzelm@12714
|
514 |
fun gen_have_thmss f args state =
|
wenzelm@5820
|
515 |
state
|
wenzelm@5820
|
516 |
|> assert_forward
|
wenzelm@12714
|
517 |
|> map_context_result (f args)
|
wenzelm@9196
|
518 |
|> these_factss;
|
wenzelm@5820
|
519 |
|
wenzelm@12714
|
520 |
in
|
wenzelm@9196
|
521 |
|
wenzelm@12714
|
522 |
val have_thmss = gen_have_thmss ProofContext.have_thmss;
|
wenzelm@12714
|
523 |
val have_thmss_i = gen_have_thmss ProofContext.have_thmss_i;
|
wenzelm@12714
|
524 |
|
wenzelm@12714
|
525 |
fun simple_have_thms name thms = have_thmss_i [((name, []), [(thms, [])])];
|
wenzelm@12714
|
526 |
|
wenzelm@12714
|
527 |
end;
|
wenzelm@12714
|
528 |
|
wenzelm@12714
|
529 |
|
wenzelm@12714
|
530 |
(* with_thmss *)
|
wenzelm@12714
|
531 |
|
wenzelm@12714
|
532 |
local
|
wenzelm@12714
|
533 |
|
wenzelm@12714
|
534 |
fun gen_with_thmss f args state =
|
wenzelm@12714
|
535 |
let val state' = state |> f args
|
wenzelm@9196
|
536 |
in state' |> simple_have_thms "" (the_facts state' @ the_facts state) end;
|
wenzelm@6876
|
537 |
|
wenzelm@12714
|
538 |
in
|
wenzelm@12714
|
539 |
|
wenzelm@12714
|
540 |
val with_thmss = gen_with_thmss have_thmss;
|
wenzelm@12714
|
541 |
val with_thmss_i = gen_with_thmss have_thmss_i;
|
wenzelm@12714
|
542 |
|
wenzelm@12714
|
543 |
end;
|
wenzelm@12714
|
544 |
|
wenzelm@5820
|
545 |
|
wenzelm@12930
|
546 |
(* using_thmss *)
|
wenzelm@12930
|
547 |
|
wenzelm@12930
|
548 |
local
|
wenzelm@12930
|
549 |
|
wenzelm@12930
|
550 |
fun gen_using_thmss f args state =
|
wenzelm@12930
|
551 |
state
|
wenzelm@12930
|
552 |
|> assert_backward
|
wenzelm@12930
|
553 |
|> map_context_result (f (map (pair ("", [])) args))
|
wenzelm@12930
|
554 |
|> (fn (st, named_facts) =>
|
wenzelm@12971
|
555 |
let val (_, (_, ((result, (facts, thm)), x))) = find_goal st;
|
wenzelm@12971
|
556 |
in st |> map_goal I (K ((result, (facts @ flat (map snd named_facts), thm)), x)) end);
|
wenzelm@12930
|
557 |
|
wenzelm@12930
|
558 |
in
|
wenzelm@12930
|
559 |
|
wenzelm@12930
|
560 |
val using_thmss = gen_using_thmss ProofContext.have_thmss;
|
wenzelm@12930
|
561 |
val using_thmss_i = gen_using_thmss ProofContext.have_thmss_i;
|
wenzelm@12930
|
562 |
|
wenzelm@12930
|
563 |
end;
|
wenzelm@12930
|
564 |
|
wenzelm@12930
|
565 |
|
wenzelm@5820
|
566 |
(* fix *)
|
wenzelm@5820
|
567 |
|
wenzelm@5820
|
568 |
fun gen_fix f xs state =
|
wenzelm@5820
|
569 |
state
|
wenzelm@5820
|
570 |
|> assert_forward
|
wenzelm@5820
|
571 |
|> map_context (f xs)
|
wenzelm@5820
|
572 |
|> reset_facts;
|
wenzelm@5820
|
573 |
|
wenzelm@5820
|
574 |
val fix = gen_fix ProofContext.fix;
|
wenzelm@5820
|
575 |
val fix_i = gen_fix ProofContext.fix_i;
|
wenzelm@5820
|
576 |
|
wenzelm@5820
|
577 |
|
wenzelm@11891
|
578 |
(* assume and presume *)
|
wenzelm@5820
|
579 |
|
wenzelm@9469
|
580 |
fun gen_assume f exp args state =
|
wenzelm@5820
|
581 |
state
|
wenzelm@5820
|
582 |
|> assert_forward
|
wenzelm@9469
|
583 |
|> map_context_result (f exp args)
|
wenzelm@11924
|
584 |
|> these_factss;
|
wenzelm@6932
|
585 |
|
wenzelm@7271
|
586 |
val assm = gen_assume ProofContext.assume;
|
wenzelm@7271
|
587 |
val assm_i = gen_assume ProofContext.assume_i;
|
wenzelm@11917
|
588 |
val assume = assm ProofContext.export_assume;
|
wenzelm@11917
|
589 |
val assume_i = assm_i ProofContext.export_assume;
|
wenzelm@11917
|
590 |
val presume = assm ProofContext.export_presume;
|
wenzelm@11917
|
591 |
val presume_i = assm_i ProofContext.export_presume;
|
wenzelm@5820
|
592 |
|
wenzelm@7271
|
593 |
|
wenzelm@5820
|
594 |
|
wenzelm@11891
|
595 |
(** local definitions **)
|
wenzelm@11891
|
596 |
|
wenzelm@11891
|
597 |
fun gen_def fix prep_term prep_pats raw_name atts (x, (raw_rhs, raw_pats)) state =
|
wenzelm@11891
|
598 |
let
|
wenzelm@11891
|
599 |
val _ = assert_forward state;
|
wenzelm@11891
|
600 |
val ctxt = context_of state;
|
wenzelm@11891
|
601 |
|
wenzelm@11891
|
602 |
(*rhs*)
|
wenzelm@11891
|
603 |
val name = if raw_name = "" then Thm.def_name x else raw_name;
|
wenzelm@11891
|
604 |
val rhs = prep_term ctxt raw_rhs;
|
wenzelm@11891
|
605 |
val T = Term.fastype_of rhs;
|
wenzelm@11891
|
606 |
val pats = prep_pats T (ProofContext.declare_term rhs ctxt) raw_pats;
|
wenzelm@11891
|
607 |
|
wenzelm@11891
|
608 |
(*lhs*)
|
wenzelm@11891
|
609 |
val lhs = ProofContext.bind_skolem ctxt [x] (Free (x, T));
|
wenzelm@11891
|
610 |
in
|
wenzelm@11891
|
611 |
state
|
wenzelm@11891
|
612 |
|> fix [([x], None)]
|
wenzelm@11891
|
613 |
|> match_bind_i [(pats, rhs)]
|
wenzelm@11917
|
614 |
|> assm_i ProofContext.export_def [((name, atts), [(Logic.mk_equals (lhs, rhs), ([], []))])]
|
wenzelm@11891
|
615 |
end;
|
wenzelm@11891
|
616 |
|
wenzelm@11891
|
617 |
val def = gen_def fix ProofContext.read_term ProofContext.read_term_pats;
|
wenzelm@11891
|
618 |
val def_i = gen_def fix_i ProofContext.cert_term ProofContext.cert_term_pats;
|
wenzelm@11891
|
619 |
|
wenzelm@11891
|
620 |
|
wenzelm@8374
|
621 |
(* invoke_case *)
|
wenzelm@8374
|
622 |
|
wenzelm@11793
|
623 |
fun invoke_case (name, xs, atts) state =
|
wenzelm@9292
|
624 |
let
|
wenzelm@10830
|
625 |
val (state', (lets, asms)) =
|
wenzelm@11793
|
626 |
map_context_result (ProofContext.apply_case (get_case state name xs)) state;
|
wenzelm@13425
|
627 |
val assumptions = asms |> map (fn (a, ts) =>
|
wenzelm@13425
|
628 |
((if a = "" then "" else NameSpace.append name a, atts), map (rpair ([], [])) ts));
|
wenzelm@13425
|
629 |
val qnames = filter_out (equal "") (map (#1 o #1) assumptions);
|
wenzelm@9292
|
630 |
in
|
wenzelm@10830
|
631 |
state'
|
wenzelm@10809
|
632 |
|> add_binds_i lets
|
wenzelm@13425
|
633 |
|> map_context (ProofContext.qualified true)
|
wenzelm@13425
|
634 |
|> assume_i assumptions
|
wenzelm@13425
|
635 |
|> map_context (ProofContext.hide_thms false qnames)
|
wenzelm@13425
|
636 |
|> (fn st => simple_have_thms name (the_facts st) st)
|
wenzelm@13425
|
637 |
|> map_context (ProofContext.restore_qualified (context_of state))
|
wenzelm@8374
|
638 |
end;
|
wenzelm@8374
|
639 |
|
wenzelm@8374
|
640 |
|
wenzelm@5820
|
641 |
|
wenzelm@5820
|
642 |
(** goals **)
|
wenzelm@5820
|
643 |
|
wenzelm@5820
|
644 |
(* forward chaining *)
|
wenzelm@5820
|
645 |
|
wenzelm@5820
|
646 |
fun chain state =
|
wenzelm@5820
|
647 |
state
|
wenzelm@5820
|
648 |
|> assert_forward
|
wenzelm@6848
|
649 |
|> assert_facts
|
wenzelm@5820
|
650 |
|> enter_forward_chain;
|
wenzelm@5820
|
651 |
|
wenzelm@5820
|
652 |
fun from_facts facts state =
|
wenzelm@5820
|
653 |
state
|
wenzelm@5820
|
654 |
|> put_facts (Some facts)
|
wenzelm@5820
|
655 |
|> chain;
|
wenzelm@5820
|
656 |
|
wenzelm@5820
|
657 |
|
wenzelm@5820
|
658 |
(* setup goals *)
|
wenzelm@5820
|
659 |
|
wenzelm@11549
|
660 |
val rule_contextN = "rule_context";
|
wenzelm@8991
|
661 |
|
wenzelm@12971
|
662 |
fun setup_goal opt_block prepp autofix kind after_qed pr names raw_propp state =
|
wenzelm@5936
|
663 |
let
|
wenzelm@12146
|
664 |
val (state', (propss, gen_binds)) =
|
wenzelm@5936
|
665 |
state
|
wenzelm@5936
|
666 |
|> assert_forward_or_chain
|
wenzelm@5936
|
667 |
|> enter_forward
|
wenzelm@8617
|
668 |
|> opt_block
|
wenzelm@12534
|
669 |
|> map_context_result (fn ctxt => prepp (ctxt, raw_propp));
|
wenzelm@12808
|
670 |
val sign' = sign_of state';
|
wenzelm@12146
|
671 |
|
wenzelm@12146
|
672 |
val props = flat propss;
|
wenzelm@12808
|
673 |
val cprop = Thm.cterm_of sign' (Logic.mk_conjunction_list props);
|
wenzelm@7556
|
674 |
val goal = Drule.mk_triv_goal cprop;
|
wenzelm@10553
|
675 |
|
wenzelm@12146
|
676 |
val tvars = foldr Term.add_term_tvars (props, []);
|
wenzelm@12146
|
677 |
val vars = foldr Term.add_term_vars (props, []);
|
wenzelm@5820
|
678 |
in
|
wenzelm@10553
|
679 |
if null tvars then ()
|
wenzelm@10553
|
680 |
else raise STATE ("Goal statement contains illegal schematic type variable(s): " ^
|
wenzelm@10553
|
681 |
commas (map (Syntax.string_of_vname o #1) tvars), state);
|
wenzelm@10553
|
682 |
if null vars then ()
|
wenzelm@10553
|
683 |
else warning ("Goal statement contains unbound schematic variable(s): " ^
|
wenzelm@12055
|
684 |
commas (map (ProofContext.string_of_term (context_of state')) vars));
|
wenzelm@5936
|
685 |
state'
|
wenzelm@12146
|
686 |
|> map_context (autofix props)
|
wenzelm@12971
|
687 |
|> put_goal (Some (((kind, names, propss), ([], goal)),
|
wenzelm@12971
|
688 |
(after_qed o map_context gen_binds, pr)))
|
wenzelm@12167
|
689 |
|> map_context (ProofContext.add_cases
|
wenzelm@12808
|
690 |
(if length props = 1 then
|
nipkow@13596
|
691 |
RuleCases.make None None (Thm.sign_of_thm goal, Thm.prop_of goal) [rule_contextN]
|
wenzelm@12167
|
692 |
else [(rule_contextN, RuleCases.empty)]))
|
wenzelm@12146
|
693 |
|> auto_bind_goal props
|
wenzelm@5820
|
694 |
|> (if is_chain state then use_facts else reset_facts)
|
wenzelm@5820
|
695 |
|> new_block
|
wenzelm@5820
|
696 |
|> enter_backward
|
wenzelm@5820
|
697 |
end;
|
wenzelm@5820
|
698 |
|
wenzelm@5820
|
699 |
(*global goals*)
|
wenzelm@12959
|
700 |
fun global_goal prep kind raw_locale a elems concl thy =
|
wenzelm@12503
|
701 |
let
|
wenzelm@12549
|
702 |
val init = init_state thy;
|
wenzelm@13399
|
703 |
val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
|
wenzelm@12959
|
704 |
prep (apsome fst raw_locale) elems (map snd concl) (context_of init);
|
wenzelm@12503
|
705 |
in
|
wenzelm@12549
|
706 |
init
|
wenzelm@12549
|
707 |
|> open_block
|
wenzelm@12511
|
708 |
|> map_context (K locale_ctxt)
|
wenzelm@12065
|
709 |
|> open_block
|
wenzelm@12511
|
710 |
|> map_context (K elems_ctxt)
|
wenzelm@12959
|
711 |
|> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
|
wenzelm@13415
|
712 |
(Theorem {kind = kind,
|
wenzelm@13415
|
713 |
theory_spec = (a, map (snd o fst) concl),
|
wenzelm@13415
|
714 |
locale_spec = (case raw_locale of None => None | Some (_, x) => Some (the opt_name, x)),
|
wenzelm@13415
|
715 |
view = view})
|
wenzelm@12971
|
716 |
Seq.single true (map (fst o fst) concl) propp
|
wenzelm@12065
|
717 |
end;
|
wenzelm@5820
|
718 |
|
wenzelm@12534
|
719 |
val multi_theorem = global_goal Locale.read_context_statement;
|
wenzelm@12534
|
720 |
val multi_theorem_i = global_goal Locale.cert_context_statement;
|
wenzelm@12146
|
721 |
|
wenzelm@5820
|
722 |
|
wenzelm@5820
|
723 |
(*local goals*)
|
wenzelm@12971
|
724 |
fun local_goal' prepp kind (check: bool -> state -> state) f pr args int state =
|
wenzelm@7928
|
725 |
state
|
wenzelm@12146
|
726 |
|> setup_goal open_block prepp (K I) (kind (map (snd o fst) args))
|
wenzelm@12971
|
727 |
f pr (map (fst o fst) args) (map snd args)
|
wenzelm@10936
|
728 |
|> warn_extra_tfrees state
|
wenzelm@10936
|
729 |
|> check int;
|
wenzelm@5820
|
730 |
|
wenzelm@12971
|
731 |
fun local_goal prepp kind f pr args = local_goal' prepp kind (K I) f pr args false;
|
wenzelm@10936
|
732 |
|
wenzelm@10936
|
733 |
val show = local_goal' ProofContext.bind_propp Show;
|
wenzelm@10936
|
734 |
val show_i = local_goal' ProofContext.bind_propp_i Show;
|
wenzelm@10936
|
735 |
val have = local_goal ProofContext.bind_propp Have;
|
wenzelm@10380
|
736 |
val have_i = local_goal ProofContext.bind_propp_i Have;
|
wenzelm@5820
|
737 |
|
wenzelm@5820
|
738 |
|
wenzelm@5820
|
739 |
|
wenzelm@5820
|
740 |
(** conclusions **)
|
wenzelm@5820
|
741 |
|
wenzelm@5820
|
742 |
(* current goal *)
|
wenzelm@5820
|
743 |
|
wenzelm@7176
|
744 |
fun current_goal (State (Node {context, goal = Some goal, ...}, _)) = (context, goal)
|
wenzelm@5820
|
745 |
| current_goal state = raise STATE ("No current goal!", state);
|
wenzelm@5820
|
746 |
|
wenzelm@7176
|
747 |
fun assert_current_goal true (state as State (Node {goal = None, ...}, _)) =
|
wenzelm@6404
|
748 |
raise STATE ("No goal in this block!", state)
|
wenzelm@7176
|
749 |
| assert_current_goal false (state as State (Node {goal = Some _, ...}, _)) =
|
wenzelm@6404
|
750 |
raise STATE ("Goal present in this block!", state)
|
wenzelm@6404
|
751 |
| assert_current_goal _ state = state;
|
wenzelm@5820
|
752 |
|
wenzelm@12010
|
753 |
fun assert_bottom b (state as State (_, nodes)) =
|
wenzelm@12010
|
754 |
let val bot = (length nodes <= 2) in
|
wenzelm@12010
|
755 |
if b andalso not bot then raise STATE ("Not at bottom of proof!", state)
|
wenzelm@12010
|
756 |
else if not b andalso bot then raise STATE ("Already at bottom of proof!", state)
|
wenzelm@12010
|
757 |
else state
|
wenzelm@12010
|
758 |
end;
|
wenzelm@5820
|
759 |
|
wenzelm@6404
|
760 |
val at_bottom = can (assert_bottom true o close_block);
|
wenzelm@6404
|
761 |
|
wenzelm@6932
|
762 |
fun end_proof bot state =
|
wenzelm@5820
|
763 |
state
|
wenzelm@5820
|
764 |
|> assert_forward
|
wenzelm@5820
|
765 |
|> close_block
|
wenzelm@5820
|
766 |
|> assert_bottom bot
|
wenzelm@7011
|
767 |
|> assert_current_goal true
|
wenzelm@7011
|
768 |
|> goal_facts (K []);
|
wenzelm@5820
|
769 |
|
wenzelm@5820
|
770 |
|
wenzelm@6404
|
771 |
(* local_qed *)
|
wenzelm@5820
|
772 |
|
wenzelm@6982
|
773 |
fun finish_local (print_result, print_rule) state =
|
wenzelm@5820
|
774 |
let
|
wenzelm@12971
|
775 |
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), (after_qed, pr))) = current_goal state;
|
wenzelm@8617
|
776 |
val outer_state = state |> close_block;
|
wenzelm@8617
|
777 |
val outer_ctxt = context_of outer_state;
|
wenzelm@8617
|
778 |
|
wenzelm@12146
|
779 |
val ts = flat tss;
|
wenzelm@12146
|
780 |
val results = prep_result state ts raw_thm;
|
wenzelm@12146
|
781 |
val resultq =
|
wenzelm@12146
|
782 |
results |> map (ProofContext.export false goal_ctxt outer_ctxt)
|
wenzelm@12146
|
783 |
|> Seq.commute |> Seq.map (Library.unflat tss);
|
wenzelm@9469
|
784 |
|
wenzelm@12146
|
785 |
val (attss, opt_solve) =
|
wenzelm@5820
|
786 |
(case kind of
|
wenzelm@12971
|
787 |
Show attss => (attss,
|
wenzelm@12971
|
788 |
export_goals goal_ctxt (if pr then print_rule else (K (K ()))) results)
|
wenzelm@12146
|
789 |
| Have attss => (attss, Seq.single)
|
wenzelm@6932
|
790 |
| _ => err_malformed "finish_local" state);
|
wenzelm@5820
|
791 |
in
|
wenzelm@12971
|
792 |
conditional pr (fn () => print_result goal_ctxt
|
wenzelm@12971
|
793 |
(kind_name (sign_of state) kind, names ~~ Library.unflat tss results));
|
wenzelm@8617
|
794 |
outer_state
|
wenzelm@12549
|
795 |
|> auto_bind_facts (ProofContext.generalize goal_ctxt outer_ctxt ts)
|
wenzelm@9469
|
796 |
|> (fn st => Seq.map (fn res =>
|
wenzelm@12714
|
797 |
have_thmss_i ((names ~~ attss) ~~ map (single o Thm.no_attributes) res) st) resultq)
|
wenzelm@9469
|
798 |
|> (Seq.flat o Seq.map opt_solve)
|
wenzelm@7176
|
799 |
|> (Seq.flat o Seq.map after_qed)
|
wenzelm@5820
|
800 |
end;
|
wenzelm@5820
|
801 |
|
wenzelm@6982
|
802 |
fun local_qed finalize print state =
|
wenzelm@6404
|
803 |
state
|
wenzelm@6932
|
804 |
|> end_proof false
|
wenzelm@6871
|
805 |
|> finalize
|
wenzelm@6982
|
806 |
|> (Seq.flat o Seq.map (finish_local print));
|
wenzelm@5820
|
807 |
|
wenzelm@5820
|
808 |
|
wenzelm@12703
|
809 |
(* global_qed *)
|
wenzelm@12065
|
810 |
|
wenzelm@6950
|
811 |
fun finish_global state =
|
wenzelm@5820
|
812 |
let
|
wenzelm@12146
|
813 |
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
|
wenzelm@12065
|
814 |
val locale_ctxt = context_of (state |> close_block);
|
wenzelm@12065
|
815 |
val theory_ctxt = context_of (state |> close_block |> close_block);
|
wenzelm@13415
|
816 |
val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view} =
|
wenzelm@13399
|
817 |
(case kind of Theorem x => x | _ => err_malformed "finish_global" state);
|
wenzelm@5820
|
818 |
|
wenzelm@12146
|
819 |
val ts = flat tss;
|
wenzelm@13415
|
820 |
val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt)
|
wenzelm@13377
|
821 |
(prep_result state ts raw_thm);
|
wenzelm@13377
|
822 |
val results = map (Drule.strip_shyps_warning o
|
wenzelm@13399
|
823 |
ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results;
|
wenzelm@12703
|
824 |
|
wenzelm@12959
|
825 |
val (theory', results') =
|
wenzelm@12959
|
826 |
theory_of state
|
wenzelm@13415
|
827 |
|> (case locale_spec of None => I | Some (loc, (loc_atts, loc_attss)) => fn thy =>
|
wenzelm@12959
|
828 |
if length names <> length loc_attss then
|
wenzelm@12959
|
829 |
raise THEORY ("Bad number of locale attributes", [thy])
|
wenzelm@13335
|
830 |
else (thy, locale_ctxt)
|
wenzelm@12959
|
831 |
|> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss)
|
wenzelm@13335
|
832 |
|> (fn ((thy', ctxt'), res) =>
|
wenzelm@12959
|
833 |
if name = "" andalso null loc_atts then thy'
|
wenzelm@13335
|
834 |
else (thy', ctxt')
|
wenzelm@13377
|
835 |
|> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
|
wenzelm@13415
|
836 |
|> Locale.smart_have_thmss k locale_spec
|
wenzelm@12703
|
837 |
((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
|
wenzelm@12959
|
838 |
|> (fn (thy, res) => (thy, res)
|
wenzelm@13415
|
839 |
|>> (#1 o Locale.smart_have_thmss k locale_spec
|
wenzelm@12959
|
840 |
[((name, atts), [(flat (map #2 res), [])])]));
|
wenzelm@12959
|
841 |
in (theory', ((k, name), results')) end;
|
wenzelm@12959
|
842 |
|
wenzelm@5820
|
843 |
|
wenzelm@10553
|
844 |
(*note: clients should inspect first result only, as backtracking may destroy theory*)
|
wenzelm@6950
|
845 |
fun global_qed finalize state =
|
wenzelm@5820
|
846 |
state
|
wenzelm@6932
|
847 |
|> end_proof true
|
wenzelm@6871
|
848 |
|> finalize
|
wenzelm@12065
|
849 |
|> Seq.map finish_global;
|
wenzelm@5820
|
850 |
|
wenzelm@5820
|
851 |
|
wenzelm@6896
|
852 |
|
wenzelm@6896
|
853 |
(** blocks **)
|
wenzelm@6896
|
854 |
|
wenzelm@6896
|
855 |
(* begin_block *)
|
wenzelm@6896
|
856 |
|
wenzelm@6896
|
857 |
fun begin_block state =
|
wenzelm@6896
|
858 |
state
|
wenzelm@6896
|
859 |
|> assert_forward
|
wenzelm@6896
|
860 |
|> new_block
|
wenzelm@6896
|
861 |
|> open_block;
|
wenzelm@6896
|
862 |
|
wenzelm@6896
|
863 |
|
wenzelm@6896
|
864 |
(* end_block *)
|
wenzelm@6896
|
865 |
|
wenzelm@6896
|
866 |
fun end_block state =
|
wenzelm@6896
|
867 |
state
|
wenzelm@6896
|
868 |
|> assert_forward
|
wenzelm@6896
|
869 |
|> close_block
|
wenzelm@6896
|
870 |
|> assert_current_goal false
|
wenzelm@6896
|
871 |
|> close_block
|
wenzelm@6932
|
872 |
|> transfer_facts state;
|
wenzelm@6896
|
873 |
|
wenzelm@6896
|
874 |
|
wenzelm@6896
|
875 |
(* next_block *)
|
wenzelm@6896
|
876 |
|
wenzelm@6896
|
877 |
fun next_block state =
|
wenzelm@6896
|
878 |
state
|
wenzelm@6896
|
879 |
|> assert_forward
|
wenzelm@6896
|
880 |
|> close_block
|
wenzelm@8718
|
881 |
|> new_block
|
wenzelm@8718
|
882 |
|> reset_facts;
|
wenzelm@6896
|
883 |
|
wenzelm@6896
|
884 |
|
wenzelm@5820
|
885 |
end;
|
wenzelm@8152
|
886 |
|
wenzelm@8152
|
887 |
structure BasicProof: BASIC_PROOF = Proof;
|
wenzelm@8152
|
888 |
open BasicProof;
|