author  clasohm 
Mon, 29 Jan 1996 13:56:41 +0100  
changeset 1458  fd510875fb71 
parent 1209  03dc596b3a18 
child 1460  5a6f2aabd538 
permissions  rwrr 
1458  1 
(* Title: tactic 
0  2 
ID: $Id$ 
1458  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright 1991 University of Cambridge 
5 

6 
Tactics 

7 
*) 

8 

9 
signature TACTIC = 

10 
sig 

11 
structure Tactical: TACTICAL and Net: NET 

12 
local open Tactical Tactical.Thm Net 

13 
in 

14 
val ares_tac: thm list > int > tactic 

15 
val asm_rewrite_goal_tac: 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

16 
bool*bool > (meta_simpset > tactic) > meta_simpset > int > tactic 
0  17 
val assume_tac: int > tactic 
18 
val atac: int >tactic 

670  19 
val bimatch_from_nets_tac: 
20 
(int*(bool*thm)) net * (int*(bool*thm)) net > int > tactic 

0  21 
val bimatch_tac: (bool*thm)list > int > tactic 
670  22 
val biresolve_from_nets_tac: 
23 
(int*(bool*thm)) net * (int*(bool*thm)) net > int > tactic 

0  24 
val biresolve_tac: (bool*thm)list > int > tactic 
25 
val build_net: thm list > (int*thm) net 

670  26 
val build_netpair: (int*(bool*thm)) net * (int*(bool*thm)) net > 
27 
(bool*thm)list > (int*(bool*thm)) net * (int*(bool*thm)) net 

0  28 
val compose_inst_tac: (string*string)list > (bool*thm*int) > int > tactic 
29 
val compose_tac: (bool * thm * int) > int > tactic 

30 
val cut_facts_tac: thm list > int > tactic 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

31 
val cut_inst_tac: (string*string)list > thm > int > tactic 
0  32 
val dmatch_tac: thm list > int > tactic 
33 
val dresolve_tac: thm list > int > tactic 

34 
val dres_inst_tac: (string*string)list > thm > int > tactic 

35 
val dtac: thm > int >tactic 

36 
val etac: thm > int >tactic 

37 
val eq_assume_tac: int > tactic 

38 
val ematch_tac: thm list > int > tactic 

39 
val eresolve_tac: thm list > int > tactic 

40 
val eres_inst_tac: (string*string)list > thm > int > tactic 

41 
val filter_thms: (term*term>bool) > int*term*thm list > thm list 

42 
val filt_resolve_tac: thm list > int > int > tactic 

43 
val flexflex_tac: tactic 

44 
val fold_goals_tac: thm list > tactic 

45 
val fold_tac: thm list > tactic 

46 
val forward_tac: thm list > int > tactic 

47 
val forw_inst_tac: (string*string)list > thm > int > tactic 

947  48 
val freeze: thm > thm 
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

