author | paulson |
Mon, 23 Sep 1996 17:46:12 +0200 | |
changeset 2005 | a52f53caf424 |
parent 1643 | 3f83b629f2e3 |
child 2158 | 77dfe65b5bb3 |
permissions | -rw-r--r-- |
1460 | 1 |
(* Title: tctical |
0 | 2 |
ID: $Id$ |
1460 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
6 |
Tacticals |
|
7 |
*) |
|
8 |
||
1583 | 9 |
infix 1 THEN THEN'; |
0 | 10 |
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; |
11 |
||
671 | 12 |
infix 0 THEN_ELSE; |
13 |
||
0 | 14 |
|
15 |
signature TACTICAL = |
|
16 |
sig |
|
1502 | 17 |
type tactic (* = thm -> thm Sequence.seq*) |
1460 | 18 |
val all_tac : tactic |
19 |
val ALLGOALS : (int -> tactic) -> tactic |
|
20 |
val APPEND : tactic * tactic -> tactic |
|
21 |
val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
22 |
val CHANGED : tactic -> tactic |
|
23 |
val COND : (thm -> bool) -> tactic -> tactic -> tactic |
|
24 |
val DETERM : tactic -> tactic |
|
25 |
val EVERY : tactic list -> tactic |
|
26 |
val EVERY' : ('a -> tactic) list -> 'a -> tactic |
|
27 |
val EVERY1 : (int -> tactic) list -> tactic |
|
28 |
val FILTER : (thm -> bool) -> tactic -> tactic |
|
29 |
val FIRST : tactic list -> tactic |
|
30 |
val FIRST' : ('a -> tactic) list -> 'a -> tactic |
|
31 |
val FIRST1 : (int -> tactic) list -> tactic |
|
32 |
val FIRSTGOAL : (int -> tactic) -> tactic |
|
33 |
val goals_limit : int ref |
|
34 |
val INTLEAVE : tactic * tactic -> tactic |
|
35 |
val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
36 |
val METAHYPS : (thm list -> tactic) -> int -> tactic |
|
37 |
val no_tac : tactic |
|
38 |
val ORELSE : tactic * tactic -> tactic |
|
39 |
val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
40 |
val pause_tac : tactic |
|
41 |
val print_tac : tactic |
|
42 |
val REPEAT : tactic -> tactic |
|
43 |
val REPEAT1 : tactic -> tactic |
|
44 |
val REPEAT_DETERM_N : int -> tactic -> tactic |
|
45 |
val REPEAT_DETERM : tactic -> tactic |
|
46 |
val REPEAT_DETERM1 : tactic -> tactic |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
47 |
val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
48 |
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic |
1460 | 49 |
val REPEAT_FIRST : (int -> tactic) -> tactic |
50 |
val REPEAT_SOME : (int -> tactic) -> tactic |
|
51 |
val SELECT_GOAL : tactic -> int -> tactic |
|
52 |
val SOMEGOAL : (int -> tactic) -> tactic |
|
53 |
val STATE : (thm -> tactic) -> tactic |
|
54 |
val strip_context : term -> (string * typ) list * term list * term |
|
55 |
val SUBGOAL : ((term*int) -> tactic) -> int -> tactic |
|
56 |
val suppress_tracing : bool ref |
|
57 |
val THEN : tactic * tactic -> tactic |
|
58 |
val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
59 |
val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
|
60 |
val traced_tac : (thm -> (thm * thm Sequence.seq) option) -> tactic |
|
61 |
val tracify : bool ref -> tactic -> thm -> thm Sequence.seq |
|
62 |
val trace_REPEAT : bool ref |
|
63 |
val TRY : tactic -> tactic |
|
64 |
val TRYALL : (int -> tactic) -> tactic |
|
0 | 65 |
end; |
66 |
||
67 |
||
1502 | 68 |
structure Tactical : TACTICAL = |
0 | 69 |
struct |
70 |
||
71 |
(**** Tactics ****) |
|
72 |
||
73 |
(*A tactic maps a proof tree to a sequence of proof trees: |
|
74 |
if length of sequence = 0 then the tactic does not apply; |
|
75 |
if length > 1 then backtracking on the alternatives can occur.*) |
|
76 |
||
1502 | 77 |
type tactic = thm -> thm Sequence.seq; |
0 | 78 |
|
79 |
(*Makes a tactic from one that uses the components of the state.*) |
|
1502 | 80 |
fun STATE tacfun st = tacfun st st; |
0 | 81 |
|
82 |
||
83 |
(*** LCF-style tacticals ***) |
|
84 |
||
85 |
(*the tactical THEN performs one tactic followed by another*) |
|
1502 | 86 |
fun (tac1 THEN tac2) st = Sequence.flats (Sequence.maps tac2 (tac1 st)); |
0 | 87 |
|
88 |
||
89 |
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
|
90 |
Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
|
91 |
Does not backtrack to tac2 if tac1 was initially chosen. *) |
|
1502 | 92 |
fun (tac1 ORELSE tac2) st = |
93 |
case Sequence.pull(tac1 st) of |
|
94 |
None => tac2 st |
|
95 |
| sequencecell => Sequence.seqof(fn()=> sequencecell); |
|
0 | 96 |
|
97 |
||
98 |
(*The tactical APPEND combines the results of two tactics. |
|
99 |
Like ORELSE, but allows backtracking on both tac1 and tac2. |
|
100 |
The tactic tac2 is not applied until needed.*) |
|
1502 | 101 |
fun (tac1 APPEND tac2) st = |
102 |
Sequence.append(tac1 st, |
|
103 |
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
|
0 | 104 |
|
105 |
(*Like APPEND, but interleaves results of tac1 and tac2.*) |
|
1502 | 106 |
fun (tac1 INTLEAVE tac2) st = |
107 |
Sequence.interleave(tac1 st, |
|
108 |
Sequence.seqof(fn()=> Sequence.pull (tac2 st))); |
|
0 | 109 |
|
671 | 110 |
(*Conditional tactic. |
1460 | 111 |
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) |
112 |
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) |
|
671 | 113 |
*) |
1502 | 114 |
fun (tac THEN_ELSE (tac1, tac2)) st = |
115 |
case Sequence.pull(tac st) of |
|
116 |
None => tac2 st (*failed; try tactic 2*) |
|
1460 | 117 |
| seqcell => Sequence.flats (*succeeded; use tactic 1*) |
1502 | 118 |
(Sequence.maps tac1 (Sequence.seqof(fn()=> seqcell))); |
671 | 119 |
|
120 |
||
0 | 121 |
(*Versions for combining tactic-valued functions, as in |
122 |
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
|
1502 | 123 |
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; |
124 |
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; |
|
125 |
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; |
|
126 |
fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; |
|
0 | 127 |
|
128 |
(*passes all proofs through unchanged; identity of THEN*) |
|
1502 | 129 |
fun all_tac st = Sequence.single st; |
0 | 130 |
|
131 |
(*passes no proofs through; identity of ORELSE and APPEND*) |
|
1502 | 132 |
fun no_tac st = Sequence.null; |
0 | 133 |
|
134 |
||
135 |
(*Make a tactic deterministic by chopping the tail of the proof sequence*) |
|
1502 | 136 |
fun DETERM tac st = |
137 |
case Sequence.pull (tac st) of |
|
1460 | 138 |
None => Sequence.null |
1502 | 139 |
| Some(x,_) => Sequence.cons(x, Sequence.null); |
0 | 140 |
|
141 |
||
142 |
(*Conditional tactical: testfun controls which tactic to use next. |
|
143 |
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) |
|
1502 | 144 |
fun COND testfun thenf elsef = (fn prf => |
0 | 145 |
if testfun prf then thenf prf else elsef prf); |
146 |
||
147 |
(*Do the tactic or else do nothing*) |
|
148 |
fun TRY tac = tac ORELSE all_tac; |
|
149 |
||
150 |
||
151 |
(*** List-oriented tactics ***) |
|
152 |
||
153 |
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) |
|
154 |
fun EVERY tacs = foldr (op THEN) (tacs, all_tac); |
|
155 |
||
1502 | 156 |
(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) |
157 |
fun EVERY' tacs = foldr (op THEN') (tacs, K all_tac); |
|
0 | 158 |
|
159 |
(*Apply every tactic to 1*) |
|
1502 | 160 |
fun EVERY1 tacs = EVERY' tacs 1; |
0 | 161 |
|
162 |
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) |
|
163 |
fun FIRST tacs = foldr (op ORELSE) (tacs, no_tac); |
|
164 |
||
1502 | 165 |
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) |
166 |
fun FIRST' tacs = foldr (op ORELSE') (tacs, K no_tac); |
|
0 | 167 |
|
168 |
(*Apply first tactic to 1*) |
|
1502 | 169 |
fun FIRST1 tacs = FIRST' tacs 1; |
0 | 170 |
|
171 |
||
172 |
(*** Tracing tactics ***) |
|
173 |
||
174 |
(*Max number of goals to print -- set by user*) |
|
175 |
val goals_limit = ref 10; |
|
176 |
||
177 |
(*Print the current proof state and pass it on.*) |
|
1502 | 178 |
val print_tac = |
179 |
(fn st => |
|
180 |
(!print_goals_ref (!goals_limit) st; Sequence.single st)); |
|
0 | 181 |
|
182 |
(*Pause until a line is typed -- if non-empty then fail. *) |
|
1502 | 183 |
fun pause_tac st = |
0 | 184 |
(prs"** Press RETURN to continue: "; |
1502 | 185 |
if input(std_in,1) = "\n" then Sequence.single st |
186 |
else (prs"Goodbye\n"; Sequence.null)); |
|
0 | 187 |
|
188 |
exception TRACE_EXIT of thm |
|
189 |
and TRACE_QUIT; |
|
190 |
||
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
191 |
(*Tracing flags*) |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
192 |
val trace_REPEAT= ref false |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
193 |
and suppress_tracing = ref false; |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
194 |
|
0 | 195 |
(*Handle all tracing commands for current state and tactic *) |
1502 | 196 |
fun exec_trace_command flag (tac, st) = |
0 | 197 |
case input_line(std_in) of |
1502 | 198 |
"\n" => tac st |
0 | 199 |
| "f\n" => Sequence.null |
1502 | 200 |
| "o\n" => (flag:=false; tac st) |
201 |
| "s\n" => (suppress_tracing:=true; tac st) |
|
202 |
| "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT st)) |
|
0 | 203 |
| "quit\n" => raise TRACE_QUIT |
204 |
| _ => (prs |
|
205 |
"Type RETURN to continue or...\n\ |
|
206 |
\ f - to fail here\n\ |
|
207 |
\ o - to switch tracing off\n\ |
|
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
208 |
\ s - to suppress tracing until next entry to a tactical\n\ |
0 | 209 |
\ x - to exit at this point\n\ |
210 |
\ quit - to abort this tracing run\n\ |
|
1502 | 211 |
\** Well? " ; exec_trace_command flag (tac, st)); |
0 | 212 |
|
213 |
||
214 |
(*Extract from a tactic, a thm->thm seq function that handles tracing*) |
|
1502 | 215 |
fun tracify flag tac st = |
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
216 |
if !flag andalso not (!suppress_tracing) |
1502 | 217 |
then (!print_goals_ref (!goals_limit) st; |
1460 | 218 |
prs"** Press RETURN to continue: "; |
1502 | 219 |
exec_trace_command flag (tac,st)) |
220 |
else tac st; |
|
0 | 221 |
|
222 |
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
|
1502 | 223 |
fun traced_tac seqf st = |
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
224 |
(suppress_tracing := false; |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
225 |
Sequence.seqof (fn()=> seqf st |
1502 | 226 |
handle TRACE_EXIT st' => Some(st', Sequence.null))); |
0 | 227 |
|
228 |
||
229 |
(*Deterministic REPEAT: only retains the first outcome; |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
230 |
uses less space than REPEAT; tail recursive. |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
231 |
If non-negative, n bounds the number of repetitions.*) |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
232 |
fun REPEAT_DETERM_N n tac = |
1502 | 233 |
let val tac = tracify trace_REPEAT tac |
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
234 |
fun drep 0 st = Some(st, Sequence.null) |
1460 | 235 |
| drep n st = |
1502 | 236 |
(case Sequence.pull(tac st) of |
1460 | 237 |
None => Some(st, Sequence.null) |
238 |
| Some(st',_) => drep (n-1) st') |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
239 |
in traced_tac (drep n) end; |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
240 |
|
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
241 |
(*Allows any number of repetitions*) |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
242 |
val REPEAT_DETERM = REPEAT_DETERM_N ~1; |
0 | 243 |
|
244 |
(*General REPEAT: maintains a stack of alternatives; tail recursive*) |
|
245 |
fun REPEAT tac = |
|
1502 | 246 |
let val tac = tracify trace_REPEAT tac |
0 | 247 |
fun rep qs st = |
1502 | 248 |
case Sequence.pull(tac st) of |
1460 | 249 |
None => Some(st, Sequence.seqof(fn()=> repq qs)) |
0 | 250 |
| Some(st',q) => rep (q::qs) st' |
251 |
and repq [] = None |
|
252 |
| repq(q::qs) = case Sequence.pull q of |
|
1460 | 253 |
None => repq qs |
0 | 254 |
| Some(st,q) => rep (q::qs) st |
255 |
in traced_tac (rep []) end; |
|
256 |
||
257 |
(*Repeat 1 or more times*) |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
258 |
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; |
0 | 259 |
fun REPEAT1 tac = tac THEN REPEAT tac; |
260 |
||
261 |
||
262 |
(** Filtering tacticals **) |
|
263 |
||
264 |
(*Returns all states satisfying the predicate*) |
|
1502 | 265 |
fun FILTER pred tac st = Sequence.filters pred (tac st); |
0 | 266 |
|
267 |
(*Returns all changed states*) |
|
1643
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset
|
268 |
fun CHANGED tac st = |
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset
|
269 |
let fun diff st' = not (eq_thm(st,st')) |
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset
|
270 |
in Sequence.filters diff (tac st) end; |
0 | 271 |
|
272 |
||
273 |
(*** Tacticals based on subgoal numbering ***) |
|
274 |
||
1502 | 275 |
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) |
276 |
Essential to work backwards since tac(i) may add/delete subgoals at i. *) |
|
277 |
fun ALLGOALS tac st = |
|
278 |
let fun doall 0 = all_tac |
|
279 |
| doall n = tac(n) THEN doall(n-1) |
|
280 |
in doall(nprems_of st)st end; |
|
0 | 281 |
|
1502 | 282 |
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) |
283 |
fun SOMEGOAL tac st = |
|
284 |
let fun find 0 = no_tac |
|
285 |
| find n = tac(n) ORELSE find(n-1) |
|
286 |
in find(nprems_of st)st end; |
|
0 | 287 |
|
1502 | 288 |
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). |
0 | 289 |
More appropriate than SOMEGOAL in some cases.*) |
1502 | 290 |
fun FIRSTGOAL tac st = |
291 |
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) |
|
292 |
in find(1, nprems_of st)st end; |
|
0 | 293 |
|
1502 | 294 |
(*Repeatedly solve some using tac. *) |
295 |
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); |
|
296 |
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 297 |
|
1502 | 298 |
(*Repeatedly solve the first possible subgoal using tac. *) |
299 |
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); |
|
300 |
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 301 |
|
1502 | 302 |
(*For n subgoals, tries to apply tac to n,...1 *) |
303 |
fun TRYALL tac = ALLGOALS (TRY o tac); |
|
0 | 304 |
|
305 |
||
306 |
(*Make a tactic for subgoal i, if there is one. *) |
|
1502 | 307 |
fun SUBGOAL goalfun i st = |
308 |
case drop(i-1, prems_of st) of |
|
0 | 309 |
[] => Sequence.null |
1502 | 310 |
| prem::_ => goalfun (prem,i) st; |
0 | 311 |
|
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
312 |
|
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
313 |
(*** SELECT_GOAL ***) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
314 |
|
0 | 315 |
(*Tactical for restricting the effect of a tactic to subgoal i. |
1502 | 316 |
Works by making a new state from subgoal i, applying tac to it, and |
0 | 317 |
composing the resulting metathm with the original state. |
318 |
The "main goal" of the new state will not be atomic, some tactics may fail! |
|
319 |
DOES NOT work if tactic affects the main goal other than by instantiation.*) |
|
320 |
||
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
321 |
(*SELECT_GOAL optimization: replace the conclusion by a variable X, |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
322 |
to avoid copying. Proof states have X==concl as an assuption.*) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
323 |
|
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
324 |
val prop_equals = cterm_of Sign.proto_pure |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
325 |
(Const("==", propT-->propT-->propT)); |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
326 |
|
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
327 |
fun mk_prop_equals(t,u) = capply (capply prop_equals t) u; |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
328 |
|
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
329 |
(*Like trivial but returns [ct==X] ct==>X instead of ct==>ct, if possible. |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
330 |
It is paired with a function to undo the transformation. If ct contains |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
331 |
Vars then it returns ct==>ct.*) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
332 |
fun eq_trivial ct = |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
333 |
let val xfree = cterm_of Sign.proto_pure (Free (gensym"X", propT)) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
334 |
val ct_eq_x = mk_prop_equals (adjust_maxidx ct, xfree) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
335 |
and refl_ct = reflexive ct |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
336 |
fun restore th = |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
337 |
implies_elim |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
338 |
(forall_elim ct (forall_intr xfree (implies_intr ct_eq_x th))) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
339 |
refl_ct |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
340 |
in (equal_elim |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
341 |
(combination (combination refl_implies refl_ct) (assume ct_eq_x)) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
342 |
(trivial ct), |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
343 |
restore) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
344 |
end (*Fails if there are Vars or TVars*) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
345 |
handle THM _ => (trivial ct, I); |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
346 |
|
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
347 |
(*Does the work of SELECT_GOAL. *) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
348 |
fun select tac st0 i = |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
349 |
let val cprem::_ = drop(i-1, cprems_of st0) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
350 |
val (eq_cprem, restore) = eq_trivial cprem |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
351 |
fun next st = bicompose false (false, restore st, nprems_of st) i st0 |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
352 |
in Sequence.flats (Sequence.maps next (tac eq_cprem)) |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
353 |
end; |
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
354 |
|
31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset
|
355 |
(* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) |
0 | 356 |
val dummy_quant_rl = |
357 |
standard (forall_elim_var 0 (assume |
|
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
729
diff
changeset
|
358 |
(read_cterm Sign.proto_pure ("!!x::prop. PROP V",propT)))); |
0 | 359 |
|
360 |
(* Prevent the subgoal's assumptions from becoming additional subgoals in the |
|
361 |
new proof state by enclosing them by a universal quantification *) |
|
1502 | 362 |
fun protect_subgoal st i = |
363 |
Sequence.hd (bicompose false (false,dummy_quant_rl,1) i st) |
|
1460 | 364 |
handle _ => error"SELECT_GOAL -- impossible error???"; |
0 | 365 |
|
1502 | 366 |
fun SELECT_GOAL tac i st = |
367 |
case (i, drop(i-1, prems_of st)) of |
|
0 | 368 |
(_,[]) => Sequence.null |
1502 | 369 |
| (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) |
370 |
| (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i |
|
371 |
| (_, _::_) => select tac st i; |
|
0 | 372 |
|
373 |
||
374 |
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
|
375 |
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
|
376 |
Main difference from strip_assums concerns parameters: |
|
377 |
it replaces the bound variables by free variables. *) |
|
378 |
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = |
|
1460 | 379 |
strip_context_aux (params, H::Hs, B) |
0 | 380 |
| strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = |
381 |
let val (b,u) = variant_abs(a,T,t) |
|
1460 | 382 |
in strip_context_aux ((b,T)::params, Hs, u) end |
0 | 383 |
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
384 |
||
385 |
fun strip_context A = strip_context_aux ([],[],A); |
|
386 |
||
387 |
||
388 |
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
|
1502 | 389 |
METAHYPS (fn prems => tac prems) i |
0 | 390 |
|
391 |
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new |
|
392 |
proof state A==>A, supplying A1,...,An as meta-level assumptions (in |
|
393 |
"prems"). The parameters x1,...,xm become free variables. If the |
|
394 |
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) |
|
395 |
then it is lifted back into the original context, yielding k subgoals. |
|
396 |
||
397 |
Replaces unknowns in the context by Frees having the prefix METAHYP_ |
|
398 |
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. |
|
399 |
DOES NOT HANDLE TYPE UNKNOWNS. |
|
400 |
****) |
|
401 |
||
402 |
local |
|
403 |
||
404 |
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
|
405 |
Instantiates distinct free variables by terms of same type.*) |
|
406 |
fun free_instantiate ctpairs = |
|
407 |
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); |
|
408 |
||
409 |
fun free_of s ((a,i), T) = |
|
410 |
Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), |
|
1460 | 411 |
T) |
0 | 412 |
|
413 |
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T)) |
|
414 |
in |
|
415 |
||
1502 | 416 |
fun metahyps_aux_tac tacf (prem,i) state = |
0 | 417 |
let val {sign,maxidx,...} = rep_thm state |
230 | 418 |
val cterm = cterm_of sign |
0 | 419 |
(*find all vars in the hyps -- should find tvars also!*) |
1502 | 420 |
val hyps_vars = foldr add_term_vars (Logic.strip_assums_hyp prem, []) |
0 | 421 |
val insts = map mk_inst hyps_vars |
422 |
(*replace the hyps_vars by Frees*) |
|
423 |
val prem' = subst_atomic insts prem |
|
424 |
val (params,hyps,concl) = strip_context prem' |
|
425 |
val fparams = map Free params |
|
426 |
val cparams = map cterm fparams |
|
427 |
and chyps = map cterm hyps |
|
428 |
val hypths = map assume chyps |
|
429 |
fun swap_ctpair (t,u) = (cterm u, cterm t) |
|
430 |
(*Subgoal variables: make Free; lift type over params*) |
|
431 |
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = |
|
432 |
if var mem concl_vars |
|
1460 | 433 |
then (var, true, free_of "METAHYP2_" (v,T)) |
434 |
else (var, false, |
|
435 |
free_of "METAHYP2_" (v, map #2 params --->T)) |
|
0 | 436 |
(*Instantiate subgoal vars by Free applied to params*) |
437 |
fun mk_ctpair (t,in_concl,u) = |
|
1460 | 438 |
if in_concl then (cterm t, cterm u) |
0 | 439 |
else (cterm t, cterm (list_comb (u,fparams))) |
440 |
(*Restore Vars with higher type and index*) |
|
441 |
fun mk_subgoal_swap_ctpair |
|
1460 | 442 |
(t as Var((a,i),_), in_concl, u as Free(_,U)) = |
443 |
if in_concl then (cterm u, cterm t) |
|
0 | 444 |
else (cterm u, cterm(Var((a, i+maxidx), U))) |
445 |
(*Embed B in the original context of params and hyps*) |
|
1502 | 446 |
fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
0 | 447 |
(*Strip the context using elimination rules*) |
448 |
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
|
449 |
(*Embed an ff pair in the original params*) |
|
1502 | 450 |
fun embed_ff(t,u) = Logic.mk_flexpair (list_abs_free (params, t), |
451 |
list_abs_free (params, u)) |
|
0 | 452 |
(*Remove parameter abstractions from the ff pairs*) |
453 |
fun elim_ff ff = flexpair_abs_elim_list cparams ff |
|
454 |
(*A form of lifting that discharges assumptions.*) |
|
455 |
fun relift st = |
|
1460 | 456 |
let val prop = #prop(rep_thm st) |
457 |
val subgoal_vars = (*Vars introduced in the subgoals*) |
|
1502 | 458 |
foldr add_term_vars (Logic.strip_imp_prems prop, []) |
459 |
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) |
|
1460 | 460 |
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
461 |
val st' = instantiate ([], map mk_ctpair subgoal_insts) st |
|
462 |
val emBs = map (cterm o embed) (prems_of st') |
|
0 | 463 |
and ffs = map (cterm o embed_ff) (tpairs_of st') |
1460 | 464 |
val Cth = implies_elim_list st' |
465 |
(map (elim_ff o assume) ffs @ |
|
466 |
map (elim o assume) emBs) |
|
467 |
in (*restore the unknowns to the hypotheses*) |
|
468 |
free_instantiate (map swap_ctpair insts @ |
|
469 |
map mk_subgoal_swap_ctpair subgoal_insts) |
|
470 |
(*discharge assumptions from state in same order*) |
|
471 |
(implies_intr_list (ffs@emBs) |
|
472 |
(forall_intr_list cparams (implies_intr_list chyps Cth))) |
|
473 |
end |
|
0 | 474 |
val subprems = map (forall_elim_vars 0) hypths |
475 |
and st0 = trivial (cterm concl) |
|
476 |
(*function to replace the current subgoal*) |
|
477 |
fun next st = bicompose false (false, relift st, nprems_of st) |
|
1460 | 478 |
i state |
1502 | 479 |
in Sequence.flats (Sequence.maps next (tacf subprems st0)) |
480 |
end; |
|
0 | 481 |
end; |
482 |
||
483 |
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); |
|
484 |
||
485 |
end; |
|
1502 | 486 |
|
487 |
open Tactical; |