author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 17969  7262f4a45190 
child 19153  0864119a9611 
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 
15006
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

55 
val SINGLE : tactic > thm > thm option 
13108  56 
val SOMEGOAL : (int > tactic) > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

57 
val strip_context : term > (string * typ) list * term list * term 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

58 
val SUBGOAL : ((term*int) > tactic) > int > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

59 
val suppress_tracing : bool ref 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

61 
val THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic 
13108  62 
val THEN_ALL_NEW : (int > tactic) * (int > tactic) > int > tactic 
63 
val REPEAT_ALL_NEW : (int > tactic) > int > tactic 

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

64 
val THEN_ELSE : tactic * (tactic*tactic) > tactic 
4270  65 
val traced_tac : (thm > (thm * thm Seq.seq) option) > tactic 
5141  66 
val tracify : bool ref > tactic > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

67 
val trace_REPEAT : bool ref 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

68 
val TRY : tactic > tactic 
13108  69 
val TRYALL : (int > tactic) > tactic 
11916  70 
end; 
0  71 

72 

13108  73 
structure Tactical : TACTICAL = 
0  74 
struct 
75 

76 
(**** Tactics ****) 

77 

78 
(*A tactic maps a proof tree to a sequence of proof trees: 

79 
if length of sequence = 0 then the tactic does not apply; 

80 
if length > 1 then backtracking on the alternatives can occur.*) 

81 

4270  82 
type tactic = thm > thm Seq.seq; 
0  83 

84 

85 
(*** LCFstyle tacticals ***) 

86 

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

17344  88 
fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st); 
0  89 

90 

91 
(*The tactical ORELSE uses the first tactic that returns a nonempty sequence. 

92 
Like in LCF, ORELSE commits to either tac1 or tac2 immediately. 

93 
Does not backtrack to tac2 if tac1 was initially chosen. *) 

1502  94 
fun (tac1 ORELSE tac2) st = 
4270  95 
case Seq.pull(tac1 st) of 
15531  96 
NONE => tac2 st 
4270  97 
 sequencecell => Seq.make(fn()=> sequencecell); 
0  98 

99 

100 
(*The tactical APPEND combines the results of two tactics. 

101 
Like ORELSE, but allows backtracking on both tac1 and tac2. 

102 
The tactic tac2 is not applied until needed.*) 

13108  103 
fun (tac1 APPEND tac2) st = 
4270  104 
Seq.append(tac1 st, 
105 
Seq.make(fn()=> Seq.pull (tac2 st))); 

0  106 

107 
(*Like APPEND, but interleaves results of tac1 and tac2.*) 

13108  108 
fun (tac1 INTLEAVE tac2) st = 
4270  109 
Seq.interleave(tac1 st, 
110 
Seq.make(fn()=> Seq.pull (tac2 st))); 

0  111 

671  112 
(*Conditional tactic. 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

113 
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

114 
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) 
671  115 
*) 
13108  116 
fun (tac THEN_ELSE (tac1, tac2)) st = 
4270  117 
case Seq.pull(tac st) of 
17344  118 
NONE => tac2 st (*failed; try tactic 2*) 
119 
 seqcell => Seq.maps tac1 (Seq.make(fn()=> seqcell)); (*succeeded; use tactic 1*) 

671  120 

121 

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

1502  124 
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; 
125 
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; 

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

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

0  128 

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

4270  130 
fun all_tac st = Seq.single st; 
0  131 

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

4270  133 
fun no_tac st = Seq.empty; 
0  134 

135 

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

12851  137 
fun DETERM tac = Seq.DETERM tac; 
0  138 

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

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

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

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

145 
fun TRY tac = tac ORELSE all_tac; 

146 

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

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

148 

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

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

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

151 

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

156 
case Seq.pull(tac st) of 

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

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

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

13108  164 
then evyBack ((st',q',tacs)::trail) 
165 
else EVY ((st,q',tacs)::trail, tacs) st 

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

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

167 

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

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

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

170 
end; 
2627  171 

0  172 

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

174 
fun EVERY' tacs i = EVERY (map (fn f => f i) tacs); 
0  175 

176 
(*Apply every tactic to 1*) 

1502  177 
fun EVERY1 tacs = EVERY' tacs 1; 
0  178 

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

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

180 
fun FIRST tacs = foldr (op ORELSE) no_tac tacs; 
0  181 

1502  182 
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

183 
fun FIRST' tacs = foldr (op ORELSE') (K no_tac) tacs; 
0  184 

185 
(*Apply first tactic to 1*) 

1502  186 
fun FIRST1 tacs = FIRST' tacs 1; 
0  187 

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

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

191 

0  192 

193 
(*** Tracing tactics ***) 

194 

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

13108  196 
fun print_tac msg = 
197 
(fn st => 

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

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

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

201 
Seq.single st)); 
0  202 

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

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

