author wenzelm Mon, 22 Jun 2015 21:50:12 +0200 changeset 60558 4fcc6861e64f parent 60557 5854821993d2 child 60559 48d7b203c0ea
tuned proofs;
```--- a/src/HOL/Library/Formal_Power_Series.thy	Mon Jun 22 21:07:10 2015 +0200
+++ b/src/HOL/Library/Formal_Power_Series.thy	Mon Jun 22 21:50:12 2015 +0200
@@ -508,9 +508,9 @@
using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c]
by auto
have th1: "\<And>n. (2::real)^n > 0" by auto
-    {
-      assume h: "dist a b > dist a c + dist b c"
-      then have gt: "dist a b > dist a c" "dist a b > dist b c"
+    have False if "dist a b > dist a c + dist b c"
+    proof -
+      from that have gt: "dist a b > dist a c" "dist a b > dist b c"
using pos by auto
from gt have gtn: "n a b < n b c" "n a b < n a c"
unfolding dab dbc dac by (auto simp add: th1)
@@ -518,8 +518,8 @@
have "a \$ n a b = b \$ n a b" by simp
moreover have "a \$ n a b \<noteq> b \$ n a b"
unfolding n_def by (rule LeastI_ex) (insert \<open>a \<noteq> b\<close>, simp add: fps_eq_iff)
-      ultimately have False by contradiction
-    }
+      ultimately show ?thesis by contradiction
+    qed
then show ?thesis
qed
@@ -527,7 +527,7 @@

end

-text \<open>The infinite sums and justification of the notation in textbooks\<close>
+text \<open>The infinite sums and justification of the notation in textbooks.\<close>

lemma reals_power_lt_ex:
fixes x y :: real
@@ -576,19 +576,17 @@
lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a\$i) * X^i) {0..n}) ----> a"
(is "?s ----> a")
proof -
-  {
-    fix r :: real
-    assume "r > 0"
+  have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" if "r > 0" for r
+  proof -
obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0"
using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto
-    have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r"
+    show ?thesis
proof -
-      {
-        fix n :: nat
-        assume nn0: "n \<ge> n0"
-        then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
+      have "dist (?s n) a < r" if nn0: "n \<ge> n0" for n
+      proof -
+        from that have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0"
-        have "dist (?s n) a < r"
+        show ?thesis
proof (cases "?s n = a")
case True
then show ?thesis
@@ -610,10 +608,10 @@
using n0 by simp
finally show ?thesis .
qed
-      }
+      qed
then show ?thesis by blast
qed
-  }
+  qed
then show ?thesis
unfolding lim_sequentially by blast
qed
@@ -623,7 +621,7 @@

declare setsum.cong[fundef_cong]

-instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse
begin

fun natfun_inverse:: "'a fps \<Rightarrow> nat \<Rightarrow> 'a"
@@ -778,8 +776,8 @@
shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g"
proof -
let ?D = "fps_deriv"
-  {
-    fix n :: nat
+  have "(f * ?D g + ?D f * g) \$ n = ?D (f*g) \$ n" for n
+  proof -
let ?Zn = "{0 ..n}"
let ?Zn1 = "{0 .. n + 1}"
let ?g = "\<lambda>i. of_nat (i+1) * g \$ (i+1) * f \$ (n - i) +
@@ -806,9 +804,10 @@
apply (rule setsum.cong)
apply (auto simp add: of_nat_diff field_simps)
done
-    finally have "(f * ?D g + ?D f * g) \$ n = ?D (f*g) \$ n" .
-  }
-  then show ?thesis unfolding fps_eq_iff by auto
+    finally show ?thesis .
+  qed
+  then show ?thesis
+    unfolding fps_eq_iff by auto
qed

lemma fps_deriv_X[simp]: "fps_deriv X = 1"
@@ -1407,9 +1406,10 @@
assumes "h \<le> k"
shows "natpermute n k =
(\<Union>m \<in>{0..n}. {l1 @ l2 |l1 l2. l1 \<in> natpermute m h \<and> l2 \<in> natpermute (n - m) (k - h)})"
-  (is "?L = ?R" is "?L = (\<Union>m \<in>{0..n}. ?S m)")
-proof -
-  {
+  (is "?L = ?R" is "_ = (\<Union>m \<in>{0..n}. ?S m)")
+proof
+  show "?R \<subseteq> ?L"
+  proof
fix l
assume l: "l \<in> ?R"
from l obtain m xs ys where h: "m \<in> {0..n}"
@@ -1420,16 +1420,16 @@
from ys have ys': "listsum ys = n - m"
-    have "l \<in> ?L" using leq xs ys h
+    show "l \<in> ?L" using leq xs ys h
unfolding xs' ys'
using assms xs ys
unfolding natpermute_def
apply simp
done
-  }
-  moreover
-  {
+  qed
+  show "?L \<subseteq> ?R"
+  proof
fix l
assume l: "l \<in> natpermute n k"
let ?xs = "take h l"
@@ -1445,7 +1445,7 @@
using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id)
from ls have m: "?m \<in> {0..n}"
by (simp add: l_take_drop del: append_take_drop_id)
-    from xs ys ls have "l \<in> ?R"
+    from xs ys ls show "l \<in> ?R"
apply auto
apply (rule bexI [where x = "?m"])
apply (rule exI [where x = "?xs"])
@@ -1454,8 +1454,7 @@
apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id)
apply simp
done
-  }
-  ultimately show ?thesis by blast
+  qed
qed

lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})"
@@ -1486,13 +1485,16 @@
qed

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]})"
+  "{xs \<in> natpermute n (k + 1). n \<in> set xs} = (\<Union>i\<in>{0 .. k}. {(replicate (k + 1) 0) [i:=n]})"
(is "?A = ?B")
-proof -
-  {
+proof
+  show "?A \<subseteq> ?B"
+  proof
fix xs
-    assume H: "xs \<in> natpermute n (k+1)" and n: "n \<in> set xs"
-    from n obtain i where i: "i \<in> {0.. k}" "xs!i = n" using H
+    assume "xs \<in> ?A"
+    then have H: "xs \<in> natpermute n (k + 1)" and n: "n \<in> set xs"
+      by blast+
+    then obtain i where i: "i \<in> {0.. k}" "xs!i = n"
unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def)
have eqs: "({0..k} - {i}) \<union> {i} = {0..k}"
using i by auto
@@ -1522,33 +1524,34 @@
apply (case_tac "ia = i")
apply (auto simp del: replicate.simps)
done
-    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]"
-    have nxs: "n \<in> set ?xs"
+    then show "xs \<in> ?B" using i by blast
+  qed
+  show "?B \<subseteq> ?A"
+  proof
+    fix xs
+    assume "xs \<in> ?B"
+    then obtain i where i: "i \<in> {0..k}" and xs: "xs = replicate (k + 1) 0 [i:=n]"
+      by auto
+    have nxs: "n \<in> set xs"
+      unfolding xs
apply (rule set_update_memI)
using i apply simp
done
-    have xsl: "length ?xs = k+1"
-      by (simp only: length_replicate length_list_update)
-    have "listsum ?xs = setsum (nth ?xs) {0..<k+1}"
+    have xsl: "length xs = k + 1"
+      by (simp only: xs length_replicate length_list_update)
+    have "listsum xs = setsum (nth xs) {0..<k+1}"
unfolding listsum_setsum_nth xsl ..
also have "\<dots> = setsum (\<lambda>j. if j = i then n else 0) {0..< k+1}"
-      by (rule setsum.cong) (simp_all del: replicate.simps)
+      by (rule setsum.cong) (simp_all add: xs del: replicate.simps)
also have "\<dots> = n" using i by (simp add: setsum.delta)
-    finally have "?xs \<in> natpermute n (k+1)"
+    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
-  }
-  ultimately show ?thesis by auto
+    then show "xs \<in> ?A"
+      using nxs by blast
+  qed
qed

-text \<open>The general form\<close>
+text \<open>The general form.\<close>
lemma fps_setprod_nth:
fixes m :: nat
and a :: "nat \<Rightarrow> 'a::comm_ring_1 fps"
@@ -1603,7 +1606,7 @@
qed
qed

-text \<open>The special form for powers\<close>
+text \<open>The special form for powers.\<close>
lemma fps_power_nth_Suc:
fixes m :: nat
and a :: "'a::comm_ring_1 fps"
@@ -1708,8 +1711,8 @@
next
fix r k a n xs i
assume xs: "xs \<in> {xs \<in> natpermute (Suc n) (Suc k). Suc n \<notin> set xs}" and i: "i \<in> {0..k}"
-    {
-      assume c: "Suc n \<le> xs ! i"
+    have False if c: "Suc n \<le> xs ! i"
+    proof -
from xs i have "xs !i \<noteq> Suc n"
by (auto simp add: in_set_conv_nth natpermute_def)
with c have c': "Suc n < xs!i" by arith
@@ -1727,8 +1730,8 @@
unfolding eqs  setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)]
unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)]
by simp
-      finally have False using c' by simp
-    }
+      finally show ?thesis using c' by simp
+    qed
then show "((r, Suc k, a, xs!i), r, Suc k, a, Suc n) \<in> ?R"
apply auto
apply (metis not_less)
@@ -1775,7 +1778,7 @@

lemma natpermute_max_card:
assumes n0: "n \<noteq> 0"
-  shows "card {xs \<in> natpermute n (k+1). n \<in> set xs} = k + 1"
+  shows "card {xs \<in> natpermute n (k + 1). n \<in> set xs} = k + 1"
unfolding natpermute_contain_maximal
proof -
let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}"
@@ -1789,16 +1792,16 @@
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]"
+    have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]"
+    proof -
have "(replicate (k+1) 0 [i:=n] ! i) = n"
using i by (simp del: replicate.simps)
moreover
have "(replicate (k+1) 0 [j:=n] ! i) = 0"
using i ij by (simp del: replicate.simps)
-      ultimately have False
+      ultimately show ?thesis
using eq n0 by (simp del: replicate.simps)
-    }
+    qed
then show "{replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}"
by auto
qed
@@ -1811,10 +1814,11 @@
fixes a:: "'a::field_char_0 fps"
assumes a0: "a\$0 \<noteq> 0"
shows "(r (Suc k) (a\$0)) ^ Suc k = a\$0 \<longleftrightarrow> (fps_radical r (Suc k) a) ^ (Suc k) = a"
-proof -
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof
let ?r = "fps_radical r (Suc k) a"
-  {
-    assume r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0"
+  show ?rhs if r0: ?lhs
+  proof -
from a0 r0 have r00: "r (Suc k) (a\$0) \<noteq> 0" by auto
have "?r ^ Suc k \$ z = a\$z" for z
proof (induct z rule: nat_less_induct)
@@ -1865,17 +1869,16 @@
finally show ?thesis .
qed
qed
-    then have ?thesis using r0 by (simp add: fps_eq_iff)
-  }
-  moreover
-  {
-    assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a"
-    then have "((fps_radical r (Suc k) a) ^ (Suc k))\$0 = a\$0" by simp
-    then have "(r (Suc k) (a\$0)) ^ Suc k = a\$0"
+    then show ?thesis using r0 by (simp add: fps_eq_iff)
+  qed
+  show ?lhs if ?rhs
+  proof -
+    from that have "((fps_radical r (Suc k) a) ^ (Suc k))\$0 = a\$0"
+      by simp
+    then show ?thesis
unfolding fps_power_nth_Suc
by (simp add: setprod_constant del: replicate.simps)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

(*
@@ -2101,16 +2104,17 @@
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"
+    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)"
-    then have r0: "(r (k) ((a*b)\$0)) ^ k = (a*b)\$0"
+    fps_radical r k (a * b) = fps_radical r k a * fps_radical r k b"
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  show ?rhs if r0': ?lhs
+  proof -
+    from r0' have r0: "(r k ((a * b) \$ 0)) ^ k = (a * b) \$ 0"
by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib)
-    have ?thesis
+    show ?thesis
proof (cases k)
case 0
then show ?thesis using r0' by simp
@@ -2127,16 +2131,14 @@
show ?thesis
by (auto simp add: power_mult_distrib simp del: power_Suc)
qed
-  }
-  moreover
-  {
-    assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b"
-    then have "(fps_radical r k (a*b))\$0 = (fps_radical r k a * fps_radical r k b)\$0"
+  qed
+  show ?lhs if ?rhs
+  proof -
+    from that have "(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)"
+    then show ?thesis
using k by (simp add: fps_mult_nth)
-  }
-  ultimately show ?thesis by blast
+  qed
qed

(*
@@ -2182,7 +2184,8 @@
(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

@@ -3122,7 +3125,7 @@
show ?thesis by (simp add: fps_inverse_def)
qed

-text \<open>Vandermonde's Identity as a consequence\<close>
+text \<open>Vandermonde's Identity as a consequence.\<close>
lemma gbinomial_Vandermonde:
"setsum (\<lambda>k. (a gchoose k) * (b gchoose (n - k))) {0..n} = (a + b) gchoose n"
proof -
@@ -3162,9 +3165,14 @@
let ?p = "\<lambda>(x::'a). pochhammer (- x)"
from b have bn0: "?p b n \<noteq> 0"
unfolding pochhammer_eq_0_iff by simp
-  {
-    fix k
-    assume kn: "k \<in> {0..n}"
+  have th00:
+    "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)"
+      (is ?gchoose)
+    "pochhammer (1 + b - of_nat n) k \<noteq> 0"
+      (is ?pochhammer)
+    if kn: "k \<in> {0..n}" for k
+  proof -
have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0"
proof
assume "pochhammer (1 + b - of_nat n) n = 0"
@@ -3274,15 +3282,12 @@
finally show ?thesis by simp
qed
qed
-    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)"
-      "pochhammer (1 + b - of_nat n) k \<noteq> 0 "
+    then show ?gchoose and ?pochhammer
apply (cases "n = 0")
using nz'
apply auto
done
-  }
-  note th00 = this
+  qed
have "?r = ((a + b) gchoose n) * (of_nat (fact n) / (?m1 n * pochhammer (- b) n))"
unfolding gbinomial_pochhammer
using bn0 by (auto simp add: field_simps)
@@ -3308,7 +3313,8 @@
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
+  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)
apply (auto simp add: of_nat_diff algebra_simps)
@@ -3524,7 +3530,7 @@
done
qed

-text \<open>Connection to E c over the complex numbers --- Euler and De Moivre\<close>
+text \<open>Connection to E c over the complex numbers --- Euler and de Moivre.\<close>

lemma Eii_sin_cos: "E (ii * c) = fps_cos c + fps_const ii * fps_sin c"
(is "?l = ?r")```