# HG changeset patch
# User hoelzl
# Date 1401454510 -7200
# Node ID 7edb7550663e37be9683aecaa874bc5f4b18a8d2
# Parent  4874411752fe41c9e6cebd109669146f4f6a3040
introduce more powerful reindexing rules for big operators

diff -r 4874411752fe -r 7edb7550663e src/HOL/Fact.thy
--- a/src/HOL/Fact.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Fact.thy	Fri May 30 14:55:10 2014 +0200
@@ -308,12 +308,7 @@
 
 lemma fact_eq_rev_setprod_nat: "fact (k::nat) = (\<Prod>i<k. k - i)"
   unfolding fact_altdef_nat
-proof (rule strong_setprod_reindex_cong)
-  { fix i assume "Suc 0 \<le> i" "i \<le> k" then have "\<exists>j\<in>{..<k}. i = k - j"
-      by (intro bexI[of _ "k - i"]) simp_all }
-  then show "{1..k} = (\<lambda>i. k - i) ` {..<k}"
-    by (auto simp: image_iff)
-qed (auto intro: inj_onI)
+  by (rule setprod.reindex_bij_witness[where i="\<lambda>i. k - i" and j="\<lambda>i. k - i"]) auto
 
 lemma fact_div_fact_le_pow:
   assumes "r \<le> n" shows "fact n div fact (n - r) \<le> n ^ r"
diff -r 4874411752fe -r 7edb7550663e src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Groups_Big.thy	Fri May 30 14:55:10 2014 +0200
@@ -131,27 +131,8 @@
   assumes "A = B"
   assumes g_h: "\<And>x. x \<in> B \<Longrightarrow> g x = h x"
   shows "F g A = F h B"
-proof (cases "finite A")
-  case True
-  then have "\<And>C. C \<subseteq> A \<longrightarrow> (\<forall>x\<in>C. g x = h x) \<longrightarrow> F g C = F h C"
-  proof induct
-    case empty then show ?case by simp
-  next
-    case (insert x F) then show ?case apply -
-    apply (simp add: subset_insert_iff, clarify)
-    apply (subgoal_tac "finite C")
-      prefer 2 apply (blast dest: finite_subset [rotated])
-    apply (subgoal_tac "C = insert x (C - {x})")
-      prefer 2 apply blast
-    apply (erule ssubst)
-    apply (simp add: Ball_def del: insert_Diff_single)
-    done
-  qed
-  with `A = B` g_h show ?thesis by simp
-next
-  case False
-  with `A = B` show ?thesis by simp
-qed
+  using g_h unfolding `A = B`
+  by (induct B rule: infinite_finite_induct) auto
 
 lemma strong_cong [cong]:
   assumes "A = B" "\<And>x. x \<in> B =simp=> g x = h x"
@@ -206,42 +187,6 @@
   shows "R (F h S) (F g S)"
   using fS by (rule finite_subset_induct) (insert assms, auto)
 
-lemma eq_general:
-  assumes h: "\<forall>y\<in>S'. \<exists>!x. x \<in> S \<and> h x = y" 
-  and f12:  "\<forall>x\<in>S. h x \<in> S' \<and> f2 (h x) = f1 x"
-  shows "F f1 S = F f2 S'"
-proof-
-  from h f12 have hS: "h ` S = S'" by blast
-  {fix x y assume H: "x \<in> S" "y \<in> S" "h x = h y"
-    from f12 h H  have "x = y" by auto }
-  hence hinj: "inj_on h S" unfolding inj_on_def Ex1_def by blast
-  from f12 have th: "\<And>x. x \<in> S \<Longrightarrow> (f2 \<circ> h) x = f1 x" by auto 
-  from hS have "F f2 S' = F f2 (h ` S)" by simp
-  also have "\<dots> = F (f2 o h) S" using reindex [OF hinj, of f2] .
-  also have "\<dots> = F f1 S " using th cong [of _ _ "f2 o h" f1]
-    by blast
-  finally show ?thesis ..
-qed
-
-lemma eq_general_reverses:
-  assumes kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
-  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = j x"
-  shows "F j S = F g T"
-  (* metis solves it, but not yet available here *)
-  apply (rule eq_general [of T S h g j])
-  apply (rule ballI)
-  apply (frule kh)
-  apply (rule ex1I[])
-  apply blast
-  apply clarsimp
-  apply (drule hk) apply simp
-  apply (rule sym)
-  apply (erule conjunct1[OF conjunct2[OF hk]])
-  apply (rule ballI)
-  apply (drule hk)
-  apply blast
-  done
-
 lemma mono_neutral_cong_left:
   assumes "finite T" and "S \<subseteq> T" and "\<forall>i \<in> T - S. h i = 1"
   and "\<And>x. x \<in> S \<Longrightarrow> g x = h x" shows "F g S = F h T"
@@ -267,6 +212,74 @@
   "\<lbrakk> finite T;  S \<subseteq> T;  \<forall>i \<in> T - S. g i = 1 \<rbrakk> \<Longrightarrow> F g T = F g S"
   by (blast intro!: mono_neutral_left [symmetric])
 
