# HG changeset patch
# User wenzelm
# Date 1375910411 -7200
# Node ID 6c89225ddeba84dfe094af039185952b2037e0d3
# Parent  7196e1ce1cd825252a570a95516fe7f3eac82926
tuned proofs;

diff -r 7196e1ce1cd8 -r 6c89225ddeba src/HOL/Library/Binomial.thy
--- a/src/HOL/Library/Binomial.thy	Wed Aug 07 21:16:20 2013 +0200
+++ b/src/HOL/Library/Binomial.thy	Wed Aug 07 23:20:11 2013 +0200
@@ -12,10 +12,10 @@
 text {* This development is based on the work of Andy Gordon and
   Florian Kammueller. *}
 
-primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65) where
-  binomial_0: "(0 choose k) = (if k = 0 then 1 else 0)"
-| binomial_Suc: "(Suc n choose k) =
-                 (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
+primrec binomial :: "nat \<Rightarrow> nat \<Rightarrow> nat" (infixl "choose" 65)
+where
+  "0 choose k = (if k = 0 then 1 else 0)"
+| "Suc n choose k = (if k = 0 then 1 else (n choose (k - 1)) + (n choose k))"
 
 lemma binomial_n_0 [simp]: "(n choose 0) = 1"
   by (cases n) simp_all
@@ -23,41 +23,40 @@
 lemma binomial_0_Suc [simp]: "(0 choose Suc k) = 0"
   by simp
 
-lemma binomial_Suc_Suc [simp]:
-  "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
+lemma binomial_Suc_Suc [simp]: "(Suc n choose Suc k) = (n choose k) + (n choose Suc k)"
   by simp
 
-lemma binomial_eq_0: "!!k. n < k ==> (n choose k) = 0"
-  by (induct n) auto
+lemma binomial_eq_0: "n < k \<Longrightarrow> n choose k = 0"
+  by (induct n arbitrary: k) auto
 
-declare binomial_0 [simp del] binomial_Suc [simp del]
+declare binomial.simps [simp del]
 
-lemma binomial_n_n [simp]: "(n choose n) = 1"
+lemma binomial_n_n [simp]: "n choose n = 1"
   by (induct n) (simp_all add: binomial_eq_0)
 
-lemma binomial_Suc_n [simp]: "(Suc n choose n) = Suc n"
+lemma binomial_Suc_n [simp]: "Suc n choose n = Suc n"
   by (induct n) simp_all
 
-lemma binomial_1 [simp]: "(n choose Suc 0) = n"
+lemma binomial_1 [simp]: "n choose Suc 0 = n"
   by (induct n) simp_all
 
-lemma zero_less_binomial: "k \<le> n ==> (n choose k) > 0"
+lemma zero_less_binomial: "k \<le> n \<Longrightarrow> n choose k > 0"
   by (induct n k rule: diff_induct) simp_all
 
-lemma binomial_eq_0_iff: "(n choose k = 0) = (n<k)"
+lemma binomial_eq_0_iff: "n choose k = 0 \<longleftrightarrow> n < k"
   apply (safe intro!: binomial_eq_0)
   apply (erule contrapos_pp)
   apply (simp add: zero_less_binomial)
   done
 
-lemma zero_less_binomial_iff: "(n choose k > 0) = (k\<le>n)"
+lemma zero_less_binomial_iff: "n choose k > 0 \<longleftrightarrow> k \<le> n"
   by (simp add: linorder_not_less binomial_eq_0_iff neq0_conv[symmetric] del: neq0_conv)
 
 (*Might be more useful if re-oriented*)
 lemma Suc_times_binomial_eq:
-  "!!k. k \<le> n ==> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
-  apply (induct n)
-   apply (simp add: binomial_0)
+  "k \<le> n \<Longrightarrow> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+  apply (induct n arbitrary: k)
+   apply (simp add: binomial.simps)
    apply (case_tac k)
   apply (auto simp add: add_mult_distrib add_mult_distrib2 le_Suc_eq binomial_eq_0)
   done
@@ -65,15 +64,14 @@
 text{*This is the well-known version, but it's harder to use because of the
   need to reason about division.*}
 lemma binomial_Suc_Suc_eq_times:
-    "k \<le> n ==> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
+    "k \<le> n \<Longrightarrow> (Suc n choose Suc k) = (Suc n * (n choose k)) div Suc k"
   by (simp add: Suc_times_binomial_eq del: mult_Suc mult_Suc_right)
 
 text{*Another version, with -1 instead of Suc.*}
 lemma times_binomial_minus1_eq:
-    "[|k \<le> n;  0<k|] ==> (n choose k) * k = n * ((n - 1) choose (k - 1))"
-  apply (cut_tac n = "n - 1" and k = "k - 1" in Suc_times_binomial_eq)
-   apply (simp split add: nat_diff_split, auto)
-  done
+  "k \<le> n \<Longrightarrow> 0 < k \<Longrightarrow> (n choose k) * k = n * ((n - 1) choose (k - 1))"
+  using Suc_times_binomial_eq [where n = "n - 1" and k = "k - 1"]
+  by (auto split add: nat_diff_split)
 
 
 subsection {* Theorems about @{text "choose"} *}
@@ -83,17 +81,17 @@
   Kamm\"uller, tidied by LCP.
 *}
 
-lemma card_s_0_eq_empty: "finite A ==> card {B. B \<subseteq> A & card B = 0} = 1"
+lemma card_s_0_eq_empty: "finite A \<Longrightarrow> card {B. B \<subseteq> A & card B = 0} = 1"
   by (simp cong add: conj_cong add: finite_subset [THEN card_0_eq])
 
-lemma choose_deconstruct: "finite M ==> x \<notin> M
-  ==> {s. s <= insert x M & card(s) = Suc k}
-       = {s. s <= M & card(s) = Suc k} Un
-         {s. EX t. t <= M & card(t) = k & s = insert x t}"
+lemma choose_deconstruct: "finite M \<Longrightarrow> x \<notin> M \<Longrightarrow>
+    {s. s \<subseteq> insert x M \<and> card s = Suc k} =
+    {s. s \<subseteq> M \<and> card s = Suc k} \<union> {s. \<exists>t. t \<subseteq> M \<and> card t = k \<and> s = insert x t}"
   apply safe
      apply (auto intro: finite_subset [THEN card_insert_disjoint])
   apply (drule_tac x = "xa - {x}" in spec)
-  apply (subgoal_tac "x \<notin> xa", auto)
+  apply (subgoal_tac "x \<notin> xa")
+   apply auto
   apply (erule rev_mp, subst card_Diff_singleton)
     apply (auto intro: finite_subset)
   done
@@ -102,27 +100,30 @@
 apply simp
 lemma Collect_ex_eq
 
-lemma "{x. EX y. P x y} = (UN y. {x. P x y})"
+lemma "{x. \<exists>y. P x y} = (UN y. {x. P x y})"
 apply blast
 *)
 
-lemma finite_bex_subset[simp]:
-  "finite B \<Longrightarrow> (!!A. A<=B \<Longrightarrow> finite{x. P x A}) \<Longrightarrow> finite{x. EX A<=B. P x A}"
-  apply (subgoal_tac "{x. EX A<=B. P x A} = (UN A:Pow B. {x. P x A})")
-   apply simp
-  apply blast
-  done
+lemma finite_bex_subset [simp]:
+  assumes "finite B"
+    and "\<And>A. A \<subseteq> B \<Longrightarrow> finite {x. P x A}"
+  shows "finite {x. \<exists>A \<subseteq> B. P x A}"
+proof -
+  have "{x. \<exists>A\<subseteq>B. P x A} = (\<Union>A \<in> Pow B. {x. P x A})" by blast
+  with assms show ?thesis by simp
+qed
 
 text{*There are as many subsets of @{term A} having cardinality @{term k}
  as there are sets obtained from the former by inserting a fixed element
  @{term x} into each.*}
 lemma constr_bij:
-   "[|finite A; x \<notin> A|] ==>
-    card {B. EX C. C <= A & card(C) = k & B = insert x C} =
-    card {B. B <= A & card(B) = k}"
-  apply (rule_tac f = "%s. s - {x}" and g = "insert x" in card_bij_eq)
+   "finite A \<Longrightarrow> x \<notin> A \<Longrightarrow>
+    card {B. \<exists>C. C \<subseteq> A \<and> card C = k \<and> B = insert x C} =
+    card {B. B \<subseteq> A & card(B) = k}"
+  apply (rule_tac f = "\<lambda>s. s - {x}" and g = "insert x" in card_bij_eq)
        apply (auto elim!: equalityE simp add: inj_on_def)
-  apply (subst Diff_insert0, auto)
+  apply (subst Diff_insert0)
+   apply auto
   done
 
 text {*
@@ -130,10 +131,12 @@
 *}
 
 lemma n_sub_lemma:
-    "!!A. finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
-  apply (induct k)
-   apply (simp add: card_s_0_eq_empty, atomize)
-  apply (rotate_tac -1, erule finite_induct)
+    "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)"
+  apply (induct k arbitrary: A)
+   apply (simp add: card_s_0_eq_empty)
+   apply atomize
+  apply (rotate_tac -1)
+  apply (erule finite_induct)
    apply (simp_all (no_asm_simp) cong add: conj_cong
      add: card_s_0_eq_empty choose_deconstruct)
   apply (subst card_Un_disjoint)
@@ -144,23 +147,23 @@
   apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
   done
 
-theorem n_subsets:
-    "finite A ==> card {B. B <= A & card B = k} = (card A choose k)"
+theorem n_subsets: "finite A \<Longrightarrow> card {B. B \<subseteq> A \<and> card B = k} = (card A choose k)"
   by (simp add: n_sub_lemma)
 
 
 text{* The binomial theorem (courtesy of Tobias Nipkow): *}
 
-theorem binomial: "(a+b::nat)^n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
+theorem binomial: "(a + b::nat)^n = (\<Sum>k=0..n. (n choose k) * a^k * b^(n - k))"
 proof (induct n)
-  case 0 thus ?case by simp
+  case 0
+  then show ?case by simp
 next
   case (Suc n)
   have decomp: "{0..n+1} = {0} \<union> {n+1} \<union> {1..n}"
     by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
   have decomp2: "{0..n} = {0} \<union> {1..n}"
     by (auto simp add:atLeastAtMost_def atLeast_def atMost_def)
-  have "(a+b::nat)^(n+1) = (a+b) * (\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
+  have "(a + b)^(n + 1) = (a + b) * (\<Sum>k=0..n. (n choose k) * a^k * b^(n - k))"
     using Suc by simp
   also have "\<dots> =  a*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k)) +
                    b*(\<Sum>k=0..n. (n choose k) * a^k * b^(n-k))"
