author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24359  44556727197a 
child 26626  c6231d64d264 
permissions  rwrr 
16179  1 
(* Title: Pure/tctical.ML 
0  2 
ID: $Id$ 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1993 University of Cambridge 
5 

16179  6 
Tacticals. 
0  7 
*) 
8 

4602  9 
infix 1 THEN THEN' THEN_ALL_NEW; 
0  10 
infix 0 ORELSE APPEND INTLEAVE ORELSE' APPEND' INTLEAVE'; 
671  11 
infix 0 THEN_ELSE; 
12 

0  13 
signature TACTICAL = 
11916  14 
sig 
23538  15 
type tactic = thm > thm Seq.seq 
16 
val THEN: tactic * tactic > tactic 

17 
val ORELSE: tactic * tactic > tactic 

18 
val APPEND: tactic * tactic > tactic 

19 
val INTLEAVE: tactic * tactic > tactic 

20 
val THEN_ELSE: tactic * (tactic*tactic) > tactic 

21 
val THEN': ('a > tactic) * ('a > tactic) > 'a > tactic 

22 
val ORELSE': ('a > tactic) * ('a > tactic) > 'a > tactic 

23 
val APPEND': ('a > tactic) * ('a > tactic) > 'a > tactic 

24 
val INTLEAVE': ('a > tactic) * ('a > tactic) > 'a > tactic 

25 
val all_tac: tactic 

26 
val no_tac: tactic 

27 
val DETERM: tactic > tactic 

28 
val COND: (thm > bool) > tactic > tactic > tactic 

29 
val TRY: tactic > tactic 

30 
val EVERY: tactic list > tactic 

31 
val EVERY': ('a > tactic) list > 'a > tactic 

32 
val EVERY1: (int > tactic) list > tactic 

33 
val FIRST: tactic list > tactic 

34 
val FIRST': ('a > tactic) list > 'a > tactic 

35 
val FIRST1: (int > tactic) list > tactic 

36 
val RANGE: (int > tactic) list > int > tactic 

37 
val print_tac: string > tactic 

38 
val pause_tac: tactic 

39 
val trace_REPEAT: bool ref 

40 
val suppress_tracing: bool ref 

41 
val tracify: bool ref > tactic > tactic 

42 
val traced_tac: (thm > (thm * thm Seq.seq) option) > tactic 

43 
val DETERM_UNTIL: (thm > bool) > tactic > tactic 

44 
val REPEAT_DETERM_N: int > tactic > tactic 

45 
val REPEAT_DETERM: tactic > tactic 

46 
val REPEAT: tactic > tactic 

47 
val REPEAT_DETERM1: tactic > tactic 

48 
val REPEAT1: tactic > tactic 

49 
val FILTER: (thm > bool) > tactic > tactic 

50 
val CHANGED: tactic > tactic 

51 
val CHANGED_PROP: tactic > tactic 

52 
val ALLGOALS: (int > tactic) > tactic 

53 
val SOMEGOAL: (int > tactic) > tactic 

54 
val FIRSTGOAL: (int > tactic) > tactic 

55 
val REPEAT_SOME: (int > tactic) > tactic 

56 
val REPEAT_DETERM_SOME: (int > tactic) > tactic 

57 
val REPEAT_FIRST: (int > tactic) > tactic 

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

58 
val REPEAT_DETERM_FIRST: (int > tactic) > tactic 
23538  59 
val TRYALL: (int > tactic) > tactic 
60 
val CSUBGOAL: ((cterm * int) > tactic) > int > tactic 

61 
val SUBGOAL: ((term * int) > tactic) > int > tactic 

62 
val CHANGED_GOAL: (int > tactic) > int > tactic 

63 
val THEN_ALL_NEW: (int > tactic) * (int > tactic) > int > tactic 

64 
val REPEAT_ALL_NEW: (int > tactic) > int > tactic 

65 
val strip_context: term > (string * typ) list * term list * term 

66 
val metahyps_thms: int > thm > thm list option 

67 
val METAHYPS: (thm list > tactic) > int > tactic 

68 
val PRIMSEQ: (thm > thm Seq.seq) > tactic 

69 
val PRIMITIVE: (thm > thm) > tactic 

