author  paulson 
Mon, 30 Nov 1998 10:45:39 +0100  
changeset 5997  4d00bbd3d3ac 
parent 5957  9c0c69ab7d02 
child 6041  684ec6a1d802 
permissions  rwrr 
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 

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 = 

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 
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 
5141  22 
val CHANGED_GOAL : (int > tactic) > int > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

25 
val EVERY : tactic list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

26 
val EVERY' : ('a > tactic) list > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

27 
val EVERY1 : (int > tactic) list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

29 
val FIRST : tactic list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

30 
val FIRST' : ('a > tactic) list > 'a > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

31 
val FIRST1 : (int > tactic) list > tactic 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

33 
val goals_limit : int ref 
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 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

57 
val THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic 
4602  58 
val THEN_ALL_NEW : (int > tactic) * (int > tactic) > int > tactic 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

64 
val TRYALL : (int > tactic) > tactic 
0  65 
end; 
66 

67 

1502  68 
structure Tactical : TACTICAL = 
0  69 
struct 
70 

71 
(**** Tactics ****) 

72 

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

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

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

76 

4270  77 
type tactic = thm > thm Seq.seq; 
0  78 

79 

80 
(*** LCFstyle tacticals ***) 

81 

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

4270  83 
fun (tac1 THEN tac2) st = Seq.flat (Seq.map tac2 (tac1 st)); 
0  84 

85 

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

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

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

1502  89 
fun (tac1 ORELSE tac2) st = 
4270  90 
case Seq.pull(tac1 st) of 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

91 
None => tac2 st 
4270  92 
 sequencecell => Seq.make(fn()=> sequencecell); 
0  93 

94 

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

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

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

1502  98 
fun (tac1 APPEND tac2) st = 
4270  99 
Seq.append(tac1 st, 
100 
Seq.make(fn()=> Seq.pull (tac2 st))); 

0  101 

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

1502  103 
fun (tac1 INTLEAVE tac2) st = 
4270  104 
Seq.interleave(tac1 st, 
105 
Seq.make(fn()=> Seq.pull (tac2 st))); 

0  106 

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

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

109 
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) 
671  110 
*) 
1502  111 
fun (tac THEN_ELSE (tac1, tac2)) st = 
4270  112 
case Seq.pull(tac st) of 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

113 
None => tac2 st (*failed; try tactic 2*) 
4270  114 
 seqcell => Seq.flat (*succeeded; use tactic 1*) 
115 
(Seq.map tac1 (Seq.make(fn()=> seqcell))); 

671  116 

117 

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

1502  120 
fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x; 
121 
fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x; 

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

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

0  124 

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

4270  126 
fun all_tac st = Seq.single st; 
0  127 

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

4270  129 
fun no_tac st = Seq.empty; 
0  130 

131 

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

1502  133 
fun DETERM tac st = 
4270  134 
case Seq.pull (tac st) of 
135 
None => Seq.empty 

136 
 Some(x,_) => Seq.cons(x, Seq.empty); 

0  137 

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 

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

152 
fun EVY (trail, []) st = 
4270  153 
Seq.make (fn()=> Some(st, 
154 
Seq.make (fn()=> Seq.pull (evyBack trail)))) 

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

155 
 EVY (trail, tac::tacs) st = 
4270  156 
case Seq.pull(tac st) of 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

157 
None => evyBack trail (*failed: backtrack*) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

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) = 
4270  161 
case Seq.pull q of 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

162 
None => evyBack trail 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

163 
 Some(st,q') => if eq_thm (st',st) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

164 
then evyBack ((st',q',tacs)::trail) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2627
diff
changeset

165 
else EVY ((st,q',tacs)::trail, tacs) st 
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 *) 

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

181 

1502  182 
(* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *) 
183 
fun FIRST' tacs = foldr (op ORELSE') (tacs, K no_tac); 

0  184 

185 
(*Apply first tactic to 1*) 

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

188 

189 
(*** Tracing tactics ***) 

190 

191 
(*Max number of goals to print  set by user*) 

192 
val goals_limit = ref 10; 

193 

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

1502  195 
val print_tac = 
196 
(fn st => 

4270  197 
(print_goals (!goals_limit) st; Seq.single st)); 
0  198 

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