+lemma reindex_bij_betw: "bij_betw h S T \<Longrightarrow> F (\<lambda>x. g (h x)) S = F g T"
+  by (auto simp: bij_betw_def reindex)
+
+lemma reindex_bij_witness:
+  assumes witness:
+    "\<And>a. a \<in> S \<Longrightarrow> i (j a) = a"
+    "\<And>a. a \<in> S \<Longrightarrow> j a \<in> T"
+    "\<And>b. b \<in> T \<Longrightarrow> j (i b) = b"
+    "\<And>b. b \<in> T \<Longrightarrow> i b \<in> S"
+  assumes eq:
+    "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
+  shows "F g S = F h T"
+proof -
+  have "bij_betw j S T"
+    using bij_betw_byWitness[where A=S and f=j and f'=i and A'=T] witness by auto
+  moreover have "F g S = F (\<lambda>x. h (j x)) S"
+    by (intro cong) (auto simp: eq)
+  ultimately show ?thesis
+    by (simp add: reindex_bij_betw)
+qed
+
+lemma reindex_bij_betw_not_neutral:
+  assumes fin: "finite S'" "finite T'"
+  assumes bij: "bij_betw h (S - S') (T - T')"
+  assumes nn:
+    "\<And>a. a \<in> S' \<Longrightarrow> g (h a) = z"
+    "\<And>b. b \<in> T' \<Longrightarrow> g b = z"
+  shows "F (\<lambda>x. g (h x)) S = F g T"
+proof -
+  have [simp]: "finite S \<longleftrightarrow> finite T"
+    using bij_betw_finite[OF bij] fin by auto
+
+  show ?thesis
+  proof cases
+    assume "finite S"
+    with nn have "F (\<lambda>x. g (h x)) S = F (\<lambda>x. g (h x)) (S - S')"
+      by (intro mono_neutral_cong_right) auto
+    also have "\<dots> = F g (T - T')"
+      using bij by (rule reindex_bij_betw)
+    also have "\<dots> = F g T"
+      using nn `finite S` by (intro mono_neutral_cong_left) auto
+    finally show ?thesis .
+  qed simp
+qed
+
+lemma reindex_bij_witness_not_neutral:
+  assumes fin: "finite S'" "finite T'"
+  assumes witness:
+    "\<And>a. a \<in> S - S' \<Longrightarrow> i (j a) = a"
+    "\<And>a. a \<in> S - S' \<Longrightarrow> j a \<in> T - T'"
+    "\<And>b. b \<in> T - T' \<Longrightarrow> j (i b) = b"
+    "\<And>b. b \<in> T - T' \<Longrightarrow> i b \<in> S - S'"
+  assumes nn:
+    "\<And>a. a \<in> S' \<Longrightarrow> g a = z"
+    "\<And>b. b \<in> T' \<Longrightarrow> h b = z"
+  assumes eq:
+    "\<And>a. a \<in> S \<Longrightarrow> h (j a) = g a"
+  shows "F g S = F h T"
+proof -
+  have bij: "bij_betw j (S - (S' \<inter> S)) (T - (T' \<inter> T))"
+    using witness by (intro bij_betw_byWitness[where f'=i]) auto
+  have F_eq: "F g S = F (\<lambda>x. h (j x)) S"
+    by (intro cong) (auto simp: eq)
+  show ?thesis
+    unfolding F_eq using fin nn eq
+    by (intro reindex_bij_betw_not_neutral[OF _ _ bij]) auto
+qed
+
 lemma delta: 
   assumes fS: "finite S"
   shows "F (\<lambda>k. if k = a then b k else 1) S = (if a \<in> S then b a else 1)"
@@ -403,46 +416,17 @@
 begin
 
 lemma setsum_reindex_id: 
-  "inj_on f B ==> setsum f B = setsum id (f ` B)"
+  "inj_on f B \<Longrightarrow> setsum f B = setsum id (f ` B)"
   by (simp add: setsum.reindex)
 
 lemma setsum_reindex_nonzero:
   assumes fS: "finite S"
   and nz: "\<And>x y. x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x = f y \<Longrightarrow> h (f x) = 0"
   shows "setsum h (f ` S) = setsum (h \<circ> f) S"
-using nz proof (induct rule: finite_induct [OF fS])
-  case 1 thus ?case by simp
-next
-  case (2 x F) 
-  { assume fxF: "f x \<in> f ` F" hence "\<exists>y \<in> F . f y = f x" by auto
-    then obtain y where y: "y \<in> F" "f x = f y" by auto 
-    from "2.hyps" y have xy: "x \<noteq> y" by auto
-    from "2.prems" [of x y] "2.hyps" xy y have h0: "h (f x) = 0" by simp
-    have "setsum h (f ` insert x F) = setsum h (f ` F)" using fxF by auto
-    also have "\<dots> = setsum (h o f) (insert x F)" 
-      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
-      using h0
-      apply (simp cong del: setsum.strong_cong)
-      apply (rule "2.hyps"(3))
-      apply (rule_tac y="y" in  "2.prems")
-      apply simp_all
-      done
-    finally have ?case . }
-  moreover
-  { assume fxF: "f x \<notin> f ` F"
-    have "setsum h (f ` insert x F) = h (f x) + setsum h (f ` F)" 
-      using fxF "2.hyps" by simp 
-    also have "\<dots> = setsum (h o f) (insert x F)"
-      unfolding setsum.insert[OF `finite F` `x\<notin>F`]
-      apply (simp cong del: setsum.strong_cong)
-      apply (rule cong [OF refl [of "op + (h (f x))"]])
-      apply (rule "2.hyps"(3))
-      apply (rule_tac y="y" in  "2.prems")
-      apply simp_all
-      done
-    finally have ?case . }
-  ultimately show ?case by blast
-qed
+proof (subst setsum.reindex_bij_betw_not_neutral[symmetric])
+  show "bij_betw f (S - {x\<in>S. h (f x) = 0}) (f`S - f`{x\<in>S. h (f x) = 0})"
+    using nz by (auto intro!: inj_onI simp: bij_betw_def)
+qed (insert fS, auto)
 
 lemma setsum_cong2:
   "(\<And>x. x \<in> A \<Longrightarrow> f x = g x) \<Longrightarrow> setsum f A = setsum g A"
@@ -494,19 +478,8 @@
 
 lemma setsum_commute:
   "(\<Sum>i\<in>A. \<Sum>j\<in>B. f i j) = (\<Sum>j\<in>B. \<Sum>i\<in>A. f i j)"
-proof (simp add: setsum_cartesian_product)
-  have "(\<Sum>(x,y) \<in> A <*> B. f x y) =
-    (\<Sum>(y,x) \<in> (%(i, j). (j, i)) ` (A \<times> B). f x y)"
-    (is "?s = _")
-    apply (simp add: setsum.reindex [where h = "%(i, j). (j, i)"] swap_inj_on)
-    apply (simp add: split_def)
-    done
-  also have "... = (\<Sum>(y,x)\<in>B \<times> A. f x y)"
-    (is "_ = ?t")
-    apply (simp add: swap_product)
-    done
-  finally show "?s = ?t" .
-qed
+  unfolding setsum_cartesian_product
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>(i, j). (j, i)" and j="\<lambda>(i, j). (j, i)"]) auto
 
 lemma setsum_Plus:
   fixes A :: "'a set" and B :: "'b set"
@@ -616,14 +589,6 @@
   setsum f (S \<union> T) = setsum f S + setsum f T"
   by (fact setsum.union_inter_neutral)
 
-lemma setsum_eq_general_reverses:
-  assumes fS: "finite S" and fT: "finite T"
-  and kh: "\<And>y. y \<in> T \<Longrightarrow> k y \<in> S \<and> h (k y) = y"
-  and hk: "\<And>x. x \<in> S \<Longrightarrow> h x \<in> T \<and> k (h x) = x \<and> g (h x) = f x"
-  shows "setsum f S = setsum g T"
-  using kh hk by (fact setsum.eq_general_reverses)
-
-
 subsubsection {* Properties in more restricted classes of structures *}
 
 lemma setsum_Un: "finite A ==> finite B ==>
@@ -1124,17 +1089,9 @@
   by (frule setprod.reindex, simp)
 
 lemma strong_setprod_reindex_cong:
-  assumes i: "inj_on f A"
-  and B: "B = f ` A" and eq: "\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x"
-  shows "setprod h B = setprod g A"
-proof-
-  have "setprod h B = setprod (h o f) A"
-    by (simp add: B setprod.reindex [OF i, of h])
-  then show ?thesis apply simp
-    apply (rule setprod.cong)
-    apply simp
-    by (simp add: eq)
-qed
+  "inj_on f A \<Longrightarrow> B = f ` A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x = (h \<circ> f) x) \<Longrightarrow> setprod h B = setprod g A"
+  by (subst setprod.reindex_bij_betw[symmetric, where h=f])
+     (auto simp: bij_betw_def)
 
 lemma setprod_Union_disjoint:
   assumes "\<forall>A\<in>C. finite A" "\<forall>A\<in>C. \<forall>B\<in>C. A \<noteq> B \<longrightarrow> A Int B = {}" 
diff -r 4874411752fe -r 7edb7550663e src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri May 30 14:55:10 2014 +0200
@@ -163,20 +163,7 @@
   fixes n :: nat
     and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i=0..n. f i (n - i)) = (\<Sum>i=0..n. f (n - i) i)"
-proof (rule setsum_reindex_cong)
-  show "inj_on (\<lambda>i. n - i) {0..n}"
-    by (rule inj_onI) simp
-  show "{0..n} = (\<lambda>i. n - i) ` {0..n}"
-    apply auto
-    apply (rule_tac x = "n - x" in image_eqI)
-    apply simp_all
-    done
-next
-  fix i
-  assume "i \<in> {0..n}"
-  then have "n - (n - i) = i" by simp
-  then show "f (n - i) i = f (n - i) (n - (n - i))" by simp
-qed
+  by (rule setsum.reindex_bij_witness[where i="op - n" and j="op - n"]) auto
 
 instance fps :: (comm_semiring_0) ab_semigroup_mult
 proof
@@ -811,54 +798,23 @@
     fix n :: nat
     let ?Zn = "{0 ..n}"
     let ?Zn1 = "{0 .. n + 1}"
-    let ?f = "\<lambda>i. i + 1"
-    have fi: "inj_on ?f {0..n}"
-      by (simp add: inj_on_def)
-    have eq: "{1.. n+1} = ?f ` {0..n}"
-      by auto
     let ?g = "\<lambda>i. of_nat (i+1) * g $ (i+1) * f $ (n - i) +
         of_nat (i+1)* f $ (i+1) * g $ (n - i)"
     let ?h = "\<lambda>i. of_nat i * g $ i * f $ ((n+1) - i) +
         of_nat i* f $ i * g $ ((n + 1) - i)"
-    {
-      fix k
-      assume k: "k \<in> {0..n}"
-      have "?h (k + 1) = ?g k"
-        using k by auto
-    }
-    note th0 = this
-    have eq': "{0..n +1}- {1 .. n+1} = {0}" by auto
     have s0: "setsum (\<lambda>i. of_nat i * f $ i * g $ (n + 1 - i)) ?Zn1 =
       setsum (\<lambda>i. of_nat (n + 1 - i) * f $ (n + 1 - i) * g $ i) ?Zn1"
-      apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1 - i"])
-      apply (simp add: inj_on_def Ball_def)
-      apply presburger
-      apply (rule set_eqI)
-      apply (presburger add: image_iff)
-      apply simp
-      done
+       by (rule setsum.reindex_bij_witness[where i="op - (n + 1)" and j="op - (n + 1)"]) auto
     have s1: "setsum (\<lambda>i. f $ i * g $ (n + 1 - i)) ?Zn1 =
       setsum (\<lambda>i. f $ (n + 1 - i) * g $ i) ?Zn1"
-      apply (rule setsum_reindex_cong[where f="\<lambda>i. n + 1 - i"])
-      apply (simp add: inj_on_def Ball_def)
-      apply presburger
-      apply (rule set_eqI)
-      apply (presburger add: image_iff)
-      apply simp
-      done
+       by (rule setsum.reindex_bij_witness[where i="op - (n + 1)" and j="op - (n + 1)"]) auto
     have "(f * ?D g + ?D f * g)$n = (?D g * f + ?D f * g)$n"
       by (simp only: mult_commute)
     also have "\<dots> = (\<Sum>i = 0..n. ?g i)"
       by (simp add: fps_mult_nth setsum_addf[symmetric])
-    also have "\<dots> = setsum ?h {1..n+1}"
-      using th0 setsum_reindex_cong[OF fi eq, of "?g" "?h"] by auto
     also have "\<dots> = setsum ?h {0..n+1}"
-      apply (rule setsum_mono_zero_left)
-      apply simp
-      apply (simp add: subset_eq)
-      unfolding eq'
-      apply simp
-      done
+      by (rule setsum.reindex_bij_witness_not_neutral
+            [where S'="{}" and T'="{0}" and j="Suc" and i="\<lambda>i. i - 1"]) auto
     also have "\<dots> = (fps_deriv (f * g)) $ n"
       apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf)
       unfolding s0 s1
@@ -2521,14 +2477,7 @@
 lemma convolution_eq:
   "setsum (\<lambda>i. a (i :: nat) * b (n - i)) {0 .. n} =
     setsum (\<lambda>(i,j). a i * b j) {(i,j). i \<le> n \<and> j \<le> n \<and> i + j = n}"
-  apply (rule setsum_reindex_cong[where f=fst])
-  apply (clarsimp simp add: inj_on_def)
-  apply (auto simp add: set_eq_iff image_iff)
-  apply (rule_tac x= "x" in exI)
-  apply clarsimp
-  apply (rule_tac x="n - x" in exI)
-  apply arith
-  done
+  by (rule setsum.reindex_bij_witness[where i=fst and j="\<lambda>i. (i, n - i)"]) auto
 
 lemma product_composition_lemma:
   assumes c0: "c$0 = (0::'a::idom)"
@@ -3329,12 +3278,9 @@
           done
         have eq1: "setprod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {0 .. h} =
           setprod of_nat {Suc (m - h) .. Suc m}"
-          apply (rule strong_setprod_reindex_cong[where f="\<lambda>k. Suc m - k "])
           using kn' h m
-          apply (auto simp add: inj_on_def image_def)
-          apply (rule_tac x="Suc m - x" in bexI)
-          apply (simp_all add: of_nat_diff)
-          done
+          by (intro setprod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
+             (auto simp: of_nat_diff)
 
         have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
           unfolding m1nk
@@ -3360,12 +3306,9 @@
         have th21:"pochhammer (b - of_nat n + 1) k = setprod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
           unfolding h m
           unfolding pochhammer_Suc_setprod
-          apply (rule strong_setprod_reindex_cong[where f="\<lambda>k. n - 1 - k"])
-          using kn
-          apply (auto simp add: inj_on_def m h image_def)
-          apply (rule_tac x= "m - x" in bexI)
-          apply (auto simp add: of_nat_diff)
-          done
+          using kn m h
+          by (intro setprod.reindex_bij_witness[where i="\<lambda>k. n - 1 - k" and j="\<lambda>i. m-i"])
+             (auto simp: of_nat_diff)
 
         have "?m1 n * ?p b n =
           pochhammer (b - of_nat n + 1) k * setprod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
diff -r 4874411752fe -r 7edb7550663e src/HOL/Library/Permutations.thy
--- a/src/HOL/Library/Permutations.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Library/Permutations.thy	Fri May 30 14:55:10 2014 +0200
@@ -1025,7 +1025,7 @@
   show ?thesis
     unfolding permutes_insert
     unfolding setsum_cartesian_product
-    unfolding  th1[symmetric]
+    unfolding th1[symmetric]
     unfolding th0
   proof (rule setsum_reindex)
     let ?f = "(\<lambda>(b, y). Fun.swap a b id \<circ> y)"
diff -r 4874411752fe -r 7edb7550663e src/HOL/Lifting_Set.thy
--- a/src/HOL/Lifting_Set.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Lifting_Set.thy	Fri May 30 14:55:10 2014 +0200
@@ -85,6 +85,26 @@
   "rel_set (eq_onp P) = eq_onp (\<lambda>A. Ball A P)"
   unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast
 
+lemma bi_unique_rel_set_lemma:
+  assumes "bi_unique R" and "rel_set R X Y"
+  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
+proof
+  def f \<equiv> "\<lambda>x. THE y. R x y"
+  { fix x assume "x \<in> X"
+    with `rel_set R X Y` `bi_unique R` have "R x (f x)"
+      by (simp add: bi_unique_def rel_set_def f_def) (metis theI)
+    with assms `x \<in> X` 
+    have  "R x (f x)" "\<forall>x'\<in>X. R x' (f x) \<longrightarrow> x = x'" "\<forall>y\<in>Y. R x y \<longrightarrow> y = f x" "f x \<in> Y"
+      by (fastforce simp add: bi_unique_def rel_set_def)+ }
+  note * = this
+  moreover
+  { fix y assume "y \<in> Y"
+    with `rel_set R X Y` *(3) `y \<in> Y` have "\<exists>x\<in>X. y = f x"
+      by (fastforce simp: rel_set_def) }
+  ultimately show "\<forall>x\<in>X. R x (f x)" "Y = image f X" "inj_on f X"
+    by (auto simp: inj_on_def image_iff)
+qed
+
 subsection {* Quotient theorem for the Lifting package *}
 
 lemma Quotient_set[quot_map]:
@@ -231,90 +251,37 @@
   shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
   unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
 
-lemma bi_unique_rel_set_lemma:
-  assumes "bi_unique R" and "rel_set R X Y"
-  obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
-proof
-  let ?f = "\<lambda>x. THE y. R x y"
-  from assms show f: "\<forall>x\<in>X. R x (?f x)"
-    apply (clarsimp simp add: rel_set_def)
-    apply (drule (1) bspec, clarify)
-    apply (rule theI2, assumption)
-    apply (simp add: bi_unique_def)
-    apply assumption
-    done
-  from assms show "Y = image ?f X"
-    apply safe
-    apply (clarsimp simp add: rel_set_def)
-    apply (drule (1) bspec, clarify)
-    apply (rule image_eqI)
-    apply (rule the_equality [symmetric], assumption)
-    apply (simp add: bi_unique_def)
-    apply assumption
-    apply (clarsimp simp add: rel_set_def)
-    apply (frule (1) bspec, clarify)
-    apply (rule theI2, assumption)
-    apply (clarsimp simp add: bi_unique_def)
-    apply (simp add: bi_unique_def, metis)
-    done
-  show "inj_on ?f X"
-    apply (rule inj_onI)
-    apply (drule f [rule_format])
-    apply (drule f [rule_format])
-    apply (simp add: assms(1) [unfolded bi_unique_def])
-    done
-qed
-
 lemma finite_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
-  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
-    auto dest: finite_imageD)
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
+     (auto dest: finite_imageD)
 
 lemma card_transfer [transfer_rule]:
   "bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
-  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
+  by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
+     (simp add: card_image)
 
 lemma vimage_parametric [transfer_rule]:
   assumes [transfer_rule]: "bi_total A" "bi_unique B"
   shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
-unfolding vimage_def[abs_def] by transfer_prover
-
-lemma setsum_parametric [transfer_rule]:
-  assumes "bi_unique A"
-  shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
-proof(rule rel_funI)+
-  fix f :: "'a \<Rightarrow> 'c" and g S T
-  assume fg: "(A ===> op =) f g"
-    and ST: "rel_set A S T"
-  show "setsum f S = setsum g T"
-  proof(rule setsum_reindex_cong)
-    let ?f = "\<lambda>t. THE s. A s t"
-    show "S = ?f ` T"
-      by(blast dest: rel_setD1[OF ST] rel_setD2[OF ST] bi_uniqueDl[OF assms] 
-           intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
-
-    show "inj_on ?f T"
-    proof(rule inj_onI)
-      fix t1 t2
-      assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
-      from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: rel_setD2)
-      hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
-      moreover
-      from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: rel_setD2)
-      hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
-      ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
-      with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
-    qed
-
-    fix t
-    assume "t \<in> T"
-    with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
-    hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
-    moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
-    ultimately show "g t = f (?f t)" by simp
-  qed
-qed
+  unfolding vimage_def[abs_def] by transfer_prover
 
 end
 
