summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

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 by (auto simp add: not_le[symmetric]) 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" by (simp add: divide_simps) - 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 +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 @@ by (simp add: natpermute_def) from ys have ys': "listsum ys = n - m" by (simp add: natpermute_def) - have "l \<in> ?L" using leq xs ys h + show "l \<in> ?L" using leq xs ys h apply (clarsimp simp add: natpermute_def) 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> - fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" -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")