author  noschinl 
Fri, 17 Apr 2015 10:49:57 +0200  
changeset 60108  d7fe3e0aca85 
parent 60088  0a064330a885 
child 60109  22389d4cdd6b 
permissions  rwrr 
59975  1 
(* Title: HOL/Library/rewrite.ML 
2 
Author: Christoph Traut, Lars Noschinski, TU Muenchen 

59739  3 

59975  4 
This is a rewrite method that supports subtermselection based on patterns. 
59739  5 

59975  6 
The patterns accepted by rewrite are of the following form: 
7 
<atom> ::= <term>  "concl"  "asm"  "for" "(" <names> ")" 

8 
<pattern> ::= (in <atom>  at <atom>) [<pattern>] 

9 
<args> ::= [<pattern>] ("to" <term>) <thms> 

59739  10 

59975  11 
This syntax was clearly inspired by Gonthier's and Tassi's language of 
12 
patterns but has diverged significantly during its development. 

59739  13 

59975  14 
We also allow introduction of identifiers for bound variables, 
15 
which can then be used to match arbitrary subterms inside abstractions. 

59739  16 
*) 
17 

59975  18 
signature REWRITE = 
19 
sig 

60079  20 
datatype ('a, 'b) pattern = At  In  Term of 'a  Concl  Asm  For of 'b list 
21 

22 
val mk_hole: int > typ > term 

23 

24 
val rewrite: Proof.context 

25 
> (term * (string * typ) list, string * typ option) pattern list * term option 

26 
> thm list 

27 
> cterm 

28 
> thm Seq.seq 

29 

30 
val rewrite_tac: Proof.context 

31 
> (term * (string * typ) list, string * typ option) pattern list * term option 

32 
> thm list 

33 
> int 

34 
> tactic 

59739  35 
end 
36 

59975  37 
structure Rewrite : REWRITE = 
59739  38 
struct 
39 

40 
datatype ('a, 'b) pattern = At  In  Term of 'a  Concl  Asm  For of 'b list 

41 

42 
fun map_term_pattern f (Term x) = f x 

43 
 map_term_pattern _ (For ss) = (For ss) 

44 
 map_term_pattern _ At = At 

45 
 map_term_pattern _ In = In 

46 
 map_term_pattern _ Concl = Concl 

47 
 map_term_pattern _ Asm = Asm 

48 

49 

50 
exception NO_TO_MATCH 

51 

52 
fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq 

53 

54 
(* We rewrite subterms using rewrite conversions. These are conversions 

55 
that also take a context and a list of identifiers for bound variables 

56 
as parameters. *) 

57 
type rewrite_conv = Proof.context > (string * term) list > conv 

58 

59 
(* To apply such a rewrite conversion to a subterm of our goal, we use 

60 
subterm positions, which are just functions that map a rewrite conversion, 

61 
working on the top level, to a new rewrite conversion, working on 

62 
a specific subterm. 

63 

64 
During substitution, we are traversing the goal to find subterms that 

65 
we can rewrite. For each of these subterms, a subterm position is 

66 
created and later used in creating a conversion that we use to try and 

67 
rewrite this subterm. *) 

68 
type subterm_position = rewrite_conv > rewrite_conv 

69 

70 
(* A focusterm represents a subterm. It is a tuple (t, p), consisting 

71 
of the subterm t itself and its subterm position p. *) 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

72 
type focusterm = (Type.tyenv * Proof.context) * term * subterm_position 
59739  73 

74 
val dummyN = Name.internal "__dummy" 

75 
val holeN = Name.internal "_hole" 

76 

77 
fun prep_meta_eq ctxt = 

78 
Simplifier.mksimps ctxt #> map Drule.zero_var_indexes 

79 

80 

81 
(* rewrite conversions *) 

82 

83 
fun abs_rewr_cconv ident : subterm_position = 

84 
let 

85 
fun add_ident NONE _ l = l 

86 
 add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l 

59975  87 
fun inner rewr ctxt idents = 
88 
CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt 

59739  89 
in inner end 
59975  90 

59739  91 
val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr 
92 
val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr 

60050  93 
val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr 
60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset

94 
val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr 
59739  95 

96 

97 
(* focus terms *) 

98 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

99 
fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) = 
59739  100 
case try (fastype_of #> dest_funT) u of 
101 
NONE => raise TERM ("ft_abs: no function type", [u]) 

102 
 SOME (U, _) => 

59975  103 
let 
104 
val tyenv' = 

105 
if T = dummyT then tyenv 

106 
else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

107 
val (s', u_ctxt') = 
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

108 
case s of 
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

109 
NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt 
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

110 
 SOME s => (s, u_ctxt) 
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

111 
val x = Free (s', Envir.norm_type tyenv' T) 
59975  112 
val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand} 
113 
fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds 

