summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Pure/tactical.ML

author | wenzelm |

Tue Sep 26 20:54:40 2017 +0200 (22 months ago) | |

changeset 66695 | 91500c024c7f |

parent 62916 | 621afc4607ec |

permissions | -rw-r--r-- |

tuned;

1 (* Title: Pure/tactical.ML

2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory

4 Tacticals.

5 *)

7 infix 1 THEN THEN' THEN_ALL_NEW;

8 infix 0 ORELSE APPEND ORELSE' APPEND';

9 infix 0 THEN_ELSE;

11 signature TACTICAL =

12 sig

13 type tactic = thm -> thm Seq.seq

14 val THEN: tactic * tactic -> tactic

15 val ORELSE: tactic * tactic -> tactic

16 val APPEND: tactic * tactic -> tactic

17 val THEN_ELSE: tactic * (tactic*tactic) -> tactic

18 val THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic

19 val ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic

20 val APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic

21 val all_tac: tactic

22 val no_tac: tactic

23 val DETERM: tactic -> tactic

24 val COND: (thm -> bool) -> tactic -> tactic -> tactic

25 val TRY: tactic -> tactic

26 val EVERY: tactic list -> tactic

27 val EVERY': ('a -> tactic) list -> 'a -> tactic

28 val EVERY1: (int -> tactic) list -> tactic

29 val FIRST: tactic list -> tactic

30 val FIRST': ('a -> tactic) list -> 'a -> tactic

31 val FIRST1: (int -> tactic) list -> tactic

32 val RANGE: (int -> tactic) list -> int -> tactic

33 val print_tac: Proof.context -> string -> tactic

34 val REPEAT_DETERM_N: int -> tactic -> tactic

35 val REPEAT_DETERM: tactic -> tactic

36 val REPEAT: tactic -> tactic

37 val REPEAT_DETERM1: tactic -> tactic

38 val REPEAT1: tactic -> tactic

39 val FILTER: (thm -> bool) -> tactic -> tactic

40 val CHANGED: tactic -> tactic

41 val CHANGED_PROP: tactic -> tactic

42 val ALLGOALS: (int -> tactic) -> tactic

43 val SOMEGOAL: (int -> tactic) -> tactic

44 val FIRSTGOAL: (int -> tactic) -> tactic

45 val HEADGOAL: (int -> tactic) -> tactic

46 val REPEAT_SOME: (int -> tactic) -> tactic

47 val REPEAT_DETERM_SOME: (int -> tactic) -> tactic

48 val REPEAT_FIRST: (int -> tactic) -> tactic

49 val REPEAT_DETERM_FIRST: (int -> tactic) -> tactic

50 val TRYALL: (int -> tactic) -> tactic

51 val CSUBGOAL: ((cterm * int) -> tactic) -> int -> tactic

52 val SUBGOAL: ((term * int) -> tactic) -> int -> tactic

53 val ASSERT_SUBGOAL: (int -> tactic) -> int -> tactic

54 val CHANGED_GOAL: (int -> tactic) -> int -> tactic

55 val SOLVED': (int -> tactic) -> int -> tactic

56 val THEN_ALL_NEW: (int -> tactic) * (int -> tactic) -> int -> tactic

57 val REPEAT_ALL_NEW: (int -> tactic) -> int -> tactic

58 val PRIMSEQ: (thm -> thm Seq.seq) -> tactic

59 val PRIMITIVE: (thm -> thm) -> tactic

60 val SINGLE: tactic -> thm -> thm option

61 val CONVERSION: conv -> int -> tactic

62 end;

64 structure Tactical : TACTICAL =

65 struct

67 (**** Tactics ****)

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

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

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

73 type tactic = thm -> thm Seq.seq;

76 (*** LCF-style tacticals ***)

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

79 fun (tac1 THEN tac2) st = Seq.maps tac2 (tac1 st);

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

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

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

85 fun (tac1 ORELSE tac2) st =

86 (case Seq.pull (tac1 st) of

87 NONE => tac2 st

88 | some => Seq.make (fn () => some));

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

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

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

94 fun (tac1 APPEND tac2) st =

95 Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st)));

97 (*Conditional tactic.

98 tac1 ORELSE tac2 = tac1 THEN_ELSE (all_tac, tac2)

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

100 *)

