author | wenzelm |
Thu, 27 Jul 2006 13:43:03 +0200 | |
changeset 20225 | 4b8e42490e58 |
parent 20194 | c9dbce9a23a1 |
child 20664 | ffbc5a57191a |
permissions | -rw-r--r-- |
16179 | 1 |
(* Title: Pure/tctical.ML |
0 | 2 |
ID: $Id$ |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1993 University of Cambridge |
5 |
||
16179 | 6 |
Tacticals. |
0 | 7 |
*) |
8 |
||
4602 | 9 |
infix 1 THEN THEN' THEN_ALL_NEW; |
0 | 10 |
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; |
671 | 11 |
infix 0 THEN_ELSE; |
12 |
||
0 | 13 |
|
14 |
signature TACTICAL = |
|
11916 | 15 |
sig |
4270 | 16 |
type tactic (* = thm -> thm Seq.seq*) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
17 |
val all_tac : tactic |
13108 | 18 |
val ALLGOALS : (int -> tactic) -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
19 |
val APPEND : tactic * tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
20 |
val APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
21 |
val CHANGED : tactic -> tactic |
10821 | 22 |
val CHANGED_PROP : tactic -> tactic |
13108 | 23 |
val CHANGED_GOAL : (int -> tactic) -> int -> tactic |
24 |
val COND : (thm -> bool) -> tactic -> tactic -> tactic |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
25 |
val DETERM : tactic -> tactic |
13108 | 26 |
val EVERY : tactic list -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
27 |
val EVERY' : ('a -> tactic) list -> 'a -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
28 |
val EVERY1 : (int -> tactic) list -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
29 |
val FILTER : (thm -> bool) -> tactic -> tactic |
13108 | 30 |
val FIRST : tactic list -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
31 |
val FIRST' : ('a -> tactic) list -> 'a -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
32 |
val FIRST1 : (int -> tactic) list -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
33 |
val FIRSTGOAL : (int -> tactic) -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
34 |
val INTLEAVE : tactic * tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
35 |
val INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
36 |
val METAHYPS : (thm list -> tactic) -> int -> tactic |
19153 | 37 |
val metahyps_thms : int -> thm -> thm list option |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
38 |
val no_tac : tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
39 |
val ORELSE : tactic * tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
40 |
val ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
41 |
val pause_tac : tactic |
6041 | 42 |
val print_tac : string -> tactic |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
43 |
val PRIMITIVE : (thm -> thm) -> tactic |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
44 |
val PRIMSEQ : (thm -> thm Seq.seq) -> tactic |
11916 | 45 |
val RANGE : (int -> tactic) list -> int -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
46 |
val REPEAT : tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
47 |
val REPEAT1 : tactic -> tactic |
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
48 |
val REPEAT_FIRST : (int -> tactic) -> tactic |
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
49 |
val REPEAT_SOME : (int -> tactic) -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
50 |
val REPEAT_DETERM_N : int -> tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
51 |
val REPEAT_DETERM : tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
52 |
val REPEAT_DETERM1 : tactic -> tactic |
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
53 |
val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
54 |
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic |
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
55 |
val DETERM_UNTIL : (thm -> bool) -> tactic -> tactic |
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
56 |
val SINGLE : tactic -> thm -> thm option |
13108 | 57 |
val SOMEGOAL : (int -> tactic) -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
58 |
val strip_context : term -> (string * typ) list * term list * term |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
59 |
val SUBGOAL : ((term*int) -> tactic) -> int -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
60 |
val suppress_tracing : bool ref |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
61 |
val THEN : tactic * tactic -> tactic |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
62 |
val THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
13108 | 63 |
val THEN_ALL_NEW : (int -> tactic) * (int -> tactic) -> int -> tactic |
64 |
val REPEAT_ALL_NEW : (int -> tactic) -> int -> tactic |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
65 |
val THEN_ELSE : tactic * (tactic*tactic) -> tactic |
4270 | 66 |
val traced_tac : (thm -> (thm * thm Seq.seq) option) -> tactic |
5141 | 67 |
val tracify : bool ref -> tactic -> tactic |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
68 |
val trace_REPEAT : bool ref |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
69 |
val TRY : tactic -> tactic |
13108 | 70 |
val TRYALL : (int -> tactic) -> tactic |
11916 | 71 |
end; |
0 | 72 |
|
73 |
||
13108 | 74 |
structure Tactical : TACTICAL = |
0 | 75 |
struct |
76 |
||
77 |
(**** Tactics ****) |
|
78 |
||
79 |
(*A tactic maps a proof tree to a sequence of proof trees: |
|
80 |
if length of sequence = 0 then the tactic does not apply; |
|
81 |
if length > 1 then backtracking on the alternatives can occur.*) |
|
82 |
||
4270 | 83 |
type tactic = thm -> thm Seq.seq; |
0 | 84 |
|
85 |
||
86 |
(*** LCF-style tacticals ***) |
|
87 |
||
88 |
(*the tactical THEN performs one tactic followed by another*) |
|
17344 | 89 |
fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st); |
0 | 90 |
|
91 |
||
92 |
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
|
93 |
Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
|
94 |
Does not backtrack to tac2 if tac1 was initially chosen. *) |
|
1502 | 95 |
fun (tac1 ORELSE tac2) st = |
4270 | 96 |
case Seq.pull(tac1 st) of |
15531 | 97 |
NONE => tac2 st |
4270 | 98 |
| sequencecell => Seq.make(fn()=> sequencecell); |
0 | 99 |
|
100 |
||
101 |
(*The tactical APPEND combines the results of two tactics. |
|
102 |
Like ORELSE, but allows backtracking on both tac1 and tac2. |
|
103 |
The tactic tac2 is not applied until needed.*) |
|
13108 | 104 |
fun (tac1 APPEND tac2) st = |
19861 | 105 |
Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st))); |
0 | 106 |
|
107 |
(*Like APPEND, but interleaves results of tac1 and tac2.*) |
|
13108 | 108 |
fun (tac1 INTLEAVE tac2) st = |
4270 | 109 |
Seq.interleave(tac1 st, |
110 |
Seq.make(fn()=> Seq.pull (tac2 st))); |
|
0 | 111 |
|
671 | 112 |
(*Conditional tactic. |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
113 |
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
114 |
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) |
671 | 115 |
*) |
13108 | 116 |
fun (tac THEN_ELSE (tac1, tac2)) st = |
4270 | 117 |
case Seq.pull(tac st) of |
17344 | 118 |
NONE => tac2 st (*failed; try tactic 2*) |
119 |
| seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*) |
|
671 | 120 |
|
121 |
||
0 | 122 |
(*Versions for combining tactic-valued functions, as in |
123 |
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
|
1502 | 124 |
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; |
125 |
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; |
|
126 |
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; |
|
127 |
fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; |
|
0 | 128 |
|
129 |
(*passes all proofs through unchanged; identity of THEN*) |
|
4270 | 130 |
fun all_tac st = Seq.single st; |
0 | 131 |
|
132 |
(*passes no proofs through; identity of ORELSE and APPEND*) |
|
4270 | 133 |
fun no_tac st = Seq.empty; |
0 | 134 |
|
135 |
||
136 |
(*Make a tactic deterministic by chopping the tail of the proof sequence*) |
|
12851 | 137 |
fun DETERM tac = Seq.DETERM tac; |
0 | 138 |
|
139 |
(*Conditional tactical: testfun controls which tactic to use next. |
|
140 |
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) |
|
1502 | 141 |
fun COND testfun thenf elsef = (fn prf => |
0 | 142 |
if testfun prf then thenf prf else elsef prf); |
143 |
||
144 |
(*Do the tactic or else do nothing*) |
|
145 |
fun TRY tac = tac ORELSE all_tac; |
|
146 |
||
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
147 |
(*** List-oriented tactics ***) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
148 |
|
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
149 |
local |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
150 |
(*This version of EVERY avoids backtracking over repeated states*) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
151 |
|
13108 | 152 |
fun EVY (trail, []) st = |
15531 | 153 |
Seq.make (fn()=> SOME(st, |
13108 | 154 |
Seq.make (fn()=> Seq.pull (evyBack trail)))) |
155 |
| EVY (trail, tac::tacs) st = |
|
156 |
case Seq.pull(tac st) of |
|
15531 | 157 |
NONE => evyBack trail (*failed: backtrack*) |
158 |
| SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st' |
|
4270 | 159 |
and evyBack [] = Seq.empty (*no alternatives*) |
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
160 |
| evyBack ((st',q,tacs)::trail) = |
13108 | 161 |
case Seq.pull q of |
15531 | 162 |
NONE => evyBack trail |
163 |
| SOME(st,q') => if eq_thm (st',st) |
|
13108 | 164 |
then evyBack ((st',q',tacs)::trail) |
165 |
else EVY ((st,q',tacs)::trail, tacs) st |
|
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
166 |
in |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
167 |
|
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
168 |
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
169 |
fun EVERY tacs = EVY ([], tacs); |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
170 |
end; |
2627 | 171 |
|
0 | 172 |
|
1502 | 173 |
(* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *) |
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
174 |
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); |
0 | 175 |
|
176 |
(*Apply every tactic to 1*) |
|
1502 | 177 |
fun EVERY1 tacs = EVERY' tacs 1; |
0 | 178 |
|
179 |
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
180 |
fun FIRST tacs = foldr (op ORELSE) no_tac tacs; |
0 | 181 |
|
1502 | 182 |
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
183 |
fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs; |
0 | 184 |
|
185 |
(*Apply first tactic to 1*) |
|
1502 | 186 |
fun FIRST1 tacs = FIRST' tacs 1; |
0 | 187 |
|
11916 | 188 |
(*Apply tactics on consecutive subgoals*) |
189 |
fun RANGE [] _ = all_tac |
|
190 |
| RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; |
|
191 |
||
0 | 192 |
|
193 |
(*** Tracing tactics ***) |
|
194 |
||
195 |
(*Print the current proof state and pass it on.*) |
|
13108 | 196 |
fun print_tac msg = |
197 |
(fn st => |
|
12262 | 198 |
(tracing msg; |
15017
9ad392226da5
print_tac now outputs goals through trace-channel
schirmer
parents:
15006
diff
changeset
|
199 |
tracing ((Pretty.string_of o Pretty.chunks o |
9ad392226da5
print_tac now outputs goals through trace-channel
schirmer
parents:
15006
diff
changeset
|
200 |
Display.pretty_goals (! Display.goals_limit)) st); |
9ad392226da5
print_tac now outputs goals through trace-channel
schirmer
parents:
15006
diff
changeset
|
201 |
Seq.single st)); |
0 | 202 |
|
203 |
(*Pause until a line is typed -- if non-empty then fail. *) |
|
13108 | 204 |
fun pause_tac st = |
12262 | 205 |
(tracing "** Press RETURN to continue:"; |
4270 | 206 |
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st |
12262 | 207 |
else (tracing "Goodbye"; Seq.empty)); |
0 | 208 |
|
209 |
exception TRACE_EXIT of thm |
|
210 |
and TRACE_QUIT; |
|
211 |
||
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
212 |
(*Tracing flags*) |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
213 |
val trace_REPEAT= ref false |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
214 |
and suppress_tracing = ref false; |
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
215 |
|
0 | 216 |
(*Handle all tracing commands for current state and tactic *) |
13108 | 217 |
fun exec_trace_command flag (tac, st) = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
218 |
case TextIO.inputLine(TextIO.stdIn) of |
1502 | 219 |
"\n" => tac st |
4270 | 220 |
| "f\n" => Seq.empty |
1502 | 221 |
| "o\n" => (flag:=false; tac st) |
222 |
| "s\n" => (suppress_tracing:=true; tac st) |
|
12262 | 223 |
| "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) |
0 | 224 |
| "quit\n" => raise TRACE_QUIT |
12262 | 225 |
| _ => (tracing |
0 | 226 |
"Type RETURN to continue or...\n\ |
227 |
\ f - to fail here\n\ |
|
228 |
\ 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
|
229 |
\ s - to suppress tracing until next entry to a tactical\n\ |
0 | 230 |
\ x - to exit at this point\n\ |
231 |
\ quit - to abort this tracing run\n\ |
|
1502 | 232 |
\** Well? " ; exec_trace_command flag (tac, st)); |
0 | 233 |
|
234 |
||
235 |
(*Extract from a tactic, a thm->thm seq function that handles tracing*) |
|
1502 | 236 |
fun tracify flag tac st = |
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
237 |
if !flag andalso not (!suppress_tracing) |
12082 | 238 |
then (Display.print_goals (! Display.goals_limit) st; |
12262 | 239 |
tracing "** Press RETURN to continue:"; |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
240 |
exec_trace_command flag (tac,st)) |
1502 | 241 |
else tac st; |
0 | 242 |
|
243 |
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
|
13108 | 244 |
fun traced_tac seqf st = |
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
245 |
(suppress_tracing := false; |
4270 | 246 |
Seq.make (fn()=> seqf st |
15531 | 247 |
handle TRACE_EXIT st' => SOME(st', Seq.empty))); |
0 | 248 |
|
249 |
||
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
250 |
(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive. |
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
251 |
Forces repitition until predicate on state is fulfilled.*) |
13108 | 252 |
fun DETERM_UNTIL p tac = |
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
253 |
let val tac = tracify trace_REPEAT tac |
15531 | 254 |
fun drep st = if p st then SOME (st, Seq.empty) |
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
255 |
else (case Seq.pull(tac st) of |
15531 | 256 |
NONE => NONE |
257 |
| SOME(st',_) => drep st') |
|
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
258 |
in traced_tac drep end; |
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset
|
259 |
|
13108 | 260 |
(*Deterministic REPEAT: only retains the first outcome; |
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
261 |
uses less space than REPEAT; tail recursive. |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
262 |
If non-negative, n bounds the number of repetitions.*) |
13108 | 263 |
fun REPEAT_DETERM_N n tac = |
1502 | 264 |
let val tac = tracify trace_REPEAT tac |
15531 | 265 |
fun drep 0 st = SOME(st, Seq.empty) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
266 |
| drep n st = |
4270 | 267 |
(case Seq.pull(tac st) of |
15531 | 268 |
NONE => SOME(st, Seq.empty) |
269 |
| SOME(st',_) => drep (n-1) st') |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
270 |
in traced_tac (drep n) end; |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
271 |
|
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
272 |
(*Allows any number of repetitions*) |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
273 |
val REPEAT_DETERM = REPEAT_DETERM_N ~1; |
0 | 274 |
|
275 |
(*General REPEAT: maintains a stack of alternatives; tail recursive*) |
|
13108 | 276 |
fun REPEAT tac = |
1502 | 277 |
let val tac = tracify trace_REPEAT tac |
13108 | 278 |
fun rep qs st = |
4270 | 279 |
case Seq.pull(tac st) of |
15531 | 280 |
NONE => SOME(st, Seq.make(fn()=> repq qs)) |
281 |
| SOME(st',q) => rep (q::qs) st' |
|
282 |
and repq [] = NONE |
|
4270 | 283 |
| repq(q::qs) = case Seq.pull q of |
15531 | 284 |
NONE => repq qs |
285 |
| SOME(st,q) => rep (q::qs) st |
|
0 | 286 |
in traced_tac (rep []) end; |
287 |
||
288 |
(*Repeat 1 or more times*) |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
289 |
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; |
0 | 290 |
fun REPEAT1 tac = tac THEN REPEAT tac; |
291 |
||
292 |
||
293 |
(** Filtering tacticals **) |
|
294 |
||
4270 | 295 |
fun FILTER pred tac st = Seq.filter pred (tac st); |
0 | 296 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset
|
297 |
(*Accept only next states that change the theorem somehow*) |
13108 | 298 |
fun CHANGED tac st = |
299 |
let fun diff st' = not (Thm.eq_thm (st, st')); |
|
300 |
in Seq.filter diff (tac st) end; |
|
0 | 301 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset
|
302 |
(*Accept only next states that change the theorem's prop field |
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset
|
303 |
(changes to signature, hyps, etc. don't count)*) |
13108 | 304 |
fun CHANGED_PROP tac st = |
305 |
let fun diff st' = not (Drule.eq_thm_prop (st, st')); |
|
306 |
in Seq.filter diff (tac st) end; |
|
10821 | 307 |
|
0 | 308 |
|
309 |
(*** Tacticals based on subgoal numbering ***) |
|
310 |
||
13108 | 311 |
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) |
1502 | 312 |
Essential to work backwards since tac(i) may add/delete subgoals at i. *) |
13108 | 313 |
fun ALLGOALS tac st = |
1502 | 314 |
let fun doall 0 = all_tac |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
315 |
| doall n = tac(n) THEN doall(n-1) |
1502 | 316 |
in doall(nprems_of st)st end; |
0 | 317 |
|
1502 | 318 |
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) |
13108 | 319 |
fun SOMEGOAL tac st = |
1502 | 320 |
let fun find 0 = no_tac |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
321 |
| find n = tac(n) ORELSE find(n-1) |
1502 | 322 |
in find(nprems_of st)st end; |
0 | 323 |
|
1502 | 324 |
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). |
0 | 325 |
More appropriate than SOMEGOAL in some cases.*) |
13108 | 326 |
fun FIRSTGOAL tac st = |
1502 | 327 |
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) |
328 |
in find(1, nprems_of st)st end; |
|
0 | 329 |
|
1502 | 330 |
(*Repeatedly solve some using tac. *) |
331 |
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); |
|
332 |
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 333 |
|
1502 | 334 |
(*Repeatedly solve the first possible subgoal using tac. *) |
335 |
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); |
|
336 |
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 337 |
|
1502 | 338 |
(*For n subgoals, tries to apply tac to n,...1 *) |
339 |
fun TRYALL tac = ALLGOALS (TRY o tac); |
|
0 | 340 |
|
341 |
||
342 |
(*Make a tactic for subgoal i, if there is one. *) |
|
16510
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
343 |
fun SUBGOAL goalfun i st = |
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
344 |
(case try Logic.nth_prem (i, Thm.prop_of st) of |
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
345 |
SOME goal => goalfun (goal, i) st |
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
346 |
| NONE => Seq.empty); |
0 | 347 |
|
5141 | 348 |
(*Returns all states that have changed in subgoal i, counted from the LAST |
349 |
subgoal. For stac, for example.*) |
|
13108 | 350 |
fun CHANGED_GOAL tac i st = |
7686 | 351 |
let val np = nprems_of st |
352 |
val d = np-i (*distance from END*) |
|
5141 | 353 |
val t = List.nth(prems_of st, i-1) |
13108 | 354 |
fun diff st' = |
355 |
nprems_of st' - d <= 0 (*the subgoal no longer exists*) |
|
356 |
orelse |
|
7686 | 357 |
not (Pattern.aeconv (t, |
13108 | 358 |
List.nth(prems_of st', |
359 |
nprems_of st' - d - 1))) |
|
5141 | 360 |
in Seq.filter diff (tac i st) end |
361 |
handle Subscript => Seq.empty (*no subgoal i*); |
|
362 |
||
4602 | 363 |
fun (tac1 THEN_ALL_NEW tac2) i st = |
8535 | 364 |
st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); |
4602 | 365 |
|
8341 | 366 |
(*repeatedly dig into any emerging subgoals*) |
367 |
fun REPEAT_ALL_NEW tac = |
|
368 |
tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i)); |
|
369 |
||
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset
|
370 |
|
0 | 371 |
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) |
13108 | 372 |
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. |
373 |
Main difference from strip_assums concerns parameters: |
|
0 | 374 |
it replaces the bound variables by free variables. *) |
13108 | 375 |
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
376 |
strip_context_aux (params, H::Hs, B) |
0 | 377 |
| strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = |
20194 | 378 |
let val (b,u) = Syntax.variant_abs(a,T,t) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
379 |
in strip_context_aux ((b,T)::params, Hs, u) end |
0 | 380 |
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); |
381 |
||
382 |
fun strip_context A = strip_context_aux ([],[],A); |
|
383 |
||
384 |
||
385 |
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions |
|
1502 | 386 |
METAHYPS (fn prems => tac prems) i |
0 | 387 |
|
388 |
converts subgoal i, of the form !!x1...xm. [| A1;...;An] ==> A into a new |
|
389 |
proof state A==>A, supplying A1,...,An as meta-level assumptions (in |
|
390 |
"prems"). The parameters x1,...,xm become free variables. If the |
|
391 |
resulting proof state is [| B1;...;Bk] ==> C (possibly assuming A1,...,An) |
|
392 |
then it is lifted back into the original context, yielding k subgoals. |
|
393 |
||
394 |
Replaces unknowns in the context by Frees having the prefix METAHYP_ |
|
395 |
New unknowns in [| B1;...;Bk] ==> C are lifted over x1,...,xm. |
|
396 |
DOES NOT HANDLE TYPE UNKNOWNS. |
|
397 |
****) |
|
398 |
||
13108 | 399 |
local |
0 | 400 |
|
401 |
(*Left-to-right replacements: ctpairs = [...,(vi,ti),...]. |
|
402 |
Instantiates distinct free variables by terms of same type.*) |
|
13108 | 403 |
fun free_instantiate ctpairs = |
0 | 404 |
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); |
405 |
||
406 |
fun free_of s ((a,i), T) = |
|
407 |
Free(s ^ (case i of 0 => a | _ => a ^ "_" ^ string_of_int i), |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
408 |
T) |
0 | 409 |
|
410 |
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T)) |
|
411 |
in |
|
412 |
||
19153 | 413 |
(*Common code for METAHYPS and metahyps_thms*) |
414 |
fun metahyps_split_prem prem = |
|
415 |
let (*find all vars in the hyps -- should find tvars also!*) |
|
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
416 |
val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem) |
0 | 417 |
val insts = map mk_inst hyps_vars |
418 |
(*replace the hyps_vars by Frees*) |
|
419 |
val prem' = subst_atomic insts prem |
|
420 |
val (params,hyps,concl) = strip_context prem' |
|
19153 | 421 |
in (insts,params,hyps,concl) end; |
422 |
||
423 |
fun metahyps_aux_tac tacf (prem,gno) state = |
|
424 |
let val (insts,params,hyps,concl) = metahyps_split_prem prem |
|
425 |
val {sign,maxidx,...} = rep_thm state |
|
426 |
val cterm = cterm_of sign |
|
427 |
val chyps = map cterm hyps |
|
428 |
val hypths = map assume chyps |
|
429 |
val subprems = map (forall_elim_vars 0) hypths |
|
0 | 430 |
val fparams = map Free params |
431 |
val cparams = map cterm fparams |
|
432 |
fun swap_ctpair (t,u) = (cterm u, cterm t) |
|
433 |
(*Subgoal variables: make Free; lift type over params*) |
|
13108 | 434 |
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = |
435 |
if var mem concl_vars |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
436 |
then (var, true, free_of "METAHYP2_" (v,T)) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
437 |
else (var, false, |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
438 |
free_of "METAHYP2_" (v, map #2 params --->T)) |
0 | 439 |
(*Instantiate subgoal vars by Free applied to params*) |
13108 | 440 |
fun mk_ctpair (t,in_concl,u) = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
441 |
if in_concl then (cterm t, cterm u) |
0 | 442 |
else (cterm t, cterm (list_comb (u,fparams))) |
443 |
(*Restore Vars with higher type and index*) |
|
13108 | 444 |
fun mk_subgoal_swap_ctpair |
445 |
(t as Var((a,i),_), in_concl, u as Free(_,U)) = |
|
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
446 |
if in_concl then (cterm u, cterm t) |
0 | 447 |
else (cterm u, cterm(Var((a, i+maxidx), U))) |
448 |
(*Embed B in the original context of params and hyps*) |
|
1502 | 449 |
fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) |
0 | 450 |
(*Strip the context using elimination rules*) |
451 |
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths |
|
452 |
(*A form of lifting that discharges assumptions.*) |
|
13108 | 453 |
fun relift st = |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
454 |
let val prop = #prop(rep_thm st) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
455 |
val subgoal_vars = (*Vars introduced in the subgoals*) |
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset
|
456 |
foldr add_term_vars [] (Logic.strip_imp_prems prop) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
457 |
and concl_vars = add_term_vars (Logic.strip_imp_concl prop, []) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
458 |
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars |
13664
cfe1dc32c2e5
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset
|
459 |
val st' = Thm.instantiate ([], map mk_ctpair subgoal_insts) st |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
460 |
val emBs = map (cterm o embed) (prems_of st') |
13664
cfe1dc32c2e5
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset
|
461 |
val Cth = implies_elim_list st' (map (elim o assume) emBs) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
462 |
in (*restore the unknowns to the hypotheses*) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
463 |
free_instantiate (map swap_ctpair insts @ |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
464 |
map mk_subgoal_swap_ctpair subgoal_insts) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
465 |
(*discharge assumptions from state in same order*) |
13664
cfe1dc32c2e5
No more explicit manipulation of flex-flex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset
|
466 |
(implies_intr_list emBs |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
467 |
(forall_intr_list cparams (implies_intr_list chyps Cth))) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
468 |
end |
0 | 469 |
(*function to replace the current subgoal*) |
470 |
fun next st = bicompose false (false, relift st, nprems_of st) |
|
19153 | 471 |
gno state |
472 |
in Seq.maps next (tacf subprems (trivial (cterm concl))) end; |
|
473 |
||
0 | 474 |
end; |
475 |
||
19153 | 476 |
(*Returns the theorem list that METAHYPS would supply to its tactic*) |
477 |
fun metahyps_thms i state = |
|
478 |
let val prem = Logic.nth_prem (i, Thm.prop_of state) |
|
479 |
val (insts,params,hyps,concl) = metahyps_split_prem prem |
|
480 |
val cterm = cterm_of (#sign (rep_thm state)) |
|
481 |
in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end |
|
482 |
handle TERM ("nth_prem", [A]) => NONE; |
|
483 |
||
19455 | 484 |
local |
19229
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset
|
485 |
|
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset
|
486 |
fun print_vars_terms thy (n,thm) = |
19455 | 487 |
let |
19646 | 488 |
fun typed ty = " has type: " ^ Sign.string_of_typ thy ty; |
19455 | 489 |
fun find_vars thy (Const (c, ty)) = |
490 |
(case Term.typ_tvars ty |
|
491 |
of [] => I |
|
19646 | 492 |
| _ => insert (op =) (c ^ typed ty)) |
493 |
| find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty) |
|
19455 | 494 |
| find_vars _ (Free _) = I |
495 |
| find_vars _ (Bound _) = I |
|
496 |
| find_vars thy (Abs (_, _, t)) = find_vars thy t |
|
497 |
| find_vars thy (t1 $ t2) = |
|
498 |
find_vars thy t1 #> find_vars thy t1; |
|
499 |
val prem = Logic.nth_prem (n, Thm.prop_of thm) |
|
500 |
val tms = find_vars thy prem [] |
|
501 |
in |
|
502 |
(warning "Found schematic vars in assumptions:"; warning (cat_lines tms)) |
|
503 |
end; |
|
504 |
||
505 |
in |
|
19229
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset
|
506 |
|
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset
|
507 |
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm |
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset
|
508 |
handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty) |
0 | 509 |
|
19455 | 510 |
end; (*local*) |
511 |
||
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
512 |
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*) |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
513 |
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
514 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
515 |
(*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*) |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
516 |
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
517 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
518 |
(* Inverse (more or less) of PRIMITIVE *) |
15570 | 519 |
fun SINGLE tacf = Option.map fst o Seq.pull o tacf |
19455 | 520 |
|
0 | 521 |
end; |
1502 | 522 |
|
523 |
open Tactical; |