+lemma (in comm_monoid_set) F_parametric [transfer_rule]:
+  fixes A :: "'b \<Rightarrow> 'c \<Rightarrow> bool"
+  assumes "bi_unique A"
+  shows "rel_fun (rel_fun A (op =)) (rel_fun (rel_set A) (op =)) F F"
+proof(rule rel_funI)+
+  fix f :: "'b \<Rightarrow> 'a" and g S T
+  assume "rel_fun A (op =) f g" "rel_set A S T"
+  with `bi_unique A` obtain i where "bij_betw i S T" "\<And>x. x \<in> S \<Longrightarrow> f x = g (i x)"
+    by (auto elim: bi_unique_rel_set_lemma simp: rel_fun_def bij_betw_def)
+  then show "F f S = F g T"
+    by (simp add: reindex_bij_betw)
+qed
+
+lemmas setsum_parametric = setsum.F_parametric
+lemmas setprod_parametric = setprod.F_parametric
+
 end
diff -r 4874411752fe -r 7edb7550663e src/HOL/Multivariate_Analysis/Determinants.thy
--- a/src/HOL/Multivariate_Analysis/Determinants.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Determinants.thy	Fri May 30 14:55:10 2014 +0200
@@ -40,12 +40,7 @@
 lemma setprod_offset:
   fixes m n :: nat
   shows "setprod f {m + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"
