# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1554928172 -3600
# Node ID c8deb8ba6d05321bb7c4e30a233713f42a310189
# Parent  4005298550a69e1af773eb4da784ede61b3e7037
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context

diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- 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)
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Conformal_Mappings.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/FPS_Convergence.thy
--- 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))"
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Gamma_Function.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Harmonic_Numbers.thy
--- 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)
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Infinite_Products.thy
--- 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"
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Poly_Roots.thy
--- 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
 
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/Summation_Tests.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Analysis/ex/Approximations.thy
--- 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)) =
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Binomial.thy
--- 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))"
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Computational_Algebra/Polynomial.thy
--- 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"
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Decision_Procs/Approximation.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Factorial.thy
--- 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)
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Homology/Homology.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Homology/Invariance_of_Domain.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Homology/Simplices.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Library/Stirling.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Library/Uprod.thy
--- 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 .
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Nonstandard_Analysis/HSeries.thy
--- 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>
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Real_Asymp/Multiseries_Expansion.thy
--- 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)
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Series.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Set_Interval.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/Transcendental.thy
--- 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)
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/ex/HarmonicSeries.thy
--- 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
diff -r 4005298550a6 -r c8deb8ba6d05 src/HOL/ex/ThreeDivides.thy
--- 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)"