209 
exception TRACE_EXIT of thm 

210 
and TRACE_QUIT; 

211 

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

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

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

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

215 

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

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

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

228 
\ o  to switch tracing off\n\ 

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

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

1502  232 
\** Well? " ; exec_trace_command flag (tac, st)); 
0  233 

234 

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

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

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

240 
exec_trace_command flag (tac,st)) 
1502  241 
else tac st; 
0  242 

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

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

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

249 

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

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

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

253 
let val tac = tracify trace_REPEAT tac 
15531  254 
fun drep st = if p st then SOME (st, Seq.empty) 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
7686
diff
changeset

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

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

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

259 

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

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

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

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

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

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

271 

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

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

273 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  274 

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

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

282 
and repq [] = NONE 

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

0  286 
in traced_tac (rep []) end; 
287 

288 
(*Repeat 1 or more times*) 

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

289 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  290 
fun REPEAT1 tac = tac THEN REPEAT tac; 
291 

292 

293 
(** Filtering tacticals **) 

294 

4270  295 
fun FILTER pred tac st = Seq.filter pred (tac st); 
0  296 

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

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

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

0  301 

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

302 
(*Accept only next states that change the theorem's prop field 
31bd2a8cdbe2
fixing the cut_tac method to work when there are no instantiations and the
paulson
parents:
13108
diff
changeset

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

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

10821  307 

0  308 

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

310 

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

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

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

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

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

0  329 

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

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

0  333 

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

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

0  337 

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

0  340 

341 

342 
(*Make a tactic for subgoal i, if there is one. *) 

16510
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset

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

344 
(case try Logic.nth_prem (i, Thm.prop_of st) of 
606d919ad3c3
tuned SUBGOAL: Logic.nth_prem instead of List.nth o prems_of;
wenzelm
parents:
16179
diff
changeset

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

346 
 NONE => Seq.empty); 
0  347 

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

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

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

356 
orelse 

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

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

362 

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

8341  366 
(*repeatedly dig into any emerging subgoals*) 
367 
fun REPEAT_ALL_NEW tac = 

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

369 

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

370 

0  371 
(*Strips assumptions in goal yielding ( [x1,...,xm], [H1,...,Hn], B ) 
13108  372 
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. 
373 
Main difference from strip_assums concerns parameters: 

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

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

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

379 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  380 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
381 

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

383 

384 

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

1502  386 
METAHYPS (fn prems => tac prems) i 
0  387 

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

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

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

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

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

393 

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

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

396 
DOES NOT HANDLE TYPE UNKNOWNS. 

397 
****) 

398 

13108  399 
local 
0  400 

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

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

13108  403 
fun free_instantiate ctpairs = 
0  404 
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); 
405 

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

407 
Free(s ^ (case i of 0 => a  _ => a ^ "_" ^ string_of_int i), 

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

408 
T) 
0  409 

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

411 
in 

412 

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

417 
val hyps_vars = foldr add_term_vars [] (Logic.strip_assums_hyp prem) 
0  418 
val insts = map mk_inst hyps_vars 
419 
(*replace the hyps_vars by Frees*) 

420 
val prem' = subst_atomic insts prem 

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

422 
val fparams = map Free params 

423 
val cparams = map cterm fparams 

424 
and chyps = map cterm hyps 

425 
val hypths = map assume chyps 

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

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

13108  428 
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
429 
if var mem concl_vars 

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

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

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

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

435 
if in_concl then (cterm t, cterm u) 
0  436 
else (cterm t, cterm (list_comb (u,fparams))) 
437 
(*Restore Vars with higher type and index*) 

13108  438 
fun mk_subgoal_swap_ctpair 
439 
(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

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

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

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

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

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

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

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

451 
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

452 
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

453 
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

454 
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

455 
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

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

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

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

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

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

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

462 
end 
0  463 
val subprems = map (forall_elim_vars 0) hypths 
464 
and st0 = trivial (cterm concl) 

465 
(*function to replace the current subgoal*) 

466 
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

467 
i state 
17344  468 
in Seq.maps next (tacf subprems st0) end; 
0  469 
end; 
470 

471 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

472 

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

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

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

475 

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

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

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

478 

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

479 
(* Inverse (more or less) of PRIMITIVE *) 
15570  480 
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

481 

0  482 
end; 
1502  483 

484 
open Tactical; 