1502  200 
fun pause_tac st = 
5957  201 
(writeln "** Press RETURN to continue:"; 
4270  202 
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st 
5956  203 
else (writeln "Goodbye"; Seq.empty)); 
0  204 

205 
exception TRACE_EXIT of thm 

206 
and TRACE_QUIT; 

207 

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

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

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

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

211 

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

214 
case TextIO.inputLine(TextIO.stdIn) of 
1502  215 
"\n" => tac st 
4270  216 
 "f\n" => Seq.empty 
1502  217 
 "o\n" => (flag:=false; tac st) 
218 
 "s\n" => (suppress_tracing:=true; tac st) 

5956  219 
 "x\n" => (writeln "Exiting now"; raise (TRACE_EXIT st)) 
0  220 
 "quit\n" => raise TRACE_QUIT 
5956  221 
 _ => (writeln 
0  222 
"Type RETURN to continue or...\n\ 
223 
\ f  to fail here\n\ 

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

225 
\ s  to suppress tracing until next entry to a tactical\n\ 
0  226 
\ x  to exit at this point\n\ 
227 
\ quit  to abort this tracing run\n\ 

1502  228 
\** Well? " ; exec_trace_command flag (tac, st)); 
0  229 

230 

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

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

233 
if !flag andalso not (!suppress_tracing) 
3669
3384c6f1f095
removed print_goals_ref (which was broken anyway);
wenzelm
parents:
3561
diff
changeset

234 
then (print_goals (!goals_limit) st; 
5957  235 
writeln "** Press RETURN to continue:"; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

236 
exec_trace_command flag (tac,st)) 
1502  237 
else tac st; 
0  238 

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

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

241 
(suppress_tracing := false; 
4270  242 
Seq.make (fn()=> seqf st 
243 
handle TRACE_EXIT st' => Some(st', Seq.empty))); 

0  244 

245 

246 
(*Deterministic REPEAT: only retains the first outcome; 

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

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

248 
If nonnegative, n bounds the number of repetitions.*) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

249 
fun REPEAT_DETERM_N n tac = 
1502  250 
let val tac = tracify trace_REPEAT tac 
4270  251 
fun drep 0 st = Some(st, Seq.empty) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

252 
 drep n st = 
4270  253 
(case Seq.pull(tac st) of 
254 
None => Some(st, Seq.empty) 

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

255 
 Some(st',_) => drep (n1) st') 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

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

257 

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

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

259 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  260 

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

262 
fun REPEAT tac = 

1502  263 
let val tac = tracify trace_REPEAT tac 
0  264 
fun rep qs st = 
4270  265 
case Seq.pull(tac st) of 
266 
None => Some(st, Seq.make(fn()=> repq qs)) 

0  267 
 Some(st',q) => rep (q::qs) st' 
268 
and repq [] = None 

4270  269 
 repq(q::qs) = case Seq.pull q of 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

270 
None => repq qs 
0  271 
 Some(st,q) => rep (q::qs) st 
272 
in traced_tac (rep []) end; 

273 

274 
(*Repeat 1 or more times*) 

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

275 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  276 
fun REPEAT1 tac = tac THEN REPEAT tac; 
277 

278 

279 
(** Filtering tacticals **) 

280 

281 
(*Returns all states satisfying the predicate*) 

4270  282 
fun FILTER pred tac st = Seq.filter pred (tac st); 
0  283 

284 
(*Returns all changed states*) 

1643
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset

285 
fun CHANGED tac st = 
3f83b629f2e3
Fixed error in CHANGED (caused by variable renaming)
paulson
parents:
1583
diff
changeset

286 
let fun diff st' = not (eq_thm(st,st')) 
4270  287 
in Seq.filter diff (tac st) end; 
0  288 

289 

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

291 

1502  292 
(*For n subgoals, performs tac(n) THEN ... THEN tac(1) 
293 
Essential to work backwards since tac(i) may add/delete subgoals at i. *) 

294 
fun ALLGOALS tac st = 

295 
let fun doall 0 = all_tac 

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

296 
 doall n = tac(n) THEN doall(n1) 