114 
val (u', pos') = 

115 
case u of 

116 
Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s) 

117 
 _ => (u $ x, pos o eta_expand o abs_rewr_cconv s) 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

118 
in ((tyenv', u_ctxt'), u', pos') end 
59975  119 
handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u]) 
59739  120 

121 
fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv) 

122 
 ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft 

123 
 ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t]) 

124 

60050  125 
local 
126 

127 
fun ft_arg_gen cconv _ (tyenv, _ $ r, pos) = (tyenv, r, pos o cconv) 

128 
 ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft 

129 
 ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t]) 

130 

131 
in 

132 

133 
val ft_arg = ft_arg_gen arg_rewr_cconv 

134 
val ft_imp = ft_arg_gen imp_rewr_cconv 

135 

136 
end 

59739  137 

138 
(* Move to B in !!x_1 ... x_n. B. Do not etaexpand *) 

139 
fun ft_params ctxt (ft as (_, t, _) : focusterm) = 

140 
case t of 

141 
Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) => 

142 
(ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft 

143 
 Const (@{const_name "Pure.all"}, _) => 

144 
(ft_params ctxt o ft_arg ctxt) ft 

145 
 _ => ft 

146 

147 
fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) = 

148 
let 

149 
val def_U = T > dest_funT > fst > dest_funT > fst 

150 
val ident' = apsnd (the_default (def_U)) ident 

151 
in (ft_abs ctxt ident' o ft_arg ctxt) ft end 

152 
 ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t]) 

153 

154 
fun ft_for ctxt idents (ft as (_, t, _) : focusterm) = 

155 
let 

156 
fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) = 

157 
let 

158 
val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u  _ => t) 

159 
in 

160 
case rev_idents' of 

161 
[] => ([], desc o ft_all ctxt (NONE, NONE)) 

162 
 (x :: xs) => (xs , desc o ft_all ctxt x) 

163 
end 

164 
 f rev_idents _ = (rev_idents, I) 

59975  165 
in 
166 
case f (rev idents) t of 

59739  167 
([], ft') => SOME (ft' ft) 
168 
 _ => NONE 

169 
end 

170 

171 
fun ft_concl ctxt (ft as (_, t, _) : focusterm) = 

172 
case t of 

60050  173 
(Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft 
59739  174 
 _ => ft 
175 

60054
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset

176 
fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) = 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset

177 
(tyenv, l, pos o with_prems_rewr_cconv) 
ef4878146485
rewrite: with asm pattern, propagate also remaining assumptions to new subgoals
noschinl
parents:
60053
diff
changeset

178 
 ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t]) 
59739  179 

180 
fun ft_judgment ctxt (ft as (_, t, _) : focusterm) = 

59970  181 
if Object_Logic.is_judgment ctxt t 
59739  182 
then ft_arg ctxt ft 
183 
else ft 

184 

60055  185 
(* Find all subterms that might be a valid point to apply a rule. *) 
186 
fun valid_match_points ctxt (ft : focusterm) = 

59739  187 
let 
60055  188 
fun descend (_, _ $ _, _) = [ft_fun ctxt, ft_arg ctxt] 
189 
 descend (_, Abs (_, T, _), _) = [ft_abs ctxt (NONE, T)] 

190 
 descend _ = [] 

191 
fun subseq ft = 

192 
descend ft > Seq.of_list > Seq.maps (fn f => ft > f > valid_match_points ctxt) 

59739  193 
fun is_valid (l $ _) = is_valid l 
194 
 is_valid (Abs (_, _, a)) = is_valid a 

195 
 is_valid (Var _) = false 

196 
 is_valid (Bound _) = false 

197 
 is_valid _ = true 

198 
in 

