author  lcp 
Mon, 14 Nov 1994 10:49:39 +0100  
changeset 709  0d0df9b5afe3 
parent 703  3a5cd2883581 
child 729  cc4c4eafe628 
permissions  rwrr 
0  1 
(* Title: tctical 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright 1993 University of Cambridge 

5 

6 
Tacticals 

7 
*) 

8 

9 
infix 1 THEN THEN' THEN_BEST_FIRST; 

10 
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; 

11 

671  12 
infix 0 THEN_ELSE; 
13 

0  14 

15 
signature TACTICAL = 

16 
sig 

17 
structure Thm : THM 

18 
local open Thm in 

19 
datatype tactic = Tactic of thm > thm Sequence.seq 

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

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

21 
val ALLGOALS : (int > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

22 
val APPEND : tactic * tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

23 
val APPEND' : ('a > tactic) * ('a > tactic) > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

24 
val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

25 
val BREADTH_FIRST : (thm > bool) > tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

26 
val CHANGED : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

27 
val COND : (thm > bool) > tactic > tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

28 
val DEPTH_FIRST : (thm > bool) > tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

29 
val DEPTH_SOLVE : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

30 
val DEPTH_SOLVE_1 : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

31 
val DETERM : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

32 
val EVERY : tactic list > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

33 
val EVERY' : ('a > tactic) list > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

34 
val EVERY1 : (int > tactic) list > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

35 
val FILTER : (thm > bool) > tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

36 
val FIRST : tactic list > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

37 
val FIRST' : ('a > tactic) list > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

38 
val FIRST1 : (int > tactic) list > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

