
diff -r 1943db7bc34c -r e4b18828a817 src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 25 20:57:09 2013 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Sun Aug 25 21:25:17 2013 +0200
@@ -139,7 +139,8 @@
 qed
 
 lemma fps_mult_assoc_lemma:
-  fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
+  fixes k :: nat
+    and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add"
   shows "(\<Sum>j=0..k. \<Sum>i=0..j. f i (j - i) (n - j)) =
          (\<Sum>j=0..k. \<Sum>i=0..k - j. f j i (n - j - i))"
   by (induct k) (simp_all add: Suc_diff_le setsum_addf add_assoc)
@@ -254,7 +255,7 @@
 
 instance fps :: (semiring_0) semiring_0
 proof
-  fix a:: "'a fps"
+  fix a :: "'a fps"
   show "0 * a = 0" by (simp add: fps_ext fps_mult_nth)
   show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth)
 qed
@@ -392,22 +393,19 @@
   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))"
-proof -
-  {
-    assume n: "n \<noteq> 0"
-    have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
-      by (simp add: fps_mult_nth)
-    also have "\<dots> = f $ (n - 1)"
-      using n by (simp add: X_def mult_delta_left setsum_delta)
-    finally have ?thesis using n by simp
-  }
-  moreover
-  {
-    assume n: "n=0"
-    hence ?thesis by (simp add: fps_mult_nth X_def)
-  }
-  ultimately show ?thesis by blast
+
+lemma X_mult_nth [simp]:
+  "(X * (f :: ('a::semiring_1) fps)) $n = (if n = 0 then 0 else f $ (n - 1))"
+proof (cases "n = 0")
+  case False
+  have "(X * f) $n = (\<Sum>i = 0..n. X $ i * f $ (n - i))"
+    by (simp add: fps_mult_nth)
+  also have "\<dots> = f $ (n - 1)"
+    using False by (simp add: X_def mult_delta_left setsum_delta)
+  finally show ?thesis using False by simp
+next
+  case True
+  then show ?thesis by (simp add: fps_mult_nth X_def)
 qed
 
 lemma X_mult_right_nth[simp]:
@@ -911,17 +909,12 @@
 
 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"
-    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 False
+  then show ?thesis by simp
+next
+  case True
+  show ?thesis by (induct rule: finite_induct [OF True]) simp_all
 qed
 
 lemma fps_deriv_eq_0_iff [simp]:
@@ -959,10 +952,7 @@
 
 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
+  by (auto simp: fps_deriv_eq_iff)
 
 
 fun fps_nth_deriv :: "nat \<Rightarrow> ('a::semiring_1) fps \<Rightarrow> 'a fps"
@@ -1272,14 +1262,16 @@
   "fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) =
     fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0"
   (is "?l = ?r")
-proof-
+proof -
   have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral)
   moreover have "?l$0 = ?r$0" by (simp add: fps_integral_def)
   ultimately show ?thesis
     unfolding fps_deriv_eq_iff by auto
 qed
 
+
 subsection {* Composition of FPSs *}
+
 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})"
 
@@ -1341,7 +1333,8 @@
   then show ?thesis by (simp add: fps_eq_iff)
 qed
 
-subsubsection{* Rule 2*}
+
+subsubsection {* Rule 2*}
 
   (* We can not reach the form of Wilf, but still near to it using rewrite rules*)
   (* If f reprents {a_n} and P is a polynomial, then
@@ -1372,12 +1365,14 @@
   "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)"
   by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def)
 
+
 subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*}
+
 subsubsection{* Rule 5 --- summation and "division" by (1 - X)*}
 
 lemma fps_divide_X_minus1_setsum_lemma:
   "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
-proof-
+proof -
   let ?X = "X::('a::comm_ring_1) fps"
   let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
   have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)"
@@ -1417,7 +1412,7 @@
 qed
 
 lemma fps_divide_X_minus1_setsum:
-  "a /((1::('a::field) fps) - X)  = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
+  "a /((1::('a::field) fps) - X) = Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})"
 proof -
   let ?X = "1 - (X::('a::field) fps)"
   have th0: "?X $ 0 \<noteq> 0" by simp
@@ -1429,6 +1424,7 @@
   finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0])
 qed
 
+
 subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary
   finite product of FPS, also the relvant instance of powers of a FPS*}
 
@@ -1445,9 +1441,8 @@
   shows "listsum xs \<le> n" and "listsum ys \<le> n"
 proof -
   from h have "listsum (xs @ ys) = n" by (simp add: natpermute_def)
-  hence *: "listsum xs + listsum ys = n" by simp
-  from * show "listsum xs \<le> n" by simp
-  from * show "listsum ys \<le> n" by simp
+  hence "listsum xs + listsum ys = n" by simp
+  then show "listsum xs \<le> n" and "listsum ys \<le> n" by simp_all
 qed
 
 lemma natpermute_split:
@@ -1667,23 +1662,17 @@
 lemma fps_nth_power_0:
   fixes m :: nat and a :: "('a::{comm_ring_1}) fps"
   shows "(a ^m)$0 = (a$0) ^ m"
-proof -
-  {
-    assume "m = 0"
-    hence ?thesis by simp
-  }
-  moreover
-  {
-    fix n
-    assume m: "m = Suc n"
-    have c: "m = card {0..n}" using m by simp
-    have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
-      by (simp add: m fps_power_nth del: replicate.simps power_Suc)
-    also have "\<dots> = (a$0) ^ m"
-     unfolding c by (rule setprod_constant) simp
-   finally have ?thesis .
-  }
-  ultimately show ?thesis by (cases m) auto
+proof (cases m)
+  case 0
+  then show ?thesis by simp
+next
+  case (Suc n)
+  then have c: "m = card {0..n}" by simp
+  have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}"
+    by (simp add: Suc fps_power_nth del: replicate.simps power_Suc)
+  also have "\<dots> = (a$0) ^ m"
+   unfolding c by (rule setprod_constant) simp
+ finally show ?thesis .
 qed
 
 lemma fps_compose_inj_right:
@@ -2316,8 +2305,7 @@
       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)
+      by (rule setsum_reindex_cong [where f = Suc]) (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}" .
 
@@ -2626,8 +2614,10 @@
   apply (simp add: fps_compose_mult_distrib[OF c0])
   done
 
-lemma fps_compose_power:   assumes c0: "c$0 = (0::'a::idom)"
-  shows "(a oo c)^n = a^n oo c" (is "?l = ?r")
+lemma fps_compose_power:
+  assumes c0: "c$0 = (0::'a::idom)"
+  shows "(a oo c)^n = a^n oo c"
+  (is "?l = ?r")
 proof (cases n)
   case 0
   then show ?thesis by simp
@@ -2844,14 +2834,16 @@
   then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp
   then have "?r b (?r c a) oo (?r c a oo a) = b oo a"
     apply (subst fps_compose_assoc)
-    using a0 c0 apply (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 apply (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
@@ -2883,13 +2875,16 @@
 subsection{* Elementary series *}
 
 subsubsection{* Exponential series *}
+
 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
+  {
+    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)
+      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
   }
@@ -2960,7 +2955,7 @@
   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"
-proof-
+proof -
   let ?b = "E a - 1"
   have b0: "?b $ 0 = 0" by simp
   have b1: "?b $ 1 \<noteq> 0" by (simp add: a)
@@ -2968,7 +2963,6 @@
   from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" .
 qed
 
-
 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)
@@ -3034,6 +3028,7 @@
   unfolding of_nat_add[symmetric] of_nat_power[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric]
   by simp
 
+
 subsubsection{* Logarithmic series *}
 
 lemma Abs_fps_if_0:
@@ -3206,15 +3201,17 @@
 
 lemma binomial_Vandermonde: "setsum (\<lambda>k. (a choose k) * (b choose (n - k))) {0..n} = (a + b) choose n"
   using gbinomial_Vandermonde[of "(of_nat a)" "of_nat b" n]
-
   apply (simp only: binomial_gbinomial[symmetric] of_nat_mult[symmetric] of_nat_setsum[symmetric] of_nat_add[symmetric])
-  by simp
+  apply simp
+  done
 
 lemma binomial_Vandermonde_same: "setsum (\<lambda>k. (n choose k)\<^sup>2) {0..n} = (2*n) choose n"
   using binomial_Vandermonde[of n n n,symmetric]
-  unfolding mult_2 apply (simp add: power2_eq_square)
+  unfolding mult_2
+  apply (simp add: power2_eq_square)
   apply (rule setsum_cong2)
-  by (auto intro:  binomial_symmetric)
+  apply (auto intro:  binomial_symmetric)
+  done
 
 lemma Vandermonde_pochhammer_lemma:
   fixes a :: "'a::field_char_0"
@@ -3244,17 +3241,19 @@
         using kn
         by (cases "k=0", simp_all add: gbinomial_pochhammer)}
     moreover
