author  wenzelm 
Tue, 21 Jun 2005 09:35:30 +0200  
changeset 16510  606d919ad3c3 
parent 16179  fa7e70be26b0 
child 17344  8b2f56aff711 
permissions  rwrr 
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 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

37 
val no_tac : tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

38 
val ORELSE : tactic * tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

39 
val ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

40 
val pause_tac : tactic 
6041  41 
val print_tac : string > tactic 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

42 
val PRIMITIVE : (thm > thm) > tactic 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

43 
val PRIMSEQ : (thm > thm Seq.seq) > tactic 
11916  44 
val RANGE : (int > tactic) list > int > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

45 
val REPEAT : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

46 
val REPEAT1 : tactic > tactic 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

47 
val REPEAT_FIRST : (int > tactic) > tactic 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

48 
val REPEAT_SOME : (int > tactic) > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

49 
val REPEAT_DETERM_N : int > tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

50 
val REPEAT_DETERM : tactic > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

51 
val REPEAT_DETERM1 : tactic > tactic 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

52 
val REPEAT_DETERM_FIRST: (int > tactic) > tactic 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

53 
val REPEAT_DETERM_SOME: (int > tactic) > tactic 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

54 
val DETERM_UNTIL : (thm > bool) > tactic > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

55 
val SELECT_GOAL : tactic > int > tactic 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. 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 
(*** LCFstyle tacticals ***) 

87 

88 
(*the tactical THEN performs one tactic followed by another*) 