-  apply (rule setprod_reindex_cong[where f="op + p"])
-  apply (auto simp add: image_iff Bex_def inj_on_def)
-  apply presburger
-  apply (rule ext)
-  apply (simp add: add_commute)
-  done
+  by (rule setprod.reindex_bij_witness[where i="op + p" and j="\<lambda>i. i - p"]) auto
 
 lemma setprod_singleton: "setprod f {x} = f x"
   by simp
@@ -678,7 +673,7 @@
   let ?h = "\<lambda>(y,g) i. if i = z then y else g i"
   let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"
   let ?s = "\<lambda> k a c f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)"
-  let ?c = "\<lambda>i. if i = z then a i j else c i"
+  let ?c = "\<lambda>j i. if i = z then a i j else c i"
   have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)"
     by simp
   have thif2: "\<And>a b c d e. (if a then b else if c then d else e) =
@@ -702,14 +697,9 @@
                                 else c i))"
     unfolding insert.hyps unfolding setsum_cartesian_product by blast
   show ?case unfolding tha
-    apply (rule setsum_eq_general_reverses[where h= "?h" and k= "?k"],
-      blast intro: finite_cartesian_product fS finite,
-      blast intro: finite_cartesian_product fS finite)
     using `z \<notin> T`
-    apply auto
-    apply (rule cong[OF refl[of det]])
-    apply vector
-    done
+    by (intro setsum.reindex_bij_witness[where i="?k" and j="?h"])
+       (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff)
 qed
 
 lemma det_linear_rows_setsum:
diff -r 4874411752fe -r 7edb7550663e src/HOL/Multivariate_Analysis/Integration.thy
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri May 30 14:55:10 2014 +0200
@@ -1672,41 +1672,30 @@
   by blast
 
 lemma setsum_over_tagged_division_lemma:
-  fixes d :: "'m::euclidean_space set \<Rightarrow> 'a::real_normed_vector"
   assumes "p tagged_division_of i"
     and "\<And>u v. cbox u v \<noteq> {} \<Longrightarrow> content (cbox u v) = 0 \<Longrightarrow> d (cbox u v) = 0"
   shows "setsum (\<lambda>(x,k). d k) p = setsum d (snd ` p)"
 proof -
-  note assm = tagged_division_ofD[OF assms(1)]
   have *: "(\<lambda>(x,k). d k) = d \<circ> snd"
     unfolding o_def by (rule ext) auto
+  note assm = tagged_division_ofD[OF assms(1)]
   show ?thesis
     unfolding *
-    apply (subst eq_commute)
-  proof (rule setsum_reindex_nonzero)
+  proof (rule setsum_reindex_nonzero[symmetric])
     show "finite p"
       using assm by auto
     fix x y
-    assume as: "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
+    assume "x\<in>p" "y\<in>p" "x\<noteq>y" "snd x = snd y"
     obtain a b where ab: "snd x = cbox a b"
-      using assm(4)[of "fst x" "snd x"] as(1) by auto
+      using assm(4)[of "fst x" "snd x"] `x\<in>p` by auto
     have "(fst x, snd y) \<in> p" "(fst x, snd y) \<noteq> y"
-      unfolding as(4)[symmetric] using as(1-3) by auto
-    then have "interior (snd x) \<inter> interior (snd y) = {}"
-      apply -
-      apply (rule assm(5)[of "fst x" _ "fst y"])
-      using as
-      apply auto
-      done
+      by (metis pair_collapse `x\<in>p` `snd x = snd y` `x \<noteq> y`)+
+    with `x\<in>p` `y\<in>p` have "interior (snd x) \<inter> interior (snd y) = {}"
+      by (intro assm(5)[of "fst x" _ "fst y"]) auto
     then have "content (cbox a b) = 0"