60055  199 
Seq.make (fn () => SOME (ft, subseq ft)) 
200 
> Seq.filter (#2 #> is_valid) 

59739  201 
end 
202 

60079  203 
fun mk_hole i T = Var ((holeN, i), T) 
204 

59739  205 
fun is_hole (Var ((name, _), _)) = (name = holeN) 
206 
 is_hole _ = false 

207 

208 
fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true 

209 
 is_hole_const _ = false 

210 

211 
val hole_syntax = 

212 
let 

213 
(* Modified variant of Term.replace_hole *) 

214 
fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i = 

60079  215 
(list_comb (mk_hole i (Ts > T), map_range Bound (length Ts)), i + 1) 
59739  216 
 replace_hole Ts (Abs (x, T, t)) i = 
217 
let val (t', i') = replace_hole (T :: Ts) t i 

218 
in (Abs (x, T, t'), i') end 

219 
 replace_hole Ts (t $ u) i = 

220 
let 

221 
val (t', i') = replace_hole Ts t i 

222 
val (u', i'') = replace_hole Ts u i' 

223 
in (t' $ u', i'') end 

224 
 replace_hole _ a i = (a, i) 

225 
fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1) 

226 
in 

227 
Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes)) 

228 
#> Proof_Context.set_mode Proof_Context.mode_pattern 

229 
end 

230 

231 
(* Find a subterm of the focusterm matching the pattern. *) 

232 
fun find_matches ctxt pattern_list = 

233 
let 

234 
fun move_term ctxt (t, off) (ft : focusterm) = 

235 
let 

236 
val thy = Proof_Context.theory_of ctxt 

237 

238 
val eta_expands = 

239 
let val (_, ts) = strip_comb t 

240 
in map fastype_of (snd (take_suffix is_Var ts)) end 

241 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

242 
fun do_match ((tyenv, u_ctxt), u, pos) = 
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

243 
case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of 
59739  244 
NONE => NONE 
60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

245 
 SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos)) 
59739  246 

247 
fun match_argT T u = 

248 
let val (U, _) = dest_funT (fastype_of u) 

249 
in try (Sign.typ_match thy (T,U)) end 

250 
handle TYPE _ => K NONE 

251 

252 
fun desc [] ft = do_match ft 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

253 
 desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) = 
59739  254 
case do_match ft of 
255 
NONE => 

256 
(case match_argT T u tyenv of 

257 
NONE => NONE 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

258 
 SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos))) 
59739  259 
 SOME ft => SOME ft 
260 
in desc eta_expands ft end 

261 

60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

262 
fun move_assms ctxt (ft: focusterm) = 
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

263 
let 
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

264 
fun f () = case try (ft_assm ctxt) ft of 
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

265 
NONE => NONE 
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

266 
 SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft)) 
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

267 
in Seq.make f end 
59739  268 

269 
fun apply_pat At = Seq.map (ft_judgment ctxt) 

270 
 apply_pat In = Seq.maps (valid_match_points ctxt) 

60052
616a17640229
rewrite: with asm pattern, try all premises for rewriting, not only the first
noschinl
parents:
60051
diff
changeset

271 
 apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt) 
59739  272 
 apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt) 
273 
 apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents))) 

274 
 apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x)) 

275 

276 
fun apply_pats ft = ft 

277 
> Seq.single 

278 
> fold apply_pat pattern_list 

279 
in 

280 
apply_pats 

281 
end 

282 

283 
fun instantiate_normalize_env ctxt env thm = 

284 
let 

285 
fun certs f = map (apply2 (f ctxt)) 

286 
val prop = Thm.prop_of thm 

287 
val norm_type = Envir.norm_type o Envir.type_env 

288 
val insts = Term.add_vars prop [] 

289 
> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x))) 

290 
> certs Thm.cterm_of 

291 
val tyinsts = Term.add_tvars prop [] 

292 
> map (fn x => (TVar x, norm_type env (TVar x))) 

293 
> certs Thm.ctyp_of 

294 
in Drule.instantiate_normalize (tyinsts, insts) thm end 

295 

296 
fun unify_with_rhs context to env thm = 

297 
let 

298 
val (_, rhs) = thm > Thm.concl_of > Logic.dest_equals 

299 
val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env 

300 
handle Pattern.Unif => raise NO_TO_MATCH 

301 
in env' end 

302 

303 
fun inst_thm_to _ (NONE, _) thm = thm 

304 
 inst_thm_to (ctxt : Proof.context) (SOME to, env) thm = 

305 
instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm 

306 

307 
fun inst_thm ctxt idents (to, tyenv) thm = 

308 
let 

309 
(* Replace any identifiers with their corresponding bound variables. *) 

310 
val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0 

311 
val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv} 

312 
val replace_idents = 

313 
let 

314 
fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t 

315 
 subst _ t = t 

316 
in Term.map_aterms (subst idents) end 

317 

60051  318 
val maxidx = Envir.maxidx_of env > fold Term.maxidx_term (the_list to) 
59739  319 
val thm' = Thm.incr_indexes (maxidx + 1) thm 
320 
in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end 