@@ -186,55 +189,61 @@
 
 subsection{* Pochhammer's symbol : generalized raising factorial*}
 
-definition "pochhammer (a::'a::comm_semiring_1) n = (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
+definition "pochhammer (a::'a::comm_semiring_1) n =
+  (if n = 0 then 1 else setprod (\<lambda>n. a + of_nat n) {0 .. n - 1})"
 
-lemma pochhammer_0[simp]: "pochhammer a 0 = 1"
+lemma pochhammer_0 [simp]: "pochhammer a 0 = 1"
   by (simp add: pochhammer_def)
 
-lemma pochhammer_1[simp]: "pochhammer a 1 = a" by (simp add: pochhammer_def)
-lemma pochhammer_Suc0[simp]: "pochhammer a (Suc 0) = a"
+lemma pochhammer_1 [simp]: "pochhammer a 1 = a"
+  by (simp add: pochhammer_def)
+
+lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"
   by (simp add: pochhammer_def)
 
 lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"
   by (simp add: pochhammer_def)
 
 lemma setprod_nat_ivl_Suc: "setprod f {0 .. Suc n} = setprod f {0..n} * f (Suc n)"
-proof-
-  have eq: "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
-  show ?thesis unfolding eq by (simp add: field_simps)
+proof -
+  have "{0..Suc n} = {0..n} \<union> {Suc n}" by auto
+  then show ?thesis by (simp add: field_simps)
 qed
 
 lemma setprod_nat_ivl_1_Suc: "setprod f {0 .. Suc n} = f 0 * setprod f {1.. Suc n}"
-proof-
-  have eq: "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
-  show ?thesis unfolding eq by simp
+proof -
+  have "{0..Suc n} = {0} \<union> {1 .. Suc n}" by auto
+  then show ?thesis by simp
 qed
 
 
 lemma pochhammer_Suc: "pochhammer a (Suc n) = pochhammer a n * (a + of_nat n)"
-proof-
-  { assume "n=0" then have ?thesis by simp }
-  moreover
-  { fix m assume m: "n = Suc m"
-    have ?thesis unfolding m pochhammer_Suc_setprod setprod_nat_ivl_Suc .. }
-  ultimately show ?thesis by (cases n) auto
+proof (cases n)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc n)
+  show ?thesis unfolding Suc pochhammer_Suc_setprod setprod_nat_ivl_Suc ..
 qed
 
 lemma pochhammer_rec: "pochhammer a (Suc n) = a * pochhammer (a + 1) n"
-proof-
-  { assume "n=0" then have ?thesis by (simp add: pochhammer_Suc_setprod) }
-  moreover
-  { assume n0: "n \<noteq> 0"
-    have th0: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
-    have eq: "insert 0 {1 .. n} = {0..n}" by auto
-    have th1: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) =
-      (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
-      apply (rule setprod_reindex_cong [where f = Suc])
-      using n0 by (auto simp add: fun_eq_iff field_simps)
-    have ?thesis apply (simp add: pochhammer_def)
-    unfolding setprod_insert[OF th0, unfolded eq]
-    using th1 by (simp add: field_simps) }
-  ultimately show ?thesis by blast
+proof (cases "n = 0")
+  case True
+  then show ?thesis by (simp add: pochhammer_Suc_setprod)
+next
+  case False
+  have *: "finite {1 .. n}" "0 \<notin> {1 .. n}" by auto
+  have eq: "insert 0 {1 .. n} = {0..n}" by auto
+  have **: "(\<Prod>n\<in>{1\<Colon>nat..n}. a + of_nat n) = (\<Prod>n\<in>{0\<Colon>nat..n - 1}. a + 1 + of_nat n)"
+    apply (rule setprod_reindex_cong [where f = Suc])
+    using False
+    apply (auto simp add: fun_eq_iff field_simps)
+    done
+  show ?thesis
+    apply (simp add: pochhammer_def)
+    unfolding setprod_insert [OF *, unfolded eq]
+    using ** apply (simp add: field_simps)
+    done
 qed
 
 lemma pochhammer_fact: "of_nat (fact n) = pochhammer 1 n"
@@ -246,44 +255,46 @@
   done
 
 lemma pochhammer_of_nat_eq_0_lemma:
-  assumes kn: "k > n"
+  assumes "k > n"
   shows "pochhammer (- (of_nat n :: 'a:: idom)) k = 0"
-proof-
-  from kn obtain h where h: "k = Suc h" by (cases k) auto
-  { assume n0: "n=0" then have ?thesis using kn
-      by (cases k) (simp_all add: pochhammer_rec) }
-  moreover
-  { assume n0: "n \<noteq> 0"
-    then have ?thesis
-      apply (simp add: h pochhammer_Suc_setprod)
-      apply (rule_tac x="n" in bexI)
-      using h kn
-      apply auto
-      done }
-  ultimately show ?thesis by blast
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    using assms by (cases k) (simp_all add: pochhammer_rec)
+next
+  case False
+  from assms obtain h where "k = Suc h" by (cases k) auto
+  then show ?thesis
+    apply (simp add: pochhammer_Suc_setprod)
+    apply (rule_tac x="n" in bexI)
+    using assms
+    apply auto
+    done
 qed
 
-lemma pochhammer_of_nat_eq_0_lemma': assumes kn: "k \<le> n"
-  shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k \<noteq> 0"
-proof-
-  { assume "k=0" then have ?thesis by simp }
-  moreover
-  { fix h assume h: "k = Suc h"
-    then have ?thesis apply (simp add: pochhammer_Suc_setprod)
-      using h kn by (auto simp add: algebra_simps) }
-  ultimately show ?thesis by (cases k) auto
+lemma pochhammer_of_nat_eq_0_lemma':
+  assumes kn: "k \<le> n"
+  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k \<noteq> 0"
+proof (cases k)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc h)
+  then show ?thesis
+    apply (simp add: pochhammer_Suc_setprod)
+    using Suc kn apply (auto simp add: algebra_simps)
+    done
 qed
 
 lemma pochhammer_of_nat_eq_0_iff:
-  shows "pochhammer (- (of_nat n :: 'a:: {idom, ring_char_0})) k = 0 \<longleftrightarrow> k > n"
+  shows "pochhammer (- (of_nat n :: 'a:: {idom,ring_char_0})) k = 0 \<longleftrightarrow> k > n"
   (is "?l = ?r")
   using pochhammer_of_nat_eq_0_lemma[of n k, where ?'a='a]
     pochhammer_of_nat_eq_0_lemma'[of k n, where ?'a = 'a]
   by (auto simp add: not_le[symmetric])
 
 
-lemma pochhammer_eq_0_iff:
-  "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (EX k < n . a = - of_nat k) "
+lemma pochhammer_eq_0_iff: "pochhammer a n = (0::'a::field_char_0) \<longleftrightarrow> (\<exists>k < n. a = - of_nat k)"
   apply (auto simp add: pochhammer_of_nat_eq_0_iff)
   apply (cases n)
    apply (auto simp add: pochhammer_def algebra_simps group_add_class.eq_neg_iff_add_eq_0)
@@ -303,21 +314,22 @@
 lemma pochhammer_minus:
   assumes kn: "k \<le> n"
   shows "pochhammer (- b) k = ((- 1) ^ k :: 'a::comm_ring_1) * pochhammer (b - of_nat k + 1) k"
-proof-
-  { assume k0: "k = 0" then have ?thesis by simp }
-  moreover
-  { fix h assume h: "k = Suc h"
-    have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}"
-      using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
-      by auto
-    have ?thesis
-      unfolding h pochhammer_Suc_setprod eq setprod_timesf[symmetric]
-      apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
-      apply (auto simp add: inj_on_def image_def h )
-      apply (rule_tac x="h - x" in bexI)
-      apply (auto simp add: fun_eq_iff h of_nat_diff)
-      done }
-  ultimately show ?thesis by (cases k) auto
+proof (cases k)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc h)
+  have eq: "((- 1) ^ Suc h :: 'a) = setprod (%i. - 1) {0 .. h}"
+    using setprod_constant[where A="{0 .. h}" and y="- 1 :: 'a"]
+    by auto
+  show ?thesis
+    unfolding Suc pochhammer_Suc_setprod eq setprod_timesf[symmetric]
+    apply (rule strong_setprod_reindex_cong[where f = "%i. h - i"])
+    using Suc
+    apply (auto simp add: inj_on_def image_def)
+    apply (rule_tac x="h - x" in bexI)
+    apply (auto simp add: fun_eq_iff of_nat_diff)
+    done
 qed
 
 lemma pochhammer_minus':
@@ -326,20 +338,21 @@
   unfolding pochhammer_minus[OF kn, where b=b]
   unfolding mult_assoc[symmetric]
   unfolding power_add[symmetric]
-  apply simp
-  done
+  by simp
 
