src/HOL/Library/rewrite.ML
author noschinl
Fri Apr 17 11:12:19 2015 +0200 (2015-04-17)
changeset 60109 22389d4cdd6b
parent 60108 d7fe3e0aca85
parent 60102 820e8e704ba6
child 60117 2712f40d6309
permissions -rw-r--r--
merged
     1 (*  Title:      HOL/Library/rewrite.ML
     2     Author:     Christoph Traut, Lars Noschinski, TU Muenchen
     3 
     4 This is a rewrite method that supports subterm-selection based on patterns.
     5 
     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>
    10 
    11 This syntax was clearly inspired by Gonthier's and Tassi's language of
    12 patterns but has diverged significantly during its development.
    13 
    14 We also allow introduction of identifiers for bound variables,
    15 which can then be used to match arbitrary subterms inside abstractions.
    16 *)
    17 
    18 signature REWRITE =
    19 sig
    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
    35 end
    36 
    37 structure Rewrite : REWRITE =
    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. *)
    72 type focusterm = (Type.tyenv * Proof.context) * term * subterm_position
    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
    87     fun inner rewr ctxt idents =
    88       CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    89   in inner end
    90 
    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
    93 val imp_rewr_cconv : subterm_position = fn rewr => CConv.concl_cconv 1 oo rewr
    94 val with_prems_rewr_cconv : subterm_position = fn rewr => CConv.with_prems_cconv ~1 oo rewr
    95 
    96 
    97 (* focus terms *)
    98 
    99 fun ft_abs ctxt (s,T) ((tyenv, u_ctxt), u, pos) =
   100   case try (fastype_of #> dest_funT) u of
   101     NONE => raise TERM ("ft_abs: no function type", [u])
   102   | SOME (U, _) =>
   103       let
   104         val tyenv' =
   105           if T = dummyT then tyenv
   106           else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
   107         val (s', u_ctxt') =
   108           case s of
   109            NONE => yield_singleton Variable.variant_fixes (Name.internal dummyN) u_ctxt
   110           | SOME s => (s, u_ctxt)
   111         val x = Free (s', Envir.norm_type tyenv' T)
   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)
   118       in ((tyenv', u_ctxt'), u', pos') end
   119       handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
   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 
   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 fun ft_arg ctxt = ft_arg_gen arg_rewr_cconv ctxt
   134 fun ft_imp ctxt = ft_arg_gen imp_rewr_cconv ctxt
   135 
   136 end
   137 
   138 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
   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)
   165   in
   166     case f (rev idents) t of
   167       ([], ft') => SOME (ft' ft)
   168     | _ => NONE
   169   end
   170 
   171 fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
   172   case t of
   173     (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_imp ctxt) ft
   174   | _ => ft
   175 
   176 fun ft_assm _ (tyenv, (Const (@{const_name "Pure.imp"}, _) $ l) $ _, pos) =
   177       (tyenv, l, pos o with_prems_rewr_cconv)
   178   | ft_assm _ (_, t, _) = raise TERM ("ft_assm", [t])
   179 
   180 fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
   181   if Object_Logic.is_judgment ctxt t
   182   then ft_arg ctxt ft
   183   else ft
   184 
   185 (* Find all subterms that might be a valid point to apply a rule. *)
   186 fun valid_match_points ctxt (ft : focusterm) =
   187   let
   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)
   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
   199     Seq.make (fn () => SOME (ft, subseq ft))
   200     |> Seq.filter (#2 #> is_valid)
   201   end
   202 
   203 fun mk_hole i T = Var ((holeN, i), T)
   204 
   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 =
   215           (list_comb (mk_hole i (Ts ---> T), map_range Bound (length Ts)), i + 1)
   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 
   242         fun do_match ((tyenv, u_ctxt), u, pos) =
   243           case try (Pattern.match thy (apply2 Logic.mk_term (t,u))) (tyenv, Vartab.empty) of
   244             NONE => NONE
   245           | SOME (tyenv', _) => SOME (off ((tyenv', u_ctxt), u, pos))
   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
   253           | desc (T :: Ts) (ft as ((tyenv, u_ctxt) , u, pos)) =
   254             case do_match ft of
   255               NONE =>
   256                 (case match_argT T u tyenv of
   257                   NONE => NONE
   258                 | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) ((tyenv', u_ctxt), u, pos)))
   259             | SOME ft => SOME ft
   260       in desc eta_expands ft end
   261 
   262     fun move_assms ctxt (ft: focusterm) =
   263       let
   264         fun f () = case try (ft_assm ctxt) ft of
   265             NONE => NONE
   266           | SOME ft' => SOME (ft', move_assms ctxt (ft_imp ctxt ft))
   267       in Seq.make f end
   268 
   269     fun apply_pat At = Seq.map (ft_judgment ctxt)
   270       | apply_pat In = Seq.maps (valid_match_points ctxt)
   271       | apply_pat Asm = Seq.maps (move_assms ctxt o ft_params ctxt)
   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 
   318     val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (the_list to)
   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 
   323 local
   324 
   325 fun rewrite_raw ctxt (pattern, to) thms ct =
   326   let
   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
   356     val matches = find_matches ctxt pattern' ((Vartab.empty, ctxt), Thm.term_of ct, I)
   357 
   358     val thms' = maps (prep_meta_eq ctxt) thms
   359 
   360     fun rewrite_conv insty ctxt bounds =
   361       CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) thms')
   362 
   363     fun distinct_prems th =
   364       case Seq.pull (distinct_subgoals_tac th) of
   365         NONE => th
   366       | SOME (th', _) => th'
   367 
   368     fun conv (((tyenv, _), _, position) : focusterm) =
   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)
   377 
   378 fun rewrite_export_tac ctxt (pat, pat_ctxt) thms =
   379   let
   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)
   387   in tac end
   388 
   389 fun rewrite_tac ctxt pat = rewrite_export_tac ctxt (pat, NONE)
   390 
   391 end
   392 
   393 val _ =
   394   Theory.setup
   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
   409           | append_default [For x, In] = [For x, Concl, In]
   410           | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
   411           | append_default ps = ps
   412 
   413       in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
   414 
   415     fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
   416       let
   417         val (r, toks') = scan toks
   418         val (r', context') = Context.map_proof_result (fn ctxt => f ctxt r) context
   419       in (r', (context', toks' : Token.T list)) end
   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 
   492             val ts = maps mk_free_constrs ps @ the_list to
   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 
   507       in ((pats', ths, (to', ctxt)), ctxt'') end
   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
   513       in context_lift scan prep_args end
   514   in
   515     Method.setup @{binding rewrite} (subst_parser >>
   516       (fn (pattern, inthms, (to, pat_ctxt)) => fn orig_ctxt =>
   517         SIMPLE_METHOD' (rewrite_export_tac orig_ctxt ((pattern, to), SOME pat_ctxt) inthms)))
   518       "single-step rewriting, allowing subterm selection via patterns."
   519   end
   520 end