wenzelm@17980
|
1 |
(* Title: Pure/goal.ML
|
wenzelm@29345
|
2 |
Author: Makarius
|
wenzelm@17980
|
3 |
|
wenzelm@50076
|
4 |
Goals in tactical theorem proving, with support for forked proofs.
|
wenzelm@17980
|
5 |
*)
|
wenzelm@17980
|
6 |
|
wenzelm@17980
|
7 |
signature BASIC_GOAL =
|
wenzelm@17980
|
8 |
sig
|
wenzelm@32738
|
9 |
val parallel_proofs: int Unsynchronized.ref
|
wenzelm@42577
|
10 |
val parallel_proofs_threshold: int Unsynchronized.ref
|
wenzelm@17980
|
11 |
val SELECT_GOAL: tactic -> int -> tactic
|
wenzelm@23418
|
12 |
val CONJUNCTS: tactic -> int -> tactic
|
wenzelm@23414
|
13 |
val PRECISE_CONJUNCTS: int -> tactic -> int -> tactic
|
wenzelm@32365
|
14 |
val PARALLEL_CHOICE: tactic list -> tactic
|
wenzelm@32365
|
15 |
val PARALLEL_GOALS: tactic -> tactic
|
wenzelm@17980
|
16 |
end;
|
wenzelm@17980
|
17 |
|
wenzelm@17980
|
18 |
signature GOAL =
|
wenzelm@17980
|
19 |
sig
|
wenzelm@17980
|
20 |
include BASIC_GOAL
|
wenzelm@17980
|
21 |
val init: cterm -> thm
|
wenzelm@18027
|
22 |
val protect: thm -> thm
|
wenzelm@17980
|
23 |
val conclude: thm -> thm
|
wenzelm@50860
|
24 |
val check_finished: Proof.context -> thm -> thm
|
wenzelm@32203
|
25 |
val finish: Proof.context -> thm -> thm
|
wenzelm@21604
|
26 |
val norm_result: thm -> thm
|
wenzelm@42548
|
27 |
val fork_name: string -> (unit -> 'a) -> 'a future
|
wenzelm@37186
|
28 |
val fork: (unit -> 'a) -> 'a future
|
wenzelm@50076
|
29 |
val peek_futures: serial -> unit future list
|
wenzelm@50946
|
30 |
val reset_futures: unit -> Future.group list
|
wenzelm@50027
|
31 |
val future_enabled_level: int -> bool
|
wenzelm@29448
|
32 |
val future_enabled: unit -> bool
|
wenzelm@50027
|
33 |
val future_enabled_nested: int -> bool
|
wenzelm@28973
|
34 |
val future_result: Proof.context -> thm future -> term -> thm
|
wenzelm@23356
|
35 |
val prove_internal: cterm list -> cterm -> (thm list -> tactic) -> thm
|
wenzelm@20290
|
36 |
val prove_multi: Proof.context -> string list -> term list -> term list ->
|
wenzelm@20290
|
37 |
({prems: thm list, context: Proof.context} -> tactic) -> thm list
|
wenzelm@28446
|
38 |
val prove_future: Proof.context -> string list -> term list -> term ->
|
wenzelm@28340
|
39 |
({prems: thm list, context: Proof.context} -> tactic) -> thm
|
wenzelm@20290
|
40 |
val prove: Proof.context -> string list -> term list -> term ->
|
wenzelm@20290
|
41 |
({prems: thm list, context: Proof.context} -> tactic) -> thm
|
wenzelm@26713
|
42 |
val prove_global: theory -> string list -> term list -> term ->
|
wenzelm@26713
|
43 |
({prems: thm list, context: Proof.context} -> tactic) -> thm
|
wenzelm@19184
|
44 |
val extract: int -> int -> thm -> thm Seq.seq
|
wenzelm@19184
|
45 |
val retrofit: int -> int -> thm -> thm -> thm Seq.seq
|
wenzelm@23418
|
46 |
val conjunction_tac: int -> tactic
|
wenzelm@23414
|
47 |
val precise_conjunction_tac: int -> int -> tactic
|
wenzelm@23418
|
48 |
val recover_conjunction_tac: tactic
|
wenzelm@21687
|
49 |
val norm_hhf_tac: int -> tactic
|
wenzelm@21687
|
50 |
val compose_hhf_tac: thm -> int -> tactic
|
wenzelm@23237
|
51 |
val assume_rule_tac: Proof.context -> int -> tactic
|
wenzelm@17980
|
52 |
end;
|
wenzelm@17980
|
53 |
|
wenzelm@17980
|
54 |
structure Goal: GOAL =
|
wenzelm@17980
|
55 |
struct
|
wenzelm@17980
|
56 |
|
wenzelm@18027
|
57 |
(** goals **)
|
wenzelm@17980
|
58 |
|
wenzelm@17980
|
59 |
(*
|
wenzelm@18027
|
60 |
-------- (init)
|
wenzelm@18027
|
61 |
C ==> #C
|
wenzelm@17980
|
62 |
*)
|
wenzelm@20290
|
63 |
val init =
|
wenzelm@22902
|
64 |
let val A = #1 (Thm.dest_implies (Thm.cprop_of Drule.protectI))
|
wenzelm@20290
|
65 |
in fn C => Thm.instantiate ([], [(A, C)]) Drule.protectI end;
|
wenzelm@17980
|
66 |
|
wenzelm@17980
|
67 |
(*
|
wenzelm@18119
|
68 |
C
|
wenzelm@18119
|
69 |
--- (protect)
|
wenzelm@18119
|
70 |
#C
|
wenzelm@18027
|
71 |
*)
|
wenzelm@29345
|
72 |
fun protect th = Drule.comp_no_flatten (th, 0) 1 Drule.protectI;
|
wenzelm@18027
|
73 |
|
wenzelm@18027
|
74 |
(*
|
wenzelm@18027
|
75 |
A ==> ... ==> #C
|
wenzelm@18027
|
76 |
---------------- (conclude)
|
wenzelm@17980
|
77 |
A ==> ... ==> C
|
wenzelm@17980
|
78 |
*)
|
wenzelm@29345
|
79 |
fun conclude th = Drule.comp_no_flatten (th, Thm.nprems_of th) 1 Drule.protectD;
|
wenzelm@17980
|
80 |
|
wenzelm@17980
|
81 |
(*
|
wenzelm@18027
|
82 |
#C
|
wenzelm@18027
|
83 |
--- (finish)
|
wenzelm@18027
|
84 |
C
|
wenzelm@17983
|
85 |
*)
|
wenzelm@32203
|
86 |
fun check_finished ctxt th =
|
wenzelm@17980
|
87 |
(case Thm.nprems_of th of
|
wenzelm@50860
|
88 |
0 => th
|
wenzelm@17980
|
89 |
| n => raise THM ("Proof failed.\n" ^
|
wenzelm@50862
|
90 |
Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
|
wenzelm@32203
|
91 |
|
wenzelm@50860
|
92 |
fun finish ctxt = check_finished ctxt #> conclude;
|
wenzelm@17980
|
93 |
|
wenzelm@17980
|
94 |
|
wenzelm@18027
|
95 |
|
wenzelm@18027
|
96 |
(** results **)
|
wenzelm@18027
|
97 |
|
wenzelm@28340
|
98 |
(* normal form *)
|
wenzelm@28340
|
99 |
|
wenzelm@21604
|
100 |
val norm_result =
|
wenzelm@21604
|
101 |
Drule.flexflex_unique
|
wenzelm@41494
|
102 |
#> Raw_Simplifier.norm_hhf_protect
|
wenzelm@21604
|
103 |
#> Thm.strip_shyps
|
wenzelm@21604
|
104 |
#> Drule.zero_var_indexes;
|
wenzelm@21604
|
105 |
|
wenzelm@21604
|
106 |
|
wenzelm@42577
|
107 |
(* forked proofs *)
|
wenzelm@42577
|
108 |
|
wenzelm@50076
|
109 |
local
|
wenzelm@42577
|
110 |
|
wenzelm@50076
|
111 |
val forked_proofs =
|
wenzelm@50076
|
112 |
Synchronized.var "forked_proofs"
|
wenzelm@50076
|
113 |
(0, []: Future.group list, Inttab.empty: unit future list Inttab.table);
|
wenzelm@50076
|
114 |
|
wenzelm@50076
|
115 |
fun count_forked i =
|
wenzelm@50076
|
116 |
Synchronized.change forked_proofs (fn (m, groups, tab) =>
|
wenzelm@42577
|
117 |
let
|
wenzelm@42577
|
118 |
val n = m + i;
|
wenzelm@51989
|
119 |
val _ = Future.forked_proofs := n;
|
wenzelm@50076
|
120 |
in (n, groups, tab) end);
|
wenzelm@50076
|
121 |
|
wenzelm@50076
|
122 |
fun register_forked id future =
|
wenzelm@50076
|
123 |
Synchronized.change forked_proofs (fn (m, groups, tab) =>
|
wenzelm@50076
|
124 |
let
|
wenzelm@50076
|
125 |
val groups' = Task_Queue.group_of_task (Future.task_of future) :: groups;
|
wenzelm@50076
|
126 |
val tab' = Inttab.cons_list (id, Future.map (K ()) future) tab;
|
wenzelm@50076
|
127 |
in (m, groups', tab') end);
|
wenzelm@37186
|
128 |
|
wenzelm@50051
|
129 |
fun status task markups =
|
wenzelm@51216
|
130 |
let val props = Markup.properties [(Markup.taskN, Task_Queue.str_of_task task)]
|
wenzelm@50051
|
131 |
in Output.status (implode (map (Markup.markup_only o props) markups)) end;
|
wenzelm@50024
|
132 |
|
wenzelm@50076
|
133 |
in
|
wenzelm@50076
|
134 |
|
wenzelm@42548
|
135 |
fun fork_name name e =
|
wenzelm@42577
|
136 |
uninterruptible (fn _ => fn () =>
|
wenzelm@42577
|
137 |
let
|
wenzelm@51929
|
138 |
val pos = Position.thread_data ();
|
wenzelm@51929
|
139 |
val id = the_default 0 (Position.parse_id pos);
|
wenzelm@50076
|
140 |
val _ = count_forked 1;
|
wenzelm@51929
|
141 |
|
wenzelm@42577
|
142 |
val future =
|
wenzelm@45177
|
143 |
(singleton o Future.forks)
|
wenzelm@48287
|
144 |
{name = name, group = NONE, deps = [], pri = ~1, interrupts = false}
|
wenzelm@50051
|
145 |
(fn () =>
|
wenzelm@50051
|
146 |
let
|
wenzelm@50051
|
147 |
val task = the (Future.worker_task ());
|
wenzelm@51216
|
148 |
val _ = status task [Markup.running];
|
wenzelm@51929
|
149 |
val result =
|
wenzelm@51929
|
150 |
Exn.capture (Future.interruptible_task e) ()
|
wenzelm@51929
|
151 |
|> Future.identify_result pos;
|
wenzelm@51216
|
152 |
val _ = status task [Markup.finished, Markup.joined];
|
wenzelm@50051
|
153 |
val _ =
|
wenzelm@50056
|
154 |
(case result of
|
wenzelm@50056
|
155 |
Exn.Res _ => ()
|
wenzelm@50056
|
156 |
| Exn.Exn exn =>
|
wenzelm@50845
|
157 |
if id = 0 orelse Exn.is_interrupt exn then ()
|
wenzelm@50844
|
158 |
else
|
wenzelm@51216
|
159 |
(status task [Markup.failed];
|
wenzelm@51216
|
160 |
Output.report (Markup.markup_only Markup.bad);
|
wenzelm@51929
|
161 |
List.app (Future.error_msg pos) (ML_Compiler.exn_messages_ids exn)));
|
wenzelm@50076
|
162 |
val _ = count_forked ~1;
|
wenzelm@50051
|
163 |
in Exn.release result end);
|
wenzelm@51216
|
164 |
val _ = status (Future.task_of future) [Markup.forked];
|
wenzelm@50076
|
165 |
val _ = register_forked id future;
|
wenzelm@42577
|
166 |
in future end) ();
|
wenzelm@29448
|
167 |
|
wenzelm@42548
|
168 |
fun fork e = fork_name "Goal.fork" e;
|
wenzelm@42548
|
169 |
|
wenzelm@50076
|
170 |
fun forked_count () = #1 (Synchronized.value forked_proofs);
|
wenzelm@50076
|
171 |
|
wenzelm@50076
|
172 |
fun peek_futures id =
|
wenzelm@50076
|
173 |
Inttab.lookup_list (#3 (Synchronized.value forked_proofs)) id;
|
wenzelm@50076
|
174 |
|
wenzelm@50946
|
175 |
fun reset_futures () =
|
wenzelm@50946
|
176 |
Synchronized.change_result forked_proofs (fn (m, groups, tab) =>
|
wenzelm@51989
|
177 |
(Future.forked_proofs := 0; (groups, (0, [], Inttab.empty))));
|
wenzelm@50076
|
178 |
|
wenzelm@50076
|
179 |
end;
|
wenzelm@50076
|
180 |
|
wenzelm@42548
|
181 |
|
wenzelm@42577
|
182 |
(* scheduling parameters *)
|
wenzelm@42577
|
183 |
|
wenzelm@32738
|
184 |
val parallel_proofs = Unsynchronized.ref 1;
|
wenzelm@42690
|
185 |
val parallel_proofs_threshold = Unsynchronized.ref 50;
|
wenzelm@29448
|
186 |
|
wenzelm@50027
|
187 |
fun future_enabled_level n =
|
wenzelm@50027
|
188 |
Multithreading.enabled () andalso ! parallel_proofs >= n andalso
|
wenzelm@42577
|
189 |
is_some (Future.worker_task ());
|
wenzelm@32077
|
190 |
|
wenzelm@50027
|
191 |
fun future_enabled () = future_enabled_level 1;
|
wenzelm@50027
|
192 |
|
wenzelm@50027
|
193 |
fun future_enabled_nested n =
|
wenzelm@50027
|
194 |
future_enabled_level n andalso
|
wenzelm@50076
|
195 |
forked_count () < ! parallel_proofs_threshold * Multithreading.max_threads_value ();
|
wenzelm@29448
|
196 |
|
wenzelm@29448
|
197 |
|
wenzelm@28446
|
198 |
(* future_result *)
|
wenzelm@28340
|
199 |
|
wenzelm@28446
|
200 |
fun future_result ctxt result prop =
|
wenzelm@28340
|
201 |
let
|
wenzelm@43231
|
202 |
val thy = Proof_Context.theory_of ctxt;
|
wenzelm@28340
|
203 |
val _ = Context.reject_draft thy;
|
wenzelm@28340
|
204 |
val cert = Thm.cterm_of thy;
|
wenzelm@28340
|
205 |
val certT = Thm.ctyp_of thy;
|
wenzelm@28340
|
206 |
|
wenzelm@30479
|
207 |
val assms = Assumption.all_assms_of ctxt;
|
wenzelm@28340
|
208 |
val As = map Thm.term_of assms;
|
wenzelm@28340
|
209 |
|
wenzelm@28340
|
210 |
val xs = map Free (fold Term.add_frees (prop :: As) []);
|
wenzelm@28340
|
211 |
val fixes = map cert xs;
|
wenzelm@28340
|
212 |
|
wenzelm@28340
|
213 |
val tfrees = fold Term.add_tfrees (prop :: As) [];
|
wenzelm@28340
|
214 |
val instT = map (fn (a, S) => (certT (TVar ((a, 0), S)), certT (TFree (a, S)))) tfrees;
|
wenzelm@28340
|
215 |
|
wenzelm@28340
|
216 |
val global_prop =
|
wenzelm@46216
|
217 |
cert (Logic.varify_types_global (fold_rev Logic.all xs (Logic.list_implies (As, prop))))
|
wenzelm@32072
|
218 |
|> Thm.weaken_sorts (Variable.sorts_of ctxt);
|
wenzelm@28973
|
219 |
val global_result = result |> Future.map
|
wenzelm@33814
|
220 |
(Drule.flexflex_unique #>
|
wenzelm@33814
|
221 |
Thm.adjust_maxidx_thm ~1 #>
|
wenzelm@28973
|
222 |
Drule.implies_intr_list assms #>
|
wenzelm@28973
|
223 |
Drule.forall_intr_list fixes #>
|
wenzelm@36636
|
224 |
Thm.generalize (map #1 tfrees, []) 0 #>
|
wenzelm@36636
|
225 |
Thm.strip_shyps);
|
wenzelm@28340
|
226 |
val local_result =
|
wenzelm@32072
|
227 |
Thm.future global_result global_prop
|
wenzelm@52002
|
228 |
|> Thm.close_derivation
|
wenzelm@28340
|
229 |
|> Thm.instantiate (instT, [])
|
wenzelm@28340
|
230 |
|> Drule.forall_elim_list fixes
|
wenzelm@28340
|
231 |
|> fold (Thm.elim_implies o Thm.assume) assms;
|
wenzelm@28340
|
232 |
in local_result end;
|
wenzelm@28340
|
233 |
|
wenzelm@28340
|
234 |
|
wenzelm@18027
|
235 |
|
wenzelm@18027
|
236 |
(** tactical theorem proving **)
|
wenzelm@18027
|
237 |
|
wenzelm@23356
|
238 |
(* prove_internal -- minimal checks, no normalization of result! *)
|
wenzelm@20250
|
239 |
|
wenzelm@23356
|
240 |
fun prove_internal casms cprop tac =
|
wenzelm@20250
|
241 |
(case SINGLE (tac (map Assumption.assume casms)) (init cprop) of
|
wenzelm@32203
|
242 |
SOME th => Drule.implies_intr_list casms
|
wenzelm@32203
|
243 |
(finish (Syntax.init_pretty_global (Thm.theory_of_thm th)) th)
|
wenzelm@39201
|
244 |
| NONE => error "Tactic failed");
|
wenzelm@20250
|
245 |
|
wenzelm@20250
|
246 |
|
wenzelm@28340
|
247 |
(* prove_common etc. *)
|
wenzelm@17986
|
248 |
|
wenzelm@28340
|
249 |
fun prove_common immediate ctxt xs asms props tac =
|
wenzelm@17980
|
250 |
let
|
wenzelm@43231
|
251 |
val thy = Proof_Context.theory_of ctxt;
|
wenzelm@26939
|
252 |
val string_of_term = Syntax.string_of_term ctxt;
|
wenzelm@20056
|
253 |
|
wenzelm@28355
|
254 |
val pos = Position.thread_data ();
|
wenzelm@20250
|
255 |
fun err msg = cat_error msg
|
wenzelm@20250
|
256 |
("The error(s) above occurred for the goal statement:\n" ^
|
wenzelm@28355
|
257 |
string_of_term (Logic.list_implies (asms, Logic.mk_conjunction_list props)) ^
|
wenzelm@50007
|
258 |
(case Position.here pos of "" => "" | s => "\n" ^ s));
|
wenzelm@17980
|
259 |
|
wenzelm@20250
|
260 |
fun cert_safe t = Thm.cterm_of thy (Envir.beta_norm (Term.no_dummy_patterns t))
|
wenzelm@17980
|
261 |
handle TERM (msg, _) => err msg | TYPE (msg, _, _) => err msg;
|
wenzelm@20250
|
262 |
val casms = map cert_safe asms;
|
wenzelm@20250
|
263 |
val cprops = map cert_safe props;
|
wenzelm@17980
|
264 |
|
wenzelm@20250
|
265 |
val (prems, ctxt') = ctxt
|
wenzelm@20250
|
266 |
|> Variable.add_fixes_direct xs
|
wenzelm@27218
|
267 |
|> fold Variable.declare_term (asms @ props)
|
wenzelm@26713
|
268 |
|> Assumption.add_assumes casms
|
wenzelm@26713
|
269 |
||> Variable.set_body true;
|
wenzelm@28619
|
270 |
val sorts = Variable.sorts_of ctxt';
|
wenzelm@17980
|
271 |
|
wenzelm@28619
|
272 |
val stmt = Thm.weaken_sorts sorts (Conjunction.mk_conjunction_balanced cprops);
|
wenzelm@28340
|
273 |
|
wenzelm@28340
|
274 |
fun result () =
|
wenzelm@28340
|
275 |
(case SINGLE (tac {prems = prems, context = ctxt'}) (init stmt) of
|
wenzelm@39201
|
276 |
NONE => err "Tactic failed"
|
wenzelm@28340
|
277 |
| SOME st =>
|
wenzelm@32203
|
278 |
let val res = finish ctxt' st handle THM (msg, _, _) => err msg in
|
wenzelm@28619
|
279 |
if Unify.matches_list thy [Thm.term_of stmt] [Thm.prop_of res]
|
wenzelm@28619
|
280 |
then Thm.check_shyps sorts res
|
wenzelm@28340
|
281 |
else err ("Proved a different theorem: " ^ string_of_term (Thm.prop_of res))
|
wenzelm@28340
|
282 |
end);
|
wenzelm@19774
|
283 |
val res =
|
wenzelm@29448
|
284 |
if immediate orelse #maxidx (Thm.rep_cterm stmt) >= 0 orelse not (future_enabled ())
|
wenzelm@29088
|
285 |
then result ()
|
wenzelm@37186
|
286 |
else future_result ctxt' (fork result) (Thm.term_of stmt);
|
wenzelm@17980
|
287 |
in
|
wenzelm@28340
|
288 |
Conjunction.elim_balanced (length props) res
|
wenzelm@20290
|
289 |
|> map (Assumption.export false ctxt' ctxt)
|
wenzelm@20056
|
290 |
|> Variable.export ctxt' ctxt
|
wenzelm@20250
|
291 |
|> map Drule.zero_var_indexes
|
wenzelm@17980
|
292 |
end;
|
wenzelm@17980
|
293 |
|
wenzelm@28341
|
294 |
val prove_multi = prove_common true;
|
wenzelm@17980
|
295 |
|
wenzelm@28446
|
296 |
fun prove_future ctxt xs asms prop tac = hd (prove_common false ctxt xs asms [prop] tac);
|
wenzelm@28340
|
297 |
fun prove ctxt xs asms prop tac = hd (prove_common true ctxt xs asms [prop] tac);
|
wenzelm@20056
|
298 |
|
wenzelm@20056
|
299 |
fun prove_global thy xs asms prop tac =
|
wenzelm@43231
|
300 |
Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
|
wenzelm@18027
|
301 |
|
wenzelm@18027
|
302 |
|
wenzelm@17980
|
303 |
|
wenzelm@21687
|
304 |
(** goal structure **)
|
wenzelm@21687
|
305 |
|
wenzelm@21687
|
306 |
(* nested goals *)
|
wenzelm@17980
|
307 |
|
wenzelm@19184
|
308 |
fun extract i n st =
|
wenzelm@19184
|
309 |
(if i < 1 orelse n < 1 orelse i + n - 1 > Thm.nprems_of st then Seq.empty
|
wenzelm@19184
|
310 |
else if n = 1 then Seq.single (Thm.cprem_of st i)
|
wenzelm@23418
|
311 |
else
|
wenzelm@23418
|
312 |
Seq.single (Conjunction.mk_conjunction_balanced (map (Thm.cprem_of st) (i upto i + n - 1))))
|
wenzelm@20260
|
313 |
|> Seq.map (Thm.adjust_maxidx_cterm ~1 #> init);
|
wenzelm@18207
|
314 |
|
wenzelm@19221
|
315 |
fun retrofit i n st' st =
|
wenzelm@19221
|
316 |
(if n = 1 then st
|
wenzelm@23418
|
317 |
else st |> Drule.with_subgoal i (Conjunction.uncurry_balanced n))
|
wenzelm@19221
|
318 |
|> Thm.compose_no_flatten false (conclude st', Thm.nprems_of st') i;
|
wenzelm@18207
|
319 |
|
wenzelm@17980
|
320 |
fun SELECT_GOAL tac i st =
|
wenzelm@19191
|
321 |
if Thm.nprems_of st = 1 andalso i = 1 then tac st
|
wenzelm@19184
|
322 |
else Seq.lifts (retrofit i 1) (Seq.maps tac (extract i 1 st)) st;
|
wenzelm@17980
|
323 |
|
wenzelm@21687
|
324 |
|
wenzelm@21687
|
325 |
(* multiple goals *)
|
wenzelm@21687
|
326 |
|
wenzelm@23418
|
327 |
fun precise_conjunction_tac 0 i = eq_assume_tac i
|
wenzelm@23418
|
328 |
| precise_conjunction_tac 1 i = SUBGOAL (K all_tac) i
|
wenzelm@23418
|
329 |
| precise_conjunction_tac n i = PRIMITIVE (Drule.with_subgoal i (Conjunction.curry_balanced n));
|
wenzelm@21687
|
330 |
|
wenzelm@23418
|
331 |
val adhoc_conjunction_tac = REPEAT_ALL_NEW
|
wenzelm@23418
|
332 |
(SUBGOAL (fn (goal, i) =>
|
wenzelm@23418
|
333 |
if can Logic.dest_conjunction goal then rtac Conjunction.conjunctionI i
|
wenzelm@23418
|
334 |
else no_tac));
|
wenzelm@23414
|
335 |
|
wenzelm@23418
|
336 |
val conjunction_tac = SUBGOAL (fn (goal, i) =>
|
wenzelm@23418
|
337 |
precise_conjunction_tac (length (Logic.dest_conjunctions goal)) i ORELSE
|
wenzelm@23418
|
338 |
TRY (adhoc_conjunction_tac i));
|
wenzelm@23414
|
339 |
|
wenzelm@23418
|
340 |
val recover_conjunction_tac = PRIMITIVE (fn th =>
|
wenzelm@23418
|
341 |
Conjunction.uncurry_balanced (Thm.nprems_of th) th);
|
wenzelm@23414
|
342 |
|
wenzelm@23414
|
343 |
fun PRECISE_CONJUNCTS n tac =
|
wenzelm@23414
|
344 |
SELECT_GOAL (precise_conjunction_tac n 1
|
wenzelm@23414
|
345 |
THEN tac
|
wenzelm@23418
|
346 |
THEN recover_conjunction_tac);
|
wenzelm@23414
|
347 |
|
wenzelm@21687
|
348 |
fun CONJUNCTS tac =
|
wenzelm@21687
|
349 |
SELECT_GOAL (conjunction_tac 1
|
wenzelm@21687
|
350 |
THEN tac
|
wenzelm@23418
|
351 |
THEN recover_conjunction_tac);
|
wenzelm@21687
|
352 |
|
wenzelm@21687
|
353 |
|
wenzelm@21687
|
354 |
(* hhf normal form *)
|
wenzelm@21687
|
355 |
|
wenzelm@21687
|
356 |
val norm_hhf_tac =
|
wenzelm@21687
|
357 |
rtac Drule.asm_rl (*cheap approximation -- thanks to builtin Logic.flatten_params*)
|
wenzelm@21687
|
358 |
THEN' SUBGOAL (fn (t, i) =>
|
wenzelm@21687
|
359 |
if Drule.is_norm_hhf t then all_tac
|
wenzelm@41494
|
360 |
else rewrite_goal_tac Drule.norm_hhf_eqs i);
|
wenzelm@21687
|
361 |
|
wenzelm@25301
|
362 |
fun compose_hhf_tac th i st =
|
wenzelm@25301
|
363 |
PRIMSEQ (Thm.bicompose false (false, Drule.lift_all (Thm.cprem_of st i) th, 0) i) st;
|
wenzelm@21687
|
364 |
|
wenzelm@23237
|
365 |
|
wenzelm@23237
|
366 |
(* non-atomic goal assumptions *)
|
wenzelm@23237
|
367 |
|
wenzelm@23356
|
368 |
fun non_atomic (Const ("==>", _) $ _ $ _) = true
|
wenzelm@23356
|
369 |
| non_atomic (Const ("all", _) $ _) = true
|
wenzelm@23356
|
370 |
| non_atomic _ = false;
|
wenzelm@23356
|
371 |
|
wenzelm@23237
|
372 |
fun assume_rule_tac ctxt = norm_hhf_tac THEN' CSUBGOAL (fn (goal, i) =>
|
wenzelm@23237
|
373 |
let
|
wenzelm@43367
|
374 |
val ((_, goal'), ctxt') = Variable.focus_cterm goal ctxt;
|
wenzelm@23237
|
375 |
val goal'' = Drule.cterm_rule (singleton (Variable.export ctxt' ctxt)) goal';
|
wenzelm@23356
|
376 |
val Rs = filter (non_atomic o Thm.term_of) (Drule.strip_imp_prems goal'');
|
wenzelm@23237
|
377 |
val tacs = Rs |> map (fn R =>
|
wenzelm@41494
|
378 |
Tactic.etac (Raw_Simplifier.norm_hhf (Thm.trivial R)) THEN_ALL_NEW assume_tac);
|
wenzelm@23237
|
379 |
in fold_rev (curry op APPEND') tacs (K no_tac) i end);
|
wenzelm@23237
|
380 |
|
wenzelm@32365
|
381 |
|
wenzelm@32365
|
382 |
(* parallel tacticals *)
|
wenzelm@32365
|
383 |
|
wenzelm@32365
|
384 |
(*parallel choice of single results*)
|
wenzelm@32365
|
385 |
fun PARALLEL_CHOICE tacs st =
|
wenzelm@32365
|
386 |
(case Par_List.get_some (fn tac => SINGLE tac st) tacs of
|
wenzelm@32365
|
387 |
NONE => Seq.empty
|
wenzelm@32365
|
388 |
| SOME st' => Seq.single st');
|
wenzelm@32365
|
389 |
|
wenzelm@32365
|
390 |
(*parallel refinement of non-schematic goal by single results*)
|
wenzelm@32795
|
391 |
exception FAILED of unit;
|
wenzelm@43241
|
392 |
fun PARALLEL_GOALS tac =
|
wenzelm@43241
|
393 |
Thm.adjust_maxidx_thm ~1 #>
|
wenzelm@43241
|
394 |
(fn st =>
|
wenzelm@43242
|
395 |
if not (Multithreading.enabled ()) orelse Thm.maxidx_of st >= 0 orelse Thm.nprems_of st <= 1
|
wenzelm@43241
|
396 |
then DETERM tac st
|
wenzelm@43241
|
397 |
else
|
wenzelm@43241
|
398 |
let
|
wenzelm@43241
|
399 |
fun try_tac g =
|
wenzelm@43241
|
400 |
(case SINGLE tac g of
|
wenzelm@43241
|
401 |
NONE => raise FAILED ()
|
wenzelm@43241
|
402 |
| SOME g' => g');
|
wenzelm@32365
|
403 |
|
wenzelm@43241
|
404 |
val goals = Drule.strip_imp_prems (Thm.cprop_of st);
|
wenzelm@43241
|
405 |
val results = Par_List.map (try_tac o init) goals;
|
wenzelm@43241
|
406 |
in ALLGOALS (fn i => retrofit i 1 (nth results (i - 1))) st end
|
wenzelm@43241
|
407 |
handle FAILED () => Seq.empty);
|
wenzelm@32365
|
408 |
|
wenzelm@18207
|
409 |
end;
|
wenzelm@18207
|
410 |
|
wenzelm@32365
|
411 |
structure Basic_Goal: BASIC_GOAL = Goal;
|
wenzelm@32365
|
412 |
open Basic_Goal;
|