theory Scratch
  imports "HOL-Library.Rewrite"
begin

(* A useful lemma *)
lemma sum_single: 
  assumes "finite A"
  assumes "\<And>j. j \<noteq> i \<Longrightarrow> j\<in>A \<Longrightarrow> f j = 0"
  shows "sum f A = (if i\<in>A then f i else 0)"
  apply (subst sum.mono_neutral_cong_right[where S=\<open>A \<inter> {i}\<close> and h=f])
  using assms by auto

lemma \<open>(\<Sum>x::bool\<in>UNIV. (\<Sum>y\<in>UNIV. of_bool (x=y))) = 2\<close>
  (* Lets rewrite the inner sum with sum_single. *)
  apply (rewrite at \<open>\<Sum>x\<in>UNIV. \<hole>\<close> sum_single)
  (* This gives us the schematic variable ?i8 that we would like to instantiate with x *)
  oops

lemma \<open>(\<Sum>x::bool\<in>UNIV. (\<Sum>y\<in>UNIV. of_bool (x=y))) = 2\<close>
  apply (rewrite at \<open>\<Sum>x\<in>UNIV. \<hole>\<close> sum_single where ?i=x)
  (* Error (this syntax has been removed, it seems) *)
  oops

lemma \<open>(\<Sum>x::bool\<in>UNIV. (\<Sum>y\<in>UNIV. of_bool (x=y))) = 2\<close>
  (* Trying to instantiate. *)
  apply (rewrite at \<open>\<Sum>x\<in>UNIV. \<hole>\<close> to \<open>if x\<in>_ then _ else _\<close> sum_single)
  (* Exception Pattern *)