--- 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"
--- 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 = {}"
--- 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}"
--- 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)"
--- 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
--- 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:
--- 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)
--- 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
--- 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
--- 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
--- 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
--- 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}"
--- 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 *}
--- 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}"