Merge
authorpaulson <lp15@cam.ac.uk>
Wed Mar 18 14:28:40 2015 +0000 (2015-03-18)
changeset 59743d8fb00487c4d
parent 59742 1441ca50f047
parent 59739 4ed50ebf5d36
child 59744 37c3ffe95b8a
Merge
src/HOL/ROOT
     1.1 --- a/NEWS	Wed Mar 18 14:14:07 2015 +0000
     1.2 +++ b/NEWS	Wed Mar 18 14:28:40 2015 +0000
     1.3 @@ -76,6 +76,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* New proof method "rewrite" (in ~~/src/HOL/Library/Rewrite) for
     1.8 +  single-step rewriting with subterm selection based on patterns.
     1.9 +
    1.10  * the functions "sin" and "cos" are now defined for any "'{real_normed_algebra_1,banach}"
    1.11    type, so in particular on "real" and "complex" uniformly.
    1.12    Minor INCOMPATIBILITY: type constraints may be needed.
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/Rewrite.thy	Wed Mar 18 14:28:40 2015 +0000
     2.3 @@ -0,0 +1,17 @@
     2.4 +theory Rewrite
     2.5 +imports Main
     2.6 +begin
     2.7 +
     2.8 +consts rewrite_HOLE :: "'a :: {}"
     2.9 +notation rewrite_HOLE ("HOLE")
    2.10 +notation rewrite_HOLE ("\<box>")
    2.11 +
    2.12 +lemma eta_expand:
    2.13 +  fixes f :: "'a :: {} \<Rightarrow> 'b :: {}" shows "f \<equiv> (\<lambda>x. f x)"
    2.14 +  by (rule reflexive)
    2.15 +
    2.16 +ML_file "cconv.ML"
    2.17 +ML_file "rewrite.ML"
    2.18 +setup Rewrite.setup
    2.19 +
    2.20 +end
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/cconv.ML	Wed Mar 18 14:28:40 2015 +0000
     3.3 @@ -0,0 +1,225 @@
     3.4 +infix 1 then_cconv
     3.5 +infix 0 else_cconv
     3.6 +
     3.7 +type cconv = conv
     3.8 +
     3.9 +signature BASIC_CCONV =
    3.10 +sig
    3.11 +  val then_cconv: cconv * cconv -> cconv
    3.12 +  val else_cconv: cconv * cconv -> cconv
    3.13 +  val CCONVERSION: cconv -> int -> tactic
    3.14 +end
    3.15 +
    3.16 +signature CCONV =
    3.17 +sig
    3.18 +  include BASIC_CCONV
    3.19 +  val no_cconv: cconv
    3.20 +  val all_cconv: cconv
    3.21 +  val first_cconv: cconv list -> cconv
    3.22 +  val abs_cconv: (cterm * Proof.context -> cconv) -> Proof.context -> cconv
    3.23 +  val combination_cconv: cconv -> cconv -> cconv
    3.24 +  val comb_cconv: cconv -> cconv
    3.25 +  val arg_cconv: cconv -> cconv
    3.26 +  val fun_cconv: cconv -> cconv
    3.27 +  val arg1_cconv: cconv -> cconv
    3.28 +  val fun2_cconv: cconv -> cconv
    3.29 +  val rewr_cconv: thm -> cconv
    3.30 +  val rewrs_cconv: thm list -> cconv
    3.31 +  val params_cconv: int -> (Proof.context -> cconv) -> Proof.context -> cconv
    3.32 +  val prems_cconv: int -> cconv -> cconv
    3.33 +  val concl_cconv: int -> cconv -> cconv
    3.34 +  val fconv_rule: cconv -> thm -> thm
    3.35 +  val gconv_rule: cconv -> int -> thm -> thm
    3.36 +end
    3.37 +
    3.38 +structure CConv : CCONV =
    3.39 +struct
    3.40 +
    3.41 +val concl_lhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_lhs
    3.42 +val concl_rhs_of = Thm.cprop_of #> Drule.strip_imp_concl #> Thm.dest_equals_rhs
    3.43 +
    3.44 +fun transitive th1 th2 = Drule.transitive_thm OF [th1, th2]
    3.45 +
    3.46 +val combination_thm =
    3.47 +  let
    3.48 +    val fg = @{cprop "f :: 'a :: {} \<Rightarrow> 'b :: {} \<equiv> g"}
    3.49 +    val st = @{cprop "s :: 'a :: {} \<equiv> t"}
    3.50 +    val thm = Thm.combination (Thm.assume fg) (Thm.assume st)
    3.51 +      |> Thm.implies_intr st
    3.52 +      |> Thm.implies_intr fg
    3.53 +  in Drule.export_without_context thm end
    3.54 +
    3.55 +fun abstract_rule_thm n =
    3.56 +  let
    3.57 +    val eq = @{cprop "\<And>x :: 'a :: {}. (s :: 'a \<Rightarrow> 'b :: {}) x \<equiv> t x"}
    3.58 +    val x = @{cterm "x :: 'a :: {}"}
    3.59 +    val thm = eq
    3.60 +      |> Thm.assume
    3.61 +      |> Thm.forall_elim x
    3.62 +      |> Thm.abstract_rule n x
    3.63 +      |> Thm.implies_intr eq
    3.64 +  in Drule.export_without_context thm end
    3.65 +
    3.66 +val no_cconv = Conv.no_conv
    3.67 +val all_cconv = Conv.all_conv
    3.68 +
    3.69 +fun (cv1 else_cconv cv2) ct =
    3.70 +  (cv1 ct
    3.71 +    handle THM _ => cv2 ct
    3.72 +      | CTERM _ => cv2 ct
    3.73 +      | TERM _ => cv2 ct
    3.74 +      | TYPE _ => cv2 ct)
    3.75 +
    3.76 +fun (cv1 then_cconv cv2) ct =
    3.77 +  let
    3.78 +    val eq1 = cv1 ct
    3.79 +    val eq2 = cv2 (concl_rhs_of eq1)
    3.80 +  in
    3.81 +    if Thm.is_reflexive eq1 then eq2
    3.82 +    else if Thm.is_reflexive eq2 then eq1
    3.83 +    else transitive eq1 eq2
    3.84 +  end
    3.85 +
    3.86 +fun first_cconv cvs = fold_rev (curry op else_cconv) cvs no_cconv
    3.87 +
    3.88 +fun rewr_cconv rule ct =
    3.89 +  let
    3.90 +    val rule1 = Thm.incr_indexes (Thm.maxidx_of_cterm ct + 1) rule
    3.91 +    val lhs = concl_lhs_of rule1
    3.92 +    val rule2 = Thm.rename_boundvars (Thm.term_of lhs) (Thm.term_of ct) rule1
    3.93 +    val rule3 = Thm.instantiate (Thm.match (lhs, ct)) rule2
    3.94 +                handle Pattern.MATCH => raise CTERM ("rewr_cconv", [lhs, ct])
    3.95 +    val rule4 =
    3.96 +      if concl_lhs_of rule3 aconvc ct then rule3
    3.97 +      else let val ceq = Thm.dest_fun2 (Thm.cprop_of rule3)
    3.98 +           in rule3 COMP Thm.trivial (Thm.mk_binop ceq ct (concl_rhs_of rule3)) end
    3.99 +  in
   3.100 +    transitive rule4 (Thm.beta_conversion true (concl_rhs_of rule4))
   3.101 +  end
   3.102 +
   3.103 +fun rewrs_cconv rules = first_cconv (map rewr_cconv rules)
   3.104 +
   3.105 +fun combination_cconv cv1 cv2 cterm =
   3.106 +  let val (l, r) = Thm.dest_comb cterm
   3.107 +  in combination_thm OF [cv1 l, cv2 r] end
   3.108 +
   3.109 +fun comb_cconv cv = combination_cconv cv cv
   3.110 +
   3.111 +fun fun_cconv conversion =
   3.112 +  combination_cconv conversion all_cconv
   3.113 +
   3.114 +fun arg_cconv conversion =
   3.115 +  combination_cconv all_cconv conversion
   3.116 +
   3.117 +fun abs_cconv cv ctxt ct =
   3.118 +  (case Thm.term_of ct of
   3.119 +     Abs (x, _, _) =>
   3.120 +       let
   3.121 +         (* Instantiate the rule properly and apply it to the eq theorem. *)
   3.122 +         fun abstract_rule u v eq =
   3.123 +           let
   3.124 +             (* Take a variable v and an equality theorem of form:
   3.125 +                  P1 Pure.imp ... Pure.imp Pn Pure.imp L v == R v
   3.126 +                And build a term of form:
   3.127 +                  !!v. (%x. L x) v == (%x. R x) v *)
   3.128 +             fun mk_concl var eq =
   3.129 +               let
   3.130 +                 val certify = Thm.cterm_of ctxt
   3.131 +                 fun abs term = (Term.lambda var term) $ var
   3.132 +                 fun equals_cong f t =
   3.133 +                   Logic.dest_equals t
   3.134 +                   |> (fn (a, b) => (f a, f b))
   3.135 +                   |> Logic.mk_equals
   3.136 +               in
   3.137 +                 Thm.concl_of eq
   3.138 +                 |> equals_cong abs
   3.139 +                 |> Logic.all var |> certify
   3.140 +               end
   3.141 +             val rule = abstract_rule_thm x
   3.142 +             val inst = Thm.match (Drule.cprems_of rule |> hd, mk_concl (Thm.term_of v) eq)
   3.143 +           in
   3.144 +             (Drule.instantiate_normalize inst rule OF [Drule.generalize ([], [u]) eq])
   3.145 +             |> Drule.zero_var_indexes
   3.146 +           end
   3.147 +
   3.148 +         (* Destruct the abstraction and apply the conversion. *)
   3.149 +         val (u, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
   3.150 +         val (v, ct') = Thm.dest_abs (SOME u) ct
   3.151 +         val eq = cv (v, ctxt') ct'
   3.152 +       in
   3.153 +         if Thm.is_reflexive eq
   3.154 +         then all_cconv ct
   3.155 +         else abstract_rule u v eq
   3.156 +       end
   3.157 +   | _ => raise CTERM ("abs_cconv", [ct]))
   3.158 +
   3.159 +val arg1_cconv = fun_cconv o arg_cconv
   3.160 +val fun2_cconv = fun_cconv o fun_cconv
   3.161 +
   3.162 +(* conversions on HHF rules *)
   3.163 +
   3.164 +(*rewrite B in !!x1 ... xn. B*)
   3.165 +fun params_cconv n cv ctxt ct =
   3.166 +  if n <> 0 andalso Logic.is_all (Thm.term_of ct)
   3.167 +  then arg_cconv (abs_cconv (params_cconv (n - 1) cv o #2) ctxt) ct
   3.168 +  else cv ctxt ct
   3.169 +
   3.170 +(* TODO: This code behaves not exactly like Conv.prems_cconv does.
   3.171 +         Fix this! *)
   3.172 +(*rewrite the A's in A1 Pure.imp ... Pure.imp An Pure.imp B*)
   3.173 +fun prems_cconv 0 cv ct = cv ct
   3.174 +  | prems_cconv n cv ct =
   3.175 +      (case ct |> Thm.term_of of
   3.176 +        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => ((if n = 1 then fun_cconv else I) o arg_cconv) (prems_cconv (n-1) cv) ct
   3.177 +      | _ =>  cv ct)
   3.178 +
   3.179 +(*rewrite B in A1 Pure.imp ... Pure.imp An Pure.imp B*)
   3.180 +fun concl_cconv 0 cv ct = cv ct
   3.181 +  | concl_cconv n cv ct =
   3.182 +      (case ct |> Thm.term_of of
   3.183 +        (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => arg_cconv (concl_cconv (n-1) cv) ct
   3.184 +      | _ =>  cv ct)
   3.185 +
   3.186 +(*forward conversion, cf. FCONV_RULE in LCF*)
   3.187 +fun fconv_rule cv th =
   3.188 +  let
   3.189 +    val eq = cv (Thm.cprop_of th)
   3.190 +  in
   3.191 +    if Thm.is_reflexive eq then th
   3.192 +    else th COMP (Thm.permute_prems 0 (Thm.nprems_of eq) (eq RS Drule.equal_elim_rule1))
   3.193 +  end
   3.194 +
   3.195 +(*goal conversion*)
   3.196 +fun gconv_rule cv i th =
   3.197 +  (case try (Thm.cprem_of th) i of
   3.198 +    SOME ct =>
   3.199 +      let
   3.200 +        val eq = cv ct
   3.201 +
   3.202 +        (* Drule.with_subgoal assumes that there are no new premises generated
   3.203 +           and thus rotates the premises wrongly. *)
   3.204 +        fun with_subgoal i f thm =
   3.205 +          let
   3.206 +            val num_prems = Thm.nprems_of thm
   3.207 +            val rotate_to_front = rotate_prems (i - 1)
   3.208 +            fun rotate_back thm = rotate_prems (1 - i + num_prems - Thm.nprems_of thm) thm
   3.209 +          in
   3.210 +            thm |> rotate_to_front |> f |> rotate_back
   3.211 +          end
   3.212 +      in
   3.213 +        if Thm.is_reflexive eq then th
   3.214 +        else with_subgoal i (fconv_rule (arg1_cconv (K eq))) th
   3.215 +      end
   3.216 +  | NONE => raise THM ("gconv_rule", i, [th]))
   3.217 +
   3.218 +  (* Conditional conversions as tactics. *)
   3.219 +fun CCONVERSION cv i st = Seq.single (gconv_rule cv i st)
   3.220 +  handle THM _ => Seq.empty
   3.221 +       | CTERM _ => Seq.empty
   3.222 +       | TERM _ => Seq.empty
   3.223 +       | TYPE _ => Seq.empty
   3.224 +
   3.225 +end
   3.226 +
   3.227 +structure Basic_CConv: BASIC_CCONV = CConv
   3.228 +open Basic_CConv
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/rewrite.ML	Wed Mar 18 14:28:40 2015 +0000
     4.3 @@ -0,0 +1,479 @@
     4.4 +(* Author: Christoph Traut, Lars Noschinski
     4.5 +
     4.6 +  This is a rewrite method supports subterm-selection based on patterns.
     4.7 +
     4.8 +  The patterns accepted by rewrite are of the following form:
     4.9 +    <atom>    ::= <term> | "concl" | "asm" | "for" "(" <names> ")"
    4.10 +    <pattern> ::= (in <atom> | at <atom>) [<pattern>]
    4.11 +    <args>    ::= [<pattern>] ("to" <term>) <thms>
    4.12 +
    4.13 +  This syntax was clearly inspired by Gonthier's and Tassi's language of
    4.14 +  patterns but has diverged significantly during its development.
    4.15 +
    4.16 +  We also allow introduction of identifiers for bound variables,
    4.17 +  which can then be used to match arbitary subterms inside abstractions.
    4.18 +*)
    4.19 +
    4.20 +signature REWRITE1 = sig
    4.21 +  val setup : theory -> theory
    4.22 +end
    4.23 +
    4.24 +structure Rewrite : REWRITE1 =
    4.25 +struct
    4.26 +
    4.27 +datatype ('a, 'b) pattern = At | In | Term of 'a | Concl | Asm | For of 'b list
    4.28 +
    4.29 +fun map_term_pattern f (Term x) = f x
    4.30 +  | map_term_pattern _ (For ss) = (For ss)
    4.31 +  | map_term_pattern _ At = At
    4.32 +  | map_term_pattern _ In = In
    4.33 +  | map_term_pattern _ Concl = Concl
    4.34 +  | map_term_pattern _ Asm = Asm
    4.35 +
    4.36 +
    4.37 +exception NO_TO_MATCH
    4.38 +
    4.39 +fun SEQ_CONCAT (tacq : tactic Seq.seq) : tactic = fn st => Seq.maps (fn tac => tac st) tacq
    4.40 +
    4.41 +(* We rewrite subterms using rewrite conversions. These are conversions
    4.42 +   that also take a context and a list of identifiers for bound variables
    4.43 +   as parameters. *)
    4.44 +type rewrite_conv = Proof.context -> (string * term) list -> conv
    4.45 +
    4.46 +(* To apply such a rewrite conversion to a subterm of our goal, we use
    4.47 +   subterm positions, which are just functions that map a rewrite conversion,
    4.48 +   working on the top level, to a new rewrite conversion, working on
    4.49 +   a specific subterm.
    4.50 +
    4.51 +   During substitution, we are traversing the goal to find subterms that
    4.52 +   we can rewrite. For each of these subterms, a subterm position is
    4.53 +   created and later used in creating a conversion that we use to try and
    4.54 +   rewrite this subterm. *)
    4.55 +type subterm_position = rewrite_conv -> rewrite_conv
    4.56 +
    4.57 +(* A focusterm represents a subterm. It is a tuple (t, p), consisting
    4.58 +  of the subterm t itself and its subterm position p. *)
    4.59 +type focusterm = Type.tyenv * term * subterm_position
    4.60 +
    4.61 +val dummyN = Name.internal "__dummy"
    4.62 +val holeN = Name.internal "_hole"
    4.63 +
    4.64 +fun prep_meta_eq ctxt =
    4.65 +  Simplifier.mksimps ctxt #> map Drule.zero_var_indexes
    4.66 +
    4.67 +
    4.68 +(* rewrite conversions *)
    4.69 +
    4.70 +fun abs_rewr_cconv ident : subterm_position =
    4.71 +  let
    4.72 +    fun add_ident NONE _ l = l
    4.73 +      | add_ident (SOME name) ct l = (name, Thm.term_of ct) :: l
    4.74 +    fun inner rewr ctxt idents = CConv.abs_cconv (fn (ct, ctxt) => rewr ctxt (add_ident ident ct idents)) ctxt
    4.75 +  in inner end
    4.76 +val fun_rewr_cconv : subterm_position = fn rewr => CConv.fun_cconv oo rewr
    4.77 +val arg_rewr_cconv : subterm_position = fn rewr => CConv.arg_cconv oo rewr
    4.78 +
    4.79 +
    4.80 +(* focus terms *)
    4.81 +
    4.82 +fun ft_abs ctxt (s,T) (tyenv, u, pos) =
    4.83 +  case try (fastype_of #> dest_funT) u of
    4.84 +    NONE => raise TERM ("ft_abs: no function type", [u])
    4.85 +  | SOME (U, _) =>
    4.86 +  let
    4.87 +    val tyenv' = if T = dummyT then tyenv else Sign.typ_match (Proof_Context.theory_of ctxt) (T, U) tyenv
    4.88 +    val x = Free (the_default (Name.internal dummyN) s, Envir.norm_type tyenv' T)
    4.89 +    val eta_expand_cconv = CConv.rewr_cconv @{thm eta_expand}
    4.90 +    fun eta_expand rewr ctxt bounds = eta_expand_cconv then_conv rewr ctxt bounds
    4.91 +    val (u', pos') =
    4.92 +      case u of
    4.93 +        Abs (_,_,t') => (subst_bound (x, t'), pos o abs_rewr_cconv s)
    4.94 +      | _ => (u $ x, pos o eta_expand o abs_rewr_cconv s)
    4.95 +  in (tyenv', u', pos') end
    4.96 +  handle Pattern.MATCH => raise TYPE ("ft_abs: types don't match", [T,U], [u])
    4.97 +
    4.98 +fun ft_fun _ (tyenv, l $ _, pos) = (tyenv, l, pos o fun_rewr_cconv)
    4.99 +  | ft_fun ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_fun ctxt o ft_abs ctxt (NONE, T)) ft
   4.100 +  | ft_fun _ (_, t, _) = raise TERM ("ft_fun", [t])
   4.101 +
   4.102 +fun ft_arg _ (tyenv, _ $ r, pos) = (tyenv, r, pos o arg_rewr_cconv)
   4.103 +  | ft_arg ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg ctxt o ft_abs ctxt (NONE, T)) ft
   4.104 +  | ft_arg _ (_, t, _) = raise TERM ("ft_arg", [t])
   4.105 +
   4.106 +(* Move to B in !!x_1 ... x_n. B. Do not eta-expand *)
   4.107 +fun ft_params ctxt (ft as (_, t, _) : focusterm) =
   4.108 +  case t of
   4.109 +    Const (@{const_name "Pure.all"}, _) $ Abs (_,T,_) =>
   4.110 +      (ft_params ctxt o ft_abs ctxt (NONE, T) o ft_arg ctxt) ft
   4.111 +  | Const (@{const_name "Pure.all"}, _) =>
   4.112 +      (ft_params ctxt o ft_arg ctxt) ft
   4.113 +  | _ => ft
   4.114 +
   4.115 +fun ft_all ctxt ident (ft as (_, Const (@{const_name "Pure.all"}, T) $ _, _) : focusterm) =
   4.116 +    let
   4.117 +      val def_U = T |> dest_funT |> fst |> dest_funT |> fst
   4.118 +      val ident' = apsnd (the_default (def_U)) ident
   4.119 +    in (ft_abs ctxt ident' o ft_arg ctxt) ft end
   4.120 +  | ft_all _ _ (_, t, _) = raise TERM ("ft_all", [t])
   4.121 +
   4.122 +fun ft_for ctxt idents (ft as (_, t, _) : focusterm) =
   4.123 +  let
   4.124 +    fun f rev_idents (Const (@{const_name "Pure.all"}, _) $ t) =
   4.125 +        let
   4.126 +         val (rev_idents', desc) = f rev_idents (case t of Abs (_,_,u) => u | _ => t)
   4.127 +        in
   4.128 +          case rev_idents' of
   4.129 +            [] => ([], desc o ft_all ctxt (NONE, NONE))
   4.130 +          | (x :: xs) => (xs , desc o ft_all ctxt x)
   4.131 +        end
   4.132 +      | f rev_idents _ = (rev_idents, I)
   4.133 +  in case f (rev idents) t of
   4.134 +      ([], ft') => SOME (ft' ft)
   4.135 +    | _ => NONE
   4.136 +  end
   4.137 +
   4.138 +fun ft_concl ctxt (ft as (_, t, _) : focusterm) =
   4.139 +  case t of
   4.140 +    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt) ft
   4.141 +  | _ => ft
   4.142 +
   4.143 +fun ft_assm ctxt (ft as (_, t, _) : focusterm) =
   4.144 +  case t of
   4.145 +    (Const (@{const_name "Pure.imp"}, _) $ _) $ _ => (ft_concl ctxt o ft_arg ctxt o ft_fun ctxt) ft
   4.146 +  | _ => raise TERM ("ft_assm", [t])
   4.147 +
   4.148 +fun ft_judgment ctxt (ft as (_, t, _) : focusterm) =
   4.149 +  if Object_Logic.is_judgment (Proof_Context.theory_of ctxt) t
   4.150 +  then ft_arg ctxt ft
   4.151 +  else ft
   4.152 +
   4.153 +
   4.154 +(* Return a lazy sequenze of all subterms of the focusterm for which
   4.155 +   the condition holds. *)
   4.156 +fun find_subterms ctxt condition (ft as (_, t, _) : focusterm) =
   4.157 +  let
   4.158 +    val recurse = find_subterms ctxt condition
   4.159 +    val recursive_matches = case t of
   4.160 +        _ $ _ => Seq.append (ft |> ft_fun ctxt |> recurse) (ft |> ft_arg ctxt |> recurse)
   4.161 +      | Abs (_,T,_) => ft |> ft_abs ctxt (NONE, T) |> recurse
   4.162 +      | _ => Seq.empty
   4.163 +  in
   4.164 +    (* If the condition is met, then the current focusterm is part of the
   4.165 +       sequence of results. Otherwise, only the results of the recursive
   4.166 +       application are. *)
   4.167 +    if condition ft
   4.168 +    then Seq.cons ft recursive_matches
   4.169 +    else recursive_matches
   4.170 +  end
   4.171 +
   4.172 +(* Find all subterms that might be a valid point to apply a rule. *)
   4.173 +fun valid_match_points ctxt =
   4.174 +  let
   4.175 +    fun is_valid (l $ _) = is_valid l
   4.176 +      | is_valid (Abs (_, _, a)) = is_valid a
   4.177 +      | is_valid (Var _) = false
   4.178 +      | is_valid (Bound _) = false
   4.179 +      | is_valid _ = true
   4.180 +  in
   4.181 +    find_subterms ctxt (#2 #> is_valid )
   4.182 +  end
   4.183 +
   4.184 +fun is_hole (Var ((name, _), _)) = (name = holeN)
   4.185 +  | is_hole _ = false
   4.186 +
   4.187 +fun is_hole_const (Const (@{const_name rewrite_HOLE}, _)) = true
   4.188 +  | is_hole_const _ = false
   4.189 +
   4.190 +val hole_syntax =
   4.191 +  let
   4.192 +    (* Modified variant of Term.replace_hole *)
   4.193 +    fun replace_hole Ts (Const (@{const_name rewrite_HOLE}, T)) i =
   4.194 +          (list_comb (Var ((holeN, i), Ts ---> T), map_range Bound (length Ts)), i + 1)
   4.195 +      | replace_hole Ts (Abs (x, T, t)) i =
   4.196 +          let val (t', i') = replace_hole (T :: Ts) t i
   4.197 +          in (Abs (x, T, t'), i') end
   4.198 +      | replace_hole Ts (t $ u) i =
   4.199 +          let
   4.200 +            val (t', i') = replace_hole Ts t i
   4.201 +            val (u', i'') = replace_hole Ts u i'
   4.202 +          in (t' $ u', i'') end
   4.203 +      | replace_hole _ a i = (a, i)
   4.204 +    fun prep_holes ts = #1 (fold_map (replace_hole []) ts 1)
   4.205 +  in
   4.206 +    Context.proof_map (Syntax_Phases.term_check 101 "hole_expansion" (K prep_holes))
   4.207 +    #> Proof_Context.set_mode Proof_Context.mode_pattern
   4.208 +  end
   4.209 +
   4.210 +(* Find a subterm of the focusterm matching the pattern. *)
   4.211 +fun find_matches ctxt pattern_list =
   4.212 +  let
   4.213 +    fun move_term ctxt (t, off) (ft : focusterm) =
   4.214 +      let
   4.215 +        val thy = Proof_Context.theory_of ctxt
   4.216 +
   4.217 +        val eta_expands =
   4.218 +          let val (_, ts) = strip_comb t
   4.219 +          in map fastype_of (snd (take_suffix is_Var ts)) end
   4.220 +
   4.221 +        fun do_match (tyenv, u, pos) =
   4.222 +          case try (Pattern.match thy (t,u)) (tyenv, Vartab.empty) of
   4.223 +            NONE => NONE
   4.224 +          | SOME (tyenv', _) => SOME (off (tyenv', u, pos))
   4.225 +
   4.226 +        fun match_argT T u =
   4.227 +          let val (U, _) = dest_funT (fastype_of u)
   4.228 +          in try (Sign.typ_match thy (T,U)) end
   4.229 +          handle TYPE _ => K NONE
   4.230 +
   4.231 +        fun desc [] ft = do_match ft
   4.232 +          | desc (T :: Ts) (ft as (tyenv , u, pos)) =
   4.233 +            case do_match ft of
   4.234 +              NONE =>
   4.235 +                (case match_argT T u tyenv of
   4.236 +                  NONE => NONE
   4.237 +                | SOME tyenv' => desc Ts (ft_abs ctxt (NONE, T) (tyenv', u, pos)))
   4.238 +            | SOME ft => SOME ft
   4.239 +      in desc eta_expands ft end
   4.240 +
   4.241 +    fun seq_unfold f ft =
   4.242 +      case f ft of
   4.243 +        NONE => Seq.empty
   4.244 +      | SOME ft' => Seq.cons ft' (seq_unfold f ft')
   4.245 +
   4.246 +    fun apply_pat At = Seq.map (ft_judgment ctxt)
   4.247 +      | apply_pat In = Seq.maps (valid_match_points ctxt)
   4.248 +      | apply_pat Asm = Seq.maps (seq_unfold (try (ft_assm ctxt)) o ft_params ctxt)
   4.249 +      | apply_pat Concl = Seq.map (ft_concl ctxt o ft_params ctxt)
   4.250 +      | apply_pat (For idents) = Seq.map_filter ((ft_for ctxt (map (apfst SOME) idents)))
   4.251 +      | apply_pat (Term x) = Seq.map_filter ( (move_term ctxt x))
   4.252 +
   4.253 +    fun apply_pats ft = ft
   4.254 +      |> Seq.single
   4.255 +      |> fold apply_pat pattern_list
   4.256 +
   4.257 +  in
   4.258 +    apply_pats
   4.259 +  end
   4.260 +
   4.261 +fun instantiate_normalize_env ctxt env thm =
   4.262 +  let
   4.263 +    fun certs f = map (apply2 (f ctxt))
   4.264 +    val prop = Thm.prop_of thm
   4.265 +    val norm_type = Envir.norm_type o Envir.type_env
   4.266 +    val insts = Term.add_vars prop []
   4.267 +      |> map (fn x as (s,T) => (Var (s, norm_type env T), Envir.norm_term env (Var x)))
   4.268 +      |> certs Thm.cterm_of
   4.269 +    val tyinsts = Term.add_tvars prop []
   4.270 +      |> map (fn x => (TVar x, norm_type env (TVar x)))
   4.271 +      |> certs Thm.ctyp_of
   4.272 +  in Drule.instantiate_normalize (tyinsts, insts) thm end
   4.273 +
   4.274 +fun unify_with_rhs context to env thm =
   4.275 +  let
   4.276 +    val (_, rhs) = thm |> Thm.concl_of |> Logic.dest_equals
   4.277 +    val env' = Pattern.unify context (Logic.mk_term to, Logic.mk_term rhs) env
   4.278 +      handle Pattern.Unif => raise NO_TO_MATCH
   4.279 +  in env' end
   4.280 +
   4.281 +fun inst_thm_to _ (NONE, _) thm = thm
   4.282 +  | inst_thm_to (ctxt : Proof.context) (SOME to, env) thm =
   4.283 +      instantiate_normalize_env ctxt (unify_with_rhs (Context.Proof ctxt) to env thm) thm
   4.284 +
   4.285 +fun inst_thm ctxt idents (to, tyenv) thm =
   4.286 +  let
   4.287 +    (* Replace any identifiers with their corresponding bound variables. *)
   4.288 +    val maxidx = Term.maxidx_typs (map (snd o snd) (Vartab.dest tyenv)) 0
   4.289 +    val env = Envir.Envir {maxidx = maxidx, tenv = Vartab.empty, tyenv = tyenv}
   4.290 +    val replace_idents =
   4.291 +      let
   4.292 +        fun subst ((n1, s)::ss) (t as Free (n2, _)) = if n1 = n2 then s else subst ss t
   4.293 +          | subst _ t = t
   4.294 +      in Term.map_aterms (subst idents) end
   4.295 +
   4.296 +    val maxidx = Envir.maxidx_of env |> fold Term.maxidx_term (map_filter I [to])
   4.297 +    val thm' = Thm.incr_indexes (maxidx + 1) thm
   4.298 +  in SOME (inst_thm_to ctxt (Option.map replace_idents to, env) thm') end
   4.299 +  handle NO_TO_MATCH => NONE
   4.300 +
   4.301 +(* Rewrite in subgoal i. *)
   4.302 +fun rewrite_goal_with_thm ctxt (pattern, (to, orig_ctxt)) rules = SUBGOAL (fn (t,i) =>
   4.303 +  let
   4.304 +    val matches = find_matches ctxt pattern (Vartab.empty, t, I)
   4.305 +
   4.306 +    fun rewrite_conv insty ctxt bounds =
   4.307 +      CConv.rewrs_cconv (map_filter (inst_thm ctxt bounds insty) rules)
   4.308 +
   4.309 +    val export = singleton (Proof_Context.export ctxt orig_ctxt)
   4.310 +
   4.311 +    fun distinct_prems th =
   4.312 +      case Seq.pull (distinct_subgoals_tac th) of
   4.313 +        NONE => th
   4.314 +      | SOME (th', _) => th'
   4.315 +
   4.316 +    fun tac (tyenv, _, position) = CCONVERSION
   4.317 +      (distinct_prems o export o position (rewrite_conv (to, tyenv)) ctxt []) i
   4.318 +  in
   4.319 +    SEQ_CONCAT (Seq.map tac matches)
   4.320 +  end)
   4.321 +
   4.322 +fun rewrite_tac ctxt pattern thms =
   4.323 +  let
   4.324 +    val thms' = maps (prep_meta_eq ctxt) thms
   4.325 +    val tac = rewrite_goal_with_thm ctxt pattern thms'
   4.326 +  in tac end
   4.327 +
   4.328 +val setup =
   4.329 +  let
   4.330 +
   4.331 +    fun mk_fix s = (Binding.name s, NONE, NoSyn)
   4.332 +
   4.333 +    val raw_pattern : (string, binding * string option * mixfix) pattern list parser =
   4.334 +      let
   4.335 +        val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
   4.336 +        val atom =  (Args.$$$ "asm" >> K Asm) ||
   4.337 +          (Args.$$$ "concl" >> K Concl) ||
   4.338 +          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
   4.339 +          (Parse.term >> Term)
   4.340 +        val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
   4.341 +
   4.342 +        fun append_default [] = [Concl, In]
   4.343 +          | append_default (ps as Term _ :: _) = Concl :: In :: ps
   4.344 +          | append_default ps = ps
   4.345 +
   4.346 +      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
   4.347 +
   4.348 +    fun ctxt_lift (scan : 'a parser) f = fn (ctxt : Context.generic, toks) =>
   4.349 +      let
   4.350 +        val (r, toks') = scan toks
   4.351 +        val (r', ctxt') = Context.map_proof_result (fn ctxt => f ctxt r) ctxt
   4.352 +      in (r', (ctxt', toks' : Token.T list))end
   4.353 +
   4.354 +    fun read_fixes fixes ctxt =
   4.355 +      let fun read_typ (b, rawT, mx) = (b, Option.map (Syntax.read_typ ctxt) rawT, mx)
   4.356 +      in Proof_Context.add_fixes (map read_typ fixes) ctxt end
   4.357 +
   4.358 +    fun prep_pats ctxt (ps : (string, binding * string option * mixfix) pattern list) =
   4.359 +      let
   4.360 +
   4.361 +        fun add_constrs ctxt n (Abs (x, T, t)) =
   4.362 +            let
   4.363 +              val (x', ctxt') = yield_singleton Proof_Context.add_fixes (mk_fix x) ctxt
   4.364 +            in
   4.365 +              (case add_constrs ctxt' (n+1) t of
   4.366 +                NONE => NONE
   4.367 +              | SOME ((ctxt'', n', xs), t') =>
   4.368 +                  let
   4.369 +                    val U = Type_Infer.mk_param n []
   4.370 +                    val u = Type.constraint (U --> dummyT) (Abs (x, T, t'))
   4.371 +                  in SOME ((ctxt'', n', (x', U) :: xs), u) end)
   4.372 +            end
   4.373 +          | add_constrs ctxt n (l $ r) =
   4.374 +            (case add_constrs ctxt n l of
   4.375 +              SOME (c, l') => SOME (c, l' $ r)
   4.376 +            | NONE =>
   4.377 +              (case add_constrs ctxt n r of
   4.378 +                SOME (c, r') => SOME (c, l $ r')
   4.379 +              | NONE => NONE))
   4.380 +          | add_constrs ctxt n t =
   4.381 +            if is_hole_const t then SOME ((ctxt, n, []), t) else NONE
   4.382 +
   4.383 +        fun prep (Term s) (n, ctxt) =
   4.384 +            let
   4.385 +              val t = Syntax.parse_term ctxt s
   4.386 +              val ((ctxt', n', bs), t') =
   4.387 +                the_default ((ctxt, n, []), t) (add_constrs ctxt (n+1) t)
   4.388 +            in (Term (t', bs), (n', ctxt')) end
   4.389 +          | prep (For ss) (n, ctxt) =
   4.390 +            let val (ns, ctxt') = read_fixes ss ctxt
   4.391 +            in (For ns, (n, ctxt')) end
   4.392 +          | prep At (n,ctxt) = (At, (n, ctxt))
   4.393 +          | prep In (n,ctxt) = (In, (n, ctxt))
   4.394 +          | prep Concl (n,ctxt) = (Concl, (n, ctxt))
   4.395 +          | prep Asm (n,ctxt) = (Asm, (n, ctxt))
   4.396 +
   4.397 +        val (xs, (_, ctxt')) = fold_map prep ps (0, ctxt)
   4.398 +
   4.399 +      in (xs, ctxt') end
   4.400 +
   4.401 +    fun prep_args ctxt (((raw_pats, raw_to), raw_ths)) =
   4.402 +      let
   4.403 +
   4.404 +        fun interpret_term_patterns ctxt =
   4.405 +          let
   4.406 +
   4.407 +            fun descend_hole fixes (Abs (_, _, t)) =
   4.408 +                (case descend_hole fixes t of
   4.409 +                  NONE => NONE
   4.410 +                | SOME (fix :: fixes', pos) => SOME (fixes', pos o ft_abs ctxt (apfst SOME fix))
   4.411 +                | SOME ([], _) => raise Match (* XXX -- check phases modified binding *))
   4.412 +              | descend_hole fixes (t as l $ r) =
   4.413 +                let val (f, _) = strip_comb t
   4.414 +                in
   4.415 +                  if is_hole f
   4.416 +                  then SOME (fixes, I)
   4.417 +                  else
   4.418 +                    (case descend_hole fixes l of
   4.419 +                      SOME (fixes', pos) => SOME (fixes', pos o ft_fun ctxt)
   4.420 +                    | NONE =>
   4.421 +                      (case descend_hole fixes r of
   4.422 +                        SOME (fixes', pos) => SOME (fixes', pos o ft_arg ctxt)
   4.423 +                      | NONE => NONE))
   4.424 +                end
   4.425 +              | descend_hole fixes t =
   4.426 +                if is_hole t then SOME (fixes, I) else NONE
   4.427 +
   4.428 +            fun f (t, fixes) = Term (t, (descend_hole (rev fixes) #> the_default ([], I) #> snd) t)
   4.429 +
   4.430 +          in map (map_term_pattern f) end
   4.431 +
   4.432 +        fun check_terms ctxt ps to =
   4.433 +          let
   4.434 +            fun safe_chop (0: int) xs = ([], xs)
   4.435 +              | safe_chop n (x :: xs) = chop (n - 1) xs |>> cons x
   4.436 +              | safe_chop _ _ = raise Match
   4.437 +
   4.438 +            fun reinsert_pat _ (Term (_, cs)) (t :: ts) =
   4.439 +                let val (cs', ts') = safe_chop (length cs) ts
   4.440 +                in (Term (t, map dest_Free cs'), ts') end
   4.441 +              | reinsert_pat _ (Term _) [] = raise Match
   4.442 +              | reinsert_pat ctxt (For ss) ts =
   4.443 +                let val fixes = map (fn s => (s, Variable.default_type ctxt s)) ss
   4.444 +                in (For fixes, ts) end
   4.445 +              | reinsert_pat _ At ts = (At, ts)
   4.446 +              | reinsert_pat _ In ts = (In, ts)
   4.447 +              | reinsert_pat _ Concl ts = (Concl, ts)
   4.448 +              | reinsert_pat _ Asm ts = (Asm, ts)
   4.449 +
   4.450 +            fun free_constr (s,T) = Type.constraint T (Free (s, dummyT))
   4.451 +            fun mk_free_constrs (Term (t, cs)) = t :: map free_constr cs
   4.452 +              | mk_free_constrs _ = []
   4.453 +
   4.454 +            val ts = maps mk_free_constrs ps @ map_filter I [to]
   4.455 +              |> Syntax.check_terms (hole_syntax ctxt)
   4.456 +            val ctxt' = fold Variable.declare_term ts ctxt
   4.457 +            val (ps', (to', ts')) = fold_map (reinsert_pat ctxt') ps ts
   4.458 +              ||> (fn xs => case to of NONE => (NONE, xs) | SOME _ => (SOME (hd xs), tl xs))
   4.459 +            val _ = case ts' of (_ :: _) => raise Match | [] => ()
   4.460 +          in ((ps', to'), ctxt') end
   4.461 +
   4.462 +        val (pats, ctxt') = prep_pats ctxt raw_pats
   4.463 +
   4.464 +        val ths = Attrib.eval_thms ctxt' raw_ths
   4.465 +        val to = Option.map (Syntax.parse_term ctxt') raw_to
   4.466 +
   4.467 +        val ((pats', to'), ctxt'') = check_terms ctxt' pats to
   4.468 +        val pats'' = interpret_term_patterns ctxt'' pats'
   4.469 +
   4.470 +      in ((pats'', ths, (to', ctxt)), ctxt'') end
   4.471 +
   4.472 +    val to_parser = Scan.option ((Args.$$$ "to") |-- Parse.term)
   4.473 +
   4.474 +    val subst_parser =
   4.475 +      let val scan = raw_pattern -- to_parser -- Parse.xthms1
   4.476 +      in ctxt_lift scan prep_args end
   4.477 +  in
   4.478 +    Method.setup @{binding rewrite} (subst_parser >>
   4.479 +      (fn (pattern, inthms, inst) => fn ctxt => SIMPLE_METHOD' (rewrite_tac ctxt (pattern, inst) inthms)))
   4.480 +      "single-step rewriting, allowing subterm selection via patterns."
   4.481 +  end
   4.482 +end
     5.1 --- a/src/HOL/ROOT	Wed Mar 18 14:14:07 2015 +0000
     5.2 +++ b/src/HOL/ROOT	Wed Mar 18 14:28:40 2015 +0000
     5.3 @@ -548,7 +548,7 @@
     5.4      NatSum
     5.5      ThreeDivides
     5.6      Cubic_Quartic
     5.7 -	Pythagoras
     5.8 +    Pythagoras
     5.9      Intuitionistic
    5.10      CTL
    5.11      Arith_Examples
    5.12 @@ -591,6 +591,7 @@
    5.13      SVC_Oracle
    5.14      Simps_Case_Conv_Examples
    5.15      ML
    5.16 +    Rewrite_Examples
    5.17      SAT_Examples
    5.18      SOS
    5.19      SOS_Cert
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/ex/Rewrite_Examples.thy	Wed Mar 18 14:28:40 2015 +0000
     6.3 @@ -0,0 +1,172 @@
     6.4 +theory Rewrite_Examples
     6.5 +imports Main "~~/src/HOL/Library/Rewrite"
     6.6 +begin
     6.7 +
     6.8 +section \<open>The rewrite Proof Method by Example\<close>
     6.9 +
    6.10 +(* This file is intended to give an overview over
    6.11 +   the features of the pattern-based rewrite proof method.
    6.12 +
    6.13 +   See also https://www21.in.tum.de/~noschinl/Pattern-2014/
    6.14 +*)
    6.15 +
    6.16 +lemma
    6.17 +  fixes a::int and b::int and c::int
    6.18 +  assumes "P (b + a)"
    6.19 +  shows "P (a + b)"
    6.20 +by (rewrite at "a + b" add.commute)
    6.21 +   (rule assms)
    6.22 +
    6.23 +(* Selecting a specific subterm in a large, ambiguous term. *)
    6.24 +lemma
    6.25 +  fixes a b c :: int
    6.26 +  assumes "f (a - a + (a - a)) + f (   0    + c) = f 0 + f c"
    6.27 +  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
    6.28 +  by (rewrite in "f _ + f \<box> = _" diff_self) fact
    6.29 +
    6.30 +lemma
    6.31 +  fixes a b c :: int
    6.32 +  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
    6.33 +  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
    6.34 +  by (rewrite at "f (_ + \<box>) + f _ = _" diff_self) fact
    6.35 +
    6.36 +lemma
    6.37 +  fixes a b c :: int
    6.38 +  assumes "f (  0   + (a - a)) + f ((a - a) + c) = f 0 + f c"
    6.39 +  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
    6.40 +  by (rewrite in "f (\<box> + _) + _ = _" diff_self) fact
    6.41 +
    6.42 +lemma
    6.43 +  fixes a b c :: int
    6.44 +  assumes "f (a - a +    0   ) + f ((a - a) + c) = f 0 + f c"
    6.45 +  shows   "f (a - a + (a - a)) + f ((a - a) + c) = f 0 + f c"
    6.46 +  by (rewrite in "f (_ + \<box>) + _ = _" diff_self) fact
    6.47 +
    6.48 +lemma
    6.49 +  fixes x y :: nat
    6.50 +  shows"x + y > c \<Longrightarrow> y + x > c"
    6.51 +  by (rewrite at "\<box> > c" add.commute) assumption
    6.52 +
    6.53 +(* We can also rewrite in the assumptions.  *)
    6.54 +lemma
    6.55 +  fixes x y :: nat
    6.56 +  assumes "y + x > c \<Longrightarrow> y + x > c"
    6.57 +  shows   "x + y > c \<Longrightarrow> y + x > c"
    6.58 +  by (rewrite in asm add.commute) fact
    6.59 +
    6.60 +lemma
    6.61 +  fixes x y :: nat
    6.62 +  assumes "y + x > c \<Longrightarrow> y + x > c"
    6.63 +  shows   "x + y > c \<Longrightarrow> y + x > c"
    6.64 +  by (rewrite in "x + y > c" at asm add.commute) fact
    6.65 +
    6.66 +lemma
    6.67 +  fixes x y :: nat
    6.68 +  assumes "y + x > c \<Longrightarrow> y + x > c"
    6.69 +  shows   "x + y > c \<Longrightarrow> y + x > c"
    6.70 +  by (rewrite at "\<box> > c" at asm  add.commute) fact
    6.71 +
    6.72 +lemma
    6.73 +  assumes "P {x::int. y + 1 = 1 + x}"
    6.74 +  shows   "P {x::int. y + 1 = x + 1}"
    6.75 +  by (rewrite at "x+1" in "{x::int. \<box> }" add.commute) fact
    6.76 +
    6.77 +lemma
    6.78 +  assumes "P {x::int. y + 1 = 1 + x}"
    6.79 +  shows   "P {x::int. y + 1 = x + 1}"
    6.80 +  by (rewrite at "any_identifier_will_work+1" in "{any_identifier_will_work::int. \<box> }" add.commute)
    6.81 +   fact
    6.82 +
    6.83 +lemma
    6.84 +  assumes "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. s * t + y - 3)}"
    6.85 +  shows   "P {(x::nat, y::nat, z). x + z * 3 = Q (\<lambda>s t. y + s * t - 3)}"
    6.86 +  by (rewrite at "b + d * e" in "\<lambda>(a, b, c). _ = Q (\<lambda>d e. \<box>)" add.commute) fact
    6.87 +
    6.88 +
    6.89 +(* Rewriting with conditional rewriting rules works just as well. *)
    6.90 +lemma test_theorem:
    6.91 +  fixes x :: nat
    6.92 +  shows "x \<le> y \<Longrightarrow> x \<ge> y \<Longrightarrow> x = y"
    6.93 +  by (rule Orderings.order_antisym)
    6.94 +
    6.95 +lemma
    6.96 +fixes f :: "nat \<Rightarrow> nat"
    6.97 +  assumes "f x \<le> 0" "f x \<ge> 0"
    6.98 +  shows "f x = 0"
    6.99 +  apply (rewrite at "f x" to "0" test_theorem)
   6.100 +  apply fact
   6.101 +  apply fact
   6.102 +  apply (rule refl)
   6.103 +done
   6.104 +
   6.105 +(*
   6.106 +   Instantiation.
   6.107 +
   6.108 +   Since all rewriting is now done via conversions,
   6.109 +   instantiation becomes fairly easy to do.
   6.110 +*)
   6.111 +
   6.112 +(* We first introduce a function f and an extended
   6.113 +   version of f that is annotated with an invariant. *)
   6.114 +fun f :: "nat \<Rightarrow> nat" where "f n = n"
   6.115 +definition "f_inv (I :: nat \<Rightarrow> bool) n \<equiv> f n"
   6.116 +
   6.117 +lemma annotate_f: "f = f_inv I"
   6.118 +  by (simp add: f_inv_def fun_eq_iff)
   6.119 +
   6.120 +(* We have a lemma with a bound variable n, and
   6.121 +   want to add an invariant to f. *)
   6.122 +lemma
   6.123 +  assumes "P (\<lambda>n. f_inv (\<lambda>_. True) n + 1) = x"
   6.124 +  shows "P (\<lambda>n. f n + 1) = x"
   6.125 +  by (rewrite to "f_inv (\<lambda>_. True)" annotate_f) fact
   6.126 +
   6.127 +(* We can also add an invariant that contains the variable n bound in the outer context.
   6.128 +   For this, we need to bind this variable to an identifier. *)
   6.129 +lemma
   6.130 +  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
   6.131 +  shows "P (\<lambda>n. f n + 1) = x"
   6.132 +  by (rewrite in "\<lambda>n. \<box>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) fact
   6.133 +
   6.134 +(* Any identifier will work *)
   6.135 +lemma
   6.136 +  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = x"
   6.137 +  shows "P (\<lambda>n. f n + 1) = x"
   6.138 +  by (rewrite in "\<lambda>abc. \<box>" to "f_inv (\<lambda>x. abc < x + 1)" annotate_f) fact
   6.139 +
   6.140 +(* The "for" keyword. *)
   6.141 +lemma
   6.142 +  assumes "P (2 + 1)"
   6.143 +  shows "\<And>x y. P (1 + 2 :: nat)"
   6.144 +by (rewrite in "P (1 + 2)" at for (x) add.commute) fact
   6.145 +
   6.146 +lemma
   6.147 +  assumes "\<And>x y. P (y + x)"
   6.148 +  shows "\<And>x y. P (x + y :: nat)"
   6.149 +by (rewrite in "P (x + _)" at for (x y) add.commute) fact
   6.150 +
   6.151 +lemma
   6.152 +  assumes "\<And>x y z. y + x + z = z + y + (x::int)"
   6.153 +  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
   6.154 +by (rewrite at "x + y" in "x + y + z" in concl at for (x y z) add.commute) fact
   6.155 +
   6.156 +lemma
   6.157 +  assumes "\<And>x y z. z + (x + y) = z + y + (x::int)"
   6.158 +  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
   6.159 +by (rewrite at "(_ + y) + z" in concl at for (y z) add.commute) fact
   6.160 +
   6.161 +lemma
   6.162 +  assumes "\<And>x y z. x + y + z = y + z + (x::int)"
   6.163 +  shows   "\<And>x y z. x + y + z = z + y + (x::int)"
   6.164 +by (rewrite at "\<box> + _" at "_ = \<box>" in concl at for () add.commute) fact
   6.165 +
   6.166 +(* The all-keyword can be used anywhere in the pattern where there is an \<And>-Quantifier. *)
   6.167 +lemma
   6.168 +  assumes "(\<And>(x::int). x < 1 + x)"
   6.169 +  and     "(x::int) + 1 > x"
   6.170 +  shows   "(\<And>(x::int). x + 1 > x) \<Longrightarrow> (x::int) + 1 > x"
   6.171 +by (rewrite at "x + 1" in for (x) at asm add.commute)
   6.172 +   (rule assms)
   6.173 +
   6.174 +end
   6.175 +