-lemma pochhammer_same: "pochhammer (- of_nat n) n = ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
+lemma pochhammer_same: "pochhammer (- of_nat n) n =
+    ((- 1) ^ n :: 'a::comm_ring_1) * of_nat (fact n)"
   unfolding pochhammer_minus[OF le_refl[of n]]
   by (simp add: of_nat_diff pochhammer_fact)
 
+
 subsection{* Generalized binomial coefficients *}
 
 definition gbinomial :: "'a::field_char_0 \<Rightarrow> nat \<Rightarrow> 'a" (infixl "gchoose" 65)
   where "a gchoose n =
     (if n = 0 then 1 else (setprod (\<lambda>i. a - of_nat i) {0 .. n - 1}) / of_nat (fact n))"
 
-lemma gbinomial_0[simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
+lemma gbinomial_0 [simp]: "a gchoose 0 = 1" "0 gchoose (Suc n) = 0"
   apply (simp_all add: gbinomial_def)
   apply (subgoal_tac "(\<Prod>i\<Colon>nat\<in>{0\<Colon>nat..n}. - of_nat i) = (0::'b)")
    apply (simp del:setprod_zero_iff)
@@ -347,17 +360,17 @@
   done
 
 lemma gbinomial_pochhammer: "a gchoose n = (- 1) ^ n * pochhammer (- a) n / of_nat (fact n)"
-proof -
-  { assume "n=0" then have ?thesis by simp }
-  moreover
-  { assume n0: "n\<noteq>0"
-    from n0 setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
-    have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
-      by auto
-    from n0 have ?thesis
-      by (simp add: pochhammer_def gbinomial_def field_simps
-        eq setprod_timesf[symmetric] del: minus_one) (* FIXME: del: minus_one *) }
-  ultimately show ?thesis by blast
+proof (cases "n = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  from this setprod_constant[of "{0 .. n - 1}" "- (1:: 'a)"]
+  have eq: "(- (1\<Colon>'a)) ^ n = setprod (\<lambda>i. - 1) {0 .. n - 1}"
+    by auto
+  from False show ?thesis
+    by (simp add: pochhammer_def gbinomial_def field_simps
+      eq setprod_timesf[symmetric] del: minus_one)
 qed
 
 lemma binomial_fact_lemma: "k \<le> n \<Longrightarrow> fact k * fact (n - k) * (n choose k) = fact n"
@@ -380,13 +393,14 @@
       by simp
     from n h th0
     have "fact k * fact (n - k) * (n choose k) =
-        k * (fact h * fact (m - h) * (m choose h)) +  (m - h) * (fact k * fact (m - k) * (m choose k))"
+        k * (fact h * fact (m - h) * (m choose h)) + 
+        (m - h) * (fact k * fact (m - k) * (m choose k))"
       by (simp add: field_simps)
     also have "\<dots> = (k + (m - h)) * fact m"
       using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
       by (simp add: field_simps)
     finally have ?ths using h n km by simp }
-  moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (EX m h. n=Suc m \<and> k = Suc h \<and> h < m)"
+  moreover have "n=0 \<or> k = 0 \<or> k = n \<or> (\<exists>m h. n = Suc m \<and> k = Suc h \<and> h < m)"
     using kn by presburger
   ultimately show ?ths by blast
 qed
@@ -410,7 +424,7 @@
     from k0 obtain h where h: "k = Suc h" by (cases k) auto
     from h
     have eq:"(- 1 :: 'a) ^ k = setprod (\<lambda>i. - 1) {0..h}"
-      by (subst setprod_constant, auto)
+      by (subst setprod_constant) auto
     have eq': "(\<Prod>i\<in>{0..h}. of_nat n + - (of_nat i :: 'a)) = (\<Prod>i\<in>{n - h..n}. of_nat i)"
       apply (rule strong_setprod_reindex_cong[where f="op - n"])
         using h kn
@@ -484,45 +498,42 @@
   "((a::'a::field_char_0) gchoose (Suc k)) * (of_nat (fact (Suc k)) :: 'a) =
     (setprod (\<lambda>i. a - of_nat i) {0 .. k})"
   using gbinomial_mult_fact[of k a]
-  apply (subst mult_commute)
-  apply assumption
-  done
+  by (subst mult_commute)
 
 
 lemma gbinomial_Suc_Suc:
   "((a::'a::field_char_0) + 1) gchoose (Suc k) = a gchoose k + (a gchoose (Suc k))"
-proof -
-  { assume "k = 0" then have ?thesis by simp }
-  moreover
-  { fix h assume h: "k = Suc h"
-    have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
-      apply (rule strong_setprod_reindex_cong[where f = Suc])
-        using h
-        apply auto
-      done
+proof (cases k)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc h)
+  have eq0: "(\<Prod>i\<in>{1..k}. (a + 1) - of_nat i) = (\<Prod>i\<in>{0..h}. a - of_nat i)"
+    apply (rule strong_setprod_reindex_cong[where f = Suc])
+      using Suc
+      apply auto
+    done
 
-    have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
-      ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
-      apply (simp add: h field_simps del: fact_Suc)
-      unfolding gbinomial_mult_fact'
-      apply (subst fact_Suc)
-      unfolding of_nat_mult
-      apply (subst mult_commute)
-      unfolding mult_assoc
-      unfolding gbinomial_mult_fact
-      apply (simp add: field_simps)
-      done
-    also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
-      unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
-      by (simp add: field_simps h)
-    also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
-      using eq0
-      by (simp add: h setprod_nat_ivl_1_Suc)
-    also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
-      unfolding gbinomial_mult_fact ..
-    finally have ?thesis by (simp del: fact_Suc)
-  }
-  ultimately show ?thesis by (cases k) auto
+  have "of_nat (fact (Suc k)) * (a gchoose k + (a gchoose (Suc k))) =
+    ((a gchoose Suc h) * of_nat (fact (Suc h)) * of_nat (Suc k)) + (\<Prod>i\<in>{0\<Colon>nat..Suc h}. a - of_nat i)"
+    apply (simp add: Suc field_simps del: fact_Suc)
+    unfolding gbinomial_mult_fact'
+    apply (subst fact_Suc)
+    unfolding of_nat_mult
+    apply (subst mult_commute)
+    unfolding mult_assoc
+    unfolding gbinomial_mult_fact
+    apply (simp add: field_simps)
+    done
+  also have "\<dots> = (\<Prod>i\<in>{0..h}. a - of_nat i) * (a + 1)"
+    unfolding gbinomial_mult_fact' setprod_nat_ivl_Suc
+    by (simp add: field_simps Suc)
+  also have "\<dots> = (\<Prod>i\<in>{0..k}. (a + 1) - of_nat i)"
+    using eq0
+    by (simp add: Suc setprod_nat_ivl_1_Suc)
+  also have "\<dots> = of_nat (fact (Suc k)) * ((a + 1) gchoose (Suc k))"
+    unfolding gbinomial_mult_fact ..
+  finally show ?thesis by (simp del: fact_Suc)
 qed
 
 
@@ -540,10 +551,12 @@
 (* Contributed by Manuel Eberl *)
 (* Alternative definition of the binomial coefficient as \<Prod>i<k. (n - i) / (k - i) *)
 lemma binomial_altdef_of_nat:
-  fixes n k :: nat and x :: "'a :: {field_char_0, field_inverse_zero}"
-  assumes "k \<le> n" shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
-proof cases
-  assume "0 < k"
+  fixes n k :: nat
+    and x :: "'a :: {field_char_0,field_inverse_zero}"
+  assumes "k \<le> n"
+  shows "of_nat (n choose k) = (\<Prod>i<k. of_nat (n - i) / of_nat (k - i) :: 'a)"
+proof (cases "0 < k")
+  case True
   then have "(of_nat (n choose k) :: 'a) = (\<Prod>i<k. of_nat n - of_nat i) / of_nat (fact k)"
     unfolding binomial_gbinomial gbinomial_def
     by (auto simp: gr0_conv_Suc lessThan_Suc_atMost atLeast0AtMost)
@@ -551,23 +564,30 @@
     using `k \<le> n` unfolding fact_eq_rev_setprod_nat of_nat_setprod
     by (auto simp add: setprod_dividef intro!: setprod_cong of_nat_diff[symmetric])
   finally show ?thesis .
-qed simp
+next
+  case False
+  then show ?thesis by simp
+qed
 
 lemma binomial_ge_n_over_k_pow_k:
-  fixes k n :: nat and x :: "'a :: linordered_field_inverse_zero"
-  assumes "0 < k" and "k \<le> n" shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
+  fixes k n :: nat
+    and x :: "'a :: linordered_field_inverse_zero"
+  assumes "0 < k"
+    and "k \<le> n"
+  shows "(of_nat n / of_nat k :: 'a) ^ k \<le> of_nat (n choose k)"
 proof -
   have "(of_nat n / of_nat k :: 'a) ^ k = (\<Prod>i<k. of_nat n / of_nat k :: 'a)"
     by (simp add: setprod_constant)
   also have "\<dots> \<le> of_nat (n choose k)"
     unfolding binomial_altdef_of_nat[OF `k\<le>n`]
   proof (safe intro!: setprod_mono)
-    fix i::nat  assume  "i < k"
+    fix i :: nat
+    assume  "i < k"
     from assms have "n * i \<ge> i * k" by simp
-    hence "n * k - n * i \<le> n * k - i * k" by arith
-    hence "n * (k - i) \<le> (n - i) * k"
+    then have "n * k - n * i \<le> n * k - i * k" by arith
+    then have "n * (k - i) \<le> (n - i) * k"
       by (simp add: diff_mult_distrib2 nat_mult_commute)
-    hence "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)"
+    then have "of_nat n * of_nat (k - i) \<le> of_nat (n - i) * (of_nat k :: 'a)"
       unfolding of_nat_mult[symmetric] of_nat_le_iff .
     with assms show "of_nat n / of_nat k \<le> of_nat (n - i) / (of_nat (k - i) :: 'a)"
       using `i < k` by (simp add: field_simps)
@@ -576,15 +596,16 @@
 qed
 
 lemma binomial_le_pow:
-  assumes "r \<le> n" shows "n choose r \<le> n ^ r"
+  assumes "r \<le> n"
+  shows "n choose r \<le> n ^ r"
 proof -
   have "n choose r \<le> fact n div fact (n - r)"
     using `r \<le> n` by (subst binomial_fact_lemma[symmetric]) auto
-  with fact_div_fact_le_pow[OF assms] show ?thesis by auto
+  with fact_div_fact_le_pow [OF assms] show ?thesis by auto
 qed
 
 lemma binomial_altdef_nat: "(k::nat) \<le> n \<Longrightarrow>
     n choose k = fact n div (fact k * fact (n - k))"
- by (subst binomial_fact_lemma[symmetric]) auto
+ by (subst binomial_fact_lemma [symmetric]) auto
 
 end
diff -r 7196e1ce1cd8 -r 6c89225ddeba src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 07 21:16:20 2013 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Aug 07 23:20:11 2013 +0200
@@ -159,7 +159,8 @@
 qed
 
 lemma fps_mult_commute_lemma:
-  fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
+  fixes n :: nat
+    and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>i=0..n. f i (n - i)) = (\<Sum>i=0..n. f (n - i) i)"
 proof (rule setsum_reindex_cong)
   show "inj_on (\<lambda>i. n - i) {0..n}"
@@ -949,8 +950,10 @@
   fixes f:: "('a::{idom,semiring_char_0}) fps"
   shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)"
 proof -
-  have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0" by simp
-  also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)" unfolding fps_deriv_eq_0_iff ..
+  have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0"
+    by simp
+  also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f-g)$0)"
+    unfolding fps_deriv_eq_0_iff ..
   finally show ?thesis by (simp add: field_simps)
 qed
 
@@ -1007,17 +1010,12 @@
 
 lemma fps_nth_deriv_setsum:
   "fps_nth_deriv n (setsum f S) = setsum (\<lambda>i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S"
