# HG changeset patch
# User paulson
# Date 1606069614 0
# Node ID 8e5428ff35af9d99a82e83e6c190b10818c0de31
# Parent  a7877e14e7f8d2c7d65bc766b2081464ca790a4c# Parent  703b601d71b5bc881ae7630e927e357ce3a01c01
merged

diff -r a7877e14e7f8 -r 8e5428ff35af src/HOL/Computational_Algebra/Formal_Power_Series.thy
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Nov 22 13:31:33 2020 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Nov 22 18:26:54 2020 +0000
@@ -120,7 +120,10 @@
 lemma fps_mult_nth_0 [simp]: "(f * g) $ 0 = f $ 0 * g $ 0"
   unfolding fps_times_def by simp
 
-lemma fps_mult_nth_1 [simp]: "(f * g) $ 1 = f$0 * g$1 + f$1 * g$0"
+lemma fps_mult_nth_1: "(f * g) $ 1 = f$0 * g$1 + f$1 * g$0"
+  by (simp add: fps_mult_nth)
+
+lemma fps_mult_nth_1' [simp]: "(f * g) $ Suc 0 = f$0 * g$Suc 0 + f$Suc 0 * g$0"
   by (simp add: fps_mult_nth)
 
 lemmas mult_nth_0 = fps_mult_nth_0
@@ -1976,35 +1979,6 @@
     fps_const (inverse (of_nat n))"
   by (simp add: fps_of_nat fps_const_inverse[symmetric])
 
-lemma sum_zero_lemma:
-  fixes n::nat
-  assumes "0 < n"
-  shows "(\<Sum>i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)"
-proof -
-  let ?f = "\<lambda>i. if n = i then 1 else if n - i = 1 then - 1 else 0"
-  let ?g = "\<lambda>i. if i = n then 1 else if i = n - 1 then - 1 else 0"
-  let ?h = "\<lambda>i. if i=n - 1 then - 1 else 0"
-  have th1: "sum ?f {0..n} = sum ?g {0..n}"
-    by (rule sum.cong) auto
-  have th2: "sum ?g {0..n - 1} = sum ?h {0..n - 1}"
-    apply (rule sum.cong)
-    using assms
-    apply auto
-    done
-  have eq: "{0 .. n} = {0.. n - 1} \<union> {n}"
-    by auto
-  from assms have d: "{0.. n - 1} \<inter> {n} = {}"
-    by auto
-  have f: "finite {0.. n - 1}" "finite {n}"
-    by auto
-  show ?thesis
-    unfolding th1
-    apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def)
-    unfolding th2
-    apply simp
-    done
-qed
-
 lemma fps_lr_inverse_mult_ring1:
   fixes   f g :: "'a::ring_1 fps"
   assumes x: "x * f$0 = 1" "f$0 * x = 1"
@@ -2943,10 +2917,16 @@
   show "euclidean_size f \<le> euclidean_size (f * g)"
     by (cases "f = 0") (simp_all add: fps_euclidean_size_def)
   show "euclidean_size (f mod g) < euclidean_size g"
-    apply (cases "f = 0", simp add: fps_euclidean_size_def)
-    apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
-    apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
-    done
+  proof (cases "f = 0")
+    case True
+    then show ?thesis
+      by (simp add: fps_euclidean_size_def)
+  next
+    case False
+    then show ?thesis 
+      using le_less_linear[of "subdegree g" "subdegree f"]
+      by (force simp add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
+  qed
 next
   fix f g h :: "'a fps" assume [simp]: "h \<noteq> 0"
   show "(h * f) div (h * g) = f div g"
@@ -3428,12 +3408,10 @@
   assumes a0: "a $0 = 0"
     and kn: "n \<ge> k"
   shows "sum (\<lambda>i. (a ^ i)$k) {0 .. n} = sum (\<lambda>i. (a ^ i)$k) {0 .. k}"
-  apply (rule sum.mono_neutral_right)
-  using kn
-  apply auto
-  apply (rule startsby_zero_power_prefix[rule_format, OF a0])
-  apply arith
-  done
+proof (intro strip sum.mono_neutral_right)
+  show "\<And>i. i \<in> {0..n} - {0..k} \<Longrightarrow> a ^ i $ k = 0"
+    by (simp add: a0 startsby_zero_power_prefix)
+qed (use kn in auto)
 
 lemma startsby_zero_power_nth_same:
   assumes a0: "a$0 = 0"
@@ -3750,10 +3728,7 @@
         using Suc.hyps[symmetric] unfolding fps_sub_nth by simp
       also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)"
         unfolding fps_X_power_mult_right_nth
-        apply (auto simp add: not_less fps_const_def)
-        apply (rule cong[of a a, OF refl])
-        apply arith
-        done
+        by (simp add: not_less le_less_Suc_eq)
       finally show ?case
         by simp
     qed
@@ -3840,10 +3815,15 @@
 definition "natpermute n k = {l :: nat list. length l = k \<and> sum_list l = n}"
 
 lemma natlist_trivial_1: "natpermute n 1 = {[n]}"
-  apply (auto simp add: natpermute_def)
-  apply (case_tac x)
-  apply auto
-  done
+proof -
+  have "\<lbrakk>length xs = 1; n = sum_list xs\<rbrakk> \<Longrightarrow> xs = [sum_list xs]" for xs
+    by (cases xs) auto
+  then show ?thesis
+    by (auto simp add: natpermute_def)
+qed
+
+lemma natlist_trivial_Suc0 [simp]: "natpermute n (Suc 0) = {[n]}"
+  using natlist_trivial_1 by force
 
 lemma append_natpermute_less_eq:
   assumes "xs @ ys \<in> natpermute n k"
@@ -3877,12 +3857,7 @@
     from ys have ys': "sum_list ys = n - m"
       by (simp add: natpermute_def)
     show "l \<in> ?L" using leq xs ys h
-      apply (clarsimp simp add: natpermute_def)
-      unfolding xs' ys'
-      using assms xs ys
-      unfolding natpermute_def
-      apply simp
-      done
+      using assms by (force simp add: natpermute_def)
   qed
   show "?L \<subseteq> ?R"
   proof
@@ -3901,15 +3876,10 @@
       using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
     from ls have m: "?m \<in> {0..n}"
       by (simp add: l_take_drop del: append_take_drop_id)
-    from xs ys ls show "l \<in> ?R"
-      apply auto
-      apply (rule bexI [where x = "?m"])
-      apply (rule exI [where x = "?xs"])
-      apply (rule exI [where x = "?ys"])
-      using ls l
-      apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
-      apply simp
-      done
+    have "sum_list (take h l) \<le> sum_list l"
+      using l_take_drop ls m by presburger
+    with xs ys ls l show "l \<in> ?R"
+      by simp (metis append_take_drop_id m)
   qed
 qed
 
@@ -3917,27 +3887,17 @@
   by (auto simp add: natpermute_def)
 
 lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})"
-  apply (auto simp add: set_replicate_conv_if natpermute_def)
-  apply (rule nth_equalityI)
-  apply simp_all
-  done
+  by (auto simp add: set_replicate_conv_if natpermute_def replicate_length_same)
 
 lemma natpermute_finite: "finite (natpermute n k)"
 proof (induct k arbitrary: n)
   case 0
   then show ?case
