author  paulson 
Tue, 14 Jul 1998 13:31:55 +0200  
changeset 5141  495a4f9af897 
parent 4602  0e034d76932e 
child 5312  b380921982b9 
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 = 
0  201 
(prs"** Press RETURN to continue: "; 
4270  202 
if TextIO.inputLine TextIO.stdIn = "\n" then Seq.single st 
203 
else (prs"Goodbye\n"; 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) 

219 
 "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT st)) 

0  220 
 "quit\n" => raise TRACE_QUIT 
221 
 _ => (prs 

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; 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

235 
prs"** Press RETURN to continue: "; 
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 = 

330 
let val j = nprems_of st  i 

331 
val t = List.nth(prems_of st, i1) 

332 
fun diff st' = 

333 
not (nprems_of st' > j (*subgoal is still there*) 

334 
andalso 

335 
t aconv List.nth(prems_of st', nprems_of st'  j  1)) 

336 
in Seq.filter diff (tac i st) end 

337 
handle Subscript => Seq.empty (*no subgoal i*); 

338 

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

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

342 

343 
fun (tac1 THEN_ALL_NEW tac2) i st = 

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

345 

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

346 

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

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

348 

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

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

354 

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

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

356 
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

357 

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

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

360 

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

361 
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

362 

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

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

364 
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

365 
Vars then it returns ct==>ct.*) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

366 
fun eq_trivial ct = 
3991  367 
let val xfree = cterm_of (sign_of ProtoPure.thy) (Free (gensym"EQ_TRIVIAL_", propT)) 
2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

368 
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

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

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

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

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

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

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

375 
(combination (combination refl_implies refl_ct) (assume ct_eq_x)) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

376 
(trivial ct), 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

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

378 
end (*Fails if there are Vars or TVars*) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

379 
handle THM _ => (trivial ct, I); 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

380 

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

381 
(*Does the work of SELECT_GOAL. *) 
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

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

383 
let val (eq_cprem, restore) = (*we hope maxidx goes to ~1*) 
e3f680709487
Gradual switching to Basis Library functions nth, drop, etc.
paulson
parents:
2244
diff
changeset

384 
eq_trivial (adjust_maxidx (List.nth(cprems_of st0, i1))) 
2005
a52f53caf424
Optimized version of SELECT_GOAL, up to 10% faster
paulson
parents:
1643
diff
changeset

385 
fun next st = bicompose false (false, restore st, nprems_of st) i st0 
4270  386 
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

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

388 

2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

389 
(* (!!selct. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) 
0  390 
val dummy_quant_rl = 
3991  391 
read_cterm (sign_of ProtoPure.thy) ("!!selct::prop. PROP V",propT) > 
2158
77dfe65b5bb3
Renamed SELECT_GOAL's new parameter from x to selct to avoid clashes
paulson
parents:
2005
diff
changeset

392 
assume > forall_elim_var 0 > standard; 
0  393 

394 
(* Prevent the subgoal's assumptions from becoming additional subgoals in the 

395 
new proof state by enclosing them by a universal quantification *) 

1502  396 
fun protect_subgoal st i = 
4270  397 
Seq.hd (bicompose false (false,dummy_quant_rl,1) i st) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

398 
handle _ => error"SELECT_GOAL  impossible error???"; 
0  399 

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

401 
case (i, List.drop(prems_of st, i1)) of 
4270  402 
(_,[]) => Seq.empty 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

403 
 (1,[_]) => tac st (*If i=1 and only one subgoal do nothing!*) 
1502  404 
 (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal st i) i 
405 
 (_, _::_) => select tac st i; 

0  406 

407 

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

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

410 
Main difference from strip_assums concerns parameters: 

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

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

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

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

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

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

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

420 

421 

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

1502  423 
METAHYPS (fn prems => tac prems) i 
0  424 

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

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

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

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

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

430 

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

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

433 
DOES NOT HANDLE TYPE UNKNOWNS. 

434 
****) 

435 

436 
local 

437 

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

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

440 
fun free_instantiate ctpairs = 

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

442 

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

444 
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

445 
T) 
0  446 

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

448 
in 

449 

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

457 
val prem' = subst_atomic insts prem 

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

459 
val fparams = map Free params 

460 
val cparams = map cterm fparams 

461 
and chyps = map cterm hyps 

462 
val hypths = map assume chyps 

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

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

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

466 
if var mem concl_vars 

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

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

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

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

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

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

475 
fun mk_subgoal_swap_ctpair 

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

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

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

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

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

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

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

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

489 
fun relift st = 

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

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

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

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

493 
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

494 
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

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

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

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

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

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

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

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

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

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

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

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

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

510 
(*function to replace the current subgoal*) 

511 
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

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

517 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

518 

519 
end; 

1502  520 

521 
open Tactical; 