-      unfolding as(4)[symmetric] ab content_eq_0_interior by auto
+      unfolding `snd x = snd y`[symmetric] ab content_eq_0_interior by auto
     then have "d (cbox a b) = 0"
-      apply -
-      apply (rule assms(2))
-      using assm(2)[of "fst x" "snd x"] as(1)
-      unfolding ab[symmetric]
-      apply auto
-      done
+      using assm(2)[of "fst x" "snd x"] `x\<in>p` ab[symmetric] by (intro assms(2)) auto
     then show "d (snd x) = 0"
       unfolding ab by auto
   qed
@@ -7433,18 +7422,10 @@
         have *: "inj_on (\<lambda>(x, k). (g x, g ` k)) p"
           using inj(1) unfolding inj_on_def by fastforce
         have "(\<Sum>(x, k)\<in>(\<lambda>(x, k). (g x, g ` k)) ` p. content k *\<^sub>R f x) - i = r *\<^sub>R (\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - i" (is "?l = _")
-          unfolding algebra_simps add_left_cancel
-          unfolding setsum_reindex[OF *]
-          apply (subst scaleR_right.setsum)
-          defer
-          apply (rule setsum_cong2)
-          unfolding o_def split_paired_all split_conv
-          apply (drule p(4))
-          apply safe
-          unfolding assms(7)[rule_format]
-          using p
-          apply auto
-          done
+          using assms(7)
+          unfolding algebra_simps add_left_cancel scaleR_right.setsum
+          by (subst setsum.reindex_bij_betw[symmetric, where h="\<lambda>(x, k). (g x, g ` k)" and S=p])
+             (auto intro!: * setsum_cong simp: bij_betw_def dest!: p(4))
       also have "\<dots> = r *\<^sub>R ((\<Sum>(x, k)\<in>p. content k *\<^sub>R f (g x)) - (1 / r) *\<^sub>R i)" (is "_ = ?r")
         unfolding scaleR_diff_right scaleR_scaleR
         using assms(1)
diff -r 4874411752fe -r 7edb7550663e src/HOL/Multivariate_Analysis/PolyRoots.thy
--- a/src/HOL/Multivariate_Analysis/PolyRoots.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/PolyRoots.thy	Fri May 30 14:55:10 2014 +0200
@@ -30,11 +30,8 @@
 proof -
   have "(\<Sum>i=m..n. x^i) = x^m * (\<Sum>i=m..n. x^(i-m))"
     by (simp add: setsum_right_distrib power_add [symmetric])
-  also have "... = x^m * (\<Sum>i\<le>n-m. x^i)"
-    apply (subst setsum_reindex_cong [where f = "%i. i+m" and A = "{..n-m}"])
-    apply (auto simp: image_def)
-    apply (rule_tac x="x-m" in bexI, auto)
-    by (metis assms ordered_cancel_comm_monoid_diff_class.le_diff_conv2)
+  also have "(\<Sum>i=m..n. x^(i-m)) = (\<Sum>i\<le>n-m. x^i)"
+    using `m \<le> n` by (intro setsum.reindex_bij_witness[where j="\<lambda>i. i - m" and i="\<lambda>i. i + m"]) auto
   finally show ?thesis .
 qed
 
@@ -95,13 +92,9 @@
            (x - y) * (\<Sum>j<n. \<Sum>k<n-j. a (j+k+1) * y^k * x^j)"
 proof -
   { fix j
-    assume "j < n"
     have "(\<Sum>k = Suc j..n. a k * y^(k - Suc j) * x^j) =
           (\<Sum>k <n - j. a (Suc (j + k)) * y^k * x^j)"
-      apply (rule_tac f = "\<lambda>i. Suc j + i" in setsum_reindex_cong)
-      apply (auto simp: inj_on_def image_def atLeastLessThan_def lessThan_def)
-      apply (metis Suc_le_eq diff_add_inverse diff_less_mono le_add1 less_imp_Suc_add)
-      done }
+      by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + Suc j" and j="\<lambda>i. i - Suc j"]) auto }
   then show ?thesis
     by (simp add: sub_polyfun)
 qed
diff -r 4874411752fe -r 7edb7550663e src/HOL/Number_Theory/Binomial.thy
--- a/src/HOL/Number_Theory/Binomial.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Number_Theory/Binomial.thy	Fri May 30 14:55:10 2014 +0200
@@ -198,12 +198,8 @@
 
 lemma natsum_reverse_index:
   fixes m::nat
-  assumes "\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)"
-  shows "(\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
-apply (rule setsum_reindex_cong [where f = "\<lambda>k. m+n-k"])
-apply (auto simp add: inj_on_def image_def)
-apply (rule_tac x="m+n-x" in bexI, auto simp: assms)
-done
+  shows "(\<And>k. m \<le> k \<Longrightarrow> k \<le> n \<Longrightarrow> g k = f (m + n - k)) \<Longrightarrow> (\<Sum>k=m..n. f k) = (\<Sum>k=m..n. g k)"
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>k. m+n-k" and j="\<lambda>k. m+n-k"]) auto
 
 lemma sum_choose_diagonal:
   assumes "m\<le>n" shows "(\<Sum>k=0..m. (n-k) choose (m-k)) = Suc n choose m"
@@ -347,16 +343,13 @@
   then show ?thesis by simp
 next
   case (Suc h)
-  have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}"
+  have eq: "((- 1) ^ Suc h :: 'a) = (\<Prod>i=0..h. - 1)"
     using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
     by auto
   show ?thesis
     unfolding Suc pochhammer_Suc_setprod eq setprod_timesf[symmetric]
-    apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
-    using Suc
-    apply (auto simp add: inj_on_def image_def of_nat_diff)
-    apply (metis atLeast0AtMost atMost_iff diff_diff_cancel diff_le_self)
-    done
+    by (rule setprod.reindex_bij_witness[where i="op - h" and j="op - h"])
+       (auto simp: of_nat_diff)
 qed
 
 lemma pochhammer_minus':