-    apply (subst natpermute_split[of 0 0, simplified])
-    apply (simp add: natpermute_0)
-    done
+    by (simp add: natpermute_0)
 next
   case (Suc k)
-  then show ?case unfolding natpermute_split [of k "Suc k", simplified]
-    apply -
-    apply (rule finite_UN_I)
-    apply simp
-    unfolding One_nat_def[symmetric] natlist_trivial_1
-    apply simp
-    done
+  then show ?case
+    using natpermute_split [of k "Suc k"] finite_UN_I by simp
 qed
 
 lemma natpermute_contain_maximal:
@@ -3959,9 +3919,7 @@
     have d: "({0..k} - {i}) \<inter> {i} = {}"
       using i by auto
     from H have "n = sum (nth xs) {0..k}"
-      apply (simp add: natpermute_def)
-      apply (auto simp add: atLeastLessThanSuc_atLeastAtMost sum_list_sum_nth)
-      done
+      by (auto simp add: natpermute_def atLeastLessThanSuc_atLeastAtMost sum_list_sum_nth)
     also have "\<dots> = n + sum (nth xs) ({0..k} - {i})"
       unfolding sum.union_disjoint[OF f d, unfolded eqs] using i by simp
     finally have zxs: "\<forall> j\<in> {0..k} - {i}. xs!j = 0"
@@ -3994,10 +3952,8 @@
     then obtain i where i: "i \<in> {0..k}" and xs: "xs = (replicate (k + 1) 0) [i:=n]"
       by auto
     have nxs: "n \<in> set xs"
-      unfolding xs
-      apply (rule set_update_memI)
-      using i apply simp
-      done
+      unfolding xs using set_update_memI i 
+      by (metis Suc_eq_plus1 atLeast0AtMost atMost_iff le_simps(2) length_replicate)
     have xsl: "length xs = k + 1"
       by (simp only: xs length_replicate length_list_update)
     have "sum_list xs = sum (nth xs) {0..<k+1}"
@@ -4025,10 +3981,7 @@
   proof (cases m)
     case 0
     then show ?thesis
-      apply simp
-      unfolding natlist_trivial_1[where n = n, unfolded One_nat_def]
-      apply simp
-      done
+      by simp
   next
     case (Suc k)
     then have km: "k < m" by arith
@@ -4038,31 +3991,18 @@
     have d0: "{0 .. k} \<inter> {m} = {}" using Suc by auto
     have "(prod a {0 .. m}) $ n = (prod a {0 .. k} * a m) $ n"
       unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp
-    also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1). \<Prod>j\<in>{0..k}. a j $ v ! j) * a m $ (n - i))"
-      unfolding fps_mult_nth H[rule_format, OF km] ..
+    also have "\<dots> = (\<Sum>i = 0..n. (\<Sum>v\<in>natpermute i (k + 1).
+            (\<Prod>j = 0..k. a j $ v ! j) * a m $ (n - i)))"
+      unfolding fps_mult_nth H[rule_format, OF km] sum_distrib_right ..
+    also have "... = (\<Sum>i = 0..n.
+                       \<Sum>v\<in>(\<lambda>l1. l1 @ [n - i]) ` natpermute i (Suc k).
+                        (\<Prod>j = 0..k. a j $ v ! j) * a (Suc k) $ v ! Suc k)"
+      by (intro sum.cong [OF refl sym] sum.reindex_cong) (auto simp: inj_on_def natpermute_def nth_append Suc)
+    also have "... = (\<Sum>v\<in>(\<Union>x\<in>{0..n}. {l1 @ [n - x] |l1. l1 \<in> natpermute x (Suc k)}).
+                      (\<Prod>j = 0..k. a j $ v ! j) * a (Suc k) $ v ! Suc k)"
+      by (subst sum.UNION_disjoint) (auto simp add: natpermute_finite setcompr_eq_image)
     also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j $ v ! j)"
-      apply (simp add: Suc)
-      unfolding natpermute_split[of m "m + 1", simplified, of n,
-        unfolded natlist_trivial_1[unfolded One_nat_def] Suc]
-      apply (subst sum.UNION_disjoint)
-      apply simp
-      apply simp
-      unfolding image_Collect[symmetric]
-      apply clarsimp
-      apply (rule finite_imageI)
-      apply (rule natpermute_finite)
-      apply (clarsimp simp add: set_eq_iff)
-      apply auto
-      apply (rule sum.cong)
-      apply (rule refl)
-      unfolding sum_distrib_right
-      apply (rule sym)
-      apply (rule_tac l = "\<lambda>xs. xs @ [n - x]" in sum.reindex_cong)
-      apply (simp add: inj_on_def)
-      apply auto
-      unfolding prod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc]
-      apply (clarsimp simp add: natpermute_def nth_append)
-      done
+      using natpermute_split[of m "m + 1"] by (simp add: Suc)
     finally show ?thesis .
   qed
 qed
@@ -4264,10 +4204,7 @@
         have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using Suc by auto
         have d: "{0 .. n1} \<inter> {n} = {}" using Suc by auto
         have seq: "(\<Sum>i = 0..n1. b $ i * a ^ i $ n) = (\<Sum>i = 0..n1. c $ i * a ^ i $ n)"
-          apply (rule sum.cong)
-          using H Suc
-          apply auto
-          done
+          using H Suc by auto
         have th0: "(b oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n"
           unfolding fps_compose_nth sum.union_disjoint[OF f d, unfolded eq] seq
           using startsby_zero_power_nth_same[OF a0]
@@ -4332,9 +4269,7 @@
       finally show ?thesis using c' by simp
     qed
     then show "((r, Suc k, a, xs!i), r, Suc k, a, Suc n) \<in> ?R"
-      apply auto
-      apply (metis not_less)
-      done
+      using not_less by auto
   next
     fix r :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
     and a :: "'a fps"
@@ -4345,11 +4280,11 @@
 
 definition "fps_radical r n a = Abs_fps (radical r n a)"
 
+lemma radical_0 [simp]: "\<And>n. 0 < n \<Longrightarrow> radical r 0 a n = 0"
+  using radical.elims by blast
+
 lemma fps_radical0[simp]: "fps_radical r 0 a = 1"
-  apply (auto simp add: fps_eq_iff fps_radical_def)
-  apply (case_tac n)
-  apply auto
-  done
+  by (auto simp add: fps_eq_iff fps_radical_def)
 
 lemma fps_radical_nth_0[simp]: "fps_radical r n a $ 0 = (if n = 0 then 1 else r n (a$0))"
   by (cases n) (simp_all add: fps_radical_def)
@@ -4365,14 +4300,17 @@
   have eq1: "fps_radical r k a ^ k $ 0 = (\<Prod>j\<in>{0..h}. fps_radical r k a $ (replicate k 0) ! j)"
     unfolding fps_power_nth Suc by simp
   also have "\<dots> = (\<Prod>j\<in>{0..h}. r k (a$0))"
-    apply (rule prod.cong)
-    apply simp
-    using Suc
-    apply (subgoal_tac "replicate k 0 ! x = 0")
-    apply (auto intro: nth_replicate simp del: replicate.simps)
-    done
+  proof (rule prod.cong [OF refl])
+    show "fps_radical r k a $ replicate k 0 ! j = r k (a $ 0)" if "j \<in> {0..h}" for j
+    proof -
+      have "j < Suc h"
+        using that by presburger
+      then show ?thesis
+        by (metis Suc fps_radical_nth_0 nth_replicate old.nat.distinct(2))
+    qed
+  qed
   also have "\<dots> = a$0"
-    using r Suc by (simp add: prod_constant)
+    using r Suc by simp
   finally show ?thesis
     using Suc by simp
 qed
@@ -4416,11 +4354,8 @@
           from v obtain i where i: "i \<in> {0..k}" "v = (replicate (k+1) 0) [i:= n]"
             unfolding natpermute_contain_maximal by auto
           have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) =
-              (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
-            apply (rule prod.cong, simp)
-            using i r0
-            apply (simp del: replicate.simps)
-            done
+                (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
+              using i r0 by (auto simp del: replicate.simps intro: prod.cong)
           also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
             using i r0 by (simp add: prod_gen_delta)
           finally show ?ths .
@@ -4448,65 +4383,6 @@
   qed
 qed
 
-(*
-lemma power_radical:
-  fixes a:: "'a::field_char_0 fps"
-  assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" and a0: "a$0 \<noteq> 0"
-  shows "(fps_radical r (Suc k) a) ^ (Suc k) = a"
-proof-
-  let ?r = "fps_radical r (Suc k) a"
-  from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto
-  {fix z have "?r ^ Suc k $ z = a$z"
-    proof(induct z rule: nat_less_induct)
-      fix n assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m"
-      {assume "n = 0" then have "?r ^ Suc k $ n = a $n"
-          using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp}
-      moreover
-      {fix n1 assume n1: "n = Suc n1"
-        have fK: "finite {0..k}" by simp
-        have nz: "n \<noteq> 0" using n1 by arith
-        let ?Pnk = "natpermute n (k + 1)"
-        let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}"
-        let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}"
-        have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast
-        have d: "?Pnkn \<inter> ?Pnknn = {}" by blast
-        have f: "finite ?Pnkn" "finite ?Pnknn"
-          using finite_Un[of ?Pnkn ?Pnknn, unfolded eq]
-          by (metis natpermute_finite)+
-        let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j"
-        have "sum ?f ?Pnkn = sum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn"
-        proof(rule sum.cong2)
-          fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}"
-          let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k"
-          from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
-            unfolding natpermute_contain_maximal by auto
-          have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))"
-            apply (rule prod.cong, simp)
-            using i r0 by (simp del: replicate.simps)
-          also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
-            unfolding prod_gen_delta[OF fK] using i r0 by simp
-          finally show ?ths .
-        qed
-        then have "sum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k"
-          by (simp add: natpermute_max_card[OF nz, simplified])
-        also have "\<dots> = a$n - sum ?f ?Pnknn"
-          unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc )
-        finally have fn: "sum ?f ?Pnkn = a$n - sum ?f ?Pnknn" .
-        have "(?r ^ Suc k)$n = sum ?f ?Pnkn + sum ?f ?Pnknn"
-          unfolding fps_power_nth_Suc sum.union_disjoint[OF f d, unfolded eq] ..
-        also have "\<dots> = a$n" unfolding fn by simp
-        finally have "?r ^ Suc k $ n = a $n" .}
-      ultimately  show "?r ^ Suc k $ n = a $n" by (cases n, auto)
-  qed }
-  then show ?thesis by (simp add: fps_eq_iff)
-qed
-
-*)
-lemma eq_divide_imp':
-  fixes c :: "'a::field"
-  shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
-  by (simp add: field_simps)
-
 lemma radical_unique:
   assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"
     and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0"
@@ -4552,10 +4428,7 @@
             unfolding Suc_eq_plus1 natpermute_contain_maximal
             by (auto simp del: replicate.simps)
           have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
-            apply (rule prod.cong, simp)
-            using i a0
-            apply (simp del: replicate.simps)
-            done
+            using i a0 by (auto simp del: replicate.simps intro: prod.cong)
           also have "\<dots> = a $ n * (?r $ 0)^k"
             using i by (simp add: prod_gen_delta)
           finally show ?ths .
@@ -4600,20 +4473,14 @@
             unfolded eq, of ?g] by simp
         also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + sum ?f ?Pnknn"
           unfolding th0 th1 ..
-        finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - sum ?f ?Pnknn"
+        finally have \<section>: "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - sum ?f ?Pnknn"
           by simp
-        then have "a$n = (b$n - sum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)"
-          apply -
-          apply (rule eq_divide_imp')
-          using r00
-          apply (simp del: of_nat_Suc)
-          apply (simp add: ac_simps)
-          done
+        have "a$n = (b$n - sum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)"
+          apply (rule eq_divide_imp)
+          using r00 \<section> by (simp_all add: ac_simps del: of_nat_Suc)
         then show ?thesis
-          apply (simp del: of_nat_Suc)
           unfolding fps_radical_def Suc
-          apply (simp add: field_simps Suc th00 del: of_nat_Suc)
-          done
+          by (simp del: of_nat_Suc)
       qed
     qed
     then show ?rhs by (simp add: fps_eq_iff)
@@ -4820,9 +4687,7 @@
     also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}"
       unfolding fps_mult_nth ..
     also have "\<dots> = sum (\<lambda>i. of_nat i * a$i * (sum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}"
-      apply (rule sum.mono_neutral_right)
-      apply (auto simp add: mult_delta_left not_le)
-      done
+      by (intro sum.mono_neutral_right) (auto simp add: mult_delta_left not_le)
     also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
       unfolding fps_deriv_nth
       by (rule sum.reindex_cong [of Suc]) (simp_all add: mult.assoc)
@@ -4833,22 +4698,10 @@
       unfolding fps_mult_nth by (simp add: ac_simps)
     also have "\<dots> = sum (\<lambda>i. sum (\<lambda>j. of_nat (n - i +1) * b$(n - i + 1) * of_nat (j + 1) * a$(j+1) * (b^j)$i) {0..n}) {0..n}"
       unfolding fps_deriv_nth fps_compose_nth sum_distrib_left mult.assoc
-      apply (rule sum.cong)
-      apply (rule refl)
-      apply (rule sum.mono_neutral_left)
-      apply (simp_all add: subset_eq)
-      apply clarify
-      apply (subgoal_tac "b^i$x = 0")
-      apply simp
-      apply (rule startsby_zero_power_prefix[OF b0, rule_format])
-      apply simp
-      done
+      by (auto simp: subset_eq b0 startsby_zero_power_prefix sum.mono_neutral_left intro: sum.cong)
     also have "\<dots> = sum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (sum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
       unfolding sum_distrib_left
-      apply (subst sum.swap)
-      apply (rule sum.cong, rule refl)+
-      apply simp
-      done
+      by (subst sum.swap) (force intro: sum.cong)
     finally show ?thesis
       unfolding th0 by simp
   qed
@@ -4950,13 +4803,16 @@
 qed
 
 lemma fps_inv_ginv: "fps_inv = fps_ginv fps_X"
-  apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
-  apply (induct_tac n rule: nat_less_induct)
-  apply auto
-  apply (case_tac na)
-  apply simp
-  apply simp
-  done
+proof -
+  have "compinv x n = gcompinv fps_X x n" for n and x :: "'a fps"
+  proof (induction n rule: nat_less_induct)
+    case (1 n)
+    then show ?case
+      by (cases n) auto
+  qed
+  then show ?thesis
+    by (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
+qed
 
 lemma fps_compose_1[simp]: "1 oo a = 1"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left)
@@ -5004,80 +4860,32 @@
   let ?S = "{(k::nat, m::nat). k + m \<le> n}"
   have s: "?S \<subseteq> {0..n} \<times> {0..n}" by (simp add: subset_eq)
   have f: "finite {(k::nat, m::nat). k + m \<le> n}"
-    apply (rule finite_subset[OF s])
-    apply auto
-    done
-  have "?r =  sum (\<lambda>i. sum (\<lambda>(k,m). a$k * (c^k)$i * b$m * (d^m) $ (n - i)) {(k,m). k + m \<le> n}) {0..n}"
-    apply (simp add: fps_mult_nth sum_distrib_left)
-    apply (subst sum.swap)
-    apply (rule sum.cong)
-    apply (auto simp add: field_simps)
-    done
-  also have "\<dots> = ?l"
-    apply (simp add: fps_mult_nth fps_compose_nth sum_product)
-    apply (rule sum.cong)
-    apply (rule refl)
+    by (auto intro: finite_subset[OF s])
+  have "?r = (\<Sum>(k, m) \<in> {(k, m). k + m \<le> n}. \<Sum>j = 0..n. a $ k * b $ m * (c ^ k $ j * d ^ m $ (n - j)))"
+    by (simp add: fps_mult_nth sum_distrib_left)
+  also have "\<dots> = (\<Sum>i = 0..n. \<Sum>(k,m)\<in>{(k,m). k+m \<le> n}. a $ k * c ^ k $ i * b $ m * d ^ m $ (n-i))"
+    unfolding sum.swap [where A = "{0..n}"] by (auto simp add: field_simps intro: sum.cong)
+  also have "... = (\<Sum>i = 0..n.
+                    \<Sum>q = 0..i. \<Sum>j = 0..n - i. a $ q * c ^ q $ i * (b $ j * d ^ j $ (n - i)))"
+    apply (rule sum.cong [OF refl])
     apply (simp add: sum.cartesian_product mult.assoc)
-    apply (rule sum.mono_neutral_right[OF f])
-    apply (simp add: subset_eq)
-    apply presburger
-    apply clarsimp
-    apply (rule ccontr)
-    apply (clarsimp simp add: not_le)
-    apply (case_tac "x < aa")
-    apply simp
-    apply (frule_tac startsby_zero_power_prefix[rule_format, OF c0])
-    apply blast
-    apply simp
-    apply (frule_tac startsby_zero_power_prefix[rule_format, OF d0])
-    apply blast
-    done
+    apply (rule sum.mono_neutral_right[OF f], force)
+    by clarsimp (meson c0 d0 leI startsby_zero_power_prefix)
+  also have "\<dots> = ?l"
+    by (simp add: fps_mult_nth fps_compose_nth sum_product)
   finally show ?thesis by simp
 qed
 
-lemma product_composition_lemma':
-  assumes c0: "c$0 = (0::'a::idom)"
-    and d0: "d$0 = 0"
-  shows "((a oo c) * (b oo d))$n =
-    sum (\<lambda>k. sum (\<lambda>m. a$k * b$m * (c^k * d^m) $ n) {0..n}) {0..n}"  (is "?l = ?r")
-  unfolding product_composition_lemma[OF c0 d0]
-  unfolding sum.cartesian_product
-  apply (rule sum.mono_neutral_left)
-  apply simp
-  apply (clarsimp simp add: subset_eq)
-  apply clarsimp
-  apply (rule ccontr)
-  apply (subgoal_tac "(c^aa * d^ba) $ n = 0")
-  apply simp
-  unfolding fps_mult_nth
-  apply (rule sum.neutral)
-  apply (clarsimp simp add: not_le)
-  apply (case_tac "x < aa")
-  apply (rule startsby_zero_power_prefix[OF c0, rule_format])
-  apply simp
-  apply (subgoal_tac "n - x < ba")
-  apply (frule_tac k = "ba" in startsby_zero_power_prefix[OF d0, rule_format])
-  apply simp
-  apply arith
-  done
-
-
 lemma sum_pair_less_iff:
   "sum (\<lambda>((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} =
     sum (\<lambda>s. sum (\<lambda>i. a i * b (s - i) * c s) {0..s}) {0..n}"
   (is "?l = ?r")
 proof -
-  let ?KM = "{(k,m). k + m \<le> n}"
-  let ?f = "\<lambda>s. \<Union>i\<in>{0..s}. {(i, s - i)}"
-  have th0: "?KM = \<Union> (?f ` {0..n})"
+  have th0: "{(k, m). k + m \<le> n} = (\<Union>s\<in>{0..n}. \<Union>i\<in>{0..s}. {(i, s - i)})"
     by auto