-    {assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0"
+    { assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0"
       then obtain m where m: "n = Suc m" by (cases n, auto)
       from k0 obtain h where h: "k = Suc h" by (cases k, auto)
-      {assume kn: "k = n"
+      { assume kn: "k = n"
         then have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
           using kn pochhammer_minus'[where k=k and n=n and b=b]
           apply (simp add:  pochhammer_same)
           using bn0
-          by (simp add: field_simps power_add[symmetric])}
+          apply (simp add: field_simps power_add[symmetric])
+          done
+      }
       moreover
-      {assume nk: "k \<noteq> n"
+      { assume nk: "k \<noteq> n"
         have m1nk: "?m1 n = setprod (%i. - 1) {0..m}"
           "?m1 k = setprod (%i. - 1) {0..h}"
           by (simp_all add: setprod_constant m h)
@@ -3323,11 +3322,16 @@
           using kn' by (simp add: gbinomial_def)
         finally have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" by simp}
       ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)"
-        by (cases "k =n", auto)}
+        by (cases "k = n") auto
+    }
     ultimately have "b gchoose (n - k) = (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
+      apply (cases "n = 0")
       using nz'
-      apply (cases "n=0", auto)
-      by (cases "k", auto)}
+      apply auto
+      apply (cases k)
+      apply auto
+      done
+  }
   note th00 = this
   have "?r = ((a + b) gchoose n) * (of_nat (fact n)/ (?m1 n * pochhammer (- b) n))"
     unfolding gbinomial_pochhammer
@@ -3345,16 +3349,18 @@
 
 
 lemma Vandermonde_pochhammer:
-   fixes a :: "'a::field_char_0"
+  fixes a :: "'a::field_char_0"
   assumes c: "ALL i : {0..< n}. c \<noteq> - of_nat i"
-  shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) / (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n"
-proof-
+  shows "setsum (%k. (pochhammer a k * pochhammer (- (of_nat n)) k) /
+    (of_nat (fact k) * pochhammer c k)) {0..n} = pochhammer (c - a) n / pochhammer c n"
+proof -
   let ?a = "- a"
   let ?b = "c + of_nat n - 1"
   have h: "\<forall> j \<in>{0..< n}. ?b \<noteq> of_nat j" using c
     apply (auto simp add: algebra_simps of_nat_diff)
     apply (erule_tac x= "n - j - 1" in ballE)
-    by (auto simp add: of_nat_diff algebra_simps)
+    apply (auto simp add: of_nat_diff algebra_simps)
+    done
   have th0: "pochhammer (- (?a + ?b)) n = (- 1)^n * pochhammer (c - a) n"
     unfolding pochhammer_minus[OF le_refl]
     by (simp add: algebra_simps)
@@ -3367,6 +3373,7 @@
   show ?thesis using nz by (simp add: field_simps setsum_right_distrib)
 qed
 
+
 subsubsection{* Formal trigonometric functions  *}
 
 definition "fps_sin (c::'a::field_char_0) =
@@ -3379,7 +3386,7 @@
   "fps_deriv (fps_sin c) = fps_const c * fps_cos c"
   (is "?lhs = ?rhs")
 proof (rule fps_ext)
-  fix n::nat
+  fix n :: nat
   {
     assume en: "even n"
     have "?lhs$n = of_nat (n+1) * (fps_sin c $ (n+1))" by simp
@@ -3394,7 +3401,7 @@
       by (simp add: fps_cos_def field_simps)
   }
   then show "?lhs $ n = ?rhs $ n"
-    by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def)
+    by (cases "even n") (simp_all add: fps_deriv_def fps_sin_def fps_cos_def)
 qed
 
 lemma fps_cos_deriv: "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)"
@@ -3439,30 +3446,30 @@
 qed
 
 lemma divide_eq_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x / a = y \<longleftrightarrow> x = y * a"
-by auto
+  by auto
 
 lemma eq_divide_iff: "a \<noteq> (0::'a::field) \<Longrightarrow> x = y / a \<longleftrightarrow> x * a = y"
-by auto
+  by auto
 
 lemma fps_sin_nth_0 [simp]: "fps_sin c $ 0 = 0"
-unfolding fps_sin_def by simp
+  unfolding fps_sin_def by simp
 
 lemma fps_sin_nth_1 [simp]: "fps_sin c $ 1 = c"
-unfolding fps_sin_def by simp
+  unfolding fps_sin_def by simp
 
 lemma fps_sin_nth_add_2:
   "fps_sin c $ (n + 2) = - (c * c * fps_sin c $ n / (of_nat(n+1) * of_nat(n+2)))"
-unfolding fps_sin_def
-apply (cases n, simp)
-apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
-apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
-done
+  unfolding fps_sin_def
+  apply (cases n, simp)
+  apply (simp add: divide_eq_iff eq_divide_iff del: of_nat_Suc fact_Suc)
+  apply (simp add: of_nat_mult del: of_nat_Suc mult_Suc)
+  done
 
 lemma fps_cos_nth_0 [simp]: "fps_cos c $ 0 = 1"
-unfolding fps_cos_def by simp
+  unfolding fps_cos_def by simp
 
 lemma fps_cos_nth_1 [simp]: "fps_cos c $ 1 = 0"
-unfolding fps_cos_def by simp
+  unfolding fps_cos_def by simp
 
 lemma fps_cos_nth_add_2:
   "fps_cos c $ (n + 2) = - (c * c * fps_cos c $ n / (of_nat(n+1) * of_nat(n+2)))"




