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