@@ -454,14 +447,9 @@
     have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
       by (subst setprod_constant) auto
     have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
-      apply (rule strong_setprod_reindex_cong[where f="op - n"])
         using h kn
-        apply (simp_all add: inj_on_def image_iff Bex_def set_eq_iff)
-        apply clarsimp
-        apply presburger
-       apply presburger
-      apply (simp add: fun_eq_iff field_simps of_nat_add[symmetric] del: of_nat_add)
-      done
+      by (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
+         (auto simp: of_nat_diff)
     have th0: "finite {1..n - Suc h}" "finite {n - h .. n}"
         "{1..n - Suc h} \<inter> {n - h .. n} = {}" and
         eq3: "{1..n - Suc h} \<union> {n - h .. n} = {1..n}"
@@ -476,13 +464,8 @@
       unfolding mult_assoc[symmetric]
       unfolding setprod_timesf[symmetric]
       apply simp
-      apply (rule strong_setprod_reindex_cong[where f= "op - n"])
-        apply (auto simp add: inj_on_def image_iff Bex_def)
-       apply presburger
-      apply (subgoal_tac "(of_nat (n - x) :: 'a) = of_nat n - of_nat x")
-       apply simp
-      apply (rule of_nat_diff)
-      apply simp
+      apply (intro setprod.reindex_bij_witness[where i="op - n" and j="op - n"])
+      apply (auto simp: of_nat_diff)
       done
   }
   moreover
diff -r 4874411752fe -r 7edb7550663e src/HOL/Old_Number_Theory/Finite2.thy
--- a/src/HOL/Old_Number_Theory/Finite2.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Finite2.thy	Fri May 30 14:55:10 2014 +0200
@@ -185,38 +185,4 @@
   by (auto simp add: card_bdd_int_set_l_le)
 
 
-subsection {* Cardinality of finite cartesian products *}
-
-(* FIXME could be useful in general but not needed here
-lemma insert_Sigma [simp]: "(insert x A) <*> B = ({ x } <*> B) \<union> (A <*> B)"
-  by blast
- *)
-
-text {* Lemmas for counting arguments. *}
-
-lemma setsum_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
-    g ` B \<subseteq> A; inj_on g B |] ==> setsum g B = setsum (g \<circ> f) A"
-  apply (frule_tac h = g and f = f in setsum_reindex)
-  apply (subgoal_tac "setsum g B = setsum g (f ` A)")
-   apply (simp add: inj_on_def)
-  apply (subgoal_tac "card A = card B")
-   apply (drule_tac A = "f ` A" and B = B in card_seteq)
-     apply (auto simp add: card_image)
-  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
-  apply (frule_tac A = B and B = A and f = g in card_inj_on_le)
-    apply auto
-  done
-
-lemma setprod_bij_eq: "[| finite A; finite B; f ` A \<subseteq> B; inj_on f A;
-    g ` B \<subseteq> A; inj_on g B |] ==> setprod g B = setprod (g \<circ> f) A"
-  apply (frule_tac h = g and f = f in setprod_reindex)
-  apply (subgoal_tac "setprod g B = setprod g (f ` A)")
-   apply (simp add: inj_on_def)
-  apply (subgoal_tac "card A = card B")
-   apply (drule_tac A = "f ` A" and B = B in card_seteq)
-     apply (auto simp add: card_image)
-  apply (frule_tac A = A and B = B and f = f in card_inj_on_le, auto)
-  apply (frule_tac A = B and B = A and f = g in card_inj_on_le, auto)
-  done
-
 end
diff -r 4874411752fe -r 7edb7550663e src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri May 30 14:55:10 2014 +0200
@@ -18,6 +18,13 @@
   "\<lbrakk> [a = b] (mod p); [b = c] (mod p) \<rbrakk> \<Longrightarrow> [a = c] (mod p)"
   by (simp add:modeq_def)
 
+lemma modeq_sym[sym]:
+  "[a = b] (mod p) \<Longrightarrow> [b = a] (mod p)"
+  unfolding modeq_def by simp
+
+lemma modneq_sym[sym]:
+  "[a \<noteq> b] (mod p) \<Longrightarrow> [b \<noteq> a] (mod p)"
+  by (simp add: modneq_def)
 
 lemma nat_mod_lemma: assumes xyn: "[x = y] (mod n)" and xy:"y \<le> x"
   shows "\<exists>q. x = y + n * q"
@@ -597,44 +604,39 @@
       by (simp add: coprime_commute)
     have Paphi: "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
     proof-
