author paulson Sun, 22 Nov 2020 18:26:45 +0000 changeset 72686 703b601d71b5 parent 72645 f8cc3153ac77 child 72687 8e5428ff35af
cleanup of old proofs
```--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Wed Nov 18 18:45:50 2020 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy	Sun Nov 22 18:26:45 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"
+
+lemma fps_mult_nth_1' [simp]: "(f * g) \$ Suc 0 = f\$0 * g\$Suc 0 + f\$Suc 0 * g\$0"

lemmas mult_nth_0 = fps_mult_nth_0
@@ -1976,35 +1979,6 @@
fps_const (inverse (of_nat n))"

-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
+  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"
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 @@

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])
-    done
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 (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)"
-      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 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 @@

+lemma radical_0 [simp]: "\<And>n. 0 < n \<Longrightarrow> radical r 0 a n = 0"
+
-  apply (case_tac n)
-  apply auto
-  done

lemma fps_radical_nth_0[simp]: "fps_radical r n a \$ 0 = (if n = 0 then 1 else r n (a\$0))"
@@ -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

-(*
-  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"
-
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)
-          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)
-          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 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 (rule sum.mono_neutral_right[OF f])
-    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"
+    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
-    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
-    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)
-    done
+    using of_nat_neq_0 by (auto simp add: fps_exp_def divide_simps)
then show ?thesis
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)"
also have "\<dots> = fps_const a * (fps_X + 1)"
-    done
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)"
also have "\<dots> = fps_deriv ?l"
-    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])
-      done
+      unfolding fps_divide_def  mult.assoc[symmetric] inverse_mult_eq_1[OF x10]
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
-        done
+        by (simp add: divide_simps del: of_nat_Suc)
qed
show ?thesis
-      apply (subst th1)
-      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
-    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 (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 @@
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]
-          using bn0
-          done
+        with pochhammer_minus'[where k=k and b=b] bn0 show ?thesis
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
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])
+        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]
-    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
@@ -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

"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

"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)

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: 1 del: One_nat_def)
-  apply (rename_tac m, cut_tac f="\<lambda>a. a \$ m" in arg_cong [OF 2])
-  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
+    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: 1 del: One_nat_def)
-  apply (rename_tac m, cut_tac f="\<lambda>a. a \$ m" in arg_cong [OF 2])
-  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
+    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
-                   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
+  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
-                   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
+  then show ?thesis
+    by (auto intro: eq_fps_cos)
+qed

lemma fps_sin_even: "fps_sin (- c) = - fps_sin c"
@@ -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)
unfolding foldl_prod_prod[unfolded foldl_mult_start] pochhammer_Suc
-  done

lemma fps_XD_nth[simp]: "fps_XD a \$ n = of_nat n * a\$n"
@@ -6359,12 +6144,6 @@
else 0)"

-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)
```
```--- a/src/HOL/Set_Interval.thy	Wed Nov 18 18:45:50 2020 +0000
+++ b/src/HOL/Set_Interval.thy	Sun Nov 22 18:26:45 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)
+
+  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)
+