-proof -
-  {
-    assume "\<not> finite S"
-    then have ?thesis by simp
-  }
-  moreover
-  {
-    assume fS: "finite S"
-    have ?thesis by (induct rule: finite_induct[OF fS]) simp_all
-  }
-  ultimately show ?thesis by blast
+proof (cases "finite S")
+  case True
+  show ?thesis by (induct rule: finite_induct [OF True]) simp_all
+next
+  case False
+  then show ?thesis by simp
 qed
 
 lemma fps_deriv_maclauren_0:
@@ -1185,8 +1183,9 @@
   have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0"
     unfolding power2_eq_square
     apply (simp add: field_simps)
-    by (simp add: mult_assoc[symmetric])
-  hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
+    apply (simp add: mult_assoc[symmetric])
+    done
+  then have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
       0 - fps_deriv a * inverse a ^ 2"
     by simp
   then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2"
@@ -1196,7 +1195,7 @@
 lemma fps_inverse_mult:
   fixes a::"('a :: field) fps"
   shows "inverse (a * b) = inverse a * inverse b"
-proof-
+proof -
   {
     assume a0: "a$0 = 0" hence ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth)
     from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all
@@ -1262,9 +1261,8 @@
 
 subsection{* Integration *}
 
-definition
-  fps_integral :: "'a::field_char_0 fps \<Rightarrow> 'a \<Rightarrow> 'a fps" where
-  "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
+definition fps_integral :: "'a::field_char_0 fps \<Rightarrow> 'a \<Rightarrow> 'a fps"
+  where "fps_integral a a0 = Abs_fps (\<lambda>n. if n = 0 then a0 else (a$(n - 1) / of_nat n))"
 
 lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a"
   unfolding fps_integral_def fps_deriv_def
@@ -1537,7 +1535,7 @@
 lemma natpermute_contain_maximal:
   "{xs \<in> natpermute n (k+1). n \<in> set xs} = UNION {0 .. k} (\<lambda>i. {(replicate (k+1) 0) [i:=n]})"
   (is "?A = ?B")
-proof-
+proof -
   {
     fix xs
     assume H: "xs \<in> natpermute n (k+1)" and n: "n \<in> set xs"
@@ -1653,7 +1651,8 @@
 
 text{* The special form for powers *}
 lemma fps_power_nth_Suc:
-  fixes m :: nat and a :: "('a::comm_ring_1) fps"
+  fixes m :: nat
+    and a :: "('a::comm_ring_1) fps"
   shows "(a ^ Suc m)$n = setsum (\<lambda>v. setprod (\<lambda>j. a $ (v!j)) {0..m}) (natpermute n (m+1))"
 proof -
   have th0: "a^Suc m = setprod (\<lambda>i. a) {0..m}" by (simp add: setprod_constant)
@@ -1735,7 +1734,8 @@
 
 subsection {* Radicals *}
 
-declare setprod_cong[fundef_cong]
+declare setprod_cong [fundef_cong]
+
 function radical :: "(nat \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> ('a::{field}) fps \<Rightarrow> nat \<Rightarrow> 'a"
 where
   "radical r 0 a 0 = 1"
@@ -1860,15 +1860,23 @@
   shows "(r (Suc k) (a$0)) ^ Suc k = a$0 \<longleftrightarrow> (fps_radical r (Suc k) a) ^ (Suc k) = a"
 proof-
   let ?r = "fps_radical r (Suc k) a"
-  {assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
+  {
+    assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
     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" hence "?r ^ Suc k $ n = a $n"
-            using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp}
+    {
+      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"
+          hence "?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"
+        {
+          fix n1 assume n1: "n = Suc n1"
           have nz: "n \<noteq> 0" using n1 by arith
           let ?Pnk = "natpermute n (k + 1)"
           let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}"
@@ -1880,37 +1888,45 @@
             by (metis natpermute_finite)+
           let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j"
           have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn"
-          proof(rule setsum_cong2)
+          proof (rule setsum_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 setprod_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"
-            using i r0 by (simp add: setprod_gen_delta)
-          finally show ?ths .
-        qed
-        then have "setsum ?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 - setsum ?f ?Pnknn"
-          unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc)
-        finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
-        have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
-          unfolding fps_power_nth_Suc setsum_Un_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 have ?thesis using r0 by (simp add: fps_eq_iff)}
-moreover
-{ assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a"
-  hence "((fps_radical r (Suc k) a) ^ (Suc k))$0 = a$0" by simp
-  then have "(r (Suc k) (a$0)) ^ Suc k = a$0"
-    unfolding fps_power_nth_Suc
-    by (simp add: setprod_constant del: replicate.simps)}
-ultimately show ?thesis by blast
+            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 setprod_cong, simp)
+              using i r0 apply (simp del: replicate.simps)
+              done
+            also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k"
+              using i r0 by (simp add: setprod_gen_delta)
+            finally show ?ths .
+          qed
+          then have "setsum ?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 - setsum ?f ?Pnknn"
+            unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc)
+          finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" .
+          have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn"
+            unfolding fps_power_nth_Suc setsum_Un_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 have ?thesis using r0 by (simp add: fps_eq_iff)
+  }
+  moreover
+  {
+    assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a"
+    hence "((fps_radical r (Suc k) a) ^ (Suc k))$0 = a$0" by simp
+    then have "(r (Suc k) (a$0)) ^ Suc k = a$0"
+      unfolding fps_power_nth_Suc
+      by (simp add: setprod_constant del: replicate.simps)
+  }
+  ultimately show ?thesis by blast
 qed
 
 (*
@@ -1967,33 +1983,51 @@
 qed
 
 *)
-lemma eq_divide_imp': assumes c0: "(c::'a::field) ~= 0" and eq: "a * c = b"
+lemma eq_divide_imp':
+  assumes c0: "(c::'a::field) ~= 0"
+    and eq: "a * c = b"
   shows "a = b / c"
-proof-
-  from eq have "a * c * inverse c = b * inverse c" by simp
-  hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse)
-  then show "a = b/c" unfolding  field_inverse[OF c0] by simp
+proof -
+  from eq have "a * c * inverse c = b * inverse c"
+    by simp
+  hence "a * (inverse c * c) = b/c"
+    by (simp only: field_simps divide_inverse)
+  then show "a = b/c"
+    unfolding  field_inverse[OF c0] by simp
 qed
 
 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" and b0: "b$0 \<noteq> 0"
+    and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0"
+    and b0: "b$0 \<noteq> 0"
   shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b"
 proof-
   let ?r = "fps_radical r (Suc k) b"
   have r00: "r (Suc k) (b$0) \<noteq> 0" using b0 r0 by auto
-  {assume H: "a = ?r"
-    from H have "a^Suc k = b" using power_radical[OF b0, of r k, unfolded r0] by simp}
+  {
+    assume H: "a = ?r"
+    from H have "a^Suc k = b"
+      using power_radical[OF b0, of r k, unfolded r0] by simp
+  }
   moreover
-  {assume H: "a^Suc k = b"
+  {
+    assume H: "a^Suc k = b"
     have ceq: "card {0..k} = Suc k" by simp
     from a0 have a0r0: "a$0 = ?r$0" by simp
-    {fix n have "a $ n = ?r $ n"
-      proof(induct n rule: nat_less_induct)
-        fix n assume h: "\<forall>m<n. a$m = ?r $m"
-        {assume "n = 0" hence "a$n = ?r $n" using a0 by simp }
+    {
+      fix n
+      have "a $ n = ?r $ n"
+      proof (induct n rule: nat_less_induct)
+        fix n
+        assume h: "\<forall>m<n. a$m = ?r $m"
+        {
+          assume "n = 0"
+          hence "a$n = ?r $n" using a0 by simp
+        }
         moreover
-        {fix n1 assume n1: "n = Suc n1"
+        {
+          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 (Suc k)"
@@ -2007,14 +2041,17 @@
         let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j"
         let ?g = "\<lambda>v. \<Prod>j\<in>{0..k}. a $ v ! j"
         have "setsum ?g ?Pnkn = setsum (\<lambda>v. a $ n * (?r$0)^k) ?Pnkn"
-        proof(rule setsum_cong2)
-          fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
+        proof (rule setsum_cong2)
+          fix v
+          assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
           let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k"
           from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
-            unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
+            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 setprod_cong, simp)
-            using i a0 by (simp del: replicate.simps)
+            using i a0 apply (simp del: replicate.simps)
+            done
           also have "\<dots> = a $ n * (?r $ 0)^k"
             using i by (simp add: setprod_gen_delta)
           finally show ?ths .
@@ -2023,46 +2060,60 @@
           by (simp add: natpermute_max_card[OF nz, simplified])
         have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn"
         proof (rule setsum_cong2, rule setprod_cong, simp)
-          fix xs i assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}"
-          {assume c: "n \<le> xs ! i"
-            from xs i have "xs !i \<noteq> n" by (auto simp add: in_set_conv_nth natpermute_def)
+          fix xs i
+          assume xs: "xs \<in> ?Pnknn" and i: "i \<in> {0..k}"
+          {
+            assume c: "n \<le> xs ! i"
+            from xs i have "xs !i \<noteq> n"
+              by (auto simp add: in_set_conv_nth natpermute_def)
             with c have c': "n < xs!i" by arith
-            have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}" by simp_all
-            have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}" by auto
-            have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})" using i by auto
-            from xs have "n = listsum xs" by (simp add: natpermute_def)
-            also have "\<dots> = setsum (nth xs) {0..<Suc k}" using xs
-              by (simp add: natpermute_def listsum_setsum_nth)
+            have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1..<Suc k}"
+              by simp_all
+            have d: "{0 ..< i} \<inter> ({i} \<union> {i+1 ..< Suc k}) = {}" "{i} \<inter> {i+1..< Suc k} = {}"
+              by auto
+            have eqs: "{0..<Suc k} = {0 ..< i} \<union> ({i} \<union> {i+1 ..< Suc k})"
+              using i by auto
+            from xs have "n = listsum xs"
+              by (simp add: natpermute_def)
+            also have "\<dots> = setsum (nth xs) {0..<Suc k}"
+              using xs by (simp add: natpermute_def listsum_setsum_nth)
             also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}"
               unfolding eqs  setsum_Un_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
               unfolding setsum_Un_disjoint[OF fths(2) fths(3) d(2)]
               by simp
-            finally have False using c' by simp}
+            finally have False using c' by simp
+          }
           then have thn: "xs!i < n" by presburger
-          from h[rule_format, OF thn]
-          show "a$(xs !i) = ?r$(xs!i)" .
+          from h[rule_format, OF thn] show "a$(xs !i) = ?r$(xs!i)" .
         qed
         have th00: "\<And>(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x"
           by (simp add: field_simps del: of_nat_Suc)