321 
handle NO_TO_MATCH => NONE 

322 

60079  323 
local 
324 

325 
fun rewrite_raw ctxt (pattern, to) thms ct = 

59739  326 
let 
60079  327 
fun interpret_term_patterns ctxt = 
328 
let 

329 

330 
fun descend_hole fixes (Abs (_, _, t)) = 

331 
(case descend_hole fixes t of 

332 
NONE => NONE 

333 
 SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix)) 

334 
 SOME ([], _) => raise Match (* XXX  check phases modified binding *)) 

335 
 descend_hole fixes (t as l $ r) = 

336 
let val (f, _) = strip_comb t 

337 
in 

338 
if is_hole f 

339 
then SOME (fixes, I) 

340 
else 

341 
(case descend_hole fixes l of 

342 
SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt) 

343 
 NONE => 

344 
(case descend_hole fixes r of 

345 
SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt) 

346 
 NONE => NONE)) 

347 
end 

348 
 descend_hole fixes t = 

349 
if is_hole t then SOME (fixes, I) else NONE 

350 

351 
fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t) 

352 

353 
in map (map_term_pattern f) end 

354 

355 
val pattern' = interpret_term_patterns ctxt pattern 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

356 
val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I) 
60079  357 

358 
val thms' = maps (prep_meta_eq ctxt) thms 

59739  359 

360 
fun rewrite_conv insty ctxt bounds = 

60079  361 
CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) thms') 
59739  362 

363 
fun distinct_prems th = 

364 
case Seq.pull (distinct_subgoals_tac th) of 

365 
NONE => th 