49 
val insert_tagged_brl: ('a*(bool*thm)) * 
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

50 
(('a*(bool*thm))net * ('a*(bool*thm))net) > 
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

51 
('a*(bool*thm))net * ('a*(bool*thm))net 
0  52 
val is_fact: thm > bool 
53 
val lessb: (bool * thm) * (bool * thm) > bool 

54 
val lift_inst_rule: thm * int * (string*string)list * thm > thm 

55 
val make_elim: thm > thm 

56 
val match_from_net_tac: (int*thm) net > int > tactic 

57 
val match_tac: thm list > int > tactic 

58 
val metacut_tac: thm > int > tactic 

59 
val net_bimatch_tac: (bool*thm) list > int > tactic 

60 
val net_biresolve_tac: (bool*thm) list > int > tactic 

61 
val net_match_tac: thm list > int > tactic 

62 
val net_resolve_tac: thm list > int > tactic 

63 
val PRIMITIVE: (thm > thm) > tactic 

64 
val PRIMSEQ: (thm > thm Sequence.seq) > tactic 

65 
val prune_params_tac: tactic 

66 
val rename_tac: string > int > tactic 

67 
val rename_last_tac: string > string list > int > tactic 

68 
val resolve_from_net_tac: (int*thm) net > int > tactic 

69 
val resolve_tac: thm list > int > tactic 

70 
val res_inst_tac: (string*string)list > thm > int > tactic 

71 
val rewrite_goals_tac: thm list > tactic 

72 
val rewrite_tac: thm list > tactic 

73 
val rewtac: thm > tactic 

1209  74 
val rotate_tac: int > int > tactic 
0  75 
val rtac: thm > int > tactic 
76 
val rule_by_tactic: tactic > thm > thm 

439  77 
val subgoal_tac: string > int > tactic 
78 
val subgoals_tac: string list > int > tactic 

0  79 
val subgoals_of_brl: bool * thm > int 
80 
val trace_goalno_tac: (int > tactic) > int > tactic 

81 
end 

82 
end; 

83 

84 

85 
functor TacticFun (structure Logic: LOGIC and Drule: DRULE and 

1458  86 
Tactical: TACTICAL and Net: NET 
87 
sharing Drule.Thm = Tactical.Thm) : TACTIC = 

0  88 
struct 
89 
structure Tactical = Tactical; 

90 
structure Thm = Tactical.Thm; 

91 
structure Net = Net; 

92 
structure Sequence = Thm.Sequence; 

93 
structure Sign = Thm.Sign; 

94 
local open Tactical Tactical.Thm Drule 

95 
in 

96 

97 
(*Discover what goal is chosen: SOMEGOAL(trace_goalno_tac tac) *) 

98 
fun trace_goalno_tac tf i = Tactic (fn state => 

99 
case Sequence.pull(tapply(tf i, state)) of 

1458  100 
None => Sequence.null 
0  101 
 seqcell => (prs("Subgoal " ^ string_of_int i ^ " selected\n"); 
1458  102 
Sequence.seqof(fn()=> seqcell))); 
0  103 

104 
fun string_of (a,0) = a 

105 
 string_of (a,i) = a ^ "_" ^ string_of_int i; 

106 

947  107 
(*convert all Vars in a theorem to Frees*) 
0  108 
fun freeze th = 
109 
let val fth = freezeT th 

110 
val {prop,sign,...} = rep_thm fth 

111 
fun mk_inst (Var(v,T)) = 

1458  112 
(cterm_of sign (Var(v,T)), 
113 
cterm_of sign (Free(string_of v, T))) 

0  114 
val insts = map mk_inst (term_vars prop) 
115 
in instantiate ([],insts) fth end; 

116 

117 
(*Makes a rule by applying a tactic to an existing rule*) 

118 
fun rule_by_tactic (Tactic tf) rl = 

119 
case Sequence.pull(tf (freeze (standard rl))) of 

1458  120 
None => raise THM("rule_by_tactic", 0, [rl]) 
0  121 
 Some(rl',_) => standard rl'; 
122 

123 
(*** Basic tactics ***) 

124 

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

126 
fun PRIMSEQ thmfun = Tactic (fn state => thmfun state 

1458  127 
handle THM _ => Sequence.null); 
0  128 

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

130 
fun PRIMITIVE thmfun = PRIMSEQ (Sequence.single o thmfun); 

131 

132 
(*** The following fail if the goal number is out of range: 

133 
thus (REPEAT (resolve_tac rules i)) stops once subgoal i disappears. *) 

134 

135 
(*Solve subgoal i by assumption*) 

136 
fun assume_tac i = PRIMSEQ (assumption i); 

137 

138 
(*Solve subgoal i by assumption, using no unification*) 

139 
fun eq_assume_tac i = PRIMITIVE (eq_assumption i); 

140 

141 
(** Resolution/matching tactics **) 

142 

143 
(*The composition rule/state: no lifting or var renaming. 

144 
The arg = (bires_flg, orule, m) ; see bicompose for explanation.*) 

145 
fun compose_tac arg i = PRIMSEQ (bicompose false arg i); 

146 

147 
(*Converts a "destruct" rule like P&Q==>P to an "elimination" rule 

148 
like [ P&Q; P==>R ] ==> R *) 

149 
fun make_elim rl = zero_var_indexes (rl RS revcut_rl); 

150 

151 
(*Attack subgoal i by resolution, using flags to indicate elimination rules*) 

152 
fun biresolve_tac brules i = PRIMSEQ (biresolution false brules i); 

153 

154 
(*Resolution: the simple case, works for introduction rules*) 

155 
fun resolve_tac rules = biresolve_tac (map (pair false) rules); 

156 

157 
(*Resolution with elimination rules only*) 

158 
fun eresolve_tac rules = biresolve_tac (map (pair true) rules); 

159 

160 
(*Forward reasoning using destruction rules.*) 

161 
fun forward_tac rls = resolve_tac (map make_elim rls) THEN' assume_tac; 

162 

163 
(*Like forward_tac, but deletes the assumption after use.*) 

164 
fun dresolve_tac rls = eresolve_tac (map make_elim rls); 

165 

166 
(*Shorthand versions: for resolution with a single theorem*) 

1458  167 
fun rtac rl = rtac rl ; 
168 
fun etac rl = etac rl ; 

169 
fun dtac rl = dtac rl ; 

0  170 
val atac = assume_tac; 
171 

172 
(*Use an assumption or some rules ... A popular combination!*) 

173 
fun ares_tac rules = assume_tac ORELSE' resolve_tac rules; 

174 

175 
(*Matching tactics  as above, but forbid updating of state*) 

176 
fun bimatch_tac brules i = PRIMSEQ (biresolution true brules i); 

177 
fun match_tac rules = bimatch_tac (map (pair false) rules); 

178 
fun ematch_tac rules = bimatch_tac (map (pair true) rules); 

179 
fun dmatch_tac rls = ematch_tac (map make_elim rls); 

180 

181 
(*Smash all flexflex disagreement pairs in the proof state.*) 

182 
val flexflex_tac = PRIMSEQ flexflex_rule; 

183 

184 
(*Lift and instantiate a rule wrt the given state and subgoal number *) 

185 
fun lift_inst_rule (state, i, sinsts, rule) = 

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

187 
val (_, _, Bi, _) = dest_state(state,i) 

1458  188 
val params = Logic.strip_params Bi (*params of subgoal i*) 
0  189 
val params = rev(rename_wrt_term Bi params) (*as they are printed*) 
190 
val paramTs = map #2 params 

191 
and inc = maxidx+1 

192 
fun liftvar (Var ((a,j), T)) = Var((a, j+inc), paramTs> incr_tvar inc T) 

193 
 liftvar t = raise TERM("Variable expected", [t]); 

194 
fun liftterm t = list_abs_free (params, 

1458  195 
Logic.incr_indexes(paramTs,inc) t) 
0  196 
(*Lifts instantiation pair over params*) 
230  197 
fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) 
0  198 
fun lifttvar((a,i),ctyp) = 
1458  199 
let val {T,sign} = rep_ctyp ctyp 
200 
in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end 

0  201 
val rts = types_sorts rule and (types,sorts) = types_sorts state 
202 
fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1)  sm => sm) 