39 
val FIRSTGOAL : (int > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

40 
val goals_limit : int ref 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

41 
val has_fewer_prems : int > thm > bool 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

42 
val IF_UNSOLVED : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

43 
val INTLEAVE : tactic * tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

44 
val INTLEAVE' : ('a > tactic) * ('a > tactic) > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

45 
val METAHYPS : (thm list > tactic) > int > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

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

47 
val ORELSE : tactic * tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

48 
val ORELSE' : ('a > tactic) * ('a > tactic) > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

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

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

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

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

53 
val REPEAT_DETERM_N : int > tactic > tactic 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

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

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

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

57 
val REPEAT_DETERM_SOME: (int > tactic) > tactic 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

58 
val REPEAT_FIRST : (int > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

59 
val REPEAT_SOME : (int > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

60 
val SELECT_GOAL : tactic > int > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

61 
val SOMEGOAL : (int > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

62 
val STATE : (thm > tactic) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

63 
val strip_context : term > (string * typ) list * term list * term 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

64 
val SUBGOAL : ((term*int) > tactic) > int > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

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

66 
val tapply : tactic * thm > thm Sequence.seq 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

67 
val THEN : tactic * tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

68 
val THEN' : ('a > tactic) * ('a > tactic) > 'a > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

69 
val THEN_BEST_FIRST : tactic * ((thm>bool) * (thm>int) * tactic) 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

70 
> tactic 
671  71 
val THEN_ELSE : tactic * (tactic*tactic) > tactic 
631
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

72 
val traced_tac : (thm > (thm * thm Sequence.seq) option) > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

73 
val tracify : bool ref > tactic > thm > thm Sequence.seq 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

74 
val trace_BEST_FIRST : bool ref 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

75 
val trace_DEPTH_FIRST : bool ref 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

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

77 
val TRY : tactic > tactic 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

78 
val TRYALL : (int > tactic) > tactic 
0  79 
end 
80 
end; 

81 

82 

83 
functor TacticalFun (structure Logic: LOGIC and Drule: DRULE) : TACTICAL = 

84 
struct 

85 
structure Thm = Drule.Thm; 

86 
structure Sequence = Thm.Sequence; 

87 
structure Sign = Thm.Sign; 

88 
local open Drule Thm 

89 
in 

90 

91 
(**** Tactics ****) 

92 

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

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

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

96 

97 
datatype tactic = Tactic of thm > thm Sequence.seq; 

98 

99 
fun tapply(Tactic tf, state) = tf (state); 

100 

101 
(*Makes a tactic from one that uses the components of the state.*) 

102 
fun STATE tacfun = Tactic (fn state => tapply(tacfun state, state)); 

103 

104 

105 
(*** LCFstyle tacticals ***) 

106 

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

108 
fun (Tactic tf1) THEN (Tactic tf2) = 

109 
Tactic (fn state => Sequence.flats (Sequence.maps tf2 (tf1 state))); 

110 

111 

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

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

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

115 
fun (Tactic tf1) ORELSE (Tactic tf2) = 

116 
Tactic (fn state => 

117 
case Sequence.pull(tf1 state) of 

118 
None => tf2 state 

119 
 sequencecell => Sequence.seqof(fn()=> sequencecell)); 

120 

121 

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

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

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

125 
fun (Tactic tf1) APPEND (Tactic tf2) = 

126 
Tactic (fn state => Sequence.append(tf1 state, 

127 
Sequence.seqof(fn()=> Sequence.pull (tf2 state)))); 

128 

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

130 
fun (Tactic tf1) INTLEAVE (Tactic tf2) = 

131 
Tactic (fn state => Sequence.interleave(tf1 state, 

132 
Sequence.seqof(fn()=> Sequence.pull (tf2 state)))); 

133 

671  134 
(*Conditional tactic. 
135 
tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2) 

136 
tac1 THEN tac2 = tac1 THEN_ELSE (tac2, no_tac) 

137 
*) 

138 
fun (Tactic tf) THEN_ELSE (Tactic tf1, Tactic tf2) = 

139 
Tactic (fn state => 

140 
case Sequence.pull(tf state) of 

141 
None => tf2 state (*failed; try tactic 2*) 

142 
 seqcell => Sequence.flats (*succeeded; use tactic 1*) 

143 
(Sequence.maps tf1 (Sequence.seqof(fn()=> seqcell)))); 

144 

145 

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

148 
fun tac1 THEN' tac2 = fn x => tac1 x THEN tac2 x; 

149 
fun tac1 ORELSE' tac2 = fn x => tac1 x ORELSE tac2 x; 

150 
fun tac1 APPEND' tac2 = fn x => tac1 x APPEND tac2 x; 

151 
fun tac1 INTLEAVE' tac2 = fn x => tac1 x INTLEAVE tac2 x; 

152 

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

154 
val all_tac = Tactic (fn state => Sequence.single state); 

155 

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

157 
val no_tac = Tactic (fn state => Sequence.null); 

158 

159 

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

161 
fun DETERM (Tactic tf) = Tactic (fn state => 

162 
case Sequence.pull (tf state) of 

163 
None => Sequence.null 

164 
 Some(x,_) => Sequence.cons(x, Sequence.null)); 

165 

166 

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

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

169 
fun COND testfun (Tactic thenf) (Tactic elsef) = Tactic (fn prf => 

170 
if testfun prf then thenf prf else elsef prf); 

171 

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

173 
fun TRY tac = tac ORELSE all_tac; 

174 

175 

176 
(*** Listoriented tactics ***) 

177 

178 
(* EVERY [tac1,...,tacn] equals tac1 THEN ... THEN tacn *) 

179 
fun EVERY tacs = foldr (op THEN) (tacs, all_tac); 

180 

181 
(* EVERY' [tf1,...,tfn] i equals tf1 i THEN ... THEN tfn i *) 

182 
fun EVERY' tfs = foldr (op THEN') (tfs, K all_tac); 

183 

184 
(*Apply every tactic to 1*) 

185 
fun EVERY1 tfs = EVERY' tfs 1; 

186 

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

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

189 

190 
(* FIRST' [tf1,...,tfn] i equals tf1 i ORELSE ... ORELSE tfn i *) 

191 
fun FIRST' tfs = foldr (op ORELSE') (tfs, K no_tac); 

192 

193 
(*Apply first tactic to 1*) 

194 
fun FIRST1 tfs = FIRST' tfs 1; 

195 

196 

197 
(*** Tracing tactics ***) 

198 

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

200 
val goals_limit = ref 10; 

201 

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

67  203 
val print_tac = Tactic 
204 
(fn state => 

205 
(!print_goals_ref (!goals_limit) state; Sequence.single state)); 

0  206 

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

208 
val pause_tac = Tactic (fn state => 

209 
(prs"** Press RETURN to continue: "; 

210 
if input(std_in,1) = "\n" then Sequence.single state 

211 
else (prs"Goodbye\n"; Sequence.null))); 

212 

213 
exception TRACE_EXIT of thm 

214 
and TRACE_QUIT; 

215 

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

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

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

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

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

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

221 

0  222 
(*Handle all tracing commands for current state and tactic *) 
223 
fun exec_trace_command flag (tf, state) = 

224 
case input_line(std_in) of 

225 
"\n" => tf state 

226 
 "f\n" => Sequence.null 

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

227 
 "o\n" => (flag:=false; tf state) 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

228 
 "s\n" => (suppress_tracing:=true; tf state) 
0  229 
 "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT state)) 
230 
 "quit\n" => raise TRACE_QUIT 

231 
 _ => (prs 

232 
"Type RETURN to continue or...\n\ 

233 
\ f  to fail here\n\ 

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

235 
\ s  to suppress tracing until next entry to a tactical\n\ 
0  236 
\ x  to exit at this point\n\ 
237 
\ quit  to abort this tracing run\n\ 

238 
\** Well? " ; exec_trace_command flag (tf, state)); 

239 

240 

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

242 
fun tracify flag (Tactic tf) state = 

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

243 
if !flag andalso not (!suppress_tracing) 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

244 
then (!print_goals_ref (!goals_limit) state; 
0  245 
prs"** Press RETURN to continue: "; 
246 
exec_trace_command flag (tf,state)) 

247 
else tf state; 

248 

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

250 
fun traced_tac seqf = Tactic (fn st => 

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

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

252 
Sequence.seqof (fn()=> seqf st 
8bc44f7bbab8
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
lcp
parents:
230
diff
changeset

253 
handle TRACE_EXIT st' => Some(st', Sequence.null)))); 
0  254 

255 

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

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

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

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

259 
fun REPEAT_DETERM_N n tac = 
0  260 
let val tf = tracify trace_REPEAT tac 
703
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

261 
fun drep 0 st = Some(st, Sequence.null) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

262 
 drep n st = 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

263 
(case Sequence.pull(tf st) of 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

264 
None => Some(st, Sequence.null) 
3a5cd2883581
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
lcp
parents:
671
diff
changeset

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

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

267 

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

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

269 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  270 

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

272 
fun REPEAT tac = 

273 
let val tf = tracify trace_REPEAT tac 

274 
fun rep qs st = 

275 
case Sequence.pull(tf st) of 

276 
None => Some(st, Sequence.seqof(fn()=> repq qs)) 

277 
 Some(st',q) => rep (q::qs) st' 

278 
and repq [] = None 

279 
 repq(q::qs) = case Sequence.pull q of 

280 
None => repq qs 

281 
 Some(st,q) => rep (q::qs) st 

282 
in traced_tac (rep []) end; 

283 

284 
(*Repeat 1 or more times*) 

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

285 
fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac; 
0  286 
fun REPEAT1 tac = tac THEN REPEAT tac; 
287 

288 

289 
(** Search tacticals **) 

290 

291 
(*Seaarches "satp" reports proof tree as satisfied*) 

292 
fun DEPTH_FIRST satp tac = 

293 
let val tf = tracify trace_DEPTH_FIRST tac 

294 
fun depth [] = None 

295 
 depth(q::qs) = 

296 
case Sequence.pull q of 

297 
None => depth qs 

298 
 Some(st,stq) => 

299 
if satp st then Some(st, Sequence.seqof(fn()=> depth(stq::qs))) 

300 
else depth (tf st :: stq :: qs) 

301 
in traced_tac (fn st => depth([Sequence.single st])) end; 

302 

303 

304 
(*Predicate: Does the rule have fewer than n premises?*) 

305 
fun has_fewer_prems n rule = (nprems_of rule < n); 

306 

307 
(*Apply a tactic if subgoals remain, else do nothing.*) 

308 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

309 

310 
(*Tactical to reduce the number of premises by 1. 

311 
If no subgoals then it must fail! *) 

312 
fun DEPTH_SOLVE_1 tac = STATE 

313 
(fn state => 

314 
(case nprems_of state of 

315 
0 => no_tac 

316 
 n => DEPTH_FIRST (has_fewer_prems n) tac)); 

317 

318 
(*Uses depthfirst search to solve ALL subgoals*) 

319 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

320 

321 
(*** Bestfirst search ***) 

322 

323 
(*Insertion into priority queue of states *) 

324 
fun insert (nth: int*thm, []) = [nth] 

325 
 insert ((m,th), (n,th')::nths) = 

326 
if n<m then (n,th') :: insert ((m,th), nths) 

327 
else if n=m andalso eq_thm(th,th') 

328 
then (n,th')::nths 

329 
else (m,th)::(n,th')::nths; 

330 

331 
(*For creating output sequence*) 

332 
fun some_of_list [] = None 

333 
 some_of_list (x::l) = Some (x, Sequence.seqof (fn () => some_of_list l)); 

334 

335 

336 
(* Bestfirst search for a state that satisfies satp (incl initial state) 

337 
Function sizef estimates size of problem remaining (smaller means better). 

338 
tactic tf0 sets up the initial priority queue, which is searched by tac. *) 

339 
fun (Tactic tf0) THEN_BEST_FIRST (satp, sizef, tac) = 

340 
let val tf = tracify trace_BEST_FIRST tac 

341 
fun pairsize th = (sizef th, th); 

342 
fun bfs (news,nprfs) = 

343 
(case partition satp news of 

344 
([],nonsats) => next(foldr insert 

345 
(map pairsize nonsats, nprfs)) 

346 
 (sats,_) => some_of_list sats) 

347 
and next [] = None 

348 
 next ((n,prf)::nprfs) = 

349 
(if !trace_BEST_FIRST 

350 
then writeln("state size = " ^ string_of_int n ^ 

351 
" queue length =" ^ string_of_int (length nprfs)) 

352 
else (); 

353 
bfs (Sequence.list_of_s (tf prf), nprfs)) 

354 
fun tf st = bfs (Sequence.list_of_s (tf0 st), []) 

355 
in traced_tac tf end; 

356 

357 
(*Ordinary bestfirst search, with no initial tactic*) 

358 
fun BEST_FIRST (satp,sizef) tac = all_tac THEN_BEST_FIRST (satp,sizef,tac); 

359 

360 
(*Breadthfirst search to satisfy satpred (including initial state) 

361 
SLOW  SHOULD NOT USE APPEND!*) 

362 
fun BREADTH_FIRST satpred (Tactic tf) = 

363 
let val tacf = Sequence.list_of_s o tf; 

364 
fun bfs prfs = 

365 
(case partition satpred prfs of 

366 
([],[]) => [] 

367 
 ([],nonsats) => 

368 
(prs("breadth=" ^ string_of_int(length nonsats) ^ "\n"); 

369 
bfs (flat (map tacf nonsats))) 

370 
 (sats,_) => sats) 

371 
in Tactic (fn state => Sequence.s_of_list (bfs [state])) end; 

372 

373 

374 
(** Filtering tacticals **) 

375 

376 
(*Returns all states satisfying the predicate*) 

377 
fun FILTER pred (Tactic tf) = Tactic 

378 
(fn state => Sequence.filters pred (tf state)); 

379 

380 
(*Returns all changed states*) 

381 
fun CHANGED (Tactic tf) = 

382 
Tactic (fn state => 

383 
let fun diff st = not (eq_thm(state,st)) 

384 
in Sequence.filters diff (tf state) 

385 
end ); 

386 

387 

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

389 

390 
(*For n subgoals, performs tf(n) THEN ... THEN tf(1) 

391 
Essential to work backwards since tf(i) may add/delete subgoals at i. *) 

392 
fun ALLGOALS tf = 

393 
let fun tac 0 = all_tac 

394 
 tac n = tf(n) THEN tac(n1) 

395 
in Tactic(fn state => tapply(tac(nprems_of state), state)) end; 

396 

397 
(*For n subgoals, performs tf(n) ORELSE ... ORELSE tf(1) *) 

398 
fun SOMEGOAL tf = 

399 
let fun tac 0 = no_tac 

400 
 tac n = tf(n) ORELSE tac(n1) 

401 
in Tactic(fn state => tapply(tac(nprems_of state), state)) end; 

402 

403 
(*For n subgoals, performs tf(1) ORELSE ... ORELSE tf(n). 

404 
More appropriate than SOMEGOAL in some cases.*) 

405 
fun FIRSTGOAL tf = 

406 
let fun tac (i,n) = if i>n then no_tac else tf(i) ORELSE tac (i+1,n) 

407 
in Tactic(fn state => tapply(tac(1, nprems_of state), state)) end; 

408 

409 
(*Repeatedly solve some using tf. *) 

410 
fun REPEAT_SOME tf = REPEAT1 (SOMEGOAL (REPEAT1 o tf)); 

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

411 
fun REPEAT_DETERM_SOME tf = REPEAT_DETERM1 (SOMEGOAL (REPEAT_DETERM1 o tf)); 
0  412 

413 
(*Repeatedly solve the first possible subgoal using tf. *) 

414 
fun REPEAT_FIRST tf = REPEAT1 (FIRSTGOAL (REPEAT1 o tf)); 

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

415 
fun REPEAT_DETERM_FIRST tf = REPEAT_DETERM1 (FIRSTGOAL (REPEAT_DETERM1 o tf)); 
0  416 

417 
(*For n subgoals, tries to apply tf to n,...1 *) 

418 
fun TRYALL tf = ALLGOALS (TRY o tf); 

419 

420 

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

422 
fun SUBGOAL goalfun i = Tactic(fn state => 

423 
case drop(i1, prems_of state) of 

424 
[] => Sequence.null 

425 
 prem::_ => tapply(goalfun (prem,i), state)); 

426 

427 
(*Tactical for restricting the effect of a tactic to subgoal i. 

428 
Works by making a new state from subgoal i, applying tf to it, and 

429 
composing the resulting metathm with the original state. 

430 
The "main goal" of the new state will not be atomic, some tactics may fail! 

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

432 

31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset

433 
(* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) 
0  434 
val dummy_quant_rl = 
435 
standard (forall_elim_var 0 (assume 

230  436 
(read_cterm Sign.pure ("!!x::prop. PROP V",propT)))); 
0  437 

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

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

440 
fun protect_subgoal state i = 

31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset

441 
case Sequence.chop (1, bicompose false (false,dummy_quant_rl,1) i state) of 
0  442 
([state'],_) => state' 
31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset

443 
 _ => error"SELECT_GOAL  impossible error???"; 
0  444 

445 
(*Does the work of SELECT_GOAL. *) 

446 
fun select (Tactic tf) state i = 

709
0d0df9b5afe3
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
lcp
parents:
703
diff
changeset

447 
let val cprem::_ = drop(i1, cprems_of state) 
0  448 
fun next st = bicompose false (false, st, nprems_of st) i state 
709
0d0df9b5afe3
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
lcp
parents:
703
diff
changeset

449 
in Sequence.flats (Sequence.maps next (tf (trivial cprem))) 
0  450 
end; 
451 

452 
fun SELECT_GOAL tac i = Tactic (fn state => 

453 
case (i, drop(i1, prems_of state)) of 

454 
(_,[]) => Sequence.null 

31
eb01df4ffe66
tctical/dummy_quant_rl: specifies type prop to avoid the type variable
lcp
parents:
0
diff
changeset

455 
 (1,[_]) => tapply(tac,state) (*If i=1 and only one subgoal do nothing!*) 
0  456 
 (_, (Const("==>",_)$_$_) :: _) => select tac (protect_subgoal state i) i 
457 
 (_, _::_) => select tac state i); 

458 

459 

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

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

462 
Main difference from strip_assums concerns parameters: 

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

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

465 
strip_context_aux (params, H::Hs, B) 

466 
 strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = 

467 
let val (b,u) = variant_abs(a,T,t) 

468 
in strip_context_aux ((b,T)::params, Hs, u) end 

469 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 

470 

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

472 

473 

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

475 
METAHYPS (fn prems => tac (prems)) i 

476 

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

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

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

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

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

482 

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

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

485 
DOES NOT HANDLE TYPE UNKNOWNS. 

486 
****) 

487 

488 
local 

489 
open Logic 

490 

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

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

493 
fun free_instantiate ctpairs = 

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

495 

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

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

498 
T) 

499 

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

501 
in 

502 

503 
fun metahyps_aux_tac tacf (prem,i) = Tactic (fn state => 

504 
let val {sign,maxidx,...} = rep_thm state 

230  505 
val cterm = cterm_of sign 
0  506 
(*find all vars in the hyps  should find tvars also!*) 
507 
val hyps_vars = foldr add_term_vars (strip_assums_hyp prem, []) 

508 
val insts = map mk_inst hyps_vars 

509 
(*replace the hyps_vars by Frees*) 

510 
val prem' = subst_atomic insts prem 

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

512 
val fparams = map Free params 

513 
val cparams = map cterm fparams 

514 
and chyps = map cterm hyps 

515 
val hypths = map assume chyps 

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

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

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

519 
if var mem concl_vars 

520 
then (var, true, free_of "METAHYP2_" (v,T)) 

521 
else (var, false, 

522 
free_of "METAHYP2_" (v, map #2 params >T)) 

523 
(*Instantiate subgoal vars by Free applied to params*) 

524 
fun mk_ctpair (t,in_concl,u) = 

525 
if in_concl then (cterm t, cterm u) 

526 
else (cterm t, cterm (list_comb (u,fparams))) 

527 
(*Restore Vars with higher type and index*) 

528 
fun mk_subgoal_swap_ctpair 

529 
(t as Var((a,i),_), in_concl, u as Free(_,U)) = 

530 
if in_concl then (cterm u, cterm t) 

531 
else (cterm u, cterm(Var((a, i+maxidx), U))) 

532 
(*Embed B in the original context of params and hyps*) 

533 
fun embed B = list_all_free (params, list_implies (hyps, B)) 

534 
(*Strip the context using elimination rules*) 

535 
fun elim Bhyp = implies_elim_list (forall_elim_list cparams Bhyp) hypths 

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

537 
fun embed_ff(t,u) = 

538 
mk_flexpair (list_abs_free (params, t), list_abs_free (params, u)) 

539 
(*Remove parameter abstractions from the ff pairs*) 

540 
fun elim_ff ff = flexpair_abs_elim_list cparams ff 

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

542 
fun relift st = 

543 
let val prop = #prop(rep_thm st) 

544 
val subgoal_vars = (*Vars introduced in the subgoals*) 

545 
foldr add_term_vars (strip_imp_prems prop, []) 

546 
and concl_vars = add_term_vars (strip_imp_concl prop, []) 

547 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 

548 
val st' = instantiate ([], map mk_ctpair subgoal_insts) st 

549 
val emBs = map (cterm o embed) (prems_of st') 

550 
and ffs = map (cterm o embed_ff) (tpairs_of st') 

551 
val Cth = implies_elim_list st' 

552 
(map (elim_ff o assume) ffs @ 

553 
map (elim o assume) emBs) 

554 
in (*restore the unknowns to the hypotheses*) 

555 
free_instantiate (map swap_ctpair insts @ 

556 
map mk_subgoal_swap_ctpair subgoal_insts) 

557 
(*discharge assumptions from state in same order*) 

558 
(implies_intr_list (ffs@emBs) 

559 
(forall_intr_list cparams (implies_intr_list chyps Cth))) 

560 
end 

561 
val subprems = map (forall_elim_vars 0) hypths 

562 
and st0 = trivial (cterm concl) 

563 
(*function to replace the current subgoal*) 

564 
fun next st = bicompose false (false, relift st, nprems_of st) 

565 
i state 

566 
in Sequence.flats (Sequence.maps next (tapply(tacf subprems, st0))) 

567 
end); 

568 
end; 

569 

570 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

571 

572 
end; 

573 
end; 