-  show "?l = ?r "
+  show "?l = ?r"
     unfolding th0
-    apply (subst sum.UNION_disjoint)
-    apply auto
-    apply (subst sum.UNION_disjoint)
-    apply auto
-    done
+    by (simp add: sum.UNION_disjoint eq_diff_iff disjoint_iff)
 qed
 
 lemma fps_compose_mult_distrib_lemma:
@@ -5089,19 +4897,21 @@
 lemma fps_compose_mult_distrib:
   assumes c0: "c $ 0 = (0::'a::idom)"
   shows "(a * b) oo c = (a oo c) * (b oo c)"
-  apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0])
-  apply (simp add: fps_compose_nth fps_mult_nth sum_distrib_right)
-  done
+proof (clarsimp simp add: fps_eq_iff fps_compose_mult_distrib_lemma [OF c0])
+  show "(a * b oo c) $ n = (\<Sum>s = 0..n. \<Sum>i = 0..s. a $ i * b $ (s - i) * c ^ s $ n)" for n
+    by (simp add: fps_compose_nth fps_mult_nth sum_distrib_right)
+qed
+
 
 lemma fps_compose_prod_distrib:
   assumes c0: "c$0 = (0::'a::idom)"
   shows "prod a S oo c = prod (\<lambda>k. a k oo c) S"
-  apply (cases "finite S")
-  apply simp_all
-  apply (induct S rule: finite_induct)
-  apply simp
-  apply (simp add: fps_compose_mult_distrib[OF c0])
-  done
+proof (induct S rule: infinite_finite_induct)
+next
+  case (insert)
+  then show ?case   
+    by (simp add: fps_compose_mult_distrib[OF c0])
+qed auto
 
 lemma fps_compose_divide:
   assumes [simp]: "g dvd f" "h $ 0 = 0"
