author wenzelm Sun, 25 Aug 2013 21:25:17 +0200 changeset 53195 e4b18828a817 parent 53194 1943db7bc34c child 53196 942a1b48bb31
tuned proofs;
```--- 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))"
@@ -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))"
-    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))"
+  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 @@
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)
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 @@
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 (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]
using bn0
+          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]
@@ -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 @@
}
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

"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