70 
val SINGLE: tactic > thm > thm option 

71 
val CONVERSION: conv > int > tactic 

11916  72 
end; 
0  73 

13108  74 
structure Tactical : TACTICAL = 
0  75 
struct 
76 

77 
(**** Tactics ****) 

78 

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

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

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

82 

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

85 

86 
(*** LCFstyle tacticals ***) 

87 

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

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

91 

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

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

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

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

100 

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

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

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

13108  104 
fun (tac1 APPEND tac2) st = 
19861  105 
Seq.append (tac1 st) (Seq.make(fn()=> Seq.pull (tac2 st))); 
0  106 

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

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

0  111 

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

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

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

671  120 

121 

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

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

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

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

0  128 

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

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

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

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

135 

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

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

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

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

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

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

145 
fun TRY tac = tac ORELSE all_tac; 

146 

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

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

148 

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

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

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

151 

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

156 
case Seq.pull(tac st) of 

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

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

160 
 evyBack ((st',q,tacs)::trail) = 
13108  161 
case Seq.pull q of 
15531  162 
NONE => evyBack trail 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
20664
diff
changeset

163 
 SOME(st,q') => if Thm.eq_thm (st',st) 
13108  164 
then evyBack ((st',q',tacs)::trail) 
165 
else EVY ((st,q',tacs)::trail, tacs) st 

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

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

167 

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

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

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

170 
end; 
2627  171 

0  172 

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

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

176 
(*Apply every tactic to 1*) 

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

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

23178  180 
fun FIRST tacs = fold_rev (curry op ORELSE) tacs no_tac; 
0  181 

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

185 
(*Apply first tactic to 1*) 

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

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

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

191 

0  192 

193 
(*** Tracing tactics ***) 

194 

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

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

12262  198 
(tracing msg; 
23224  199 
tracing ((Pretty.string_of o Pretty.chunks o 
200 
Display.pretty_goals (! Display.goals_limit)) st); 

15017
9ad392226da5
print_tac now outputs goals through tracechannel
schirmer
parents:
15006
diff
changeset

201 
Seq.single st)); 
0  202 

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

13108  204 
fun pause_tac st = 
12262  205 
(tracing "** Press RETURN to continue:"; 
24359
44556727197a
TextIO.inputLine: noncritical (assume exclusive ownership);
wenzelm
parents:
23922
diff
changeset

206 
if TextIO.inputLine TextIO.stdIn = SOME "\n" then Seq.single st 
12262  207 
else (tracing "Goodbye"; Seq.empty)); 
0  208 

209 
exception TRACE_EXIT of thm 

210 
and TRACE_QUIT; 

211 

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

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

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

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

215 

0  216 
(*Handle all tracing commands for current state and tactic *) 
13108  217 
fun exec_trace_command flag (tac, st) = 
24359
44556727197a
TextIO.inputLine: noncritical (assume exclusive ownership);
wenzelm
parents:
23922
diff
changeset

218 
case TextIO.inputLine TextIO.stdIn of 
23139
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

219 
SOME "\n" => tac st 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

220 
 SOME "f\n" => Seq.empty 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

221 
 SOME "o\n" => (flag:=false; tac st) 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

222 
 SOME "s\n" => (suppress_tracing:=true; tac st) 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

223 
 SOME "x\n" => (tracing "Exiting now"; raise (TRACE_EXIT st)) 
aa899bce7c3b
TextIO.inputLine: use present SML B library version;
wenzelm
parents:
22596
diff
changeset

224 
 SOME "quit\n" => raise TRACE_QUIT 
12262  225 
 _ => (tracing 
0  226 
"Type RETURN to continue or...\n\ 
227 
\ f  to fail here\n\ 

228 
\ o  to switch tracing off\n\ 

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

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

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

234 

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

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

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

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

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

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

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

249 

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

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

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

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

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

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

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

259 

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

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

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

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

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

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

271 

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

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

273 
val REPEAT_DETERM = REPEAT_DETERM_N ~1; 
0  274 

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

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

282 
and repq [] = NONE 

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

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

288 
(*Repeat 1 or more times*) 

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

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

292 

293 
(** Filtering tacticals **) 

294 

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

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

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

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

0  301 

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

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

303 
(changes to signature, hyps, etc. don't count)*) 
13108  304 
fun CHANGED_PROP tac st = 
22360
26ead7ed4f4b
moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
wenzelm
parents:
20664
diff
changeset

305 
let fun diff st' = not (Thm.eq_thm_prop (st, st')); 
13108  306 
in Seq.filter diff (tac st) end; 
10821  307 

0  308 

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

310 

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

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

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

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

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

0  329 

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

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

0  333 

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

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

0  337 

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

0  340 

341 

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

23224  343 
fun CSUBGOAL goalfun i st = 
344 
(case SOME (Thm.cprem_of st i) handle THM _ => NONE of 

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

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

346 
 NONE => Seq.empty); 
0  347 

23224  348 
fun SUBGOAL goalfun = 
349 
CSUBGOAL (fn (goal, i) => goalfun (Thm.term_of goal, i)); 

350 

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

13108  353 
fun CHANGED_GOAL tac i st = 
7686  354 
let val np = nprems_of st 
355 
val d = npi (*distance from END*) 

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

359 
orelse 

7686  360 
not (Pattern.aeconv (t, 
13108  361 
List.nth(prems_of st', 
362 
nprems_of st'  d  1))) 

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

365 

4602  366 
fun (tac1 THEN_ALL_NEW tac2) i st = 
8535  367 
st > (tac1 i THEN (fn st' => Seq.INTERVAL tac2 i (i + nprems_of st'  nprems_of st) st')); 
4602  368 

8341  369 
(*repeatedly dig into any emerging subgoals*) 
370 
fun REPEAT_ALL_NEW tac = 

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

372 

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

373 

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

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

379 
strip_context_aux (params, H::Hs, B) 
0  380 
 strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) = 
20194  381 
let val (b,u) = Syntax.variant_abs(a,T,t) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

382 
in strip_context_aux ((b,T)::params, Hs, u) end 
0  383 
 strip_context_aux (params, Hs, B) = (rev params, rev Hs, B); 
384 

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

386 

387 

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

1502  389 
METAHYPS (fn prems => tac prems) i 
0  390 

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

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

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

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

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

396 

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

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

399 
DOES NOT HANDLE TYPE UNKNOWNS. 

400 
****) 

401 

13108  402 
local 
0  403 

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

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

13108  406 
fun free_instantiate ctpairs = 
0  407 
forall_elim_list (map snd ctpairs) o forall_intr_list (map fst ctpairs); 
408 

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

410 
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

411 
T) 
0  412 

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

414 
in 

415 

19153  416 
(*Common code for METAHYPS and metahyps_thms*) 
417 
fun metahyps_split_prem prem = 

418 
let (*find all vars in the hyps  should find tvars also!*) 

23178  419 
val hyps_vars = List.foldr add_term_vars [] (Logic.strip_assums_hyp prem) 
0  420 
val insts = map mk_inst hyps_vars 
421 
(*replace the hyps_vars by Frees*) 

422 
val prem' = subst_atomic insts prem 

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

19153  424 
in (insts,params,hyps,concl) end; 
425 

426 
fun metahyps_aux_tac tacf (prem,gno) state = 

23224  427 
let val (insts,params,hyps,concl) = metahyps_split_prem prem 
22596  428 
val {thy = sign,maxidx,...} = rep_thm state 
19153  429 
val cterm = cterm_of sign 
430 
val chyps = map cterm hyps 

431 
val hypths = map assume chyps 

432 
val subprems = map (forall_elim_vars 0) hypths 

0  433 
val fparams = map Free params 
434 
val cparams = map cterm fparams 

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

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

13108  437 
fun mk_subgoal_inst concl_vars (var as Var(v,T)) = 
20664  438 
if member (op =) concl_vars var 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

444 
if in_concl then (cterm t, cterm u) 
0  445 
else (cterm t, cterm (list_comb (u,fparams))) 
446 
(*Restore Vars with higher type and index*) 

13108  447 
fun mk_subgoal_swap_ctpair 
448 
(t as Var((a,i),_), in_concl, u as Free(_,U)) = 

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

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

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

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

13108  456 
fun relift st = 
22596  457 
let val prop = Thm.prop_of st 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

458 
val subgoal_vars = (*Vars introduced in the subgoals*) 
23178  459 
List.foldr add_term_vars [] (Logic.strip_imp_prems prop) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

460 
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

461 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

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

463 
val emBs = map (cterm o embed) (prems_of st') 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

464 
val Cth = implies_elim_list st' (map (elim o assume) emBs) 
2244
dacee519738a
Converted I/O operatios for Basis Library compatibility
paulson
parents:
2158
diff
changeset

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

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

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

468 
(*discharge assumptions from state in same order*) 
13664
cfe1dc32c2e5
No more explicit manipulation of flexflex constraints in metahyps_aux_tac.
berghofe
parents:
13650
diff
changeset

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

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

471 
end 
0  472 
(*function to replace the current subgoal*) 
473 
fun next st = bicompose false (false, relift st, nprems_of st) 

19153  474 
gno state 
475 
in Seq.maps next (tacf subprems (trivial (cterm concl))) end; 

476 

0  477 
end; 
478 

19153  479 
(*Returns the theorem list that METAHYPS would supply to its tactic*) 
480 
fun metahyps_thms i state = 

23224  481 
let val prem = Logic.nth_prem (i, Thm.prop_of state) 
23384  482 
and cterm = cterm_of (Thm.theory_of_thm state) 
483 
val (_,_,hyps,_) = metahyps_split_prem prem 

19153  484 
in SOME (map (forall_elim_vars 0 o assume o cterm) hyps) end 
485 
handle TERM ("nth_prem", [A]) => NONE; 

486 

19455  487 
local 
19229
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset

488 

7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset

489 
fun print_vars_terms thy (n,thm) = 
19455  490 
let 
19646  491 
fun typed ty = " has type: " ^ Sign.string_of_typ thy ty; 
19455  492 
fun find_vars thy (Const (c, ty)) = 
493 
(case Term.typ_tvars ty 

494 
of [] => I 

19646  495 
 _ => insert (op =) (c ^ typed ty)) 
496 
 find_vars thy (Var (xi, ty)) = insert (op =) (Term.string_of_vname xi ^ typed ty) 

19455  497 
 find_vars _ (Free _) = I 
498 
 find_vars _ (Bound _) = I 

499 
 find_vars thy (Abs (_, _, t)) = find_vars thy t 

23224  500 
 find_vars thy (t1 $ t2) = 
19455  501 
find_vars thy t1 #> find_vars thy t1; 
502 
val prem = Logic.nth_prem (n, Thm.prop_of thm) 

503 
val tms = find_vars thy prem [] 

504 
in 

505 
(warning "Found schematic vars in assumptions:"; warning (cat_lines tms)) 

506 
end; 

507 

508 
in 

19229
7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset

509 

7183628d7b29
METAHYPS catches THM assume exception and prints out the terms containing schematic vars.
mengj
parents:
19153
diff
changeset

510 
fun METAHYPS tacf n thm = SUBGOAL (metahyps_aux_tac tacf) n thm 
23224  511 
handle THM("assume: variables",_,_) => (print_vars_terms (theory_of_thm thm) (n,thm); Seq.empty) 
0  512 

23224  513 
end; 
19455  514 

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

515 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm seq.*) 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

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

517 

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

518 
(*Makes a tactic whose effect on a state is given by thmfun: thm>thm.*) 
107e4dfd3b96
Merging the metasimplifier with the Proverssimplifier. Next step:
skalberg
parents:
13664
diff
changeset

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

520 

23538  521 
(*Inverse (more or less) of PRIMITIVE*) 
15570  522 
fun SINGLE tacf = Option.map fst o Seq.pull o tacf 
19455  523 

23538  524 
(*Conversions as tactics*) 
23584  525 
fun CONVERSION cv i st = Seq.single (Conv.gconv_rule cv i st) 
23561  526 
handle THM _ => Seq.empty 
527 
 CTERM _ => Seq.empty 

528 
 TERM _ => Seq.empty 

529 
 TYPE _ => Seq.empty; 

23538  530 

0  531 
end; 
1502  532 

533 
open Tactical; 