4270  89 
fun (tac1 THEN tac2) st = Seq.flat (Seq.map 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 
15531  119 
NONE => tac2 st (*failed; try tactic 2*) 
4270  120 
 seqcell => Seq.flat (*succeeded; use tactic 1*) 
121 
(Seq.map tac1 (Seq.make(fn()=> seqcell))); 

671  122 

123 

0  124 
(*Versions for combining tacticvalued functions, as in 
125 
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) 

1502  126 
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; 
127 
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; 

128 
fun (tac1 APPEND' tac2) x = tac1 x APPEND tac2 x; 

129 
fun (tac1 INTLEAVE' tac2) x = tac1 x INTLEAVE tac2 x; 

0  130 

131 
(*passes all proofs through unchanged; identity of THEN*) 

4270  132 
fun all_tac st = Seq.single st; 
0  133 

134 
(*passes no proofs through; identity of ORELSE and APPEND*) 

4270  135 
fun no_tac st = Seq.empty; 
0  136 

137 

138 
(*Make a tactic deterministic by chopping the tail of the proof sequence*) 

12851  139 
fun DETERM tac = Seq.DETERM tac; 
0  140 

141 
(*Conditional tactical: testfun controls which tactic to use next. 

142 
Beware: due to eager evaluation, both thentac and elsetac are evaluated.*) 

1502  143 
fun COND testfun thenf elsef = (fn prf => 
0  144 
if testfun prf then thenf prf else elsef prf); 
145 

146 
(*Do the tactic or else do nothing*) 

147 
fun TRY tac = tac ORELSE all_tac; 

148 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

149 
(*** Listoriented tactics ***) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

150 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

151 
local 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

152 
(*This version of EVERY avoids backtracking over repeated states*) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

153 

13108  154 
fun EVY (trail, []) st = 
15531  155 
Seq.make (fn()=> SOME(st, 
13108  156 
Seq.make (fn()=> Seq.pull (evyBack trail)))) 
157 
 EVY (trail, tac::tacs) st = 

158 
case Seq.pull(tac st) of 

15531  159 
NONE => evyBack trail (*failed: backtrack*) 
160 
 SOME(st',q) => EVY ((st',q,tacs)::trail, tacs) st' 

4270  161 
and evyBack [] = Seq.empty (*no alternatives*) 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

162 
 evyBack ((st',q,tacs)::trail) = 
13108  163 
case Seq.pull q of 
15531  164 
NONE => evyBack trail 
165 
 SOME(st,q') => if eq_thm (st',st) 

13108  166 
then evyBack ((st',q',tacs)::trail) 
167 
else EVY ((st,q',tacs)::trail, tacs) st 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

168 
in 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

169 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

170 
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

171 
fun EVERY tacs = EVY ([], tacs); 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

172 
end; 
2627  173 

0  174 

1502  175 
(* 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

176 
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); 
0  177 

178 
(*Apply every tactic to 1*) 

1502  179 
fun EVERY1 tacs = EVERY' tacs 1; 
0  180 

181 
(* FIRST [tac1,...,tacn] equals tac1 ORELSE ... ORELSE tacn *) 

15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

182 
fun FIRST tacs = foldr (op ORELSE) no_tac tacs; 
0  183 

1502  184 
(* 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

185 
fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs; 
0  186 

187 
(*Apply first tactic to 1*) 

1502  188 
fun FIRST1 tacs = FIRST' tacs 1; 
0  189 

11916  190 
(*Apply tactics on consecutive subgoals*) 
191 
fun RANGE [] _ = all_tac 

192 
 RANGE (tac :: tacs) i = RANGE tacs (i + 1) THEN tac i; 

193 

0  194 

195 
(*** Tracing tactics ***) 

196 

197 
(*Print the current proof state and pass it on.*) 

13108  198 
fun print_tac msg = 
199 
(fn st => 

12262  200 
(tracing msg; 
15017
9ad392226da5
print_tac now outputs goals through tracechannel
schirmer
parents:
15006
diff
changeset

201 
tracing ((Pretty.string_of o Pretty.chunks o 
9ad392226da5
print_tac now outputs goals through tracechannel
schirmer
parents:
15006
diff
changeset

202 
Display.pretty_goals (! Display.goals_limit)) st); 
9ad392226da5
print_tac now outputs goals through tracechannel
schirmer
parents:
15006
diff
changeset

203 
Seq.single st)); 
0  204 

205 
(*Pause until a line is typed  if nonempty then fail. *) 

13108  206 
fun pause_tac st = 
12262  207 
(tracing "** Press RETURN to continue:"; 
4270  208 
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st 
12262  209 
else (tracing "Goodbye"; Seq.empty)); 
0  210 

211 
exception TRACE_EXIT of thm 

212 
and TRACE_QUIT; 

213 

631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

214 
(*Tracing flags*) 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

215 
val trace_REPEAT= ref false 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

216 
and suppress_tracing = ref false; 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

217 

0  218 
(*Handle all tracing commands for current state and tactic *) 
13108  219 
fun exec_trace_command flag (tac, st) = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

220 
case TextIO.inputLine(TextIO.stdIn) of 
1502  221 
"\n" => tac st 
4270  222 
 "f\n" => Seq.empty 
1502  223 
 "o\n" => (flag:=false; tac st) 
224 
 "s\n" => (suppress_tracing:=true; tac st) 

12262  225 
 "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) 
0  226 
 "quit\n" => raise TRACE_QUIT 
12262  227 
 _ => (tracing 
0  228 
"Type RETURN to continue or...\n\ 
229 
\ f  to fail here\n\ 

230 
\ 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

231 
\ s  to suppress tracing until next entry to a tactical\n\ 
0  232 
\ x  to exit at this point\n\ 
233 
\ quit  to abort this tracing run\n\ 

1502  234 
\** Well? " ; exec_trace_command flag (tac, st)); 
0  235 

236 

237 
(*Extract from a tactic, a thm>thm seq function that handles tracing*) 

1502  238 
fun tracify flag tac st = 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

239 
if !flag andalso not (!suppress_tracing) 
12082  240 
then (Display.print_goals (! Display.goals_limit) st; 
12262  241 
tracing "** Press RETURN to continue:"; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

242 
exec_trace_command flag (tac,st)) 
1502  243 
else tac st; 
0  244 

245 
(*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) 

13108  246 
fun traced_tac seqf st = 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

247 
(suppress_tracing := false; 
4270  248 
Seq.make (fn()=> seqf st 
15531  249 
handle TRACE_EXIT st' => SOME(st', Seq.empty))); 
0  250 

251 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

252 
(*Deterministic DO..UNTIL: only retains the first outcome; tail recursive. 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

253 
Forces repitition until predicate on state is fulfilled.*) 
13108  254 
fun DETERM_UNTIL p tac = 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

255 
let val tac = tracify trace_REPEAT tac 
15531  256 
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

257 
else (case Seq.pull(tac st) of 
15531  258 
NONE => NONE 
259 
 SOME(st',_) => drep st') 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

260 
in traced_tac drep end; 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

261 

13108  262 
(*Deterministic REPEAT: only retains the first outcome; 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

263 
uses less space than REPEAT; tail recursive. 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

264 
If nonnegative, n bounds the number of repetitions.*) 
13108  265 
fun REPEAT_DETERM_N n tac = 
1502  266 
let val tac = tracify trace_REPEAT tac 
15531  267 
fun drep 0 st = SOME(st, Seq.empty) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

268 
 drep n st = 
4270  269 
(case Seq.pull(tac st) of 
15531  270 
NONE => SOME(st, Seq.empty) 
271 
 SOME(st',_) => drep (n1) st') 

703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

272 
in traced_tac (drep n) end; 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

273 

3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

274 
(*Allows any number of repetitions*) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

275 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  276 

277 
(*General REPEAT: maintains a stack of alternatives; tail recursive*) 

13108  278 
fun REPEAT tac = 
1502  279 
let val tac = tracify trace_REPEAT tac 
13108  280 
fun rep qs st = 
4270  281 
case Seq.pull(tac st) of 
15531  282 
NONE => SOME(st, Seq.make(fn()=> repq qs)) 
283 
 SOME(st',q) => rep (q::qs) st' 

284 
and repq [] = NONE 

4270  285 
 repq(q::qs) = case Seq.pull q of 
15531  286 
NONE => repq qs 
287 
 SOME(st,q) => rep (q::qs) st 

0  288 
in traced_tac (rep []) end; 
289 

290 
(*Repeat 1 or more times*) 

703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

291 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  292 
fun REPEAT1 tac = tac THEN REPEAT tac; 
293 

294 

295 
(** Filtering tacticals **) 

296 

4270  297 
fun FILTER pred tac st = Seq.filter pred (tac st); 
0  298 

13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset

299 
(*Accept only next states that change the theorem somehow*) 
13108  300 
fun CHANGED tac st = 
301 
let fun diff st' = not (Thm.eq_thm (st, st')); 

302 
in Seq.filter diff (tac st) end; 

0  303 

13650
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset

304 
(*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

305 
(changes to signature, hyps, etc. don't count)*) 
13108  306 
fun CHANGED_PROP tac st = 
307 
let fun diff st' = not (Drule.eq_thm_prop (st, st')); 

308 
in Seq.filter diff (tac st) end; 

10821  309 

0  310 

311 
(*** Tacticals based on subgoal numbering ***) 

312 

13108  313 
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) 
1502  314 
Essential to work backwards since tac(i) may add/delete subgoals at i. *) 
13108  315 
fun ALLGOALS tac st = 
1502  316 
let fun doall 0 = all_tac 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

317 
 doall n = tac(n) THEN doall(n1) 
1502  318 
in doall(nprems_of st)st end; 
0  319 

1502  320 
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) 
13108  321 
fun SOMEGOAL tac st = 
1502  322 
let fun find 0 = no_tac 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

323 
 find n = tac(n) ORELSE find(n1) 
1502  324 
in find(nprems_of st)st end; 
0  325 

1502  326 
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). 
0  327 
More appropriate than SOMEGOAL in some cases.*) 
13108  328 
fun FIRSTGOAL tac st = 
1502  329 
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) 
330 
in find(1, nprems_of st)st end; 

0  331 

1502  332 
(*Repeatedly solve some using tac. *) 
333 
fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac)); 