-        from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
+        from H have "b$n = a^Suc k $ n"
+          by (simp add: fps_eq_iff)
         also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
           unfolding fps_power_nth_Suc
           using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric],
             unfolded eq, of ?g] by simp
-        also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 ..
-        finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp
+        also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn"
+          unfolding th0 th1 ..
+        finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn"
+          by simp
         then have "a$n = (b$n - setsum ?f ?Pnknn) / (of_nat (k+1) * (?r $ 0)^k)"
           apply -
           apply (rule eq_divide_imp')
           using r00
           apply (simp del: of_nat_Suc)
-          by (simp add: mult_ac)
+          apply (simp add: mult_ac)
+          done
         then have "a$n = ?r $n"
           apply (simp del: of_nat_Suc)
           unfolding fps_radical_def n1
-          by (simp add: field_simps n1 th00 del: of_nat_Suc)}
-        ultimately show "a$n = ?r $ n" by (cases n, auto)
-      qed}
+          apply (simp add: field_simps n1 th00 del: of_nat_Suc)
+          done
+        }
+        ultimately show "a$n = ?r $ n" by (cases n) auto
+      qed
+    }
     then have "a = ?r" by (simp add: fps_eq_iff)
   }
   ultimately show ?thesis by blast
@@ -2071,33 +2122,43 @@
 
 lemma radical_power:
   assumes r0: "r (Suc k) ((a$0) ^ Suc k) = a$0"
-  and a0: "(a$0 ::'a::field_char_0) \<noteq> 0"
+    and a0: "(a$0 ::'a::field_char_0) \<noteq> 0"
   shows "(fps_radical r (Suc k) (a ^ Suc k)) = a"
-proof-
+proof -
   let ?ak = "a^ Suc k"
-  have ak0: "?ak $ 0 = (a$0) ^ Suc k" by (simp add: fps_nth_power_0 del: power_Suc)
-  from r0 have th0: "r (Suc k) (a ^ Suc k $ 0) ^ Suc k = a ^ Suc k $ 0" using ak0 by auto
-  from r0 ak0 have th1: "r (Suc k) (a ^ Suc k $ 0) = a $ 0" by auto
-  from ak0 a0 have ak00: "?ak $ 0 \<noteq>0 " by auto
-  from radical_unique[of r k ?ak a, OF th0 th1 ak00] show ?thesis by metis
+  have ak0: "?ak $ 0 = (a$0) ^ Suc k"
+    by (simp add: fps_nth_power_0 del: power_Suc)
+  from r0 have th0: "r (Suc k) (a ^ Suc k $ 0) ^ Suc k = a ^ Suc k $ 0"
+    using ak0 by auto
+  from r0 ak0 have th1: "r (Suc k) (a ^ Suc k $ 0) = a $ 0"
+    by auto
+  from ak0 a0 have ak00: "?ak $ 0 \<noteq>0 "
+    by auto
+  from radical_unique[of r k ?ak a, OF th0 th1 ak00] show ?thesis
+    by metis
 qed
 
 lemma fps_deriv_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"
+  assumes r0: "(r (Suc k) (a$0)) ^ Suc k = a$0"
+    and a0: "a$0 \<noteq> 0"
   shows "fps_deriv (fps_radical r (Suc k) a) = fps_deriv a / (fps_const (of_nat (Suc k)) * (fps_radical r (Suc k) a) ^ k)"
-proof-
-  let ?r= "fps_radical r (Suc k) a"
+proof -
+  let ?r = "fps_radical r (Suc k) a"
   let ?w = "(fps_const (of_nat (Suc k)) * ?r ^ k)"
-  from a0 r0 have r0': "r (Suc k) (a$0) \<noteq> 0" by auto
-  from r0' have w0: "?w $ 0 \<noteq> 0" by (simp del: of_nat_Suc)
+  from a0 r0 have r0': "r (Suc k) (a$0) \<noteq> 0"
+    by auto
+  from r0' have w0: "?w $ 0 \<noteq> 0"
+    by (simp del: of_nat_Suc)
   note th0 = inverse_mult_eq_1[OF w0]
   let ?iw = "inverse ?w"
   from iffD1[OF power_radical[of a r], OF a0 r0]
-  have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp
+  have "fps_deriv (?r ^ Suc k) = fps_deriv a"
+    by simp
   hence "fps_deriv ?r * ?w = fps_deriv a"
     by (simp add: fps_deriv_power mult_ac del: power_Suc)
-  hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a" by simp
+  hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a"
+    by simp
   hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w"
     by (simp add: fps_divide_def)
   then show ?thesis unfolding th0 by simp
@@ -2112,28 +2173,39 @@
     and b0: "b$0 \<noteq> 0"
   shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow>
     fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)"
-proof-
-  {assume  r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
-  from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0"
-    by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
-  {assume "k=0" hence ?thesis using r0' by simp}
+proof -
+  {
+    assume  r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
+    from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0"
+      by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
+    {
+      assume "k = 0"
+      hence ?thesis using r0' by simp
+    }
+    moreover
+    {
+      fix h assume k: "k = Suc h"
+      let ?ra = "fps_radical r (Suc h) a"
+      let ?rb = "fps_radical r (Suc h) b"
+      have th0: "r (Suc h) ((a * b) $ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) $ 0"
+        using r0' k by (simp add: fps_mult_nth)
+      have ab0: "(a*b) $ 0 \<noteq> 0"
+        using a0 b0 by (simp add: fps_mult_nth)
+      from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric]
+        iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded k]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded k]] k r0'
+      have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)
+    }
+    ultimately have ?thesis by (cases k) auto
+  }
   moreover
-  {fix h assume k: "k = Suc h"
-  let ?ra = "fps_radical r (Suc h) a"
-  let ?rb = "fps_radical r (Suc h) b"
-  have th0: "r (Suc h) ((a * b) $ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) $ 0"
-    using r0' k by (simp add: fps_mult_nth)
-  have ab0: "(a*b) $ 0 \<noteq> 0" using a0 b0 by (simp add: fps_mult_nth)
-  from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric]
-    iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded k]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded k]] k r0'
-  have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)}
-ultimately have ?thesis by (cases k, auto)}
-moreover
-{assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b"
-  hence "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0" by simp
-  then have "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
-    using k by (simp add: fps_mult_nth)}
-ultimately show ?thesis by blast
+  {
+    assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b"
+    hence "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0"
+      by simp
+    then have "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)"
+      using k by (simp add: fps_mult_nth)
+  }
+  ultimately show ?thesis by blast
 qed
 
 (*
@@ -2169,16 +2241,17 @@
 
 lemma radical_divide:
   fixes a :: "'a::field_char_0 fps"
-  assumes
-  kp: "k>0"
-  and ra0: "(r k (a $ 0)) ^ k = a $ 0"
-  and rb0: "(r k (b $ 0)) ^ k = b $ 0"
-  and a0: "a$0 \<noteq> 0"
-  and b0: "b$0 \<noteq> 0"
-  shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \<longleftrightarrow> fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" (is "?lhs = ?rhs")
-proof-
+  assumes kp: "k > 0"
+    and ra0: "(r k (a $ 0)) ^ k = a $ 0"
+    and rb0: "(r k (b $ 0)) ^ k = b $ 0"
+    and a0: "a$0 \<noteq> 0"
+    and b0: "b$0 \<noteq> 0"
+  shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \<longleftrightarrow>
+    fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b"
+  (is "?lhs = ?rhs")
+proof -
   let ?r = "fps_radical r k"
-  from kp obtain h where k: "k = Suc h" by (cases k, auto)
+  from kp obtain h where k: "k = Suc h" by (cases k) auto
   have ra0': "r k (a$0) \<noteq> 0" using a0 ra0 k by auto
   have rb0': "r k (b$0) \<noteq> 0" using b0 rb0 k by auto
 
@@ -2212,11 +2285,10 @@
 
 lemma radical_inverse:
   fixes a :: "'a::field_char_0 fps"
-  assumes
-  k: "k>0"
-  and ra0: "r k (a $ 0) ^ k = a $ 0"
-  and r1: "(r k 1)^k = 1"
-  and a0: "a$0 \<noteq> 0"
+  assumes k: "k > 0"
+    and ra0: "r k (a $ 0) ^ k = a $ 0"
+    and r1: "(r k 1)^k = 1"
+    and a0: "a$0 \<noteq> 0"
   shows "r k (inverse (a $ 0)) = r k 1 / (r k (a $ 0)) \<longleftrightarrow> fps_radical r k (inverse a) = fps_radical r k 1 / fps_radical r k a"
   using radical_divide[where k=k and r=r and a=1 and b=a, OF k ] ra0 r1 a0
   by (simp add: divide_inverse fps_divide_def)
@@ -2227,72 +2299,80 @@
   fixes a:: "('a::idom) fps"
   assumes b0: "b$0 = 0"
   shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * (fps_deriv b)"
-proof-
-  {fix n
+proof -
+  {
+    fix n
     have "(fps_deriv (a oo b))$n = setsum (\<lambda>i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}"
       by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc)
     also have "\<dots> = setsum (\<lambda>i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}"
       by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc)
-  also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}"
-    unfolding fps_mult_left_const_nth  by (simp add: field_simps)
-  also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}"
-    unfolding fps_mult_nth ..
-  also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}"
-    apply (rule setsum_mono_zero_right)
-    apply (auto simp add: mult_delta_left setsum_delta not_le)
-    done
-  also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
-    unfolding fps_deriv_nth
-    apply (rule setsum_reindex_cong [where f = Suc])
-    by (auto simp add: mult_assoc)
-  finally have th0: "(fps_deriv (a oo b))$n = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
-
-  have "(((fps_deriv a) oo b) * (fps_deriv b))$n = setsum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}"
-    unfolding fps_mult_nth by (simp add: mult_ac)
-  also have "\<dots> = setsum (\<lambda>i. setsum (\<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 setsum_right_distrib mult_assoc
-    apply (rule setsum_cong2)
-    apply (rule setsum_mono_zero_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])
-    by simp
-  also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
-    unfolding setsum_right_distrib
-    apply (subst setsum_commute)
-    by ((rule setsum_cong2)+) simp
-  finally have "(fps_deriv (a oo b))$n = (((fps_deriv a) oo b) * (fps_deriv b)) $n"
-    unfolding th0 by simp}
-then show ?thesis by (simp add: fps_eq_iff)
+    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}"
+      unfolding fps_mult_left_const_nth  by (simp add: field_simps)
+    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {0.. Suc n}"
+      unfolding fps_mult_nth ..
+    also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (setsum (\<lambda>j. (b^ (i - 1))$j * (fps_deriv b)$(n - j)) {0..n})) {1.. Suc n}"
+      apply (rule setsum_mono_zero_right)
+      apply (auto simp add: mult_delta_left setsum_delta not_le)
+      done
+    also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
+      unfolding fps_deriv_nth
+      apply (rule setsum_reindex_cong [where f = Suc])
+      by (auto simp add: mult_assoc)
+    finally have th0: "(fps_deriv (a oo b))$n =
+      setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}" .
+
+    have "(((fps_deriv a) oo b) * (fps_deriv b))$n = setsum (\<lambda>i. (fps_deriv b)$ (n - i) * ((fps_deriv a) oo b)$i) {0..n}"
+      unfolding fps_mult_nth by (simp add: mult_ac)
+    also have "\<dots> = setsum (\<lambda>i. setsum (\<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 setsum_right_distrib mult_assoc
+      apply (rule setsum_cong2)
+      apply (rule setsum_mono_zero_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
+    also have "\<dots> = setsum (\<lambda>i. of_nat (i + 1) * a$(i+1) * (setsum (\<lambda>j. (b^ i)$j * of_nat (n - j + 1) * b$(n - j + 1)) {0..n})) {0.. n}"
+      unfolding setsum_right_distrib
+      apply (subst setsum_commute)
+      apply (rule setsum_cong2)+
+      apply simp
+      done
+    finally have "(fps_deriv (a oo b))$n = (((fps_deriv a) oo b) * (fps_deriv b)) $n"
+      unfolding th0 by simp
+  }
+  then show ?thesis by (simp add: fps_eq_iff)
 qed
 
 lemma fps_mult_X_plus_1_nth:
   "((1+X)*a) $n = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
