theory Scratch
  imports "HOL-Library.Rewrite"
begin

(* Copied from Rewrite_Examples.thy *)
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)

(* Copied and slightly modified from Rewrite_Examples.thy.
   (Rhs x renamed to xx for readability.) *)
lemma
  assumes "P (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = xx"
  shows "P (\<lambda>n. f n + 1) = xx"
  apply (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f) 
    (* Works and puts bound variable n inside the f_inv call. *)
  by fact

(* We replace P by sum. *)
lemma
  assumes "sum (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) = xx"
  shows "sum (\<lambda>n. f n + 1) = xx"
  apply (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f)
    (*  Still works. *)
  by fact

(* We add argument UNIV to "sum (...)" *)
lemma
  assumes "sum (\<lambda>n. f_inv (\<lambda>x. n < x + 1) n + 1) UNIV = xx UNIV"
  shows "sum (\<lambda>n. f n + 1) UNIV = xx UNIV"
  apply (rewrite in "\<lambda>n. \<hole>" to "f_inv (\<lambda>x. n < x + 1)" annotate_f)
    (* Rewrite succeeds but uses completely wrong value for n. It instantiates n := xx UNIV. *)
  by fact