author | blanchet |
Fri, 20 Dec 2013 20:36:38 +0100 | |
changeset 54838 | 16511f84913c |
parent 52131 | 366fa32ee2a3 |
child 56231 | b98813774a63 |
permissions | -rw-r--r-- |
32169 | 1 |
(* Title: Pure/tactical.ML |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
|
16179 | 4 |
Tacticals. |
0 | 5 |
*) |
6 |
||
4602 | 7 |
infix 1 THEN THEN' THEN_ALL_NEW; |
46463 | 8 |
infix 0 ORELSE APPEND ORELSE' APPEND'; |
671 | 9 |
infix 0 THEN_ELSE; |
10 |
||
0 | 11 |
signature TACTICAL = |
11916 | 12 |
sig |
23538 | 13 |
type tactic = thm -> thm Seq.seq |
14 |
val THEN: tactic * tactic -> tactic |
|
15 |
val ORELSE: tactic * tactic -> tactic |
|
16 |
val APPEND: tactic * tactic -> tactic |
|
17 |
val THEN_ELSE: tactic * (tactic*tactic) -> tactic |
|
18 |
val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
19 |
val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
20 |
val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
|
21 |
val all_tac: tactic |
|
22 |
val no_tac: tactic |
|
23 |
val DETERM: tactic -> tactic |
|
24 |
val COND: (thm -> bool) -> tactic -> tactic -> tactic |
|
25 |
val TRY: tactic -> tactic |
|
26 |
val EVERY: tactic list -> tactic |
|
27 |
val EVERY': ('a -> tactic) list -> 'a -> tactic |
|
28 |
val EVERY1: (int -> tactic) list -> tactic |
|
29 |
val FIRST: tactic list -> tactic |
|
30 |
val FIRST': ('a -> tactic) list -> 'a -> tactic |
|
31 |
val FIRST1: (int -> tactic) list -> tactic |
|
32 |
val RANGE: (int -> tactic) list -> int -> tactic |
|
33 |
val print_tac: string -> tactic |
|
34 |
val pause_tac: tactic |
|
32738 | 35 |
val trace_REPEAT: bool Unsynchronized.ref |
36 |
val suppress_tracing: bool Unsynchronized.ref |
|
37 |
val tracify: bool Unsynchronized.ref -> tactic -> tactic |
|
23538 | 38 |
val traced_tac: (thm -> (thm * thm Seq.seq) option) -> tactic |
39 |
val REPEAT_DETERM_N: int -> tactic -> tactic |
|
40 |
val REPEAT_DETERM: tactic -> tactic |
|
41 |
val REPEAT: tactic -> tactic |
|
42 |
val REPEAT_DETERM1: tactic -> tactic |
|
43 |
val REPEAT1: tactic -> tactic |
|
44 |
val FILTER: (thm -> bool) -> tactic -> tactic |
|
45 |
val CHANGED: tactic -> tactic |
|
46 |
val CHANGED_PROP: tactic -> tactic |
|
47 |
val ALLGOALS: (int -> tactic) -> tactic |
|
48 |
val SOMEGOAL: (int -> tactic) -> tactic |
|
49 |
val FIRSTGOAL: (int -> tactic) -> tactic |
|
46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
46463
diff
changeset
|
50 |
val HEADGOAL: (int -> thm -> 'a Seq.seq) -> thm -> 'a Seq.seq |
23538 | 51 |
val REPEAT_SOME: (int -> tactic) -> tactic |
52 |
val REPEAT_DETERM_SOME: (int -> tactic) -> tactic |
|
53 |
val REPEAT_FIRST: (int -> tactic) -> tactic |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
54 |
val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic |
23538 | 55 |
val TRYALL: (int -> tactic) -> tactic |
56 |
val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic |
|
57 |
val SUBGOAL: ((term * int) -> tactic) -> int -> tactic |
|
49865 | 58 |
val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic |
23538 | 59 |
val CHANGED_GOAL: (int -> tactic) -> int -> tactic |
34885
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
60 |
val SOLVED': (int -> tactic) -> int -> tactic |
23538 | 61 |
val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic |
62 |
val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic |
|
63 |
val PRIMSEQ: (thm -> thm Seq.seq) -> tactic |
|
64 |
val PRIMITIVE: (thm -> thm) -> tactic |
|
65 |
val SINGLE: tactic -> thm -> thm option |
|
66 |
val CONVERSION: conv -> int -> tactic |
|
11916 | 67 |
end; |
0 | 68 |
|
13108 | 69 |
structure Tactical : TACTICAL = |
0 | 70 |
struct |
71 |
||
72 |
(**** Tactics ****) |
|
73 |
||
74 |
(*A tactic maps a proof tree to a sequence of proof trees: |
|
75 |
if length of sequence = 0 then the tactic does not apply; |
|
76 |
if length > 1 then backtracking on the alternatives can occur.*) |
|
77 |
||
4270 | 78 |
type tactic = thm -> thm Seq.seq; |
0 | 79 |
|
80 |
||
81 |
(*** LCF-style tacticals ***) |
|
82 |
||
83 |
(*the tactical THEN performs one tactic followed by another*) |
|
17344 | 84 |
fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st); |
0 | 85 |
|
86 |
||
87 |
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. |
|
88 |
Like in LCF, ORELSE commits to either tac1 or tac2 immediately. |
|
89 |
Does not backtrack to tac2 if tac1 was initially chosen. *) |
|
1502 | 90 |
fun (tac1 ORELSE tac2) st = |
4270 | 91 |
case Seq.pull(tac1 st) of |
15531 | 92 |
NONE => tac2 st |
4270 | 93 |
| sequencecell => Seq.make(fn()=> sequencecell); |
0 | 94 |
|
95 |
||
96 |
(*The tactical APPEND combines the results of two tactics. |
|
97 |
Like ORELSE, but allows backtracking on both tac1 and tac2. |
|
98 |
The tactic tac2 is not applied until needed.*) |
|
13108 | 99 |
fun (tac1 APPEND tac2) st = |
19861 | 100 |
Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st))); |
0 | 101 |
|
671 | 102 |
(*Conditional tactic. |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
103 |
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) |
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
104 |
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) |
671 | 105 |
*) |
13108 | 106 |
fun (tac THEN_ELSE (tac1, tac2)) st = |
4270 | 107 |
case Seq.pull(tac st) of |
17344 | 108 |
NONE => tac2 st (*failed; try tactic 2*) |
109 |
| seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*) |
|
671 | 110 |
|
111 |
||
0 | 112 |
(*Versions for combining tactic-valued functions, as in |
113 |
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) |
|
1502 | 114 |
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; |
115 |
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; |
|
116 |
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; |
|
0 | 117 |
|
118 |
(*passes all proofs through unchanged; identity of THEN*) |
|
4270 | 119 |
fun all_tac st = Seq.single st; |
0 | 120 |
|
121 |
(*passes no proofs through; identity of ORELSE and APPEND*) |
|
4270 | 122 |
fun no_tac st = Seq.empty; |
0 | 123 |
|
124 |
||
125 |
(*Make a tactic deterministic by chopping the tail of the proof sequence*) |
|
12851 | 126 |
fun DETERM tac = Seq.DETERM tac; |
0 | 127 |
|
128 |
(*Conditional tactical: testfun controls which tactic to use next. |
|
129 |
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) |
|
1502 | 130 |
fun COND testfun thenf elsef = (fn prf => |
0 | 131 |
if testfun prf then thenf prf else elsef prf); |
132 |
||
133 |
(*Do the tactic or else do nothing*) |
|
134 |
fun TRY tac = tac ORELSE all_tac; |
|
135 |
||
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
136 |
(*** List-oriented tactics ***) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
137 |
|
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
138 |
local |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
139 |
(*This version of EVERY avoids backtracking over repeated states*) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
140 |
|
13108 | 141 |
fun EVY (trail, []) st = |
15531 | 142 |
Seq.make (fn()=> SOME(st, |
13108 | 143 |
Seq.make (fn()=> Seq.pull (evyBack trail)))) |
144 |
| EVY (trail, tac::tacs) st = |
|
145 |
case Seq.pull(tac st) of |
|
15531 | 146 |
NONE => evyBack trail (*failed: backtrack*) |
147 |
| SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st' |
|
4270 | 148 |
and evyBack [] = Seq.empty (*no alternatives*) |
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
149 |
| evyBack ((st',q,tacs)::trail) = |
13108 | 150 |
case Seq.pull q of |
15531 | 151 |
NONE => evyBack trail |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
20664
diff
changeset
|
152 |
| SOME(st,q') => if Thm.eq_thm (st',st) |
13108 | 153 |
then evyBack ((st',q',tacs)::trail) |
154 |
else EVY ((st,q',tacs)::trail, tacs) st |
|
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
155 |
in |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
156 |
|
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
157 |
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
158 |
fun EVERY tacs = EVY ([], tacs); |
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset
|
159 |
end; |
2627 | 160 |
|
0 | 161 |
|
1502 | 162 |
(* 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
|
163 |
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); |
0 | 164 |
|
165 |
(*Apply every tactic to 1*) |
|
1502 | 166 |
fun EVERY1 tacs = EVERY' tacs 1; |
0 | 167 |
|
168 |
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) |
|
23178 | 169 |
fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac; |
0 | 170 |
|
1502 | 171 |
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) |
23178 | 172 |
fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac); |
0 | 173 |
|
174 |
(*Apply first tactic to 1*) |
|
1502 | 175 |
fun FIRST1 tacs = FIRST' tacs 1; |
0 | 176 |
|
11916 | 177 |
(*Apply tactics on consecutive subgoals*) |
178 |
fun RANGE [] _ = all_tac |
|
179 |
| RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; |
|
180 |
||
0 | 181 |
|
182 |
(*** Tracing tactics ***) |
|
183 |
||
184 |
(*Print the current proof state and pass it on.*) |
|
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
185 |
fun print_tac msg st = |
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
186 |
(tracing (msg ^ "\n" ^ |
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
34885
diff
changeset
|
187 |
Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st))); |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
188 |
Seq.single st); |
0 | 189 |
|
190 |
(*Pause until a line is typed -- if non-empty then fail. *) |
|
13108 | 191 |
fun pause_tac st = |
12262 | 192 |
(tracing "** Press RETURN to continue:"; |
24359
44556727197a
TextIO.inputLine: non-critical (assume exclusive ownership);
wenzelm
parents:
23922
diff
changeset
|
193 |
if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st |
12262 | 194 |
else (tracing "Goodbye"; Seq.empty)); |
0 | 195 |
|
196 |
exception TRACE_EXIT of thm |
|
197 |
and TRACE_QUIT; |
|
198 |
||
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
199 |
(*Tracing flags*) |
32738 | 200 |
val trace_REPEAT= Unsynchronized.ref false |
201 |
and suppress_tracing = Unsynchronized.ref false; |
|
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
202 |
|
0 | 203 |
(*Handle all tracing commands for current state and tactic *) |
13108 | 204 |
fun exec_trace_command flag (tac, st) = |
24359
44556727197a
TextIO.inputLine: non-critical (assume exclusive ownership);
wenzelm
parents:
23922
diff
changeset
|
205 |
case TextIO.inputLine TextIO.stdIn of |
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset
|
206 |
SOME "\n" => tac st |
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset
|
207 |
| SOME "f\n" => Seq.empty |
32738 | 208 |
| SOME "o\n" => (flag := false; tac st) |
209 |
| SOME "s\n" => (suppress_tracing := true; tac st) |
|
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset
|
210 |
| SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) |
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset
|
211 |
| SOME "quit\n" => raise TRACE_QUIT |
12262 | 212 |
| _ => (tracing |
0 | 213 |
"Type RETURN to continue or...\n\ |
214 |
\ f - to fail here\n\ |
|
215 |
\ 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
|
216 |
\ s - to suppress tracing until next entry to a tactical\n\ |
0 | 217 |
\ x - to exit at this point\n\ |
218 |
\ quit - to abort this tracing run\n\ |
|
1502 | 219 |
\** Well? " ; exec_trace_command flag (tac, st)); |
0 | 220 |
|
221 |
||
222 |
(*Extract from a tactic, a thm->thm seq function that handles tracing*) |
|
1502 | 223 |
fun tracify flag tac st = |
32145
220c9e439d39
clarified pretty_goals, pretty_thm_aux: plain context;
wenzelm
parents:
32089
diff
changeset
|
224 |
if !flag andalso not (!suppress_tracing) then |
32168
116461b8fc01
eliminated print_goals_without_context -- proper pretty printing;
wenzelm
parents:
32145
diff
changeset
|
225 |
(tracing (Pretty.string_of (Pretty.chunks |
39125
f45d332a90e3
pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context;
wenzelm
parents:
34885
diff
changeset
|
226 |
(Goal_Display.pretty_goals_without_context st @ |
32168
116461b8fc01
eliminated print_goals_without_context -- proper pretty printing;
wenzelm
parents:
32145
diff
changeset
|
227 |
[Pretty.str "** Press RETURN to continue:"]))); |
116461b8fc01
eliminated print_goals_without_context -- proper pretty printing;
wenzelm
parents:
32145
diff
changeset
|
228 |
exec_trace_command flag (tac, st)) |
1502 | 229 |
else tac st; |
0 | 230 |
|
231 |
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) |
|
13108 | 232 |
fun traced_tac seqf st = |
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset
|
233 |
(suppress_tracing := false; |
4270 | 234 |
Seq.make (fn()=> seqf st |
15531 | 235 |
handle TRACE_EXIT st' => SOME(st', Seq.empty))); |
0 | 236 |
|
237 |
||
13108 | 238 |
(*Deterministic REPEAT: only retains the first outcome; |
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
239 |
uses less space than REPEAT; tail recursive. |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
240 |
If non-negative, n bounds the number of repetitions.*) |
13108 | 241 |
fun REPEAT_DETERM_N n tac = |
1502 | 242 |
let val tac = tracify trace_REPEAT tac |
15531 | 243 |
fun drep 0 st = SOME(st, Seq.empty) |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
244 |
| drep n st = |
4270 | 245 |
(case Seq.pull(tac st) of |
15531 | 246 |
NONE => SOME(st, Seq.empty) |
247 |
| SOME(st',_) => drep (n-1) st') |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
248 |
in traced_tac (drep n) end; |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
249 |
|
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
250 |
(*Allows any number of repetitions*) |
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
251 |
val REPEAT_DETERM = REPEAT_DETERM_N ~1; |
0 | 252 |
|
253 |
(*General REPEAT: maintains a stack of alternatives; tail recursive*) |
|
13108 | 254 |
fun REPEAT tac = |
1502 | 255 |
let val tac = tracify trace_REPEAT tac |
13108 | 256 |
fun rep qs st = |
4270 | 257 |
case Seq.pull(tac st) of |
15531 | 258 |
NONE => SOME(st, Seq.make(fn()=> repq qs)) |
259 |
| SOME(st',q) => rep (q::qs) st' |
|
260 |
and repq [] = NONE |
|
4270 | 261 |
| repq(q::qs) = case Seq.pull q of |
15531 | 262 |
NONE => repq qs |
263 |
| SOME(st,q) => rep (q::qs) st |
|
0 | 264 |
in traced_tac (rep []) end; |
265 |
||
266 |
(*Repeat 1 or more times*) |
|
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset
|
267 |
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; |
0 | 268 |
fun REPEAT1 tac = tac THEN REPEAT tac; |
269 |
||
270 |
||
271 |
(** Filtering tacticals **) |
|
272 |
||
4270 | 273 |
fun FILTER pred tac st = Seq.filter pred (tac st); |
0 | 274 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset
|
275 |
(*Accept only next states that change the theorem somehow*) |
13108 | 276 |
fun CHANGED tac st = |
277 |
let fun diff st' = not (Thm.eq_thm (st, st')); |
|
278 |
in Seq.filter diff (tac st) end; |
|
0 | 279 |
|
13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset
|
280 |
(*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
|
281 |
(changes to signature, hyps, etc. don't count)*) |
13108 | 282 |
fun CHANGED_PROP tac st = |
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
20664
diff
changeset
|
283 |
let fun diff st' = not (Thm.eq_thm_prop (st, st')); |
13108 | 284 |
in Seq.filter diff (tac st) end; |
10821 | 285 |
|
0 | 286 |
|
287 |
(*** Tacticals based on subgoal numbering ***) |
|
288 |
||
13108 | 289 |
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) |
1502 | 290 |
Essential to work backwards since tac(i) may add/delete subgoals at i. *) |
13108 | 291 |
fun ALLGOALS tac st = |
1502 | 292 |
let fun doall 0 = all_tac |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
293 |
| doall n = tac(n) THEN doall(n-1) |
1502 | 294 |
in doall(nprems_of st)st end; |
0 | 295 |
|
1502 | 296 |
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) |
13108 | 297 |
fun SOMEGOAL tac st = |
1502 | 298 |
let fun find 0 = no_tac |
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset
|
299 |
| find n = tac(n) ORELSE find(n-1) |
1502 | 300 |
in find(nprems_of st)st end; |
0 | 301 |
|
1502 | 302 |
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). |
0 | 303 |
More appropriate than SOMEGOAL in some cases.*) |
13108 | 304 |
fun FIRSTGOAL tac st = |
1502 | 305 |
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) |
306 |
in find(1, nprems_of st)st end; |
|
0 | 307 |
|
46466
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
46463
diff
changeset
|
308 |
(*First subgoal only.*) |
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
46463
diff
changeset
|
309 |
fun HEADGOAL tac = tac 1; |
61c7214b4885
tuned signature, according to actual usage of these operations;
wenzelm
parents:
46463
diff
changeset
|
310 |
|
1502 | 311 |
(*Repeatedly solve some using tac. *) |
312 |
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); |
|
313 |
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 314 |
|
1502 | 315 |
(*Repeatedly solve the first possible subgoal using tac. *) |
316 |
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); |
|
317 |
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); |
|
0 | 318 |
|
1502 | 319 |
(*For n subgoals, tries to apply tac to n,...1 *) |
320 |
fun TRYALL tac = ALLGOALS (TRY o tac); |
|
0 | 321 |
|
322 |
||
323 |
(*Make a tactic for subgoal i, if there is one. *) |
|
23224 | 324 |
fun CSUBGOAL goalfun i st = |
325 |
(case SOME (Thm.cprem_of st i) handle THM _ => NONE of |
|
16510
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
326 |
SOME goal => goalfun (goal, i) st |
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset
|
327 |
| NONE => Seq.empty); |
0 | 328 |
|
23224 | 329 |
fun SUBGOAL goalfun = |
330 |
CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i)); |
|
331 |
||
49865 | 332 |
fun ASSERT_SUBGOAL (tac: int -> tactic) i st = (Logic.get_goal (Thm.prop_of st) i; tac i st); |
333 |
||
5141 | 334 |
(*Returns all states that have changed in subgoal i, counted from the LAST |
335 |
subgoal. For stac, for example.*) |
|
13108 | 336 |
fun CHANGED_GOAL tac i st = |
30145
09817540ccae
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
wenzelm
parents:
29272
diff
changeset
|
337 |
let val np = Thm.nprems_of st |
7686 | 338 |
val d = np-i (*distance from END*) |
30145
09817540ccae
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
wenzelm
parents:
29272
diff
changeset
|
339 |
val t = Thm.term_of (Thm.cprem_of st i) |
13108 | 340 |
fun diff st' = |
30145
09817540ccae
tuned CHANGED_GOAL: use Thm.cprem_of instead of selecting from Thm.prems_of;
wenzelm
parents:
29272
diff
changeset
|
341 |
Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*) |
13108 | 342 |
orelse |
52131 | 343 |
not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d)))) |
5141 | 344 |
in Seq.filter diff (tac i st) end |
43278 | 345 |
handle General.Subscript => Seq.empty (*no subgoal i*); |
5141 | 346 |
|
34885
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
347 |
(*Returns all states where some subgoals have been solved. For |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
348 |
subgoal-based tactics this means subgoal i has been solved |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
349 |
altogether -- no new subgoals have emerged.*) |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
350 |
fun SOLVED' tac i st = |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
351 |
tac i st |> Seq.filter (fn st' => nprems_of st' < nprems_of st); |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
352 |
|
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
353 |
(*Apply second tactic to all subgoals emerging from the first -- |
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
354 |
following usual convention for subgoal-based tactics.*) |
4602 | 355 |
fun (tac1 THEN_ALL_NEW tac2) i st = |
8535 | 356 |
st |> (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st' - nprems_of st) st')); |
4602 | 357 |
|
34885
6587c24ef6d8
added SOLVED' -- a more direct version of THEN_ALL_NEW (K no_tac) -- strictly speaking it does not even depend on subgoal addressing, but it would be too confusing without it;
wenzelm
parents:
32738
diff
changeset
|
358 |
(*Repeatedly dig into any emerging subgoals.*) |
8341 | 359 |
fun REPEAT_ALL_NEW tac = |
360 |
tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i)); |
|
361 |
||
15006
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
362 |
(*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
|
363 |
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
|
364 |
|
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
365 |
(*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
|
366 |
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); |
107e4dfd3b96
Merging the meta-simplifier with the Provers-simplifier. Next step:
skalberg
parents:
13664
diff
changeset
|
367 |
|
23538 | 368 |
(*Inverse (more or less) of PRIMITIVE*) |
15570 | 369 |
fun SINGLE tacf = Option.map fst o Seq.pull o tacf |
19455 | 370 |
|
23538 | 371 |
(*Conversions as tactics*) |
23584 | 372 |
fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) |
23561 | 373 |
handle THM _ => Seq.empty |
374 |
| CTERM _ => Seq.empty |
|
375 |
| TERM _ => Seq.empty |
|
376 |
| TYPE _ => Seq.empty; |
|
23538 | 377 |
|
0 | 378 |
end; |
1502 | 379 |
|
380 |
open Tactical; |