-proof-
-  {assume "n = 0" hence ?thesis by (simp add: fps_mult_nth )}
-  moreover
-  {fix m assume m: "n = Suc m"
-    have "((1+X)*a) $n = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0..n}"
-      by (simp add: fps_mult_nth)
-    also have "\<dots> = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0.. 1}"
-      unfolding m
-      apply (rule setsum_mono_zero_right)
-      by (auto simp add: )
-    also have "\<dots> = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
-      unfolding m
-      by (simp add: )
-    finally have ?thesis .}
-  ultimately show ?thesis by (cases n, auto)
+proof (cases n)
+  case 0
+  then show ?thesis by (simp add: fps_mult_nth )
+next
+  case (Suc m)
+  have "((1+X)*a) $n = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0..n}"
+    by (simp add: fps_mult_nth)
+  also have "\<dots> = setsum (\<lambda>i. (1+X)$i * a$(n-i)) {0.. 1}"
+    unfolding Suc
+    apply (rule setsum_mono_zero_right)
+    apply auto
+    done
+  also have "\<dots> = (if n = 0 then (a$n :: 'a::comm_ring_1) else a$n + a$(n - 1))"
+    by (simp add: Suc)
+  finally show ?thesis .
 qed
 
 subsection{* Finite FPS (i.e. polynomials) and X *}
+
 lemma fps_poly_sum_X:
   assumes z: "\<forall>i > n. a$i = (0::'a::comm_ring_1)"
   shows "a = setsum (\<lambda>i. fps_const (a$i) * X^i) {0..n}" (is "a = ?r")
-proof-
-  {fix i
+proof -
+  {
+    fix i
     have "a$i = ?r$i"
       unfolding fps_setsum_nth fps_mult_left_const_nth X_power_nth
       by (simp add: mult_delta_right setsum_delta' z)
@@ -2300,67 +2380,87 @@
   then show ?thesis unfolding fps_eq_iff by blast
 qed
 
+
 subsection{* Compositional inverses *}
 
-
-fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
+fun compinv :: "'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+where
   "compinv a 0 = X$0"
-| "compinv a (Suc n) = (X$ Suc n - setsum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
+| "compinv a (Suc n) =
+    (X$ Suc n - setsum (\<lambda>i. (compinv a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
 
 definition "fps_inv a = Abs_fps (compinv a)"
 
-lemma fps_inv: assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+lemma fps_inv:
+  assumes a0: "a$0 = 0"
+    and a1: "a$1 \<noteq> 0"
   shows "fps_inv a oo a = X"
-proof-
+proof -
   let ?i = "fps_inv a oo a"
-  {fix n
+  {
+    fix n
     have "?i $n = X$n"
-    proof(induct n rule: nat_less_induct)
-      fix n assume h: "\<forall>m<n. ?i$m = X$m"
-      {assume "n=0" hence "?i $n = X$n" using a0
-          by (simp add: fps_compose_nth fps_inv_def)}
-      moreover
-      {fix n1 assume n1: "n = Suc n1"
+    proof (induct n rule: nat_less_induct)
+      fix n
+      assume h: "\<forall>m<n. ?i$m = X$m"
+      show "?i $ n = X$n"
+      proof (cases n)
+        case 0
+        then show ?thesis using a0
+          by (simp add: fps_compose_nth fps_inv_def)
+      next
+        case (Suc n1)
         have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1"
-          by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
-                   del: power_Suc)
-        also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
-          using a0 a1 n1 by (simp add: fps_inv_def)
-        also have "\<dots> = X$n" using n1 by simp
-        finally have "?i $ n = X$n" .}
-      ultimately show "?i $ n = X$n" by (cases n, auto)
-    qed}
+          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+        also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} +
+          (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})"
+          using a0 a1 Suc by (simp add: fps_inv_def)
+        also have "\<dots> = X$n" using Suc by simp
+        finally show ?thesis .
+      qed
+    qed
+  }
   then show ?thesis by (simp add: fps_eq_iff)
 qed
 
 
-fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}" where
+fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::{field}"
+where
   "gcompinv b a 0 = b$0"
-| "gcompinv b a (Suc n) = (b$ Suc n - setsum (\<lambda>i. (gcompinv b a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
+| "gcompinv b a (Suc n) =
+    (b$ Suc n - setsum (\<lambda>i. (gcompinv b a i) * (a^i)$Suc n) {0 .. n}) / (a$1) ^ Suc n"
 
 definition "fps_ginv b a = Abs_fps (gcompinv b a)"
 
-lemma fps_ginv: assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+lemma fps_ginv:
+  assumes a0: "a$0 = 0"
+    and a1: "a$1 \<noteq> 0"
   shows "fps_ginv b a oo a = b"
-proof-
+proof -
   let ?i = "fps_ginv b a oo a"
-  {fix n
+  {
+    fix n
     have "?i $n = b$n"
-    proof(induct n rule: nat_less_induct)
-      fix n assume h: "\<forall>m<n. ?i$m = b$m"
-      {assume "n=0" hence "?i $n = b$n" using a0
-          by (simp add: fps_compose_nth fps_ginv_def)}
-      moreover
-      {fix n1 assume n1: "n = Suc n1"
+    proof (induct n rule: nat_less_induct)
+      fix n
+      assume h: "\<forall>m<n. ?i$m = b$m"
+      show "?i $ n = b$n"
+      proof (cases n)
+        case 0
+        then show ?thesis using a0
+          by (simp add: fps_compose_nth fps_ginv_def)
+      next
+        case (Suc n1)
         have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1"
-          by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0]
-                   del: power_Suc)
-        also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
-          using a0 a1 n1 by (simp add: fps_ginv_def)
-        also have "\<dots> = b$n" using n1 by simp
-        finally have "?i $ n = b$n" .}
-      ultimately show "?i $ n = b$n" by (cases n, auto)
-    qed}
+          by (simp add: fps_compose_nth Suc startsby_zero_power_nth_same[OF a0] del: power_Suc)
+        also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} +
+          (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})"
+          using a0 a1 Suc by (simp add: fps_ginv_def)
+        also have "\<dots> = b$n" using Suc by simp
+        finally show ?thesis .
+      qed
+    qed
+  }
   then show ?thesis by (simp add: fps_eq_iff)
 qed
 
@@ -2386,19 +2486,22 @@
   by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_addf)
 
 lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\<lambda>i. f i oo a) S"
-proof-
-  {assume "\<not> finite S" hence ?thesis by simp}
-  moreover
-  {assume fS: "finite S"
-    have ?thesis
-    proof(rule finite_induct[OF fS])
-      show "setsum f {} oo a = (\<Sum>i\<in>{}. f i oo a)" by simp
-    next
-      fix x F assume fF: "finite F" and xF: "x \<notin> F" and h: "setsum f F oo a = setsum (\<lambda>i. f i oo a) F"
-      show "setsum f (insert x F) oo a  = setsum (\<lambda>i. f i oo a) (insert x F)"
-        using fF xF h by (simp add: fps_compose_add_distrib)
-    qed}
-  ultimately show ?thesis by blast
+proof (cases "finite S")
+  case True
+  show ?thesis
+  proof (rule finite_induct[OF True])
+    show "setsum f {} oo a = (\<Sum>i\<in>{}. f i oo a)" by simp
+  next
+    fix x F
+    assume fF: "finite F"
+      and xF: "x \<notin> F"
+      and h: "setsum f F oo a = setsum (\<lambda>i. f i oo a) F"
+    show "setsum f (insert x F) oo a  = setsum (\<lambda>i. f i oo a) (insert x F)"
+      using fF xF h by (simp add: fps_compose_add_distrib)
+  qed
+next
+  case False
+  then show ?thesis by simp
 qed
 
 lemma convolution_eq:
@@ -2413,19 +2516,23 @@
   done
 
 lemma product_composition_lemma:
-  assumes c0: "c$0 = (0::'a::idom)" and d0: "d$0 = 0"
-  shows "((a oo c) * (b oo d))$n = setsum (%(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r")
-proof-
+  assumes c0: "c$0 = (0::'a::idom)"
+    and d0: "d$0 = 0"
+  shows "((a oo c) * (b oo d))$n =
+    setsum (%(k,m). a$k * b$m * (c^k * d^m) $ n) {(k,m). k + m \<le> n}" (is "?l = ?r")
+proof -
   let ?S = "{(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
   have s: "?S \<subseteq> {0..n} <*> {0..n}" by (auto simp add: subset_eq)
   have f: "finite {(k\<Colon>nat, m\<Colon>nat). k + m \<le> n}"
     apply (rule finite_subset[OF s])
-    by auto
+    apply auto
+    done
   have "?r =  setsum (%i. setsum (%(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 setsum_right_distrib)
     apply (subst setsum_commute)
     apply (rule setsum_cong2)