-      let ?h = "\<lambda>m. m mod n"
-      {fix m assume mS: "m\<in> ?S"
-        hence "?h m \<in> ?S" by simp}
-      hence hS: "?h ` ?S = ?S"by (auto simp add: image_iff)
-      have "a\<noteq>0" using an n1 nz apply- apply (rule ccontr) by simp
-      hence inj: "inj_on (op * a) ?S" unfolding inj_on_def by simp
-      have eq0: "setprod (?h \<circ> op * a) {m. coprime m n \<and> m < n} = setprod (\<lambda>m. m) {m. coprime m n \<and> m < n}"
-      proof (rule setprod.eq_general [where h="?h o (op * a)"])
-        {fix y assume yS: "y \<in> ?S" hence y: "coprime y n" "y < n" by simp_all
-          from cong_solve_unique[OF an nz, of y]
-          obtain x where x:"x < n" "[a * x = y] (mod n)" "\<forall>z. z < n \<and> [a * z = y] (mod n) \<longrightarrow> z=x" by blast
-          from cong_coprime[OF x(2)] y(1)
-          have xm: "coprime x n" by (simp add: coprime_mul_eq coprime_commute)
-          {fix z assume "z \<in> ?S" "(?h \<circ> op * a) z = y"
-            hence z: "coprime z n" "z < n" "(?h \<circ> op * a) z = y" by simp_all
-            from x(3)[rule_format, of z] z(2,3) have "z=x"
-              unfolding modeq_def mod_less[OF y(2)] by simp}
-          with xm x(1,2) have "\<exists>!x. x \<in> ?S \<and> (?h \<circ> op * a) x = y"
-            unfolding modeq_def mod_less[OF y(2)] by safe auto }
-        thus "\<forall>y\<in>{m. coprime m n \<and> m < n}.
-       \<exists>!x. x \<in> {m. coprime m n \<and> m < n} \<and> ((\<lambda>m. m mod n) \<circ> op * a) x = y" by blast
-      next
-        {fix x assume xS: "x\<in> ?S"
-          hence x: "coprime x n" "x < n" by simp_all
-          with an have "coprime (a*x) n"
-            by (simp add: coprime_mul_eq[of n a x] coprime_commute)
-          hence "?h (a*x) \<in> ?S" using nz
-            by (simp add: coprime_mod[OF nz])}
-        thus " \<forall>x\<in>{m. coprime m n \<and> m < n}.
-       ((\<lambda>m. m mod n) \<circ> op * a) x \<in> {m. coprime m n \<and> m < n} \<and>
-       ((\<lambda>m. m mod n) \<circ> op * a) x = ((\<lambda>m. m mod n) \<circ> op * a) x" by simp
+      let ?h = "\<lambda>m. (a * m) mod n"
+      
+      have eq0: "(\<Prod>i\<in>?S. ?h i) = (\<Prod>i\<in>?S. i)"
+      proof (rule setprod.reindex_bij_betw)
+        have "inj_on (\<lambda>i. ?h i) ?S"
+        proof (rule inj_onI)
+          fix x y assume "?h x = ?h y"
+          then have "[a * x = a * y] (mod n)"
+            by (simp add: modeq_def)
+          moreover assume "x \<in> ?S" "y \<in> ?S"
+          ultimately show "x = y"
+            by (auto intro: cong_imp_eq cong_mult_lcancel an)
+        qed
+        moreover have "?h ` ?S = ?S"
+        proof safe
+          fix y assume "coprime y n" then show "coprime (?h y) n"
+            by (metis an nz coprime_commute coprime_mod coprime_mul_eq)
+        next
+          fix y assume y: "coprime y n" "y < n"
+          from cong_solve_unique[OF an nz] obtain x where x: "x < n" "[a * x = y] (mod n)"
+            by blast
+          then show "y \<in> ?h ` ?S"
+            using cong_coprime[OF x(2)] coprime_mul_eq[of n a x] an y x
+            by (intro image_eqI[of _ _ x]) (auto simp add: coprime_commute modeq_def)
+        qed (insert nz, simp)
+        ultimately show "bij_betw ?h ?S ?S"
+          by (simp add: bij_betw_def)
       qed
       from nproduct_mod[OF fS nz, of "op * a"]
-      have "[(setprod (op *a) ?S) = (setprod (?h o (op * a)) ?S)] (mod n)"
-        unfolding o_def
+      have "[(\<Prod>i\<in>?S. a * i) = (\<Prod>i\<in>?S. ?h i)] (mod n)"
         by (simp add: cong_commute)
-      also have "[setprod (?h o (op * a)) ?S = ?P ] (mod n)"
-        using eq0 fS an by (simp add: setprod_def modeq_def o_def)
+      also have "[(\<Prod>i\<in>?S. ?h i) = ?P] (mod n)"
+        using eq0 fS an by (simp add: setprod_def modeq_def)
       finally show "[?P*a^ (\<phi> n) = ?P*1] (mod n)"
         unfolding cardfS mult_commute[of ?P "a^ (card ?S)"]
           nproduct_cmul[OF fS, symmetric] mult_1_right by simp
diff -r 4874411752fe -r 7edb7550663e src/HOL/Series.thy
--- a/src/HOL/Series.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Series.thy	Fri May 30 14:55:10 2014 +0200
@@ -560,19 +560,10 @@
 lemma setsum_triangle_reindex:
   fixes n :: nat
   shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
-proof -
-  have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
-    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
-  proof (rule setsum_reindex_cong)
-    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
-      by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
-    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
-      by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
-    show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
-      by clarify
-  qed
-  thus ?thesis by (simp add: setsum_Sigma)
-qed
+  apply (simp add: setsum_Sigma)
+  apply (rule setsum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
+  apply auto
+  done
 
 lemma Cauchy_product_sums:
   fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
diff -r 4874411752fe -r 7edb7550663e src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Set_Interval.thy	Fri May 30 14:55:10 2014 +0200
@@ -1537,9 +1537,7 @@
 
 lemma setsum_shift_bounds_cl_nat_ivl:
   "setsum f {m+k..n+k} = setsum (%i. f(i + k)){m..n::nat}"
-apply (insert setsum_reindex[OF inj_on_add_nat, where h=f and B = "{m..n}"])
-apply (simp add:image_add_atLeastAtMost o_def)
-done
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
 
 corollary setsum_shift_bounds_cl_Suc_ivl:
   "setsum f {Suc m..Suc n} = setsum (%i. f(Suc i)){m..n}"
@@ -1706,13 +1704,8 @@
   show ?case by simp
 qed
 
-lemma nat_diff_setsum_reindex:
-  fixes x :: "'a::{comm_ring,monoid_mult}"
-  shows "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
-apply (subst setsum_reindex_cong [of "%i. n - Suc i" "{..< n}"])
-apply (auto simp: inj_on_def)
-apply (rule_tac x="n - Suc x" in image_eqI, auto)
-done
+lemma nat_diff_setsum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
+  by (rule setsum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
 
 subsection {* Products indexed over intervals *}
 
diff -r 4874411752fe -r 7edb7550663e src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Fri May 30 12:54:42 2014 +0200
+++ b/src/HOL/Transcendental.thy	Fri May 30 14:55:10 2014 +0200
@@ -76,10 +76,7 @@
 lemma lemma_realpow_rev_sumr:
    "(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) =
     (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
-  apply (rule setsum_reindex_cong [where f="\<lambda>i. n - i"])
-  apply (auto simp: image_iff Bex_def intro!: inj_onI)
-  apply arith
-  done
+  by (subst nat_diff_setsum_reindex[symmetric]) simp
 
 lemma power_diff_1_eq:
   fixes x :: "'a::{comm_ring,monoid_mult}"