author wenzelm Fri, 10 Aug 2012 16:19:51 +0200 changeset 48757 1232760e208e parent 48756 1c843142758e child 48758 80ad6e0e147f
tuned proofs;
```--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 10 15:57:22 2012 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Aug 10 16:19:51 2012 +0200
@@ -26,7 +26,8 @@
lemma fps_nth_Abs_fps [simp]: "Abs_fps f \$ n = f n"

-text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *}
+text{* Definition of the basic elements 0 and 1 and the basic operations of addition,
+  negation and multiplication *}

instantiation fps :: (zero) zero
begin
@@ -335,10 +336,12 @@
lemma fps_const_mult[simp]: "fps_const (c::'a\<Colon>ring) * fps_const d = fps_const (c * d)"
by (simp add: fps_eq_iff fps_mult_nth setsum_0')

-lemma fps_const_add_left: "fps_const (c::'a\<Colon>monoid_add) + f = Abs_fps (\<lambda>n. if n = 0 then c + f\$0 else f\$n)"
+    Abs_fps (\<lambda>n. if n = 0 then c + f\$0 else f\$n)"

-lemma fps_const_add_right: "f + fps_const (c::'a\<Colon>monoid_add) = Abs_fps (\<lambda>n. if n = 0 then f\$0 + c else f\$n)"
+    Abs_fps (\<lambda>n. if n = 0 then f\$0 + c else f\$n)"

lemma fps_const_mult_left: "fps_const (c::'a\<Colon>semiring_0) * f = Abs_fps (\<lambda>n. c * f\$n)"
@@ -393,7 +396,7 @@
instance fps :: (idom) idom ..

lemma numeral_fps_const: "numeral k = fps_const (numeral k)"
-  by (induct k, simp_all only: numeral.simps fps_const_1_eq_1
+  by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1

lemma neg_numeral_fps_const: "neg_numeral k = fps_const (neg_numeral k)"
@@ -402,7 +405,7 @@
subsection{* The eXtractor series X*}

lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)"
-  by (induct n, auto)
+  by (induct n) auto

definition "X = Abs_fps (\<lambda>n. if n = 1 then 1 else 0)"
lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))"
@@ -417,7 +420,8 @@
ultimately show ?thesis by blast
qed

-lemma X_mult_right_nth[simp]: "((f :: ('a::comm_semiring_1) fps) * X) \$n = (if n = 0 then 0 else f \$ (n - 1))"
+lemma X_mult_right_nth[simp]:
+    "((f :: ('a::comm_semiring_1) fps) * X) \$n = (if n = 0 then 0 else f \$ (n - 1))"
by (metis X_mult_nth mult_commute)

lemma X_power_iff: "X^k = Abs_fps (\<lambda>n. if n = k then (1::'a::comm_ring_1) else 0)"
@@ -433,13 +437,17 @@
then show ?case by (simp add: fps_eq_iff)
qed

-lemma X_power_mult_nth: "(X^k * (f :: ('a::comm_ring_1) fps)) \$n = (if n < k then 0 else f \$ (n - k))"
+lemma X_power_mult_nth:
+    "(X^k * (f :: ('a::comm_ring_1) fps)) \$n = (if n < k then 0 else f \$ (n - k))"
apply (induct k arbitrary: n)
apply (simp)
unfolding power_Suc mult_assoc
-  by (case_tac n, auto)
-
-lemma X_power_mult_right_nth: "((f :: ('a::comm_ring_1) fps) * X^k) \$n = (if n < k then 0 else f \$ (n - k))"
+  apply (case_tac n)
+  apply auto
+  done
+
+lemma X_power_mult_right_nth:
+    "((f :: ('a::comm_ring_1) fps) * X^k) \$n = (if n < k then 0 else f \$ (n - k))"
by (metis X_power_mult_nth mult_commute)

@@ -448,10 +456,12 @@
subsection{* Formal Power series form a metric space *}

definition (in dist) ball_def: "ball x r = {y. dist y x < r}"
+
instantiation fps :: (comm_ring_1) dist
begin

-definition dist_fps_def: "dist (a::'a fps) b = (if (\<exists>n. a\$n \<noteq> b\$n) then inverse (2 ^ The (leastP (\<lambda>n. a\$n \<noteq> b\$n))) else 0)"
+definition dist_fps_def:
+  "dist (a::'a fps) b = (if (\<exists>n. a\$n \<noteq> b\$n) then inverse (2 ^ The (leastP (\<lambda>n. a\$n \<noteq> b\$n))) else 0)"

lemma dist_fps_ge0: "dist (a::'a fps) b \<ge> 0"
@@ -460,8 +470,11 @@
apply (rule cong[OF refl, where x="(\<lambda>n\<Colon>nat. a \$ n \<noteq> b \$ n)"])
apply (rule ext)
-  by auto
+  apply auto
+  done
+
instance ..
+
end

lemma fps_nonzero_least_unique: assumes a0: "a \<noteq> 0"
@@ -481,10 +494,11 @@
ultimately show ?thesis by blast
qed

-lemma fps_eq_least_unique: assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
+lemma fps_eq_least_unique:
+  assumes ab: "(a::('a::ab_group_add) fps) \<noteq> b"
shows "\<exists>! n. leastP (\<lambda>n. a\$n \<noteq> b\$n) n"
-using fps_nonzero_least_unique[of "a - b"] ab
-by auto
+  using fps_nonzero_least_unique[of "a - b"] ab
+  by auto

instantiation fps :: (comm_ring_1) metric_space
begin
@@ -497,25 +511,36 @@
show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
by (auto simp add: open_fps_def ball_def subset_eq)
next
-{  fix a b :: "'a fps"
-  {assume ab: "a = b"
-   then have "\<not> (\<exists>n. a\$n \<noteq> b\$n)" by simp
-   then have "dist a b = 0" by (simp add: dist_fps_def)}
- moreover
- {assume d: "dist a b = 0"
-   then have "\<forall>n. a\$n = b\$n"
-     by - (rule ccontr, simp add: dist_fps_def)
-   then have "a = b" by (simp add: fps_eq_iff)}
- ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast}
-note th = this
-from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
+  {
+    fix a b :: "'a fps"
+    {
+      assume ab: "a = b"
+      then have "\<not> (\<exists>n. a\$n \<noteq> b\$n)" by simp
+      then have "dist a b = 0" by (simp add: dist_fps_def)
+    }
+    moreover
+    {
+      assume d: "dist a b = 0"
+      then have "\<forall>n. a\$n = b\$n"
+        by - (rule ccontr, simp add: dist_fps_def)
+      then have "a = b" by (simp add: fps_eq_iff)
+    }
+    ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast
+  }
+  note th = this
+  from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp
fix a b c :: "'a fps"
-  {assume ab: "a = b" then have d0: "dist a b = 0"  unfolding th .
+  {
+    assume ab: "a = b" then have d0: "dist a b = 0"  unfolding th .
then have "dist a b \<le> dist a c + dist b c"
-      using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp}
+      using dist_fps_ge0[of a c] dist_fps_ge0[of b c] by simp
+  }
moreover
-  {assume c: "c = a \<or> c = b" then have "dist a b \<le> dist a c + dist b c"
-      by (cases "c=a", simp_all add: th dist_fps_sym) }
+  {
+    assume c: "c = a \<or> c = b"
+    then have "dist a b \<le> dist a c + dist b c"
+      by (cases "c=a") (simp_all add: th dist_fps_sym)
+  }
moreover
{assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c"
let ?P = "\<lambda>a b n. a\$n \<noteq> b\$n"
@@ -591,9 +616,12 @@

-lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a\$i)*X^i) {0..m})\$n = (if n \<le> m then a\$n else (0::'a::comm_ring_1))"
-  apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff  cong del: if_weak_cong)
+lemma fps_sum_rep_nth: "(setsum (%i. fps_const(a\$i)*X^i) {0..m})\$n =
+    (if n \<le> m then a\$n else (0::'a::comm_ring_1))"
+  apply (auto simp add: fps_eq_iff fps_setsum_nth X_power_nth cond_application_beta cond_value_iff
+    cong del: if_weak_cong)
+  done

lemma fps_notation:
"(%n. setsum (%i. fps_const(a\$i) * X^i) {0..n}) ----> a" (is "?s ----> a")
@@ -702,7 +730,8 @@
ultimately show ?thesis by blast
qed

-lemma fps_inverse_idempotent[intro]: assumes f0: "f\$0 \<noteq> (0::'a::field)"
+lemma fps_inverse_idempotent[intro]:
+  assumes f0: "f\$0 \<noteq> (0::'a::field)"
shows "inverse (inverse f) = f"
proof-
from f0 have if0: "inverse f \$ 0 \<noteq> 0" by simp
@@ -711,7 +740,8 @@
then show ?thesis using f0 unfolding mult_cancel_left by simp
qed

-lemma fps_inverse_unique: assumes f0: "f\$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
+lemma fps_inverse_unique:
+  assumes f0: "f\$0 \<noteq> (0::'a::field)" and fg: "f*g = 1"
shows "inverse f = g"
proof-
from inverse_mult_eq_1[OF f0] fg
@@ -748,9 +778,12 @@

definition "fps_deriv f = Abs_fps (\<lambda>n. of_nat (n + 1) * f \$ (n + 1))"

-lemma fps_deriv_nth[simp]: "fps_deriv f \$ n = of_nat (n +1) * f \$ (n+1)" by (simp add: fps_deriv_def)
-
-lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g"
+lemma fps_deriv_nth[simp]: "fps_deriv f \$ n = of_nat (n +1) * f \$ (n+1)"
+
+lemma fps_deriv_linear[simp]:
+  "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+    fps_const a * fps_deriv f + fps_const b * fps_deriv g"

lemma fps_deriv_mult[simp]:
@@ -821,7 +854,8 @@
lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0"
by (simp add: fps_ext fps_deriv_def fps_const_def)

-lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
+lemma fps_deriv_mult_const_left[simp]:
+    "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f"
by simp

lemma fps_deriv_0[simp]: "fps_deriv 0 = 0"
@@ -830,19 +864,24 @@
lemma fps_deriv_1[simp]: "fps_deriv 1 = 0"
by (simp add: fps_deriv_def fps_eq_iff )

-lemma fps_deriv_mult_const_right[simp]: "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
+lemma fps_deriv_mult_const_right[simp]:
+    "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c"
by simp

-lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
+lemma fps_deriv_setsum:
+  "fps_deriv (setsum f S) = setsum (\<lambda>i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S"
proof-
-  {assume "\<not> finite S" hence ?thesis by simp}
+  { assume "\<not> finite S" hence ?thesis by simp }
moreover
-  {assume fS: "finite S"
-    have ?thesis  by (induct rule: finite_induct[OF fS], simp_all)}
+  {
+    assume fS: "finite S"
+    have ?thesis  by (induct rule: finite_induct[OF fS]) simp_all
+  }
ultimately show ?thesis by blast
qed

-lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f\$0 :: 'a::{idom,semiring_char_0}))"
+lemma fps_deriv_eq_0_iff[simp]:
+  "fps_deriv f = 0 \<longleftrightarrow> (f = fps_const (f\$0 :: 'a::{idom,semiring_char_0}))"
proof-
{assume "f= fps_const (f\$0)" hence "fps_deriv f = fps_deriv (fps_const (f\$0))" by simp
hence "fps_deriv f = 0" by simp }
@@ -866,60 +905,76 @@
finally show ?thesis by (simp add: field_simps)
qed

-lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
-  apply auto unfolding fps_deriv_eq_iff by blast
-
-
-fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps" where
+lemma fps_deriv_eq_iff_ex:
+  "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>(c::'a::{idom,semiring_char_0}). f = fps_const c + g)"
+  apply auto unfolding fps_deriv_eq_iff
+  apply blast
+  done
+
+
+fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
+where
"fps_nth_deriv 0 f = f"
| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)"

lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)"
-  by (induct n arbitrary: f, auto)
-
-lemma fps_nth_deriv_linear[simp]: "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
-  by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute)
-
-lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
-  by (induct n arbitrary: f, simp_all)
-
-lemma fps_nth_deriv_add[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
+  by (induct n arbitrary: f) auto
+
+lemma fps_nth_deriv_linear[simp]:
+  "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) =
+    fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g"
+  by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute)
+
+lemma fps_nth_deriv_neg[simp]:
+  "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)"
+  by (induct n arbitrary: f) simp_all
+
+  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g"
using fps_nth_deriv_linear[of n 1 f 1 g] by simp

-lemma fps_nth_deriv_sub[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"
+lemma fps_nth_deriv_sub[simp]:
+  "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g"

lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0"
-  by (induct n, simp_all )
+  by (induct n) simp_all

lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)"
-  by (induct n, simp_all )
-
-lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
-  by (cases n, simp_all)
-
-lemma fps_nth_deriv_mult_const_left[simp]: "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
+  by (induct n) simp_all
+
+lemma fps_nth_deriv_const[simp]:
+  "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)"
+  by (cases n) simp_all
+
+lemma fps_nth_deriv_mult_const_left[simp]:
+  "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f"
using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp

-lemma fps_nth_deriv_mult_const_right[simp]: "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
+lemma fps_nth_deriv_mult_const_right[simp]:
+  "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c"
using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute)

-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"
+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" hence ?thesis by simp}
+  { assume "\<not> finite S" hence ?thesis by simp }
moreover
-  {assume fS: "finite S"
-    have ?thesis  by (induct rule: finite_induct[OF fS], simp_all)}
+  {
+    assume fS: "finite S"
+    have ?thesis  by (induct rule: finite_induct[OF fS]) simp_all
+  }
ultimately show ?thesis by blast
qed

-lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) \$ 0 = of_nat (fact k) * f\$(k)"
+lemma fps_deriv_maclauren_0:
+  "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) \$ 0 = of_nat (fact k) * f\$(k)"
by (induct k arbitrary: f) (auto simp add: field_simps of_nat_mult)

subsection {* Powers*}

lemma fps_power_zeroth_eq_one: "a\$0 =1 \<Longrightarrow> a^n \$ 0 = (1::'a::semiring_1)"
-  by (induct n, auto simp add: expand_fps_eq fps_mult_nth)
+  by (induct n) (auto simp add: expand_fps_eq fps_mult_nth)

lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)\$0 =1 \<Longrightarrow> a^n \$ 1 = of_nat n * a\$1"
proof(induct n)
@@ -932,19 +987,21 @@
qed

lemma startsby_one_power:"a \$ 0 = (1::'a::comm_ring_1) \<Longrightarrow> a^n \$ 0 = 1"
-  by (induct n, auto simp add: fps_mult_nth)
+  by (induct n) (auto simp add: fps_mult_nth)

lemma startsby_zero_power:"a \$0 = (0::'a::comm_ring_1) \<Longrightarrow> n > 0 \<Longrightarrow> a^n \$0 = 0"
-  by (induct n, auto simp add: fps_mult_nth)
+  by (induct n) (auto simp add: fps_mult_nth)

lemma startsby_power:"a \$0 = (v::'a::{comm_ring_1}) \<Longrightarrow> a^n \$0 = v^n"
-  by (induct n, auto simp add: fps_mult_nth power_Suc)
+  by (induct n) (auto simp add: fps_mult_nth power_Suc)

lemma startsby_zero_power_iff[simp]:
"a^n \$0 = (0::'a::{idom}) \<longleftrightarrow> (n \<noteq> 0 \<and> a\$0 = 0)"
apply (rule iffI)
-apply (induct n, auto simp add: power_Suc fps_mult_nth)
-by (rule startsby_zero_power, simp_all)
+apply (induct n)
+apply (rule startsby_zero_power, simp_all)
+done

lemma startsby_zero_power_prefix:
assumes a0: "a \$0 = (0::'a::idom)"
@@ -1029,9 +1086,13 @@
ultimately show ?thesis by blast
qed

-lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
-  by (case_tac n, auto simp add: power_Suc field_simps)
+lemma fps_deriv_power:
+    "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)"
+  apply (induct n)
+  apply (case_tac n)
+  apply (auto simp add: power_Suc field_simps)
+  done

lemma fps_inverse_deriv:
fixes a:: "('a :: field) fps"
@@ -1079,8 +1140,8 @@
assumes a0: "a\$0 \<noteq> 0"
shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2"
using fps_inverse_deriv[OF a0]
-  unfolding power2_eq_square fps_divide_def
-    fps_inverse_mult by simp
+  unfolding power2_eq_square fps_divide_def fps_inverse_mult
+  by simp

lemma inverse_mult_eq_1': assumes f0: "f\$0 \<noteq> (0::'a::field)"
shows "f * inverse f= 1"
@@ -1090,7 +1151,8 @@
assumes a0: "b\$0 \<noteq> 0"
shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2"
using fps_inverse_deriv[OF a0]
-  by (simp add: fps_divide_def field_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])
+  by (simp add: fps_divide_def field_simps
+    power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0])

lemma fps_inverse_gp': "inverse (Abs_fps(\<lambda>n. (1::'a::field)))
@@ -1136,7 +1198,8 @@
definition fps_compose :: "('a::semiring_1) fps \<Rightarrow> 'a fps \<Rightarrow> 'a fps" (infixl "oo" 55) where
fps_compose_def: "a oo b = Abs_fps (\<lambda>n. setsum (\<lambda>i. a\$i * (b^i\$n)) {0..n})"

-lemma fps_compose_nth: "(a oo b)\$n = setsum (\<lambda>i. a\$i * (b^i\$n)) {0..n}" by (simp add: fps_compose_def)
+lemma fps_compose_nth: "(a oo b)\$n = setsum (\<lambda>i. a\$i * (b^i\$n)) {0..n}"

lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)"
by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta')
@@ -1207,7 +1270,7 @@

lemma XDN_linear:
"(XD ^^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)"
-  by (induct n, simp_all)
+  by (induct n) simp_all

lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a\$n)" by (simp add: fps_eq_iff)

@@ -1296,7 +1359,10 @@
unfolding xs' ys'
using mn xs ys
-      unfolding natpermute_def by simp}
+      unfolding natpermute_def
+      apply simp
+      done
+  }
moreover
{fix l assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
@@ -1315,7 +1381,9 @@
apply (rule exI[where x = "?ys"])
using ls l
apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
-      by simp}
+      apply simp
+      done
+  }
ultimately show ?thesis by blast
qed

@@ -1324,7 +1392,8 @@
lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})"
apply (auto simp add: set_replicate_conv_if natpermute_def)
apply (rule nth_equalityI)
-  by simp_all
+  apply simp_all
+  done

lemma natpermute_finite: "finite (natpermute n k)"
proof(induct k arbitrary: n)
@@ -1368,7 +1437,8 @@
unfolding nth_list_update[OF i'(1)]
using i zxs
by (case_tac "ia=i", auto simp del: replicate.simps)
-    then have "xs \<in> ?B" using i by blast}
+    then have "xs \<in> ?B" using i by blast
+  }
moreover
{fix i assume i: "i \<in> {0..k}"
let ?xs = "replicate (k+1) 0 [i:=n]"
@@ -1383,7 +1453,8 @@
finally
have "?xs \<in> natpermute n (k+1)" using xsl unfolding natpermute_def mem_Collect_eq
by blast
-    then have "?xs \<in> ?A"  using nxs  by blast}
+    then have "?xs \<in> ?A"  using nxs  by blast
+  }
ultimately show ?thesis by auto
qed

@@ -1409,7 +1480,8 @@
unfolding fps_mult_nth H[rule_format, OF km] ..
also have "\<dots> = (\<Sum>v\<in>natpermute n (m + 1). \<Prod>j\<in>{0..m}. a j \$ v ! j)"
-      unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k]
+      unfolding natpermute_split[of m "m + 1", simplified, of n,
+        unfolded natlist_trivial_1[unfolded One_nat_def] k]
apply (subst setsum_UN_disjoint)
apply simp
apply simp
@@ -1428,8 +1500,9 @@
unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k]
apply (clarsimp simp add: natpermute_def nth_append)
done
-    finally have "?P m n" .}
-  ultimately show "?P m n " by (cases m, auto)
+    finally have "?P m n" .
+  }
+  ultimately show "?P m n " by (cases m) auto
qed

text{* The special form for powers *}
@@ -1474,7 +1547,8 @@
fix n assume H: "\<forall>m<n. b\$m = c\$m"
{assume n0: "n=0"
from h have "(b oo a)\$n = (c oo a)\$n" by simp
-          hence "b\$n = c\$n" using n0 by (simp add: fps_compose_nth)}
+          hence "b\$n = c\$n" using n0 by (simp add: fps_compose_nth)
+        }
moreover
{fix n1 assume n1: "n = Suc n1"
have f: "finite {0 .. n1}" "finite {n}" by simp_all
@@ -1492,10 +1566,12 @@
using startsby_zero_power_nth_same[OF a0]
by simp
from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1
-          have "b\$n = c\$n" by auto}
-        ultimately show "b\$n = c\$n" by (cases n, auto)
+          have "b\$n = c\$n" by auto
+        }
+        ultimately show "b\$n = c\$n" by (cases n) auto
qed}
-    then have ?rhs by (simp add: fps_eq_iff)}
+    then have ?rhs by (simp add: fps_eq_iff)
+  }
ultimately show ?thesis by blast
qed

@@ -1507,7 +1583,10 @@
"radical r 0 a 0 = 1"
| "radical r 0 a (Suc n) = 0"
| "radical r (Suc k) a 0 = r (Suc k) (a\$0)"
-| "radical r (Suc k) a (Suc n) = (a\$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k}) {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) / (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
+| "radical r (Suc k) a (Suc n) =
+    (a\$ Suc n - setsum (\<lambda>xs. setprod (\<lambda>j. radical r (Suc k) a (xs ! j)) {0..k})
+      {xs. xs \<in> natpermute (Suc n) (Suc k) \<and> Suc n \<notin> set xs}) /
+    (of_nat (Suc k) * (radical r (Suc k) a 0)^k)"
by pat_completeness auto

@@ -1574,7 +1653,8 @@
let ?K = "{0 ..k}"
have fK: "finite ?K" by simp
have fAK: "\<forall>i\<in>?K. finite (?A i)" by auto
-  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow> {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
+  have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow>
+    {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
proof(clarify)
fix i j assume i: "i \<in> ?K" and j: "j\<in> ?K" and ij: "i\<noteq>j"
{assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
@@ -1839,13 +1919,13 @@

fixes a:: "'a::field_char_0 fps"
-  assumes
-  k: "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 * 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)"
+  assumes k: "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 * 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"
@@ -2095,7 +2175,8 @@

lemma fps_inv_ginv: "fps_inv = fps_ginv X"
apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def)
-  apply (induct_tac n rule: nat_less_induct, auto)
+  apply (induct_tac n rule: nat_less_induct)
+  apply auto
apply (case_tac na)
apply simp
apply simp
@@ -2305,7 +2386,7 @@
qed

lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)"
-by (induct n, auto)
+  by (induct n) auto

assumes b0: "b\$0 = (0::'a::field_char_0)"
@@ -2532,7 +2613,7 @@
qed

lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)"
-  by (induct n, auto simp add: power_Suc)
+  by (induct n) (auto simp add: power_Suc)

lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1"
@@ -2565,7 +2646,7 @@
qed

lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)"

assumes r: "r (Suc k) 1 = 1"
@@ -3197,10 +3278,10 @@

lemma foldl_mult_start:
"foldl (%r x. r * f x) (v::'a::comm_ring_1) as * x = foldl (%r x. r * f x) (v * x) as "
-  by (induct as arbitrary: x v, auto simp add: algebra_simps)
+  by (induct as arbitrary: x v) (auto simp add: algebra_simps)

lemma foldr_mult_foldl: "foldr (%x r. r * f x) as v = foldl (%r x. r * f x) (v :: 'a::comm_ring_1) as"
-  by (induct as arbitrary: v, auto simp add: foldl_mult_start)
+  by (induct as arbitrary: v) (auto simp add: foldl_mult_start)

lemma F_nth_alt: "F as bs c \$ n = foldr (\<lambda>a r. r * pochhammer a n) as (c ^ n) /
foldr (\<lambda>b r. r * pochhammer b n) bs (of_nat (fact n))"
@@ -3224,11 +3305,12 @@
apply simp
apply (subgoal_tac "ALL as. foldl (%(r::'a) (a::'a). r) 1 as = 1")
apply auto
-  apply (induct_tac as, auto)
+  apply (induct_tac as)
+  apply auto
done

lemma foldl_prod_prod: "foldl (%(r::'b::comm_ring_1) (x::'a::comm_ring_1). r * f x) v as * foldl (%r x. r * g x) w as = foldl (%r x. r * f x * g x) (v*w) as"
-  by (induct as arbitrary: v w, auto simp add: algebra_simps)
+  by (induct as arbitrary: v w) (auto simp add: algebra_simps)

lemma F_rec: "F as bs c \$ Suc n = ((foldl (%r a. r* (a + of_nat n)) c as)/ (foldl (%r b. r * (b + of_nat n)) (of_nat (Suc n)) bs )) * F as bs c \$ n"
@@ -3276,7 +3358,7 @@

lemma XDp_foldr_nth[simp]: "foldr (%c r. XDp c o r) cs (%c. XDp c a) c0 \$ n =
foldr (%c r. (c + of_nat n) * r) cs (c0 + of_nat n) * a\$n"
-  by (induct cs arbitrary: c0, auto simp add: algebra_simps)
+  by (induct cs arbitrary: c0) (auto simp add: algebra_simps)

lemma genric_XDp_foldr_nth:
assumes
@@ -3284,6 +3366,6 @@

shows "foldr (%c r. f c o r) cs (%c. g c a) c0 \$ n =
foldr (%c r. (k c + of_nat n) * r) cs (g c0 a \$ n)"
-  by (induct cs arbitrary: c0, auto simp add: algebra_simps f)
+  by (induct cs arbitrary: c0) (auto simp add: algebra_simps f)

end```