author  lcp 
Tue, 21 Jun 1994 17:20:34 +0200  
changeset 435  ca5356bd315a 
parent 230  ec8a2b6aa8a7 
child 631  8bc44f7bbab8 
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 

12 

13 
signature TACTICAL = 

14 
sig 

15 
structure Thm : THM 

16 
local open Thm in 

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

18 
val all_tac: tactic 

19 
val ALLGOALS: (int > tactic) > tactic 

20 
val APPEND: tactic * tactic > tactic 

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

22 
val BEST_FIRST: (thm > bool) * (thm > int) > tactic > tactic 

23 
val BREADTH_FIRST: (thm > bool) > tactic > tactic 

24 
val CHANGED: tactic > tactic 

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

26 
val DEPTH_FIRST: (thm > bool) > tactic > tactic 

27 
val DEPTH_SOLVE: tactic > tactic 

28 
val DEPTH_SOLVE_1: tactic > tactic 

29 
val DETERM: 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 FILTER: (thm > bool) > tactic > tactic 

34 
val FIRST: tactic list > tactic 

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

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

37 
val FIRSTGOAL: (int > tactic) > tactic 

38 
val goals_limit: int ref 

39 
val has_fewer_prems: int > thm > bool 

40 
val IF_UNSOLVED: tactic > tactic 

41 
val INTLEAVE: tactic * tactic > tactic 

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

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

44 
val no_tac: tactic 

45 
val ORELSE: tactic * tactic > tactic 

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

47 
val pause_tac: tactic 

48 
val print_tac: tactic 

49 
val REPEAT1: tactic > tactic 

50 
val REPEAT: tactic > tactic 

51 
val REPEAT_DETERM: tactic > tactic 

52 
val REPEAT_FIRST: (int > tactic) > tactic 

53 
val REPEAT_SOME: (int > tactic) > tactic 

54 
val SELECT_GOAL: tactic > int > tactic 

55 
val SOMEGOAL: (int > tactic) > tactic 

56 
val STATE: (thm > tactic) > tactic 

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

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

59 
val tapply: tactic * thm > thm Sequence.seq 

60 
val THEN: tactic * tactic > tactic 

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

62 
val THEN_BEST_FIRST: tactic * ((thm>bool) * (thm>int) * tactic) > tactic 

63 
val traced_tac: (thm > (thm * thm Sequence.seq) option) > tactic 

64 
val tracify: bool ref > tactic > thm > thm Sequence.seq 

65 
val trace_BEST_FIRST: bool ref 

66 
val trace_DEPTH_FIRST: bool ref 

67 
val trace_REPEAT: bool ref 

68 
val TRY: tactic > tactic 

69 
val TRYALL: (int > tactic) > tactic 

70 
end 

71 
end; 

72 

73 

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

75 
struct 

76 
structure Thm = Drule.Thm; 

77 
structure Sequence = Thm.Sequence; 

78 
structure Sign = Thm.Sign; 

79 
local open Drule Thm 

80 
in 

81 

82 
(**** Tactics ****) 

83 

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

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

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

87 

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

89 

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

91 

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

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

94 

95 

96 
(*** LCFstyle tacticals ***) 

97 

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

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

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

101 

102 

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

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

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

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