101 fun (tac THEN_ELSE (tac1, tac2)) st =

102 (case Seq.pull (tac st) of

103 NONE => tac2 st (*failed; try tactic 2*)

104 | some => Seq.maps tac1 (Seq.make (fn () => some))); (*succeeded; use tactic 1*)

107 (*Versions for combining tactic-valued functions, as in

108 SOMEGOAL (resolve_tac rls THEN' assume_tac) *)

109 fun (tac1 THEN' tac2) x = tac1 x THEN tac2 x;

110 fun (tac1 ORELSE' tac2) x = tac1 x ORELSE tac2 x;

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

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

114 fun all_tac st = Seq.single st;

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

117 fun no_tac st = Seq.empty;

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

121 fun DETERM tac = Seq.DETERM tac;

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

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

125 fun COND testfun thenf elsef =

126 (fn st => if testfun st then thenf st else elsef st);

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

129 fun TRY tac = tac ORELSE all_tac;

132 (*** List-oriented tactics ***)

134 local

135 (*This version of EVERY avoids backtracking over repeated states*)

137 fun EVY (trail, []) st =

138 Seq.make (fn () => SOME (st, Seq.make (fn () => Seq.pull (evyBack trail))))

139 | EVY (trail, tac :: tacs) st =

140 (case Seq.pull (tac st) of

141 NONE => evyBack trail (*failed: backtrack*)

142 | SOME (st', q) => EVY ((st', q, tacs) :: trail, tacs) st')

143 and evyBack [] = Seq.empty (*no alternatives*)

144 | evyBack ((st', q, tacs) :: trail) =

145 (case Seq.pull q of

146 NONE => evyBack trail

147 | SOME (st, q') =>

148 if Thm.eq_thm (st', st)

149 then evyBack ((st', q', tacs) :: trail)

150 else EVY ((st, q', tacs) :: trail, tacs) st);

151 in

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

153 fun EVERY tacs = EVY ([], tacs);

154 end;

157 (* EVERY' [tac1,...,tacn] i equals tac1 i THEN ... THEN tacn i *)

158 fun EVERY' tacs i = EVERY (map (fn f => f i) tacs);

160 (*Apply every tactic to 1*)

161 fun EVERY1 tacs = EVERY' tacs 1;

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

164 fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac;

166 (* FIRST' [tac1,...,tacn] i equals tac1 i ORELSE ... ORELSE tacn i *)

167 fun FIRST' tacs = fold_rev (curry op ORELSE') tacs (K no_tac);

169 (*Apply first tactic to 1*)

170 fun FIRST1 tacs = FIRST' tacs 1;

172 (*Apply tactics on consecutive subgoals*)

173 fun RANGE [] _ = all_tac

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

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

178 fun print_tac ctxt msg st =

179 (tracing (msg ^ "\n" ^ Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals ctxt st)));

180 Seq.single st);

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

184 uses less space than REPEAT; tail recursive.

185 If non-negative, n bounds the number of repetitions.*)

186 fun REPEAT_DETERM_N n tac =

187 let

188 fun drep 0 st = SOME (st, Seq.empty)

189 | drep n st =

190 (case Seq.pull (tac st) of

191 NONE => SOME(st, Seq.empty)

192 | SOME (st', _) => drep (n - 1) st');

193 in fn st => Seq.make (fn () => drep n st) end;

195 (*Allows any number of repetitions*)

196 val REPEAT_DETERM = REPEAT_DETERM_N ~1;

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

199 fun REPEAT tac =

200 let

201 fun rep qs st =

202 (case Seq.pull (tac st) of

203 NONE => SOME (st, Seq.make (fn () => repq qs))

204 | SOME (st', q) => rep (q :: qs) st')

205 and repq [] = NONE

206 | repq (q :: qs) =

207 (case Seq.pull q of

208 NONE => repq qs

209 | SOME (st, q) => rep (q :: qs) st);

210 in fn st => Seq.make (fn () => rep [] st) end;

212 (*Repeat 1 or more times*)

213 fun REPEAT_DETERM1 tac = DETERM tac THEN REPEAT_DETERM tac;

214 fun REPEAT1 tac = tac THEN REPEAT tac;

217 (** Filtering tacticals **)

219 fun FILTER pred tac st = Seq.filter pred (tac st);

221 (*Accept only next states that change the theorem somehow*)

222 fun CHANGED tac st =

223 let fun diff st' = not (Thm.eq_thm (st, st'));

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

226 (*Accept only next states that change the theorem's prop field

227 (changes to signature, hyps, etc. don't count)*)

228 fun CHANGED_PROP tac st =

229 let fun diff st' = not (Thm.eq_thm_prop (st, st'));

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

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

235 (*For n subgoals, performs tac(n) THEN ... THEN tac(1)

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

237 fun ALLGOALS tac st =

238 let

239 fun doall 0 = all_tac

240 | doall n = tac n THEN doall (n - 1);

241 in doall (Thm.nprems_of st) st end;

243 (*For n subgoals, performs tac(n) ORELSE ... ORELSE tac(1) *)

244 fun SOMEGOAL tac st =

245 let

246 fun find 0 = no_tac

247 | find n = tac n ORELSE find (n - 1);

248 in find (Thm.nprems_of st) st end;

250 (*For n subgoals, performs tac(1) ORELSE ... ORELSE tac(n).

251 More appropriate than SOMEGOAL in some cases.*)

252 fun FIRSTGOAL tac st =

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

254 in find (1, Thm.nprems_of st) st end;

256 (*First subgoal only.*)

257 fun HEADGOAL tac = tac 1;

259 (*Repeatedly solve some using tac. *)

260 fun REPEAT_SOME tac = REPEAT1 (SOMEGOAL (REPEAT1 o tac));

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

263 (*Repeatedly solve the first possible subgoal using tac. *)

264 fun REPEAT_FIRST tac = REPEAT1 (FIRSTGOAL (REPEAT1 o tac));

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

267 (*For n subgoals, tries to apply tac to n,...1 *)

268 fun TRYALL tac = ALLGOALS (TRY o tac);

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

272 fun CSUBGOAL goalfun i st =

273 (case SOME (Thm.cprem_of st i) handle THM _ => NONE of

274 SOME goal => goalfun (goal, i) st

275 | NONE => Seq.empty);

277 fun SUBGOAL goalfun =

278 CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i));

280 fun ASSERT_SUBGOAL (tac: int -> tactic) i st =

281 (Logic.get_goal (Thm.prop_of st) i; tac i st);

283 (*Returns all states that have changed in subgoal i, counted from the LAST

284 subgoal. For stac, for example.*)

285 fun CHANGED_GOAL tac i st =

286 SUBGOAL (fn (t, _) =>

287 let

288 val np = Thm.nprems_of st;

289 val d = np - i; (*distance from END*)

290 fun diff st' =

291 Thm.nprems_of st' - d <= 0 orelse (*the subgoal no longer exists*)

292 not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))));

293 in Seq.filter diff o tac i end) i st;

295 (*Returns all states where some subgoals have been solved. For

296 subgoal-based tactics this means subgoal i has been solved

297 altogether -- no new subgoals have emerged.*)

298 fun SOLVED' tac i st =

299 tac i st |> Seq.filter (fn st' => Thm.nprems_of st' < Thm.nprems_of st);

301 (*Apply second tactic to all subgoals emerging from the first --

302 following usual convention for subgoal-based tactics.*)

303 fun (tac1 THEN_ALL_NEW tac2) i st =

304 st |> (tac1 i THEN (fn st' =>

305 st' |> Seq.INTERVAL tac2 i (i + Thm.nprems_of st' - Thm.nprems_of st)));

307 (*Repeatedly dig into any emerging subgoals.*)

308 fun REPEAT_ALL_NEW tac =

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

311 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm seq.*)

312 fun PRIMSEQ thmfun st = thmfun st handle THM _ => Seq.empty;

314 (*Makes a tactic whose effect on a state is given by thmfun: thm->thm.*)

315 fun PRIMITIVE thmfun = PRIMSEQ (Seq.single o thmfun);

317 (*Inverse (more or less) of PRIMITIVE*)

318 fun SINGLE tacf = Option.map fst o Seq.pull o tacf

320 (*Conversions as tactics*)

321 fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st)

322 handle THM _ => Seq.empty

323 | CTERM _ => Seq.empty

324 | TERM _ => Seq.empty

325 | TYPE _ => Seq.empty;

327 end;

329 open Tactical;