334 
fun REPEAT_DETERM_SOME tac = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tac)); 

0  335 

1502  336 
(*Repeatedly solve the first possible subgoal using tac. *) 
337 
fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac)); 

338 
fun REPEAT_DETERM_FIRST tac = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tac)); 

0  339 

1502  340 
(*For n subgoals, tries to apply tac to n,...1 *) 
341 
fun TRYALL tac = ALLGOALS (TRY o tac); 

0  342 

343 

344 
(*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

345 
fun SUBGOAL goalfun i st = 
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset

346 
(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

347 
SOME goal => goalfun (goal, i) st 
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset

348 
 NONE => Seq.empty); 
0  349 

5141  350 
(*Returns all states that have changed in subgoal i, counted from the LAST 
351 
subgoal. For stac, for example.*) 

13108  352 
fun CHANGED_GOAL tac i st = 
7686  353 
let val np = nprems_of st 
354 
val d = npi (*distance from END*) 

5141  355 
val t = List.nth(prems_of st, i1) 
13108  356 
fun diff st' = 
357 
nprems_of st'  d <= 0 (*the subgoal no longer exists*) 

358 
orelse 

7686  359 
not (Pattern.aeconv (t, 
13108  360 
List.nth(prems_of st', 
361 
nprems_of st'  d  1))) 

5141  362 
in Seq.filter diff (tac i st) end 
363 
handle Subscript => Seq.empty (*no subgoal i*); 

364 

4602  365 
fun (tac1 THEN_ALL_NEW tac2) i st = 
8535  366 
st > (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st'  nprems_of st) st')); 
4602  367 

8341  368 
(*repeatedly dig into any emerging subgoals*) 
369 
fun REPEAT_ALL_NEW tac = 

370 
tac THEN_ALL_NEW (TRY o (fn i => REPEAT_ALL_NEW tac i)); 

371 

2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

372 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

373 
(*** SELECT_GOAL ***) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

374 

0  375 
(*Tactical for restricting the effect of a tactic to subgoal i. 
1502  376 
Works by making a new state from subgoal i, applying tac to it, and 
11517  377 
composing the resulting metathm with the original state.*) 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

378 

a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

379 
(*Does the work of SELECT_GOAL. *) 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

380 
fun select tac st i = 
11517  381 
let 
382 
val thm = Drule.mk_triv_goal (adjust_maxidx (List.nth (cprems_of st, i1))); 

383 
fun restore th = Seq.hd (bicompose false (false, th, nprems_of th) 1 

384 
(Thm.incr_indexes (#maxidx (rep_thm th) + 1) Drule.rev_triv_goal)); 

385 
fun next st' = bicompose false (false, restore st', nprems_of st') i st; 

386 
in Seq.flat (Seq.map next (tac thm)) 

2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

387 
end; 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

388 

13108  389 
fun SELECT_GOAL tac i st = 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

390 
let val np = nprems_of st 
13108  391 
in if 1<=i andalso i<=np then 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

392 
(*If only one subgoal, then just apply tactic*) 
13108  393 
if np=1 then tac st else select tac st i 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

394 
else Seq.empty 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

395 
end; 
0  396 

397 

398 
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) 

13108  399 
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. 
400 
Main difference from strip_assums concerns parameters: 

0  401 
it replaces the bound variables by free variables. *) 
13108  402 
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

403 
strip_context_aux (params, H::Hs, B) 
0  404 
 strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = 
405 
let val (b,u) = variant_abs(a,T,t) 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

406 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  407 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
408 

409 
fun strip_context A = strip_context_aux ([],[],A); 

410 

411 

412 
(**** METAHYPS  tactical for using hypotheses as metalevel assumptions 

1502  413 
METAHYPS (fn prems => tac prems) i 
0  414 

415 
converts subgoal i, of the form !!x1...xm. [ A1;...;An] ==> A into a new 

416 
proof state A==>A, supplying A1,...,An as metalevel assumptions (in 

417 
"prems"). The parameters x1,...,xm become free variables. If the 

418 
resulting proof state is [ B1;...;Bk] ==> C (possibly assuming A1,...,An) 

419 
then it is lifted back into the original context, yielding k subgoals. 

420 

421 
Replaces unknowns in the context by Frees having the prefix METAHYP_ 

422 
New unknowns in [ B1;...;Bk] ==> C are lifted over x1,...,xm. 

423 
DOES NOT HANDLE TYPE UNKNOWNS. 

424 
****) 

425 

13108  426 
local 
0  427 

428 
(*Lefttoright replacements: ctpairs = [...,(vi,ti),...]. 

429 
Instantiates distinct free variables by terms of same type.*) 

13108  430 
fun free_instantiate ctpairs = 
0  431 
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); 
432 

433 
fun free_of s ((a,i), T) = 

434 
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

435 
T) 
0  436 

437 
fun mk_inst (var as Var(v,T)) = (var, free_of "METAHYP1_" (v,T)) 

438 
in 

439 

13108  440 
fun metahyps_aux_tac tacf (prem,i) state = 
0  441 
let val {sign,maxidx,...} = rep_thm state 
230  442 
val cterm = cterm_of sign 
0  443 
(*find all vars in the hyps  should find tvars also!*) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

444 
val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem) 
0  445 
val insts = map mk_inst hyps_vars 
446 
(*replace the hyps_vars by Frees*) 

447 
val prem' = subst_atomic insts prem 

448 
val (params,hyps,concl) = strip_context prem' 

449 
val fparams = map Free params 

450 
val cparams = map cterm fparams 

451 
and chyps = map cterm hyps 

452 
val hypths = map assume chyps 

453 
fun swap_ctpair (t,u) = (cterm u, cterm t) 

454 
(*Subgoal variables: make Free; lift type over params*) 

13108  455 
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
456 
if var mem concl_vars 

2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

457 
then (var, true, free_of "METAHYP2_" (v,T)) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

458 
else (var, false, 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

459 
free_of "METAHYP2_" (v, map #2 params >T)) 
0  460 
(*Instantiate subgoal vars by Free applied to params*) 
13108  461 
fun mk_ctpair (t,in_concl,u) = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

462 
if in_concl then (cterm t, cterm u) 
0  463 
else (cterm t, cterm (list_comb (u,fparams))) 
464 
(*Restore Vars with higher type and index*) 

13108  465 
fun mk_subgoal_swap_ctpair 
466 
(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

467 
if in_concl then (cterm u, cterm t) 
0  468 
else (cterm u, cterm(Var((a, i+maxidx), U))) 
469 
(*Embed B in the original context of params and hyps*) 

1502  470 
fun embed B = list_all_free (params, Logic.list_implies (hyps, B)) 
0  471 
(*Strip the context using elimination rules*) 
472 
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths 

473 
(*A form of lifting that discharges assumptions.*) 

13108  474 
fun relift st = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

475 
let val prop = #prop(rep_thm st) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

476 
val subgoal_vars = (*Vars introduced in the subgoals*) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

477 
foldr add_term_vars [] (Logic.strip_imp_prems prop) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

478 
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

479 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

480 
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

481 
val emBs = map (cterm o embed) (prems_of st') 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

482 
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

483 
in (*restore the unknowns to the hypotheses*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

484 
free_instantiate (map swap_ctpair insts @ 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

485 
map mk_subgoal_swap_ctpair subgoal_insts) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

486 
(*discharge assumptions from state in same order*) 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

487 
(implies_intr_list emBs 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

488 
(forall_intr_list cparams (implies_intr_list chyps Cth))) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

489 
end 
0  490 
val subprems = map (forall_elim_vars 0) hypths 
491 
and st0 = trivial (cterm concl) 

492 
(*function to replace the current subgoal*) 

493 
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

494 
i state 
4270  495 
in Seq.flat (Seq.map next (tacf subprems st0)) 
1502  496 
end; 
0  497 
end; 
498 

499 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

500 

15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

501 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm seq.*) 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

502 
fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty; 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

503 

107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

504 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm.*) 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

505 
fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun); 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

506 

107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

507 
(* Inverse (more or less) of PRIMITIVE *) 
15570  508 
fun SINGLE tacf = Option.map fst o Seq.pull o tacf 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

509 

0  510 
end; 
1502  511 

512 
open Tactical; 