# HG changeset patch # User wenzelm # Date 1434556324 -7200 # Node ID 839169c70e920c3991ed1244a8e79da63accbf22 # Parent 903bb14952397f21cd0998c791b08ff0767ee15e tuned proofs; diff -r 903bb1495239 -r 839169c70e92 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Wed Jun 17 11:03:05 2015 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Wed Jun 17 17:52:04 2015 +0200 @@ -2,12 +2,13 @@ Author: Amine Chaieb, University of Cambridge *) -section\A formalization of formal power series\ +section \A formalization of formal power series\ theory Formal_Power_Series imports Complex_Main begin + subsection \The type of formal power series\ typedef 'a fps = "{f :: nat \ 'a. True}" @@ -25,16 +26,13 @@ lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n" by (simp add: Abs_fps_inverse) -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 - -definition fps_zero_def: - "0 = Abs_fps (\n. 0)" - -instance .. + definition fps_zero_def: "0 = Abs_fps (\n. 0)" + instance .. end lemma fps_zero_nth [simp]: "0 $ n = 0" @@ -42,11 +40,8 @@ instantiation fps :: ("{one, zero}") one begin - -definition fps_one_def: - "1 = Abs_fps (\n. if n = 0 then 1 else 0)" - -instance .. + definition fps_one_def: "1 = Abs_fps (\n. if n = 0 then 1 else 0)" + instance .. end lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)" @@ -54,11 +49,8 @@ instantiation fps :: (plus) plus begin - -definition fps_plus_def: - "op + = (\f g. Abs_fps (\n. f $ n + g $ n))" - -instance .. + definition fps_plus_def: "op + = (\f g. Abs_fps (\n. f $ n + g $ n))" + instance .. end lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n" @@ -66,11 +58,8 @@ instantiation fps :: (minus) minus begin - -definition fps_minus_def: - "op - = (\f g. Abs_fps (\n. f $ n - g $ n))" - -instance .. + definition fps_minus_def: "op - = (\f g. Abs_fps (\n. f $ n - g $ n))" + instance .. end lemma fps_sub_nth [simp]: "(f - g) $ n = f $ n - g $ n" @@ -78,11 +67,8 @@ instantiation fps :: (uminus) uminus begin - -definition fps_uminus_def: - "uminus = (\f. Abs_fps (\n. - (f $ n)))" - -instance .. + definition fps_uminus_def: "uminus = (\f. Abs_fps (\n. - (f $ n)))" + instance .. end lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)" @@ -90,11 +76,8 @@ instantiation fps :: ("{comm_monoid_add, times}") times begin - -definition fps_times_def: - "op * = (\f g. Abs_fps (\n. \i=0..n. f $ i * g $ (n - i)))" - -instance .. + definition fps_times_def: "op * = (\f g. Abs_fps (\n. \i=0..n. f $ i * g $ (n - i)))" + instance .. end lemma fps_mult_nth: "(f * g) $ n = (\i=0..n. f$i * g$(n - i))" @@ -120,7 +103,8 @@ lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" by auto -subsection\Formal power series form a commutative ring with unity, if the range of sequences + +subsection \Formal power series form a commutative ring with unity, if the range of sequences they represent is a commutative ring with unity\ instance fps :: (semigroup_add) semigroup_add @@ -193,22 +177,28 @@ instance fps :: (semiring_1) monoid_mult proof fix a :: "'a fps" - show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) - show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') + show "1 * a = a" + by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) + show "a * 1 = a" + by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') qed instance fps :: (cancel_semigroup_add) cancel_semigroup_add proof fix a b c :: "'a fps" - { assume "a + b = a + c" then show "b = c" by (simp add: expand_fps_eq) } - { assume "b + a = c + a" then show "b = c" by (simp add: expand_fps_eq) } + show "b = c" if "a + b = a + c" + using that by (simp add: expand_fps_eq) + show "b = c" if "b + a = c + a" + using that by (simp add: expand_fps_eq) qed instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add proof fix a b c :: "'a fps" - show "a + b - a = b" by (simp add: expand_fps_eq) - show "a - b - c = a - (b + c)" by (simp add: expand_fps_eq diff_diff_eq) + show "a + b - a = b" + by (simp add: expand_fps_eq) + show "a - b - c = a - (b + c)" + by (simp add: expand_fps_eq diff_diff_eq) qed instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. @@ -242,32 +232,37 @@ instance fps :: (semiring_0) semiring_0 proof 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) + 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 instance fps :: (semiring_0_cancel) semiring_0_cancel .. + subsection \Selection of the nth power of the implicit variable in the infinite sum\ lemma fps_nonzero_nth: "f \ 0 \ (\ n. f $n \ 0)" by (simp add: expand_fps_eq) lemma fps_nonzero_nth_minimal: "f \ 0 \ (\n. f $ n \ 0 \ (\m < n. f $ m = 0))" + (is "?lhs \ ?rhs") proof let ?n = "LEAST n. f $ n \ 0" - assume "f \ 0" - then have "\n. f $ n \ 0" - by (simp add: fps_nonzero_nth) - then have "f $ ?n \ 0" - by (rule LeastI_ex) - moreover have "\m 0 \ (\mn. f $ n \ 0 \ (\mn. f $ n \ 0 \ (\m 0" by (auto simp add: expand_fps_eq) + show ?rhs if ?lhs + proof - + from that have "\n. f $ n \ 0" + by (simp add: fps_nonzero_nth) + then have "f $ ?n \ 0" + by (rule LeastI_ex) + moreover have "\m 0 \ (\m (\n. f $ n = g $n)" @@ -282,7 +277,8 @@ then show ?thesis by simp qed -subsection\Injection of the basic ring elements and multiplication by scalars\ + +subsection \Injection of the basic ring elements and multiplication by scalars\ definition "fps_const c = Abs_fps (\n. if n = 0 then c else 0)" @@ -329,6 +325,7 @@ lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))$n = f$n * c" by (simp add: fps_mult_nth mult_delta_right setsum.delta') + subsection \Formal power series form an integral domain\ instance fps :: (ring) ring .. @@ -342,24 +339,29 @@ instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors proof fix a b :: "'a fps" - assume a0: "a \ 0" and b0: "b \ 0" - then obtain i j where i: "a$i\0" "\k0" "\k 0" and "b \ 0" + then obtain i j where i: "a $ i \ 0" "\k 0" "\kk=0..i+j. a$k * b$(i+j-k))" + have "(a * b) $ (i + j) = (\k=0..i+j. a $ k * b $ (i + j - k))" by (rule fps_mult_nth) - also have "\ = (a$i * b$(i+j-i)) + (\k\{0..i+j}-{i}. a$k * b$(i+j-k))" + also have "\ = (a $ i * b $ (i + j - i)) + (\k\{0..i+j} - {i}. a $ k * b $ (i + j - k))" by (rule setsum.remove) simp_all - also have "(\k\{0..i+j}-{i}. a$k * b$(i+j-k)) = 0" - proof (rule setsum.neutral [rule_format]) - fix k assume "k \ {0..i+j} - {i}" - then have "k < i \ i+j-k < j" by auto - then show "a$k * b$(i+j-k) = 0" using i j by auto - qed - also have "a$i * b$(i+j-i) + 0 = a$i * b$j" by simp - also have "a$i * b$j \ 0" using i j by simp + also have "(\k\{0..i+j}-{i}. a $ k * b $ (i + j - k)) = 0" + proof (rule setsum.neutral [rule_format]) + fix k assume "k \ {0..i+j} - {i}" + then have "k < i \ i+j-k < j" + by auto + then show "a $ k * b $ (i + j - k) = 0" + using i j by auto + qed + also have "a $ i * b $ (i + j - i) + 0 = a $ i * b $ j" + by simp + also have "a $ i * b $ j \ 0" + using i j by simp finally have "(a*b) $ (i+j) \ 0" . - then show "a*b \ 0" unfolding fps_nonzero_nth by blast + then show "a * b \ 0" + unfolding fps_nonzero_nth by blast qed instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. @@ -373,7 +375,8 @@ lemma neg_numeral_fps_const: "- numeral k = fps_const (- numeral k)" by (simp only: numeral_fps_const fps_const_neg) -subsection\The eXtractor series X\ + +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 @@ -388,10 +391,12 @@ by (simp add: fps_mult_nth) also have "\ = f $ (n - 1)" using False by (simp add: X_def mult_delta_left setsum.delta) - finally show ?thesis using False by simp + finally show ?thesis + using False by simp next case True - then show ?thesis by (simp add: fps_mult_nth X_def) + then show ?thesis + by (simp add: fps_mult_nth X_def) qed lemma X_mult_right_nth[simp]: @@ -404,18 +409,18 @@ then show ?case by (simp add: X_def fps_eq_iff) next case (Suc k) - { - fix m - have "(X^Suc k) $ m = (if m = 0 then 0::'a else (X^k) $ (m - 1))" + have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" for m + proof - + have "(X^Suc k) $ m = (if m = 0 then 0 else (X^k) $ (m - 1))" by (simp del: One_nat_def) - then have "(X^Suc k) $ m = (if m = Suc k then 1::'a else 0)" + then show ?thesis using Suc.hyps by (auto cong del: if_weak_cong) - } - then show ?case by (simp add: fps_eq_iff) + qed + 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 @@ -428,7 +433,7 @@ by (metis X_power_mult_nth mult.commute) -subsection\Formal Power series form a metric space\ +subsection \Formal Power series form a metric space\ definition (in dist) "ball x r = {y. dist y x < r}" @@ -460,59 +465,49 @@ instance proof - fix S :: "'a fps set" - show "open S = (\x\S. \e>0. \y. dist y x < e \ y \ S)" + show "open S = (\x\S. \e>0. \y. dist y x < e \ y \ S)" for S :: "'a fps set" by (auto simp add: open_fps_def ball_def subset_eq) -next - { - fix a b :: "'a fps" - { - assume "a = b" - then have "\ (\n. a $ n \ 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 "\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 \ a = b" by blast - } - note th = this - from th have th'[simp]: "\a::'a fps. dist a a = 0" by simp + show th: "dist a b = 0 \ a = b" for a b :: "'a fps" + proof + assume "a = b" + then have "\ (\n. a $ n \ b $ n)" by simp + then show "dist a b = 0" by (simp add: dist_fps_def) + next + assume d: "dist a b = 0" + then have "\n. a$n = b$n" + by - (rule ccontr, simp add: dist_fps_def) + then show "a = b" by (simp add: fps_eq_iff) + qed + then have th'[simp]: "dist a a = 0" for a :: "'a fps" + by simp + fix a b c :: "'a fps" - { - assume "a = b" + consider "a = b" | "c = a \ c = b" | "a \ b" "a \ c" "b \ c" by blast + then show "dist a b \ dist a c + dist b c" + proof cases + case 1 then have "dist a b = 0" unfolding th . - then have "dist a b \ dist a c + dist b c" + then show ?thesis using dist_fps_ge0 [of a c] dist_fps_ge0 [of b c] by simp - } - moreover - { - assume "c = a \ c = b" - then have "dist a b \ dist a c + dist b c" + next + case 2 + then show ?thesis by (cases "c = a") (simp_all add: th dist_fps_sym) - } - moreover - { - assume ab: "a \ b" and ac: "a \ c" and bc: "b \ c" + next + case 3 def n \ "\a b::'a fps. LEAST n. a$n \ b$n" then have n': "\m a b. m < n a b \ a$m = b$m" by (auto dest: not_less_Least) - - from ab ac bc - have dab: "dist a b = inverse (2 ^ n a b)" + from 3 have dab: "dist a b = inverse (2 ^ n a b)" and dac: "dist a c = inverse (2 ^ n a c)" and dbc: "dist b c = inverse (2 ^ n b c)" by (simp_all add: dist_fps_def n_def fps_eq_iff) - from ab ac bc have nz: "dist a b \ 0" "dist a c \ 0" "dist b c \ 0" + from 3 have nz: "dist a b \ 0" "dist a c \ 0" "dist b c \ 0" unfolding th by simp_all from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] by auto - have th1: "\n. (2::real)^n >0" by auto + have th1: "\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" @@ -522,18 +517,17 @@ from n'[OF gtn(2)] n'(1)[OF gtn(1)] have "a $ n a b = b $ n a b" by simp moreover have "a $ n a b \ b $ n a b" - unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff) + unfolding n_def by (rule LeastI_ex) (insert \a \ b\, simp add: fps_eq_iff) ultimately have False by contradiction } - then have "dist a b \ dist a c + dist b c" + then show ?thesis by (auto simp add: not_le[symmetric]) - } - ultimately show "dist a b \ dist a c + dist b c" by blast + qed qed end -text\The infinite sums and justification of the notation in textbooks\ +text \The infinite sums and justification of the notation in textbooks\ lemma reals_power_lt_ex: fixes x y :: real @@ -584,51 +578,48 @@ proof - { fix r :: real - assume rp: "r > 0" - have th0: "(2::real) > 1" by simp - from reals_power_lt_ex[OF rp th0] - obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast - { - fix n :: nat - assume nn0: "n \ n0" - then have thnn0: "(1/2)^n \ (1/2 :: real)^n0" - by (simp add: divide_simps) - { - assume "?s n = a" - then have "dist (?s n) a < r" - unfolding dist_eq_0_iff[of "?s n" a, symmetric] - using rp by (simp del: dist_eq_0_iff) - } - moreover + assume "r > 0" + obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" + using reals_power_lt_ex[OF \r > 0\, of 2] by auto + have "\n0. \n \ n0. dist (?s n) a < r" + proof - { - assume neq: "?s n \ a" - def k \ "LEAST i. ?s n $ i \ a $ i" - from neq have dth: "dist (?s n) a = (1/2)^k" - by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) - - from neq have kn: "k > n" - by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff + fix n :: nat + assume nn0: "n \ n0" + then have thnn0: "(1/2)^n \ (1/2 :: real)^n0" + by (simp add: divide_simps) + have "dist (?s n) a < r" + proof (cases "?s n = a") + case True + then show ?thesis + unfolding dist_eq_0_iff[of "?s n" a, symmetric] + using \r > 0\ by (simp del: dist_eq_0_iff) + next + case False + def k \ "LEAST i. ?s n $ i \ a $ i" + from False have dth: "dist (?s n) a = (1/2)^k" + by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) + from False have kn: "k > n" + by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff split: split_if_asm intro: LeastI2_ex) - then have "dist (?s n) a < (1/2)^n" - unfolding dth by (simp add: divide_simps) - also have "\ \ (1/2)^n0" - using nn0 by (simp add: divide_simps) - also have "\ < r" - using n0 by simp - finally have "dist (?s n) a < r" . + then have "dist (?s n) a < (1/2)^n" + unfolding dth by (simp add: divide_simps) + also have "\ \ (1/2)^n0" + using nn0 by (simp add: divide_simps) + also have "\ < r" + using n0 by simp + finally show ?thesis . + qed } - ultimately have "dist (?s n) a < r" - by blast - } - then have "\n0. \ n \ n0. dist (?s n) a < r" - by blast + then show ?thesis by blast + qed } then show ?thesis unfolding lim_sequentially by blast qed -subsection\Inverses of formal power series\ +subsection \Inverses of formal power series\ declare setsum.cong[fundef_cong] @@ -640,11 +631,9 @@ "natfun_inverse f 0 = inverse (f$0)" | "natfun_inverse f n = - inverse (f$0) * setsum (\i. f$i * natfun_inverse f (n - i)) {1..n}" -definition - fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" - -definition - fps_divide_def: "divide = (\(f::'a fps) g. f * inverse g)" +definition fps_inverse_def: "inverse f = (if f $ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" + +definition fps_divide_def: "divide = (\(f::'a fps) g. f * inverse g)" instance .. @@ -670,9 +659,8 @@ by (simp add: fps_inverse_def) from f0 have th0: "(inverse f * f) $ 0 = 1" by (simp add: fps_mult_nth fps_inverse_def) - { - fix n :: nat - assume np: "n > 0" + have "(inverse f * f)$n = 0" if np: "n > 0" for n + proof - from np have eq: "{0..n} = {0} \ {1 .. n}" by auto have d: "{0} \ {1 .. n} = {}" @@ -689,31 +677,26 @@ by (simp add: eq) also have "\ = 0" unfolding th1 ifn by simp - finally have "(inverse f * f)$n = 0" - unfolding c . - } + finally show ?thesis unfolding c . + qed with th0 show ?thesis by (simp add: fps_eq_iff) qed -lemma fps_inverse_0_iff[simp]: "(inverse f)$0 = (0::'a::division_ring) \ f$0 = 0" +lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \ f $ 0 = 0" by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) -lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \ f $0 = 0" -proof - - { - assume "f $ 0 = 0" - then have "inverse f = 0" - by (simp add: fps_inverse_def) - } - moreover - { - assume h: "inverse f = 0" +lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \ f $ 0 = 0" + (is "?lhs \ ?rhs") +proof + show ?lhs if ?rhs + using that by (simp add: fps_inverse_def) + show ?rhs if h: ?lhs + proof (rule ccontr) assume c: "f $0 \ 0" - from inverse_mult_eq_1[OF c] h have False + from inverse_mult_eq_1[OF c] h show False by simp - } - ultimately show ?thesis by blast + qed qed lemma fps_inverse_idempotent[intro]: @@ -771,8 +754,8 @@ done qed -lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) - = Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" +lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) = + Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" apply (rule fps_inverse_unique) apply (simp_all add: fps_eq_iff fps_mult_nth setsum_zero_lemma) done @@ -872,24 +855,27 @@ lemma fps_deriv_eq_0_iff [simp]: "fps_deriv f = 0 \ f = fps_const (f$0 :: 'a::{idom,semiring_char_0})" -proof - - { - assume "f = fps_const (f$0)" - then have "fps_deriv f = fps_deriv (fps_const (f$0))" by simp - then have "fps_deriv f = 0" by simp - } - moreover - { - assume z: "fps_deriv f = 0" - then have "\n. (fps_deriv f)$n = 0" by simp - then have "\n. f$(n+1) = 0" by (simp del: of_nat_Suc of_nat_add One_nat_def) - then have "f = fps_const (f$0)" + (is "?lhs \ ?rhs") +proof + show ?lhs if ?rhs + proof - + from that have "fps_deriv f = fps_deriv (fps_const (f$0))" + by simp + then show ?thesis + by simp + qed + show ?rhs if ?lhs + proof - + from that have "\n. (fps_deriv f)$n = 0" + by simp + then have "\n. f$(n+1) = 0" + by (simp del: of_nat_Suc of_nat_add One_nat_def) + then show ?thesis apply (clarsimp simp add: fps_eq_iff fps_const_def) apply (erule_tac x="n - 1" in allE) apply simp done - } - ultimately show ?thesis by blast + qed qed lemma fps_deriv_eq_iff: @@ -900,7 +886,8 @@ by simp also have "\ \ f - g = fps_const ((f - g) $ 0)" unfolding fps_deriv_eq_0_iff .. - finally show ?thesis by (simp add: field_simps) + finally show ?thesis + by (simp add: field_simps) qed lemma fps_deriv_eq_iff_ex: @@ -977,9 +964,8 @@ then show ?case by simp next case (Suc n) - note h = Suc.hyps[OF \a$0 = 1\] show ?case unfolding power_Suc fps_mult_nth - using h \a$0 = 1\ fps_power_zeroth_eq_one[OF \a$0=1\] + using Suc.hyps[OF \a$0 = 1\] \a$0 = 1\ fps_power_zeroth_eq_one[OF \a$0=1\] by (simp add: field_simps) qed @@ -1000,53 +986,41 @@ done lemma startsby_zero_power_prefix: - assumes a0: "a $0 = (0::'a::idom)" + assumes a0: "a $ 0 = (0::'a::idom)" shows "\n < k. a ^ k $ n = 0" using a0 proof (induct k rule: nat_less_induct) fix k assume H: "\m (\n 0" - have "a ^k $ m = (a^l * a) $m" - by (simp add: k mult.commute) - also have "\ = (\i = 0..m. a ^ l $ i * a $ (m - i))" - by (simp add: fps_mult_nth) - also have "\ = 0" - apply (rule setsum.neutral) - apply auto - apply (case_tac "x = m") - using a0 apply simp - apply (rule H[rule_format]) - using a0 k mk apply auto - done - finally have "a^k $ m = 0" . - } - ultimately have "a^k $ m = 0" - by blast - } - then have ?ths by blast - } - ultimately show ?ths - by (cases k) auto + show "\m = (\i = 0..m. a ^ l $ i * a $ (m - i))" + by (simp add: fps_mult_nth) + also have "\ = 0" + apply (rule setsum.neutral) + apply auto + apply (case_tac "x = m") + using a0 apply simp + apply (rule H[rule_format]) + using a0 Suc mk apply auto + done + finally show ?thesis . + qed + then show ?thesis by blast + qed qed lemma startsby_zero_setsum_depends: @@ -1089,37 +1063,31 @@ lemma fps_inverse_power: fixes a :: "'a::field fps" shows "inverse (a^n) = inverse a ^ n" -proof - - { - assume a0: "a$0 = 0" - then have eq: "inverse a = 0" +proof (cases "a$0 = 0") + case True + then have eq: "inverse a = 0" + by (simp add: fps_inverse_def) + consider "n = 0" | "n > 0" by blast + then show ?thesis + proof cases + case 1 + then show ?thesis by simp + next + case 2 + from startsby_zero_power[OF True 2] eq show ?thesis by (simp add: fps_inverse_def) - { - assume "n = 0" - then have ?thesis by simp - } - moreover - { - assume n: "n > 0" - from startsby_zero_power[OF a0 n] eq a0 n have ?thesis - by (simp add: fps_inverse_def) - } - ultimately have ?thesis by blast - } - moreover - { - assume a0: "a$0 \ 0" - have ?thesis - apply (rule fps_inverse_unique) - apply (simp add: a0) - unfolding power_mult_distrib[symmetric] - apply (rule ssubst[where t = "a * inverse a" and s= 1]) - apply simp_all - apply (subst mult.commute) - apply (rule inverse_mult_eq_1[OF a0]) - done - } - ultimately show ?thesis by blast + qed +next + case False + show ?thesis + apply (rule fps_inverse_unique) + apply (simp add: False) + unfolding power_mult_distrib[symmetric] + apply (rule ssubst[where t = "a * inverse a" and s= 1]) + apply simp_all + apply (subst mult.commute) + apply (rule inverse_mult_eq_1[OF False]) + done qed lemma fps_deriv_power: @@ -1158,35 +1126,42 @@ fixes a :: "'a::field fps" shows "inverse (a * b) = inverse a * inverse b" proof - - { - assume a0: "a$0 = 0" - then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) - from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all - have ?thesis unfolding th by simp - } - moreover - { - assume b0: "b$0 = 0" - then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) - from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all - have ?thesis unfolding th by simp - } - moreover - { - assume a0: "a$0 \ 0" and b0: "b$0 \ 0" - from a0 b0 have ab0:"(a*b) $ 0 \ 0" by (simp add: fps_mult_nth) + consider "a $ 0 = 0" | "b $ 0 = 0" | "a $ 0 \ 0" "b $ 0 \ 0" + by blast + then show ?thesis + proof cases + case 1 + then have "(a * b) $ 0 = 0" + by (simp add: fps_mult_nth) + with 1 have th: "inverse a = 0" "inverse (a * b) = 0" + by simp_all + show ?thesis + unfolding th by simp + next + case 2 + then have "(a * b) $ 0 = 0" + by (simp add: fps_mult_nth) + with 2 have th: "inverse b = 0" "inverse (a * b) = 0" + by simp_all + show ?thesis + unfolding th by simp + next + case 3 + then have ab0:"(a * b) $ 0 \ 0" + by (simp add: fps_mult_nth) from inverse_mult_eq_1[OF ab0] - have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp + have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" + by simp then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" by (simp add: field_simps) - then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp - } - ultimately show ?thesis by blast + then show ?thesis + using inverse_mult_eq_1[OF \a $ 0 \ 0\] inverse_mult_eq_1[OF \b $ 0 \ 0\] by simp + qed qed lemma fps_inverse_deriv': fixes a :: "'a::field fps" - assumes a0: "a$0 \ 0" + assumes a0: "a $ 0 \ 0" shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2" using fps_inverse_deriv[OF a0] unfolding power2_eq_square fps_divide_def fps_inverse_mult @@ -1212,9 +1187,8 @@ lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" by (cases n) simp_all - -lemma fps_inverse_X_plus1: - "inverse (1 + X) = Abs_fps (\n. (- (1::'a::field)) ^ n)" (is "_ = ?r") +lemma fps_inverse_X_plus1: "inverse (1 + X) = Abs_fps (\n. (- (1::'a::field)) ^ n)" + (is "_ = ?r") proof - have eq: "(1 + X) * ?r = 1" unfolding minus_one_power_iff @@ -1224,7 +1198,7 @@ qed -subsection\Integration\ +subsection \Integration\ definition fps_integral :: "'a::field_char_0 fps \ 'a \ 'a fps" where "fps_integral a a0 = Abs_fps (\n. if n = 0 then a0 else (a$(n - 1) / of_nat n))" @@ -1249,7 +1223,7 @@ subsection \Composition of FPSs\ -definition fps_compose :: "'a::semiring_1 fps \ 'a fps \ 'a fps" (infixl "oo" 55) +definition fps_compose :: "'a::semiring_1 fps \ 'a fps \ 'a fps" (infixl "oo" 55) where "a oo b = Abs_fps (\n. setsum (\i. a$i * (b^i$n)) {0..n})" lemma fps_compose_nth: "(a oo b)$n = setsum (\i. a$i * (b^i$n)) {0..n}" @@ -1258,8 +1232,7 @@ 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') -lemma fps_const_compose[simp]: - "fps_const (a::'a::comm_ring_1) oo b = fps_const a" +lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a" by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum.delta) lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k" @@ -1282,33 +1255,36 @@ Abs_fps a - setsum (\i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}" (is "?lhs = ?rhs") proof - - { fix n :: nat + have "?lhs $ n = ?rhs $ n" for n :: nat + proof - have "?lhs $ n = (if n < Suc k then 0 else a n)" unfolding X_power_mult_nth by auto also have "\ = ?rhs $ n" proof (induct k) case 0 - then show ?case by (simp add: fps_setsum_nth) + then show ?case + by (simp add: fps_setsum_nth) next case (Suc k) - note th = Suc.hyps[symmetric] have "(Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = (Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) $ n" by (simp add: field_simps) also have "\ = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n" - using th unfolding fps_sub_nth by simp + using Suc.hyps[symmetric] unfolding fps_sub_nth by simp also have "\ = (if n < Suc (Suc k) then 0 else a n)" unfolding X_power_mult_right_nth apply (auto simp add: not_less fps_const_def) apply (rule cong[of a a, OF refl]) apply arith done - finally show ?case by simp + finally show ?case + by simp qed - finally have "?lhs $ n = ?rhs $ n" . - } - then show ?thesis by (simp add: fps_eq_iff) + finally show ?thesis . + qed + then show ?thesis + by (simp add: fps_eq_iff) qed @@ -1338,13 +1314,15 @@ lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\n. of_nat n* a$n)" by (simp add: fps_eq_iff) - lemma fps_mult_XD_shift: "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\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 3\ + +text \Rule 3 is trivial and is given by @{text fps_times_def}.\ + subsubsection \Rule 5 --- summation and "division" by (1 - X)\ @@ -1354,39 +1332,33 @@ let ?sa = "Abs_fps (\n. setsum (\i. a $ i) {0..n})" have th0: "\i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" by simp - { - fix n :: nat - { - assume "n = 0" - then have "a $ n = ((1 - X) * ?sa) $ n" - by (simp add: fps_mult_nth) - } - moreover - { - assume n0: "n \ 0" - then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1} \ {2..n} = {1..n}" - "{0..n - 1} \ {n} = {0..n}" - by (auto simp: set_eq_iff) - have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" "{0..n - 1} \ {n} = {}" - using n0 by simp_all - have f: "finite {0}" "finite {1}" "finite {2 .. n}" - "finite {0 .. n - 1}" "finite {n}" by simp_all - have "((1 - X) * ?sa) $ n = setsum (\i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}" - by (simp add: fps_mult_nth) - also have "\ = a$n" - unfolding th0 - unfolding setsum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] - unfolding setsum.union_disjoint[OF f(2) f(3) d(2)] - apply (simp) - unfolding setsum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] - apply simp - done - finally have "a$n = ((1 - X) * ?sa) $ n" - by simp - } - ultimately have "a$n = ((1 - X) * ?sa) $ n" - by blast - } + have "a$n = ((1 - X) * ?sa) $ n" for n + proof (cases "n = 0") + case True + then show ?thesis + by (simp add: fps_mult_nth) + next + case False + then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1} \ {2..n} = {1..n}" + "{0..n - 1} \ {n} = {0..n}" + by (auto simp: set_eq_iff) + have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" "{0..n - 1} \ {n} = {}" + using False by simp_all + have f: "finite {0}" "finite {1}" "finite {2 .. n}" + "finite {0 .. n - 1}" "finite {n}" by simp_all + have "((1 - X) * ?sa) $ n = setsum (\i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}" + by (simp add: fps_mult_nth) + also have "\ = a$n" + unfolding th0 + unfolding setsum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] + unfolding setsum.union_disjoint[OF f(2) f(3) d(2)] + apply (simp) + unfolding setsum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] + apply simp + done + finally show ?thesis + by simp + qed then show ?thesis unfolding fps_eq_iff by blast qed @@ -1407,7 +1379,7 @@ qed -subsubsection\Rule 4 in its more general form: generalizes Rule 3 for an arbitrary +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\ definition "natpermute n k = {l :: nat list. length l = k \ listsum l = n}" @@ -1631,7 +1603,7 @@ qed qed -text\The special form for powers\ +text \The special form for powers\ lemma fps_power_nth_Suc: fixes m :: nat and a :: "'a::comm_ring_1 fps" @@ -1672,30 +1644,28 @@ shows "(b oo a = c oo a) \ b = c" (is "?lhs \?rhs") proof - assume ?rhs - then show "?lhs" by simp -next - assume h: ?lhs - { - fix n - have "b$n = c$n" + show ?lhs if ?rhs using that by simp + show ?rhs if ?lhs + proof - + have "b$n = c$n" for n proof (induct n rule: nat_less_induct) fix n assume H: "\m?lhs\ have "(b oo a)$n = (c oo a)$n" + by simp + then show ?thesis + using 0 by (simp add: fps_compose_nth) + next + case (Suc n1) have f: "finite {0 .. n1}" "finite {n}" by simp_all - have eq: "{0 .. n1} \ {n} = {0 .. n}" using n1 by auto - have d: "{0 .. n1} \ {n} = {}" using n1 by auto + have eq: "{0 .. n1} \ {n} = {0 .. n}" using Suc by auto + have d: "{0 .. n1} \ {n} = {}" using Suc by auto have seq: "(\i = 0..n1. b $ i * a ^ i $ n) = (\i = 0..n1. c $ i * a ^ i $ n)" apply (rule setsum.cong) - using H n1 + using H Suc apply auto done have th0: "(b oo a) $n = (\i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" @@ -1706,12 +1676,12 @@ unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] 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 - qed} - then show ?rhs by (simp add: fps_eq_iff) + from \?lhs\[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 + show ?thesis by auto + qed + qed + then show ?rhs by (simp add: fps_eq_iff) + qed qed @@ -1777,7 +1747,7 @@ apply auto done -lemma fps_radical_nth_0[simp]: "fps_radical r n a $ 0 = (if n=0 then 1 else r n (a$0))" +lemma fps_radical_nth_0[simp]: "fps_radical r n a $ 0 = (if n = 0 then 1 else r n (a$0))" by (cases n) (simp_all add: fps_radical_def) lemma fps_radical_power_nth[simp]: @@ -1797,8 +1767,10 @@ apply (subgoal_tac "replicate k 0 ! x = 0") apply (auto intro: nth_replicate simp del: replicate.simps) done - also have "\ = a$0" using r Suc by (simp add: setprod_constant) - finally show ?thesis using Suc by simp + also have "\ = a$0" + using r Suc by (simp add: setprod_constant) + finally show ?thesis + using Suc by simp qed lemma natpermute_max_card: @@ -1806,15 +1778,17 @@ shows "card {xs \ natpermute n (k+1). n \ set xs} = k + 1" unfolding natpermute_contain_maximal proof - - let ?A= "\i. {replicate (k + 1) 0[i := n]}" + let ?A = "\i. {replicate (k + 1) 0[i := n]}" let ?K = "{0 ..k}" - have fK: "finite ?K" by simp - have fAK: "\i\?K. finite (?A i)" by auto + have fK: "finite ?K" + by simp + have fAK: "\i\?K. finite (?A i)" + by auto have d: "\i\ ?K. \j\ ?K. i \ j \ {replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" proof clarify fix i j - assume i: "i \ ?K" and j: "j\ ?K" and ij: "i\j" + assume i: "i \ ?K" and j: "j \ ?K" and ij: "i \ j" { assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" have "(replicate (k+1) 0 [i:=n] ! i) = n" @@ -1842,60 +1816,55 @@ { assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" from a0 r0 have r00: "r (Suc k) (a$0) \ 0" by auto - { - fix z - have "?r ^ Suc k $ z = a$z" - proof (induct z rule: nat_less_induct) - fix n - assume H: "\m 0" using n1 by arith - let ?Pnk = "natpermute n (k + 1)" - let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" - let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" - have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast - have d: "?Pnkn \ ?Pnknn = {}" by blast - have f: "finite ?Pnkn" "finite ?Pnknn" - using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] - by (metis natpermute_finite)+ - let ?f = "\v. \j\{0..k}. ?r $ v ! j" - have "setsum ?f ?Pnkn = setsum (\v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" - proof (rule setsum.cong) - fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" - let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = - fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" - from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" - unfolding natpermute_contain_maximal by auto - have "(\j\{0..k}. fps_radical r (Suc k) a $ v ! j) = - (\j\{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" - apply (rule setprod.cong, simp) - using i r0 - apply (simp del: replicate.simps) - done - also have "\ = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" - using i r0 by (simp add: setprod_gen_delta) - finally show ?ths . - qed rule - then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" - by (simp add: natpermute_max_card[OF nz, simplified]) - also have "\ = a$n - setsum ?f ?Pnknn" - unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc) - finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . - have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" - unfolding fps_power_nth_Suc setsum.union_disjoint[OF f d, unfolded eq] .. - also have "\ = a$n" unfolding fn by simp - finally have "?r ^ Suc k $ n = a $n" . - } - ultimately show "?r ^ Suc k $ n = a $n" by (cases n) auto + have "?r ^ Suc k $ z = a$z" for z + proof (induct z rule: nat_less_induct) + fix n + assume H: "\