107 
Tactic (fn state => 

108 
case Sequence.pull(tf1 state) of 

109 
None => tf2 state 

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

111 

112 

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

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

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

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

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

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

119 

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

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

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

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

124 

125 
(*Versions for combining tacticvalued functions, as in 

126 
SOMEGOAL (resolve_tac rls THEN' assume_tac) *) 

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

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

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

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

131 

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

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

134 

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

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

137 

138 

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

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

141 
case Sequence.pull (tf state) of 

142 
None => Sequence.null 

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

144 

145 

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

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

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

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

150 

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

152 
fun TRY tac = tac ORELSE all_tac; 

153 

154 

155 
(*** Listoriented tactics ***) 

156 

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

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

159 

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

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

162 

163 
(*Apply every tactic to 1*) 

164 
fun EVERY1 tfs = EVERY' tfs 1; 

165 

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

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

168 

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

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

171 

172 
(*Apply first tactic to 1*) 

173 
fun FIRST1 tfs = FIRST' tfs 1; 

174 

175 

176 
(*** Tracing tactics ***) 

177 

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

179 
val goals_limit = ref 10; 

180 

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

67  182 
val print_tac = Tactic 
183 
(fn state => 

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

0  185 

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

187 
val pause_tac = Tactic (fn state => 

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

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

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

191 

192 
exception TRACE_EXIT of thm 

193 
and TRACE_QUIT; 

194 

195 
(*Handle all tracing commands for current state and tactic *) 

196 
fun exec_trace_command flag (tf, state) = 

197 
case input_line(std_in) of 

198 
"\n" => tf state 

199 
 "f\n" => Sequence.null 

200 
 "o\n" => (flag:=false; tf state) 

201 
 "x\n" => (prs"Exiting now\n"; raise (TRACE_EXIT state)) 

202 
 "quit\n" => raise TRACE_QUIT 

203 
 _ => (prs 

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

205 
\ f  to fail here\n\ 

206 
\ o  to switch tracing off\n\ 

207 
\ x  to exit at this point\n\ 

208 
\ quit  to abort this tracing run\n\ 

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

210 

211 

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

213 
fun tracify flag (Tactic tf) state = 

67  214 
if !flag then (!print_goals_ref (!goals_limit) state; 
0  215 
prs"** Press RETURN to continue: "; 
216 
exec_trace_command flag (tf,state)) 

217 
else tf state; 

218 

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

220 
fun traced_tac seqf = Tactic (fn st => 

221 
Sequence.seqof (fn()=> seqf st 

222 
handle TRACE_EXIT st' => Some(st', Sequence.null))); 

223 

224 

225 
(*Tracing flags*) 

226 
val trace_REPEAT= ref false 

227 
and trace_DEPTH_FIRST = ref false 

228 
and trace_BEST_FIRST = ref false; 

229 

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

231 
uses less space than REPEAT; tail recursive*) 

232 
fun REPEAT_DETERM tac = 

233 
let val tf = tracify trace_REPEAT tac 

234 
fun drep st = 

235 
case Sequence.pull(tf st) of 

236 
None => Some(st, Sequence.null) 

237 
 Some(st',_) => drep st' 

238 
in traced_tac drep end; 

239 

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

241 
fun REPEAT tac = 

242 
let val tf = tracify trace_REPEAT tac 

243 
fun rep qs st = 

244 
case Sequence.pull(tf st) of 

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

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

247 
and repq [] = None 

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

249 
None => repq qs 

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

251 
in traced_tac (rep []) end; 

252 

253 
(*Repeat 1 or more times*) 

254 
fun REPEAT1 tac = tac THEN REPEAT tac; 

255 

256 

257 
(** Search tacticals **) 

258 

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

260 
fun DEPTH_FIRST satp tac = 

261 
let val tf = tracify trace_DEPTH_FIRST tac 

262 
fun depth [] = None 

263 
 depth(q::qs) = 

264 
case Sequence.pull q of 

265 
None => depth qs 

266 
 Some(st,stq) => 

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

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

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

270 

271 

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

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

274 

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

276 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

277 

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

279 
If no subgoals then it must fail! *) 

280 
fun DEPTH_SOLVE_1 tac = STATE 

281 
(fn state => 

282 
(case nprems_of state of 

283 
0 => no_tac 

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

285 

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

287 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

288 

289 
(*** Bestfirst search ***) 

290 

291 
(*Insertion into priority queue of states *) 

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

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

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

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

296 
then (n,th')::nths 

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

298 

299 
(*For creating output sequence*) 

300 
fun some_of_list [] = None 

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

302 

303 

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

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

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

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

308 
let val tf = tracify trace_BEST_FIRST tac 

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

310 
fun bfs (news,nprfs) = 

311 
(case partition satp news of 

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

313 
(map pairsize nonsats, nprfs)) 

314 
 (sats,_) => some_of_list sats) 

315 
and next [] = None 

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

317 
(if !trace_BEST_FIRST 

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

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

320 
else (); 

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

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

323 
in traced_tac tf end; 

324 

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

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

327 

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

329 
SLOW  SHOULD NOT USE APPEND!*) 

330 
fun BREADTH_FIRST satpred (Tactic tf) = 

331 
let val tacf = Sequence.list_of_s o tf; 

332 
fun bfs prfs = 

333 
(case partition satpred prfs of 

334 
([],[]) => [] 

335 
 ([],nonsats) => 

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

337 
bfs (flat (map tacf nonsats))) 

338 
 (sats,_) => sats) 

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

340 

341 

342 
(** Filtering tacticals **) 

343 

344 
(*Returns all states satisfying the predicate*) 

345 
fun FILTER pred (Tactic tf) = Tactic 

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

347 

348 
(*Returns all changed states*) 

349 
fun CHANGED (Tactic tf) = 

350 
Tactic (fn state => 

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

352 
in Sequence.filters diff (tf state) 

353 
end ); 

354 

355 

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

357 

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

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

360 
fun ALLGOALS tf = 

361 
let fun tac 0 = all_tac 

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

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

364 

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

366 
fun SOMEGOAL tf = 

367 
let fun tac 0 = no_tac 

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

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

370 

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

372 
More appropriate than SOMEGOAL in some cases.*) 

373 
fun FIRSTGOAL tf = 

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

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

376 

377 
(*Repeatedly solve some using tf. *) 

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

379 

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

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

382 

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

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

385 

386 

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

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

389 
case drop(i1, prems_of state) of 

390 
[] => Sequence.null 

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

392 

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

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

395 
composing the resulting metathm with the original state. 

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

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

398 

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

399 
(* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) 
0  400 
val dummy_quant_rl = 
401 
standard (forall_elim_var 0 (assume 

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

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

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

406 
fun protect_subgoal state i = 

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

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

409 
 _ => error"SELECT_GOAL  impossible error???"; 
0  410 

411 
(*Does the work of SELECT_GOAL. *) 

412 
fun select (Tactic tf) state i = 

413 
let val prem::_ = drop(i1, prems_of state) 

230  414 
val st0 = trivial (cterm_of (#sign(rep_thm state)) prem); 
0  415 
fun next st = bicompose false (false, st, nprems_of st) i state 
416 
in Sequence.flats (Sequence.maps next (tf st0)) 

417 
end; 

418 

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

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

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

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

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

425 

426 

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

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

429 
Main difference from strip_assums concerns parameters: 

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

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

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

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

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

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

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

437 

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

439 

440 

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

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

443 

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

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

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

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

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

449 

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

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

452 
DOES NOT HANDLE TYPE UNKNOWNS. 

453 
****) 

454 

455 
local 

456 
open Logic 

457 

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

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

460 
fun free_instantiate ctpairs = 

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

462 

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

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

465 
T) 

466 

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

468 
in 

469 

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

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

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

475 
val insts = map mk_inst hyps_vars 

476 
(*replace the hyps_vars by Frees*) 

477 
val prem' = subst_atomic insts prem 

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

479 
val fparams = map Free params 

480 
val cparams = map cterm fparams 

481 
and chyps = map cterm hyps 

482 
val hypths = map assume chyps 

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

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

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

486 
if var mem concl_vars 

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

488 
else (var, false, 

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

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

491 
fun mk_ctpair (t,in_concl,u) = 

492 
if in_concl then (cterm t, cterm u) 

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

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

495 
fun mk_subgoal_swap_ctpair 

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

497 
if in_concl then (cterm u, cterm t) 

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

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

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

501 
(*Strip the context using elimination rules*) 

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

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

504 
fun embed_ff(t,u) = 

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

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

507 
fun elim_ff ff = flexpair_abs_elim_list cparams ff 

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

509 
fun relift st = 

510 
let val prop = #prop(rep_thm st) 

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

512 
foldr add_term_vars (strip_imp_prems prop, []) 

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

514 
val subgoal_insts = map (mk_subgoal_inst concl_vars) subgoal_vars 

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

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

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

518 
val Cth = implies_elim_list st' 

519 
(map (elim_ff o assume) ffs @ 

520 
map (elim o assume) emBs) 

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

522 
free_instantiate (map swap_ctpair insts @ 

523 
map mk_subgoal_swap_ctpair subgoal_insts) 

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

525 
(implies_intr_list (ffs@emBs) 

526 
(forall_intr_list cparams (implies_intr_list chyps Cth))) 

527 
end 

528 
val subprems = map (forall_elim_vars 0) hypths 

529 
and st0 = trivial (cterm concl) 

530 
(*function to replace the current subgoal*) 

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

532 
i state 

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

534 
end); 

535 
end; 

536 

537 
fun METAHYPS tacf = SUBGOAL (metahyps_aux_tac tacf); 

538 

539 
end; 

540 
end; 