@@ -5228,14 +5038,12 @@
         sum_distrib_left mult.assoc fps_sum_nth)
     also have "\<dots> = ((sum (\<lambda>i. fps_const (a$i) * b^i) {0..n}) oo c)$n"
       by (simp add: fps_compose_sum_distrib)
+    also have "... = (\<Sum>i = 0..n. \<Sum>j = 0..n. a $ j * (b ^ j $ i * c ^ i $ n))"
+      by (simp add: fps_compose_nth fps_sum_nth sum_distrib_right mult.assoc)
+    also have "... = (\<Sum>i = 0..n. \<Sum>j = 0..i. a $ j * (b ^ j $ i * c ^ i $ n))"
+      by (intro sum.cong [OF refl] sum.mono_neutral_right; simp add: b0 startsby_zero_power_prefix)
     also have "\<dots> = ?r$n"
-      apply (simp add: fps_compose_nth fps_sum_nth sum_distrib_right mult.assoc)
-      apply (rule sum.cong)
-      apply (rule refl)
-      apply (rule sum.mono_neutral_right)
-      apply (auto simp add: not_le)
-      apply (erule startsby_zero_power_prefix[OF b0, rule_format])
-      done
+      by (simp add: fps_compose_nth  sum_distrib_right mult.assoc)
     finally show ?thesis .
   qed
   then show ?thesis
@@ -5351,19 +5159,13 @@
   then have "?r b (?r c a) oo ?r c a oo a = b oo a"
     by simp
   then have "?r b (?r c a) oo (?r c a oo a) = b oo a"
-    apply (subst fps_compose_assoc)
-    using a0 c0
-    apply (simp_all add: fps_ginv_def)
-    done
+    by (simp add: a0 fps_compose_assoc rca0)
   then have "?r b (?r c a) oo c = b oo a"
     unfolding fps_ginv[OF a0 a1] .
   then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c"
     by simp
   then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c"
-    apply (subst fps_compose_assoc)
-    using a0 c0
-    apply (simp_all add: fps_inv_def)
-    done
+    by (metis c0 c1 fps_compose_assoc fps_compose_nth_0 fps_inv fps_inv_right)
   then show ?thesis
     unfolding fps_inv_right[OF c0 c1] by simp
 qed
@@ -5417,10 +5219,7 @@
   (is "?l = ?r")
 proof -
   have "?l$n = ?r $ n" for n
-    apply (auto simp add: fps_exp_def field_simps power_Suc[symmetric]
-      simp del: fact_Suc of_nat_Suc power_Suc)
-    apply (simp add: field_simps)
-    done
+    using of_nat_neq_0 by (auto simp add: fps_exp_def divide_simps)
   then show ?thesis
     by (simp add: fps_eq_iff)
 qed
@@ -5440,11 +5239,7 @@
     next
       case Suc
       then show ?case
-        unfolding th
-        using fact_gt_zero
-        apply (simp add: field_simps del: of_nat_Suc fact_Suc)
-        apply simp
-        done
+        by (simp add: th divide_simps)
     qed
     show ?thesis
       by (auto simp add: fps_eq_iff fps_const_mult_left fps_exp_def intro: th')
@@ -5581,9 +5376,7 @@
     (fps_const a * (fps_exp a - 1) + fps_const a) oo fps_inv (fps_exp a - 1)"
     by (simp add: field_simps)
   also have "\<dots> = fps_const a * (fps_X + 1)"
-    apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
-    apply (simp add: field_simps)
-    done
+    by (simp add: fps_compose_add_distrib fps_inv_right[OF b0 b1] distrib_left flip: fps_const_mult_apply_left)
   finally have eq: "fps_deriv (fps_exp a - 1) oo fps_inv (fps_exp a - 1) = fps_const a * (fps_X + 1)" .
   from fps_inv_deriv[OF b0 b1, unfolded eq]
   have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (fps_X + 1)"
@@ -5604,9 +5397,7 @@
   have "fps_deriv ?r = fps_const (1/c + 1/d) * inverse (1 + fps_X)"
     by (simp add: fps_ln_deriv fps_const_add[symmetric] algebra_simps del: fps_const_add)
   also have "\<dots> = fps_deriv ?l"
-    apply (simp add: fps_ln_deriv)
-    apply (simp add: fps_eq_iff eq)
-    done
+    by (simp add: eq fps_ln_deriv)
   finally show ?thesis
     unfolding fps_deriv_eq_iff by simp
 qed
@@ -5641,9 +5432,8 @@
     have x10: "?x1 $ 0 \<noteq> 0" by simp
     have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp
     also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1"
-      apply (simp only: fps_divide_def  mult.assoc[symmetric] inverse_mult_eq_1[OF x10])
-      apply (simp add: field_simps)
-      done
+      unfolding fps_divide_def  mult.assoc[symmetric] inverse_mult_eq_1[OF x10]
+      by (simp add: field_simps)
     finally show ?thesis .
   qed
 
@@ -5654,10 +5444,7 @@
     proof -
       from h have "?l $ n = ?r $ n" by simp
       then show ?thesis
-        apply (simp add: field_simps del: of_nat_Suc)
-        apply (cases n)
-        apply (simp_all add: field_simps del: of_nat_Suc)
-        done
+        by (simp add: field_simps del: of_nat_Suc split: if_split_asm)
     qed
     have th1: "a $ n = (c gchoose n) * a $ 0" for n
     proof (induct n)
@@ -5665,31 +5452,32 @@
       then show ?case by simp
     next
       case (Suc m)
-      then show ?case
+      have "(c - of_nat m) * (c gchoose m) = (c gchoose Suc m) * of_nat (Suc m)"
+        by (metis gbinomial_absorb_comp gbinomial_absorption mult.commute)
+      with Suc show ?case
         unfolding th0
-        apply (simp add: field_simps del: of_nat_Suc)
-        unfolding mult.assoc[symmetric] gbinomial_mult_1
-        apply (simp add: field_simps)
-        done
+        by (simp add: divide_simps del: of_nat_Suc)
     qed
     show ?thesis
-      apply (simp add: fps_eq_iff)
-      apply (subst th1)
-      apply (simp add: field_simps)
-      done
+      by (metis expand_fps_eq fps_binomial_nth fps_mult_right_const_nth mult.commute th1)
   qed
 
   show ?lhs if ?rhs
   proof -
     have th00: "x * (a $ 0 * y) = a $ 0 * (x * y)" for x y
       by (simp add: mult.commute)
-    have "?l = ?r"
-      apply (subst \<open>?rhs\<close>)
-      apply (subst (2) \<open>?rhs\<close>)
-      apply (clarsimp simp add: fps_eq_iff field_simps)
-      unfolding mult.assoc[symmetric] th00 gbinomial_mult_1
-      apply (simp add: field_simps gbinomial_mult_1)
-      done
+    have "?l = (1 + fps_X) * fps_deriv (fps_const (a $ 0) * fps_binomial c)"
+      using that by auto
+    also have "... = fps_const c * (fps_const (a $ 0) * fps_binomial c)"
+    proof (clarsimp simp add: fps_eq_iff algebra_simps)
+      show "a $ 0 * (c gchoose Suc n) + (of_nat n * ((c gchoose n) * a $ 0) + of_nat n * (a $ 0 * (c gchoose Suc n))) 
+         = c * ((c gchoose n) * a $ 0)" for n
+      unfolding mult.assoc[symmetric]  
+      by (simp add: field_simps gbinomial_mult_1)
+  qed
+    also have "... = ?r"
+      using that by auto
+    finally have "?l = ?r" .
     with eq show ?thesis ..
   qed
 qed
@@ -5812,13 +5600,19 @@
 
 
 lemma one_minus_const_fps_X_neg_power':
-  "n > 0 \<Longrightarrow> inverse ((1 - fps_const (c :: 'a :: field_char_0) * fps_X) ^ n) =
-       Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
-  apply (rule fps_ext)
-  apply (subst one_minus_fps_X_const_neg_power, subst fps_const_neg, subst fps_compose_linear)
-  apply (simp add: power_mult_distrib [symmetric] mult.assoc [symmetric] 
-                   gbinomial_minus binomial_gbinomial of_nat_diff)
-  done
+  fixes c :: "'a :: field_char_0"
+  assumes "n > 0"
+  shows "inverse ((1 - fps_const c * fps_X) ^ n) = Abs_fps (\<lambda>k. of_nat ((n + k - 1) choose k) * c^k)"
+proof -
+  have \<section>: "\<And>j. Abs_fps (\<lambda>na. (- c) ^ na * fps_binomial (- of_nat n) $ na) $ j =
+          Abs_fps (\<lambda>k. of_nat (n + k - 1 choose k) * c ^ k) $ j"
+    using assms
+    by (simp add: gbinomial_minus binomial_gbinomial of_nat_diff flip: power_mult_distrib mult.assoc)
+  show ?thesis
+    apply (rule fps_ext)
+    using \<section> 
+    by (metis (no_types, lifting) one_minus_fps_X_const_neg_power fps_const_neg fps_compose_linear fps_nth_Abs_fps)
+qed
 
 text \<open>Vandermonde's Identity as a consequence.\<close>
 lemma gbinomial_Vandermonde:
@@ -5840,14 +5634,11 @@
 lemma binomial_Vandermonde_same: "sum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2 * n) choose n"
   using binomial_Vandermonde[of n n n, symmetric]
   unfolding mult_2
-  apply (simp add: power2_eq_square)
-  apply (rule sum.cong)
-  apply (auto intro:  binomial_symmetric)
-  done
+  by (metis atMost_atLeast0 choose_square_sum mult_2)
 
 lemma Vandermonde_pochhammer_lemma:
   fixes a :: "'a::field_char_0"
-  assumes b: "\<forall>j\<in>{0 ..<n}. b \<noteq> of_nat j"
+  assumes b: "\<And>j. j<n \<Longrightarrow> b \<noteq> of_nat j"
   shows "sum (\<lambda>k. (pochhammer (- a) k * pochhammer (- (of_nat n)) k) /
       (of_nat (fact k) * pochhammer (b - of_nat n + 1) k)) {0..n} =
     pochhammer (- (a + b)) n / pochhammer (- b) n"