1502  297 
in doall(nprems_of st)st end; 
0  298 

1502  299 
(*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *) 
300 
fun SOMEGOAL tac st = 

301 
let fun find 0 = no_tac 

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

302 
 find n = tac(n) ORELSE find(n1) 
1502  303 
in find(nprems_of st)st end; 
0  304 

1502  305 
(*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n). 
0  306 
More appropriate than SOMEGOAL in some cases.*) 
1502  307 
fun FIRSTGOAL tac st = 
308 
let fun find (i,n) = if i>n then no_tac else tac(i) ORELSE find (i+1,n) 

309 
in find(1, nprems_of st)st end; 

0  310 

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

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

0  314 

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

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

0  318 

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

0  321 

322 

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

2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

324 
fun SUBGOAL goalfun i st = goalfun (List.nth(prems_of st, i1), i) st 
4270  325 
handle Subscript => Seq.empty; 
0  326 

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

329 
fun CHANGED_GOAL tac i st = 

5997
4d00bbd3d3ac
tactical CHANGED now uses alphaeta conversion, not alpha conversion
paulson
parents:
5957
diff
changeset

330 
let val j = nprems_of st 
5141  331 
val t = List.nth(prems_of st, i1) 
5997
4d00bbd3d3ac
tactical CHANGED now uses alphaeta conversion, not alpha conversion
paulson
parents:
5957
diff
changeset

332 
fun diff st' = (*true if subgoal still exists and is same as old one*) 
4d00bbd3d3ac
tactical CHANGED now uses alphaeta conversion, not alpha conversion
paulson
parents:
5957
diff
changeset

333 
not (nprems_of st' >= j 
5141  334 
andalso 
5997
4d00bbd3d3ac
tactical CHANGED now uses alphaeta conversion, not alpha conversion
paulson
parents:
5957
diff
changeset

335 
Pattern.aeconv (t, 
4d00bbd3d3ac
tactical CHANGED now uses alphaeta conversion, not alpha conversion
paulson
parents:
5957
diff
changeset

336 
List.nth(prems_of st', nprems_of st'  j))) 
5141  337 
in Seq.filter diff (tac i st) end 
338 
handle Subscript => Seq.empty (*no subgoal i*); 

339 

4602  340 
fun ALLGOALS_RANGE tac (i:int) j st = 
341 
if i > j then all_tac st 

342 
else (tac j THEN ALLGOALS_RANGE tac i (j  1)) st; 

343 

344 
fun (tac1 THEN_ALL_NEW tac2) i st = 

345 
st > (tac1 i THEN (fn st' => ALLGOALS_RANGE tac2 i (i + nprems_of st'  nprems_of st) st')); 

346 

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

347 

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

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

349 

0  350 
(*Tactical for restricting the effect of a tactic to subgoal i. 
1502  351 
Works by making a new state from subgoal i, applying tac to it, and 
0  352 
composing the resulting metathm with the original state. 
353 
The "main goal" of the new state will not be atomic, some tactics may fail! 

354 
DOES NOT work if tactic affects the main goal other than by instantiation.*) 

355 

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

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

357 
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

358 

3991  359 
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

360 
(Const("==", propT>propT>propT)); 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

361 

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

362 
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

363 

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

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

365 
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

366 
Vars then it returns ct==>ct.*) 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

367 

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

368 
fun eq_trivial ct = 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

369 
let val xfree = cterm_of (sign_of ProtoPure.thy) 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

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

371 
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

372 
and refl_ct = reflexive ct 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

373 
fun restore th = 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

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

378 
(combination (combination refl_implies refl_ct) (assume ct_eq_x)) 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

379 
(Drule.mk_triv_goal ct), 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

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

381 
end (*Fails if there are Vars or TVars*) 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

382 
handle THM _ => (Drule.mk_triv_goal ct, I); 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

383 

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

384 

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

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

386 
fun select tac st i = 
2580
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

387 
let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*) 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

388 
eq_trivial (adjust_maxidx (List.nth(cprems_of st, i1))) 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

389 
fun next st' = 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

390 
let val np' = nprems_of st' 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

391 
(*rename the ?A in rev_triv_goal*) 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

