Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy Wed Apr 10 21:29:32 2019 +0100
@@ -13,7 +13,7 @@
lemma sum_mult_product:
"sum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))"
- unfolding sum_nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
+ unfolding sum.nat_group[of h B A, unfolded atLeast0LessThan, symmetric]
proof (rule sum.cong, simp, rule sum.reindex_cong)
fix i
show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI)
--- a/src/HOL/Analysis/Conformal_Mappings.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Conformal_Mappings.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1070,7 +1070,7 @@
proof (cases "\<forall>i\<le>n. 0<i \<longrightarrow> a i = 0")
case True
then have [simp]: "\<And>z. f z = a 0"
- by (simp add: that sum_atMost_shift)
+ by (simp add: that sum.atMost_shift)
have False using compf [of "{a 0}"] by simp
then show ?thesis ..
next
--- a/src/HOL/Analysis/FPS_Convergence.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/FPS_Convergence.thy Wed Apr 10 21:29:32 2019 +0100
@@ -333,7 +333,7 @@
have "norm (natfun_inverse f (Suc n)) =
norm (\<Sum>i = Suc 0..Suc n. fps_nth f i * natfun_inverse f (Suc n - i))"
(is "_ = norm ?S") using assms
- by (simp add: field_simps norm_mult norm_divide del: sum_cl_ivl_Suc)
+ by (simp add: field_simps norm_mult norm_divide del: sum.cl_ivl_Suc)
also have "norm ?S \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i * natfun_inverse f (Suc n - i)))"
by (rule norm_sum)
also have "\<dots> \<le> (\<Sum>i = Suc 0..Suc n. norm (fps_nth f i) / \<delta> ^ (Suc n - i))"
--- a/src/HOL/Analysis/Gamma_Function.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Wed Apr 10 21:29:32 2019 +0100
@@ -510,7 +510,7 @@
by (simp add: fact_prod)
(subst prod_dividef [symmetric], simp_all add: field_simps)
also from m have "z * ... = (\<Prod>k=0..n. z + k) / fact n"
- by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)
also have "(\<Prod>k=0..n. z + k) = pochhammer z (Suc n)"
unfolding pochhammer_prod
by (simp add: prod.atLeast0_atMost_Suc atLeastLessThanSuc_atLeastAtMost)
@@ -535,7 +535,7 @@
proof eventually_elim
fix n :: nat assume n: "n > 0"
have "(\<Sum>k<n. ?f k) = (\<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k))"
- by (subst atLeast0LessThan [symmetric], subst sum_shift_bounds_Suc_ivl [symmetric],
+ by (subst atLeast0LessThan [symmetric], subst sum.shift_bounds_Suc_ivl [symmetric],
subst atLeastLessThanSuc_atLeastAtMost) simp_all
also have "\<dots> = z * of_real (harm n) - (\<Sum>k=1..n. ln (1 + z / of_nat k))"
by (simp add: harm_def sum_subtractf sum_distrib_left divide_inverse)
@@ -653,7 +653,7 @@
also have "(\<Sum>n\<in>\<dots>. f n) = (\<Sum>n<k. f n) + (\<Sum>n=k..<m+k. f n)"
by (rule sum.union_disjoint) auto
also have "(\<Sum>n=k..<m+k. f n) = (\<Sum>n=0..<m+k-k. f (n + k))"
- using sum_shift_bounds_nat_ivl [of f 0 k m] by simp
+ using sum.shift_bounds_nat_ivl [of f 0 k m] by simp
finally show "(\<Sum>n<k. f n) + (\<Sum>n<m. f (n + k)) = (\<Sum>n<m+k. f n)" by (simp add: atLeast0LessThan)
qed
finally have "(\<lambda>a. sum f {..<a}) \<longlonglongrightarrow> lim (\<lambda>m. sum f {..<m + k})"
@@ -2485,7 +2485,7 @@
also have "(\<Prod>k=1..n. 1 + 1 / of_nat k :: real) = (\<Prod>k=1..n. (of_nat k + 1) / of_nat k)"
by (intro prod.cong) (simp_all add: divide_simps)
also have "(\<Prod>k=1..n. (of_nat k + 1) / of_nat k :: real) = of_nat n + 1"
- by (induction n) (simp_all add: prod_nat_ivl_Suc' divide_simps)
+ by (induction n) (simp_all add: prod.nat_ivl_Suc' divide_simps)
finally show ?thesis ..
qed
@@ -2515,8 +2515,13 @@
(simp_all add: Gamma_series_euler'_def prod.distrib
prod_inversef[symmetric] divide_inverse)
also have "(\<Prod>k=1..n. (1 + z / of_nat k)) = pochhammer (z + 1) n / fact n"
- by (cases n) (simp_all add: pochhammer_prod fact_prod atLeastLessThanSuc_atLeastAtMost
- prod_dividef [symmetric] field_simps prod.atLeast_Suc_atMost_Suc_shift)
+ proof (cases n)
+ case (Suc n')
+ then show ?thesis
+ unfolding pochhammer_prod fact_prod
+ by (simp add: atLeastLessThanSuc_atLeastAtMost field_simps prod_dividef
+ prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)
+ qed auto
also have "z * \<dots> = pochhammer z (Suc n) / fact n" by (simp add: pochhammer_rec)
finally show "?r n = Gamma_series_euler' z n / Gamma_series z n" by simp
qed
@@ -2561,7 +2566,7 @@
have "(\<lambda>n. \<Sum>k=1..n. z / of_nat k - ln (1 + z / of_nat k)) \<longlonglongrightarrow> ln_Gamma z + euler_mascheroni * z + ln z"
using ln_Gamma_series'_aux[OF False]
by (simp only: atLeastLessThanSuc_atLeastAtMost [symmetric] One_nat_def
- sum_shift_bounds_Suc_ivl sums_def atLeast0LessThan)
+ sum.shift_bounds_Suc_ivl sums_def atLeast0LessThan)
from tendsto_exp[OF this] False z have "?f \<longlonglongrightarrow> z * exp (euler_mascheroni * z) * Gamma z"
by (simp add: exp_add exp_sum exp_diff mult_ac Gamma_complex_altdef A)
from tendsto_mult[OF tendsto_const[of "exp (-euler_mascheroni * z) / z"] this] z
@@ -2842,7 +2847,7 @@
also have "?A = (\<lambda>t. ?f t * ?g' t)" by (intro ext) (simp_all add: field_simps)
also have "?B = - (of_nat (Suc n) * fact n / pochhammer z (n+2))"
by (simp add: divide_simps pochhammer_rec
- prod_shift_bounds_cl_Suc_ivl del: of_nat_Suc)
+ prod.shift_bounds_cl_Suc_ivl del: of_nat_Suc)
finally show "((\<lambda>t. ?f t * ?g' t) has_integral (?f 1 * ?g 1 - ?f 0 * ?g 0 - ?I)) {0..1}"
by simp
qed (simp_all add: bounded_bilinear_mult)
@@ -3248,7 +3253,7 @@
have "(\<lambda>n. P x n - P x (Suc n)) sums (P x 0 - sin (pi * x) / (pi * x))"
unfolding P_def using x by (intro telescope_sums' sin_product_formula_real')
also have "(\<lambda>n. P x n - P x (Suc n)) = (\<lambda>n. (x^2 / of_nat (Suc n)^2) * P x n)"
- unfolding P_def by (simp add: prod_nat_ivl_Suc' algebra_simps)
+ unfolding P_def by (simp add: prod.nat_ivl_Suc' algebra_simps)
also have "P x 0 = 1" by (simp add: P_def)
finally have "(\<lambda>n. x\<^sup>2 / (of_nat (Suc n))\<^sup>2 * P x n) sums (1 - sin (pi * x) / (pi * x))" .
from sums_divide[OF this, of "x^2"] x show ?thesis unfolding g_def by simp
--- a/src/HOL/Analysis/Harmonic_Numbers.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy Wed Apr 10 21:29:32 2019 +0100
@@ -61,7 +61,7 @@
also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k=Suc 0..Suc n. inverse (of_nat k) :: real)"
unfolding harm_def[abs_def] by (subst convergent_Suc_iff) simp_all
also have "... \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. inverse (of_nat (Suc k)) :: real)"
- by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
+ by (subst sum.shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
also have "... \<longleftrightarrow> summable (\<lambda>n. inverse (of_nat n) :: real)"
by (subst summable_Suc_iff [symmetric]) (simp add: summable_iff_convergent')
also have "\<not>..." by (rule not_summable_harmonic)
@@ -123,7 +123,7 @@
"euler_mascheroni.sum_integral_diff_series n = harm (Suc n) - ln (of_nat (Suc n))"
proof -
have "harm (Suc n) = (\<Sum>k=0..n. inverse (of_nat k + 1) :: real)" unfolding harm_def
- unfolding One_nat_def by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: add_ac)
+ unfolding One_nat_def by (subst sum.shift_bounds_cl_Suc_ivl) (simp add: add_ac)
moreover have "((\<lambda>x. inverse (x + 1) :: real) has_integral ln (of_nat n + 1) - ln (0 + 1))
{0..of_nat n}"
by (intro fundamental_theorem_of_calculus)
--- a/src/HOL/Analysis/Infinite_Products.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy Wed Apr 10 21:29:32 2019 +0100
@@ -620,7 +620,7 @@
then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
by simp (subst prod.union_disjoint; force)
also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
- by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
+ by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod.shift_bounds_cl_nat_ivl)
finally show ?thesis by metis
qed
ultimately have "(\<lambda>n. prod f {..n}) \<longlonglongrightarrow> prod f {..<M} * p"
@@ -975,7 +975,7 @@
have "prod f {..<n} = 1" for n
by (metis \<open>\<And>n. 1 \<le> prod f n\<close> \<open>prodinf f = 1\<close> antisym f convergent_prod_has_prod ge1 order_trans prod_le_prodinf zero_le_one)
then have "(\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" if "n \<ge> Suc i" for i n
- by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod_lessThan_Suc)
+ by (metis mult.left_neutral order_refl prod.cong prod.neutral_const prod.lessThan_Suc)
then show "\<exists>N. \<forall>n\<ge>N. (\<Prod>n\<in>{i}. f n) \<le> prod f {..<n}" for i
by blast
qed
@@ -1042,7 +1042,7 @@
using prod_le_prodinf[of f _ "Suc i"]
by (meson "0" "1" Suc_leD convergent_prod_has_prod f \<open>n \<le> i\<close> le_trans less_eq_real_def)
ultimately show ?thesis
- by (metis le_less_trans mult.commute not_le prod_lessThan_Suc)
+ by (metis le_less_trans mult.commute not_le prod.lessThan_Suc)
qed
lemma prod_less_prodinf:
@@ -1187,7 +1187,8 @@
have "raw_has_prod f M (a * f M) \<longleftrightarrow> (\<lambda>i. \<Prod>j\<le>Suc i. f (j+M)) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
by (subst LIMSEQ_Suc_iff) (simp add: raw_has_prod_def)
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M \<and> a * f M \<noteq> 0"
- by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod_atLeast1_atMost_eq lessThan_Suc_atMost)
+ by (simp add: ac_simps atMost_Suc_eq_insert_0 image_Suc_atMost prod.atLeast1_atMost_eq lessThan_Suc_atMost
+ del: prod.cl_ivl_Suc)
also have "\<dots> \<longleftrightarrow> raw_has_prod (\<lambda>n. f (Suc n)) M a \<and> f M \<noteq> 0"
proof safe
assume tends: "(\<lambda>i. (\<Prod>j\<le>i. f (Suc j + M)) * f M) \<longlonglongrightarrow> a * f M" and 0: "a * f M \<noteq> 0"
--- a/src/HOL/Analysis/Poly_Roots.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Poly_Roots.thy Wed Apr 10 21:29:32 2019 +0100
@@ -23,7 +23,7 @@
also have "... = (x - y) * (\<Sum>i\<le>n. (\<Sum>j<i. a i * y^(i - Suc j) * x^j))"
by (simp add: sum_distrib_left ac_simps)
also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - Suc j) * x^j))"
- by (simp add: nested_sum_swap')
+ by (simp add: sum.nested_swap')
finally show ?thesis .
qed
--- a/src/HOL/Analysis/Summation_Tests.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/Summation_Tests.thy Wed Apr 10 21:29:32 2019 +0100
@@ -209,7 +209,7 @@
from Bseq_mult[OF Bfun_const[of 2] this] have "Bseq (\<lambda>n. \<Sum>k<n. 2^Suc k * f (2^Suc k))"
by (simp add: sum_distrib_left sum_distrib_right mult_ac)
hence "Bseq (\<lambda>n. (\<Sum>k=Suc 0..<Suc n. 2^k * f (2^k)) + f 1)"
- by (intro Bseq_add, subst sum_shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
+ by (intro Bseq_add, subst sum.shift_bounds_Suc_ivl) (simp add: atLeast0LessThan)
hence "Bseq (\<lambda>n. (\<Sum>k=0..<Suc n. 2^k * f (2^k)))"
by (subst sum.atLeast_Suc_lessThan) (simp_all add: add_ac)
thus "Bseq (\<lambda>n. (\<Sum>k<n. 2^k * f (2^k)))"
@@ -354,7 +354,7 @@
by (intro sum_nonneg) auto
hence "norm (\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=Suc m..n. r * f k)" by simp
also have "(\<Sum>k=Suc m..n. r * f k) = (\<Sum>k=m..<n. r * f (Suc k))"
- by (subst sum_shift_bounds_Suc_ivl [symmetric])
+ by (subst sum.shift_bounds_Suc_ivl [symmetric])
(simp only: atLeastLessThanSuc_atLeastAtMost)
also from m have "\<dots> \<le> (\<Sum>k=m..<n. p k * f k - p (Suc k) * f (Suc k))"
by (intro sum_mono[OF less_imp_le]) simp_all
--- a/src/HOL/Analysis/ex/Approximations.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Analysis/ex/Approximations.thy Wed Apr 10 21:29:32 2019 +0100
@@ -29,7 +29,7 @@
have "(\<Sum>k<Suc m. f k * x^k) = f 0 + (\<Sum>k=Suc 0..<Suc m. f k * x^k)"
by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. f k * x^k) = (\<Sum>k<m. f (k+1) * x^k) * x"
- by (subst sum_shift_bounds_Suc_ivl)
+ by (subst sum.shift_bounds_Suc_ivl)
(simp add: sum_distrib_right algebra_simps atLeast0LessThan power_commutes)
finally have "(\<Sum>k<Suc m. f k * x ^ k) = f 0 + (\<Sum>k<m. f (k + 1) * x ^ k) * x" .
}
@@ -422,7 +422,7 @@
inverse (f 0) + (\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k))"
by (subst atLeast0LessThan [symmetric], subst sum.atLeast_Suc_lessThan) simp_all
also have "(\<Sum>k=Suc 0..<Suc m. inverse (f k * x^k)) = (\<Sum>k<m. inverse (f (k+1) * x^k)) / x"
- by (subst sum_shift_bounds_Suc_ivl)
+ by (subst sum.shift_bounds_Suc_ivl)
(simp add: sum_distrib_left divide_inverse algebra_simps
atLeast0LessThan power_commutes)
finally have "(\<Sum>k<Suc m. inverse (f k) * inverse (x ^ k)) =
--- a/src/HOL/Binomial.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Binomial.thy Wed Apr 10 21:29:32 2019 +0100
@@ -176,7 +176,7 @@
by (auto simp add: sum_distrib_left ac_simps)
also have "\<dots> = (\<Sum>k\<le>n. of_nat (n choose k) * a^k * b^(n + 1 - k)) +
(\<Sum>k=1..n+1. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k))"
- by (simp add: atMost_atLeast0 sum_shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum_cl_ivl_Suc)
+ by (simp add: atMost_atLeast0 sum.shift_bounds_cl_Suc_ivl Suc_diff_le field_simps del: sum.cl_ivl_Suc)
also have "\<dots> = a^(n + 1) + b^(n + 1) +
(\<Sum>k=1..n. of_nat (n choose (k - 1)) * a^k * b^(n + 1 - k)) +
(\<Sum>k=1..n. of_nat (n choose k) * a^k * b^(n + 1 - k))"
@@ -337,7 +337,7 @@
lemma gbinomial_0 [simp]:
"a gchoose 0 = 1"
"0 gchoose (Suc k) = 0"
- by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift)
+ by (simp_all add: gbinomial_prod_rev prod.atLeast0_lessThan_Suc_shift del: prod.op_ivl_Suc)
lemma gbinomial_Suc: "a gchoose (Suc k) = prod (\<lambda>i. a - of_nat i) {0..k} div fact (Suc k)"
by (simp add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
@@ -358,11 +358,14 @@
lemma gbinomial_pochhammer: "a gchoose k = (- 1) ^ k * pochhammer (- a) k / fact k"
for a :: "'a::field_char_0"
- by (cases k)
- (simp_all add: pochhammer_minus,
- simp_all add: gbinomial_prod_rev pochhammer_prod_rev
- power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
- prod.atLeast_Suc_atMost_Suc_shift of_nat_diff)
+proof (cases k)
+ case (Suc k')
+ then show ?thesis
+ apply (simp add: pochhammer_minus)
+ apply (simp add: gbinomial_prod_rev pochhammer_prod_rev power_mult_distrib [symmetric] atLeastLessThanSuc_atLeastAtMost
+ prod.atLeast_Suc_atMost_Suc_shift of_nat_diff del: prod.cl_ivl_Suc)
+ done
+qed auto
lemma gbinomial_pochhammer': "a gchoose k = pochhammer (a - of_nat k + 1) k / fact k"
for a :: "'a::field_char_0"
@@ -411,7 +414,7 @@
also have "\<dots> = ((\<Prod>i\<in>{0..<k} \<union> {k..<m + k}. of_nat (m + k - i)) :: 'a)"
by (simp add: ivl_disj_un)
finally have "fact n = (fact m * (\<Prod>i = 0..<k. of_nat m + of_nat k - of_nat i) :: 'a)"
- using prod_shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
+ using prod.shift_bounds_nat_ivl [of "\<lambda>i. of_nat (m + k - i) :: 'a" 0 k m]
by (simp add: fact_prod_rev [of m] prod.union_disjoint of_nat_diff)
then have "fact n / fact (n - k) = ((\<Prod>i = 0..<k. of_nat n - of_nat i) :: 'a)"
by (simp add: n)
@@ -465,7 +468,7 @@
by (simp add: Suc field_simps del: fact_Suc)
also have "\<dots> =
(a gchoose Suc h) * of_nat (Suc (Suc h) * fact (Suc h)) + (\<Prod>i=0..Suc h. a - of_nat i)"
- apply (simp del: fact_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
+ apply (simp del: fact_Suc prod.op_ivl_Suc add: gbinomial_mult_fact field_simps mult.left_commute [of _ "2"])
apply (simp del: fact_Suc add: fact_Suc [of "Suc h"] field_simps gbinomial_mult_fact
mult.left_commute [of _ "2"] atLeastLessThanSuc_atLeastAtMost)
done
@@ -487,7 +490,7 @@
by (simp add: field_simps Suc atLeastLessThanSuc_atLeastAtMost)
also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
using eq0
- by (simp add: Suc prod.atLeast0_atMost_Suc_shift)
+ by (simp add: Suc prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc)
also have "\<dots> = (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
by (simp only: gbinomial_mult_fact atLeastLessThanSuc_atLeastAtMost)
finally show ?thesis
@@ -536,7 +539,7 @@
have "(\<Sum>i\<le>n. i * (n choose i)) = (\<Sum>i\<le>Suc m. i * (Suc m choose i))"
by (simp add: Suc)
also have "\<dots> = Suc m * 2 ^ m"
- unfolding sum_atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric]
+ unfolding sum.atMost_Suc_shift Suc_times_binomial sum_distrib_left[symmetric]
by (simp add: choose_row_sum)
finally show ?thesis
using Suc by simp
@@ -556,7 +559,7 @@
(\<Sum>i\<le>Suc m. (-1) ^ i * of_nat i * of_nat (Suc m choose i))"
by (simp add: Suc)
also have "\<dots> = (\<Sum>i\<le>m. (-1) ^ (Suc i) * of_nat (Suc i * (Suc m choose Suc i)))"
- by (simp only: sum_atMost_Suc_shift sum_distrib_left[symmetric] mult_ac of_nat_mult) simp
+ by (simp only: sum.atMost_Suc_shift sum_distrib_left[symmetric] mult_ac of_nat_mult) simp
also have "\<dots> = - of_nat (Suc m) * (\<Sum>i\<le>m. (-1) ^ i * of_nat (m choose i))"
by (subst sum_distrib_left, rule sum.cong[OF refl], subst Suc_times_binomial)
(simp add: algebra_simps)
@@ -597,7 +600,7 @@
(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
((\<Sum>i\<le>n. of_nat (n choose Suc i) * pochhammer a (Suc i) * pochhammer b (n - i)) +
pochhammer b (Suc n))"
- by (subst sum_atMost_Suc_shift) (simp add: ring_distribs sum.distrib)
+ by (subst sum.atMost_Suc_shift) (simp add: ring_distribs sum.distrib)
also have "(\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a (Suc i) * pochhammer b (n - i)) =
a * pochhammer ((a + 1) + b) n"
by (subst Suc) (simp add: sum_distrib_left pochhammer_rec mult_ac)
@@ -606,7 +609,7 @@
(\<Sum>i=0..Suc n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
apply (subst sum.atLeast_Suc_atMost)
apply simp
- apply (subst sum_shift_bounds_cl_Suc_ivl)
+ apply (subst sum.shift_bounds_cl_Suc_ivl)
apply (simp add: atLeast0AtMost)
done
also have "\<dots> = (\<Sum>i\<le>n. of_nat (n choose i) * pochhammer a i * pochhammer b (Suc n - i))"
@@ -675,7 +678,7 @@
then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0..Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(\<Prod>i = 0..Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
- by (simp add: prod.atLeast0_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc)
also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
finally show ?thesis by (simp add: Suc field_simps del: of_nat_Suc)
@@ -690,7 +693,7 @@
then have "((a + 1) gchoose (Suc (Suc b))) = (\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) / fact (b + 2)"
by (simp add: field_simps gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost)
also have "(\<Prod>i = 0 .. Suc b. a + (1 - of_nat i)) = (a + 1) * (\<Prod>i = 0..b. a - of_nat i)"
- by (simp add: prod.atLeast0_atMost_Suc_shift)
+ by (simp add: prod.atLeast0_atMost_Suc_shift del: prod.cl_ivl_Suc)
also have "\<dots> / fact (b + 2) = (a + 1) / of_nat (Suc (Suc b)) * (a gchoose Suc b)"
by (simp_all add: gbinomial_prod_rev atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
finally show ?thesis
@@ -860,7 +863,7 @@
have "S (Suc mm) = G (Suc mm) 0 + (\<Sum>k=Suc 0..Suc mm. G (Suc mm) k)"
using SG_def by (simp add: sum.atLeast_Suc_atMost atLeast0AtMost [symmetric])
also have "(\<Sum>k=Suc 0..Suc mm. G (Suc mm) k) = (\<Sum>k=0..mm. G (Suc mm) (Suc k))"
- by (subst sum_shift_bounds_cl_Suc_ivl) simp
+ by (subst sum.shift_bounds_cl_Suc_ivl) simp
also have "\<dots> = (\<Sum>k=0..mm. ((of_nat mm + a gchoose (Suc k)) +
(of_nat mm + a gchoose k)) * x^(Suc k) * y^(mm - k))"
unfolding G_def by (subst gbinomial_addition_formula) simp
@@ -929,11 +932,11 @@
also have "(\<Sum>k = 0..(2 * m + 1). (2 * m + 1 choose k)) =
(\<Sum>k = 0..m. (2 * m + 1 choose k)) +
(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k))"
- using sum_ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"]
+ using sum.ub_add_nat[of 0 m "\<lambda>k. 2 * m + 1 choose k" "m+1"]
by (simp add: mult_2)
also have "(\<Sum>k = m+1..2*m+1. (2 * m + 1 choose k)) =
(\<Sum>k = 0..m. (2 * m + 1 choose (k + (m + 1))))"
- by (subst sum_shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
+ by (subst sum.shift_bounds_cl_nat_ivl [symmetric]) (simp add: mult_2)
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose (m - k)))"
by (intro sum.cong[OF refl], subst binomial_symmetric) simp_all
also have "\<dots> = (\<Sum>k = 0..m. (2 * m + 1 choose k))"
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1125,7 +1125,7 @@
using sum.atLeast_Suc_atMost[of 0 "n+1" "\<lambda>i. a$i * b$(n+1-i)"]
by (simp add: fps_mult_nth nth_less_subdegree_zero)
thus "fps_shift 1 (a*b) $ n = (fps_shift 1 a * b) $ n"
- using sum_shift_bounds_cl_Suc_ivl[of "\<lambda>i. a$i * b$(n+1-i)" 0 n]
+ using sum.shift_bounds_cl_Suc_ivl[of "\<lambda>i. a$i * b$(n+1-i)" 0 n]
by (simp add: fps_mult_nth)
qed
have "n \<le> subdegree g \<Longrightarrow> fps_shift n (g*h) = fps_shift n g * h"
@@ -2220,7 +2220,7 @@
"fps_left_inverse (f^2) 1 $ Suc (Suc (Suc k)) =
fps_left_inverse (f\<^sup>2) 1 $ Suc (Suc k) * of_nat 2 -
fps_left_inverse (f\<^sup>2) 1 $ Suc k"
- using sum_ub_add_nat f2_nth_simps(1,2) by simp
+ using sum.ub_add_nat f2_nth_simps(1,2) by simp
also have "\<dots> = of_nat (2 * Suc (Suc (Suc k))) - of_nat (Suc (Suc k))"
by (subst A, subst B) (simp add: invf2_def mult.commute)
also have "\<dots> = of_nat (Suc (Suc (Suc k)) + 1)"
@@ -4136,7 +4136,7 @@
from v have "k = sum_list v" by (simp add: A_def natpermute_def)
also have "\<dots> = (\<Sum>i=0..m. v ! i)"
- by (simp add: sum_list_sum_nth atLeastLessThanSuc_atLeastAtMost del: sum_op_ivl_Suc)
+ by (simp add: sum_list_sum_nth atLeastLessThanSuc_atLeastAtMost del: sum.op_ivl_Suc)
also from j have "{0..m} = insert j ({0..m}-{j})" by auto
also from j have "(\<Sum>i\<in>\<dots>. v ! i) = k + (\<Sum>i\<in>{0..m}-{j}. v ! i)"
by (subst sum.insert) simp_all
@@ -5927,10 +5927,10 @@
done
have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}"
apply (simp add: pochhammer_minus field_simps m)
- apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift)
+ apply (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift simp del: prod.cl_ivl_Suc)
done
have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
- using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift)
+ using kn apply (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift del: prod.op_ivl_Suc del: prod.cl_ivl_Suc)
using prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a]
apply (auto simp add: of_nat_diff field_simps)
done
--- a/src/HOL/Computational_Algebra/Polynomial.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Wed Apr 10 21:29:32 2019 +0100
@@ -523,7 +523,7 @@
also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
by (simp add: field_simps sum_distrib_left coeff_pCons)
- also note sum_atMost_Suc_shift[symmetric]
+ also note sum.atMost_Suc_shift[symmetric]
also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
finally show ?thesis .
qed
@@ -1000,7 +1000,7 @@
next
case (pCons a p n)
then show ?case
- by (cases n) (simp_all add: sum_atMost_Suc_shift del: sum.atMost_Suc)
+ by (cases n) (simp_all add: sum.atMost_Suc_shift del: sum.atMost_Suc)
qed
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q"
--- a/src/HOL/Decision_Procs/Approximation.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1182,7 +1182,7 @@
hence prod_head_Suc: "\<And>k i. \<Prod>{k ..< k + Suc i} = k * \<Prod>{Suc k ..< Suc k + i}"
by auto
have sum_move0: "\<And>k F. sum F {0..<Suc k} = F 0 + sum (\<lambda> k. F (Suc k)) {0..<k}"
- unfolding sum_shift_bounds_Suc_ivl[symmetric]
+ unfolding sum.shift_bounds_Suc_ivl[symmetric]
unfolding sum.atLeast_Suc_lessThan[OF zero_less_Suc] ..
define C where "C = xs!x - c"
@@ -1253,7 +1253,7 @@
proof (cases "xs ! x = c")
case True
from True[symmetric] hyp[OF bnd_xs] Suc show ?thesis
- unfolding F_def Suc sum.atLeast_Suc_lessThan[OF zero_less_Suc] sum_shift_bounds_Suc_ivl
+ unfolding F_def Suc sum.atLeast_Suc_lessThan[OF zero_less_Suc] sum.shift_bounds_Suc_ivl
by auto
next
case False
--- a/src/HOL/Factorial.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Factorial.thy Wed Apr 10 21:29:32 2019 +0100
@@ -21,15 +21,17 @@
where fact_prod: "fact n = of_nat (\<Prod>{1..n})"
lemma fact_prod_Suc: "fact n = of_nat (prod Suc {0..<n})"
- by (cases n)
- (simp_all add: fact_prod prod.atLeast_Suc_atMost_Suc_shift
- atLeastLessThanSuc_atLeastAtMost)
+ unfolding fact_prod using atLeast0LessThan prod.atLeast1_atMost_eq by auto
lemma fact_prod_rev: "fact n = of_nat (\<Prod>i = 0..<n. n - i)"
- using prod.atLeastAtMost_rev [of "\<lambda>i. i" 1 n]
- by (cases n)
- (simp_all add: fact_prod_Suc prod.atLeast_Suc_atMost_Suc_shift
- atLeastLessThanSuc_atLeastAtMost)
+proof -
+ have "prod Suc {0..<n} = \<Prod>{1..n}"
+ by (simp add: atLeast0LessThan prod.atLeast1_atMost_eq)
+ then have "prod Suc {0..<n} = prod ((-) (n + 1)) {1..n}"
+ using prod.atLeastAtMost_rev [of "\<lambda>i. i" 1 n] by presburger
+ then show ?thesis
+ unfolding fact_prod_Suc by (simp add: atLeast0LessThan prod.atLeast1_atMost_eq)
+qed
lemma fact_0 [simp]: "fact 0 = 1"
by (simp add: fact_prod)
@@ -216,7 +218,8 @@
by (simp add: pochhammer_prod atLeastLessThanSuc_atLeastAtMost)
lemma pochhammer_Suc_prod_rev: "pochhammer a (Suc n) = prod (\<lambda>i. a + of_nat (n - i)) {0..n}"
- by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift)
+ using prod.atLeast_Suc_atMost_Suc_shift
+ by (simp add: pochhammer_prod_rev prod.atLeast_Suc_atMost_Suc_shift del: prod.cl_ivl_Suc)
lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
by (simp add: pochhammer_prod)
@@ -259,7 +262,7 @@
end
lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
- by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps)
+ by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc_shift ac_simps del: prod.op_ivl_Suc)
lemma pochhammer_rec': "pochhammer z (Suc n) = (z + of_nat n) * pochhammer z n"
by (simp add: pochhammer_prod prod.atLeast0_lessThan_Suc ac_simps)
--- a/src/HOL/Homology/Homology.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Homology/Homology.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1,5 +1,5 @@
theory Homology
- imports Brouwer_Degree
+ imports Invariance_of_Domain
begin
end
--- a/src/HOL/Homology/Invariance_of_Domain.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Homology/Invariance_of_Domain.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1,7 +1,7 @@
section\<open>Invariance of Domain\<close>
theory Invariance_of_Domain
- imports Brouwer_Degree
+ imports Brouwer_Degree "HOL-Analysis.Continuous_Extension" "HOL-Analysis.Homeomorphism"
begin
@@ -2426,4 +2426,549 @@
by (simp add: eq)
qed
+lemma invariance_of_domain_homeomorphism:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+ obtains g where "homeomorphism S (f ` S) f g"
+proof
+ show "homeomorphism S (f ` S) f (inv_into S f)"
+ by (simp add: assms continuous_on_inverse_open homeomorphism_def)
+qed
+
+corollary invariance_of_domain_homeomorphic:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "open S" "continuous_on S f" "DIM('b) \<le> DIM('a)" "inj_on f S"
+ shows "S homeomorphic (f ` S)"
+ using%unimportant invariance_of_domain_homeomorphism [OF assms]
+ by%unimportant (meson homeomorphic_def)
+
+lemma continuous_image_subset_interior:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes "continuous_on S f" "inj_on f S" "DIM('b) \<le> DIM('a)"
+ shows "f ` (interior S) \<subseteq> interior(f ` S)"
+proof (rule interior_maximal)
+ show "f ` interior S \<subseteq> f ` S"
+ by (simp add: image_mono interior_subset)
+ show "open (f ` interior S)"
+ using assms
+ by (auto simp: subset_inj_on interior_subset continuous_on_subset invariance_of_domain_gen)
+qed
+
+lemma homeomorphic_interiors_same_dimension:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" and dimeq: "DIM('a) = DIM('b)"
+ shows "(interior S) homeomorphic (interior T)"
+ using assms [unfolded homeomorphic_minimal]
+ unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+ fix f g
+ assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+ by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+ have fim: "f ` interior S \<subseteq> interior T"
+ using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
+ have gim: "g ` interior T \<subseteq> interior S"
+ using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
+ show "homeomorphism (interior S) (interior T) f g"
+ unfolding homeomorphism_def
+ proof (intro conjI ballI)
+ show "\<And>x. x \<in> interior S \<Longrightarrow> g (f x) = x"
+ by (meson \<open>\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x\<close> subsetD interior_subset)
+ have "interior T \<subseteq> f ` interior S"
+ proof
+ fix x assume "x \<in> interior T"
+ then have "g x \<in> interior S"
+ using gim by blast
+ then show "x \<in> f ` interior S"
+ by (metis T \<open>x \<in> interior T\<close> image_iff interior_subset subsetCE)
+ qed
+ then show "f ` interior S = interior T"
+ using fim by blast
+ show "continuous_on (interior S) f"
+ by (metis interior_subset continuous_on_subset contf)
+ show "\<And>y. y \<in> interior T \<Longrightarrow> f (g y) = y"
+ by (meson T subsetD interior_subset)
+ have "interior S \<subseteq> g ` interior T"
+ proof
+ fix x assume "x \<in> interior S"
+ then have "f x \<in> interior T"
+ using fim by blast
+ then show "x \<in> g ` interior T"
+ by (metis S \<open>x \<in> interior S\<close> image_iff interior_subset subsetCE)
+ qed
+ then show "g ` interior T = interior S"
+ using gim by blast
+ show "continuous_on (interior T) g"
+ by (metis interior_subset continuous_on_subset contg)
+ qed
+qed
+
+lemma homeomorphic_open_imp_same_dimension:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "open S" "S \<noteq> {}" "open T" "T \<noteq> {}"
+ shows "DIM('a) = DIM('b)"
+ using assms
+ apply (simp add: homeomorphic_minimal)
+ apply (rule order_antisym; metis inj_onI invariance_of_dimension)
+ done
+
+proposition homeomorphic_interiors:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "interior S = {} \<longleftrightarrow> interior T = {}"
+ shows "(interior S) homeomorphic (interior T)"
+proof (cases "interior T = {}")
+ case True
+ with assms show ?thesis by auto
+next
+ case False
+ then have "DIM('a) = DIM('b)"
+ using assms
+ apply (simp add: homeomorphic_minimal)
+ apply (rule order_antisym; metis continuous_on_subset inj_onI inj_on_subset interior_subset invariance_of_dimension open_interior)
+ done
+ then show ?thesis
+ by (rule homeomorphic_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+lemma homeomorphic_frontiers_same_dimension:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "closed S" "closed T" and dimeq: "DIM('a) = DIM('b)"
+ shows "(frontier S) homeomorphic (frontier T)"
+ using assms [unfolded homeomorphic_minimal]
+ unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+ fix f g
+ assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+ by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+ have "g ` interior T \<subseteq> interior S"
+ using continuous_image_subset_interior [OF contg \<open>inj_on g T\<close>] dimeq gTS by simp
+ then have fim: "f ` frontier S \<subseteq> frontier T"
+ apply (simp add: frontier_def)
+ using continuous_image_subset_interior assms(2) assms(3) S by auto
+ have "f ` interior S \<subseteq> interior T"
+ using continuous_image_subset_interior [OF contf \<open>inj_on f S\<close>] dimeq fST by simp
+ then have gim: "g ` frontier T \<subseteq> frontier S"
+ apply (simp add: frontier_def)
+ using continuous_image_subset_interior T assms(2) assms(3) by auto
+ show "homeomorphism (frontier S) (frontier T) f g"
+ unfolding homeomorphism_def
+ proof (intro conjI ballI)
+ show gf: "\<And>x. x \<in> frontier S \<Longrightarrow> g (f x) = x"
+ by (simp add: S assms(2) frontier_def)
+ show fg: "\<And>y. y \<in> frontier T \<Longrightarrow> f (g y) = y"
+ by (simp add: T assms(3) frontier_def)
+ have "frontier T \<subseteq> f ` frontier S"
+ proof
+ fix x assume "x \<in> frontier T"
+ then have "g x \<in> frontier S"
+ using gim by blast
+ then show "x \<in> f ` frontier S"
+ by (metis fg \<open>x \<in> frontier T\<close> imageI)
+ qed
+ then show "f ` frontier S = frontier T"
+ using fim by blast
+ show "continuous_on (frontier S) f"
+ by (metis Diff_subset assms(2) closure_eq contf continuous_on_subset frontier_def)
+ have "frontier S \<subseteq> g ` frontier T"
+ proof
+ fix x assume "x \<in> frontier S"
+ then have "f x \<in> frontier T"
+ using fim by blast
+ then show "x \<in> g ` frontier T"
+ by (metis gf \<open>x \<in> frontier S\<close> imageI)
+ qed
+ then show "g ` frontier T = frontier S"
+ using gim by blast
+ show "continuous_on (frontier T) g"
+ by (metis Diff_subset assms(3) closure_closed contg continuous_on_subset frontier_def)
+ qed
+qed
+
+lemma homeomorphic_frontiers:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "closed S" "closed T"
+ "interior S = {} \<longleftrightarrow> interior T = {}"
+ shows "(frontier S) homeomorphic (frontier T)"
+proof (cases "interior T = {}")
+ case True
+ then show ?thesis
+ by (metis Diff_empty assms closure_eq frontier_def)
+next
+ case False
+ show ?thesis
+ apply (rule homeomorphic_frontiers_same_dimension)
+ apply (simp_all add: assms)
+ using False assms homeomorphic_interiors homeomorphic_open_imp_same_dimension by blast
+qed
+
+lemma continuous_image_subset_rel_interior:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ and TS: "aff_dim T \<le> aff_dim S"
+ shows "f ` (rel_interior S) \<subseteq> rel_interior(f ` S)"
+proof (rule rel_interior_maximal)
+ show "f ` rel_interior S \<subseteq> f ` S"
+ by(simp add: image_mono rel_interior_subset)
+ show "openin (top_of_set (affine hull f ` S)) (f ` rel_interior S)"
+ proof (rule invariance_of_domain_affine_sets)
+ show "openin (top_of_set (affine hull S)) (rel_interior S)"
+ by (simp add: openin_rel_interior)
+ show "aff_dim (affine hull f ` S) \<le> aff_dim (affine hull S)"
+ by (metis aff_dim_affine_hull aff_dim_subset fim TS order_trans)
+ show "f ` rel_interior S \<subseteq> affine hull f ` S"
+ by (meson \<open>f ` rel_interior S \<subseteq> f ` S\<close> hull_subset order_trans)
+ show "continuous_on (rel_interior S) f"
+ using contf continuous_on_subset rel_interior_subset by blast
+ show "inj_on f (rel_interior S)"
+ using inj_on_subset injf rel_interior_subset by blast
+ qed auto
+qed
+
+lemma homeomorphic_rel_interiors_same_dimension:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
+ shows "(rel_interior S) homeomorphic (rel_interior T)"
+ using assms [unfolded homeomorphic_minimal]
+ unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+ fix f g
+ assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+ by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+ have fim: "f ` rel_interior S \<subseteq> rel_interior T"
+ by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+ have gim: "g ` rel_interior T \<subseteq> rel_interior S"
+ by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+ show "homeomorphism (rel_interior S) (rel_interior T) f g"
+ unfolding homeomorphism_def
+ proof (intro conjI ballI)
+ show gf: "\<And>x. x \<in> rel_interior S \<Longrightarrow> g (f x) = x"
+ using S rel_interior_subset by blast
+ show fg: "\<And>y. y \<in> rel_interior T \<Longrightarrow> f (g y) = y"
+ using T mem_rel_interior_ball by blast
+ have "rel_interior T \<subseteq> f ` rel_interior S"
+ proof
+ fix x assume "x \<in> rel_interior T"
+ then have "g x \<in> rel_interior S"
+ using gim by blast
+ then show "x \<in> f ` rel_interior S"
+ by (metis fg \<open>x \<in> rel_interior T\<close> imageI)
+ qed
+ moreover have "f ` rel_interior S \<subseteq> rel_interior T"
+ by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+ ultimately show "f ` rel_interior S = rel_interior T"
+ by blast
+ show "continuous_on (rel_interior S) f"
+ using contf continuous_on_subset rel_interior_subset by blast
+ have "rel_interior S \<subseteq> g ` rel_interior T"
+ proof
+ fix x assume "x \<in> rel_interior S"
+ then have "f x \<in> rel_interior T"
+ using fim by blast
+ then show "x \<in> g ` rel_interior T"
+ by (metis gf \<open>x \<in> rel_interior S\<close> imageI)
+ qed
+ then show "g ` rel_interior T = rel_interior S"
+ using gim by blast
+ show "continuous_on (rel_interior T) g"
+ using contg continuous_on_subset rel_interior_subset by blast
+ qed
+qed
+
+lemma homeomorphic_rel_interiors:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
+ shows "(rel_interior S) homeomorphic (rel_interior T)"
+proof (cases "rel_interior T = {}")
+ case True
+ with assms show ?thesis by auto
+next
+ case False
+ obtain f g
+ where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ using assms [unfolded homeomorphic_minimal] by auto
+ have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+ apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
+ apply (simp_all add: openin_rel_interior False assms)
+ using contf continuous_on_subset rel_interior_subset apply blast
+ apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+ apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
+ done
+ moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
+ apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
+ apply (simp_all add: openin_rel_interior False assms)
+ using contg continuous_on_subset rel_interior_subset apply blast
+ apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
+ apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
+ done
+ ultimately have "aff_dim S = aff_dim T" by force
+ then show ?thesis
+ by (rule homeomorphic_rel_interiors_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+
+lemma homeomorphic_rel_boundaries_same_dimension:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" and aff: "aff_dim S = aff_dim T"
+ shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
+ using assms [unfolded homeomorphic_minimal]
+ unfolding homeomorphic_def
+proof (clarify elim!: ex_forward)
+ fix f g
+ assume S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ then have fST: "f ` S = T" and gTS: "g ` T = S" and "inj_on f S" "inj_on g T"
+ by (auto simp: inj_on_def intro: rev_image_eqI) metis+
+ have fim: "f ` rel_interior S \<subseteq> rel_interior T"
+ by (metis \<open>inj_on f S\<close> aff contf continuous_image_subset_rel_interior fST order_refl)
+ have gim: "g ` rel_interior T \<subseteq> rel_interior S"
+ by (metis \<open>inj_on g T\<close> aff contg continuous_image_subset_rel_interior gTS order_refl)
+ show "homeomorphism (S - rel_interior S) (T - rel_interior T) f g"
+ unfolding homeomorphism_def
+ proof (intro conjI ballI)
+ show gf: "\<And>x. x \<in> S - rel_interior S \<Longrightarrow> g (f x) = x"
+ using S rel_interior_subset by blast
+ show fg: "\<And>y. y \<in> T - rel_interior T \<Longrightarrow> f (g y) = y"
+ using T mem_rel_interior_ball by blast
+ show "f ` (S - rel_interior S) = T - rel_interior T"
+ using S fST fim gim by auto
+ show "continuous_on (S - rel_interior S) f"
+ using contf continuous_on_subset rel_interior_subset by blast
+ show "g ` (T - rel_interior T) = S - rel_interior S"
+ using T gTS gim fim by auto
+ show "continuous_on (T - rel_interior T) g"
+ using contg continuous_on_subset rel_interior_subset by blast
+ qed
+qed
+
+lemma homeomorphic_rel_boundaries:
+ fixes S :: "'a::euclidean_space set" and T :: "'b::euclidean_space set"
+ assumes "S homeomorphic T" "rel_interior S = {} \<longleftrightarrow> rel_interior T = {}"
+ shows "(S - rel_interior S) homeomorphic (T - rel_interior T)"
+proof (cases "rel_interior T = {}")
+ case True
+ with assms show ?thesis by auto
+next
+ case False
+ obtain f g
+ where S: "\<forall>x\<in>S. f x \<in> T \<and> g (f x) = x" and T: "\<forall>y\<in>T. g y \<in> S \<and> f (g y) = y"
+ and contf: "continuous_on S f" and contg: "continuous_on T g"
+ using assms [unfolded homeomorphic_minimal] by auto
+ have "aff_dim (affine hull S) \<le> aff_dim (affine hull T)"
+ apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior S" _ f])
+ apply (simp_all add: openin_rel_interior False assms)
+ using contf continuous_on_subset rel_interior_subset apply blast
+ apply (meson S hull_subset image_subsetI rel_interior_subset rev_subsetD)
+ apply (metis S inj_on_inverseI inj_on_subset rel_interior_subset)
+ done
+ moreover have "aff_dim (affine hull T) \<le> aff_dim (affine hull S)"
+ apply (rule invariance_of_dimension_affine_sets [of _ "rel_interior T" _ g])
+ apply (simp_all add: openin_rel_interior False assms)
+ using contg continuous_on_subset rel_interior_subset apply blast
+ apply (meson T hull_subset image_subsetI rel_interior_subset rev_subsetD)
+ apply (metis T inj_on_inverseI inj_on_subset rel_interior_subset)
+ done
+ ultimately have "aff_dim S = aff_dim T" by force
+ then show ?thesis
+ by (rule homeomorphic_rel_boundaries_same_dimension [OF \<open>S homeomorphic T\<close>])
+qed
+
+proposition uniformly_continuous_homeomorphism_UNIV_trivial:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'a"
+ assumes contf: "uniformly_continuous_on S f" and hom: "homeomorphism S UNIV f g"
+ shows "S = UNIV"
+proof (cases "S = {}")
+ case True
+ then show ?thesis
+ by (metis UNIV_I hom empty_iff homeomorphism_def image_eqI)
+next
+ case False
+ have "inj g"
+ by (metis UNIV_I hom homeomorphism_apply2 injI)
+ then have "open (g ` UNIV)"
+ by (blast intro: invariance_of_domain hom homeomorphism_cont2)
+ then have "open S"
+ using hom homeomorphism_image2 by blast
+ moreover have "complete S"
+ unfolding complete_def
+ proof clarify
+ fix \<sigma>
+ assume \<sigma>: "\<forall>n. \<sigma> n \<in> S" and "Cauchy \<sigma>"
+ have "Cauchy (f o \<sigma>)"
+ using uniformly_continuous_imp_Cauchy_continuous \<open>Cauchy \<sigma>\<close> \<sigma> contf by blast
+ then obtain l where "(f \<circ> \<sigma>) \<longlonglongrightarrow> l"
+ by (auto simp: convergent_eq_Cauchy [symmetric])
+ show "\<exists>l\<in>S. \<sigma> \<longlonglongrightarrow> l"
+ proof
+ show "g l \<in> S"
+ using hom homeomorphism_image2 by blast
+ have "(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l"
+ by (meson UNIV_I \<open>(f \<circ> \<sigma>) \<longlonglongrightarrow> l\<close> continuous_on_sequentially hom homeomorphism_cont2)
+ then show "\<sigma> \<longlonglongrightarrow> g l"
+ proof -
+ have "\<forall>n. \<sigma> n = (g \<circ> (f \<circ> \<sigma>)) n"
+ by (metis (no_types) \<sigma> comp_eq_dest_lhs hom homeomorphism_apply1)
+ then show ?thesis
+ by (metis (no_types) LIMSEQ_iff \<open>(g \<circ> (f \<circ> \<sigma>)) \<longlonglongrightarrow> g l\<close>)
+ qed
+ qed
+ qed
+ then have "closed S"
+ by (simp add: complete_eq_closed)
+ ultimately show ?thesis
+ using clopen [of S] False by simp
+qed
+
+proposition invariance_of_domain_sphere_affine_set_gen:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ and U: "bounded U" "convex U"
+ and "affine T" and affTU: "aff_dim T < aff_dim U"
+ and ope: "openin (top_of_set (rel_frontier U)) S"
+ shows "openin (top_of_set T) (f ` S)"
+proof (cases "rel_frontier U = {}")
+ case True
+ then show ?thesis
+ using ope openin_subset by force
+next
+ case False
+ obtain b c where b: "b \<in> rel_frontier U" and c: "c \<in> rel_frontier U" and "b \<noteq> c"
+ using \<open>bounded U\<close> rel_frontier_not_sing [of U] subset_singletonD False by fastforce
+ obtain V :: "'a set" where "affine V" and affV: "aff_dim V = aff_dim U - 1"
+ proof (rule choose_affine_subset [OF affine_UNIV])
+ show "- 1 \<le> aff_dim U - 1"
+ by (metis aff_dim_empty aff_dim_geq aff_dim_negative_iff affTU diff_0 diff_right_mono not_le)
+ show "aff_dim U - 1 \<le> aff_dim (UNIV::'a set)"
+ by (metis aff_dim_UNIV aff_dim_le_DIM le_cases not_le zle_diff1_eq)
+ qed auto
+ have SU: "S \<subseteq> rel_frontier U"
+ using ope openin_imp_subset by auto
+ have homb: "rel_frontier U - {b} homeomorphic V"
+ and homc: "rel_frontier U - {c} homeomorphic V"
+ using homeomorphic_punctured_sphere_affine_gen [of U _ V]
+ by (simp_all add: \<open>affine V\<close> affV U b c)
+ then obtain g h j k
+ where gh: "homeomorphism (rel_frontier U - {b}) V g h"
+ and jk: "homeomorphism (rel_frontier U - {c}) V j k"
+ by (auto simp: homeomorphic_def)
+ with SU have hgsub: "(h ` g ` (S - {b})) \<subseteq> S" and kjsub: "(k ` j ` (S - {c})) \<subseteq> S"
+ by (simp_all add: homeomorphism_def subset_eq)
+ have [simp]: "aff_dim T \<le> aff_dim V"
+ by (simp add: affTU affV)
+ have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}))"
+ proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
+ show "openin (top_of_set V) (g ` (S - {b}))"
+ apply (rule homeomorphism_imp_open_map [OF gh])
+ by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
+ show "continuous_on (g ` (S - {b})) (f \<circ> h)"
+ apply (rule continuous_on_compose)
+ apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets gh set_eq_subset)
+ using contf continuous_on_subset hgsub by blast
+ show "inj_on (f \<circ> h) (g ` (S - {b}))"
+ using kjsub
+ apply (clarsimp simp add: inj_on_def)
+ by (metis SU b homeomorphism_def inj_onD injf insert_Diff insert_iff gh rev_subsetD)
+ show "(f \<circ> h) ` g ` (S - {b}) \<subseteq> T"
+ by (metis fim image_comp image_mono hgsub subset_trans)
+ qed (auto simp: assms)
+ moreover
+ have "openin (top_of_set T) ((f \<circ> k) ` j ` (S - {c}))"
+ proof (rule invariance_of_domain_affine_sets [OF _ \<open>affine V\<close>])
+ show "openin (top_of_set V) (j ` (S - {c}))"
+ apply (rule homeomorphism_imp_open_map [OF jk])
+ by (meson Diff_mono Diff_subset SU ope openin_delete openin_subset_trans order_refl)
+ show "continuous_on (j ` (S - {c})) (f \<circ> k)"
+ apply (rule continuous_on_compose)
+ apply (meson Diff_mono SU homeomorphism_def homeomorphism_of_subsets jk set_eq_subset)
+ using contf continuous_on_subset kjsub by blast
+ show "inj_on (f \<circ> k) (j ` (S - {c}))"
+ using kjsub
+ apply (clarsimp simp add: inj_on_def)
+ by (metis SU c homeomorphism_def inj_onD injf insert_Diff insert_iff jk rev_subsetD)
+ show "(f \<circ> k) ` j ` (S - {c}) \<subseteq> T"
+ by (metis fim image_comp image_mono kjsub subset_trans)
+ qed (auto simp: assms)
+ ultimately have "openin (top_of_set T) ((f \<circ> h) ` g ` (S - {b}) \<union> ((f \<circ> k) ` j ` (S - {c})))"
+ by (rule openin_Un)
+ moreover have "(f \<circ> h) ` g ` (S - {b}) = f ` (S - {b})"
+ proof -
+ have "h ` g ` (S - {b}) = (S - {b})"
+ proof
+ show "h ` g ` (S - {b}) \<subseteq> S - {b}"
+ using homeomorphism_apply1 [OF gh] SU
+ by (fastforce simp add: image_iff image_subset_iff)
+ show "S - {b} \<subseteq> h ` g ` (S - {b})"
+ apply clarify
+ by (metis SU subsetD homeomorphism_apply1 [OF gh] image_iff member_remove remove_def)
+ qed
+ then show ?thesis
+ by (metis image_comp)
+ qed
+ moreover have "(f \<circ> k) ` j ` (S - {c}) = f ` (S - {c})"
+ proof -
+ have "k ` j ` (S - {c}) = (S - {c})"
+ proof
+ show "k ` j ` (S - {c}) \<subseteq> S - {c}"
+ using homeomorphism_apply1 [OF jk] SU
+ by (fastforce simp add: image_iff image_subset_iff)
+ show "S - {c} \<subseteq> k ` j ` (S - {c})"
+ apply clarify
+ by (metis SU subsetD homeomorphism_apply1 [OF jk] image_iff member_remove remove_def)
+ qed
+ then show ?thesis
+ by (metis image_comp)
+ qed
+ moreover have "f ` (S - {b}) \<union> f ` (S - {c}) = f ` (S)"
+ using \<open>b \<noteq> c\<close> by blast
+ ultimately show ?thesis
+ by simp
+qed
+
+lemma invariance_of_domain_sphere_affine_set:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on S f" and injf: "inj_on f S" and fim: "f ` S \<subseteq> T"
+ and "r \<noteq> 0" "affine T" and affTU: "aff_dim T < DIM('a)"
+ and ope: "openin (top_of_set (sphere a r)) S"
+ shows "openin (top_of_set T) (f ` S)"
+proof (cases "sphere a r = {}")
+ case True
+ then show ?thesis
+ using ope openin_subset by force
+next
+ case False
+ show ?thesis
+ proof (rule invariance_of_domain_sphere_affine_set_gen [OF contf injf fim bounded_cball convex_cball \<open>affine T\<close>])
+ show "aff_dim T < aff_dim (cball a r)"
+ by (metis False affTU aff_dim_cball assms(4) linorder_cases sphere_empty)
+ show "openin (top_of_set (rel_frontier (cball a r))) S"
+ by (simp add: \<open>r \<noteq> 0\<close> ope)
+ qed
+qed
+
+lemma no_embedding_sphere_lowdim:
+ fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+ assumes contf: "continuous_on (sphere a r) f" and injf: "inj_on f (sphere a r)" and "r > 0"
+ shows "DIM('a) \<le> DIM('b)"
+proof -
+ have "False" if "DIM('a) > DIM('b)"
+ proof -
+ have "compact (f ` sphere a r)"
+ using compact_continuous_image
+ by (simp add: compact_continuous_image contf)
+ then have "\<not> open (f ` sphere a r)"
+ using compact_open
+ by (metis assms(3) image_is_empty not_less_iff_gr_or_eq sphere_eq_empty)
+ then show False
+ using invariance_of_domain_sphere_affine_set [OF contf injf subset_UNIV] \<open>r > 0\<close>
+ by (metis aff_dim_UNIV affine_UNIV less_irrefl of_nat_less_iff open_openin openin_subtopology_self subtopology_UNIV that)
+ qed
+ then show ?thesis
+ using not_less by blast
+qed
+
end
\ No newline at end of file
--- a/src/HOL/Homology/Simplices.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Homology/Simplices.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1190,7 +1190,7 @@
by (simp add: oriented_simplex_def standard_simplex_def)
have "oriented_simplex (Suc p) (\<lambda>i. if i = 0 then v else l (i -1)) x \<in> T"
if "x \<in> standard_simplex (Suc p)" for x
- proof (simp add: that oriented_simplex_def sum_atMost_Suc_shift del: sum.atMost_Suc)
+ proof (simp add: that oriented_simplex_def sum.atMost_Suc_shift del: sum.atMost_Suc)
have x01: "\<And>i. 0 \<le> x i \<and> x i \<le> 1" and x0: "\<And>i. i > Suc p \<Longrightarrow> x i = 0" and x1: "sum x {..Suc p} = 1"
using that by (auto simp: oriented_simplex_def standard_simplex_def)
obtain a where "a \<in> S"
@@ -1224,7 +1224,7 @@
have "(\<lambda>i. (\<Sum>j\<le>p. l j i * (x (Suc j) * inverse (1 - x 0)))) \<in> S"
proof (rule S)
have "x 0 + (\<Sum>j\<le>p. x (Suc j)) = sum x {..Suc p}"
- by (metis sum_atMost_Suc_shift)
+ by (metis sum.atMost_Suc_shift)
with x1 have "(\<Sum>j\<le>p. x (Suc j)) = 1 - x 0"
by simp
with False show "(\<Sum>j\<le>p. x (Suc j) * inverse (1 - x 0)) = 1"
@@ -2936,7 +2936,7 @@
fix x
assume x: "x \<in> standard_simplex q"
have "(\<Sum>j\<le>Suc q. if j = 0 then 0 else x (j - Suc 0)) = (\<Sum>j\<le>q. x j)"
- by (simp add: sum_atMost_Suc_shift)
+ by (simp add: sum.atMost_Suc_shift)
with x have "simp q 0 (simplical_face 0 x) 0 = 1"
apply (simp add: oriented_simplex_def simp_def simplical_face_in_standard_simplex)
apply (simp add: simplical_face_def if_distrib ww_def standard_simplex_def cong: if_cong)
@@ -3230,7 +3230,7 @@
apply (simp add: chain_boundary_sum chain_boundary_cmul)
apply (subst chain_boundary_def)
apply (simp add: frag_cmul_sum sum.cartesian_product eq sum.union_disjoint disjoint_iff_not_equal
- sum.atLeast_Suc_atMost_Suc_shift del: sum_cl_ivl_Suc flip: comm_monoid_add_class.sum.Sigma)
+ sum.atLeast_Suc_atMost_Suc_shift del: sum.cl_ivl_Suc flip: comm_monoid_add_class.sum.Sigma)
apply (simp add: comm_monoid_add_class.sum.Sigma eq2 [of _ "\<lambda>i. {_ i.._ i}"])
apply (simp add: sum.union_disjoint disjoint_iff_not_equal * [OF 1 2])
done
--- a/src/HOL/Library/Stirling.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Library/Stirling.thy Wed Apr 10 21:29:32 2019 +0100
@@ -156,7 +156,7 @@
next
case (Suc n)
have "(\<Sum>k\<le>Suc n. stirling (Suc n) k) = stirling (Suc n) 0 + (\<Sum>k\<le>n. stirling (Suc n) (Suc k))"
- by (simp only: sum_atMost_Suc_shift)
+ by (simp only: sum.atMost_Suc_shift)
also have "\<dots> = (\<Sum>k\<le>n. stirling (Suc n) (Suc k))"
by simp
also have "\<dots> = (\<Sum>k\<le>n. n * stirling n (Suc k) + stirling n k)"
@@ -166,7 +166,7 @@
also have "\<dots> = n * fact n + fact n"
proof -
have "n * (\<Sum>k\<le>n. stirling n (Suc k)) = n * ((\<Sum>k\<le>Suc n. stirling n k) - stirling n 0)"
- by (metis add_diff_cancel_left' sum_atMost_Suc_shift)
+ by (metis add_diff_cancel_left' sum.atMost_Suc_shift)
also have "\<dots> = n * (\<Sum>k\<le>n. stirling n k)"
by (cases n) simp_all
also have "\<dots> = n * fact n"
@@ -192,9 +192,9 @@
(of_nat (n * stirling n 0) * x ^ 0 +
(\<Sum>i\<le>n. of_nat (n * stirling n (Suc i)) * (x ^ Suc i))) +
(\<Sum>i\<le>n. of_nat (stirling n i) * (x ^ Suc i))"
- by (subst sum_atMost_Suc_shift) (simp add: sum.distrib ring_distribs)
+ by (subst sum.atMost_Suc_shift) (simp add: sum.distrib ring_distribs)
also have "\<dots> = pochhammer x (Suc n)"
- by (subst sum_atMost_Suc_shift [symmetric])
+ by (subst sum.atMost_Suc_shift [symmetric])
(simp add: algebra_simps sum.distrib sum_distrib_left pochhammer_Suc flip: Suc)
finally show ?case .
qed
--- a/src/HOL/Library/Uprod.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Library/Uprod.thy Wed Apr 10 21:29:32 2019 +0100
@@ -210,7 +210,7 @@
by (subst card_SigmaI) simp_all
also have "\<dots> = sum of_nat {Suc 0..?A}"
using sum.atLeastLessThan_reindex [symmetric, of Suc 0 ?A id]
- by (simp del: sum_op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
+ by (simp del: sum.op_ivl_Suc add: atLeastLessThanSuc_atLeastAtMost)
also have "\<dots> = ?A * (?A + 1) div 2"
using gauss_sum_from_Suc_0 [of ?A, where ?'a = nat] by simp
finally show ?thesis .
--- a/src/HOL/Nonstandard_Analysis/HSeries.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HSeries.thy Wed Apr 10 21:29:32 2019 +0100
@@ -81,7 +81,7 @@
lemma sumhr_shift_bounds:
"\<And>m n. sumhr (m + hypnat_of_nat k, n + hypnat_of_nat k, f) =
sumhr (m, n, \<lambda>i. f (i + k))"
- unfolding sumhr_app by transfer (rule sum_shift_bounds_nat_ivl)
+ unfolding sumhr_app by transfer (rule sum.shift_bounds_nat_ivl)
subsection \<open>Nonstandard Sums\<close>
--- a/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Real_Asymp/Multiseries_Expansion.thy Wed Apr 10 21:29:32 2019 +0100
@@ -3707,7 +3707,7 @@
using h_nz by (intro bigthetaI_cong) (auto elim!: eventually_mono simp: f'_def field_simps)
also from spec[OF asymp_powser, of "Suc n"]
have "(\<lambda>x. f x - c - h x * (\<Sum>i<n. mssnth cs' i * h x ^ i)) \<in> O[F](\<lambda>x. h x * h x ^ n)"
- unfolding sum_lessThan_Suc_shift
+ unfolding sum.lessThan_Suc_shift
by (simp add: MSSCons algebra_simps sum_distrib_left sum_distrib_right)
finally show ?thesis
by (subst (asm) landau_o.big.mult_cancel_left) (insert h_nz, auto)
--- a/src/HOL/Series.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Series.thy Wed Apr 10 21:29:32 2019 +0100
@@ -80,7 +80,7 @@
by (rule sums_zero [THEN sums_summable])
lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. sum f {n * k ..< n * k + k}) sums s"
- apply (simp only: sums_def sum_nat_group tendsto_def eventually_sequentially)
+ apply (simp only: sums_def sum.nat_group tendsto_def eventually_sequentially)
apply (erule all_forward imp_forward exE| assumption)+
apply (rule_tac x="N" in exI)
by (metis le_square mult.commute mult.left_neutral mult_le_cancel2 mult_le_mono)
@@ -303,7 +303,7 @@
using assms by (auto intro!: tendsto_add simp: sums_def)
moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
unfolding lessThan_Suc_eq_insert_0
- by (simp add: ac_simps sum_atLeast1_atMost_eq image_Suc_lessThan)
+ by (simp add: ac_simps sum.atLeast1_atMost_eq image_Suc_lessThan)
ultimately show ?thesis
by (auto simp: sums_def simp del: sum.lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
qed
@@ -358,7 +358,7 @@
have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
- by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan sum_atLeast1_atMost_eq)
+ by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan sum.atLeast1_atMost_eq)
also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s"
proof
assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0"
@@ -940,7 +940,7 @@
with 1 have "(\<lambda>n. sum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)"
by (rule Lim_transform2)
then show ?thesis
- by (simp only: sums_def sum_triangle_reindex)
+ by (simp only: sums_def sum.triangle_reindex)
qed
lemma Cauchy_product:
@@ -1083,7 +1083,7 @@
with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e"
by (intro N) simp_all
also from True have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)"
- by (subst sum_diff [symmetric]) (simp_all add: sum_last_plus)
+ by (subst sum_diff [symmetric]) (simp_all add: sum.last_plus)
finally show ?thesis .
next
case False
--- a/src/HOL/Set_Interval.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Set_Interval.thy Wed Apr 10 21:29:32 2019 +0100
@@ -1861,82 +1861,158 @@
"F g {..<Suc n} = F g {..<n} \<^bold>* g n"
by (simp add: lessThan_Suc ac_simps)
-end
-
-(* FIXME why are the following simp rules but the corresponding eqns
-on intervals are not? *)
-
-lemma sum_cl_ivl_Suc [simp]:
- "sum f {m..Suc n} = (if Suc n < m then 0 else sum f {m..n} + f(Suc n))"
+lemma cl_ivl_Suc [simp]:
+ "F g {m..Suc n} = (if Suc n < m then \<^bold>1 else F g {m..n} \<^bold>* g(Suc n))"
by (auto simp: ac_simps atLeastAtMostSuc_conv)
-lemma sum_op_ivl_Suc [simp]:
- "sum f {m..<Suc n} = (if n < m then 0 else sum f {m..<n} + f(n))"
+lemma op_ivl_Suc [simp]:
+ "F g {m..<Suc n} = (if n < m then \<^bold>1 else F g {m..<n} \<^bold>* g(n))"
by (auto simp: ac_simps atLeastLessThanSuc)
-lemma sum_head:
+lemma head:
fixes n :: nat
assumes mn: "m \<le> n"
- shows "(\<Sum>x\<in>{m..n}. P x) = P m + (\<Sum>x\<in>{m<..n}. P x)" (is "?lhs = ?rhs")
+ shows "F g {m..n} = g m \<^bold>* F g {m<..n}" (is "?lhs = ?rhs")
proof -
from mn
have "{m..n} = {m} \<union> {m<..n}"
by (auto intro: ivl_disj_un_singleton)
- hence "?lhs = (\<Sum>x\<in>{m} \<union> {m<..n}. P x)"
+ hence "?lhs = F g ({m} \<union> {m<..n})"
by (simp add: atLeast0LessThan)
also have "\<dots> = ?rhs" by simp
finally show ?thesis .
qed
-lemma sum_ub_add_nat: assumes "(m::nat) \<le> n + 1"
- shows "sum f {m..n + p} = sum f {m..n} + sum f {n + 1..n + p}"
+lemma ub_add_nat:
+ assumes "(m::nat) \<le> n + 1"
+ shows "F g {m..n + p} = F g {m..n} \<^bold>* F g {n + 1..n + p}"
proof-
have "{m .. n+p} = {m..n} \<union> {n+1..n+p}" using \<open>m \<le> n+1\<close> by auto
- thus ?thesis by (auto simp: ivl_disj_int sum.union_disjoint
- atLeastSucAtMost_greaterThanAtMost)
+ thus ?thesis by (auto simp: ivl_disj_int union_disjoint atLeastSucAtMost_greaterThanAtMost)
qed
+lemma nat_group:
+ fixes k::nat shows "F (\<lambda>m. F g {m * k ..< m*k + k}) {..<n} = F g {..< n * k}"
+proof (cases k)
+ case (Suc l)
+ then have "k > 0"
+ by auto
+ then show ?thesis
+ by (induct n) (simp_all add: atLeastLessThan_concat add.commute atLeast0LessThan[symmetric])
+qed auto
+
+lemma triangle_reindex:
+ fixes n :: nat
+ shows "F (\<lambda>(i,j). g i j) {(i,j). i+j < n} = F (\<lambda>k. F (\<lambda>i. g i (k - i)) {..k}) {..<n}"
+ apply (simp add: Sigma)
+ apply (rule reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
+ apply auto
+ done
+
+lemma triangle_reindex_eq:
+ fixes n :: nat
+ shows "F (\<lambda>(i,j). g i j) {(i,j). i+j \<le> n} = F (\<lambda>k. F (\<lambda>i. g i (k - i)) {..k}) {..n}"
+using triangle_reindex [of g "Suc n"]
+by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
+
+lemma nat_diff_reindex: "F (\<lambda>i. g (n - Suc i)) {..<n} = F g {..<n}"
+ by (rule reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
+
+lemma shift_bounds_nat_ivl:
+ "F g {m+k..<n+k} = F (\<lambda>i. g(i + k)){m..<n::nat}"
+by (induct "n", auto simp: atLeastLessThanSuc)
+
+lemma shift_bounds_cl_nat_ivl:
+ "F g {m+k..n+k} = F (\<lambda>i. g(i + k)){m..n::nat}"
+ by (rule reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
+
+corollary shift_bounds_cl_Suc_ivl:
+ "F g {Suc m..Suc n} = F (\<lambda>i. g(Suc i)){m..n}"
+by (simp add: shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
+
+corollary shift_bounds_Suc_ivl:
+ "F g {Suc m..<Suc n} = F (\<lambda>i. g(Suc i)){m..<n}"
+by (simp add: shift_bounds_nat_ivl[where k="Suc 0", simplified])
+
+lemma atMost_Suc_shift:
+ shows "F g {..Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n}"
+proof (induct n)
+ case 0 show ?case by simp
+next
+ case (Suc n) note IH = this
+ have "F g {..Suc (Suc n)} = F g {..Suc n} \<^bold>* g (Suc (Suc n))"
+ by (rule atMost_Suc)
+ also have "F g {..Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n}"
+ by (rule IH)
+ also have "g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) =
+ g 0 \<^bold>* (F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)))"
+ by (rule assoc)
+ also have "F (\<lambda>i. g (Suc i)) {..n} \<^bold>* g (Suc (Suc n)) = F (\<lambda>i. g (Suc i)) {..Suc n}"
+ by (rule atMost_Suc [symmetric])
+ finally show ?case .
+qed
+
+lemma lessThan_Suc_shift:
+ "F g {..<Suc n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..<n}"
+ by (induction n) (simp_all add: ac_simps)
+
+lemma atMost_shift:
+ "F g {..n} = g 0 \<^bold>* F (\<lambda>i. g (Suc i)) {..<n}"
+ by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost
+ atLeastSucAtMost_greaterThanAtMost le0 head shift_bounds_Suc_ivl)
+
+lemma last_plus:
+ fixes n::nat shows "m \<le> n \<Longrightarrow> F g {m..n} = g n \<^bold>* F g {m..<n}"
+ by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost commute)
+
+lemma nested_swap:
+ "F (\<lambda>i. F (\<lambda>j. a i j) {0..<i}) {0..n} = F (\<lambda>j. F (\<lambda>i. a i j) {Suc j..n}) {0..<n}"
+ by (induction n) (auto simp: distrib)
+
+lemma nested_swap':
+ "F (\<lambda>i. F (\<lambda>j. a i j) {..<i}) {..n} = F (\<lambda>j. F (\<lambda>i. a i j) {Suc j..n}) {..<n}"
+ by (induction n) (auto simp: distrib)
+
+lemma atLeast1_atMost_eq:
+ "F g {Suc 0..n} = F (\<lambda>k. g (Suc k)) {..<n}"
+proof -
+ have "F g {Suc 0..n} = F g (Suc ` {..<n})"
+ by (simp add: image_Suc_lessThan)
+ also have "\<dots> = F (\<lambda>k. g (Suc k)) {..<n}"
+ by (simp add: reindex)
+ finally show ?thesis .
+qed
+
+lemma atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> F g {a..<Suc b} = F g {a..<b} \<^bold>* g b"
+ by (simp add: atLeastLessThanSuc commute)
+
+lemma nat_ivl_Suc':
+ assumes "m \<le> Suc n"
+ shows "F g {m..Suc n} = g (Suc n) \<^bold>* F g {m..n}"
+proof -
+ from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
+ also have "F g \<dots> = g (Suc n) \<^bold>* F g {m..n}" by simp
+ finally show ?thesis .
+qed
+
+end
+
+lemma sum_natinterval_diff:
+ fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
+ shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
+ (if m \<le> n then f m - f(n + 1) else 0)"
+by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
+
lemma sum_diff_nat_ivl:
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow> sum f {m..<p} - sum f {m..<n} = sum f {n..<p}"
using sum.atLeastLessThan_concat [of m n p f,symmetric]
by (simp add: ac_simps)
-lemma sum_natinterval_difff:
- fixes f:: "nat \<Rightarrow> ('a::ab_group_add)"
- shows "sum (\<lambda>k. f k - f(k + 1)) {(m::nat) .. n} =
- (if m \<le> n then f m - f(n + 1) else 0)"
-by (induct n, auto simp add: algebra_simps not_le le_Suc_eq)
-
-lemma sum_nat_group: "(\<Sum>m<n::nat. sum f {m * k ..< m*k + k}) = sum f {..< n * k}"
-proof (cases k)
- case (Suc l)
- then have "k > 0"
- by auto
- then show ?thesis
- by (induct n) (simp_all add: sum.atLeastLessThan_concat add.commute atLeast0LessThan[symmetric])
-qed auto
-
-lemma sum_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))"
- apply (simp add: sum.Sigma)
- apply (rule sum.reindex_bij_witness[where j="\<lambda>(i, j). (i+j, i)" and i="\<lambda>(k, i). (i, k - i)"])
- apply auto
- done
-
-lemma sum_triangle_reindex_eq:
- fixes n :: nat
- shows "(\<Sum>(i,j)\<in>{(i,j). i+j \<le> n}. f i j) = (\<Sum>k\<le>n. \<Sum>i\<le>k. f i (k - i))"
-using sum_triangle_reindex [of f "Suc n"]
-by (simp only: Nat.less_Suc_eq_le lessThan_Suc_atMost)
-
-lemma nat_diff_sum_reindex: "(\<Sum>i<n. f (n - Suc i)) = (\<Sum>i<n. f i)"
- by (rule sum.reindex_bij_witness[where i="\<lambda>i. n - Suc i" and j="\<lambda>i. n - Suc i"]) auto
-
lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
by (subst sum_subtractf_nat) auto
+
context semiring_parity
begin
@@ -1964,22 +2040,6 @@
subsubsection \<open>Shifting bounds\<close>
-lemma sum_shift_bounds_nat_ivl:
- "sum f {m+k..<n+k} = sum (\<lambda>i. f(i + k)){m..<n::nat}"
-by (induct "n", auto simp:atLeastLessThanSuc)
-
-lemma sum_shift_bounds_cl_nat_ivl:
- "sum f {m+k..n+k} = sum (\<lambda>i. f(i + k)){m..n::nat}"
- by (rule sum.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
-
-corollary sum_shift_bounds_cl_Suc_ivl:
- "sum f {Suc m..Suc n} = sum (\<lambda>i. f(Suc i)){m..n}"
-by (simp add:sum_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
-
-corollary sum_shift_bounds_Suc_ivl:
- "sum f {Suc m..<Suc n} = sum (\<lambda>i. f(Suc i)){m..<n}"
-by (simp add:sum_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-
context comm_monoid_add
begin
@@ -2019,37 +2079,6 @@
end
-lemma sum_atMost_Suc_shift:
- fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
- shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n) note IH = this
- have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))"
- by (rule sum.atMost_Suc)
- also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))"
- by (rule IH)
- also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) =
- f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))"
- by (rule add.assoc)
- also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))"
- by (rule sum.atMost_Suc [symmetric])
- finally show ?case .
-qed
-
-lemma sum_lessThan_Suc_shift:
- "(\<Sum>i<Suc n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
- by (induction n) (simp_all add: add_ac)
-
-lemma sum_atMost_shift:
- fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add"
- shows "(\<Sum>i\<le>n. f i) = f 0 + (\<Sum>i<n. f (Suc i))"
-by (metis atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost atLeastSucAtMost_greaterThanAtMost le0 sum_head sum_shift_bounds_Suc_ivl)
-
-lemma sum_last_plus: fixes n::nat shows "m \<le> n \<Longrightarrow> (\<Sum>i = m..n. f i) = f n + (\<Sum>i = m..<n. f i)"
- by (cases n) (auto simp: atLeastLessThanSuc_atLeastAtMost add.commute)
-
lemma sum_Suc_diff:
fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
assumes "m \<le> Suc n"
@@ -2062,24 +2091,6 @@
shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
using assms by (induct n) (auto simp: le_Suc_eq)
-lemma nested_sum_swap:
- "(\<Sum>i = 0..n. (\<Sum>j = 0..<i. a i j)) = (\<Sum>j = 0..<n. \<Sum>i = Suc j..n. a i j)"
- by (induction n) (auto simp: sum.distrib)
-
-lemma nested_sum_swap':
- "(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
- by (induction n) (auto simp: sum.distrib)
-
-lemma sum_atLeast1_atMost_eq:
- "sum f {Suc 0..n} = (\<Sum>k<n. f (Suc k))"
-proof -
- have "sum f {Suc 0..n} = sum f (Suc ` {..<n})"
- by (simp add: image_Suc_lessThan)
- also have "\<dots> = (\<Sum>k<n. f (Suc k))"
- by (simp add: sum.reindex)
- finally show ?thesis .
-qed
-
subsubsection \<open>Telescoping\<close>
@@ -2158,7 +2169,7 @@
lemma one_diff_power_eq:
fixes x :: "'a::{comm_ring,monoid_mult}"
shows "n \<noteq> 0 \<Longrightarrow> 1 - x^n = (1 - x) * (\<Sum>i<n. x^i)"
-by (metis one_diff_power_eq' [of n x] nat_diff_sum_reindex)
+by (metis one_diff_power_eq' [of n x] sum.nat_diff_reindex)
lemma sum_gp_basic:
fixes x :: "'a::{comm_ring,monoid_mult}"
@@ -2206,7 +2217,7 @@
lemma sum_gp0:
fixes x :: "'a::{comm_ring,division_ring}"
- shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
+ shows "(\<Sum>i\<le>n. x^i) = (if x = 1 then of_nat(n + 1) else (1 - x^Suc n) / (1 - x))"
using sum_gp_basic[of x n]
by (simp add: mult.commute divide_simps)
@@ -2387,16 +2398,6 @@
"\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..n}"
"\<Prod>i<n. t" \<rightleftharpoons> "CONST prod (\<lambda>i. t) {..<n}"
-lemma prod_atLeast1_atMost_eq:
- "prod f {Suc 0..n} = (\<Prod>k<n. f (Suc k))"
-proof -
- have "prod f {Suc 0..n} = prod f (Suc ` {..<n})"
- by (simp add: image_Suc_lessThan)
- also have "\<dots> = (\<Prod>k<n. f (Suc k))"
- by (simp add: prod.reindex)
- finally show ?thesis .
-qed
-
lemma prod_int_plus_eq: "prod int {i..i+j} = \<Prod>{int i..int (i+j)}"
by (induct j) (auto simp add: atLeastAtMostSuc_conv atLeastAtMostPlus1_int_conv)
@@ -2411,55 +2412,6 @@
by auto
qed
-
-subsubsection \<open>Shifting bounds\<close>
-
-lemma prod_shift_bounds_nat_ivl:
- "prod f {m+k..<n+k} = prod (\<lambda>i. f(i + k)){m..<n::nat}"
-by (induct "n", auto simp:atLeastLessThanSuc)
-
-lemma prod_shift_bounds_cl_nat_ivl:
- "prod f {m+k..n+k} = prod (\<lambda>i. f(i + k)){m..n::nat}"
- by (rule prod.reindex_bij_witness[where i="\<lambda>i. i + k" and j="\<lambda>i. i - k"]) auto
-
-corollary prod_shift_bounds_cl_Suc_ivl:
- "prod f {Suc m..Suc n} = prod (\<lambda>i. f(Suc i)){m..n}"
-by (simp add:prod_shift_bounds_cl_nat_ivl[where k="Suc 0", simplified])
-
-corollary prod_shift_bounds_Suc_ivl:
- "prod f {Suc m..<Suc n} = prod (\<lambda>i. f(Suc i)){m..<n}"
-by (simp add:prod_shift_bounds_nat_ivl[where k="Suc 0", simplified])
-
-lemma prod_lessThan_Suc [simp]: "prod f {..<Suc n} = prod f {..<n} * f n"
- by (simp add: lessThan_Suc mult.commute)
-
-lemma prod_lessThan_Suc_shift:"(\<Prod>i<Suc n. f i) = f 0 * (\<Prod>i<n. f (Suc i))"
- by (induction n) (simp_all add: lessThan_Suc mult_ac)
-
-lemma prod_atLeastLessThan_Suc: "a \<le> b \<Longrightarrow> prod f {a..<Suc b} = prod f {a..<b} * f b"
- by (simp add: atLeastLessThanSuc mult.commute)
-
-lemma prod_nat_ivl_Suc':
- assumes "m \<le> Suc n"
- shows "prod f {m..Suc n} = f (Suc n) * prod f {m..n}"
-proof -
- from assms have "{m..Suc n} = insert (Suc n) {m..n}" by auto
- also have "prod f \<dots> = f (Suc n) * prod f {m..n}" by simp
- finally show ?thesis .
-qed
-
-lemma prod_nat_group: "(\<Prod>m<n::nat. prod f {m * k ..< m*k + k}) = prod f {..< n * k}"
-proof (cases "k = 0")
- case True
- then show ?thesis
- by auto
-next
- case False
- then show ?thesis
- by (induct "n"; simp add: prod.atLeastLessThan_concat algebra_simps atLeast0_lessThan_Suc atLeast0LessThan[symmetric])
-qed
-
-
subsection \<open>Efficient folding over intervals\<close>
function fold_atLeastAtMost_nat where
--- a/src/HOL/Transcendental.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/Transcendental.thy Wed Apr 10 21:29:32 2019 +0100
@@ -400,7 +400,7 @@
have "?s sums y" using sums_if'[OF \<open>f sums y\<close>] .
from this[unfolded sums_def, THEN LIMSEQ_Suc]
have "(\<lambda>n. if even n then f (n div 2) else 0) sums y"
- by (simp add: lessThan_Suc_eq_insert_0 sum_atLeast1_atMost_eq image_Suc_lessThan
+ by (simp add: lessThan_Suc_eq_insert_0 sum.atLeast1_atMost_eq image_Suc_lessThan
if_eq sums_def cong del: if_weak_cong)
from sums_add[OF g_sums this] show ?thesis
by (simp only: if_sum)
@@ -620,7 +620,7 @@
lemma lemma_realpow_rev_sumr:
"(\<Sum>p<Suc n. (x ^ p) * (y ^ (n - p))) = (\<Sum>p<Suc n. (x ^ (n - p)) * (y ^ p))"
- by (subst nat_diff_sum_reindex[symmetric]) simp
+ by (subst sum.nat_diff_reindex[symmetric]) simp
lemma lemma_termdiff2:
fixes h :: "'a::field"
@@ -1450,7 +1450,7 @@
by (simp add: times_S Suc_diff_le)
also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n - i))) =
(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n - i)))"
- by (subst sum_atMost_Suc_shift) simp
+ by (subst sum.atMost_Suc_shift) simp
also have "(\<Sum>i\<le>n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i))) =
(\<Sum>i\<le>Suc n. real (Suc n - i) *\<^sub>R (S x i * S y (Suc n - i)))"
by simp
@@ -1462,7 +1462,7 @@
also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
by (simp only: scaleR_right.sum)
finally show "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
- by (simp del: sum_cl_ivl_Suc)
+ by (simp del: sum.cl_ivl_Suc)
qed
lemma exp_add_commuting: "x * y = y * x \<Longrightarrow> exp (x + y) = exp x * exp y"
@@ -6025,7 +6025,7 @@
by auto
lemma sum_up_index_split: "(\<Sum>k\<le>m + n. f k) = (\<Sum>k\<le>m. f k) + (\<Sum>k = Suc m..m + n. f k)"
- by (metis atLeast0AtMost Suc_eq_plus1 le0 sum_ub_add_nat)
+ by (metis atLeast0AtMost Suc_eq_plus1 le0 sum.ub_add_nat)
lemma Sigma_interval_disjoint: "(SIGMA i:A. {..v i}) \<inter> (SIGMA i:A.{v i<..w}) = {}"
for w :: "'a::order"
@@ -6054,7 +6054,7 @@
also have "\<dots> = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
by (auto simp: pairs_le_eq_Sigma sum.Sigma)
also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
- apply (subst sum_triangle_reindex_eq)
+ apply (subst sum.triangle_reindex_eq)
apply (auto simp: algebra_simps sum_distrib_left intro!: sum.cong)
apply (metis le_add_diff_inverse power_add)
done
@@ -6165,7 +6165,7 @@
have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" for w
proof -
have "(\<Sum>i\<le>Suc n. c i * w^i) = (\<Sum>i\<le>n. c (Suc i) * w ^ Suc i)"
- unfolding Set_Interval.sum_atMost_Suc_shift
+ unfolding Set_Interval.sum.atMost_Suc_shift
by simp
also have "\<dots> = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
by (simp add: sum_distrib_left ac_simps)
--- a/src/HOL/ex/HarmonicSeries.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy Wed Apr 10 21:29:32 2019 +0100
@@ -147,7 +147,7 @@
"\<dots> = (\<Sum>n\<in>{(1::nat)..2}. 1/real n)" by simp
also have
"\<dots> = ((\<Sum>n\<in>{Suc 1..2}. 1/real n) + 1/(real (1::nat)))"
- by (subst sum_head)
+ by (subst sum.head)
(auto simp: atLeastSucAtMost_greaterThanAtMost)
also have
"\<dots> = ((\<Sum>n\<in>{2..2::nat}. 1/real n) + 1/(real (1::nat)))"
@@ -283,7 +283,7 @@
have "\<forall>m\<ge>j. 0 < ?f m" by simp
with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule sum_less_suminf)
then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
- unfolding sum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
+ unfolding sum.shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
with j_def have
"(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
then have
--- a/src/HOL/ex/ThreeDivides.thy Wed Apr 10 13:34:55 2019 +0100
+++ b/src/HOL/ex/ThreeDivides.thy Wed Apr 10 21:29:32 2019 +0100
@@ -199,7 +199,7 @@
by (simp add: div_mult2_eq[symmetric])
also have
"\<dots> = (\<Sum>x\<in>{Suc 0..<Suc nd}. m div 10^x mod 10 * 10^x) + c"
- by (simp only: sum_shift_bounds_Suc_ivl)
+ by (simp only: sum.shift_bounds_Suc_ivl)
(simp add: atLeast0LessThan)
also have
"\<dots> = (\<Sum>x<Suc nd. m div 10^x mod 10 * 10^x)"