-    by (auto simp add: field_simps)
+    apply (auto simp add: field_simps)
+    done
   also have "\<dots> = ?l"
     apply (simp add: fps_mult_nth fps_compose_nth setsum_product)
     apply (rule setsum_cong2)
@@ -2447,8 +2554,10 @@
 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 = setsum (%k. setsum (%m. a$k * b$m * (c^k * d^m) $ n) {0..n}) {0..n}" (is "?l = ?r")
+  assumes c0: "c$0 = (0::'a::idom)"
+    and d0: "d$0 = 0"
+  shows "((a oo c) * (b oo d))$n =
+    setsum (%k. setsum (%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 setsum_cartesian_product
   apply (rule setsum_mono_zero_left)
@@ -2472,9 +2581,11 @@
 
 
 lemma setsum_pair_less_iff:
-  "setsum (%((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} = setsum (%s. setsum (%i. a i * b (s - i) * c s) {0..s}) {0..n}" (is "?l = ?r")
-proof-
-  let ?KM=  "{(k,m). k + m \<le> n}"
+  "setsum (%((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \<le> n} =
+    setsum (%s. setsum (%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 = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})"
   have th0: "?KM = UNION {0..n} ?f"
     apply (simp add: set_eq_iff)
@@ -2491,7 +2602,9 @@
 
 lemma fps_compose_mult_distrib_lemma:
   assumes c0: "c$0 = (0::'a::idom)"
-  shows "((a oo c) * (b oo c))$n = setsum (%s. setsum (%i. a$i * b$(s - i) * (c^s) $ n) {0..s}) {0..n}" (is "?l = ?r")
+  shows "((a oo c) * (b oo c))$n =
+    setsum (%s. setsum (%i. a$i * b$(s - i) * (c^s) $ n) {0..s}) {0..n}"
+    (is "?l = ?r")
   unfolding product_composition_lemma[OF c0 c0] power_add[symmetric]
   unfolding setsum_pair_less_iff[where a = "%k. a$k" and b="%m. b$m" and c="%s. (c ^ s)$n" and n = n] ..
 
@@ -2500,7 +2613,9 @@
   assumes c0: "c$0 = (0::'a::idom)"
   shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r")
   apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0])
-  by (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib)
+  apply (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib)
+  done
+
 lemma fps_compose_setprod_distrib:
   assumes c0: "c$0 = (0::'a::idom)"
   shows "(setprod a S) oo c = setprod (%k. a k oo c) S" (is "?l = ?r")
@@ -2513,57 +2628,59 @@
 
 lemma fps_compose_power:   assumes c0: "c$0 = (0::'a::idom)"
   shows "(a oo c)^n = a^n oo c" (is "?l = ?r")
-proof-
-  {assume "n=0" then have ?thesis by simp}
-  moreover
-  {fix m assume m: "n = Suc m"
-    have th0: "a^n = setprod (%k. a) {0..m}" "(a oo c) ^ n = setprod (%k. a oo c) {0..m}"
-      by (simp_all add: setprod_constant m)
-    then have ?thesis
-      by (simp add: fps_compose_setprod_distrib[OF c0])}
-  ultimately show ?thesis by (cases n, auto)
+proof (cases n)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc m)
+  have th0: "a^n = setprod (%k. a) {0..m}" "(a oo c) ^ n = setprod (%k. a oo c) {0..m}"
+    by (simp_all add: setprod_constant Suc)
+  then show ?thesis
+    by (simp add: fps_compose_setprod_distrib[OF c0])
 qed
 
 lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)"
   by (simp add: fps_eq_iff fps_compose_nth field_simps setsum_negf[symmetric])
 
-lemma fps_compose_sub_distrib:
-  shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
+lemma fps_compose_sub_distrib: "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)"
   unfolding diff_minus fps_compose_uminus fps_compose_add_distrib ..
 
-lemma X_fps_compose:"X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
+lemma X_fps_compose: "X oo a = Abs_fps (\<lambda>n. if n = 0 then (0::'a::comm_ring_1) else a$n)"
   by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta)
 
 lemma fps_inverse_compose:
-  assumes b0: "(b$0 :: 'a::field) = 0" and a0: "a$0 \<noteq> 0"
+  assumes b0: "(b$0 :: 'a::field) = 0"
+    and a0: "a$0 \<noteq> 0"
   shows "inverse a oo b = inverse (a oo b)"
-proof-
+proof -
   let ?ia = "inverse a"
   let ?ab = "a oo b"
   let ?iab = "inverse ?ab"
 
-from a0 have ia0: "?ia $ 0 \<noteq> 0" by (simp )
-from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def)
-have "(?ia oo b) *  (a oo b) = 1"
-unfolding fps_compose_mult_distrib[OF b0, symmetric]
-unfolding inverse_mult_eq_1[OF a0]
-fps_compose_1 ..
-
-then have "(?ia oo b) *  (a oo b) * ?iab  = 1 * ?iab" by simp
-then have "(?ia oo b) *  (?iab * (a oo b))  = ?iab" by simp
-then show ?thesis
-  unfolding inverse_mult_eq_1[OF ab0] by simp
+  from a0 have ia0: "?ia $ 0 \<noteq> 0" by simp
+  from a0 have ab0: "?ab $ 0 \<noteq> 0" by (simp add: fps_compose_def)
+  have "(?ia oo b) *  (a oo b) = 1"
+    unfolding fps_compose_mult_distrib[OF b0, symmetric]
+    unfolding inverse_mult_eq_1[OF a0]
+    fps_compose_1 ..
+  
+  then have "(?ia oo b) *  (a oo b) * ?iab  = 1 * ?iab" by simp
+  then have "(?ia oo b) *  (?iab * (a oo b))  = ?iab" by simp
+  then show ?thesis unfolding inverse_mult_eq_1[OF ab0] by simp
 qed
 
 lemma fps_divide_compose:
-  assumes c0: "(c$0 :: 'a::field) = 0" and b0: "b$0 \<noteq> 0"
+  assumes c0: "(c$0 :: 'a::field) = 0"
+    and b0: "b$0 \<noteq> 0"
   shows "(a/b) oo c = (a oo c) / (b oo c)"
     unfolding fps_divide_def fps_compose_mult_distrib[OF c0]
     fps_inverse_compose[OF c0 b0] ..
 
-lemma gp: assumes a0: "a$0 = (0::'a::field)"
-  shows "(Abs_fps (\<lambda>n. 1)) oo a = 1/(1 - a)" (is "?one oo a = _")
-proof-
+lemma gp:
+  assumes a0: "a$0 = (0::'a::field)"
+  shows "(Abs_fps (\<lambda>n. 1)) oo a = 1/(1 - a)"
+    (is "?one oo a = _")
+proof -
   have o0: "?one $ 0 \<noteq> 0" by simp
   have th0: "(1 - X) $ 0 \<noteq> (0::'a)" by simp
   from fps_inverse_gp[where ?'a = 'a]
@@ -2571,34 +2688,37 @@
   hence "inverse (inverse ?one) = inverse (1 - X)" by simp
   hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0]
     by (simp add: fps_divide_def)
-  show ?thesis unfolding th
+  show ?thesis
+    unfolding th
     unfolding fps_divide_compose[OF a0 th0]
     fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] ..
 qed
 
-lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
+lemma fps_const_power [simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
   by (induct n) auto
 
 lemma fps_compose_radical:
   assumes b0: "b$0 = (0::'a::field_char_0)"
-  and ra0: "r (Suc k) (a$0) ^ Suc k = a$0"
-  and a0: "a$0 \<noteq> 0"
+    and ra0: "r (Suc k) (a$0) ^ Suc k = a$0"
+    and a0: "a$0 \<noteq> 0"
   shows "fps_radical r (Suc k)  a oo b = fps_radical r (Suc k) (a oo b)"
-proof-
+proof -
   let ?r = "fps_radical r (Suc k)"
   let ?ab = "a oo b"
-  have ab0: "?ab $ 0 = a$0" by (simp add: fps_compose_def)
-  from ab0 a0 ra0 have rab0: "?ab $ 0 \<noteq> 0" "r (Suc k) (?ab $ 0) ^ Suc k = ?ab $ 0" by simp_all
+  have ab0: "?ab $ 0 = a$0"
+    by (simp add: fps_compose_def)
+  from ab0 a0 ra0 have rab0: "?ab $ 0 \<noteq> 0" "r (Suc k) (?ab $ 0) ^ Suc k = ?ab $ 0"
+    by simp_all
   have th00: "r (Suc k) ((a oo b) $ 0) = (fps_radical r (Suc k) a oo b) $ 0"
     by (simp add: ab0 fps_compose_def)
   have th0: "(?r a oo b) ^ (Suc k) = a  oo b"
     unfolding fps_compose_power[OF b0]
     unfolding iffD1[OF power_radical[of a r k], OF a0 ra0]  ..
-  from iffD1[OF radical_unique[where r=r and k=k and b= ?ab and a = "?r a oo b", OF rab0(2) th00 rab0(1)], OF th0] show ?thesis  .
+  from iffD1[OF radical_unique[where r=r and k=k and b= ?ab and a = "?r a oo b", OF rab0(2) th00 rab0(1)], OF th0]
+  show ?thesis  .
 qed
 
-lemma fps_const_mult_apply_left:
-  "fps_const c * (a oo b) = (fps_const c * a) oo b"
+lemma fps_const_mult_apply_left: "fps_const c * (a oo b) = (fps_const c * a) oo b"
   by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc)
 
 lemma fps_const_mult_apply_right:
@@ -2606,12 +2726,15 @@
   by (auto simp add: fps_const_mult_apply_left mult_commute)
 
 lemma fps_compose_assoc:
-  assumes c0: "c$0 = (0::'a::idom)" and b0: "b$0 = 0"
+  assumes c0: "c$0 = (0::'a::idom)"
+    and b0: "b$0 = 0"
   shows "a oo (b oo c) = a oo b oo c" (is "?l = ?r")
-proof-
-  {fix n
+proof -
+  {
+    fix n
     have "?l$n = (setsum (\<lambda>i. (fps_const (a$i) * b^i) oo c) {0..n})$n"
-      by (simp add: fps_compose_nth fps_compose_power[OF c0] fps_const_mult_apply_left setsum_right_distrib mult_assoc fps_setsum_nth)
+      by (simp add: fps_compose_nth fps_compose_power[OF c0] fps_const_mult_apply_left
+        setsum_right_distrib mult_assoc fps_setsum_nth)
     also have "\<dots> = ((setsum (\<lambda>i. fps_const (a$i) * b^i) {0..n}) oo c)$n"
       by (simp add: fps_compose_setsum_distrib)
     also have "\<dots> = ?r$n"
@@ -2619,34 +2742,46 @@
       apply (rule setsum_cong2)
       apply (rule setsum_mono_zero_right)
       apply (auto simp add: not_le)
-      by (erule startsby_zero_power_prefix[OF b0, rule_format])
-    finally have "?l$n = ?r$n" .}
+      apply (erule startsby_zero_power_prefix[OF b0, rule_format])
+      done
+    finally have "?l$n = ?r$n" .
+  }
   then show ?thesis by (simp add: fps_eq_iff)
 qed
 
 
 lemma fps_X_power_compose:
-  assumes a0: "a$0=0" shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r")
-proof-
-  {assume "k=0" hence ?thesis by simp}
-  moreover
-  {fix h assume h: "k = Suc h"
-    {fix n
-      {assume kn: "k>n" hence "?l $ n = ?r $n" using a0 startsby_zero_power_prefix[OF a0] h
-          by (simp add: fps_compose_nth del: power_Suc)}
-      moreover
-      {assume kn: "k \<le> n"
-        hence "?l$n = ?r$n"
-          by (simp add: fps_compose_nth mult_delta_left setsum_delta)}
-      moreover have "k >n \<or> k\<le> n"  by arith
-      ultimately have "?l$n = ?r$n"  by blast}
-    then have ?thesis unfolding fps_eq_iff by blast}
-  ultimately show ?thesis by (cases k, auto)
+  assumes a0: "a$0=0"
+  shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r")
+proof (cases k)
+  case 0
+  then show ?thesis by simp
+next
+  case(Suc h)
+  {
+    fix n
+    {
+      assume kn: "k>n"
+      hence "?l $ n = ?r $n" using a0 startsby_zero_power_prefix[OF a0] Suc
+        by (simp add: fps_compose_nth del: power_Suc)
+    }
+    moreover
+    {
+      assume kn: "k \<le> n"
+      hence "?l$n = ?r$n"
+        by (simp add: fps_compose_nth mult_delta_left setsum_delta)
+    }
+    moreover have "k >n \<or> k\<le> n"  by arith
+    ultimately have "?l$n = ?r$n"  by blast
+  }
+  then show ?thesis unfolding fps_eq_iff by blast
 qed
 
-lemma fps_inv_right: assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+lemma fps_inv_right:
+  assumes a0: "a$0 = 0"
+    and a1: "a$1 \<noteq> 0"
   shows "a oo fps_inv a = X"
-proof-
+proof -
   let ?ia = "fps_inv a"
   let ?iaa = "a oo fps_inv a"
   have th0: "?ia $ 0 = 0" by (simp add: fps_inv_def)
@@ -2661,9 +2796,10 @@
 qed
 
 lemma fps_inv_deriv:
-  assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
+  assumes a0:"a$0 = (0::'a::{field})"
+    and a1: "a$1 \<noteq> 0"
   shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)"
-proof-
+proof -
   let ?ia = "fps_inv a"
   let ?d = "fps_deriv a oo ?ia"
   let ?dia = "fps_deriv ?ia"
@@ -2672,14 +2808,15 @@
   from fps_inv_right[OF a0 a1] have "?d * ?dia = 1"
     by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] )
   hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp
-  with inverse_mult_eq_1[OF th0]
+  with inverse_mult_eq_1 [OF th0]
   show "?dia = inverse ?d" by simp
 qed
 
 lemma fps_inv_idempotent:
-  assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
+  assumes a0: "a$0 = 0"
+    and a1: "a$1 \<noteq> 0"
   shows "fps_inv (fps_inv a) = a"
-proof-
+proof -
   let ?r = "fps_inv"
   have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def)
   from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps)
@@ -2693,10 +2830,12 @@
 qed
 
 lemma fps_ginv_ginv:
-  assumes a0: "a$0 = 0" and a1: "a$1 \<noteq> 0"
-  and c0: "c$0 = 0" and  c1: "c$1 \<noteq> 0"
+  assumes a0: "a$0 = 0"
+    and a1: "a$1 \<noteq> 0"
+    and c0: "c$0 = 0"
+    and  c1: "c$1 \<noteq> 0"
   shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c"
-proof-
+proof -
   let ?r = "fps_ginv"
   from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def)
   from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps)
@@ -2705,20 +2844,23 @@
   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 by (auto simp add: fps_ginv_def)
+    using a0 c0 apply (auto simp add: fps_ginv_def)
+    done
   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 by (auto simp add: fps_inv_def)
+    using a0 c0 apply (auto simp add: fps_inv_def)
+    done
   then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp
 qed
 
 lemma fps_ginv_deriv:
-  assumes a0:"a$0 = (0::'a::{field})" and a1: "a$1 \<noteq> 0"
+  assumes a0:"a$0 = (0::'a::{field})"
+    and a1: "a$1 \<noteq> 0"
   shows "fps_deriv (fps_ginv b a) = (fps_deriv b / fps_deriv a) oo fps_ginv X a"
-proof-
+proof -
   let ?ia = "fps_ginv b a"
   let ?iXa = "fps_ginv X a"
   let ?d = "fps_deriv"
@@ -2744,19 +2886,21 @@
 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))"
 
 lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r")
-proof-
-  {fix n
+proof -
+  { fix n
     have "?l$n = ?r $ n"
-  apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
-  by (simp add: of_nat_mult field_simps)}
-then show ?thesis by (simp add: fps_eq_iff)
+      apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc)
+      apply (simp add: of_nat_mult field_simps)
+      done
+  }
+  then show ?thesis by (simp add: fps_eq_iff)
 qed
 
 lemma E_unique_ODE:
   "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c :: 'a::field_char_0)"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
-  {assume d: ?lhs
+proof
+  assume d: ?lhs
   from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)"
     by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc)
   {
@@ -2772,23 +2916,19 @@
       done
   }
   note th' = this
-  have ?rhs
-    by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')}
-  moreover
-  {
-    assume h: ?rhs
-    have ?lhs
-      apply (subst h)
-      apply simp
-      apply (simp only: h[symmetric])
-      apply simp
-      done
-  }
-  ultimately show ?thesis by blast
+  show ?rhs by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th')
+next
+  assume h: ?rhs
+  show ?lhs
+    apply (subst h)
+    apply simp
+    apply (simp only: h[symmetric])
+    apply simp
+    done
 qed
 
 lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r")
-proof-
+proof -
   have "fps_deriv (?r) = fps_const (a+b) * ?r"
     by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add)
   then have "?r = ?l" apply (simp only: E_unique_ODE)
@@ -2803,7 +2943,7 @@
   by (simp add: fps_eq_iff power_0_left)
 
 lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))"
-proof-
+proof -
   from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1"
     by (simp )
   have th1: "E a $ 0 \<noteq> 0" by simp
@@ -2819,7 +2959,7 @@
 lemma LE_compose:
   assumes a: "a\<noteq>0"
   shows "fps_inv (E a - 1) oo (E a - 1) = X"
-  and "(E a - 1) oo fps_inv (E a - 1) = X"
+    and "(E a - 1) oo fps_inv (E a - 1) = X"
 proof-
   let ?b = "E a - 1"
   have b0: "?b $ 0 = 0" by simp
@@ -2831,12 +2971,15 @@
 
 lemma fps_const_inverse:
   "a \<noteq> 0 \<Longrightarrow> inverse (fps_const (a::'a::field)) = fps_const (inverse a)"
-  apply (auto simp add: fps_eq_iff fps_inverse_def) by (case_tac "n", auto)
+  apply (auto simp add: fps_eq_iff fps_inverse_def)
+  apply (case_tac n)
+  apply auto
+  done
 
 lemma inverse_one_plus_X:
   "inverse (1 + X) = Abs_fps (\<lambda>n. (- 1 ::'a::{field})^n)"
   (is "inverse ?l = ?r")
-proof-
+proof -
   have th: "?l * ?r = 1"
     by (auto simp add: field_simps fps_eq_iff minus_one_power_iff simp del: minus_one)
   have th': "?l $ 0 \<noteq> 0" by (simp add: )
@@ -2849,7 +2992,7 @@
 lemma radical_E:
   assumes r: "r (Suc k) 1 = 1"
   shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))"
-proof-
+proof -
   let ?ck = "(c / of_nat (Suc k))"
   let ?r = "fps_radical r (Suc k)"
   have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c"
@@ -2908,17 +3051,21 @@
   by (simp add: L_def field_simps)
 
 lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def)
+
 lemma L_E_inv:
   assumes a: "a\<noteq> (0::'a::{field_char_0})"
   shows "L a = fps_inv (E a - 1)" (is "?l = ?r")
-proof-
+proof -
   let ?b = "E a - 1"
   have b0: "?b $ 0 = 0" by simp
   have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
-  have "fps_deriv (E a - 1) oo fps_inv (E a - 1) = (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)"
+  have "fps_deriv (E a - 1) oo fps_inv (E a - 1) =
+    (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)"
     by (simp add: field_simps)
-  also have "\<dots> = fps_const a * (X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1])
-    by (simp add: field_simps)
+  also have "\<dots> = fps_const a * (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
   finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" .
   from fps_inv_deriv[OF b0 b1, unfolded eq]
   have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)"
@@ -2931,7 +3078,8 @@
 qed
 
 lemma L_mult_add:
-  assumes c0: "c\<noteq>0" and d0: "d\<noteq>0"
+  assumes c0: "c\<noteq>0"
+    and d0: "d\<noteq>0"
   shows "L c + L d = fps_const (c+d) * L (c*d)"
   (is "?r = ?l")
 proof-
@@ -2940,7 +3088,8 @@
     by (simp add: fps_deriv_L fps_const_add[symmetric] algebra_simps del: fps_const_add)
   also have "\<dots> = fps_deriv ?l"
     apply (simp add: fps_deriv_L)
-    by (simp add: fps_eq_iff eq)
+    apply (simp add: fps_eq_iff eq)
+    done
   finally show ?thesis
     unfolding fps_deriv_eq_iff by simp
 qed
@@ -2956,7 +3105,7 @@
   fixes c :: "'a::field_char_0"
   shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c"
   (is "?lhs \<longleftrightarrow> ?rhs")
-proof-
+proof -
   let ?da = "fps_deriv a"
   let ?x1 = "(1 + X):: 'a fps"
   let ?l = "?x1 * ?da"
@@ -2965,7 +3114,8 @@
   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])
-    by (simp add: field_simps)
+    apply (simp add: field_simps)
+    done
   finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp
   moreover
   {assume h: "?l = ?r"