392 
val {maxidx,...} = rep_thm st' 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

393 
val ct = cterm_of (sign_of ProtoPure.thy) 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

394 
(Var(("A",maxidx+1), propT)) 
5906  395 
val rev_triv_goal' = instantiate' [] [Some ct] Drule.rev_triv_goal 
5312
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

396 
fun bic th = bicompose false (false, th, np') 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

397 
in bic (Seq.hd (bic (restore st') 1 rev_triv_goal')) i st end 
4270  398 
in Seq.flat (Seq.map next (tac eq_cprem)) 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

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

400 

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

402 
let val np = nprems_of st 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

403 
in if 1<=i andalso i<=np then 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

404 
(*If only one subgoal, then just apply tactic*) 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

405 
if np=1 then tac st else select tac st i 
b380921982b9
simpler SELECT_GOAL no longer inserts a dummy parameter
paulson
parents:
5141
diff
changeset

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

407 
end; 
0  408 

409 

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

411 
H1,...,Hn are the hypotheses; x1...xm are variants of the parameters. 

412 
Main difference from strip_assums concerns parameters: 

413 
it replaces the bound variables by free variables. *) 

414 
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) = 

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

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

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

418 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  419 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
420 

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

422 

423 

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

1502  425 
METAHYPS (fn prems => tac prems) i 
0  426 

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

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

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

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

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

432 

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

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

435 
DOES NOT HANDLE TYPE UNKNOWNS. 

436 
****) 

437 

438 
local 

439 

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

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

442 
fun free_instantiate ctpairs = 

443 
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); 

444 

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

446 
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

447 
T) 
0  448 

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

450 
in 

451 

1502  452 
fun metahyps_aux_tac tacf (prem,i) state = 
0  453 
let val {sign,maxidx,...} = rep_thm state 
230  454 
val cterm = cterm_of sign 
0  455 
(*find all vars in the hyps  should find tvars also!*) 
1502  456 
val hyps_vars = foldr add_term_vars (Logic.strip_assums_hyp prem, []) 
0  457 
val insts = map mk_inst hyps_vars 
458 
(*replace the hyps_vars by Frees*) 

459 
val prem' = subst_atomic insts prem 

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

461 
val fparams = map Free params 

462 
val cparams = map cterm fparams 

463 
and chyps = map cterm hyps 

464 
val hypths = map assume chyps 

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

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

467 
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 

468 
if var mem concl_vars 

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

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

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

471 
free_of "METAHYP2_" (v, map #2 params >T)) 
0  472 
(*Instantiate subgoal vars by Free applied to params*) 
473 
fun mk_ctpair (t,in_concl,u) = 

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

474 
if in_concl then (cterm t, cterm u) 
0  475 
else (cterm t, cterm (list_comb (u,fparams))) 
476 
(*Restore Vars with higher type and index*) 

477 
fun mk_subgoal_swap_ctpair 

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

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

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

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

485 
(*Embed an ff pair in the original params*) 

1502  486 
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

487 
list_abs_free (params, u)) 
0  488 
(*Remove parameter abstractions from the ff pairs*) 
489 
fun elim_ff ff = flexpair_abs_elim_list cparams ff 

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

491 
fun relift st = 

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

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

493 
val subgoal_vars = (*Vars introduced in the subgoals*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

495 
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

496 
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

497 
val st' = instantiate ([], map mk_ctpair subgoal_insts) st 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

498 
val emBs = map (cterm o embed) (prems_of st') 
0  499 
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

500 
val Cth = implies_elim_list st' 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

501 
(map (elim_ff o assume) ffs @ 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

502 
map (elim o assume) emBs) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

506 
(*discharge assumptions from state in same order*) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

507 
(implies_intr_list (ffs@emBs) 
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

509 
end 
0  510 
val subprems = map (forall_elim_vars 0) hypths 
511 
and st0 = trivial (cterm concl) 

512 
(*function to replace the current subgoal*) 

513 
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

514 
i state 
4270  515 
in Seq.flat (Seq.map next (tacf subprems st0)) 
1502  516 
end; 
0  517 
end; 
518 

519 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

520 

521 
end; 

1502  522 

523 
open Tactical; 