@@ -5878,7 +5669,8 @@
         by (simp add: algebra_simps)
       then have "b = of_nat (n - j - 1)"
         using j kn by (simp add: of_nat_diff)
-      with b show False using j by auto
+      then show False 
+        using \<open>j < n\<close> j b by auto
     qed
 
     from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0"
@@ -5901,54 +5693,48 @@
       show ?thesis
       proof (cases "k = n")
         case True
-        then show ?thesis
-          using pochhammer_minus'[where k=k and b=b]
-          apply (simp add: pochhammer_same)
-          using bn0
-          apply (simp add: field_simps power_add[symmetric])
-          done
+        with pochhammer_minus'[where k=k and b=b] bn0 show ?thesis       
+          by (simp add: pochhammer_same)
       next
         case False
         with kn have kn': "k < n"
           by simp
+        have "h \<le> m"
+          using \<open>k \<le> n\<close> h m by blast
         have m1nk: "?m1 n = prod (\<lambda>i. - 1) {..m}" "?m1 k = prod (\<lambda>i. - 1) {0..h}"
-          by (simp_all add: prod_constant m h)
+          by (simp_all add: m h)
         have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0"
           using bn0 kn
           unfolding pochhammer_eq_0_iff
-          apply auto
-          apply (erule_tac x= "n - ka - 1" in allE)
-          apply (auto simp add: algebra_simps of_nat_diff)
-          done
+          by (metis add.commute add_diff_eq nz' pochhammer_eq_0_iff)
         have eq1: "prod (\<lambda>k. (1::'a) + of_nat m - of_nat k) {..h} =
           prod of_nat {Suc (m - h) .. Suc m}"
           using kn' h m
           by (intro prod.reindex_bij_witness[where i="\<lambda>k. Suc m - k" and j="\<lambda>k. Suc m - k"])
              (auto simp: of_nat_diff)
-        have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
-          apply (simp add: pochhammer_minus field_simps)
-          using \<open>k \<le> n\<close> apply (simp add: fact_split [of k n])
-          apply (simp add: pochhammer_prod)
+        have "(\<Prod>i = 0..<k. 1 + of_nat n - of_nat k + of_nat i) = (\<Prod>x = n - k..<n. (1::'a) + of_nat x)"
+          using \<open>k \<le> n\<close> 
           using prod.atLeastLessThan_shift_bounds [where ?'a = 'a, of "\<lambda>i. 1 + of_nat i" 0 "n - k" k]
-          apply (auto simp add: of_nat_diff field_simps)
-          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 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 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
+          by (auto simp add: of_nat_diff field_simps)
+        then have "fact (n - k) * pochhammer ((1::'a) + of_nat n - of_nat k) k = fact n"
+          using \<open>k \<le> n\<close> 
+          by (auto simp add: fact_split [of k n] pochhammer_prod field_simps)
+        then have th1: "(?m1 k * ?p (of_nat n) k) / ?f n = 1 / of_nat(fact (n - k))"
+          by (simp add: pochhammer_minus field_simps)
+        have "?m1 n * ?p b n = pochhammer (b - of_nat m) (Suc m)"
+          by (simp add: pochhammer_minus field_simps m)
+        also have "... = (\<Prod>i = 0..m. b - of_nat i)"
+          by (auto simp add: pochhammer_prod_rev of_nat_diff prod.atLeast_Suc_atMost_Suc_shift simp del: prod.cl_ivl_Suc)
+        finally have th20: "?m1 n * ?p b n = prod (\<lambda>i. b - of_nat i) {0..m}" .
+        have "(\<Prod>x = 0..h. b - of_nat m + of_nat (h - x)) = (\<Prod>i = m - h..m. b - of_nat i)"
+          using \<open>h \<le> m\<close> prod.atLeastAtMost_shift_0 [of "m - h" m, where ?'a = 'a]
+          by (auto simp add: of_nat_diff field_simps)
+        then have th21:"pochhammer (b - of_nat n + 1) k = prod (\<lambda>i. b - of_nat i) {n - k .. n - 1}"
+          using kn by (simp add: pochhammer_prod_rev m h prod.atLeast_Suc_atMost_Suc_shift del: prod.op_ivl_Suc del: prod.cl_ivl_Suc)
         have "?m1 n * ?p b n =
           prod (\<lambda>i. b - of_nat i) {0.. n - k - 1} * pochhammer (b - of_nat n + 1) k"
-          using kn' m h unfolding th20 th21 apply simp
-          apply (subst prod.union_disjoint [symmetric])
-          apply auto
-          apply (rule prod.cong)
-          apply auto
-          done
+          using kn' m h unfolding th20 th21 
+          by (auto simp flip: prod.union_disjoint intro: prod.cong)
         then have th2: "(?m1 n * ?p b n)/pochhammer (b - of_nat n + 1) k =
           prod (\<lambda>i. b - of_nat i) {0.. n - k - 1}"
           using nz' by (simp add: field_simps)
@@ -5959,29 +5745,21 @@
         also have "\<dots> = b gchoose (n - k)"
           unfolding th1 th2
           using kn' m h
-          apply (simp add: field_simps gbinomial_mult_fact)
-          apply (rule prod.cong)
-          apply auto
-          done
+          by (auto simp: field_simps gbinomial_mult_fact intro: prod.cong)
         finally show ?thesis by simp
       qed
     qed
     then show ?gchoose and ?pochhammer
-      apply (cases "n = 0")
-      using nz'
-      apply auto
-      done
+      using nz' by force+
   qed
   have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))"
     unfolding gbinomial_pochhammer
     using bn0 by (auto simp add: field_simps)
   also have "\<dots> = ?l"
