theory Scratch
  imports "HOL-Library.Z2"
begin

lemma \<open>(\<Sum>(a,b)\<in>{0,1}\<times>{0,1}. x a b) = x 0 0 + x 0 1 + x 1 0 + x 1 1\<close> for x :: \<open>bit \<Rightarrow> bit \<Rightarrow> nat\<close>
  apply simp (* Fails to solve goal! *)
  oops

declare insert_Times_insert[simp del]
lemma insert_Times_insert'[simp]:
  "insert a A \<times> insert b B = insert (a,b) (A \<times> insert b B \<union> {a} \<times> B)"
  by blast

lemma \<open>(\<Sum>(a,b)\<in>{0,1}\<times>{0,1}. x a b) = x 0 0 + x 0 1 + x 1 0 + x 1 1\<close> for x :: \<open>bit \<Rightarrow> bit \<Rightarrow> nat\<close>
  by simp (* Success. *)

end