203 
 types'(ixn) = types ixn; 

949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

204 
val used = add_term_tvarnames 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

205 
(#prop(rep_thm state) $ #prop(rep_thm rule),[]) 
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

206 
val (Tinsts,insts) = read_insts sign rts (types',sorts) used sinsts 
0  207 
in instantiate (map lifttvar Tinsts, map liftpair insts) 
949
83c588d6fee9
Changed treatment of during type inference internally generated type
nipkow
parents:
947
diff
changeset

208 
(lift_rule (state,i) rule) 
0  209 
end; 
210 

211 

212 
(*** Resolve after lifting and instantation; may refer to parameters of the 

213 
subgoal. Fails if "i" is out of range. ***) 

214 

215 
(*compose version: arguments are as for bicompose.*) 

216 
fun compose_inst_tac sinsts (bires_flg, rule, nsubgoal) i = 

217 
STATE ( fn state => 

1458  218 
compose_tac (bires_flg, lift_inst_rule (state, i, sinsts, rule), 
219 
nsubgoal) i 

220 
handle TERM (msg,_) => (writeln msg; no_tac) 

221 
 THM (msg,_,_) => (writeln msg; no_tac) ); 

0  222 

761  223 
(*"Resolve" version. Note: res_inst_tac cannot behave sensibly if the 
224 
terms that are substituted contain (term or type) unknowns from the 

225 
goal, because it is unable to instantiate goal unknowns at the same time. 

226 

952
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

227 
The type checker is instructed not to freezes flexible type vars that 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

228 
were introduced during type inference and still remain in the term at the 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

229 
end. This increases flexibility but can introduce schematic type vars in 
9e10962866b0
Removed an old bug which made some simultaneous instantiations fail if they
nipkow
parents:
949
diff
changeset

230 
goals. 
761  231 
*) 
0  232 
fun res_inst_tac sinsts rule i = 
233 
compose_inst_tac sinsts (false, rule, nprems_of rule) i; 

234 

235 
(*eresolve (elimination) version*) 

236 
fun eres_inst_tac sinsts rule i = 

237 
compose_inst_tac sinsts (true, rule, nprems_of rule) i; 

238 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

239 
(*For forw_inst_tac and dres_inst_tac. Preserve Var indexes of rl; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

240 
increment revcut_rl instead.*) 
0  241 
fun make_elim_preserve rl = 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

242 
let val {maxidx,...} = rep_thm rl 
922
196ca0973a6d
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm
parents:
761
diff
changeset

243 
fun cvar ixn = cterm_of Sign.proto_pure (Var(ixn,propT)); 
270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

244 
val revcut_rl' = 
1458  245 
instantiate ([], [(cvar("V",0), cvar("V",maxidx+1)), 
246 
(cvar("W",0), cvar("W",maxidx+1))]) revcut_rl 

0  247 
val arg = (false, rl, nprems_of rl) 
248 
val [th] = Sequence.list_of_s (bicompose false arg 1 revcut_rl') 

249 
in th end 

250 
handle Bind => raise THM("make_elim_preserve", 1, [rl]); 

251 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

252 
(*instantiate and cut  for a FACT, anyway...*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

253 
fun cut_inst_tac sinsts rule = res_inst_tac sinsts (make_elim_preserve rule); 
0  254 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

255 
(*forward tactic applies a RULE to an assumption without deleting it*) 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

256 
fun forw_inst_tac sinsts rule = cut_inst_tac sinsts rule THEN' assume_tac; 
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

257 

d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

258 
(*dresolve tactic applies a RULE to replace an assumption*) 
0  259 
fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); 
260 

270
d506ea00c825
tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead
lcp
parents:
230
diff
changeset

261 
(*** Applications of cut_rl ***) 
0  262 

263 
(*Used by metacut_tac*) 

264 
fun bires_cut_tac arg i = 

1458  265 
rtac cut_rl i THEN biresolve_tac arg (i+1) ; 
0  266 

267 
(*The conclusion of the rule gets assumed in subgoal i, 

268 
while subgoal i+1,... are the premises of the rule.*) 

269 
fun metacut_tac rule = bires_cut_tac [(false,rule)]; 

270 

271 
(*Recognizes theorems that are not rules, but simple propositions*) 

272 
fun is_fact rl = 

273 
case prems_of rl of 

1458  274 
[] => true  _::_ => false; 
0  275 

276 
(*"Cut" all facts from theorem list into the goal as assumptions. *) 

277 
fun cut_facts_tac ths i = 

278 
EVERY (map (fn th => metacut_tac th i) (filter is_fact ths)); 

279 

280 
(*Introduce the given proposition as a lemma and subgoal*) 

281 
fun subgoal_tac sprop = res_inst_tac [("psi", sprop)] cut_rl; 

282 

439  283 
(*Introduce a list of lemmas and subgoals*) 
284 
fun subgoals_tac sprops = EVERY' (map subgoal_tac sprops); 

285 

0  286 

287 
(**** Indexing and filtering of theorems ****) 

288 

289 
(*Returns the list of potentially resolvable theorems for the goal "prem", 

1458  290 
using the predicate could(subgoal,concl). 
0  291 
Resulting list is no longer than "limit"*) 
292 
fun filter_thms could (limit, prem, ths) = 

293 
let val pb = Logic.strip_assums_concl prem; (*delete assumptions*) 

294 
fun filtr (limit, []) = [] 

1458  295 
 filtr (limit, th::ths) = 
296 
if limit=0 then [] 

297 
else if could(pb, concl_of th) then th :: filtr(limit1, ths) 

298 
else filtr(limit,ths) 

0  299 
in filtr(limit,ths) end; 
300 

301 

302 
(*** biresolution and resolution using nets ***) 

303 

304 
(** To preserve the order of the rules, tag them with increasing integers **) 

305 

306 
(*insert tags*) 

307 
fun taglist k [] = [] 

308 
 taglist k (x::xs) = (k,x) :: taglist (k+1) xs; 

309 

310 
(*remove tags and suppress duplicates  list is assumed sorted!*) 

311 
fun untaglist [] = [] 

312 
 untaglist [(k:int,x)] = [x] 

313 
 untaglist ((k,x) :: (rest as (k',x')::_)) = 

314 
if k=k' then untaglist rest 

315 
else x :: untaglist rest; 

316 

317 
(*return list elements in original order*) 

318 
val orderlist = untaglist o sort (fn(x,y)=> #1 x < #1 y); 

319 

320 
(*insert one tagged brl into the pair of nets*) 

1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

321 
fun insert_tagged_brl (kbrl as (k,(eres,th)), (inet,enet)) = 
0  322 
if eres then 
1458  323 
case prems_of th of 
324 
prem::_ => (inet, Net.insert_term ((prem,kbrl), enet, K false)) 

325 
 [] => error"insert_tagged_brl: elimination rule with no premises" 

0  326 
else (Net.insert_term ((concl_of th, kbrl), inet, K false), enet); 
327 

328 
(*build a pair of nets for biresolution*) 

670  329 
fun build_netpair netpair brls = 
1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

330 
foldr insert_tagged_brl (taglist 1 brls, netpair); 
0  331 

332 
(*biresolution using a pair of nets rather than rules*) 

333 
fun biresolution_from_nets_tac match (inet,enet) = 

334 
SUBGOAL 

335 
(fn (prem,i) => 

336 
let val hyps = Logic.strip_assums_hyp prem 

337 
and concl = Logic.strip_assums_concl prem 

338 
val kbrls = Net.unify_term inet concl @ 

339 
flat (map (Net.unify_term enet) hyps) 

340 
in PRIMSEQ (biresolution match (orderlist kbrls) i) end); 

341 

342 
(*versions taking prebuilt nets*) 

343 
val biresolve_from_nets_tac = biresolution_from_nets_tac false; 

344 
val bimatch_from_nets_tac = biresolution_from_nets_tac true; 

345 

346 
(*fast versions using nets internally*) 

670  347 
val net_biresolve_tac = 
348 
biresolve_from_nets_tac o build_netpair(Net.empty,Net.empty); 

349 

350 
val net_bimatch_tac = 

351 
bimatch_from_nets_tac o build_netpair(Net.empty,Net.empty); 

0  352 

353 
(*** Simpler version for resolve_tac  only one net, and no hyps ***) 

354 

355 
(*insert one tagged rl into the net*) 

356 
fun insert_krl (krl as (k,th), net) = 

357 
Net.insert_term ((concl_of th, krl), net, K false); 

358 

359 
(*build a net of rules for resolution*) 

360 
fun build_net rls = 

361 
foldr insert_krl (taglist 1 rls, Net.empty); 

362 

363 
(*resolution using a net rather than rules; pred supports filt_resolve_tac*) 

364 
fun filt_resolution_from_net_tac match pred net = 

365 
SUBGOAL 

366 
(fn (prem,i) => 

367 
let val krls = Net.unify_term net (Logic.strip_assums_concl prem) 

368 
in 

1458  369 
if pred krls 
0  370 
then PRIMSEQ 
1458  371 
(biresolution match (map (pair false) (orderlist krls)) i) 
0  372 
else no_tac 
373 
end); 

374 

375 
(*Resolve the subgoal using the rules (making a net) unless too flexible, 

376 
which means more than maxr rules are unifiable. *) 

377 
fun filt_resolve_tac rules maxr = 

378 
let fun pred krls = length krls <= maxr 

379 
in filt_resolution_from_net_tac false pred (build_net rules) end; 

380 

381 
(*versions taking prebuilt nets*) 

382 
val resolve_from_net_tac = filt_resolution_from_net_tac false (K true); 

383 
val match_from_net_tac = filt_resolution_from_net_tac true (K true); 

384 

385 
(*fast versions using nets internally*) 

386 
val net_resolve_tac = resolve_from_net_tac o build_net; 

387 
val net_match_tac = match_from_net_tac o build_net; 

388 

389 

390 
(*** For Natural Deduction using (bires_flg, rule) pairs ***) 

391 

392 
(*The number of new subgoals produced by the brule*) 

1077
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

393 
fun subgoals_of_brl (true,rule) = nprems_of rule  1 
c2df11ae8b55
Renamed insert_kbrl to insert_tagged_brl and exported it. Now
lcp
parents:
952
diff
changeset

394 
 subgoals_of_brl (false,rule) = nprems_of rule; 
0  395 

396 
(*Lessthan test: for sorting to minimize number of new subgoals*) 

397 
fun lessb (brl1,brl2) = subgoals_of_brl brl1 < subgoals_of_brl brl2; 

398 

399 

400 
(*** MetaRewriting Tactics ***) 

401 

402 
fun result1 tacf mss thm = 

403 
case Sequence.pull(tapply(tacf mss,thm)) of 

404 
None => None 

405 
 Some(thm,_) => Some(thm); 

406 

407 
(*Rewrite subgoal i only *) 

214
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

408 
fun asm_rewrite_goal_tac mode prover_tac mss i = 
ed6a3e2b1a33
added new parameter to the simplification tactics which indicates if
nipkow
parents:
191
diff
changeset

409 
PRIMITIVE(rewrite_goal_rule mode (result1 prover_tac) mss i); 
0  410 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

411 
(*Rewrite throughout proof state. *) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

412 
fun rewrite_tac defs = PRIMITIVE(rewrite_rule defs); 
0  413 

414 
(*Rewrite subgoals only, not main goal. *) 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

415 
fun rewrite_goals_tac defs = PRIMITIVE (rewrite_goals_rule defs); 
0  416 

1458  417 
fun rewtac def = rewtac def; 
0  418 

419 

69
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

420 
(*** Tactic for folding definitions, handling critical pairs ***) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

421 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

422 
(*The depth of nesting in a term*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

423 
fun term_depth (Abs(a,T,t)) = 1 + term_depth t 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

424 
 term_depth (f$t) = 1 + max [term_depth f, term_depth t] 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

425 
 term_depth _ = 0; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

426 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

427 
val lhs_of_thm = #1 o Logic.dest_equals o #prop o rep_thm; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

428 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

429 
(*folding should handle critical pairs! E.g. K == Inl(0), S == Inr(Inl(0)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

430 
Returns longest lhs first to avoid folding its subexpressions.*) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

431 
fun sort_lhs_depths defs = 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

432 
let val keylist = make_keylist (term_depth o lhs_of_thm) defs 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

433 
val keys = distinct (sort op> (map #2 keylist)) 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

434 
in map (keyfilter keylist) keys end; 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

435 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

436 
fun fold_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

437 
(map rewrite_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

438 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

439 
fun fold_goals_tac defs = EVERY 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

440 
(map rewrite_goals_tac (sort_lhs_depths (map symmetric defs))); 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

441 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

442 

e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

443 
(*** Renaming of parameters in a subgoal 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

444 
Names may contain letters, digits or primes and must be 
e7588b53d6b0
tactic/fold_tac,fold_goals_tac: now handle critical pairs on the
lcp
parents:
0
diff
changeset

445 
separated by blanks ***) 
0  446 

447 
(*Calling this will generate the warning "Same as previous level" since 

448 
it affects nothing but the names of bound variables!*) 

449 
fun rename_tac str i = 

450 
let val cs = explode str 

451 
in 

452 
if !Logic.auto_rename 

453 
then (writeln"Note: setting Logic.auto_rename := false"; 

1458  454 
Logic.auto_rename := false) 
0  455 
else (); 
456 
case #2 (take_prefix (is_letdig orf is_blank) cs) of 

457 
[] => PRIMITIVE (rename_params_rule (scanwords is_letdig cs, i)) 

458 
 c::_ => error ("Illegal character: " ^ c) 

459 
end; 

460 

461 
(*Rename recent parameters using names generated from (a) and the suffixes, 

462 
provided the string (a), which represents a term, is an identifier. *) 

463 
fun rename_last_tac a sufs i = 

464 
let val names = map (curry op^ a) sufs 

465 
in if Syntax.is_identifier a 

466 
then PRIMITIVE (rename_params_rule (names,i)) 

467 
else all_tac 

468 
end; 

469 

470 
(*Prunes all redundant parameters from the proof state by rewriting*) 

471 
val prune_params_tac = rewrite_tac [triv_forall_equality]; 

472 

1209  473 
(* rotate_tac n i: rotate the assumptions of subgoal i by n positions, from 
474 
* right to left if n is positive, and from left to right if n is negative. 

475 
*) 

476 
fun rotate_tac n = 

477 
let fun rot(n) = EVERY'(replicate n (dtac asm_rl)); 

478 
in if n >= 0 then rot n 

479 
else SUBGOAL (fn (t,i) => rot(length(Logic.strip_assums_hyp t)+n) i) 

480 
end; 

481 

0  482 
end; 
483 
end; 