+    using bn0
     unfolding gbinomial_Vandermonde[symmetric]
     apply (simp add: th00)
-    unfolding gbinomial_pochhammer
-    using bn0
-    apply (simp add: sum_distrib_right sum_distrib_left field_simps)
-    done
+    by (simp add: gbinomial_pochhammer sum_distrib_right sum_distrib_left field_simps)
   finally show ?thesis by simp
 qed
 
@@ -5993,12 +5771,13 @@
 proof -
   let ?a = "- a"
   let ?b = "c + of_nat n - 1"
-  have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j"
-    using c
-    apply (auto simp add: algebra_simps of_nat_diff)
-    apply (erule_tac x = "n - j - 1" in ballE)
-    apply (auto simp add: of_nat_diff algebra_simps)
-    done
+  have h: "?b \<noteq> of_nat j" if "j < n" for j
+  proof -
+    have "c \<noteq> - of_nat (n - j - 1)"
+      using c that by auto
+    with that show ?thesis
+      by (auto simp add: algebra_simps of_nat_diff)
+  qed
   have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
     unfolding pochhammer_minus
     by (simp add: algebra_simps)
@@ -6086,9 +5865,7 @@
   (is "?lhs = _")
 proof -
   have "fps_deriv ?lhs = 0"
-    apply (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv)
-    apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg)
-    done
+    by (simp add:  fps_deriv_power fps_sin_deriv fps_cos_deriv field_simps flip: fps_const_neg)
   then have "?lhs = fps_const (?lhs $ 0)"
     unfolding fps_deriv_eq_0_iff .
   also have "\<dots> = 1"
@@ -6099,83 +5876,95 @@
 lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0"
   unfolding fps_sin_def by simp
 
-lemma fps_sin_nth_1 [simp]: "fps_sin c $ 1 = c"
+lemma fps_sin_nth_1 [simp]: "fps_sin c $ Suc 0 = c"
   unfolding fps_sin_def by simp
 
 lemma fps_sin_nth_add_2:
     "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat (n + 1) * of_nat (n + 2)))"
