# HG changeset patch
# User noschinl
# Date 1426683093 -3600
# Node ID 4ed50ebf5d3618717d0c28acc04e445b26efc11d
# Parent  f41a2f77ab1b84b1827d6f62d2dcc581bbe85a3b
added proof method rewrite

diff -r f41a2f77ab1b -r 4ed50ebf5d36 NEWS
--- a/NEWS	Tue Mar 17 17:45:03 2015 +0000
+++ b/NEWS	Wed Mar 18 13:51:33 2015 +0100
@@ -76,6 +76,9 @@
 
 *** HOL ***
 
+* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
+  single-step rewriting with subterm selection based on patterns.
+
 * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
   type, so in particular on "real" and "complex" uniformly.
   Minor INCOMPATIBILITY: type constraints may be needed.
diff -r f41a2f77ab1b -r 4ed50ebf5d36 src/HOL/Library/Rewrite.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Rewrite.thy	Wed Mar 18 13:51:33 2015 +0100
@@ -0,0 +1,17 @@
+theory Rewrite
+imports Main
+begin
+
+consts rewrite_HOLE :: "'a :: {}"
+notation rewrite_HOLE ("HOLE")
+notation rewrite_HOLE ("\<box>")
+
+lemma eta_expand:
+  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
+  by (rule reflexive)
+
+ML_file "cconv.ML"
+ML_file "rewrite.ML"
+setup Rewrite.setup
+
+end
diff -r f41a2f77ab1b -r 4ed50ebf5d36 src/HOL/Library/cconv.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/cconv.ML	Wed Mar 18 13:51:33 2015 +0100
@@ -0,0 +1,225 @@
+infix 1 then_cconv
+infix 0 else_cconv
+
+type cconv = conv
+
+signature BASIC_CCONV =
+sig
+  val then_cconv: cconv * cconv -> cconv
+  val else_cconv: cconv * cconv -> cconv
+  val CCONVERSION: cconv -> int -> tactic
+end
+
+signature CCONV =
+sig
+  include BASIC_CCONV
+  val no_cconv: cconv
+  val all_cconv: cconv
+  val first_cconv: cconv list -> cconv
+  val abs_cconv: (cterm * Proof.context -> cconv) -> Proof.context -> cconv
+  val combination_cconv: cconv -> cconv -> cconv
+  val comb_cconv: cconv -> cconv
+  val arg_cconv: cconv -> cconv
+  val fun_cconv: cconv -> cconv
+  val arg1_cconv: cconv -> cconv
+  val fun2_cconv: cconv -> cconv
+  val rewr_cconv: thm -> cconv
+  val rewrs_cconv: thm list -> cconv
+  val params_cconv: int -> (Proof.context -> cconv) -> Proof.context -> cconv
+  val prems_cconv: int -> cconv -> cconv
+  val concl_cconv: int -> cconv -> cconv
+  val fconv_rule: cconv -> thm -> thm
+  val gconv_rule: cconv -> int -> thm -> thm
+end
+
+structure CConv : CCONV =
+struct
+
+val concl_lhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_lhs
+val concl_rhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_rhs
+
+fun transitive th1 th2 = Drule.transitive_thm OF [th1, th2]
+
+val combination_thm =
+  let
+    val fg = @{cprop "f :: 'a :: {} \<Rightarrow> 'b :: {} \<equiv> g"}
+    val st = @{cprop "s :: 'a :: {} \<equiv> t"}
+    val thm = Thm.combination (Thm.assume fg) (Thm.assume st)
+      |> Thm.implies_intr st
+      |> Thm.implies_intr fg
+  in Drule.export_without_context thm end
+
+fun abstract_rule_thm n =
+  let
+    val eq = @{cprop "\<And>x :: 'a :: {}. (s :: 'a \<Rightarrow> 'b :: {}) x \<equiv> t x"}
+    val x = @{cterm "x :: 'a :: {}"}
+    val thm = eq
+      |> Thm.assume
+      |> Thm.forall_elim x
+      |> Thm.abstract_rule n x
+      |> Thm.implies_intr eq
+  in Drule.export_without_context thm end
+
+val no_cconv = Conv.no_conv
+val all_cconv = Conv.all_conv
+
+fun (cv1 else_cconv cv2) ct =
+  (cv1 ct
+    handle THM _ => cv2 ct
+      | CTERM _ => cv2 ct
+      | TERM _ => cv2 ct
+      | TYPE _ => cv2 ct)
+
+fun (cv1 then_cconv cv2) ct =
+  let
+    val eq1 = cv1 ct
+    val eq2 = cv2 (concl_rhs_of eq1)
+  in
+    if Thm.is_reflexive eq1 then eq2
+    else if Thm.is_reflexive eq2 then eq1
+    else transitive eq1 eq2
+  end
+
+fun first_cconv cvs = fold_rev (curry op else_cconv) cvs no_cconv
+
+fun rewr_cconv rule ct =
+  let
+    val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule
+    val lhs = concl_lhs_of rule1
+    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
+    val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
+                handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
+    val rule4 =
+      if concl_lhs_of rule3 aconvc ct then rule3
+      else let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
+           in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (concl_rhs_of rule3)) end
+  in
+    transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
+  end
+
+fun rewrs_cconv rules = first_cconv (map rewr_cconv rules)
+
+fun combination_cconv cv1 cv2 cterm =
+  let val (l, r) = Thm.dest_comb cterm
+  in combination_thm OF [cv1 l, cv2 r] end
+
+fun comb_cconv cv = combination_cconv cv cv
+
+fun fun_cconv conversion =
+  combination_cconv conversion all_cconv
+
+fun arg_cconv conversion =
+  combination_cconv all_cconv conversion
+
+fun abs_cconv cv ctxt ct =
+  (case Thm.term_of ct of
+     Abs (x, _, _) =>
+       let
+         (* Instantiate the rule properly and apply it to the eq theorem. *)
+         fun abstract_rule u v eq =
+           let
+             (* Take a variable v and an equality theorem of form:
+                  P1 Pure.imp ... Pure.imp Pn Pure.imp L v == R v
+                And build a term of form:
+                  !!v. (%x. L x) v == (%x. R x) v *)
+             fun mk_concl var eq =
+               let
+                 val certify = Thm.cterm_of ctxt
+                 fun abs term = (Term.lambda var term) $ var
+                 fun equals_cong f t =
+                   Logic.dest_equals t
+                   |> (fn (a, b) => (f a, f b))
+                   |> Logic.mk_equals
+               in
+                 Thm.concl_of eq
+                 |> equals_cong abs
+                 |> Logic.all var |> certify
+               end
+             val rule = abstract_rule_thm x
+             val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
+           in
+             (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq])
+             |> Drule.zero_var_indexes
+           end
+
+         (* Destruct the abstraction and apply the conversion. *)
+         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
+         val (v, ct') = Thm.dest_abs (SOME u) ct
+         val eq = cv (v, ctxt') ct'
+       in
+         if Thm.is_reflexive eq
+         then all_cconv ct
+         else abstract_rule u v eq
+       end
+   | _ => raise CTERM ("abs_cconv", [ct]))
+
+val arg1_cconv = fun_cconv o arg_cconv
+val fun2_cconv = fun_cconv o fun_cconv
+
+(* conversions on HHF rules *)
+
+(*rewrite B in !!x1 ... xn. B*)
+fun params_cconv n cv ctxt ct =
+  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
+  then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
+  else cv ctxt ct
+
+(* TODO: This code behaves not exactly like Conv.prems_cconv does.
+         Fix this! *)
+(*rewrite the A's in A1 Pure.imp ... Pure.imp An Pure.imp B*)
+fun prems_cconv 0 cv ct = cv ct
+  | prems_cconv n cv ct =
+      (case ct |> Thm.term_of of
+        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
+      | _ =>  cv ct)
+
+(*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
+fun concl_cconv 0 cv ct = cv ct
+  | concl_cconv n cv ct =
+      (case ct |> Thm.term_of of
+        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => arg_cconv (concl_cconv (n-1) cv) ct
+      | _ =>  cv ct)
+
+(*forward conversion, cf. FCONV_RULE in LCF*)
+fun fconv_rule cv th =
+  let
+    val eq = cv (Thm.cprop_of th)
+  in
+    if Thm.is_reflexive eq then th
+    else th COMP (Thm.permute_prems 0 (Thm.nprems_of eq) (eq RS Drule.equal_elim_rule1))
+  end
+
+(*goal conversion*)
+fun gconv_rule cv i th =
+  (case try (Thm.cprem_of th) i of
+    SOME ct =>
+      let
+        val eq = cv ct
+
+        (* Drule.with_subgoal assumes that there are no new premises generated
+           and thus rotates the premises wrongly. *)
+        fun with_subgoal i f thm =
+          let
+            val num_prems = Thm.nprems_of thm
+            val rotate_to_front = rotate_prems (i - 1)
+            fun rotate_back thm = rotate_prems (1 - i + num_prems - Thm.nprems_of thm) thm
+          in
+            thm |> rotate_to_front |> f |> rotate_back
+          end
+      in
+        if Thm.is_reflexive eq then th
+        else with_subgoal i (fconv_rule (arg1_cconv (K eq))) th
+      end
+  | NONE => raise THM ("gconv_rule", i, [th]))
+
+  (* Conditional conversions as tactics. *)
+fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
+  handle THM _ => Seq.empty
+       | CTERM _ => Seq.empty
+       | TERM _ => Seq.empty
+       | TYPE _ => Seq.empty
+
+end
+
+structure Basic_CConv: BASIC_CCONV = CConv
+open Basic_CConv
diff -r f41a2f77ab1b -r 4ed50ebf5d36 src/HOL/Library/rewrite.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/rewrite.ML	Wed Mar 18 13:51:33 2015 +0100
@@ -0,0 +1,479 @@
+(* Author: Christoph Traut, Lars Noschinski
+
+  This is a rewrite method supports subterm-selection based on patterns.
+
+  The patterns accepted by rewrite are of the following form:
+    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
+    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
+    <args>    ::= [<pattern>] ("to" <term>) <thms>
+
+  This syntax was clearly inspired by Gonthier's and Tassi's language of
+  patterns but has diverged significantly during its development.
+
+  We also allow introduction of identifiers for bound variables,
+  which can then be used to match arbitary subterms inside abstractions.
+*)
+
+signature REWRITE1 = sig
+  val setup : theory -> theory
+end
+
+structure Rewrite : REWRITE1 =
+struct
+
+datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
+
+fun map_term_pattern f (Term x) = f x
+  | map_term_pattern _ (For ss) = (For ss)
+  | map_term_pattern _ At = At
+  | map_term_pattern _ In = In
+  | map_term_pattern _ Concl = Concl
+  | map_term_pattern _ Asm = Asm
+
+
+exception NO_TO_MATCH
+
+fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq
+
+(* We rewrite subterms using rewrite conversions. These are conversions
+   that also take a context and a list of identifiers for bound variables
+   as parameters. *)
+type rewrite_conv = Proof.context -> (string * term) list -> conv
+
+(* To apply such a rewrite conversion to a subterm of our goal, we use
+   subterm positions, which are just functions that map a rewrite conversion,
+   working on the top level, to a new rewrite conversion, working on
+   a specific subterm.
+
+   During substitution, we are traversing the goal to find subterms that
+   we can rewrite. For each of these subterms, a subterm position is
+   created and later used in creating a conversion that we use to try and
+   rewrite this subterm. *)
+type subterm_position = rewrite_conv -> rewrite_conv
+
+(* A focusterm represents a subterm. It is a tuple (t, p), consisting
+  of the subterm t itself and its subterm position p. *)
+type focusterm = Type.tyenv * term * subterm_position
+
+val dummyN = Name.internal "__dummy"
+val holeN = Name.internal "_hole"
+
+fun prep_meta_eq ctxt =
+  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
+
+
+(* rewrite conversions *)
+
+fun abs_rewr_cconv ident : subterm_position =
+  let
+    fun add_ident NONE _ l = l
+      | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
+    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
+  in inner end
+val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
+val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
+
+
+(* focus terms *)
+
+fun ft_abs ctxt (s,T) (tyenv, u, pos) =
+  case try (fastype_of #> dest_funT) u of
+    NONE => raise TERM ("ft_abs: no function type", [u])
+  | SOME (U, _) =>
+  let
+    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
+    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
+    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
+    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
+    val (u', pos') =
+      case u of
+        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
+      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
+  in (tyenv', u', pos') end
+  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
+
+fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
+  | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
+  | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
+
+fun ft_arg _ (tyenv, _ $ r, pos) = (tyenv, r, pos o arg_rewr_cconv)
+  | ft_arg ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg ctxt o ft_abs ctxt (NONE, T)) ft
+  | ft_arg _ (_, t, _) = raise TERM ("ft_arg", [t])
+
+(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
+fun ft_params ctxt (ft as (_, t, _) : focusterm) =
+  case t of
+    Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) =>
+      (ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft
+  | Const (@{const_name "Pure.all"}, _) =>
+      (ft_params ctxt o ft_arg ctxt) ft
+  | _ => ft
+
+fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) =
+    let
+      val def_U = T |> dest_funT |> fst |> dest_funT |> fst
+      val ident' = apsnd (the_default (def_U)) ident
+    in (ft_abs ctxt ident' o ft_arg ctxt) ft end
+  | ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t])
+
+fun ft_for ctxt idents (ft as (_, t, _) : focusterm) =
+  let
+    fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) =
+        let
+         val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
+        in
+          case rev_idents' of
+            [] => ([], desc o ft_all ctxt (NONE, NONE))
+          | (x :: xs) => (xs , desc o ft_all ctxt x)
+        end
+      | f rev_idents _ = (rev_idents, I)
+  in case f (rev idents) t of
+      ([], ft') => SOME (ft' ft)
+    | _ => NONE
+  end
+
+fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
+  case t of
+    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt) ft
+  | _ => ft
+
+fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
+  case t of
+    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt o ft_fun ctxt) ft
+  | _ => raise TERM ("ft_assm", [t])
+
+fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
+  if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
+  then ft_arg ctxt ft
+  else ft
+
+
+(* Return a lazy sequenze of all subterms of the focusterm for which
+   the condition holds. *)
+fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
+  let
+    val recurse = find_subterms ctxt condition
+    val recursive_matches = case t of
+        _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
+      | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
+      | _ => Seq.empty
+  in
+    (* If the condition is met, then the current focusterm is part of the
+       sequence of results. Otherwise, only the results of the recursive
+       application are. *)
+    if condition ft
+    then Seq.cons ft recursive_matches
+    else recursive_matches
+  end
+
+(* Find all subterms that might be a valid point to apply a rule. *)
+fun valid_match_points ctxt =
+  let
+    fun is_valid (l $ _) = is_valid l
+      | is_valid (Abs (_, _, a)) = is_valid a
+      | is_valid (Var _) = false
+      | is_valid (Bound _) = false
+      | is_valid _ = true
+  in
+    find_subterms ctxt (#2 #> is_valid )
+  end
+
+fun is_hole (Var ((name, _), _)) = (name = holeN)
+  | is_hole _ = false
+
+fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true
+  | is_hole_const _ = false
+
+val hole_syntax =
+  let
+    (* Modified variant of Term.replace_hole *)
+    fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i =
+          (list_comb (Var ((holeN, i), Ts ---> T), map_range Bound (length Ts)), i + 1)
+      | replace_hole Ts (Abs (x, T, t)) i =
+          let val (t', i') = replace_hole (T :: Ts) t i
+          in (Abs (x, T, t'), i') end
+      | replace_hole Ts (t $ u) i =
+          let
+            val (t', i') = replace_hole Ts t i
+            val (u', i'') = replace_hole Ts u i'
+          in (t' $ u', i'') end
+      | replace_hole _ a i = (a, i)
+    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
+  in
+    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
+    #> Proof_Context.set_mode Proof_Context.mode_pattern
+  end
+
+(* Find a subterm of the focusterm matching the pattern. *)
+fun find_matches ctxt pattern_list =
+  let
+    fun move_term ctxt (t, off) (ft : focusterm) =
+      let
+        val thy = Proof_Context.theory_of ctxt
+
+        val eta_expands =
+          let val (_, ts) = strip_comb t
+          in map fastype_of (snd (take_suffix is_Var ts)) end
+
+        fun do_match (tyenv, u, pos) =
+          case try (Pattern.match thy (t,u)) (tyenv, Vartab.empty) of
+            NONE => NONE
+          | SOME (tyenv', _) => SOME (off (tyenv', u, pos))
+
+        fun match_argT T u =
+          let val (U, _) = dest_funT (fastype_of u)
+          in try (Sign.typ_match thy (T,U)) end
+          handle TYPE _ => K NONE
+
+        fun desc [] ft = do_match ft
+          | desc (T :: Ts) (ft as (tyenv , u, pos)) =
+            case do_match ft of
+              NONE =>
+                (case match_argT T u tyenv of
+                  NONE => NONE
+                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) (tyenv', u, pos)))
+            | SOME ft => SOME ft
+      in desc eta_expands ft end
+
+    fun seq_unfold f ft =
+      case f ft of
+        NONE => Seq.empty
+      | SOME ft' => Seq.cons ft' (seq_unfold f ft')
+
+    fun apply_pat At = Seq.map (ft_judgment ctxt)
+      | apply_pat In = Seq.maps (valid_match_points ctxt)
+      | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt)
+      | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
+      | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
+      | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
+
+    fun apply_pats ft = ft
+      |> Seq.single
+      |> fold apply_pat pattern_list
+
+  in
+    apply_pats
+  end
+
+fun instantiate_normalize_env ctxt env thm =
+  let
+    fun certs f = map (apply2 (f ctxt))
+    val prop = Thm.prop_of thm
+    val norm_type = Envir.norm_type o Envir.type_env
+    val insts = Term.add_vars prop []
+      |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
+      |> certs Thm.cterm_of
+    val tyinsts = Term.add_tvars prop []
+      |> map (fn x => (TVar x, norm_type env (TVar x)))
+      |> certs Thm.ctyp_of
+  in Drule.instantiate_normalize (tyinsts, insts) thm end
+
+fun unify_with_rhs context to env thm =
+  let
+    val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
+    val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
+      handle Pattern.Unif => raise NO_TO_MATCH
+  in env' end
+
+fun inst_thm_to _ (NONE, _) thm = thm
+  | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
+      instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
+
+fun inst_thm ctxt idents (to, tyenv) thm =
+  let
+    (* Replace any identifiers with their corresponding bound variables. *)
+    val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
+    val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
+    val replace_idents =
+      let
+        fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
+          | subst _ t = t
+      in Term.map_aterms (subst idents) end
+
+    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (map_filter I [to])
+    val thm' = Thm.incr_indexes (maxidx + 1) thm
+  in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end
+  handle NO_TO_MATCH => NONE
+
+(* Rewrite in subgoal i. *)
+fun rewrite_goal_with_thm ctxt (pattern, (to, orig_ctxt)) rules = SUBGOAL (fn (t,i) =>
+  let
+    val matches = find_matches ctxt pattern (Vartab.empty, t, I)
+
+    fun rewrite_conv insty ctxt bounds =
+      CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) rules)
+
+    val export = singleton (Proof_Context.export ctxt orig_ctxt)
+
+    fun distinct_prems th =
+      case Seq.pull (distinct_subgoals_tac th) of
+        NONE => th
+      | SOME (th', _) => th'
+
+    fun tac (tyenv, _, position) = CCONVERSION
+      (distinct_prems o export o position (rewrite_conv (to, tyenv)) ctxt []) i
+  in
+    SEQ_CONCAT (Seq.map tac matches)
+  end)
+
+fun rewrite_tac ctxt pattern thms =
+  let
+    val thms' = maps (prep_meta_eq ctxt) thms
+    val tac = rewrite_goal_with_thm ctxt pattern thms'
+  in tac end
+
+val setup =
+  let
+
+    fun mk_fix s = (Binding.name s, NONE, NoSyn)
+
+    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
+      let
+        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
+        val atom =  (Args.$$$ "asm" >> K Asm) ||
+          (Args.$$$ "concl" >> K Concl) ||
+          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
+          (Parse.term >> Term)
+        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
+
+        fun append_default [] = [Concl, In]
+          | append_default (ps as Term _ :: _) = Concl :: In :: ps
+          | append_default ps = ps
+
+      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
+
+    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
+      let
+        val (r, toks') = scan toks
+        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
+      in (r', (ctxt', toks' : Token.T list))end
+
+    fun read_fixes fixes ctxt =
+      let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
+      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
+
+    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
+      let
+
+        fun add_constrs ctxt n (Abs (x, T, t)) =
+            let
+              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
+            in
+              (case add_constrs ctxt' (n+1) t of
+                NONE => NONE
+              | SOME ((ctxt'', n', xs), t') =>
+                  let
+                    val U = Type_Infer.mk_param n []
+                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
+                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
+            end
+          | add_constrs ctxt n (l $ r) =
+            (case add_constrs ctxt n l of
+              SOME (c, l') => SOME (c, l' $ r)
+            | NONE =>
+              (case add_constrs ctxt n r of
+                SOME (c, r') => SOME (c, l $ r')
+              | NONE => NONE))
+          | add_constrs ctxt n t =
+            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
+
+        fun prep (Term s) (n, ctxt) =
+            let
+              val t = Syntax.parse_term ctxt s
+              val ((ctxt', n', bs), t') =
+                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
+            in (Term (t', bs), (n', ctxt')) end
+          | prep (For ss) (n, ctxt) =
+            let val (ns, ctxt') = read_fixes ss ctxt
+            in (For ns, (n, ctxt')) end
+          | prep At (n,ctxt) = (At, (n, ctxt))
+          | prep In (n,ctxt) = (In, (n, ctxt))
+          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
+          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
+
+        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
+
+      in (xs, ctxt') end
+
+    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
+      let
+
+        fun interpret_term_patterns ctxt =
+          let
+
+            fun descend_hole fixes (Abs (_, _, t)) =
+                (case descend_hole fixes t of
+                  NONE => NONE
+                | SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix))
+                | SOME ([], _) => raise Match (* XXX -- check phases modified binding *))
+              | descend_hole fixes (t as l $ r) =
+                let val (f, _) = strip_comb t
+                in
+                  if is_hole f
+                  then SOME (fixes, I)
+                  else
+                    (case descend_hole fixes l of
+                      SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt)
+                    | NONE =>
+                      (case descend_hole fixes r of
+                        SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt)
+                      | NONE => NONE))
+                end
+              | descend_hole fixes t =
+                if is_hole t then SOME (fixes, I) else NONE
+
+            fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t)
+
+          in map (map_term_pattern f) end
+
+        fun check_terms ctxt ps to =
+          let
+            fun safe_chop (0: int) xs = ([], xs)
+              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
+              | safe_chop _ _ = raise Match
+
+            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
+                let val (cs', ts') = safe_chop (length cs) ts
+                in (Term (t, map dest_Free cs'), ts') end
+              | reinsert_pat _ (Term _) [] = raise Match
+              | reinsert_pat ctxt (For ss) ts =
+                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
+                in (For fixes, ts) end
+              | reinsert_pat _ At ts = (At, ts)
+              | reinsert_pat _ In ts = (In, ts)
+              | reinsert_pat _ Concl ts = (Concl, ts)
+              | reinsert_pat _ Asm ts = (Asm, ts)
+
+            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
+            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
+              | mk_free_constrs _ = []
+
+            val ts = maps mk_free_constrs ps @ map_filter I [to]
+              |> Syntax.check_terms (hole_syntax ctxt)
+            val ctxt' = fold Variable.declare_term ts ctxt
+            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
+              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
+            val _ = case ts' of (_ :: _) => raise Match | [] => ()
+          in ((ps', to'), ctxt') end
+
+        val (pats, ctxt') = prep_pats ctxt raw_pats
+
+        val ths = Attrib.eval_thms ctxt' raw_ths
+        val to = Option.map (Syntax.parse_term ctxt') raw_to
+
+        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
+        val pats'' = interpret_term_patterns ctxt'' pats'
+
+      in ((pats'', ths, (to', ctxt)), ctxt'') end
+
+    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
+
+    val subst_parser =
+      let val scan = raw_pattern -- to_parser -- Parse.xthms1
+      in ctxt_lift scan prep_args end
+  in
+    Method.setup @{binding rewrite} (subst_parser >>
+      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
+      "single-step rewriting, allowing subterm selection via patterns."
+  end
+end
diff -r f41a2f77ab1b -r 4ed50ebf5d36 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Mar 17 17:45:03 2015 +0000
+++ b/src/HOL/ROOT	Wed Mar 18 13:51:33 2015 +0100
@@ -548,7 +548,7 @@
     NatSum
     ThreeDivides
     Cubic_Quartic
-	Pythagoras
+    Pythagoras
     Intuitionistic
     CTL
     Arith_Examples
@@ -591,6 +591,7 @@
     SVC_Oracle
     Simps_Case_Conv_Examples
     ML
+    Rewrite_Examples
     SAT_Examples
     SOS
     SOS_Cert
diff -r f41a2f77ab1b -r 4ed50ebf5d36 src/HOL/ex/Rewrite_Examples.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Rewrite_Examples.thy	Wed Mar 18 13:51:33 2015 +0100
@@ -0,0 +1,172 @@
+theory Rewrite_Examples
+imports Main "~~/src/HOL/Library/Rewrite"
+begin
+
+section \<open>The rewrite Proof Method by Example\<close>
+
+(* This file is intended to give an overview over
+   the features of the pattern-based rewrite proof method.
+
+   See also https://www21.in.tum.de/~noschinl/Pattern-2014/
+*)
+
+lemma
+  fixes a::int and b::int and c::int
+  assumes "P (b + a)"
+  shows "P (a + b)"
+by (rewrite at "a + b" add.commute)
+   (rule assms)
+
+(* Selecting a specific subterm in a large, ambiguous term. *)
+lemma
+  fixes a b c :: int
+  assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
+  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+  by (rewrite in "f _ + f \<box> = _" diff_self) fact
+
+lemma
+  fixes a b c :: int
+  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
+  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+  by (rewrite at "f (_ + \<box>) + f _ = _" diff_self) fact
+
+lemma
+  fixes a b c :: int
+  assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
+  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+  by (rewrite in "f (\<box> + _) + _ = _" diff_self) fact
+
+lemma
+  fixes a b c :: int
+  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
+  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
+  by (rewrite in "f (_ + \<box>) + _ = _" diff_self) fact
+
+lemma
+  fixes x y :: nat
+  shows"x + y > c \<Longrightarrow> y + x > c"
+  by (rewrite at "\<box> > c" add.commute) assumption
+
+(* We can also rewrite in the assumptions.  *)
+lemma
+  fixes x y :: nat
+  assumes "y + x > c \<Longrightarrow> y + x > c"
+  shows   "x + y > c \<Longrightarrow> y + x > c"
+  by (rewrite in asm add.commute) fact
+
+lemma
+  fixes x y :: nat
+  assumes "y + x > c \<Longrightarrow> y + x > c"
+  shows   "x + y > c \<Longrightarrow> y + x > c"
+  by (rewrite in "x + y > c" at asm add.commute) fact
+
+lemma
+  fixes x y :: nat
+  assumes "y + x > c \<Longrightarrow> y + x > c"
+  shows   "x + y > c \<Longrightarrow> y + x > c"
+  by (rewrite at "\<box> > c" at asm  add.commute) fact
+
+lemma
+  assumes "P {x::int. y + 1 = 1 + x}"
+  shows   "P {x::int. y + 1 = x + 1}"
+  by (rewrite at "x+1" in "{x::int. \<box> }" add.commute) fact
+
+lemma
+  assumes "P {x::int. y + 1 = 1 + x}"
+  shows   "P {x::int. y + 1 = x + 1}"
+  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<box> }" add.commute)
+   fact
+
+lemma
+  assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
+  shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
+  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<box>)" add.commute) fact
+
+
+(* Rewriting with conditional rewriting rules works just as well. *)
+lemma test_theorem:
+  fixes x :: nat
+  shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
+  by (rule Orderings.order_antisym)
+
+lemma
+fixes f :: "nat \<Rightarrow> nat"
+  assumes "f x \<le> 0" "f x \<ge> 0"
+  shows "f x = 0"
+  apply (rewrite at "f x" to "0" test_theorem)
+  apply fact
+  apply fact
+  apply (rule refl)
+done
+
+(*
+   Instantiation.
+
+   Since all rewriting is now done via conversions,
+   instantiation becomes fairly easy to do.
+*)
+
+(* We first introduce a function f and an extended
+   version of f that is annotated with an invariant. *)
+fun f :: "nat \<Rightarrow> nat" where "f n = n"
+definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
+
+lemma annotate_f: "f = f_inv I"
+  by (simp add: f_inv_def fun_eq_iff)
+
+(* We have a lemma with a bound variable n, and
+   want to add an invariant to f. *)
+lemma
+  assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
+  shows "P (\<lambda>n. f n + 1) = x"
+  by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
+
+(* We can also add an invariant that contains the variable n bound in the outer context.
+   For this, we need to bind this variable to an identifier. *)
+lemma
+  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
+  shows "P (\<lambda>n. f n + 1) = x"
+  by (rewrite in "\<lambda>n. \<box>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
+
+(* Any identifier will work *)
+lemma
+  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
+  shows "P (\<lambda>n. f n + 1) = x"
+  by (rewrite in "\<lambda>abc. \<box>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
+
+(* The "for" keyword. *)
+lemma
+  assumes "P (2 + 1)"
+  shows "\<And>x y. P (1 + 2 :: nat)"
+by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
+
+lemma
+  assumes "\<And>x y. P (y + x)"
+  shows "\<And>x y. P (x + y :: nat)"
+by (rewrite in "P (x + _)" at for (x y) add.commute) fact
+
+lemma
+  assumes "\<And>x y z. y + x + z = z + y + (x::int)"
+  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
+
+lemma
+  assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
+  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
+
+lemma
+  assumes "\<And>x y z. x + y + z = y + z + (x::int)"
+  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
+by (rewrite at "\<box> + _" at "_ = \<box>" in concl at for () add.commute) fact
+
+(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
+lemma
+  assumes "(\<And>(x::int). x < 1 + x)"
+  and     "(x::int) + 1 > x"
+  shows   "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
+by (rewrite at "x + 1" in for (x) at asm add.commute)
+   (rule assms)
+
+end
+