author wenzelm Wed, 07 Aug 2013 23:20:11 +0200 changeset 52903 6c89225ddeba parent 52902 7196e1ce1cd8 child 52904 f8fca14c8cbd child 52907 288896518cf5
tuned proofs;
```--- 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)
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)
+  "k \<le> n \<Longrightarrow> Suc n * (n choose k) = (Suc n choose Suc k) * Suc k"
+  apply (induct n arbitrary: k)
apply (case_tac k)
done
@@ -65,15 +64,14 @@
text{*This is the well-known version, but it's harder to use because of the
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"

-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 atomize
+  apply (rotate_tac -1)
+  apply (erule finite_induct)
apply (simp_all (no_asm_simp) cong add: conj_cong
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)"

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"

-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"
+
+lemma pochhammer_Suc0 [simp]: "pochhammer a (Suc 0) = a"

lemma pochhammer_Suc_setprod: "pochhammer a (Suc n) = setprod (\<lambda>n. a + of_nat n) {0 .. n}"

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
+    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 (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
+    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]

-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 (cases n)
@@ -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]
-  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]]

+
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 (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))"
also have "\<dots> = (k + (m - h)) * fact m"
using H[rule_format, OF mn hm'] H[rule_format, OF mn km]
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
-      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
+    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)"
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"
-    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```
```--- 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
-  hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 =
+    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 @@

-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

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"
+            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"
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)
+          done
then have "a\$n = ?r \$n"
apply (simp del: of_nat_Suc)
-          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 @@

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

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

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

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

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

-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]
-  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

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"
+  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"
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"
also have "\<dots> = ?r\$n"
@@ -2619,34 +2742,46 @@
apply (rule setsum_cong2)
apply (rule setsum_mono_zero_right)
-      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"
then have "?r = ?l" apply (simp only: E_unique_ODE)
@@ -2803,7 +2943,7 @@

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

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)"
-  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])
+  also have "\<dots> = fps_const a * (X + 1)"
+    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

-  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 @@
also have "\<dots> = 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])