366 
 SOME (th', _) => th' 

367 

60088
0a064330a885
rewrite: use distinct names for unnamed abstractions
noschinl
parents:
60079
diff
changeset

368 
fun conv (((tyenv, _), _, position) : focusterm) = 
60079  369 
distinct_prems o position (rewrite_conv (to, tyenv)) ctxt [] 
370 

371 
in Seq.map (fn ft => conv ft) matches end 

372 

373 
in 

374 

375 
fun rewrite ctxt pat thms ct = 

376 
rewrite_raw ctxt pat thms ct > Seq.map_filter (fn cv => try cv ct) 

59739  377 

60079  378 
fun rewrite_export_tac ctxt (pat, pat_ctxt) thms = 
59739  379 
let 
60079  380 
val export = case pat_ctxt of 
381 
NONE => I 

382 
 SOME inner => singleton (Proof_Context.export inner ctxt) 

383 
val tac = CSUBGOAL (fn (ct, i) => 

384 
rewrite_raw ctxt pat thms ct 

385 
> Seq.map (fn cv => CCONVERSION (export o cv) i) 

386 
> SEQ_CONCAT) 

59739  387 
in tac end 
388 

60079  389 
fun rewrite_tac ctxt pat = rewrite_export_tac ctxt (pat, NONE) 
390 

391 
end 

392 

59975  393 
val _ = 
394 
Theory.setup 

59739  395 
let 
396 
fun mk_fix s = (Binding.name s, NONE, NoSyn) 

397 

398 
val raw_pattern : (string, binding * string option * mixfix) pattern list parser = 

399 
let 

400 
val sep = (Args.$$$ "at" >> K At)  (Args.$$$ "in" >> K In) 

401 
val atom = (Args.$$$ "asm" >> K Asm)  

402 
(Args.$$$ "concl" >> K Concl)  

403 
(Args.$$$ "for"  Args.parens (Scan.optional Parse.fixes []) >> For)  

404 
(Parse.term >> Term) 

405 
val sep_atom = sep  atom >> (fn (s,a) => [s,a]) 

406 

407 
fun append_default [] = [Concl, In] 

408 
 append_default (ps as Term _ :: _) = Concl :: In :: ps 

60108
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset

409 
 append_default [For x, In] = [For x, Concl, In] 
d7fe3e0aca85
rewrite: add default pattern "in concl" for more cases
noschinl
parents:
60088
diff
changeset

410 
 append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps 
59739  411 
 append_default ps = ps 
412 

413 
in Scan.repeat sep_atom >> (flat #> rev #> append_default) end 

414 

59975  415 
fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) => 
59739  416 
let 
417 
val (r, toks') = scan toks 

59975  418 
val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context 
419 
in (r', (context', toks' : Token.T list)) end 

59739  420 

421 
fun read_fixes fixes ctxt = 

422 
let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx) 

423 
in Proof_Context.add_fixes (map read_typ fixes) ctxt end 

424 

425 
fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) = 

426 
let 

427 
fun add_constrs ctxt n (Abs (x, T, t)) = 

428 
let 

429 
val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt 

430 
in 

431 
(case add_constrs ctxt' (n+1) t of 

432 
NONE => NONE 

433 
 SOME ((ctxt'', n', xs), t') => 

434 
let 

435 
val U = Type_Infer.mk_param n [] 

436 
val u = Type.constraint (U > dummyT) (Abs (x, T, t')) 

437 
in SOME ((ctxt'', n', (x', U) :: xs), u) end) 

438 
end 

439 
 add_constrs ctxt n (l $ r) = 

440 
(case add_constrs ctxt n l of 

441 
SOME (c, l') => SOME (c, l' $ r) 

442 
 NONE => 

443 
(case add_constrs ctxt n r of 

444 
SOME (c, r') => SOME (c, l $ r') 

445 
 NONE => NONE)) 

446 
 add_constrs ctxt n t = 

447 
if is_hole_const t then SOME ((ctxt, n, []), t) else NONE 

448 

449 
fun prep (Term s) (n, ctxt) = 

450 
let 

451 
val t = Syntax.parse_term ctxt s 

452 
val ((ctxt', n', bs), t') = 

453 
the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t) 

454 
in (Term (t', bs), (n', ctxt')) end 

455 
 prep (For ss) (n, ctxt) = 

456 
let val (ns, ctxt') = read_fixes ss ctxt 

457 
in (For ns, (n, ctxt')) end 

458 
 prep At (n,ctxt) = (At, (n, ctxt)) 

459 
 prep In (n,ctxt) = (In, (n, ctxt)) 

460 
 prep Concl (n,ctxt) = (Concl, (n, ctxt)) 

461 
 prep Asm (n,ctxt) = (Asm, (n, ctxt)) 

462 

463 
val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt) 

464 

465 
in (xs, ctxt') end 

466 

467 
fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) = 

468 
let 

469 

470 
fun check_terms ctxt ps to = 

471 
let 

472 
fun safe_chop (0: int) xs = ([], xs) 

473 
 safe_chop n (x :: xs) = chop (n  1) xs >> cons x 

474 
 safe_chop _ _ = raise Match 

475 

476 
fun reinsert_pat _ (Term (_, cs)) (t :: ts) = 

477 
let val (cs', ts') = safe_chop (length cs) ts 

478 
in (Term (t, map dest_Free cs'), ts') end 

479 
 reinsert_pat _ (Term _) [] = raise Match 

480 
 reinsert_pat ctxt (For ss) ts = 

481 
let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss 

482 
in (For fixes, ts) end 

483 
 reinsert_pat _ At ts = (At, ts) 

484 
 reinsert_pat _ In ts = (In, ts) 

485 
 reinsert_pat _ Concl ts = (Concl, ts) 

486 
 reinsert_pat _ Asm ts = (Asm, ts) 

487 

488 
fun free_constr (s,T) = Type.constraint T (Free (s, dummyT)) 

489 
fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs 

490 
 mk_free_constrs _ = [] 

491 

60051  492 
val ts = maps mk_free_constrs ps @ the_list to 
59739  493 
> Syntax.check_terms (hole_syntax ctxt) 
494 
val ctxt' = fold Variable.declare_term ts ctxt 

495 
val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts 

496 
> (fn xs => case to of NONE => (NONE, xs)  SOME _ => (SOME (hd xs), tl xs)) 

497 
val _ = case ts' of (_ :: _) => raise Match  [] => () 

498 
in ((ps', to'), ctxt') end 

499 

500 
val (pats, ctxt') = prep_pats ctxt raw_pats 

501 

502 
val ths = Attrib.eval_thms ctxt' raw_ths 

503 
val to = Option.map (Syntax.parse_term ctxt') raw_to 

504 

505 
val ((pats', to'), ctxt'') = check_terms ctxt' pats to 

506 

60079  507 
in ((pats', ths, (to', ctxt)), ctxt'') end 
59739  508 

509 
val to_parser = Scan.option ((Args.$$$ "to")  Parse.term) 

510 

511 
val subst_parser = 

512 
let val scan = raw_pattern  to_parser  Parse.xthms1 

59975  513 
in context_lift scan prep_args end 
59739  514 
in 
515 
Method.setup @{binding rewrite} (subst_parser >> 

60079  516 
(fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt => 
517 
SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms))) 

59739  518 
"singlestep rewriting, allowing subterm selection via patterns." 
519 
end 

520 
end 