-  unfolding fps_sin_def
-  apply (cases n)
-  apply simp
-  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
-  apply simp
-  done
+proof (cases n)
+  case (Suc n')
+  then show ?thesis
+    unfolding fps_sin_def by (simp add: field_simps)
+qed (auto simp: fps_sin_def)
+
 
 lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1"
   unfolding fps_cos_def by simp
 
-lemma fps_cos_nth_1 [simp]: "fps_cos c $ 1 = 0"
+lemma fps_cos_nth_1 [simp]: "fps_cos c $ Suc 0 = 0"
   unfolding fps_cos_def by simp
 
 lemma fps_cos_nth_add_2:
   "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat (n + 1) * of_nat (n + 2)))"
-  unfolding fps_cos_def
-  apply (simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq del: of_nat_Suc fact_Suc)
-  apply simp
-  done
+proof (cases n)
+  case (Suc n')
+  then show ?thesis
+    unfolding fps_cos_def by (simp add: field_simps)
+qed (auto simp: fps_cos_def)
 
 lemma nat_add_1_add_1: "(n::nat) + 1 + 1 = n + 2"
   by simp
 
 lemma eq_fps_sin:
-  assumes 0: "a $ 0 = 0"
-    and 1: "a $ 1 = c"
-    and 2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)"
-  shows "a = fps_sin c"
-  apply (rule fps_ext)
-  apply (induct_tac n rule: nat_induct2)
-  apply (simp add: 0)
-  apply (simp add: 1 del: One_nat_def)
-  apply (rename_tac m, cut_tac f="\<lambda>a. a $ m" in arg_cong [OF 2])
-  apply (simp add: nat_add_1_add_1 fps_sin_nth_add_2
-              del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
-  apply (subst minus_divide_left)
-  apply (subst nonzero_eq_divide_eq)
-  apply (simp del: of_nat_add of_nat_Suc)
-  apply (simp only: ac_simps)
-  done
+  assumes a0: "a $ 0 = 0"
+    and a1: "a $ 1 = c"
+    and a2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)"
+  shows "fps_sin c = a"
+proof (rule fps_ext)
+  fix n
+  show "fps_sin c $ n = a $ n"
+  proof (induction n rule: nat_induct2)
+    case (step n)
+    then have "of_nat (n + 1) * (of_nat (n + 2) * a $ (n + 2)) =
+     - (c * c * fps_sin c $ n)"
+      using a2
+      by (metis fps_const_mult fps_deriv_nth fps_mult_left_const_nth fps_neg_nth nat_add_1_add_1)
+    with step show ?case
+      by (metis (no_types, lifting) a0 add.commute add.inverse_inverse fps_sin_nth_0 fps_sin_nth_add_2 mult_divide_mult_cancel_left_if mult_minus_right nonzero_mult_div_cancel_left not_less_zero of_nat_eq_0_iff plus_1_eq_Suc zero_less_Suc)
+  qed (use assms in auto)
+qed
 
 lemma eq_fps_cos:
-  assumes 0: "a $ 0 = 1"
-    and 1: "a $ 1 = 0"
-    and 2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)"
-  shows "a = fps_cos c"
-  apply (rule fps_ext)
-  apply (induct_tac n rule: nat_induct2)
-  apply (simp add: 0)
-  apply (simp add: 1 del: One_nat_def)
-  apply (rename_tac m, cut_tac f="\<lambda>a. a $ m" in arg_cong [OF 2])
-  apply (simp add: nat_add_1_add_1 fps_cos_nth_add_2
-              del: One_nat_def of_nat_Suc of_nat_add add_2_eq_Suc')
-  apply (subst minus_divide_left)
-  apply (subst nonzero_eq_divide_eq)
-  apply (simp del: of_nat_add of_nat_Suc)
-  apply (simp only: ac_simps)
-  done
+  assumes a0: "a $ 0 = 1"
+    and a1: "a $ 1 = 0"
+    and a2: "fps_deriv (fps_deriv a) = - (fps_const c * fps_const c * a)"
+  shows "fps_cos c = a"
+proof (rule fps_ext)
+  fix n
+  show "fps_cos c $ n = a $ n"
+  proof (induction n rule: nat_induct2)
+    case (step n)
+    then have "of_nat (n + 1) * (of_nat (n + 2) * a $ (n + 2)) =
+     - (c * c * fps_cos c $ n)"
+      using a2
+      by (metis fps_const_mult fps_deriv_nth fps_mult_left_const_nth fps_neg_nth nat_add_1_add_1)
+    with step show ?case
+      by (metis (no_types, lifting) a0 add.commute add.inverse_inverse fps_cos_nth_0 fps_cos_nth_add_2 mult_divide_mult_cancel_left_if mult_minus_right nonzero_mult_div_cancel_left not_less_zero of_nat_eq_0_iff plus_1_eq_Suc zero_less_Suc)
+  qed (use assms in auto)
+qed
 
 lemma fps_sin_add: "fps_sin (a + b) = fps_sin a * fps_cos b + fps_cos a * fps_sin b"
-  apply (rule eq_fps_sin [symmetric], simp, simp del: One_nat_def)
-  apply (simp del: fps_const_neg fps_const_add fps_const_mult
-              add: fps_const_add [symmetric] fps_const_neg [symmetric]
-                   fps_sin_deriv fps_cos_deriv algebra_simps)
-  done
+proof -
+  have "fps_deriv (fps_deriv (fps_sin a * fps_cos b + fps_cos a * fps_sin b)) =
+         - (fps_const (a + b) * fps_const (a + b) * (fps_sin a * fps_cos b + fps_cos a * fps_sin b))"
+    by (simp flip: fps_const_neg fps_const_add fps_const_mult
+        add: fps_sin_deriv fps_cos_deriv algebra_simps)
+  then show ?thesis
+    by (auto intro: eq_fps_sin)
+qed
+
 
 lemma fps_cos_add: "fps_cos (a + b) = fps_cos a * fps_cos b - fps_sin a * fps_sin b"
-  apply (rule eq_fps_cos [symmetric], simp, simp del: One_nat_def)
-  apply (simp del: fps_const_neg fps_const_add fps_const_mult
-              add: fps_const_add [symmetric] fps_const_neg [symmetric]
-                   fps_sin_deriv fps_cos_deriv algebra_simps)
-  done
+proof -
+  have "fps_deriv
+     (fps_deriv (fps_cos a * fps_cos b - fps_sin a * fps_sin b)) =
+    - (fps_const (a + b) * fps_const (a + b) *
+       (fps_cos a * fps_cos b - fps_sin a * fps_sin b))"
+    by (simp flip: fps_const_neg fps_const_add fps_const_mult
+        add: fps_sin_deriv fps_cos_deriv algebra_simps)
+  then show ?thesis
+    by (auto intro: eq_fps_cos)
+qed
 
 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
   by (simp add: fps_eq_iff fps_sin_def)
@@ -6247,10 +6036,8 @@
 lemma fps_tan_fps_exp_ii:
   "fps_tan c = (fps_exp (\<i> * c) - fps_exp (- \<i> * c)) / 
       (fps_const \<i> * (fps_exp (\<i> * c) + fps_exp (- \<i> * c)))"
-  unfolding fps_tan_def fps_sin_fps_exp_ii fps_cos_fps_exp_ii mult_minus_left fps_exp_neg
-  apply (simp add: fps_divide_unit fps_inverse_mult fps_const_mult[symmetric] fps_const_inverse del: fps_const_mult)
-  apply simp
-  done
+  unfolding fps_tan_def fps_sin_fps_exp_ii fps_cos_fps_exp_ii
+  by (simp add: fps_divide_unit fps_inverse_mult fps_const_inverse)
 
 lemma fps_demoivre:
   "(fps_cos a + fps_const \<i> * fps_sin a)^n =
@@ -6301,12 +6088,12 @@
   by (simp add: fps_eq_iff gbinomial_pochhammer algebra_simps)
 
 lemma fps_hypergeo_0[simp]: "fps_hypergeo as bs c $ 0 = 1"
-  apply simp
-  apply (subgoal_tac "\<forall>as. foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1")
-  apply auto
-  apply (induct_tac as)
-  apply auto
-  done
+proof -
+  have "foldl (\<lambda>(r::'a) (a::'a). r) 1 as = 1" for as
+    by (induction as) auto
+  then show ?thesis
+    by auto
+qed
 
 lemma foldl_prod_prod:
   "foldl (\<lambda>(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (\<lambda>r x. r * g x) w as =
@@ -6317,11 +6104,9 @@
 lemma fps_hypergeo_rec:
   "fps_hypergeo as bs c $ Suc n = ((foldl (\<lambda>r a. r* (a + of_nat n)) c as) /
     (foldl (\<lambda>r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * fps_hypergeo as bs c $ n"
-  apply (simp del: of_nat_Suc of_nat_add fact_Suc)
-  apply (simp add: foldl_mult_start del: fact_Suc of_nat_Suc)
+  apply (simp add: foldl_mult_start del: of_nat_Suc of_nat_add fact_Suc)
   unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
-  apply (simp add: algebra_simps)
-  done
+  by (simp add: algebra_simps)
 
 lemma fps_XD_nth[simp]: "fps_XD a $ n = of_nat n * a$n"
   by (simp add: fps_XD_def)
@@ -6359,12 +6144,6 @@
      else 0)"
   by (simp_all add: pochhammer_eq_0_iff)
 
-lemma sum_eq_if: "sum f {(n::nat) .. m} = (if m < n then 0 else f n + sum f {n+1 .. m})"
-  apply simp
-  apply (subst sum.insert[symmetric])
-  apply (auto simp add: not_less sum.atLeast_Suc_atMost)
-  done
-
 lemma pochhammer_rec_if: "pochhammer a n = (if n = 0 then 1 else a * pochhammer (a + 1) (n - 1))"
   by (cases n) (simp_all add: pochhammer_rec)
 
diff -r a7877e14e7f8 -r 8e5428ff35af src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Nov 22 13:31:33 2020 +0100
+++ b/src/HOL/Set_Interval.thy	Sun Nov 22 18:26:54 2020 +0000
@@ -1921,6 +1921,15 @@
   finally show ?thesis .
 qed
 
+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 head_if:
+  fixes n :: nat
+  shows "F g {m..n} = (if n < m then \<^bold>1 else  F g {m..<n} \<^bold>* g(n))"
+  by (simp add: commute last_plus)
+
 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}"
@@ -2002,10 +2011,6 @@
   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)