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