src/HOL/Computational_Algebra/Formal_Power_Series.thy
 author wenzelm Wed Nov 01 20:46:23 2017 +0100 (22 months ago) changeset 66983 df83b66f1d94 parent 66817 0b12755ccbb2 child 67399 eab6ce8368fa permissions -rw-r--r--
proper merge (amending fb46c031c841);
 wenzelm@65435 ` 1` ```(* Title: HOL/Computational_Algebra/Formal_Power_Series.thy ``` chaieb@29687 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29687 ` 3` ```*) ``` chaieb@29687 ` 4` wenzelm@60501 ` 5` ```section \A formalization of formal power series\ ``` chaieb@29687 ` 6` chaieb@29687 ` 7` ```theory Formal_Power_Series ``` haftmann@65417 ` 8` ```imports ``` haftmann@65417 ` 9` ``` Complex_Main ``` haftmann@65417 ` 10` ``` Euclidean_Algorithm ``` chaieb@29687 ` 11` ```begin ``` chaieb@29687 ` 12` wenzelm@60501 ` 13` wenzelm@60500 ` 14` ```subsection \The type of formal power series\ ``` chaieb@29687 ` 15` wenzelm@49834 ` 16` ```typedef 'a fps = "{f :: nat \ 'a. True}" ``` huffman@29911 ` 17` ``` morphisms fps_nth Abs_fps ``` chaieb@29687 ` 18` ``` by simp ``` chaieb@29687 ` 19` huffman@29911 ` 20` ```notation fps_nth (infixl "\$" 75) ``` huffman@29911 ` 21` huffman@29911 ` 22` ```lemma expand_fps_eq: "p = q \ (\n. p \$ n = q \$ n)" ``` nipkow@39302 ` 23` ``` by (simp add: fps_nth_inject [symmetric] fun_eq_iff) ``` huffman@29911 ` 24` huffman@29911 ` 25` ```lemma fps_ext: "(\n. p \$ n = q \$ n) \ p = q" ``` huffman@29911 ` 26` ``` by (simp add: expand_fps_eq) ``` huffman@29911 ` 27` huffman@29911 ` 28` ```lemma fps_nth_Abs_fps [simp]: "Abs_fps f \$ n = f n" ``` huffman@29911 ` 29` ``` by (simp add: Abs_fps_inverse) ``` huffman@29911 ` 30` wenzelm@60501 ` 31` ```text \Definition of the basic elements 0 and 1 and the basic operations of addition, ``` wenzelm@60501 ` 32` ``` negation and multiplication.\ ``` chaieb@29687 ` 33` haftmann@36409 ` 34` ```instantiation fps :: (zero) zero ``` chaieb@29687 ` 35` ```begin ``` wenzelm@60501 ` 36` ``` definition fps_zero_def: "0 = Abs_fps (\n. 0)" ``` wenzelm@60501 ` 37` ``` instance .. ``` chaieb@29687 ` 38` ```end ``` chaieb@29687 ` 39` huffman@29911 ` 40` ```lemma fps_zero_nth [simp]: "0 \$ n = 0" ``` huffman@29911 ` 41` ``` unfolding fps_zero_def by simp ``` huffman@29911 ` 42` haftmann@36409 ` 43` ```instantiation fps :: ("{one, zero}") one ``` chaieb@29687 ` 44` ```begin ``` wenzelm@60501 ` 45` ``` definition fps_one_def: "1 = Abs_fps (\n. if n = 0 then 1 else 0)" ``` wenzelm@60501 ` 46` ``` instance .. ``` chaieb@29687 ` 47` ```end ``` chaieb@29687 ` 48` huffman@30488 ` 49` ```lemma fps_one_nth [simp]: "1 \$ n = (if n = 0 then 1 else 0)" ``` huffman@29911 ` 50` ``` unfolding fps_one_def by simp ``` huffman@29911 ` 51` wenzelm@54681 ` 52` ```instantiation fps :: (plus) plus ``` chaieb@29687 ` 53` ```begin ``` wenzelm@60501 ` 54` ``` definition fps_plus_def: "op + = (\f g. Abs_fps (\n. f \$ n + g \$ n))" ``` wenzelm@60501 ` 55` ``` instance .. ``` chaieb@29687 ` 56` ```end ``` chaieb@29687 ` 57` huffman@29911 ` 58` ```lemma fps_add_nth [simp]: "(f + g) \$ n = f \$ n + g \$ n" ``` huffman@29911 ` 59` ``` unfolding fps_plus_def by simp ``` huffman@29911 ` 60` huffman@29911 ` 61` ```instantiation fps :: (minus) minus ``` chaieb@29687 ` 62` ```begin ``` wenzelm@60501 ` 63` ``` definition fps_minus_def: "op - = (\f g. Abs_fps (\n. f \$ n - g \$ n))" ``` wenzelm@60501 ` 64` ``` instance .. ``` chaieb@29687 ` 65` ```end ``` chaieb@29687 ` 66` huffman@29911 ` 67` ```lemma fps_sub_nth [simp]: "(f - g) \$ n = f \$ n - g \$ n" ``` huffman@29911 ` 68` ``` unfolding fps_minus_def by simp ``` huffman@29911 ` 69` huffman@29911 ` 70` ```instantiation fps :: (uminus) uminus ``` chaieb@29687 ` 71` ```begin ``` wenzelm@60501 ` 72` ``` definition fps_uminus_def: "uminus = (\f. Abs_fps (\n. - (f \$ n)))" ``` wenzelm@60501 ` 73` ``` instance .. ``` chaieb@29687 ` 74` ```end ``` chaieb@29687 ` 75` huffman@29911 ` 76` ```lemma fps_neg_nth [simp]: "(- f) \$ n = - (f \$ n)" ``` huffman@29911 ` 77` ``` unfolding fps_uminus_def by simp ``` huffman@29911 ` 78` wenzelm@54681 ` 79` ```instantiation fps :: ("{comm_monoid_add, times}") times ``` chaieb@29687 ` 80` ```begin ``` wenzelm@60501 ` 81` ``` definition fps_times_def: "op * = (\f g. Abs_fps (\n. \i=0..n. f \$ i * g \$ (n - i)))" ``` wenzelm@60501 ` 82` ``` instance .. ``` chaieb@29687 ` 83` ```end ``` chaieb@29687 ` 84` huffman@29911 ` 85` ```lemma fps_mult_nth: "(f * g) \$ n = (\i=0..n. f\$i * g\$(n - i))" ``` huffman@29911 ` 86` ``` unfolding fps_times_def by simp ``` chaieb@29687 ` 87` eberlm@61608 ` 88` ```lemma fps_mult_nth_0 [simp]: "(f * g) \$ 0 = f \$ 0 * g \$ 0" ``` eberlm@61608 ` 89` ``` unfolding fps_times_def by simp ``` eberlm@61608 ` 90` wenzelm@52891 ` 91` ```declare atLeastAtMost_iff [presburger] ``` wenzelm@52891 ` 92` ```declare Bex_def [presburger] ``` wenzelm@52891 ` 93` ```declare Ball_def [presburger] ``` chaieb@29687 ` 94` huffman@29913 ` 95` ```lemma mult_delta_left: ``` huffman@29913 ` 96` ``` fixes x y :: "'a::mult_zero" ``` huffman@29913 ` 97` ``` shows "(if b then x else 0) * y = (if b then x * y else 0)" ``` huffman@29913 ` 98` ``` by simp ``` huffman@29913 ` 99` huffman@29913 ` 100` ```lemma mult_delta_right: ``` huffman@29913 ` 101` ``` fixes x y :: "'a::mult_zero" ``` huffman@29913 ` 102` ``` shows "x * (if b then y else 0) = (if b then x * y else 0)" ``` huffman@29913 ` 103` ``` by simp ``` huffman@29913 ` 104` chaieb@29687 ` 105` ```lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" ``` chaieb@29687 ` 106` ``` by auto ``` wenzelm@52891 ` 107` chaieb@29687 ` 108` ```lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" ``` chaieb@29687 ` 109` ``` by auto ``` chaieb@29687 ` 110` wenzelm@60501 ` 111` wenzelm@60501 ` 112` ```subsection \Formal power series form a commutative ring with unity, if the range of sequences ``` wenzelm@60500 ` 113` ``` they represent is a commutative ring with unity\ ``` chaieb@29687 ` 114` huffman@29911 ` 115` ```instance fps :: (semigroup_add) semigroup_add ``` chaieb@29687 ` 116` ```proof ``` wenzelm@52891 ` 117` ``` fix a b c :: "'a fps" ``` wenzelm@52891 ` 118` ``` show "a + b + c = a + (b + c)" ``` haftmann@57512 ` 119` ``` by (simp add: fps_ext add.assoc) ``` huffman@29911 ` 120` ```qed ``` huffman@29911 ` 121` huffman@29911 ` 122` ```instance fps :: (ab_semigroup_add) ab_semigroup_add ``` huffman@29911 ` 123` ```proof ``` wenzelm@52891 ` 124` ``` fix a b :: "'a fps" ``` wenzelm@52891 ` 125` ``` show "a + b = b + a" ``` haftmann@57512 ` 126` ``` by (simp add: fps_ext add.commute) ``` chaieb@29687 ` 127` ```qed ``` chaieb@29687 ` 128` huffman@29911 ` 129` ```lemma fps_mult_assoc_lemma: ``` wenzelm@53195 ` 130` ``` fixes k :: nat ``` wenzelm@53195 ` 131` ``` and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" ``` huffman@29911 ` 132` ``` shows "(\j=0..k. \i=0..j. f i (j - i) (n - j)) = ``` huffman@29911 ` 133` ``` (\j=0..k. \i=0..k - j. f j i (n - j - i))" ``` nipkow@64267 ` 134` ``` by (induct k) (simp_all add: Suc_diff_le sum.distrib add.assoc) ``` chaieb@29687 ` 135` huffman@29911 ` 136` ```instance fps :: (semiring_0) semigroup_mult ``` chaieb@29687 ` 137` ```proof ``` chaieb@29687 ` 138` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 139` ``` show "(a * b) * c = a * (b * c)" ``` huffman@29911 ` 140` ``` proof (rule fps_ext) ``` huffman@29911 ` 141` ``` fix n :: nat ``` huffman@29911 ` 142` ``` have "(\j=0..n. \i=0..j. a\$i * b\$(j - i) * c\$(n - j)) = ``` huffman@29911 ` 143` ``` (\j=0..n. \i=0..n - j. a\$j * b\$i * c\$(n - j - i))" ``` huffman@29911 ` 144` ``` by (rule fps_mult_assoc_lemma) ``` wenzelm@52891 ` 145` ``` then show "((a * b) * c) \$ n = (a * (b * c)) \$ n" ``` nipkow@64267 ` 146` ``` by (simp add: fps_mult_nth sum_distrib_left sum_distrib_right mult.assoc) ``` huffman@29911 ` 147` ``` qed ``` huffman@29911 ` 148` ```qed ``` huffman@29911 ` 149` huffman@29911 ` 150` ```lemma fps_mult_commute_lemma: ``` wenzelm@52903 ` 151` ``` fixes n :: nat ``` wenzelm@52903 ` 152` ``` and f :: "nat \ nat \ 'a::comm_monoid_add" ``` huffman@29911 ` 153` ``` shows "(\i=0..n. f i (n - i)) = (\i=0..n. f (n - i) i)" ``` nipkow@64267 ` 154` ``` by (rule sum.reindex_bij_witness[where i="op - n" and j="op - n"]) auto ``` huffman@29911 ` 155` huffman@29911 ` 156` ```instance fps :: (comm_semiring_0) ab_semigroup_mult ``` huffman@29911 ` 157` ```proof ``` huffman@29911 ` 158` ``` fix a b :: "'a fps" ``` huffman@29911 ` 159` ``` show "a * b = b * a" ``` huffman@29911 ` 160` ``` proof (rule fps_ext) ``` huffman@29911 ` 161` ``` fix n :: nat ``` huffman@29911 ` 162` ``` have "(\i=0..n. a\$i * b\$(n - i)) = (\i=0..n. a\$(n - i) * b\$i)" ``` huffman@29911 ` 163` ``` by (rule fps_mult_commute_lemma) ``` wenzelm@52891 ` 164` ``` then show "(a * b) \$ n = (b * a) \$ n" ``` haftmann@57512 ` 165` ``` by (simp add: fps_mult_nth mult.commute) ``` chaieb@29687 ` 166` ``` qed ``` chaieb@29687 ` 167` ```qed ``` chaieb@29687 ` 168` huffman@29911 ` 169` ```instance fps :: (monoid_add) monoid_add ``` chaieb@29687 ` 170` ```proof ``` wenzelm@52891 ` 171` ``` fix a :: "'a fps" ``` wenzelm@52891 ` 172` ``` show "0 + a = a" by (simp add: fps_ext) ``` wenzelm@52891 ` 173` ``` show "a + 0 = a" by (simp add: fps_ext) ``` chaieb@29687 ` 174` ```qed ``` chaieb@29687 ` 175` huffman@29911 ` 176` ```instance fps :: (comm_monoid_add) comm_monoid_add ``` chaieb@29687 ` 177` ```proof ``` wenzelm@52891 ` 178` ``` fix a :: "'a fps" ``` wenzelm@52891 ` 179` ``` show "0 + a = a" by (simp add: fps_ext) ``` chaieb@29687 ` 180` ```qed ``` chaieb@29687 ` 181` huffman@29911 ` 182` ```instance fps :: (semiring_1) monoid_mult ``` chaieb@29687 ` 183` ```proof ``` wenzelm@52891 ` 184` ``` fix a :: "'a fps" ``` wenzelm@60501 ` 185` ``` show "1 * a = a" ``` nipkow@64267 ` 186` ``` by (simp add: fps_ext fps_mult_nth mult_delta_left sum.delta) ``` wenzelm@60501 ` 187` ``` show "a * 1 = a" ``` nipkow@64267 ` 188` ``` by (simp add: fps_ext fps_mult_nth mult_delta_right sum.delta') ``` chaieb@29687 ` 189` ```qed ``` chaieb@29687 ` 190` huffman@29911 ` 191` ```instance fps :: (cancel_semigroup_add) cancel_semigroup_add ``` huffman@29911 ` 192` ```proof ``` huffman@29911 ` 193` ``` fix a b c :: "'a fps" ``` wenzelm@60501 ` 194` ``` show "b = c" if "a + b = a + c" ``` wenzelm@60501 ` 195` ``` using that by (simp add: expand_fps_eq) ``` wenzelm@60501 ` 196` ``` show "b = c" if "b + a = c + a" ``` wenzelm@60501 ` 197` ``` using that by (simp add: expand_fps_eq) ``` huffman@29911 ` 198` ```qed ``` chaieb@29687 ` 199` huffman@29911 ` 200` ```instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add ``` huffman@29911 ` 201` ```proof ``` huffman@29911 ` 202` ``` fix a b c :: "'a fps" ``` wenzelm@60501 ` 203` ``` show "a + b - a = b" ``` wenzelm@60501 ` 204` ``` by (simp add: expand_fps_eq) ``` wenzelm@60501 ` 205` ``` show "a - b - c = a - (b + c)" ``` wenzelm@60501 ` 206` ``` by (simp add: expand_fps_eq diff_diff_eq) ``` huffman@29911 ` 207` ```qed ``` chaieb@29687 ` 208` huffman@29911 ` 209` ```instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. ``` huffman@29911 ` 210` huffman@29911 ` 211` ```instance fps :: (group_add) group_add ``` chaieb@29687 ` 212` ```proof ``` wenzelm@52891 ` 213` ``` fix a b :: "'a fps" ``` wenzelm@52891 ` 214` ``` show "- a + a = 0" by (simp add: fps_ext) ``` haftmann@54230 ` 215` ``` show "a + - b = a - b" by (simp add: fps_ext) ``` chaieb@29687 ` 216` ```qed ``` chaieb@29687 ` 217` huffman@29911 ` 218` ```instance fps :: (ab_group_add) ab_group_add ``` huffman@29911 ` 219` ```proof ``` huffman@29911 ` 220` ``` fix a b :: "'a fps" ``` wenzelm@52891 ` 221` ``` show "- a + a = 0" by (simp add: fps_ext) ``` wenzelm@52891 ` 222` ``` show "a - b = a + - b" by (simp add: fps_ext) ``` huffman@29911 ` 223` ```qed ``` chaieb@29687 ` 224` huffman@29911 ` 225` ```instance fps :: (zero_neq_one) zero_neq_one ``` wenzelm@60679 ` 226` ``` by standard (simp add: expand_fps_eq) ``` chaieb@29687 ` 227` huffman@29911 ` 228` ```instance fps :: (semiring_0) semiring ``` chaieb@29687 ` 229` ```proof ``` chaieb@29687 ` 230` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 231` ``` show "(a + b) * c = a * c + b * c" ``` nipkow@64267 ` 232` ``` by (simp add: expand_fps_eq fps_mult_nth distrib_right sum.distrib) ``` huffman@29911 ` 233` ``` show "a * (b + c) = a * b + a * c" ``` nipkow@64267 ` 234` ``` by (simp add: expand_fps_eq fps_mult_nth distrib_left sum.distrib) ``` chaieb@29687 ` 235` ```qed ``` chaieb@29687 ` 236` huffman@29911 ` 237` ```instance fps :: (semiring_0) semiring_0 ``` chaieb@29687 ` 238` ```proof ``` wenzelm@53195 ` 239` ``` fix a :: "'a fps" ``` wenzelm@60501 ` 240` ``` show "0 * a = 0" ``` wenzelm@60501 ` 241` ``` by (simp add: fps_ext fps_mult_nth) ``` wenzelm@60501 ` 242` ``` show "a * 0 = 0" ``` wenzelm@60501 ` 243` ``` by (simp add: fps_ext fps_mult_nth) ``` chaieb@29687 ` 244` ```qed ``` huffman@29911 ` 245` huffman@29911 ` 246` ```instance fps :: (semiring_0_cancel) semiring_0_cancel .. ``` huffman@29911 ` 247` haftmann@60867 ` 248` ```instance fps :: (semiring_1) semiring_1 .. ``` haftmann@60867 ` 249` wenzelm@60501 ` 250` wenzelm@60500 ` 251` ```subsection \Selection of the nth power of the implicit variable in the infinite sum\ ``` chaieb@29687 ` 252` eberlm@63317 ` 253` ```lemma fps_square_nth: "(f^2) \$ n = (\k\n. f \$ k * f \$ (n - k))" ``` eberlm@63317 ` 254` ``` by (simp add: power2_eq_square fps_mult_nth atLeast0AtMost) ``` eberlm@63317 ` 255` chaieb@29687 ` 256` ```lemma fps_nonzero_nth: "f \ 0 \ (\ n. f \$n \ 0)" ``` huffman@29911 ` 257` ``` by (simp add: expand_fps_eq) ``` chaieb@29687 ` 258` wenzelm@52902 ` 259` ```lemma fps_nonzero_nth_minimal: "f \ 0 \ (\n. f \$ n \ 0 \ (\m < n. f \$ m = 0))" ``` wenzelm@60501 ` 260` ``` (is "?lhs \ ?rhs") ``` huffman@29911 ` 261` ```proof ``` huffman@29911 ` 262` ``` let ?n = "LEAST n. f \$ n \ 0" ``` wenzelm@60501 ` 263` ``` show ?rhs if ?lhs ``` wenzelm@60501 ` 264` ``` proof - ``` wenzelm@60501 ` 265` ``` from that have "\n. f \$ n \ 0" ``` wenzelm@60501 ` 266` ``` by (simp add: fps_nonzero_nth) ``` wenzelm@60501 ` 267` ``` then have "f \$ ?n \ 0" ``` wenzelm@60501 ` 268` ``` by (rule LeastI_ex) ``` wenzelm@60501 ` 269` ``` moreover have "\m 0 \ (\m (\n. f \$ n = g \$n)" ``` huffman@29911 ` 279` ``` by (rule expand_fps_eq) ``` chaieb@29687 ` 280` nipkow@64267 ` 281` ```lemma fps_sum_nth: "sum f S \$ n = sum (\k. (f k) \$ n) S" ``` huffman@29911 ` 282` ```proof (cases "finite S") ``` wenzelm@52891 ` 283` ``` case True ``` wenzelm@52891 ` 284` ``` then show ?thesis by (induct set: finite) auto ``` huffman@29911 ` 285` ```next ``` wenzelm@52891 ` 286` ``` case False ``` wenzelm@52891 ` 287` ``` then show ?thesis by simp ``` chaieb@29687 ` 288` ```qed ``` chaieb@29687 ` 289` wenzelm@60501 ` 290` wenzelm@60501 ` 291` ```subsection \Injection of the basic ring elements and multiplication by scalars\ ``` chaieb@29687 ` 292` wenzelm@52891 ` 293` ```definition "fps_const c = Abs_fps (\n. if n = 0 then c else 0)" ``` huffman@29911 ` 294` huffman@29911 ` 295` ```lemma fps_nth_fps_const [simp]: "fps_const c \$ n = (if n = 0 then c else 0)" ``` huffman@29911 ` 296` ``` unfolding fps_const_def by simp ``` huffman@29911 ` 297` huffman@29911 ` 298` ```lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0" ``` huffman@29911 ` 299` ``` by (simp add: fps_ext) ``` huffman@29911 ` 300` huffman@29911 ` 301` ```lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1" ``` huffman@29911 ` 302` ``` by (simp add: fps_ext) ``` huffman@29911 ` 303` huffman@29911 ` 304` ```lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)" ``` huffman@29911 ` 305` ``` by (simp add: fps_ext) ``` huffman@29911 ` 306` wenzelm@54681 ` 307` ```lemma fps_const_add [simp]: "fps_const (c::'a::monoid_add) + fps_const d = fps_const (c + d)" ``` huffman@29911 ` 308` ``` by (simp add: fps_ext) ``` wenzelm@52891 ` 309` wenzelm@54681 ` 310` ```lemma fps_const_sub [simp]: "fps_const (c::'a::group_add) - fps_const d = fps_const (c - d)" ``` chaieb@31369 ` 311` ``` by (simp add: fps_ext) ``` wenzelm@52891 ` 312` wenzelm@54681 ` 313` ```lemma fps_const_mult[simp]: "fps_const (c::'a::ring) * fps_const d = fps_const (c * d)" ``` nipkow@64267 ` 314` ``` by (simp add: fps_eq_iff fps_mult_nth sum.neutral) ``` chaieb@29687 ` 315` wenzelm@54681 ` 316` ```lemma fps_const_add_left: "fps_const (c::'a::monoid_add) + f = ``` wenzelm@48757 ` 317` ``` Abs_fps (\n. if n = 0 then c + f\$0 else f\$n)" ``` huffman@29911 ` 318` ``` by (simp add: fps_ext) ``` huffman@29911 ` 319` wenzelm@54681 ` 320` ```lemma fps_const_add_right: "f + fps_const (c::'a::monoid_add) = ``` wenzelm@48757 ` 321` ``` Abs_fps (\n. if n = 0 then f\$0 + c else f\$n)" ``` huffman@29911 ` 322` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 323` wenzelm@54681 ` 324` ```lemma fps_const_mult_left: "fps_const (c::'a::semiring_0) * f = Abs_fps (\n. c * f\$n)" ``` huffman@29911 ` 325` ``` unfolding fps_eq_iff fps_mult_nth ``` nipkow@64267 ` 326` ``` by (simp add: fps_const_def mult_delta_left sum.delta) ``` huffman@29911 ` 327` wenzelm@54681 ` 328` ```lemma fps_const_mult_right: "f * fps_const (c::'a::semiring_0) = Abs_fps (\n. f\$n * c)" ``` huffman@29911 ` 329` ``` unfolding fps_eq_iff fps_mult_nth ``` nipkow@64267 ` 330` ``` by (simp add: fps_const_def mult_delta_right sum.delta') ``` chaieb@29687 ` 331` huffman@29911 ` 332` ```lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)\$n = c* f\$n" ``` nipkow@64267 ` 333` ``` by (simp add: fps_mult_nth mult_delta_left sum.delta) ``` chaieb@29687 ` 334` huffman@29911 ` 335` ```lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c" ``` nipkow@64267 ` 336` ``` by (simp add: fps_mult_nth mult_delta_right sum.delta') ``` chaieb@29687 ` 337` wenzelm@60501 ` 338` wenzelm@60500 ` 339` ```subsection \Formal power series form an integral domain\ ``` chaieb@29687 ` 340` huffman@29911 ` 341` ```instance fps :: (ring) ring .. ``` chaieb@29687 ` 342` huffman@29911 ` 343` ```instance fps :: (ring_1) ring_1 ``` haftmann@54230 ` 344` ``` by (intro_classes, auto simp add: distrib_right) ``` chaieb@29687 ` 345` huffman@29911 ` 346` ```instance fps :: (comm_ring_1) comm_ring_1 ``` haftmann@54230 ` 347` ``` by (intro_classes, auto simp add: distrib_right) ``` chaieb@29687 ` 348` huffman@29911 ` 349` ```instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ``` chaieb@29687 ` 350` ```proof ``` chaieb@29687 ` 351` ``` fix a b :: "'a fps" ``` wenzelm@60501 ` 352` ``` assume "a \ 0" and "b \ 0" ``` wenzelm@60501 ` 353` ``` then obtain i j where i: "a \$ i \ 0" "\k 0" "\kk=0..i+j. a \$ k * b \$ (i + j - k))" ``` chaieb@29687 ` 357` ``` by (rule fps_mult_nth) ``` wenzelm@60501 ` 358` ``` also have "\ = (a \$ i * b \$ (i + j - i)) + (\k\{0..i+j} - {i}. a \$ k * b \$ (i + j - k))" ``` nipkow@64267 ` 359` ``` by (rule sum.remove) simp_all ``` wenzelm@60501 ` 360` ``` also have "(\k\{0..i+j}-{i}. a \$ k * b \$ (i + j - k)) = 0" ``` nipkow@64267 ` 361` ``` proof (rule sum.neutral [rule_format]) ``` wenzelm@60501 ` 362` ``` fix k assume "k \ {0..i+j} - {i}" ``` wenzelm@60501 ` 363` ``` then have "k < i \ i+j-k < j" ``` wenzelm@60501 ` 364` ``` by auto ``` wenzelm@60501 ` 365` ``` then show "a \$ k * b \$ (i + j - k) = 0" ``` wenzelm@60501 ` 366` ``` using i j by auto ``` wenzelm@60501 ` 367` ``` qed ``` wenzelm@60501 ` 368` ``` also have "a \$ i * b \$ (i + j - i) + 0 = a \$ i * b \$ j" ``` wenzelm@60501 ` 369` ``` by simp ``` wenzelm@60501 ` 370` ``` also have "a \$ i * b \$ j \ 0" ``` wenzelm@60501 ` 371` ``` using i j by simp ``` huffman@29911 ` 372` ``` finally have "(a*b) \$ (i+j) \ 0" . ``` wenzelm@60501 ` 373` ``` then show "a * b \ 0" ``` wenzelm@60501 ` 374` ``` unfolding fps_nonzero_nth by blast ``` chaieb@29687 ` 375` ```qed ``` chaieb@29687 ` 376` haftmann@36311 ` 377` ```instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. ``` haftmann@36311 ` 378` huffman@29911 ` 379` ```instance fps :: (idom) idom .. ``` chaieb@29687 ` 380` huffman@47108 ` 381` ```lemma numeral_fps_const: "numeral k = fps_const (numeral k)" ``` wenzelm@48757 ` 382` ``` by (induct k) (simp_all only: numeral.simps fps_const_1_eq_1 ``` huffman@47108 ` 383` ``` fps_const_add [symmetric]) ``` huffman@47108 ` 384` haftmann@60867 ` 385` ```lemma neg_numeral_fps_const: ``` haftmann@60867 ` 386` ``` "(- numeral k :: 'a :: ring_1 fps) = fps_const (- numeral k)" ``` haftmann@60867 ` 387` ``` by (simp add: numeral_fps_const) ``` huffman@47108 ` 388` eberlm@61608 ` 389` ```lemma fps_numeral_nth: "numeral n \$ i = (if i = 0 then numeral n else 0)" ``` eberlm@61608 ` 390` ``` by (simp add: numeral_fps_const) ``` hoelzl@62102 ` 391` eberlm@61608 ` 392` ```lemma fps_numeral_nth_0 [simp]: "numeral n \$ 0 = numeral n" ``` eberlm@61608 ` 393` ``` by (simp add: numeral_fps_const) ``` eberlm@61608 ` 394` eberlm@63317 ` 395` ```lemma fps_of_nat: "fps_const (of_nat c) = of_nat c" ``` eberlm@63317 ` 396` ``` by (induction c) (simp_all add: fps_const_add [symmetric] del: fps_const_add) ``` eberlm@63317 ` 397` eberlm@65396 ` 398` ```lemma numeral_neq_fps_zero [simp]: "(numeral f :: 'a :: field_char_0 fps) \ 0" ``` eberlm@65396 ` 399` ```proof ``` eberlm@65396 ` 400` ``` assume "numeral f = (0 :: 'a fps)" ``` eberlm@65396 ` 401` ``` from arg_cong[of _ _ "\F. F \$ 0", OF this] show False by simp ``` eberlm@65396 ` 402` ```qed ``` eberlm@63317 ` 403` wenzelm@60501 ` 404` eberlm@66480 ` 405` ```subsection \The efps_Xtractor series fps_X\ ``` chaieb@31968 ` 406` wenzelm@54681 ` 407` ```lemma minus_one_power_iff: "(- (1::'a::comm_ring_1)) ^ n = (if even n then 1 else - 1)" ``` wenzelm@48757 ` 408` ``` by (induct n) auto ``` chaieb@31968 ` 409` eberlm@66480 ` 410` ```definition "fps_X = Abs_fps (\n. if n = 1 then 1 else 0)" ``` eberlm@66480 ` 411` eberlm@66480 ` 412` ```lemma fps_X_mult_nth [simp]: ``` eberlm@66480 ` 413` ``` "(fps_X * (f :: 'a::semiring_1 fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))" ``` wenzelm@53195 ` 414` ```proof (cases "n = 0") ``` wenzelm@53195 ` 415` ``` case False ``` eberlm@66480 ` 416` ``` have "(fps_X * f) \$n = (\i = 0..n. fps_X \$ i * f \$ (n - i))" ``` wenzelm@53195 ` 417` ``` by (simp add: fps_mult_nth) ``` wenzelm@53195 ` 418` ``` also have "\ = f \$ (n - 1)" ``` eberlm@66480 ` 419` ``` using False by (simp add: fps_X_def mult_delta_left sum.delta) ``` wenzelm@60501 ` 420` ``` finally show ?thesis ``` wenzelm@60501 ` 421` ``` using False by simp ``` wenzelm@53195 ` 422` ```next ``` wenzelm@53195 ` 423` ``` case True ``` wenzelm@60501 ` 424` ``` then show ?thesis ``` eberlm@66480 ` 425` ``` by (simp add: fps_mult_nth fps_X_def) ``` chaieb@31968 ` 426` ```qed ``` chaieb@31968 ` 427` eberlm@66480 ` 428` ```lemma fps_X_mult_right_nth[simp]: ``` eberlm@66480 ` 429` ``` "((a::'a::semiring_1 fps) * fps_X) \$ n = (if n = 0 then 0 else a \$ (n - 1))" ``` eberlm@63317 ` 430` ```proof - ``` eberlm@66480 ` 431` ``` have "(a * fps_X) \$ n = (\i = 0..n. a \$ i * (if n - i = Suc 0 then 1 else 0))" ``` eberlm@66480 ` 432` ``` by (simp add: fps_times_def fps_X_def) ``` eberlm@63317 ` 433` ``` also have "\ = (\i = 0..n. if i = n - 1 then if n = 0 then 0 else a \$ i else 0)" ``` nipkow@64267 ` 434` ``` by (intro sum.cong) auto ``` nipkow@64267 ` 435` ``` also have "\ = (if n = 0 then 0 else a \$ (n - 1))" by (simp add: sum.delta) ``` eberlm@63317 ` 436` ``` finally show ?thesis . ``` eberlm@63317 ` 437` ```qed ``` eberlm@63317 ` 438` eberlm@66480 ` 439` ```lemma fps_mult_fps_X_commute: "fps_X * (a :: 'a :: semiring_1 fps) = a * fps_X" ``` eberlm@63317 ` 440` ``` by (simp add: fps_eq_iff) ``` chaieb@31968 ` 441` eberlm@66480 ` 442` ```lemma fps_X_power_iff: "fps_X ^ n = Abs_fps (\m. if m = n then 1 else 0)" ``` eberlm@66466 ` 443` ``` by (induction n) (auto simp: fps_eq_iff) ``` chaieb@31968 ` 444` eberlm@66480 ` 445` ```lemma fps_X_nth[simp]: "fps_X\$n = (if n = 1 then 1 else 0)" ``` eberlm@66480 ` 446` ``` by (simp add: fps_X_def) ``` eberlm@66480 ` 447` eberlm@66480 ` 448` ```lemma fps_X_power_nth[simp]: "(fps_X^k) \$n = (if n = k then 1 else 0::'a::comm_ring_1)" ``` eberlm@66480 ` 449` ``` by (simp add: fps_X_power_iff) ``` eberlm@66480 ` 450` eberlm@66480 ` 451` ```lemma fps_X_power_mult_nth: "(fps_X^k * (f :: 'a::comm_ring_1 fps)) \$n = (if n < k then 0 else f \$ (n - k))" ``` chaieb@31968 ` 452` ``` apply (induct k arbitrary: n) ``` wenzelm@52891 ` 453` ``` apply simp ``` haftmann@57512 ` 454` ``` unfolding power_Suc mult.assoc ``` wenzelm@48757 ` 455` ``` apply (case_tac n) ``` wenzelm@48757 ` 456` ``` apply auto ``` wenzelm@48757 ` 457` ``` done ``` wenzelm@48757 ` 458` eberlm@66480 ` 459` ```lemma fps_X_power_mult_right_nth: ``` eberlm@66480 ` 460` ``` "((f :: 'a::comm_ring_1 fps) * fps_X^k) \$n = (if n < k then 0 else f \$ (n - k))" ``` eberlm@66480 ` 461` ``` by (metis fps_X_power_mult_nth mult.commute) ``` eberlm@66480 ` 462` eberlm@66480 ` 463` eberlm@66480 ` 464` ```lemma fps_X_neq_fps_const [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ fps_const c" ``` eberlm@61608 ` 465` ```proof ``` eberlm@66480 ` 466` ``` assume "(fps_X::'a fps) = fps_const (c::'a)" ``` eberlm@66480 ` 467` ``` hence "fps_X\$1 = (fps_const (c::'a))\$1" by (simp only:) ``` eberlm@61608 ` 468` ``` thus False by auto ``` eberlm@61608 ` 469` ```qed ``` eberlm@61608 ` 470` eberlm@66480 ` 471` ```lemma fps_X_neq_zero [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ 0" ``` eberlm@66480 ` 472` ``` by (simp only: fps_const_0_eq_0[symmetric] fps_X_neq_fps_const) simp ``` eberlm@66480 ` 473` eberlm@66480 ` 474` ```lemma fps_X_neq_one [simp]: "(fps_X :: 'a :: zero_neq_one fps) \ 1" ``` eberlm@66480 ` 475` ``` by (simp only: fps_const_1_eq_1[symmetric] fps_X_neq_fps_const) simp ``` eberlm@66480 ` 476` eberlm@66480 ` 477` ```lemma fps_X_neq_numeral [simp]: "(fps_X :: 'a :: {semiring_1,zero_neq_one} fps) \ numeral c" ``` eberlm@66480 ` 478` ``` by (simp only: numeral_fps_const fps_X_neq_fps_const) simp ``` eberlm@66480 ` 479` eberlm@66480 ` 480` ```lemma fps_X_pow_eq_fps_X_pow_iff [simp]: ``` eberlm@66480 ` 481` ``` "(fps_X :: ('a :: {comm_ring_1}) fps) ^ m = fps_X ^ n \ m = n" ``` eberlm@61608 ` 482` ```proof ``` eberlm@66480 ` 483` ``` assume "(fps_X :: 'a fps) ^ m = fps_X ^ n" ``` eberlm@66480 ` 484` ``` hence "(fps_X :: 'a fps) ^ m \$ m = fps_X ^ n \$ m" by (simp only:) ``` nipkow@62390 ` 485` ``` thus "m = n" by (simp split: if_split_asm) ``` eberlm@61608 ` 486` ```qed simp_all ``` hoelzl@62102 ` 487` hoelzl@62102 ` 488` hoelzl@62102 ` 489` ```subsection \Subdegrees\ ``` hoelzl@62102 ` 490` eberlm@61608 ` 491` ```definition subdegree :: "('a::zero) fps \ nat" where ``` eberlm@61608 ` 492` ``` "subdegree f = (if f = 0 then 0 else LEAST n. f\$n \ 0)" ``` eberlm@61608 ` 493` eberlm@61608 ` 494` ```lemma subdegreeI: ``` eberlm@61608 ` 495` ``` assumes "f \$ d \ 0" and "\i. i < d \ f \$ i = 0" ``` eberlm@61608 ` 496` ``` shows "subdegree f = d" ``` eberlm@61608 ` 497` ```proof- ``` eberlm@61608 ` 498` ``` from assms(1) have "f \ 0" by auto ``` eberlm@61608 ` 499` ``` moreover from assms(1) have "(LEAST i. f \$ i \ 0) = d" ``` eberlm@61608 ` 500` ``` proof (rule Least_equality) ``` eberlm@61608 ` 501` ``` fix e assume "f \$ e \ 0" ``` eberlm@61608 ` 502` ``` with assms(2) have "\(e < d)" by blast ``` eberlm@61608 ` 503` ``` thus "e \ d" by simp ``` eberlm@61608 ` 504` ``` qed ``` eberlm@61608 ` 505` ``` ultimately show ?thesis unfolding subdegree_def by simp ``` eberlm@61608 ` 506` ```qed ``` eberlm@61608 ` 507` eberlm@61608 ` 508` ```lemma nth_subdegree_nonzero [simp,intro]: "f \ 0 \ f \$ subdegree f \ 0" ``` eberlm@61608 ` 509` ```proof- ``` eberlm@61608 ` 510` ``` assume "f \ 0" ``` eberlm@61608 ` 511` ``` hence "subdegree f = (LEAST n. f \$ n \ 0)" by (simp add: subdegree_def) ``` eberlm@61608 ` 512` ``` also from \f \ 0\ have "\n. f\$n \ 0" using fps_nonzero_nth by blast ``` eberlm@61608 ` 513` ``` from LeastI_ex[OF this] have "f \$ (LEAST n. f \$ n \ 0) \ 0" . ``` eberlm@61608 ` 514` ``` finally show ?thesis . ``` eberlm@61608 ` 515` ```qed ``` eberlm@61608 ` 516` eberlm@61608 ` 517` ```lemma nth_less_subdegree_zero [dest]: "n < subdegree f \ f \$ n = 0" ``` eberlm@61608 ` 518` ```proof (cases "f = 0") ``` eberlm@61608 ` 519` ``` assume "f \ 0" and less: "n < subdegree f" ``` eberlm@61608 ` 520` ``` note less ``` eberlm@61608 ` 521` ``` also from \f \ 0\ have "subdegree f = (LEAST n. f \$ n \ 0)" by (simp add: subdegree_def) ``` eberlm@61608 ` 522` ``` finally show "f \$ n = 0" using not_less_Least by blast ``` eberlm@61608 ` 523` ```qed simp_all ``` hoelzl@62102 ` 524` eberlm@61608 ` 525` ```lemma subdegree_geI: ``` eberlm@61608 ` 526` ``` assumes "f \ 0" "\i. i < n \ f\$i = 0" ``` eberlm@61608 ` 527` ``` shows "subdegree f \ n" ``` eberlm@61608 ` 528` ```proof (rule ccontr) ``` eberlm@61608 ` 529` ``` assume "\(subdegree f \ n)" ``` eberlm@61608 ` 530` ``` with assms(2) have "f \$ subdegree f = 0" by simp ``` eberlm@61608 ` 531` ``` moreover from assms(1) have "f \$ subdegree f \ 0" by simp ``` eberlm@61608 ` 532` ``` ultimately show False by contradiction ``` eberlm@61608 ` 533` ```qed ``` eberlm@61608 ` 534` eberlm@61608 ` 535` ```lemma subdegree_greaterI: ``` eberlm@61608 ` 536` ``` assumes "f \ 0" "\i. i \ n \ f\$i = 0" ``` eberlm@61608 ` 537` ``` shows "subdegree f > n" ``` eberlm@61608 ` 538` ```proof (rule ccontr) ``` eberlm@61608 ` 539` ``` assume "\(subdegree f > n)" ``` eberlm@61608 ` 540` ``` with assms(2) have "f \$ subdegree f = 0" by simp ``` eberlm@61608 ` 541` ``` moreover from assms(1) have "f \$ subdegree f \ 0" by simp ``` eberlm@61608 ` 542` ``` ultimately show False by contradiction ``` eberlm@61608 ` 543` ```qed ``` eberlm@61608 ` 544` eberlm@61608 ` 545` ```lemma subdegree_leI: ``` eberlm@61608 ` 546` ``` "f \$ n \ 0 \ subdegree f \ n" ``` eberlm@61608 ` 547` ``` by (rule leI) auto ``` eberlm@61608 ` 548` eberlm@61608 ` 549` eberlm@61608 ` 550` ```lemma subdegree_0 [simp]: "subdegree 0 = 0" ``` eberlm@61608 ` 551` ``` by (simp add: subdegree_def) ``` eberlm@61608 ` 552` eberlm@61608 ` 553` ```lemma subdegree_1 [simp]: "subdegree (1 :: ('a :: zero_neq_one) fps) = 0" ``` eberlm@61608 ` 554` ``` by (auto intro!: subdegreeI) ``` eberlm@61608 ` 555` eberlm@66480 ` 556` ```lemma subdegree_fps_X [simp]: "subdegree (fps_X :: ('a :: zero_neq_one) fps) = 1" ``` eberlm@66480 ` 557` ``` by (auto intro!: subdegreeI simp: fps_X_def) ``` eberlm@61608 ` 558` eberlm@61608 ` 559` ```lemma subdegree_fps_const [simp]: "subdegree (fps_const c) = 0" ``` eberlm@61608 ` 560` ``` by (cases "c = 0") (auto intro!: subdegreeI) ``` eberlm@61608 ` 561` eberlm@61608 ` 562` ```lemma subdegree_numeral [simp]: "subdegree (numeral n) = 0" ``` eberlm@61608 ` 563` ``` by (simp add: numeral_fps_const) ``` eberlm@61608 ` 564` eberlm@61608 ` 565` ```lemma subdegree_eq_0_iff: "subdegree f = 0 \ f = 0 \ f \$ 0 \ 0" ``` eberlm@61608 ` 566` ```proof (cases "f = 0") ``` eberlm@61608 ` 567` ``` assume "f \ 0" ``` eberlm@61608 ` 568` ``` thus ?thesis ``` eberlm@61608 ` 569` ``` using nth_subdegree_nonzero[OF \f \ 0\] by (fastforce intro!: subdegreeI) ``` eberlm@61608 ` 570` ```qed simp_all ``` eberlm@61608 ` 571` eberlm@61608 ` 572` ```lemma subdegree_eq_0 [simp]: "f \$ 0 \ 0 \ subdegree f = 0" ``` eberlm@61608 ` 573` ``` by (simp add: subdegree_eq_0_iff) ``` eberlm@61608 ` 574` eberlm@61608 ` 575` ```lemma nth_subdegree_mult [simp]: ``` eberlm@61608 ` 576` ``` fixes f g :: "('a :: {mult_zero,comm_monoid_add}) fps" ``` eberlm@61608 ` 577` ``` shows "(f * g) \$ (subdegree f + subdegree g) = f \$ subdegree f * g \$ subdegree g" ``` eberlm@61608 ` 578` ```proof- ``` eberlm@61608 ` 579` ``` let ?n = "subdegree f + subdegree g" ``` eberlm@61608 ` 580` ``` have "(f * g) \$ ?n = (\i=0..?n. f\$i * g\$(?n-i))" ``` eberlm@61608 ` 581` ``` by (simp add: fps_mult_nth) ``` eberlm@61608 ` 582` ``` also have "... = (\i=0..?n. if i = subdegree f then f\$i * g\$(?n-i) else 0)" ``` nipkow@64267 ` 583` ``` proof (intro sum.cong) ``` eberlm@61608 ` 584` ``` fix x assume x: "x \ {0..?n}" ``` eberlm@61608 ` 585` ``` hence "x = subdegree f \ x < subdegree f \ ?n - x < subdegree g" by auto ``` eberlm@61608 ` 586` ``` thus "f \$ x * g \$ (?n - x) = (if x = subdegree f then f \$ x * g \$ (?n - x) else 0)" ``` eberlm@61608 ` 587` ``` by (elim disjE conjE) auto ``` eberlm@61608 ` 588` ``` qed auto ``` nipkow@64267 ` 589` ``` also have "... = f \$ subdegree f * g \$ subdegree g" by (simp add: sum.delta) ``` eberlm@61608 ` 590` ``` finally show ?thesis . ``` eberlm@61608 ` 591` ```qed ``` eberlm@61608 ` 592` eberlm@61608 ` 593` ```lemma subdegree_mult [simp]: ``` eberlm@61608 ` 594` ``` assumes "f \ 0" "g \ 0" ``` eberlm@61608 ` 595` ``` shows "subdegree ((f :: ('a :: {ring_no_zero_divisors}) fps) * g) = subdegree f + subdegree g" ``` eberlm@61608 ` 596` ```proof (rule subdegreeI) ``` eberlm@61608 ` 597` ``` let ?n = "subdegree f + subdegree g" ``` eberlm@61608 ` 598` ``` have "(f * g) \$ ?n = (\i=0..?n. f\$i * g\$(?n-i))" by (simp add: fps_mult_nth) ``` eberlm@61608 ` 599` ``` also have "... = (\i=0..?n. if i = subdegree f then f\$i * g\$(?n-i) else 0)" ``` nipkow@64267 ` 600` ``` proof (intro sum.cong) ``` eberlm@61608 ` 601` ``` fix x assume x: "x \ {0..?n}" ``` eberlm@61608 ` 602` ``` hence "x = subdegree f \ x < subdegree f \ ?n - x < subdegree g" by auto ``` eberlm@61608 ` 603` ``` thus "f \$ x * g \$ (?n - x) = (if x = subdegree f then f \$ x * g \$ (?n - x) else 0)" ``` eberlm@61608 ` 604` ``` by (elim disjE conjE) auto ``` eberlm@61608 ` 605` ``` qed auto ``` nipkow@64267 ` 606` ``` also have "... = f \$ subdegree f * g \$ subdegree g" by (simp add: sum.delta) ``` eberlm@61608 ` 607` ``` also from assms have "... \ 0" by auto ``` eberlm@61608 ` 608` ``` finally show "(f * g) \$ (subdegree f + subdegree g) \ 0" . ``` eberlm@61608 ` 609` ```next ``` eberlm@61608 ` 610` ``` fix m assume m: "m < subdegree f + subdegree g" ``` hoelzl@62102 ` 611` ``` have "(f * g) \$ m = (\i=0..m. f\$i * g\$(m-i))" by (simp add: fps_mult_nth) ``` eberlm@61608 ` 612` ``` also have "... = (\i=0..m. 0)" ``` nipkow@64267 ` 613` ``` proof (rule sum.cong) ``` eberlm@61608 ` 614` ``` fix i assume "i \ {0..m}" ``` eberlm@61608 ` 615` ``` with m have "i < subdegree f \ m - i < subdegree g" by auto ``` eberlm@61608 ` 616` ``` thus "f\$i * g\$(m-i) = 0" by (elim disjE) auto ``` eberlm@61608 ` 617` ``` qed auto ``` eberlm@61608 ` 618` ``` finally show "(f * g) \$ m = 0" by simp ``` eberlm@61608 ` 619` ```qed ``` eberlm@61608 ` 620` eberlm@61608 ` 621` ```lemma subdegree_power [simp]: ``` eberlm@61608 ` 622` ``` "subdegree ((f :: ('a :: ring_1_no_zero_divisors) fps) ^ n) = n * subdegree f" ``` eberlm@61608 ` 623` ``` by (cases "f = 0"; induction n) simp_all ``` eberlm@61608 ` 624` eberlm@61608 ` 625` ```lemma subdegree_uminus [simp]: ``` eberlm@61608 ` 626` ``` "subdegree (-(f::('a::group_add) fps)) = subdegree f" ``` eberlm@61608 ` 627` ``` by (simp add: subdegree_def) ``` eberlm@61608 ` 628` eberlm@61608 ` 629` ```lemma subdegree_minus_commute [simp]: ``` eberlm@61608 ` 630` ``` "subdegree (f-(g::('a::group_add) fps)) = subdegree (g - f)" ``` eberlm@61608 ` 631` ```proof - ``` eberlm@61608 ` 632` ``` have "f - g = -(g - f)" by simp ``` eberlm@61608 ` 633` ``` also have "subdegree ... = subdegree (g - f)" by (simp only: subdegree_uminus) ``` eberlm@61608 ` 634` ``` finally show ?thesis . ``` eberlm@61608 ` 635` ```qed ``` eberlm@61608 ` 636` eberlm@61608 ` 637` ```lemma subdegree_add_ge: ``` eberlm@61608 ` 638` ``` assumes "f \ -(g :: ('a :: {group_add}) fps)" ``` eberlm@61608 ` 639` ``` shows "subdegree (f + g) \ min (subdegree f) (subdegree g)" ``` eberlm@61608 ` 640` ```proof (rule subdegree_geI) ``` eberlm@61608 ` 641` ``` from assms show "f + g \ 0" by (subst (asm) eq_neg_iff_add_eq_0) ``` eberlm@61608 ` 642` ```next ``` eberlm@61608 ` 643` ``` fix i assume "i < min (subdegree f) (subdegree g)" ``` eberlm@61608 ` 644` ``` hence "f \$ i = 0" and "g \$ i = 0" by auto ``` eberlm@61608 ` 645` ``` thus "(f + g) \$ i = 0" by force ``` eberlm@61608 ` 646` ```qed ``` eberlm@61608 ` 647` eberlm@61608 ` 648` ```lemma subdegree_add_eq1: ``` eberlm@61608 ` 649` ``` assumes "f \ 0" ``` eberlm@61608 ` 650` ``` assumes "subdegree f < subdegree (g :: ('a :: {group_add}) fps)" ``` eberlm@61608 ` 651` ``` shows "subdegree (f + g) = subdegree f" ``` eberlm@61608 ` 652` ```proof (rule antisym[OF subdegree_leI]) ``` eberlm@61608 ` 653` ``` from assms show "subdegree (f + g) \ subdegree f" ``` eberlm@61608 ` 654` ``` by (intro order.trans[OF min.boundedI subdegree_add_ge]) auto ``` eberlm@61608 ` 655` ``` from assms have "f \$ subdegree f \ 0" "g \$ subdegree f = 0" by auto ``` eberlm@61608 ` 656` ``` thus "(f + g) \$ subdegree f \ 0" by simp ``` eberlm@61608 ` 657` ```qed ``` eberlm@61608 ` 658` eberlm@61608 ` 659` ```lemma subdegree_add_eq2: ``` eberlm@61608 ` 660` ``` assumes "g \ 0" ``` eberlm@61608 ` 661` ``` assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)" ``` eberlm@61608 ` 662` ``` shows "subdegree (f + g) = subdegree g" ``` eberlm@61608 ` 663` ``` using subdegree_add_eq1[OF assms] by (simp add: add.commute) ``` eberlm@61608 ` 664` eberlm@61608 ` 665` ```lemma subdegree_diff_eq1: ``` eberlm@61608 ` 666` ``` assumes "f \ 0" ``` eberlm@61608 ` 667` ``` assumes "subdegree f < subdegree (g :: ('a :: {ab_group_add}) fps)" ``` eberlm@61608 ` 668` ``` shows "subdegree (f - g) = subdegree f" ``` eberlm@61608 ` 669` ``` using subdegree_add_eq1[of f "-g"] assms by (simp add: add.commute) ``` eberlm@61608 ` 670` eberlm@61608 ` 671` ```lemma subdegree_diff_eq2: ``` eberlm@61608 ` 672` ``` assumes "g \ 0" ``` eberlm@61608 ` 673` ``` assumes "subdegree g < subdegree (f :: ('a :: {ab_group_add}) fps)" ``` eberlm@61608 ` 674` ``` shows "subdegree (f - g) = subdegree g" ``` eberlm@61608 ` 675` ``` using subdegree_add_eq2[of "-g" f] assms by (simp add: add.commute) ``` eberlm@61608 ` 676` eberlm@61608 ` 677` ```lemma subdegree_diff_ge [simp]: ``` eberlm@61608 ` 678` ``` assumes "f \ (g :: ('a :: {group_add}) fps)" ``` eberlm@61608 ` 679` ``` shows "subdegree (f - g) \ min (subdegree f) (subdegree g)" ``` eberlm@61608 ` 680` ``` using assms subdegree_add_ge[of f "-g"] by simp ``` eberlm@61608 ` 681` eberlm@61608 ` 682` eberlm@61608 ` 683` eberlm@61608 ` 684` eberlm@61608 ` 685` ```subsection \Shifting and slicing\ ``` eberlm@61608 ` 686` eberlm@61608 ` 687` ```definition fps_shift :: "nat \ 'a fps \ 'a fps" where ``` eberlm@61608 ` 688` ``` "fps_shift n f = Abs_fps (\i. f \$ (i + n))" ``` eberlm@61608 ` 689` eberlm@61608 ` 690` ```lemma fps_shift_nth [simp]: "fps_shift n f \$ i = f \$ (i + n)" ``` eberlm@61608 ` 691` ``` by (simp add: fps_shift_def) ``` eberlm@61608 ` 692` eberlm@61608 ` 693` ```lemma fps_shift_0 [simp]: "fps_shift 0 f = f" ``` eberlm@61608 ` 694` ``` by (intro fps_ext) (simp add: fps_shift_def) ``` eberlm@61608 ` 695` eberlm@61608 ` 696` ```lemma fps_shift_zero [simp]: "fps_shift n 0 = 0" ``` eberlm@61608 ` 697` ``` by (intro fps_ext) (simp add: fps_shift_def) ``` eberlm@61608 ` 698` eberlm@61608 ` 699` ```lemma fps_shift_one: "fps_shift n 1 = (if n = 0 then 1 else 0)" ``` eberlm@61608 ` 700` ``` by (intro fps_ext) (simp add: fps_shift_def) ``` eberlm@61608 ` 701` eberlm@61608 ` 702` ```lemma fps_shift_fps_const: "fps_shift n (fps_const c) = (if n = 0 then fps_const c else 0)" ``` eberlm@61608 ` 703` ``` by (intro fps_ext) (simp add: fps_shift_def) ``` eberlm@61608 ` 704` eberlm@61608 ` 705` ```lemma fps_shift_numeral: "fps_shift n (numeral c) = (if n = 0 then numeral c else 0)" ``` eberlm@61608 ` 706` ``` by (simp add: numeral_fps_const fps_shift_fps_const) ``` eberlm@61608 ` 707` eberlm@66480 ` 708` ```lemma fps_shift_fps_X_power [simp]: ``` eberlm@66480 ` 709` ``` "n \ m \ fps_shift n (fps_X ^ m) = (fps_X ^ (m - n) ::'a::comm_ring_1 fps)" ``` hoelzl@62102 ` 710` ``` by (intro fps_ext) (auto simp: fps_shift_def ) ``` eberlm@61608 ` 711` eberlm@66480 ` 712` ```lemma fps_shift_times_fps_X_power: ``` eberlm@66480 ` 713` ``` "n \ subdegree f \ fps_shift n f * fps_X ^ n = (f :: 'a :: comm_ring_1 fps)" ``` eberlm@66480 ` 714` ``` by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) ``` eberlm@66480 ` 715` eberlm@66480 ` 716` ```lemma fps_shift_times_fps_X_power' [simp]: ``` eberlm@66480 ` 717` ``` "fps_shift n (f * fps_X^n) = (f :: 'a :: comm_ring_1 fps)" ``` eberlm@66480 ` 718` ``` by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) ``` eberlm@66480 ` 719` eberlm@66480 ` 720` ```lemma fps_shift_times_fps_X_power'': ``` eberlm@66480 ` 721` ``` "m \ n \ fps_shift n (f * fps_X^m) = fps_shift (n - m) (f :: 'a :: comm_ring_1 fps)" ``` eberlm@66480 ` 722` ``` by (intro fps_ext) (auto simp: fps_X_power_mult_right_nth nth_less_subdegree_zero) ``` eberlm@61608 ` 723` hoelzl@62102 ` 724` ```lemma fps_shift_subdegree [simp]: ``` eberlm@61608 ` 725` ``` "n \ subdegree f \ subdegree (fps_shift n f) = subdegree (f :: 'a :: comm_ring_1 fps) - n" ``` eberlm@61608 ` 726` ``` by (cases "f = 0") (force intro: nth_less_subdegree_zero subdegreeI)+ ``` eberlm@61608 ` 727` eberlm@61608 ` 728` ```lemma subdegree_decompose: ``` eberlm@66480 ` 729` ``` "f = fps_shift (subdegree f) f * fps_X ^ subdegree (f :: ('a :: comm_ring_1) fps)" ``` eberlm@66480 ` 730` ``` by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth) ``` eberlm@61608 ` 731` eberlm@61608 ` 732` ```lemma subdegree_decompose': ``` eberlm@66480 ` 733` ``` "n \ subdegree (f :: ('a :: comm_ring_1) fps) \ f = fps_shift n f * fps_X^n" ``` eberlm@66480 ` 734` ``` by (rule fps_ext) (auto simp: fps_X_power_mult_right_nth intro!: nth_less_subdegree_zero) ``` eberlm@61608 ` 735` eberlm@61608 ` 736` ```lemma fps_shift_fps_shift: ``` eberlm@61608 ` 737` ``` "fps_shift (m + n) f = fps_shift m (fps_shift n f)" ``` eberlm@61608 ` 738` ``` by (rule fps_ext) (simp add: add_ac) ``` hoelzl@62102 ` 739` eberlm@61608 ` 740` ```lemma fps_shift_add: ``` eberlm@61608 ` 741` ``` "fps_shift n (f + g) = fps_shift n f + fps_shift n g" ``` eberlm@61608 ` 742` ``` by (simp add: fps_eq_iff) ``` hoelzl@62102 ` 743` eberlm@61608 ` 744` ```lemma fps_shift_mult: ``` eberlm@61608 ` 745` ``` assumes "n \ subdegree (g :: 'b :: {comm_ring_1} fps)" ``` eberlm@61608 ` 746` ``` shows "fps_shift n (h*g) = h * fps_shift n g" ``` eberlm@61608 ` 747` ```proof - ``` eberlm@66480 ` 748` ``` from assms have "g = fps_shift n g * fps_X^n" by (rule subdegree_decompose') ``` eberlm@66480 ` 749` ``` also have "h * ... = (h * fps_shift n g) * fps_X^n" by simp ``` eberlm@61608 ` 750` ``` also have "fps_shift n ... = h * fps_shift n g" by simp ``` eberlm@61608 ` 751` ``` finally show ?thesis . ``` eberlm@61608 ` 752` ```qed ``` eberlm@61608 ` 753` eberlm@61608 ` 754` ```lemma fps_shift_mult_right: ``` eberlm@61608 ` 755` ``` assumes "n \ subdegree (g :: 'b :: {comm_ring_1} fps)" ``` eberlm@61608 ` 756` ``` shows "fps_shift n (g*h) = h * fps_shift n g" ``` eberlm@61608 ` 757` ``` by (subst mult.commute, subst fps_shift_mult) (simp_all add: assms) ``` eberlm@61608 ` 758` eberlm@61608 ` 759` ```lemma nth_subdegree_zero_iff [simp]: "f \$ subdegree f = 0 \ f = 0" ``` eberlm@61608 ` 760` ``` by (cases "f = 0") auto ``` eberlm@61608 ` 761` eberlm@61608 ` 762` ```lemma fps_shift_subdegree_zero_iff [simp]: ``` eberlm@61608 ` 763` ``` "fps_shift (subdegree f) f = 0 \ f = 0" ``` eberlm@61608 ` 764` ``` by (subst (1) nth_subdegree_zero_iff[symmetric], cases "f = 0") ``` eberlm@61608 ` 765` ``` (simp_all del: nth_subdegree_zero_iff) ``` eberlm@61608 ` 766` eberlm@61608 ` 767` eberlm@61608 ` 768` ```definition "fps_cutoff n f = Abs_fps (\i. if i < n then f\$i else 0)" ``` eberlm@61608 ` 769` eberlm@61608 ` 770` ```lemma fps_cutoff_nth [simp]: "fps_cutoff n f \$ i = (if i < n then f\$i else 0)" ``` eberlm@61608 ` 771` ``` unfolding fps_cutoff_def by simp ``` eberlm@61608 ` 772` eberlm@61608 ` 773` ```lemma fps_cutoff_zero_iff: "fps_cutoff n f = 0 \ (f = 0 \ n \ subdegree f)" ``` eberlm@61608 ` 774` ```proof ``` eberlm@61608 ` 775` ``` assume A: "fps_cutoff n f = 0" ``` eberlm@61608 ` 776` ``` thus "f = 0 \ n \ subdegree f" ``` eberlm@61608 ` 777` ``` proof (cases "f = 0") ``` eberlm@61608 ` 778` ``` assume "f \ 0" ``` eberlm@61608 ` 779` ``` with A have "n \ subdegree f" ``` nipkow@62390 ` 780` ``` by (intro subdegree_geI) (auto simp: fps_eq_iff split: if_split_asm) ``` eberlm@61608 ` 781` ``` thus ?thesis .. ``` eberlm@61608 ` 782` ``` qed simp ``` eberlm@61608 ` 783` ```qed (auto simp: fps_eq_iff intro: nth_less_subdegree_zero) ``` eberlm@61608 ` 784` eberlm@61608 ` 785` ```lemma fps_cutoff_0 [simp]: "fps_cutoff 0 f = 0" ``` eberlm@61608 ` 786` ``` by (simp add: fps_eq_iff) ``` hoelzl@62102 ` 787` eberlm@61608 ` 788` ```lemma fps_cutoff_zero [simp]: "fps_cutoff n 0 = 0" ``` eberlm@61608 ` 789` ``` by (simp add: fps_eq_iff) ``` eberlm@61608 ` 790` eberlm@61608 ` 791` ```lemma fps_cutoff_one: "fps_cutoff n 1 = (if n = 0 then 0 else 1)" ``` eberlm@61608 ` 792` ``` by (simp add: fps_eq_iff) ``` eberlm@61608 ` 793` eberlm@61608 ` 794` ```lemma fps_cutoff_fps_const: "fps_cutoff n (fps_const c) = (if n = 0 then 0 else fps_const c)" ``` hoelzl@62102 ` 795` ``` by (simp add: fps_eq_iff) ``` eberlm@61608 ` 796` eberlm@61608 ` 797` ```lemma fps_cutoff_numeral: "fps_cutoff n (numeral c) = (if n = 0 then 0 else numeral c)" ``` eberlm@61608 ` 798` ``` by (simp add: numeral_fps_const fps_cutoff_fps_const) ``` eberlm@61608 ` 799` hoelzl@62102 ` 800` ```lemma fps_shift_cutoff: ``` eberlm@66480 ` 801` ``` "fps_shift n (f :: ('a :: comm_ring_1) fps) * fps_X^n + fps_cutoff n f = f" ``` eberlm@66480 ` 802` ``` by (simp add: fps_eq_iff fps_X_power_mult_right_nth) ``` eberlm@61608 ` 803` eberlm@61608 ` 804` wenzelm@60501 ` 805` ```subsection \Formal Power series form a metric space\ ``` chaieb@31968 ` 806` chaieb@31968 ` 807` ```instantiation fps :: (comm_ring_1) dist ``` chaieb@31968 ` 808` ```begin ``` chaieb@31968 ` 809` wenzelm@52891 ` 810` ```definition ``` eberlm@61608 ` 811` ``` dist_fps_def: "dist (a :: 'a fps) b = (if a = b then 0 else inverse (2 ^ subdegree (a - b)))" ``` chaieb@31968 ` 812` wenzelm@54681 ` 813` ```lemma dist_fps_ge0: "dist (a :: 'a fps) b \ 0" ``` chaieb@31968 ` 814` ``` by (simp add: dist_fps_def) ``` chaieb@31968 ` 815` wenzelm@54681 ` 816` ```lemma dist_fps_sym: "dist (a :: 'a fps) b = dist b a" ``` eberlm@61608 ` 817` ``` by (simp add: dist_fps_def) ``` wenzelm@48757 ` 818` chaieb@31968 ` 819` ```instance .. ``` wenzelm@48757 ` 820` chaieb@30746 ` 821` ```end ``` chaieb@30746 ` 822` chaieb@31968 ` 823` ```instantiation fps :: (comm_ring_1) metric_space ``` chaieb@31968 ` 824` ```begin ``` chaieb@31968 ` 825` hoelzl@62101 ` 826` ```definition uniformity_fps_def [code del]: ``` hoelzl@62101 ` 827` ``` "(uniformity :: ('a fps \ 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})" ``` hoelzl@62101 ` 828` hoelzl@62101 ` 829` ```definition open_fps_def' [code del]: ``` hoelzl@62101 ` 830` ``` "open (U :: 'a fps set) \ (\x\U. eventually (\(x', y). x' = x \ y \ U) uniformity)" ``` eberlm@61608 ` 831` chaieb@31968 ` 832` ```instance ``` chaieb@31968 ` 833` ```proof ``` wenzelm@60501 ` 834` ``` show th: "dist a b = 0 \ a = b" for a b :: "'a fps" ``` nipkow@62390 ` 835` ``` by (simp add: dist_fps_def split: if_split_asm) ``` eberlm@61608 ` 836` ``` then have th'[simp]: "dist a a = 0" for a :: "'a fps" by simp ``` wenzelm@60501 ` 837` chaieb@31968 ` 838` ``` fix a b c :: "'a fps" ``` wenzelm@60501 ` 839` ``` consider "a = b" | "c = a \ c = b" | "a \ b" "a \ c" "b \ c" by blast ``` wenzelm@60501 ` 840` ``` then show "dist a b \ dist a c + dist b c" ``` wenzelm@60501 ` 841` ``` proof cases ``` wenzelm@60501 ` 842` ``` case 1 ``` eberlm@61608 ` 843` ``` then show ?thesis by (simp add: dist_fps_def) ``` wenzelm@60501 ` 844` ``` next ``` wenzelm@60501 ` 845` ``` case 2 ``` wenzelm@60501 ` 846` ``` then show ?thesis ``` wenzelm@52891 ` 847` ``` by (cases "c = a") (simp_all add: th dist_fps_sym) ``` wenzelm@60501 ` 848` ``` next ``` wenzelm@60567 ` 849` ``` case neq: 3 ``` wenzelm@60558 ` 850` ``` have False if "dist a b > dist a c + dist b c" ``` wenzelm@60558 ` 851` ``` proof - ``` eberlm@61608 ` 852` ``` let ?n = "subdegree (a - b)" ``` eberlm@61608 ` 853` ``` from neq have "dist a b > 0" "dist b c > 0" and "dist a c > 0" by (simp_all add: dist_fps_def) ``` eberlm@61608 ` 854` ``` with that have "dist a b > dist a c" and "dist a b > dist b c" by simp_all ``` hoelzl@62102 ` 855` ``` with neq have "?n < subdegree (a - c)" and "?n < subdegree (b - c)" ``` eberlm@61608 ` 856` ``` by (simp_all add: dist_fps_def field_simps) ``` hoelzl@62102 ` 857` ``` hence "(a - c) \$ ?n = 0" and "(b - c) \$ ?n = 0" ``` eberlm@61608 ` 858` ``` by (simp_all only: nth_less_subdegree_zero) ``` eberlm@61608 ` 859` ``` hence "(a - b) \$ ?n = 0" by simp ``` eberlm@61608 ` 860` ``` moreover from neq have "(a - b) \$ ?n \ 0" by (intro nth_subdegree_nonzero) simp_all ``` eberlm@61608 ` 861` ``` ultimately show False by contradiction ``` wenzelm@60558 ` 862` ``` qed ``` eberlm@61608 ` 863` ``` thus ?thesis by (auto simp add: not_le[symmetric]) ``` wenzelm@60501 ` 864` ``` qed ``` hoelzl@62101 ` 865` ```qed (rule open_fps_def' uniformity_fps_def)+ ``` wenzelm@52891 ` 866` chaieb@31968 ` 867` ```end ``` chaieb@31968 ` 868` hoelzl@62102 ` 869` ```declare uniformity_Abort[where 'a="'a :: comm_ring_1 fps", code] ``` hoelzl@62102 ` 870` eberlm@66373 ` 871` ```lemma open_fps_def: "open (S :: 'a::comm_ring_1 fps set) = (\a \ S. \r. r >0 \ {y. dist y a < r} \ S)" ``` eberlm@66373 ` 872` ``` unfolding open_dist subset_eq by simp ``` eberlm@61608 ` 873` wenzelm@60558 ` 874` ```text \The infinite sums and justification of the notation in textbooks.\ ``` chaieb@31968 ` 875` wenzelm@52891 ` 876` ```lemma reals_power_lt_ex: ``` wenzelm@54681 ` 877` ``` fixes x y :: real ``` wenzelm@54681 ` 878` ``` assumes xp: "x > 0" ``` wenzelm@54681 ` 879` ``` and y1: "y > 1" ``` chaieb@31968 ` 880` ``` shows "\k>0. (1/y)^k < x" ``` wenzelm@52891 ` 881` ```proof - ``` wenzelm@54681 ` 882` ``` have yp: "y > 0" ``` wenzelm@54681 ` 883` ``` using y1 by simp ``` chaieb@31968 ` 884` ``` from reals_Archimedean2[of "max 0 (- log y x) + 1"] ``` wenzelm@54681 ` 885` ``` obtain k :: nat where k: "real k > max 0 (- log y x) + 1" ``` wenzelm@54681 ` 886` ``` by blast ``` wenzelm@54681 ` 887` ``` from k have kp: "k > 0" ``` wenzelm@54681 ` 888` ``` by simp ``` wenzelm@54681 ` 889` ``` from k have "real k > - log y x" ``` wenzelm@54681 ` 890` ``` by simp ``` wenzelm@54681 ` 891` ``` then have "ln y * real k > - ln x" ``` wenzelm@54681 ` 892` ``` unfolding log_def ``` chaieb@31968 ` 893` ``` using ln_gt_zero_iff[OF yp] y1 ``` wenzelm@54681 ` 894` ``` by (simp add: minus_divide_left field_simps del: minus_divide_left[symmetric]) ``` wenzelm@54681 ` 895` ``` then have "ln y * real k + ln x > 0" ``` wenzelm@54681 ` 896` ``` by simp ``` chaieb@31968 ` 897` ``` then have "exp (real k * ln y + ln x) > exp 0" ``` haftmann@57514 ` 898` ``` by (simp add: ac_simps) ``` chaieb@31968 ` 899` ``` then have "y ^ k * x > 1" ``` lp15@65578 ` 900` ``` unfolding exp_zero exp_add exp_of_nat_mult exp_ln [OF xp] exp_ln [OF yp] ``` wenzelm@52891 ` 901` ``` by simp ``` wenzelm@52891 ` 902` ``` then have "x > (1 / y)^k" using yp ``` haftmann@60867 ` 903` ``` by (simp add: field_simps) ``` wenzelm@54681 ` 904` ``` then show ?thesis ``` wenzelm@54681 ` 905` ``` using kp by blast ``` chaieb@31968 ` 906` ```qed ``` wenzelm@52891 ` 907` eberlm@66480 ` 908` ```lemma fps_sum_rep_nth: "(sum (\i. fps_const(a\$i)*fps_X^i) {0..m})\$n = ``` wenzelm@54681 ` 909` ``` (if n \ m then a\$n else 0::'a::comm_ring_1)" ``` lp15@66089 ` 910` ``` by (auto simp add: fps_sum_nth cond_value_iff cong del: if_weak_cong) ``` wenzelm@52891 ` 911` eberlm@66480 ` 912` ```lemma fps_notation: "(\n. sum (\i. fps_const(a\$i) * fps_X^i) {0..n}) \ a" ``` wenzelm@61969 ` 913` ``` (is "?s \ a") ``` wenzelm@52891 ` 914` ```proof - ``` wenzelm@60558 ` 915` ``` have "\n0. \n \ n0. dist (?s n) a < r" if "r > 0" for r ``` wenzelm@60558 ` 916` ``` proof - ``` wenzelm@60501 ` 917` ``` obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" ``` wenzelm@60501 ` 918` ``` using reals_power_lt_ex[OF \r > 0\, of 2] by auto ``` wenzelm@60558 ` 919` ``` show ?thesis ``` wenzelm@60501 ` 920` ``` proof - ``` wenzelm@60558 ` 921` ``` have "dist (?s n) a < r" if nn0: "n \ n0" for n ``` wenzelm@60558 ` 922` ``` proof - ``` wenzelm@60558 ` 923` ``` from that have thnn0: "(1/2)^n \ (1/2 :: real)^n0" ``` wenzelm@60501 ` 924` ``` by (simp add: divide_simps) ``` wenzelm@60558 ` 925` ``` show ?thesis ``` wenzelm@60501 ` 926` ``` proof (cases "?s n = a") ``` wenzelm@60501 ` 927` ``` case True ``` wenzelm@60501 ` 928` ``` then show ?thesis ``` wenzelm@60501 ` 929` ``` unfolding dist_eq_0_iff[of "?s n" a, symmetric] ``` wenzelm@60501 ` 930` ``` using \r > 0\ by (simp del: dist_eq_0_iff) ``` wenzelm@60501 ` 931` ``` next ``` wenzelm@60501 ` 932` ``` case False ``` eberlm@61608 ` 933` ``` from False have dth: "dist (?s n) a = (1/2)^subdegree (?s n - a)" ``` eberlm@61608 ` 934` ``` by (simp add: dist_fps_def field_simps) ``` eberlm@61608 ` 935` ``` from False have kn: "subdegree (?s n - a) > n" ``` hoelzl@62102 ` 936` ``` by (intro subdegree_greaterI) (simp_all add: fps_sum_rep_nth) ``` hoelzl@62102 ` 937` ``` then have "dist (?s n) a < (1/2)^n" ``` eberlm@61608 ` 938` ``` by (simp add: field_simps dist_fps_def) ``` wenzelm@60501 ` 939` ``` also have "\ \ (1/2)^n0" ``` wenzelm@60501 ` 940` ``` using nn0 by (simp add: divide_simps) ``` wenzelm@60501 ` 941` ``` also have "\ < r" ``` wenzelm@60501 ` 942` ``` using n0 by simp ``` wenzelm@60501 ` 943` ``` finally show ?thesis . ``` wenzelm@60501 ` 944` ``` qed ``` wenzelm@60558 ` 945` ``` qed ``` wenzelm@60501 ` 946` ``` then show ?thesis by blast ``` wenzelm@60501 ` 947` ``` qed ``` wenzelm@60558 ` 948` ``` qed ``` wenzelm@54681 ` 949` ``` then show ?thesis ``` lp15@60017 ` 950` ``` unfolding lim_sequentially by blast ``` wenzelm@52891 ` 951` ```qed ``` chaieb@31968 ` 952` wenzelm@54681 ` 953` wenzelm@60501 ` 954` ```subsection \Inverses of formal power series\ ``` chaieb@29687 ` 955` nipkow@64267 ` 956` ```declare sum.cong[fundef_cong] ``` chaieb@29687 ` 957` wenzelm@60558 ` 958` ```instantiation fps :: ("{comm_monoid_add,inverse,times,uminus}") inverse ``` chaieb@29687 ` 959` ```begin ``` chaieb@29687 ` 960` wenzelm@52891 ` 961` ```fun natfun_inverse:: "'a fps \ nat \ 'a" ``` wenzelm@52891 ` 962` ```where ``` chaieb@29687 ` 963` ``` "natfun_inverse f 0 = inverse (f\$0)" ``` nipkow@64267 ` 964` ```| "natfun_inverse f n = - inverse (f\$0) * sum (\i. f\$i * natfun_inverse f (n - i)) {1..n}" ``` chaieb@29687 ` 965` wenzelm@60501 ` 966` ```definition fps_inverse_def: "inverse f = (if f \$ 0 = 0 then 0 else Abs_fps (natfun_inverse f))" ``` wenzelm@60501 ` 967` eberlm@61608 ` 968` ```definition fps_divide_def: ``` hoelzl@62102 ` 969` ``` "f div g = (if g = 0 then 0 else ``` eberlm@61608 ` 970` ``` let n = subdegree g; h = fps_shift n g ``` eberlm@61608 ` 971` ``` in fps_shift n (f * inverse h))" ``` haftmann@36311 ` 972` chaieb@29687 ` 973` ```instance .. ``` haftmann@36311 ` 974` chaieb@29687 ` 975` ```end ``` chaieb@29687 ` 976` wenzelm@52891 ` 977` ```lemma fps_inverse_zero [simp]: ``` wenzelm@54681 ` 978` ``` "inverse (0 :: 'a::{comm_monoid_add,inverse,times,uminus} fps) = 0" ``` huffman@29911 ` 979` ``` by (simp add: fps_ext fps_inverse_def) ``` chaieb@29687 ` 980` wenzelm@52891 ` 981` ```lemma fps_inverse_one [simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1" ``` huffman@29911 ` 982` ``` apply (auto simp add: expand_fps_eq fps_inverse_def) ``` wenzelm@52891 ` 983` ``` apply (case_tac n) ``` wenzelm@52891 ` 984` ``` apply auto ``` wenzelm@52891 ` 985` ``` done ``` wenzelm@52891 ` 986` wenzelm@52891 ` 987` ```lemma inverse_mult_eq_1 [intro]: ``` wenzelm@52891 ` 988` ``` assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 989` ``` shows "inverse f * f = 1" ``` wenzelm@52891 ` 990` ```proof - ``` wenzelm@54681 ` 991` ``` have c: "inverse f * f = f * inverse f" ``` haftmann@57512 ` 992` ``` by (simp add: mult.commute) ``` huffman@30488 ` 993` ``` from f0 have ifn: "\n. inverse f \$ n = natfun_inverse f n" ``` chaieb@29687 ` 994` ``` by (simp add: fps_inverse_def) ``` chaieb@29687 ` 995` ``` from f0 have th0: "(inverse f * f) \$ 0 = 1" ``` huffman@29911 ` 996` ``` by (simp add: fps_mult_nth fps_inverse_def) ``` wenzelm@60501 ` 997` ``` have "(inverse f * f)\$n = 0" if np: "n > 0" for n ``` wenzelm@60501 ` 998` ``` proof - ``` wenzelm@54681 ` 999` ``` from np have eq: "{0..n} = {0} \ {1 .. n}" ``` wenzelm@54681 ` 1000` ``` by auto ``` wenzelm@54681 ` 1001` ``` have d: "{0} \ {1 .. n} = {}" ``` wenzelm@54681 ` 1002` ``` by auto ``` wenzelm@52891 ` 1003` ``` from f0 np have th0: "- (inverse f \$ n) = ``` nipkow@64267 ` 1004` ``` (sum (\i. f\$i * natfun_inverse f (n - i)) {1..n}) / (f\$0)" ``` wenzelm@52891 ` 1005` ``` by (cases n) (simp_all add: divide_inverse fps_inverse_def) ``` chaieb@29687 ` 1006` ``` from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] ``` nipkow@64267 ` 1007` ``` have th1: "sum (\i. f\$i * natfun_inverse f (n - i)) {1..n} = - (f\$0) * (inverse f)\$n" ``` haftmann@36350 ` 1008` ``` by (simp add: field_simps) ``` huffman@30488 ` 1009` ``` have "(f * inverse f) \$ n = (\i = 0..n. f \$i * natfun_inverse f (n - i))" ``` chaieb@29687 ` 1010` ``` unfolding fps_mult_nth ifn .. ``` wenzelm@52891 ` 1011` ``` also have "\ = f\$0 * natfun_inverse f n + (\i = 1..n. f\$i * natfun_inverse f (n-i))" ``` bulwahn@46757 ` 1012` ``` by (simp add: eq) ``` wenzelm@54681 ` 1013` ``` also have "\ = 0" ``` wenzelm@54681 ` 1014` ``` unfolding th1 ifn by simp ``` wenzelm@60501 ` 1015` ``` finally show ?thesis unfolding c . ``` wenzelm@60501 ` 1016` ``` qed ``` wenzelm@54681 ` 1017` ``` with th0 show ?thesis ``` wenzelm@54681 ` 1018` ``` by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1019` ```qed ``` chaieb@29687 ` 1020` wenzelm@60501 ` 1021` ```lemma fps_inverse_0_iff[simp]: "(inverse f) \$ 0 = (0::'a::division_ring) \ f \$ 0 = 0" ``` huffman@29911 ` 1022` ``` by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) ``` hoelzl@62102 ` 1023` eberlm@61608 ` 1024` ```lemma fps_inverse_nth_0 [simp]: "inverse f \$ 0 = inverse (f \$ 0 :: 'a :: division_ring)" ``` eberlm@61608 ` 1025` ``` by (simp add: fps_inverse_def) ``` eberlm@61608 ` 1026` eberlm@61608 ` 1027` ```lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::division_ring) fps) \ f \$ 0 = 0" ``` wenzelm@60501 ` 1028` ```proof ``` eberlm@61608 ` 1029` ``` assume A: "inverse f = 0" ``` eberlm@61608 ` 1030` ``` have "0 = inverse f \$ 0" by (subst A) simp ``` eberlm@61608 ` 1031` ``` thus "f \$ 0 = 0" by simp ``` eberlm@61608 ` 1032` ```qed (simp add: fps_inverse_def) ``` eberlm@61608 ` 1033` eberlm@61608 ` 1034` ```lemma fps_inverse_idempotent[intro, simp]: ``` wenzelm@48757 ` 1035` ``` assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 1036` ``` shows "inverse (inverse f) = f" ``` wenzelm@52891 ` 1037` ```proof - ``` chaieb@29687 ` 1038` ``` from f0 have if0: "inverse f \$ 0 \ 0" by simp ``` huffman@30488 ` 1039` ``` from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] ``` wenzelm@52891 ` 1040` ``` have "inverse f * f = inverse f * inverse (inverse f)" ``` haftmann@57514 ` 1041` ``` by (simp add: ac_simps) ``` wenzelm@54681 ` 1042` ``` then show ?thesis ``` wenzelm@54681 ` 1043` ``` using f0 unfolding mult_cancel_left by simp ``` chaieb@29687 ` 1044` ```qed ``` chaieb@29687 ` 1045` wenzelm@48757 ` 1046` ```lemma fps_inverse_unique: ``` eberlm@61608 ` 1047` ``` assumes fg: "(f :: 'a :: field fps) * g = 1" ``` eberlm@61608 ` 1048` ``` shows "inverse f = g" ``` wenzelm@52891 ` 1049` ```proof - ``` eberlm@61608 ` 1050` ``` have f0: "f \$ 0 \ 0" ``` eberlm@61608 ` 1051` ``` proof ``` eberlm@61608 ` 1052` ``` assume "f \$ 0 = 0" ``` eberlm@61608 ` 1053` ``` hence "0 = (f * g) \$ 0" by simp ``` eberlm@61608 ` 1054` ``` also from fg have "(f * g) \$ 0 = 1" by simp ``` eberlm@61608 ` 1055` ``` finally show False by simp ``` eberlm@61608 ` 1056` ``` qed ``` eberlm@61608 ` 1057` ``` from inverse_mult_eq_1[OF this] fg ``` wenzelm@54681 ` 1058` ``` have th0: "inverse f * f = g * f" ``` haftmann@57514 ` 1059` ``` by (simp add: ac_simps) ``` wenzelm@54681 ` 1060` ``` then show ?thesis ``` wenzelm@54681 ` 1061` ``` using f0 ``` wenzelm@54681 ` 1062` ``` unfolding mult_cancel_right ``` huffman@29911 ` 1063` ``` by (auto simp add: expand_fps_eq) ``` chaieb@29687 ` 1064` ```qed ``` chaieb@29687 ` 1065` eberlm@63317 ` 1066` ```lemma fps_inverse_eq_0: "f\$0 = 0 \ inverse (f :: 'a :: division_ring fps) = 0" ``` eberlm@63317 ` 1067` ``` by simp ``` eberlm@63317 ` 1068` ``` ``` nipkow@64267 ` 1069` ```lemma sum_zero_lemma: ``` lp15@60162 ` 1070` ``` fixes n::nat ``` lp15@60162 ` 1071` ``` assumes "0 < n" ``` lp15@60162 ` 1072` ``` shows "(\i = 0..n. if n = i then 1 else if n - i = 1 then - 1 else 0) = (0::'a::field)" ``` wenzelm@54681 ` 1073` ```proof - ``` lp15@60162 ` 1074` ``` let ?f = "\i. if n = i then 1 else if n - i = 1 then - 1 else 0" ``` lp15@60162 ` 1075` ``` let ?g = "\i. if i = n then 1 else if i = n - 1 then - 1 else 0" ``` chaieb@29687 ` 1076` ``` let ?h = "\i. if i=n - 1 then - 1 else 0" ``` nipkow@64267 ` 1077` ``` have th1: "sum ?f {0..n} = sum ?g {0..n}" ``` nipkow@64267 ` 1078` ``` by (rule sum.cong) auto ``` nipkow@64267 ` 1079` ``` have th2: "sum ?g {0..n - 1} = sum ?h {0..n - 1}" ``` nipkow@64267 ` 1080` ``` apply (rule sum.cong) ``` lp15@60162 ` 1081` ``` using assms ``` wenzelm@54681 ` 1082` ``` apply auto ``` wenzelm@54681 ` 1083` ``` done ``` wenzelm@54681 ` 1084` ``` have eq: "{0 .. n} = {0.. n - 1} \ {n}" ``` wenzelm@54681 ` 1085` ``` by auto ``` lp15@60162 ` 1086` ``` from assms have d: "{0.. n - 1} \ {n} = {}" ``` wenzelm@54681 ` 1087` ``` by auto ``` wenzelm@54681 ` 1088` ``` have f: "finite {0.. n - 1}" "finite {n}" ``` wenzelm@54681 ` 1089` ``` by auto ``` lp15@60162 ` 1090` ``` show ?thesis ``` huffman@30488 ` 1091` ``` unfolding th1 ``` nipkow@64267 ` 1092` ``` apply (simp add: sum.union_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) ``` chaieb@29687 ` 1093` ``` unfolding th2 ``` nipkow@64267 ` 1094` ``` apply (simp add: sum.delta) ``` wenzelm@52891 ` 1095` ``` done ``` chaieb@29687 ` 1096` ```qed ``` chaieb@29687 ` 1097` eberlm@61608 ` 1098` ```lemma fps_inverse_mult: "inverse (f * g :: 'a::field fps) = inverse f * inverse g" ``` eberlm@61608 ` 1099` ```proof (cases "f\$0 = 0 \ g\$0 = 0") ``` eberlm@61608 ` 1100` ``` assume "\(f\$0 = 0 \ g\$0 = 0)" ``` eberlm@61608 ` 1101` ``` hence [simp]: "f\$0 \ 0" "g\$0 \ 0" by simp_all ``` eberlm@61608 ` 1102` ``` show ?thesis ``` eberlm@61608 ` 1103` ``` proof (rule fps_inverse_unique) ``` eberlm@61608 ` 1104` ``` have "f * g * (inverse f * inverse g) = (inverse f * f) * (inverse g * g)" by simp ``` eberlm@61608 ` 1105` ``` also have "... = 1" by (subst (1 2) inverse_mult_eq_1) simp_all ``` eberlm@61608 ` 1106` ``` finally show "f * g * (inverse f * inverse g) = 1" . ``` eberlm@61608 ` 1107` ``` qed ``` eberlm@61608 ` 1108` ```next ``` eberlm@61608 ` 1109` ``` assume A: "f\$0 = 0 \ g\$0 = 0" ``` eberlm@61608 ` 1110` ``` hence "inverse (f * g) = 0" by simp ``` eberlm@61608 ` 1111` ``` also from A have "... = inverse f * inverse g" by auto ``` eberlm@61608 ` 1112` ``` finally show "inverse (f * g) = inverse f * inverse g" . ``` eberlm@61608 ` 1113` ```qed ``` hoelzl@62102 ` 1114` eberlm@61608 ` 1115` wenzelm@60501 ` 1116` ```lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) = ``` wenzelm@60501 ` 1117` ``` Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" ``` lp15@60162 ` 1118` ``` apply (rule fps_inverse_unique) ``` nipkow@64267 ` 1119` ``` apply (simp_all add: fps_eq_iff fps_mult_nth sum_zero_lemma) ``` lp15@60162 ` 1120` ``` done ``` lp15@60162 ` 1121` eberlm@61608 ` 1122` ```lemma subdegree_inverse [simp]: "subdegree (inverse (f::'a::field fps)) = 0" ``` eberlm@61608 ` 1123` ```proof (cases "f\$0 = 0") ``` eberlm@61608 ` 1124` ``` assume nz: "f\$0 \ 0" ``` eberlm@61608 ` 1125` ``` hence "subdegree (inverse f) + subdegree f = subdegree (inverse f * f)" ``` eberlm@61608 ` 1126` ``` by (subst subdegree_mult) auto ``` eberlm@61608 ` 1127` ``` also from nz have "subdegree f = 0" by (simp add: subdegree_eq_0_iff) ``` eberlm@61608 ` 1128` ``` also from nz have "inverse f * f = 1" by (rule inverse_mult_eq_1) ``` eberlm@61608 ` 1129` ``` finally show "subdegree (inverse f) = 0" by simp ``` eberlm@61608 ` 1130` ```qed (simp_all add: fps_inverse_def) ``` eberlm@61608 ` 1131` eberlm@61608 ` 1132` ```lemma fps_is_unit_iff [simp]: "(f :: 'a :: field fps) dvd 1 \ f \$ 0 \ 0" ``` eberlm@61608 ` 1133` ```proof ``` eberlm@61608 ` 1134` ``` assume "f dvd 1" ``` eberlm@61608 ` 1135` ``` then obtain g where "1 = f * g" by (elim dvdE) ``` eberlm@61608 ` 1136` ``` from this[symmetric] have "(f*g) \$ 0 = 1" by simp ``` eberlm@61608 ` 1137` ``` thus "f \$ 0 \ 0" by auto ``` eberlm@61608 ` 1138` ```next ``` eberlm@61608 ` 1139` ``` assume A: "f \$ 0 \ 0" ``` eberlm@61608 ` 1140` ``` thus "f dvd 1" by (simp add: inverse_mult_eq_1[OF A, symmetric]) ``` eberlm@61608 ` 1141` ```qed ``` eberlm@61608 ` 1142` eberlm@61608 ` 1143` ```lemma subdegree_eq_0' [simp]: "(f :: 'a :: field fps) dvd 1 \ subdegree f = 0" ``` eberlm@61608 ` 1144` ``` by simp ``` eberlm@61608 ` 1145` eberlm@61608 ` 1146` ```lemma fps_unit_dvd [simp]: "(f \$ 0 :: 'a :: field) \ 0 \ f dvd g" ``` eberlm@61608 ` 1147` ``` by (rule dvd_trans, subst fps_is_unit_iff) simp_all ``` eberlm@61608 ` 1148` haftmann@64592 ` 1149` ```instantiation fps :: (field) normalization_semidom ``` haftmann@64592 ` 1150` ```begin ``` haftmann@64592 ` 1151` haftmann@64592 ` 1152` ```definition fps_unit_factor_def [simp]: ``` haftmann@64592 ` 1153` ``` "unit_factor f = fps_shift (subdegree f) f" ``` haftmann@64592 ` 1154` haftmann@64592 ` 1155` ```definition fps_normalize_def [simp]: ``` eberlm@66480 ` 1156` ``` "normalize f = (if f = 0 then 0 else fps_X ^ subdegree f)" ``` haftmann@64592 ` 1157` haftmann@64592 ` 1158` ```instance proof ``` haftmann@64592 ` 1159` ``` fix f :: "'a fps" ``` haftmann@64592 ` 1160` ``` show "unit_factor f * normalize f = f" ``` eberlm@66480 ` 1161` ``` by (simp add: fps_shift_times_fps_X_power) ``` haftmann@64592 ` 1162` ```next ``` haftmann@64592 ` 1163` ``` fix f g :: "'a fps" ``` haftmann@64592 ` 1164` ``` show "unit_factor (f * g) = unit_factor f * unit_factor g" ``` haftmann@64592 ` 1165` ``` proof (cases "f = 0 \ g = 0") ``` haftmann@64592 ` 1166` ``` assume "\(f = 0 \ g = 0)" ``` haftmann@64592 ` 1167` ``` thus "unit_factor (f * g) = unit_factor f * unit_factor g" ``` haftmann@64592 ` 1168` ``` unfolding fps_unit_factor_def ``` haftmann@64592 ` 1169` ``` by (auto simp: fps_shift_fps_shift fps_shift_mult fps_shift_mult_right) ``` haftmann@64592 ` 1170` ``` qed auto ``` haftmann@64592 ` 1171` ```next ``` haftmann@64592 ` 1172` ``` fix f g :: "'a fps" ``` haftmann@64592 ` 1173` ``` assume "g \ 0" ``` haftmann@64592 ` 1174` ``` then have "f * (fps_shift (subdegree g) g * inverse (fps_shift (subdegree g) g)) = f" ``` haftmann@64592 ` 1175` ``` by (metis add_cancel_right_left fps_shift_nth inverse_mult_eq_1 mult.commute mult_cancel_left2 nth_subdegree_nonzero) ``` haftmann@64592 ` 1176` ``` then have "fps_shift (subdegree g) (g * (f * inverse (fps_shift (subdegree g) g))) = f" ``` haftmann@64592 ` 1177` ``` by (simp add: fps_shift_mult_right mult.commute) ``` haftmann@64592 ` 1178` ``` with \g \ 0\ show "f * g / g = f" ``` haftmann@64592 ` 1179` ``` by (simp add: fps_divide_def Let_def ac_simps) ``` haftmann@64592 ` 1180` ```qed (auto simp add: fps_divide_def Let_def) ``` haftmann@64592 ` 1181` haftmann@64592 ` 1182` ```end ``` eberlm@61608 ` 1183` haftmann@66806 ` 1184` ```instantiation fps :: (field) idom_modulo ``` eberlm@61608 ` 1185` ```begin ``` eberlm@61608 ` 1186` eberlm@61608 ` 1187` ```definition fps_mod_def: ``` eberlm@61608 ` 1188` ``` "f mod g = (if g = 0 then f else ``` hoelzl@62102 ` 1189` ``` let n = subdegree g; h = fps_shift n g ``` eberlm@61608 ` 1190` ``` in fps_cutoff n (f * inverse h) * h)" ``` eberlm@61608 ` 1191` hoelzl@62102 ` 1192` ```lemma fps_mod_eq_zero: ``` eberlm@61608 ` 1193` ``` assumes "g \ 0" and "subdegree f \ subdegree g" ``` eberlm@61608 ` 1194` ``` shows "f mod g = 0" ``` eberlm@61608 ` 1195` ``` using assms by (cases "f = 0") (auto simp: fps_cutoff_zero_iff fps_mod_def Let_def) ``` eberlm@61608 ` 1196` hoelzl@62102 ` 1197` ```lemma fps_times_divide_eq: ``` eberlm@61608 ` 1198` ``` assumes "g \ 0" and "subdegree f \ subdegree (g :: 'a fps)" ``` eberlm@61608 ` 1199` ``` shows "f div g * g = f" ``` eberlm@61608 ` 1200` ```proof (cases "f = 0") ``` eberlm@61608 ` 1201` ``` assume nz: "f \ 0" ``` wenzelm@63040 ` 1202` ``` define n where "n = subdegree g" ``` wenzelm@63040 ` 1203` ``` define h where "h = fps_shift n g" ``` eberlm@61608 ` 1204` ``` from assms have [simp]: "h \$ 0 \ 0" unfolding h_def by (simp add: n_def) ``` hoelzl@62102 ` 1205` eberlm@61608 ` 1206` ``` from assms nz have "f div g * g = fps_shift n (f * inverse h) * g" ``` eberlm@61608 ` 1207` ``` by (simp add: fps_divide_def Let_def h_def n_def) ``` eberlm@66480 ` 1208` ``` also have "... = fps_shift n (f * inverse h) * fps_X^n * h" unfolding h_def n_def ``` eberlm@61608 ` 1209` ``` by (subst subdegree_decompose[of g]) simp ``` eberlm@66480 ` 1210` ``` also have "fps_shift n (f * inverse h) * fps_X^n = f * inverse h" ``` eberlm@66480 ` 1211` ``` by (rule fps_shift_times_fps_X_power) (simp_all add: nz assms n_def) ``` eberlm@61608 ` 1212` ``` also have "... * h = f * (inverse h * h)" by simp ``` eberlm@61608 ` 1213` ``` also have "inverse h * h = 1" by (rule inverse_mult_eq_1) simp ``` eberlm@61608 ` 1214` ``` finally show ?thesis by simp ``` eberlm@61608 ` 1215` ```qed (simp_all add: fps_divide_def Let_def) ``` eberlm@61608 ` 1216` hoelzl@62102 ` 1217` ```lemma ``` eberlm@61608 ` 1218` ``` assumes "g\$0 \ 0" ``` eberlm@61608 ` 1219` ``` shows fps_divide_unit: "f div g = f * inverse g" and fps_mod_unit [simp]: "f mod g = 0" ``` eberlm@61608 ` 1220` ```proof - ``` eberlm@61608 ` 1221` ``` from assms have [simp]: "subdegree g = 0" by (simp add: subdegree_eq_0_iff) ``` hoelzl@62102 ` 1222` ``` from assms show "f div g = f * inverse g" ``` eberlm@61608 ` 1223` ``` by (auto simp: fps_divide_def Let_def subdegree_eq_0_iff) ``` eberlm@61608 ` 1224` ``` from assms show "f mod g = 0" by (intro fps_mod_eq_zero) auto ``` eberlm@61608 ` 1225` ```qed ``` eberlm@61608 ` 1226` eberlm@61608 ` 1227` ```instance proof ``` eberlm@61608 ` 1228` ``` fix f g :: "'a fps" ``` wenzelm@63040 ` 1229` ``` define n where "n = subdegree g" ``` wenzelm@63040 ` 1230` ``` define h where "h = fps_shift n g" ``` hoelzl@62102 ` 1231` eberlm@61608 ` 1232` ``` show "f div g * g + f mod g = f" ``` eberlm@61608 ` 1233` ``` proof (cases "g = 0 \ f = 0") ``` eberlm@61608 ` 1234` ``` assume "\(g = 0 \ f = 0)" ``` eberlm@61608 ` 1235` ``` hence nz [simp]: "f \ 0" "g \ 0" by simp_all ``` eberlm@61608 ` 1236` ``` show ?thesis ``` eberlm@61608 ` 1237` ``` proof (rule disjE[OF le_less_linear]) ``` eberlm@61608 ` 1238` ``` assume "subdegree f \ subdegree g" ``` eberlm@61608 ` 1239` ``` with nz show ?thesis by (simp add: fps_mod_eq_zero fps_times_divide_eq) ``` eberlm@61608 ` 1240` ``` next ``` eberlm@61608 ` 1241` ``` assume "subdegree f < subdegree g" ``` eberlm@66480 ` 1242` ``` have g_decomp: "g = h * fps_X^n" unfolding h_def n_def by (rule subdegree_decompose) ``` hoelzl@62102 ` 1243` ``` have "f div g * g + f mod g = ``` hoelzl@62102 ` 1244` ``` fps_shift n (f * inverse h) * g + fps_cutoff n (f * inverse h) * h" ``` eberlm@61608 ` 1245` ``` by (simp add: fps_mod_def fps_divide_def Let_def n_def h_def) ``` eberlm@66480 ` 1246` ``` also have "... = h * (fps_shift n (f * inverse h) * fps_X^n + fps_cutoff n (f * inverse h))" ``` eberlm@61608 ` 1247` ``` by (subst g_decomp) (simp add: algebra_simps) ``` eberlm@61608 ` 1248` ``` also have "... = f * (inverse h * h)" ``` eberlm@61608 ` 1249` ``` by (subst fps_shift_cutoff) simp ``` eberlm@61608 ` 1250` ``` also have "inverse h * h = 1" by (rule inverse_mult_eq_1) (simp add: h_def n_def) ``` eberlm@61608 ` 1251` ``` finally show ?thesis by simp ``` eberlm@61608 ` 1252` ``` qed ``` eberlm@61608 ` 1253` ``` qed (auto simp: fps_mod_def fps_divide_def Let_def) ``` haftmann@64592 ` 1254` ```qed ``` eberlm@61608 ` 1255` eberlm@61608 ` 1256` ```end ``` eberlm@61608 ` 1257` eberlm@61608 ` 1258` ```lemma subdegree_mod: ``` eberlm@61608 ` 1259` ``` assumes "f \ 0" "subdegree f < subdegree g" ``` eberlm@61608 ` 1260` ``` shows "subdegree (f mod g) = subdegree f" ``` eberlm@61608 ` 1261` ```proof (cases "f div g * g = 0") ``` eberlm@61608 ` 1262` ``` assume "f div g * g \ 0" ``` eberlm@61608 ` 1263` ``` hence [simp]: "f div g \ 0" "g \ 0" by auto ``` haftmann@64242 ` 1264` ``` from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) ``` eberlm@61608 ` 1265` ``` also from assms have "subdegree ... = subdegree f" ``` eberlm@61608 ` 1266` ``` by (intro subdegree_diff_eq1) simp_all ``` eberlm@61608 ` 1267` ``` finally show ?thesis . ``` eberlm@61608 ` 1268` ```next ``` eberlm@61608 ` 1269` ``` assume zero: "f div g * g = 0" ``` haftmann@64242 ` 1270` ``` from div_mult_mod_eq[of f g] have "f mod g = f - f div g * g" by (simp add: algebra_simps) ``` eberlm@61608 ` 1271` ``` also note zero ``` eberlm@61608 ` 1272` ``` finally show ?thesis by simp ``` eberlm@61608 ` 1273` ```qed ``` eberlm@61608 ` 1274` eberlm@61608 ` 1275` ```lemma fps_divide_nth_0 [simp]: "g \$ 0 \ 0 \ (f div g) \$ 0 = f \$ 0 / (g \$ 0 :: _ :: field)" ``` eberlm@61608 ` 1276` ``` by (simp add: fps_divide_unit divide_inverse) ``` eberlm@61608 ` 1277` eberlm@61608 ` 1278` hoelzl@62102 ` 1279` ```lemma dvd_imp_subdegree_le: ``` eberlm@61608 ` 1280` ``` "(f :: 'a :: idom fps) dvd g \ g \ 0 \ subdegree f \ subdegree g" ``` eberlm@61608 ` 1281` ``` by (auto elim: dvdE) ``` eberlm@61608 ` 1282` hoelzl@62102 ` 1283` ```lemma fps_dvd_iff: ``` eberlm@61608 ` 1284` ``` assumes "(f :: 'a :: field fps) \ 0" "g \ 0" ``` eberlm@61608 ` 1285` ``` shows "f dvd g \ subdegree f \ subdegree g" ``` eberlm@61608 ` 1286` ```proof ``` eberlm@61608 ` 1287` ``` assume "subdegree f \ subdegree g" ``` hoelzl@62102 ` 1288` ``` with assms have "g mod f = 0" ``` eberlm@61608 ` 1289` ``` by (simp add: fps_mod_def Let_def fps_cutoff_zero_iff) ``` eberlm@61608 ` 1290` ``` thus "f dvd g" by (simp add: dvd_eq_mod_eq_0) ``` eberlm@61608 ` 1291` ```qed (simp add: assms dvd_imp_subdegree_le) ``` eberlm@61608 ` 1292` eberlm@63317 ` 1293` ```lemma fps_shift_altdef: ``` eberlm@66480 ` 1294` ``` "fps_shift n f = (f :: 'a :: field fps) div fps_X^n" ``` eberlm@63317 ` 1295` ``` by (simp add: fps_divide_def) ``` eberlm@63317 ` 1296` ``` ``` eberlm@66480 ` 1297` ```lemma fps_div_fps_X_power_nth: "((f :: 'a :: field fps) div fps_X^n) \$ k = f \$ (k + n)" ``` eberlm@63317 ` 1298` ``` by (simp add: fps_shift_altdef [symmetric]) ``` eberlm@63317 ` 1299` eberlm@66480 ` 1300` ```lemma fps_div_fps_X_nth: "((f :: 'a :: field fps) div fps_X) \$ k = f \$ Suc k" ``` eberlm@66480 ` 1301` ``` using fps_div_fps_X_power_nth[of f 1] by simp ``` eberlm@63317 ` 1302` eberlm@61608 ` 1303` ```lemma fps_const_inverse: "inverse (fps_const (a::'a::field)) = fps_const (inverse a)" ``` eberlm@61608 ` 1304` ``` by (cases "a \ 0", rule fps_inverse_unique) (auto simp: fps_eq_iff) ``` eberlm@61608 ` 1305` eberlm@61608 ` 1306` ```lemma fps_const_divide: "fps_const (x :: _ :: field) / fps_const y = fps_const (x / y)" ``` eberlm@61608 ` 1307` ``` by (cases "y = 0") (simp_all add: fps_divide_unit fps_const_inverse divide_inverse) ``` eberlm@61608 ` 1308` hoelzl@62102 ` 1309` ```lemma inverse_fps_numeral: ``` eberlm@61608 ` 1310` ``` "inverse (numeral n :: ('a :: field_char_0) fps) = fps_const (inverse (numeral n))" ``` eberlm@61608 ` 1311` ``` by (intro fps_inverse_unique fps_ext) (simp_all add: fps_numeral_nth) ``` eberlm@61608 ` 1312` eberlm@63317 ` 1313` ```lemma fps_numeral_divide_divide: ``` eberlm@63317 ` 1314` ``` "x / numeral b / numeral c = (x / numeral (b * c) :: 'a :: field fps)" ``` eberlm@63317 ` 1315` ``` by (cases "numeral b = (0::'a)"; cases "numeral c = (0::'a)") ``` eberlm@63317 ` 1316` ``` (simp_all add: fps_divide_unit fps_inverse_mult [symmetric] numeral_fps_const numeral_mult ``` eberlm@63317 ` 1317` ``` del: numeral_mult [symmetric]) ``` eberlm@63317 ` 1318` eberlm@63317 ` 1319` ```lemma fps_numeral_mult_divide: ``` eberlm@63317 ` 1320` ``` "numeral b * x / numeral c = (numeral b / numeral c * x :: 'a :: field fps)" ``` eberlm@63317 ` 1321` ``` by (cases "numeral c = (0::'a)") (simp_all add: fps_divide_unit numeral_fps_const) ``` eberlm@63317 ` 1322` eberlm@63317 ` 1323` ```lemmas fps_numeral_simps = ``` eberlm@63317 ` 1324` ``` fps_numeral_divide_divide fps_numeral_mult_divide inverse_fps_numeral neg_numeral_fps_const ``` eberlm@61608 ` 1325` eberlm@66550 ` 1326` ```lemma subdegree_div: ``` eberlm@66550 ` 1327` ``` assumes "q dvd p" ``` eberlm@66550 ` 1328` ``` shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p - subdegree q" ``` eberlm@66550 ` 1329` ```proof (cases "p = 0") ``` eberlm@66550 ` 1330` ``` case False ``` eberlm@66550 ` 1331` ``` from assms have "p = p div q * q" by simp ``` eberlm@66550 ` 1332` ``` also from assms False have "subdegree \ = subdegree (p div q) + subdegree q" ``` eberlm@66550 ` 1333` ``` by (intro subdegree_mult) (auto simp: dvd_div_eq_0_iff) ``` eberlm@66550 ` 1334` ``` finally show ?thesis by simp ``` eberlm@66550 ` 1335` ```qed simp_all ``` eberlm@66550 ` 1336` eberlm@66550 ` 1337` ```lemma subdegree_div_unit: ``` eberlm@66550 ` 1338` ``` assumes "q \$ 0 \ 0" ``` eberlm@66550 ` 1339` ``` shows "subdegree ((p :: 'a :: field fps) div q) = subdegree p" ``` eberlm@66550 ` 1340` ``` using assms by (subst subdegree_div) simp_all ``` eberlm@66550 ` 1341` eberlm@61608 ` 1342` eberlm@61608 ` 1343` ```subsection \Formal power series form a Euclidean ring\ ``` eberlm@61608 ` 1344` haftmann@64784 ` 1345` ```instantiation fps :: (field) euclidean_ring_cancel ``` eberlm@61608 ` 1346` ```begin ``` eberlm@61608 ` 1347` hoelzl@62102 ` 1348` ```definition fps_euclidean_size_def: ``` eberlm@62422 ` 1349` ``` "euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)" ``` eberlm@61608 ` 1350` haftmann@66806 ` 1351` ```context ``` haftmann@66806 ` 1352` ```begin ``` haftmann@66806 ` 1353` haftmann@66806 ` 1354` ```private lemma fps_divide_cancel_aux1: ``` haftmann@66806 ` 1355` ``` assumes "h\$0 \ (0 :: 'a :: field)" ``` haftmann@66806 ` 1356` ``` shows "(h * f) div (h * g) = f div g" ``` haftmann@66806 ` 1357` ```proof (cases "g = 0") ``` haftmann@66806 ` 1358` ``` assume "g \ 0" ``` haftmann@66806 ` 1359` ``` from assms have "h \ 0" by auto ``` haftmann@66806 ` 1360` ``` note nz [simp] = \g \ 0\ \h \ 0\ ``` haftmann@66806 ` 1361` ``` from assms have [simp]: "subdegree h = 0" by (simp add: subdegree_eq_0_iff) ``` haftmann@66806 ` 1362` haftmann@66806 ` 1363` ``` have "(h * f) div (h * g) = ``` haftmann@66806 ` 1364` ``` fps_shift (subdegree g) (h * f * inverse (fps_shift (subdegree g) (h*g)))" ``` haftmann@66806 ` 1365` ``` by (simp add: fps_divide_def Let_def) ``` haftmann@66806 ` 1366` ``` also have "h * f * inverse (fps_shift (subdegree g) (h*g)) = ``` haftmann@66806 ` 1367` ``` (inverse h * h) * f * inverse (fps_shift (subdegree g) g)" ``` haftmann@66806 ` 1368` ``` by (subst fps_shift_mult) (simp_all add: algebra_simps fps_inverse_mult) ``` haftmann@66806 ` 1369` ``` also from assms have "inverse h * h = 1" by (rule inverse_mult_eq_1) ``` haftmann@66806 ` 1370` ``` finally show "(h * f) div (h * g) = f div g" by (simp_all add: fps_divide_def Let_def) ``` haftmann@66806 ` 1371` ```qed (simp_all add: fps_divide_def) ``` haftmann@66806 ` 1372` haftmann@66806 ` 1373` ```private lemma fps_divide_cancel_aux2: ``` haftmann@66806 ` 1374` ``` "(f * fps_X^m) div (g * fps_X^m) = f div (g :: 'a :: field fps)" ``` haftmann@66806 ` 1375` ```proof (cases "g = 0") ``` haftmann@66806 ` 1376` ``` assume [simp]: "g \ 0" ``` haftmann@66806 ` 1377` ``` have "(f * fps_X^m) div (g * fps_X^m) = ``` haftmann@66806 ` 1378` ``` fps_shift (subdegree g + m) (f*inverse (fps_shift (subdegree g + m) (g*fps_X^m))*fps_X^m)" ``` haftmann@66806 ` 1379` ``` by (simp add: fps_divide_def Let_def algebra_simps) ``` haftmann@66806 ` 1380` ``` also have "... = f div g" ``` haftmann@66806 ` 1381` ``` by (simp add: fps_shift_times_fps_X_power'' fps_divide_def Let_def) ``` haftmann@66806 ` 1382` ``` finally show ?thesis . ``` haftmann@66806 ` 1383` ```qed (simp_all add: fps_divide_def) ``` haftmann@66806 ` 1384` eberlm@61608 ` 1385` ```instance proof ``` eberlm@61608 ` 1386` ``` fix f g :: "'a fps" assume [simp]: "g \ 0" ``` eberlm@61608 ` 1387` ``` show "euclidean_size f \ euclidean_size (f * g)" ``` eberlm@61608 ` 1388` ``` by (cases "f = 0") (auto simp: fps_euclidean_size_def) ``` eberlm@61608 ` 1389` ``` show "euclidean_size (f mod g) < euclidean_size g" ``` eberlm@61608 ` 1390` ``` apply (cases "f = 0", simp add: fps_euclidean_size_def) ``` eberlm@61608 ` 1391` ``` apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]]) ``` eberlm@61608 ` 1392` ``` apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod) ``` eberlm@61608 ` 1393` ``` done ``` haftmann@66806 ` 1394` ``` show "(h * f) div (h * g) = f div g" if "h \ 0" ``` haftmann@66806 ` 1395` ``` for f g h :: "'a fps" ``` haftmann@66806 ` 1396` ``` proof - ``` haftmann@66806 ` 1397` ``` define m where "m = subdegree h" ``` haftmann@66806 ` 1398` ``` define h' where "h' = fps_shift m h" ``` haftmann@66806 ` 1399` ``` have h_decomp: "h = h' * fps_X ^ m" unfolding h'_def m_def by (rule subdegree_decompose) ``` haftmann@66806 ` 1400` ``` from \h \ 0\ have [simp]: "h'\$0 \ 0" by (simp add: h'_def m_def) ``` haftmann@66806 ` 1401` ``` have "(h * f) div (h * g) = (h' * f * fps_X^m) div (h' * g * fps_X^m)" ``` haftmann@66806 ` 1402` ``` by (simp add: h_decomp algebra_simps) ``` haftmann@66806 ` 1403` ``` also have "... = f div g" ``` haftmann@66806 ` 1404` ``` by (simp add: fps_divide_cancel_aux1 fps_divide_cancel_aux2) ``` haftmann@66806 ` 1405` ``` finally show ?thesis . ``` haftmann@66806 ` 1406` ``` qed ``` haftmann@66806 ` 1407` ``` show "(f + g * h) div h = g + f div h" ``` haftmann@66806 ` 1408` ``` if "h \ 0" for f g h :: "'a fps" ``` haftmann@66806 ` 1409` ``` proof - ``` haftmann@66806 ` 1410` ``` define n h' where dfs: "n = subdegree h" "h' = fps_shift n h" ``` haftmann@66806 ` 1411` ``` have "(f + g * h) div h = fps_shift n (f * inverse h') + fps_shift n (g * (h * inverse h'))" ``` haftmann@66806 ` 1412` ``` by (simp add: fps_divide_def Let_def dfs [symmetric] algebra_simps fps_shift_add that) ``` haftmann@66806 ` 1413` ``` also have "h * inverse h' = (inverse h' * h') * fps_X^n" ``` haftmann@66806 ` 1414` ``` by (subst subdegree_decompose) (simp_all add: dfs) ``` haftmann@66806 ` 1415` ``` also have "... = fps_X^n" ``` haftmann@66806 ` 1416` ``` by (subst inverse_mult_eq_1) (simp_all add: dfs that) ``` haftmann@66806 ` 1417` ``` also have "fps_shift n (g * fps_X^n) = g" by simp ``` haftmann@66806 ` 1418` ``` also have "fps_shift n (f * inverse h') = f div h" ``` haftmann@66806 ` 1419` ``` by (simp add: fps_divide_def Let_def dfs) ``` haftmann@66806 ` 1420` ``` finally show ?thesis by simp ``` haftmann@66806 ` 1421` ``` qed ``` eberlm@62422 ` 1422` ```qed (simp_all add: fps_euclidean_size_def) ``` eberlm@61608 ` 1423` eberlm@61608 ` 1424` ```end ``` eberlm@61608 ` 1425` haftmann@66806 ` 1426` ```end ``` haftmann@66806 ` 1427` haftmann@66817 ` 1428` ```instance fps :: (field) normalization_euclidean_semiring .. ``` haftmann@66817 ` 1429` eberlm@61608 ` 1430` ```instantiation fps :: (field) euclidean_ring_gcd ``` eberlm@61608 ` 1431` ```begin ``` haftmann@64786 ` 1432` ```definition fps_gcd_def: "(gcd :: 'a fps \ _) = Euclidean_Algorithm.gcd" ``` haftmann@64786 ` 1433` ```definition fps_lcm_def: "(lcm :: 'a fps \ _) = Euclidean_Algorithm.lcm" ``` haftmann@64786 ` 1434` ```definition fps_Gcd_def: "(Gcd :: 'a fps set \ _) = Euclidean_Algorithm.Gcd" ``` haftmann@64786 ` 1435` ```definition fps_Lcm_def: "(Lcm :: 'a fps set \ _) = Euclidean_Algorithm.Lcm" ``` eberlm@62422 ` 1436` ```instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def) ``` eberlm@61608 ` 1437` ```end ``` eberlm@61608 ` 1438` eberlm@61608 ` 1439` ```lemma fps_gcd: ``` eberlm@61608 ` 1440` ``` assumes [simp]: "f \ 0" "g \ 0" ``` eberlm@66480 ` 1441` ``` shows "gcd f g = fps_X ^ min (subdegree f) (subdegree g)" ``` eberlm@61608 ` 1442` ```proof - ``` eberlm@61608 ` 1443` ``` let ?m = "min (subdegree f) (subdegree g)" ``` eberlm@66480 ` 1444` ``` show "gcd f g = fps_X ^ ?m" ``` eberlm@61608 ` 1445` ``` proof (rule sym, rule gcdI) ``` eberlm@61608 ` 1446` ``` fix d assume "d dvd f" "d dvd g" ``` eberlm@66480 ` 1447` ``` thus "d dvd fps_X ^ ?m" by (cases "d = 0") (auto simp: fps_dvd_iff) ``` eberlm@61608 ` 1448` ``` qed (simp_all add: fps_dvd_iff) ``` eberlm@61608 ` 1449` ```qed ``` eberlm@61608 ` 1450` hoelzl@62102 ` 1451` ```lemma fps_gcd_altdef: "gcd (f :: 'a :: field fps) g = ``` eberlm@61608 ` 1452` ``` (if f = 0 \ g = 0 then 0 else ``` eberlm@66480 ` 1453` ``` if f = 0 then fps_X ^ subdegree g else ``` eberlm@66480 ` 1454` ``` if g = 0 then fps_X ^ subdegree f else ``` eberlm@66480 ` 1455` ``` fps_X ^ min (subdegree f) (subdegree g))" ``` eberlm@61608 ` 1456` ``` by (simp add: fps_gcd) ``` eberlm@61608 ` 1457` eberlm@61608 ` 1458` ```lemma fps_lcm: ``` eberlm@61608 ` 1459` ``` assumes [simp]: "f \ 0" "g \ 0" ``` eberlm@66480 ` 1460` ``` shows "lcm f g = fps_X ^ max (subdegree f) (subdegree g)" ``` eberlm@61608 ` 1461` ```proof - ``` eberlm@61608 ` 1462` ``` let ?m = "max (subdegree f) (subdegree g)" ``` eberlm@66480 ` 1463` ``` show "lcm f g = fps_X ^ ?m" ``` eberlm@61608 ` 1464` ``` proof (rule sym, rule lcmI) ``` eberlm@61608 ` 1465` ``` fix d assume "f dvd d" "g dvd d" ``` eberlm@66480 ` 1466` ``` thus "fps_X ^ ?m dvd d" by (cases "d = 0") (auto simp: fps_dvd_iff) ``` eberlm@61608 ` 1467` ``` qed (simp_all add: fps_dvd_iff) ``` eberlm@61608 ` 1468` ```qed ``` eberlm@61608 ` 1469` hoelzl@62102 ` 1470` ```lemma fps_lcm_altdef: "lcm (f :: 'a :: field fps) g = ``` eberlm@66480 ` 1471` ``` (if f = 0 \ g = 0 then 0 else fps_X ^ max (subdegree f) (subdegree g))" ``` eberlm@61608 ` 1472` ``` by (simp add: fps_lcm) ``` eberlm@61608 ` 1473` eberlm@61608 ` 1474` ```lemma fps_Gcd: ``` eberlm@61608 ` 1475` ``` assumes "A - {0} \ {}" ``` eberlm@66480 ` 1476` ``` shows "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)" ``` eberlm@61608 ` 1477` ```proof (rule sym, rule GcdI) ``` eberlm@61608 ` 1478` ``` fix f assume "f \ A" ``` eberlm@66480 ` 1479` ``` thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f" ``` eberlm@61608 ` 1480` ``` by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower) ``` eberlm@61608 ` 1481` ```next ``` eberlm@61608 ` 1482` ``` fix d assume d: "\f. f \ A \ d dvd f" ``` eberlm@61608 ` 1483` ``` from assms obtain f where "f \ A - {0}" by auto ``` eberlm@61608 ` 1484` ``` with d[of f] have [simp]: "d \ 0" by auto ``` eberlm@61608 ` 1485` ``` from d assms have "subdegree d \ (INF f:A-{0}. subdegree f)" ``` eberlm@61608 ` 1486` ``` by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric]) ``` eberlm@66480 ` 1487` ``` with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff) ``` eberlm@61608 ` 1488` ```qed simp_all ``` eberlm@61608 ` 1489` hoelzl@62102 ` 1490` ```lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) = ``` eberlm@66480 ` 1491` ``` (if A \ {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))" ``` eberlm@61608 ` 1492` ``` using fps_Gcd by auto ``` eberlm@61608 ` 1493` eberlm@61608 ` 1494` ```lemma fps_Lcm: ``` eberlm@61608 ` 1495` ``` assumes "A \ {}" "0 \ A" "bdd_above (subdegree`A)" ``` eberlm@66480 ` 1496` ``` shows "Lcm A = fps_X ^ (SUP f:A. subdegree f)" ``` eberlm@61608 ` 1497` ```proof (rule sym, rule LcmI) ``` eberlm@61608 ` 1498` ``` fix f assume "f \ A" ``` eberlm@61608 ` 1499` ``` moreover from assms(3) have "bdd_above (subdegree ` A)" by auto ``` eberlm@66480 ` 1500` ``` ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2) ``` eberlm@61608 ` 1501` ``` by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper) ``` eberlm@61608 ` 1502` ```next ``` eberlm@61608 ` 1503` ``` fix d assume d: "\f. f \ A \ f dvd d" ``` eberlm@61608 ` 1504` ``` from assms obtain f where f: "f \ A" "f \ 0" by auto ``` eberlm@66480 ` 1505` ``` show "fps_X ^ (SUP f:A. subdegree f) dvd d" ``` eberlm@61608 ` 1506` ``` proof (cases "d = 0") ``` eberlm@61608 ` 1507` ``` assume "d \ 0" ``` eberlm@61608 ` 1508` ``` moreover from d have "\f. f \ A \ f \ 0 \ f dvd d" by blast ``` eberlm@61608 ` 1509` ``` ultimately have "subdegree d \ (SUP f:A. subdegree f)" using assms ``` eberlm@61608 ` 1510` ``` by (intro cSUP_least) (auto simp: fps_dvd_iff) ``` eberlm@61608 ` 1511` ``` with \d \ 0\ show ?thesis by (simp add: fps_dvd_iff) ``` eberlm@61608 ` 1512` ``` qed simp_all ``` eberlm@61608 ` 1513` ```qed simp_all ``` eberlm@61608 ` 1514` eberlm@61608 ` 1515` ```lemma fps_Lcm_altdef: ``` hoelzl@62102 ` 1516` ``` "Lcm (A :: 'a :: field fps set) = ``` eberlm@61608 ` 1517` ``` (if 0 \ A \ \bdd_above (subdegree`A) then 0 else ``` eberlm@66480 ` 1518` ``` if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))" ``` eberlm@61608 ` 1519` ```proof (cases "bdd_above (subdegree`A)") ``` eberlm@61608 ` 1520` ``` assume unbounded: "\bdd_above (subdegree`A)" ``` eberlm@61608 ` 1521` ``` have "Lcm A = 0" ``` eberlm@61608 ` 1522` ``` proof (rule ccontr) ``` eberlm@61608 ` 1523` ``` assume "Lcm A \ 0" ``` eberlm@61608 ` 1524` ``` from unbounded obtain f where f: "f \ A" "subdegree (Lcm A) < subdegree f" ``` eberlm@61608 ` 1525` ``` unfolding bdd_above_def by (auto simp: not_le) ``` wenzelm@63539 ` 1526` ``` moreover from f and \Lcm A \ 0\ have "subdegree f \ subdegree (Lcm A)" ``` eberlm@62422 ` 1527` ``` by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all ``` eberlm@61608 ` 1528` ``` ultimately show False by simp ``` eberlm@61608 ` 1529` ``` qed ``` eberlm@61608 ` 1530` ``` with unbounded show ?thesis by simp ``` eberlm@62422 ` 1531` ```qed (simp_all add: fps_Lcm Lcm_eq_0_I) ``` eberlm@62422 ` 1532` eberlm@61608 ` 1533` wenzelm@54681 ` 1534` wenzelm@60500 ` 1535` ```subsection \Formal Derivatives, and the MacLaurin theorem around 0\ ``` chaieb@29687 ` 1536` chaieb@29687 ` 1537` ```definition "fps_deriv f = Abs_fps (\n. of_nat (n + 1) * f \$ (n + 1))" ``` chaieb@29687 ` 1538` wenzelm@54681 ` 1539` ```lemma fps_deriv_nth[simp]: "fps_deriv f \$ n = of_nat (n +1) * f \$ (n + 1)" ``` wenzelm@48757 ` 1540` ``` by (simp add: fps_deriv_def) ``` wenzelm@48757 ` 1541` eberlm@65398 ` 1542` ```lemma fps_0th_higher_deriv: ``` eberlm@65398 ` 1543` ``` "(fps_deriv ^^ n) f \$ 0 = (fact n * f \$ n :: 'a :: {comm_ring_1, semiring_char_0})" ``` eberlm@65398 ` 1544` ``` by (induction n arbitrary: f) (simp_all del: funpow.simps add: funpow_Suc_right algebra_simps) ``` eberlm@65398 ` 1545` wenzelm@48757 ` 1546` ```lemma fps_deriv_linear[simp]: ``` wenzelm@48757 ` 1547` ``` "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = ``` wenzelm@48757 ` 1548` ``` fps_const a * fps_deriv f + fps_const b * fps_deriv g" ``` haftmann@36350 ` 1549` ``` unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: field_simps) ``` chaieb@29687 ` 1550` huffman@30488 ` 1551` ```lemma fps_deriv_mult[simp]: ``` wenzelm@54681 ` 1552` ``` fixes f :: "'a::comm_ring_1 fps" ``` chaieb@29687 ` 1553` ``` shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" ``` wenzelm@52891 ` 1554` ```proof - ``` chaieb@29687 ` 1555` ``` let ?D = "fps_deriv" ``` wenzelm@60558 ` 1556` ``` have "(f * ?D g + ?D f * g) \$ n = ?D (f*g) \$ n" for n ``` wenzelm@60558 ` 1557` ``` proof - ``` chaieb@29687 ` 1558` ``` let ?Zn = "{0 ..n}" ``` chaieb@29687 ` 1559` ``` let ?Zn1 = "{0 .. n + 1}" ``` chaieb@29687 ` 1560` ``` let ?g = "\i. of_nat (i+1) * g \$ (i+1) * f \$ (n - i) + ``` chaieb@29687 ` 1561` ``` of_nat (i+1)* f \$ (i+1) * g \$ (n - i)" ``` chaieb@29687 ` 1562` ``` let ?h = "\i. of_nat i * g \$ i * f \$ ((n+1) - i) + ``` chaieb@29687 ` 1563` ``` of_nat i* f \$ i * g \$ ((n + 1) - i)" ``` nipkow@64267 ` 1564` ``` have s0: "sum (\i. of_nat i * f \$ i * g \$ (n + 1 - i)) ?Zn1 = ``` nipkow@64267 ` 1565` ``` sum (\i. of_nat (n + 1 - i) * f \$ (n + 1 - i) * g \$ i) ?Zn1" ``` nipkow@64267 ` 1566` ``` by (rule sum.reindex_bij_witness[where i="op - (n + 1)" and j="op - (n + 1)"]) auto ``` nipkow@64267 ` 1567` ``` have s1: "sum (\i. f \$ i * g \$ (n + 1 - i)) ?Zn1 = ``` nipkow@64267 ` 1568` ``` sum (\i. f \$ (n + 1 - i) * g \$ i) ?Zn1" ``` nipkow@64267 ` 1569` ``` by (rule sum.reindex_bij_witness[where i="op - (n + 1)" and j="op - (n + 1)"]) auto ``` wenzelm@52891 ` 1570` ``` have "(f * ?D g + ?D f * g)\$n = (?D g * f + ?D f * g)\$n" ``` haftmann@57512 ` 1571` ``` by (simp only: mult.commute) ``` chaieb@29687 ` 1572` ``` also have "\ = (\i = 0..n. ?g i)" ``` nipkow@64267 ` 1573` ``` by (simp add: fps_mult_nth sum.distrib[symmetric]) ``` nipkow@64267 ` 1574` ``` also have "\ = sum ?h {0..n+1}" ``` nipkow@64267 ` 1575` ``` by (rule sum.reindex_bij_witness_not_neutral ``` hoelzl@57129 ` 1576` ``` [where S'="{}" and T'="{0}" and j="Suc" and i="\i. i - 1"]) auto ``` chaieb@29687 ` 1577` ``` also have "\ = (fps_deriv (f * g)) \$ n" ``` nipkow@64267 ` 1578` ``` apply (simp only: fps_deriv_nth fps_mult_nth sum.distrib) ``` chaieb@29687 ` 1579` ``` unfolding s0 s1 ``` nipkow@64267 ` 1580` ``` unfolding sum.distrib[symmetric] sum_distrib_left ``` nipkow@64267 ` 1581` ``` apply (rule sum.cong) ``` wenzelm@52891 ` 1582` ``` apply (auto simp add: of_nat_diff field_simps) ``` wenzelm@52891 ` 1583` ``` done ``` wenzelm@60558 ` 1584` ``` finally show ?thesis . ``` wenzelm@60558 ` 1585` ``` qed ``` wenzelm@60558 ` 1586` ``` then show ?thesis ``` wenzelm@60558 ` 1587` ``` unfolding fps_eq_iff by auto ``` chaieb@29687 ` 1588` ```qed ``` chaieb@29687 ` 1589` eberlm@66480 ` 1590` ```lemma fps_deriv_fps_X[simp]: "fps_deriv fps_X = 1" ``` eberlm@66480 ` 1591` ``` by (simp add: fps_deriv_def fps_X_def fps_eq_iff) ``` chaieb@31968 ` 1592` wenzelm@54681 ` 1593` ```lemma fps_deriv_neg[simp]: ``` wenzelm@54681 ` 1594` ``` "fps_deriv (- (f:: 'a::comm_ring_1 fps)) = - (fps_deriv f)" ``` huffman@29911 ` 1595` ``` by (simp add: fps_eq_iff fps_deriv_def) ``` wenzelm@52891 ` 1596` wenzelm@54681 ` 1597` ```lemma fps_deriv_add[simp]: ``` wenzelm@54681 ` 1598` ``` "fps_deriv ((f:: 'a::comm_ring_1 fps) + g) = fps_deriv f + fps_deriv g" ``` chaieb@29687 ` 1599` ``` using fps_deriv_linear[of 1 f 1 g] by simp ``` chaieb@29687 ` 1600` wenzelm@54681 ` 1601` ```lemma fps_deriv_sub[simp]: ``` wenzelm@54681 ` 1602` ``` "fps_deriv ((f:: 'a::comm_ring_1 fps) - g) = fps_deriv f - fps_deriv g" ``` haftmann@54230 ` 1603` ``` using fps_deriv_add [of f "- g"] by simp ``` chaieb@29687 ` 1604` chaieb@29687 ` 1605` ```lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0" ``` huffman@29911 ` 1606` ``` by (simp add: fps_ext fps_deriv_def fps_const_def) ``` chaieb@29687 ` 1607` eberlm@65396 ` 1608` ```lemma fps_deriv_of_nat [simp]: "fps_deriv (of_nat n) = 0" ``` eberlm@65396 ` 1609` ``` by (simp add: fps_of_nat [symmetric]) ``` eberlm@65396 ` 1610` eberlm@65396 ` 1611` ```lemma fps_deriv_numeral [simp]: "fps_deriv (numeral n) = 0" ``` eberlm@65396 ` 1612` ``` by (simp add: numeral_fps_const) ``` eberlm@65396 ` 1613` wenzelm@48757 ` 1614` ```lemma fps_deriv_mult_const_left[simp]: ``` wenzelm@54681 ` 1615` ``` "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f" ``` chaieb@29687 ` 1616` ``` by simp ``` chaieb@29687 ` 1617` chaieb@29687 ` 1618` ```lemma fps_deriv_0[simp]: "fps_deriv 0 = 0" ``` chaieb@29687 ` 1619` ``` by (simp add: fps_deriv_def fps_eq_iff) ``` chaieb@29687 ` 1620` chaieb@29687 ` 1621` ```lemma fps_deriv_1[simp]: "fps_deriv 1 = 0" ``` chaieb@29687 ` 1622` ``` by (simp add: fps_deriv_def fps_eq_iff ) ``` chaieb@29687 ` 1623` wenzelm@48757 ` 1624` ```lemma fps_deriv_mult_const_right[simp]: ``` wenzelm@54681 ` 1625` ``` "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c" ``` chaieb@29687 ` 1626` ``` by simp ``` chaieb@29687 ` 1627` nipkow@64267 ` 1628` ```lemma fps_deriv_sum: ``` nipkow@64267 ` 1629` ``` "fps_deriv (sum f S) = sum (\i. fps_deriv (f i :: 'a::comm_ring_1 fps)) S" ``` wenzelm@53195 ` 1630` ```proof (cases "finite S") ``` wenzelm@53195 ` 1631` ``` case False ``` wenzelm@53195 ` 1632` ``` then show ?thesis by simp ``` wenzelm@53195 ` 1633` ```next ``` wenzelm@53195 ` 1634` ``` case True ``` wenzelm@53195 ` 1635` ``` show ?thesis by (induct rule: finite_induct [OF True]) simp_all ``` chaieb@29687 ` 1636` ```qed ``` chaieb@29687 ` 1637` wenzelm@52902 ` 1638` ```lemma fps_deriv_eq_0_iff [simp]: ``` wenzelm@54681 ` 1639` ``` "fps_deriv f = 0 \ f = fps_const (f\$0 :: 'a::{idom,semiring_char_0})" ``` wenzelm@60501 ` 1640` ``` (is "?lhs \ ?rhs") ``` wenzelm@60501 ` 1641` ```proof ``` wenzelm@60501 ` 1642` ``` show ?lhs if ?rhs ``` wenzelm@60501 ` 1643` ``` proof - ``` wenzelm@60501 ` 1644` ``` from that have "fps_deriv f = fps_deriv (fps_const (f\$0))" ``` wenzelm@60501 ` 1645` ``` by simp ``` wenzelm@60501 ` 1646` ``` then show ?thesis ``` wenzelm@60501 ` 1647` ``` by simp ``` wenzelm@60501 ` 1648` ``` qed ``` wenzelm@60501 ` 1649` ``` show ?rhs if ?lhs ``` wenzelm@60501 ` 1650` ``` proof - ``` wenzelm@60501 ` 1651` ``` from that have "\n. (fps_deriv f)\$n = 0" ``` wenzelm@60501 ` 1652` ``` by simp ``` wenzelm@60501 ` 1653` ``` then have "\n. f\$(n+1) = 0" ``` wenzelm@60501 ` 1654` ``` by (simp del: of_nat_Suc of_nat_add One_nat_def) ``` wenzelm@60501 ` 1655` ``` then show ?thesis ``` chaieb@29687 ` 1656` ``` apply (clarsimp simp add: fps_eq_iff fps_const_def) ``` chaieb@29687 ` 1657` ``` apply (erule_tac x="n - 1" in allE) ``` wenzelm@52891 ` 1658` ``` apply simp ``` wenzelm@52891 ` 1659` ``` done ``` wenzelm@60501 ` 1660` ``` qed ``` chaieb@29687 ` 1661` ```qed ``` chaieb@29687 ` 1662` huffman@30488 ` 1663` ```lemma fps_deriv_eq_iff: ``` wenzelm@54681 ` 1664` ``` fixes f :: "'a::{idom,semiring_char_0} fps" ``` chaieb@29687 ` 1665` ``` shows "fps_deriv f = fps_deriv g \ (f = fps_const(f\$0 - g\$0) + g)" ``` wenzelm@52891 ` 1666` ```proof - ``` wenzelm@52903 ` 1667` ``` have "fps_deriv f = fps_deriv g \ fps_deriv (f - g) = 0" ``` wenzelm@52903 ` 1668` ``` by simp ``` wenzelm@54681 ` 1669` ``` also have "\ \ f - g = fps_const ((f - g) \$ 0)" ``` wenzelm@52903 ` 1670` ``` unfolding fps_deriv_eq_0_iff .. ``` wenzelm@60501 ` 1671` ``` finally show ?thesis ``` wenzelm@60501 ` 1672` ``` by (simp add: field_simps) ``` chaieb@29687 ` 1673` ```qed ``` chaieb@29687 ` 1674` wenzelm@48757 ` 1675` ```lemma fps_deriv_eq_iff_ex: ``` wenzelm@54681 ` 1676` ``` "(fps_deriv f = fps_deriv g) \ (\c::'a::{idom,semiring_char_0}. f = fps_const c + g)" ``` wenzelm@53195 ` 1677` ``` by (auto simp: fps_deriv_eq_iff) ``` wenzelm@48757 ` 1678` wenzelm@48757 ` 1679` wenzelm@54681 ` 1680` ```fun fps_nth_deriv :: "nat \ 'a::semiring_1 fps \ 'a fps" ``` wenzelm@48757 ` 1681` ```where ``` chaieb@29687 ` 1682` ``` "fps_nth_deriv 0 f = f" ``` chaieb@29687 ` 1683` ```| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" ``` chaieb@29687 ` 1684` chaieb@29687 ` 1685` ```lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)" ``` wenzelm@48757 ` 1686` ``` by (induct n arbitrary: f) auto ``` wenzelm@48757 ` 1687` wenzelm@48757 ` 1688` ```lemma fps_nth_deriv_linear[simp]: ``` wenzelm@48757 ` 1689` ``` "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = ``` wenzelm@48757 ` 1690` ``` fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g" ``` wenzelm@48757 ` 1691` ``` by (induct n arbitrary: f g) (auto simp add: fps_nth_deriv_commute) ``` wenzelm@48757 ` 1692` wenzelm@48757 ` 1693` ```lemma fps_nth_deriv_neg[simp]: ``` wenzelm@54681 ` 1694` ``` "fps_nth_deriv n (- (f :: 'a::comm_ring_1 fps)) = - (fps_nth_deriv n f)" ``` wenzelm@48757 ` 1695` ``` by (induct n arbitrary: f) simp_all ``` wenzelm@48757 ` 1696` wenzelm@48757 ` 1697` ```lemma fps_nth_deriv_add[simp]: ``` wenzelm@54681 ` 1698` ``` "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g" ``` chaieb@29687 ` 1699` ``` using fps_nth_deriv_linear[of n 1 f 1 g] by simp ``` chaieb@29687 ` 1700` wenzelm@48757 ` 1701` ```lemma fps_nth_deriv_sub[simp]: ``` wenzelm@54681 ` 1702` ``` "fps_nth_deriv n ((f :: 'a::comm_ring_1 fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g" ``` haftmann@54230 ` 1703` ``` using fps_nth_deriv_add [of n f "- g"] by simp ``` chaieb@29687 ` 1704` chaieb@29687 ` 1705` ```lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0" ``` wenzelm@48757 ` 1706` ``` by (induct n) simp_all ``` chaieb@29687 ` 1707` chaieb@29687 ` 1708` ```lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)" ``` wenzelm@48757 ` 1709` ``` by (induct n) simp_all ``` wenzelm@48757 ` 1710` wenzelm@48757 ` 1711` ```lemma fps_nth_deriv_const[simp]: ``` wenzelm@48757 ` 1712` ``` "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)" ``` wenzelm@48757 ` 1713` ``` by (cases n) simp_all ``` wenzelm@48757 ` 1714` wenzelm@48757 ` 1715` ```lemma fps_nth_deriv_mult_const_left[simp]: ``` wenzelm@48757 ` 1716` ``` "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f" ``` chaieb@29687 ` 1717` ``` using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp ``` chaieb@29687 ` 1718` wenzelm@48757 ` 1719` ```lemma fps_nth_deriv_mult_const_right[simp]: ``` wenzelm@48757 ` 1720` ``` "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c" ``` haftmann@57512 ` 1721` ``` using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult.commute) ``` chaieb@29687 ` 1722` nipkow@64267 ` 1723` ```lemma fps_nth_deriv_sum: ``` nipkow@64267 ` 1724` ``` "fps_nth_deriv n (sum f S) = sum (\i. fps_nth_deriv n (f i :: 'a::comm_ring_1 fps)) S" ``` wenzelm@52903 ` 1725` ```proof (cases "finite S") ``` wenzelm@52903 ` 1726` ``` case True ``` wenzelm@52903 ` 1727` ``` show ?thesis by (induct rule: finite_induct [OF True]) simp_all ``` wenzelm@52903 ` 1728` ```next ``` wenzelm@52903 ` 1729` ``` case False ``` wenzelm@52903 ` 1730` ``` then show ?thesis by simp ``` chaieb@29687 ` 1731` ```qed ``` chaieb@29687 ` 1732` wenzelm@48757 ` 1733` ```lemma fps_deriv_maclauren_0: ``` wenzelm@54681 ` 1734` ``` "(fps_nth_deriv k (f :: 'a::comm_semiring_1 fps)) \$ 0 = of_nat (fact k) * f \$ k" ``` haftmann@63417 ` 1735` ``` by (induct k arbitrary: f) (auto simp add: field_simps) ``` chaieb@29687 ` 1736` wenzelm@54681 ` 1737` wenzelm@60500 ` 1738` ```subsection \Powers\ ``` chaieb@29687 ` 1739` chaieb@29687 ` 1740` ```lemma fps_power_zeroth_eq_one: "a\$0 =1 \ a^n \$ 0 = (1::'a::semiring_1)" ``` wenzelm@48757 ` 1741` ``` by (induct n) (auto simp add: expand_fps_eq fps_mult_nth) ``` chaieb@29687 ` 1742` wenzelm@54681 ` 1743` ```lemma fps_power_first_eq: "(a :: 'a::comm_ring_1 fps) \$ 0 =1 \ a^n \$ 1 = of_nat n * a\$1" ``` wenzelm@52891 ` 1744` ```proof (induct n) ``` wenzelm@52891 ` 1745` ``` case 0 ``` wenzelm@52891 ` 1746` ``` then show ?case by simp ``` chaieb@29687 ` 1747` ```next ``` chaieb@29687 ` 1748` ``` case (Suc n) ``` huffman@30488 ` 1749` ``` show ?case unfolding power_Suc fps_mult_nth ``` wenzelm@60501 ` 1750` ``` using Suc.hyps[OF \a\$0 = 1\] \a\$0 = 1\ fps_power_zeroth_eq_one[OF \a\$0=1\] ``` wenzelm@52891 ` 1751` ``` by (simp add: field_simps) ``` chaieb@29687 ` 1752` ```qed ``` chaieb@29687 ` 1753` chaieb@29687 ` 1754` ```lemma startsby_one_power:"a \$ 0 = (1::'a::comm_ring_1) \ a^n \$ 0 = 1" ``` wenzelm@48757 ` 1755` ``` by (induct n) (auto simp add: fps_mult_nth) ``` chaieb@29687 ` 1756` chaieb@29687 ` 1757` ```lemma startsby_zero_power:"a \$0 = (0::'a::comm_ring_1) \ n > 0 \ a^n \$0 = 0" ``` wenzelm@48757 ` 1758` ``` by (induct n) (auto simp add: fps_mult_nth) ``` chaieb@29687 ` 1759` wenzelm@54681 ` 1760` ```lemma startsby_power:"a \$0 = (v::'a::comm_ring_1) \ a^n \$0 = v^n" ``` wenzelm@52891 ` 1761` ``` by (induct n) (auto simp add: fps_mult_nth) ``` wenzelm@52891 ` 1762` wenzelm@54681 ` 1763` ```lemma startsby_zero_power_iff[simp]: "a^n \$0 = (0::'a::idom) \ n \ 0 \ a\$0 = 0" ``` wenzelm@52891 ` 1764` ``` apply (rule iffI) ``` wenzelm@52891 ` 1765` ``` apply (induct n) ``` wenzelm@52891 ` 1766` ``` apply (auto simp add: fps_mult_nth) ``` wenzelm@52891 ` 1767` ``` apply (rule startsby_zero_power, simp_all) ``` wenzelm@52891 ` 1768` ``` done ``` chaieb@29687 ` 1769` huffman@30488 ` 1770` ```lemma startsby_zero_power_prefix: ``` wenzelm@60501 ` 1771` ``` assumes a0: "a \$ 0 = (0::'a::idom)" ``` chaieb@29687 ` 1772` ``` shows "\n < k. a ^ k \$ n = 0" ``` huffman@30488 ` 1773` ``` using a0 ``` wenzelm@54681 ` 1774` ```proof (induct k rule: nat_less_induct) ``` wenzelm@52891 ` 1775` ``` fix k ``` wenzelm@54681 ` 1776` ``` assume H: "\m (\nm = (\i = 0..m. a ^ l \$ i * a \$ (m - i))" ``` wenzelm@60501 ` 1793` ``` by (simp add: fps_mult_nth) ``` wenzelm@60501 ` 1794` ``` also have "\ = 0" ``` nipkow@64267 ` 1795` ``` apply (rule sum.neutral) ``` wenzelm@60501 ` 1796` ``` apply auto ``` wenzelm@60501 ` 1797` ``` apply (case_tac "x = m") ``` wenzelm@60501 ` 1798` ``` using a0 apply simp ``` wenzelm@60501 ` 1799` ``` apply (rule H[rule_format]) ``` wenzelm@60501 ` 1800` ``` using a0 Suc mk apply auto ``` wenzelm@60501 ` 1801` ``` done ``` wenzelm@60501 ` 1802` ``` finally show ?thesis . ``` wenzelm@60501 ` 1803` ``` qed ``` wenzelm@60501 ` 1804` ``` then show ?thesis by blast ``` wenzelm@60501 ` 1805` ``` qed ``` chaieb@29687 ` 1806` ```qed ``` chaieb@29687 ` 1807` nipkow@64267 ` 1808` ```lemma startsby_zero_sum_depends: ``` wenzelm@54681 ` 1809` ``` assumes a0: "a \$0 = (0::'a::idom)" ``` wenzelm@54681 ` 1810` ``` and kn: "n \ k" ``` nipkow@64267 ` 1811` ``` shows "sum (\i. (a ^ i)\$k) {0 .. n} = sum (\i. (a ^ i)\$k) {0 .. k}" ``` nipkow@64267 ` 1812` ``` apply (rule sum.mono_neutral_right) ``` wenzelm@54681 ` 1813` ``` using kn ``` wenzelm@54681 ` 1814` ``` apply auto ``` chaieb@29687 ` 1815` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` wenzelm@52891 ` 1816` ``` apply arith ``` wenzelm@52891 ` 1817` ``` done ``` wenzelm@52891 ` 1818` wenzelm@52891 ` 1819` ```lemma startsby_zero_power_nth_same: ``` wenzelm@54681 ` 1820` ``` assumes a0: "a\$0 = (0::'a::idom)" ``` chaieb@29687 ` 1821` ``` shows "a^n \$ n = (a\$1) ^ n" ``` wenzelm@52891 ` 1822` ```proof (induct n) ``` wenzelm@52891 ` 1823` ``` case 0 ``` wenzelm@52902 ` 1824` ``` then show ?case by simp ``` chaieb@29687 ` 1825` ```next ``` chaieb@29687 ` 1826` ``` case (Suc n) ``` wenzelm@54681 ` 1827` ``` have "a ^ Suc n \$ (Suc n) = (a^n * a)\$(Suc n)" ``` wenzelm@54681 ` 1828` ``` by (simp add: field_simps) ``` nipkow@64267 ` 1829` ``` also have "\ = sum (\i. a^n\$i * a \$ (Suc n - i)) {0.. Suc n}" ``` wenzelm@52891 ` 1830` ``` by (simp add: fps_mult_nth) ``` nipkow@64267 ` 1831` ``` also have "\ = sum (\i. a^n\$i * a \$ (Suc n - i)) {n .. Suc n}" ``` nipkow@64267 ` 1832` ``` apply (rule sum.mono_neutral_right) ``` chaieb@29687 ` 1833` ``` apply simp ``` chaieb@29687 ` 1834` ``` apply clarsimp ``` chaieb@29687 ` 1835` ``` apply clarsimp ``` chaieb@29687 ` 1836` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` chaieb@29687 ` 1837` ``` apply arith ``` chaieb@29687 ` 1838` ``` done ``` wenzelm@54681 ` 1839` ``` also have "\ = a^n \$ n * a\$1" ``` wenzelm@54681 ` 1840` ``` using a0 by simp ``` wenzelm@54681 ` 1841` ``` finally show ?case ``` wenzelm@54681 ` 1842` ``` using Suc.hyps by simp ``` chaieb@29687 ` 1843` ```qed ``` chaieb@29687 ` 1844` chaieb@29687 ` 1845` ```lemma fps_inverse_power: ``` wenzelm@54681 ` 1846` ``` fixes a :: "'a::field fps" ``` chaieb@29687 ` 1847` ``` shows "inverse (a^n) = inverse a ^ n" ``` eberlm@61608 ` 1848` ``` by (induction n) (simp_all add: fps_inverse_mult) ``` chaieb@29687 ` 1849` wenzelm@48757 ` 1850` ```lemma fps_deriv_power: ``` wenzelm@54681 ` 1851` ``` "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)" ``` wenzelm@48757 ` 1852` ``` apply (induct n) ``` wenzelm@52891 ` 1853` ``` apply (auto simp add: field_simps fps_const_add[symmetric] simp del: fps_const_add) ``` wenzelm@48757 ` 1854` ``` apply (case_tac n) ``` wenzelm@52891 ` 1855` ``` apply (auto simp add: field_simps) ``` wenzelm@48757 ` 1856` ``` done ``` chaieb@29687 ` 1857` huffman@30488 ` 1858` ```lemma fps_inverse_deriv: ``` wenzelm@54681 ` 1859` ``` fixes a :: "'a::field fps" ``` chaieb@29687 ` 1860` ``` assumes a0: "a\$0 \ 0" ``` wenzelm@53077 ` 1861` ``` shows "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2" ``` wenzelm@54681 ` 1862` ```proof - ``` chaieb@29687 ` 1863` ``` from inverse_mult_eq_1[OF a0] ``` chaieb@29687 ` 1864` ``` have "fps_deriv (inverse a * a) = 0" by simp ``` wenzelm@54452 ` 1865` ``` then have "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" ``` wenzelm@54452 ` 1866` ``` by simp ``` wenzelm@54452 ` 1867` ``` then have "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" ``` wenzelm@54452 ` 1868` ``` by simp ``` chaieb@29687 ` 1869` ``` with inverse_mult_eq_1[OF a0] ``` wenzelm@53077 ` 1870` ``` have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) = 0" ``` chaieb@29687 ` 1871` ``` unfolding power2_eq_square ``` haftmann@36350 ` 1872` ``` apply (simp add: field_simps) ``` haftmann@57512 ` 1873` ``` apply (simp add: mult.assoc[symmetric]) ``` wenzelm@52903 ` 1874` ``` done ``` wenzelm@53077 ` 1875` ``` then have "(inverse a)\<^sup>2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * (inverse a)\<^sup>2 = ``` wenzelm@53077 ` 1876` ``` 0 - fps_deriv a * (inverse a)\<^sup>2" ``` chaieb@29687 ` 1877` ``` by simp ``` wenzelm@53077 ` 1878` ``` then show "fps_deriv (inverse a) = - fps_deriv a * (inverse a)\<^sup>2" ``` wenzelm@52902 ` 1879` ``` by (simp add: field_simps) ``` chaieb@29687 ` 1880` ```qed ``` chaieb@29687 ` 1881` huffman@30488 ` 1882` ```lemma fps_inverse_deriv': ``` wenzelm@54681 ` 1883` ``` fixes a :: "'a::field fps" ``` wenzelm@60501 ` 1884` ``` assumes a0: "a \$ 0 \ 0" ``` wenzelm@53077 ` 1885` ``` shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2" ``` eberlm@61608 ` 1886` ``` using fps_inverse_deriv[OF a0] a0 ``` eberlm@61608 ` 1887` ``` by (simp add: fps_divide_unit power2_eq_square fps_inverse_mult) ``` chaieb@29687 ` 1888` wenzelm@52902 ` 1889` ```lemma inverse_mult_eq_1': ``` wenzelm@52902 ` 1890` ``` assumes f0: "f\$0 \ (0::'a::field)" ``` wenzelm@60567 ` 1891` ``` shows "f * inverse f = 1" ``` haftmann@57512 ` 1892` ``` by (metis mult.commute inverse_mult_eq_1 f0) ``` chaieb@29687 ` 1893` eberlm@63317 ` 1894` ```lemma fps_inverse_minus [simp]: "inverse (-f) = -inverse (f :: 'a :: field fps)" ``` eberlm@63317 ` 1895` ``` by (cases "f\$0 = 0") (auto intro: fps_inverse_unique simp: inverse_mult_eq_1' fps_inverse_eq_0) ``` eberlm@63317 ` 1896` ``` ``` eberlm@63317 ` 1897` ```lemma divide_fps_const [simp]: "f / fps_const (c :: 'a :: field) = fps_const (inverse c) * f" ``` eberlm@63317 ` 1898` ``` by (cases "c = 0") (simp_all add: fps_divide_unit fps_const_inverse) ``` eberlm@63317 ` 1899` eberlm@66480 ` 1900` ```(* FIfps_XME: The last part of this proof should go through by simp once we have a proper ``` eberlm@61804 ` 1901` ``` theorem collection for simplifying division on rings *) ``` wenzelm@52902 ` 1902` ```lemma fps_divide_deriv: ``` eberlm@61804 ` 1903` ``` assumes "b dvd (a :: 'a :: field fps)" ``` eberlm@61804 ` 1904` ``` shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b^2" ``` eberlm@61804 ` 1905` ```proof - ``` eberlm@61804 ` 1906` ``` have eq_divide_imp: "c \ 0 \ a * c = b \ a = b div c" for a b c :: "'a :: field fps" ``` eberlm@61804 ` 1907` ``` by (drule sym) (simp add: mult.assoc) ``` eberlm@61804 ` 1908` ``` from assms have "a = a / b * b" by simp ``` eberlm@61804 ` 1909` ``` also have "fps_deriv (a / b * b) = fps_deriv (a / b) * b + a / b * fps_deriv b" by simp ``` eberlm@61804 ` 1910` ``` finally have "fps_deriv (a / b) * b^2 = fps_deriv a * b - a * fps_deriv b" using assms ``` eberlm@61804 ` 1911` ``` by (simp add: power2_eq_square algebra_simps) ``` eberlm@61804 ` 1912` ``` thus ?thesis by (cases "b = 0") (auto simp: eq_divide_imp) ``` eberlm@61804 ` 1913` ```qed ``` chaieb@29687 ` 1914` eberlm@66480 ` 1915` ```lemma fps_inverse_gp': "inverse (Abs_fps (\n. 1::'a::field)) = 1 - fps_X" ``` eberlm@66480 ` 1916` ``` by (simp add: fps_inverse_gp fps_eq_iff fps_X_def) ``` eberlm@66480 ` 1917` eberlm@66480 ` 1918` ```lemma fps_one_over_one_minus_fps_X_squared: ``` eberlm@66480 ` 1919` ``` "inverse ((1 - fps_X)^2 :: 'a :: field fps) = Abs_fps (\n. of_nat (n+1))" ``` eberlm@63317 ` 1920` ```proof - ``` eberlm@66480 ` 1921` ``` have "inverse ((1 - fps_X)^2 :: 'a fps) = fps_deriv (inverse (1 - fps_X))" ``` eberlm@63317 ` 1922` ``` by (subst fps_inverse_deriv) (simp_all add: fps_inverse_power) ``` eberlm@66480 ` 1923` ``` also have "inverse (1 - fps_X :: 'a fps) = Abs_fps (\_. 1)" ``` eberlm@63317 ` 1924` ``` by (subst fps_inverse_gp' [symmetric]) simp ``` eberlm@63317 ` 1925` ``` also have "fps_deriv \ = Abs_fps (\n. of_nat (n + 1))" ``` eberlm@63317 ` 1926` ``` by (simp add: fps_deriv_def) ``` eberlm@63317 ` 1927` ``` finally show ?thesis . ``` eberlm@63317 ` 1928` ```qed ``` eberlm@63317 ` 1929` eberlm@66480 ` 1930` ```lemma fps_nth_deriv_fps_X[simp]: "fps_nth_deriv n fps_X = (if n = 0 then fps_X else if n=1 then 1 else 0)" ``` wenzelm@52902 ` 1931` ``` by (cases n) simp_all ``` chaieb@29687 ` 1932` eberlm@66480 ` 1933` ```lemma fps_inverse_fps_X_plus1: "inverse (1 + fps_X) = Abs_fps (\n. (- (1::'a::field)) ^ n)" ``` wenzelm@60501 ` 1934` ``` (is "_ = ?r") ``` wenzelm@54681 ` 1935` ```proof - ``` eberlm@66480 ` 1936` ``` have eq: "(1 + fps_X) * ?r = 1" ``` chaieb@29687 ` 1937` ``` unfolding minus_one_power_iff ``` haftmann@36350 ` 1938` ``` by (auto simp add: field_simps fps_eq_iff) ``` wenzelm@54681 ` 1939` ``` show ?thesis ``` wenzelm@54681 ` 1940` ``` by (auto simp add: eq intro: fps_inverse_unique) ``` chaieb@29687 ` 1941` ```qed ``` chaieb@29687 ` 1942` huffman@30488 ` 1943` wenzelm@60501 ` 1944` ```subsection \Integration\ ``` huffman@31273 ` 1945` wenzelm@52903 ` 1946` ```definition fps_integral :: "'a::field_char_0 fps \ 'a \ 'a fps" ``` wenzelm@52903 ` 1947` ``` where "fps_integral a a0 = Abs_fps (\n. if n = 0 then a0 else (a\$(n - 1) / of_nat n))" ``` chaieb@29687 ` 1948` huffman@31273 ` 1949` ```lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a" ``` huffman@31273 ` 1950` ``` unfolding fps_integral_def fps_deriv_def ``` huffman@31273 ` 1951` ``` by (simp add: fps_eq_iff del: of_nat_Suc) ``` chaieb@29687 ` 1952` huffman@31273 ` 1953` ```lemma fps_integral_linear: ``` huffman@31273 ` 1954` ``` "fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) = ``` huffman@31273 ` 1955` ``` fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0" ``` huffman@31273 ` 1956` ``` (is "?l = ?r") ``` wenzelm@53195 ` 1957` ```proof - ``` wenzelm@54681 ` 1958` ``` have "fps_deriv ?l = fps_deriv ?r" ``` wenzelm@54681 ` 1959` ``` by (simp add: fps_deriv_fps_integral) ``` wenzelm@54681 ` 1960` ``` moreover have "?l\$0 = ?r\$0" ``` wenzelm@54681 ` 1961` ``` by (simp add: fps_integral_def) ``` chaieb@29687 ` 1962` ``` ultimately show ?thesis ``` chaieb@29687 ` 1963` ``` unfolding fps_deriv_eq_iff by auto ``` chaieb@29687 ` 1964` ```qed ``` huffman@30488 ` 1965` wenzelm@53195 ` 1966` wenzelm@60500 ` 1967` ```subsection \Composition of FPSs\ ``` wenzelm@53195 ` 1968` wenzelm@60501 ` 1969` ```definition fps_compose :: "'a::semiring_1 fps \ 'a fps \ 'a fps" (infixl "oo" 55) ``` nipkow@64267 ` 1970` ``` where "a oo b = Abs_fps (\n. sum (\i. a\$i * (b^i\$n)) {0..n})" ``` nipkow@64267 ` 1971` nipkow@64267 ` 1972` ```lemma fps_compose_nth: "(a oo b)\$n = sum (\i. a\$i * (b^i\$n)) {0..n}" ``` wenzelm@48757 ` 1973` ``` by (simp add: fps_compose_def) ``` chaieb@29687 ` 1974` eberlm@61608 ` 1975` ```lemma fps_compose_nth_0 [simp]: "(f oo g) \$ 0 = f \$ 0" ``` eberlm@61608 ` 1976` ``` by (simp add: fps_compose_nth) ``` eberlm@61608 ` 1977` eberlm@66480 ` 1978` ```lemma fps_compose_fps_X[simp]: "a oo fps_X = (a :: 'a::comm_ring_1 fps)" ``` nipkow@64267 ` 1979` ``` by (simp add: fps_ext fps_compose_def mult_delta_right sum.delta') ``` huffman@30488 ` 1980` wenzelm@60501 ` 1981` ```lemma fps_const_compose[simp]: "fps_const (a::'a::comm_ring_1) oo b = fps_const a" ``` nipkow@64267 ` 1982` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left sum.delta) ``` chaieb@29687 ` 1983` wenzelm@54681 ` 1984` ```lemma numeral_compose[simp]: "(numeral k :: 'a::comm_ring_1 fps) oo b = numeral k" ``` huffman@47108 ` 1985` ``` unfolding numeral_fps_const by simp ``` huffman@47108 ` 1986` wenzelm@54681 ` 1987` ```lemma neg_numeral_compose[simp]: "(- numeral k :: 'a::comm_ring_1 fps) oo b = - numeral k" ``` huffman@47108 ` 1988` ``` unfolding neg_numeral_fps_const by simp ``` chaieb@31369 ` 1989` eberlm@66480 ` 1990` ```lemma fps_X_fps_compose_startby0[simp]: "a\$0 = 0 \ fps_X oo a = (a :: 'a::comm_ring_1 fps)" ``` nipkow@64267 ` 1991` ``` by (simp add: fps_eq_iff fps_compose_def mult_delta_left sum.delta not_le) ``` chaieb@29687 ` 1992` chaieb@29687 ` 1993` wenzelm@60500 ` 1994` ```subsection \Rules from Herbert Wilf's Generatingfunctionology\ ``` wenzelm@60500 ` 1995` wenzelm@60500 ` 1996` ```subsubsection \Rule 1\ ``` nipkow@64267 ` 1997` ``` (* {a_{n+k}}_0^infty Corresponds to (f - sum (\i. a_i * x^i))/x^h, for h>0*) ``` chaieb@29687 ` 1998` huffman@30488 ` 1999` ```lemma fps_power_mult_eq_shift: ``` eberlm@66480 ` 2000` ``` "fps_X^Suc k * Abs_fps (\n. a (n + Suc k)) = ``` eberlm@66480 ` 2001` ``` Abs_fps a - sum (\i. fps_const (a i :: 'a::comm_ring_1) * fps_X^i) {0 .. k}" ``` wenzelm@52902 ` 2002` ``` (is "?lhs = ?rhs") ``` wenzelm@52902 ` 2003` ```proof - ``` wenzelm@60501 ` 2004` ``` have "?lhs \$ n = ?rhs \$ n" for n :: nat ``` wenzelm@60501 ` 2005` ``` proof - ``` huffman@30488 ` 2006` ``` have "?lhs \$ n = (if n < Suc k then 0 else a n)" ``` eberlm@66480 ` 2007` ``` unfolding fps_X_power_mult_nth by auto ``` chaieb@29687 ` 2008` ``` also have "\ = ?rhs \$ n" ``` wenzelm@52902 ` 2009` ``` proof (induct k) ``` wenzelm@52902 ` 2010` ``` case 0 ``` wenzelm@60501 ` 2011` ``` then show ?case ``` nipkow@64267 ` 2012` ``` by (simp add: fps_sum_nth) ``` chaieb@29687 ` 2013` ``` next ``` chaieb@29687 ` 2014` ``` case (Suc k) ``` eberlm@66480 ` 2015` ``` have "(Abs_fps a - sum (\i. fps_const (a i :: 'a) * fps_X^i) {0 .. Suc k})\$n = ``` eberlm@66480 ` 2016` ``` (Abs_fps a - sum (\i. fps_const (a i :: 'a) * fps_X^i) {0 .. k} - ``` eberlm@66480 ` 2017` ``` fps_const (a (Suc k)) * fps_X^ Suc k) \$ n" ``` wenzelm@52902 ` 2018` ``` by (simp add: field_simps) ``` eberlm@66480 ` 2019` ``` also have "\ = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * fps_X^ Suc k)\$n" ``` wenzelm@60501 ` 2020` ``` using Suc.hyps[symmetric] unfolding fps_sub_nth by simp ``` chaieb@29687 ` 2021` ``` also have "\ = (if n < Suc (Suc k) then 0 else a n)" ``` eberlm@66480 ` 2022` ``` unfolding fps_X_power_mult_right_nth ``` wenzelm@32960 ` 2023` ``` apply (auto simp add: not_less fps_const_def) ``` wenzelm@32960 ` 2024` ``` apply (rule cong[of a a, OF refl]) ``` wenzelm@52902 ` 2025` ``` apply arith ``` wenzelm@52902 ` 2026` ``` done ``` wenzelm@60501 ` 2027` ``` finally show ?case ``` wenzelm@60501 ` 2028` ``` by simp ``` chaieb@29687 ` 2029` ``` qed ``` wenzelm@60501 ` 2030` ``` finally show ?thesis . ``` wenzelm@60501 ` 2031` ``` qed ``` wenzelm@60501 ` 2032` ``` then show ?thesis ``` wenzelm@60501 ` 2033` ``` by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2034` ```qed ``` chaieb@29687 ` 2035` wenzelm@53195 ` 2036` wenzelm@60500 ` 2037` ```subsubsection \Rule 2\ ``` chaieb@29687 ` 2038` chaieb@29687 ` 2039` ``` (* We can not reach the form of Wilf, but still near to it using rewrite rules*) ``` huffman@30488 ` 2040` ``` (* If f reprents {a_n} and P is a polynomial, then ``` chaieb@29687 ` 2041` ``` P(xD) f represents {P(n) a_n}*) ``` chaieb@29687 ` 2042` eberlm@66480 ` 2043` ```definition "fps_XD = op * fps_X \ fps_deriv" ``` eberlm@66480 ` 2044` eberlm@66480 ` 2045` ```lemma fps_XD_add[simp]:"fps_XD (a + b) = fps_XD a + fps_XD (b :: 'a::comm_ring_1 fps)" ``` eberlm@66480 ` 2046` ``` by (simp add: fps_XD_def field_simps) ``` eberlm@66480 ` 2047` eberlm@66480 ` 2048` ```lemma fps_XD_mult_const[simp]:"fps_XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * fps_XD a" ``` eberlm@66480 ` 2049` ``` by (simp add: fps_XD_def field_simps) ``` eberlm@66480 ` 2050` eberlm@66480 ` 2051` ```lemma fps_XD_linear[simp]: "fps_XD (fps_const c * a + fps_const d * b) = ``` eberlm@66480 ` 2052` ``` fps_const c * fps_XD a + fps_const d * fps_XD (b :: 'a::comm_ring_1 fps)" ``` chaieb@29687 ` 2053` ``` by simp ``` chaieb@29687 ` 2054` eberlm@66480 ` 2055` ```lemma fps_XDN_linear: ``` eberlm@66480 ` 2056` ``` "(fps_XD ^^ n) (fps_const c * a + fps_const d * b) = ``` eberlm@66480 ` 2057` ``` fps_const c * (fps_XD ^^ n) a + fps_const d * (fps_XD ^^ n) (b :: 'a::comm_ring_1 fps)" ``` wenzelm@48757 ` 2058` ``` by (induct n) simp_all ``` chaieb@29687 ` 2059` eberlm@66480 ` 2060` ```lemma fps_mult_fps_X_deriv_shift: "fps_X* fps_deriv a = Abs_fps (\n. of_nat n* a\$n)" ``` wenzelm@52902 ` 2061` ``` by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2062` eberlm@66480 ` 2063` ```lemma fps_mult_fps_XD_shift: ``` eberlm@66480 ` 2064` ``` "(fps_XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\n. (of_nat n ^ k) * a\$n)" ``` eberlm@66480 ` 2065` ``` by (induct k arbitrary: a) (simp_all add: fps_XD_def fps_eq_iff field_simps del: One_nat_def) ``` chaieb@29687 ` 2066` wenzelm@53195 ` 2067` wenzelm@60501 ` 2068` ```subsubsection \Rule 3\ ``` wenzelm@60501 ` 2069` wenzelm@61585 ` 2070` ```text \Rule 3 is trivial and is given by \fps_times_def\.\ ``` wenzelm@60501 ` 2071` wenzelm@60500 ` 2072` eberlm@66480 ` 2073` ```subsubsection \Rule 5 --- summation and "division" by (1 - fps_X)\ ``` eberlm@66480 ` 2074` eberlm@66480 ` 2075` ```lemma fps_divide_fps_X_minus1_sum_lemma: ``` eberlm@66480 ` 2076` ``` "a = ((1::'a::comm_ring_1 fps) - fps_X) * Abs_fps (\n. sum (\i. a \$ i) {0..n})" ``` wenzelm@53195 ` 2077` ```proof - ``` nipkow@64267 ` 2078` ``` let ?sa = "Abs_fps (\n. sum (\i. a \$ i) {0..n})" ``` eberlm@66480 ` 2079` ``` have th0: "\i. (1 - (fps_X::'a fps)) \$ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" ``` wenzelm@52902 ` 2080` ``` by simp ``` eberlm@66480 ` 2081` ``` have "a\$n = ((1 - fps_X) * ?sa) \$ n" for n ``` wenzelm@60501 ` 2082` ``` proof (cases "n = 0") ``` wenzelm@60501 ` 2083` ``` case True ``` wenzelm@60501 ` 2084` ``` then show ?thesis ``` wenzelm@60501 ` 2085` ``` by (simp add: fps_mult_nth) ``` wenzelm@60501 ` 2086` ``` next ``` wenzelm@60501 ` 2087` ``` case False ``` wenzelm@60501 ` 2088` ``` then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1} \ {2..n} = {1..n}" ``` wenzelm@60501 ` 2089` ``` "{0..n - 1} \ {n} = {0..n}" ``` wenzelm@60501 ` 2090` ``` by (auto simp: set_eq_iff) ``` wenzelm@60501 ` 2091` ``` have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" "{0..n - 1} \ {n} = {}" ``` wenzelm@60501 ` 2092` ``` using False by simp_all ``` wenzelm@60501 ` 2093` ``` have f: "finite {0}" "finite {1}" "finite {2 .. n}" ``` wenzelm@60501 ` 2094` ``` "finite {0 .. n - 1}" "finite {n}" by simp_all ``` eberlm@66480 ` 2095` ``` have "((1 - fps_X) * ?sa) \$ n = sum (\i. (1 - fps_X)\$ i * ?sa \$ (n - i)) {0 .. n}" ``` wenzelm@60501 ` 2096` ``` by (simp add: fps_mult_nth) ``` wenzelm@60501 ` 2097` ``` also have "\ = a\$n" ``` wenzelm@60501 ` 2098` ``` unfolding th0 ``` nipkow@64267 ` 2099` ``` unfolding sum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] ``` nipkow@64267 ` 2100` ``` unfolding sum.union_disjoint[OF f(2) f(3) d(2)] ``` wenzelm@60501 ` 2101` ``` apply (simp) ``` nipkow@64267 ` 2102` ``` unfolding sum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] ``` wenzelm@60501 ` 2103` ``` apply simp ``` wenzelm@60501 ` 2104` ``` done ``` wenzelm@60501 ` 2105` ``` finally show ?thesis ``` wenzelm@60501 ` 2106` ``` by simp ``` wenzelm@60501 ` 2107` ``` qed ``` wenzelm@54681 ` 2108` ``` then show ?thesis ``` wenzelm@54681 ` 2109` ``` unfolding fps_eq_iff by blast ``` chaieb@29687 ` 2110` ```qed ``` chaieb@29687 ` 2111` eberlm@66480 ` 2112` ```lemma fps_divide_fps_X_minus1_sum: ``` eberlm@66480 ` 2113` ``` "a /((1::'a::field fps) - fps_X) = Abs_fps (\n. sum (\i. a \$ i) {0..n})" ``` wenzelm@52902 ` 2114` ```proof - ``` eberlm@66480 ` 2115` ``` let ?fps_X = "1 - (fps_X::'a fps)" ``` eberlm@66480 ` 2116` ``` have th0: "?fps_X \$ 0 \ 0" ``` wenzelm@54681 ` 2117` ``` by simp ``` eberlm@66480 ` 2118` ``` have "a /?fps_X = ?fps_X * Abs_fps (\n::nat. sum (op \$ a) {0..n}) * inverse ?fps_X" ``` eberlm@66480 ` 2119` ``` using fps_divide_fps_X_minus1_sum_lemma[of a, symmetric] th0 ``` haftmann@57512 ` 2120` ``` by (simp add: fps_divide_def mult.assoc) ``` eberlm@66480 ` 2121` ``` also have "\ = (inverse ?fps_X * ?fps_X) * Abs_fps (\n::nat. sum (op \$ a) {0..n}) " ``` haftmann@57514 ` 2122` ``` by (simp add: ac_simps) ``` wenzelm@54681 ` 2123` ``` finally show ?thesis ``` wenzelm@54681 ` 2124` ``` by (simp add: inverse_mult_eq_1[OF th0]) ``` chaieb@29687 ` 2125` ```qed ``` chaieb@29687 ` 2126` wenzelm@53195 ` 2127` wenzelm@60501 ` 2128` ```subsubsection \Rule 4 in its more general form: generalizes Rule 3 for an arbitrary ``` wenzelm@60500 ` 2129` ``` finite product of FPS, also the relvant instance of powers of a FPS\ ``` chaieb@29687 ` 2130` nipkow@63882 ` 2131` ```definition "natpermute n k = {l :: nat list. length l = k \ sum_list l = n}" ``` chaieb@29687 ` 2132` chaieb@29687 ` 2133` ```lemma natlist_trivial_1: "natpermute n 1 = {[n]}" ``` chaieb@29687 ` 2134` ``` apply (auto simp add: natpermute_def) ``` wenzelm@52902 ` 2135` ``` apply (case_tac x) ``` wenzelm@52902 ` 2136` ``` apply auto ``` chaieb@29687 ` 2137` ``` done ``` chaieb@29687 ` 2138` chaieb@29687 ` 2139` ```lemma append_natpermute_less_eq: ``` wenzelm@54452 ` 2140` ``` assumes "xs @ ys \ natpermute n k" ``` nipkow@63882 ` 2141` ``` shows "sum_list xs \ n" ``` nipkow@63882 ` 2142` ``` and "sum_list ys \ n" ``` wenzelm@52902 ` 2143` ```proof - ``` nipkow@63882 ` 2144` ``` from assms have "sum_list (xs @ ys) = n" ``` wenzelm@54452 ` 2145` ``` by (simp add: natpermute_def) ``` nipkow@63882 ` 2146` ``` then have "sum_list xs + sum_list ys = n" ``` wenzelm@54452 ` 2147` ``` by simp ``` nipkow@63882 ` 2148` ``` then show "sum_list xs \ n" and "sum_list ys \ n" ``` wenzelm@54452 ` 2149` ``` by simp_all ``` chaieb@29687 ` 2150` ```qed ``` chaieb@29687 ` 2151` chaieb@29687 ` 2152` ```lemma natpermute_split: ``` wenzelm@54452 ` 2153` ``` assumes "h \ k" ``` wenzelm@52902 ` 2154` ``` shows "natpermute n k = ``` wenzelm@52902 ` 2155` ``` (\m \{0..n}. {l1 @ l2 |l1 l2. l1 \ natpermute m h \ l2 \ natpermute (n - m) (k - h)})" ``` wenzelm@60558 ` 2156` ``` (is "?L = ?R" is "_ = (\m \{0..n}. ?S m)") ``` wenzelm@60558 ` 2157` ```proof ``` wenzelm@60558 ` 2158` ``` show "?R \ ?L" ``` wenzelm@60558 ` 2159` ``` proof ``` wenzelm@52902 ` 2160` ``` fix l ``` wenzelm@52902 ` 2161` ``` assume l: "l \ ?R" ``` wenzelm@52902 ` 2162` ``` from l obtain m xs ys where h: "m \ {0..n}" ``` wenzelm@52902 ` 2163` ``` and xs: "xs \ natpermute m h" ``` wenzelm@52902 ` 2164` ``` and ys: "ys \ natpermute (n - m) (k - h)" ``` wenzelm@52902 ` 2165` ``` and leq: "l = xs@ys" by blast ``` nipkow@63882 ` 2166` ``` from xs have xs': "sum_list xs = m" ``` wenzelm@52902 ` 2167` ``` by (simp add: natpermute_def) ``` nipkow@63882 ` 2168` ``` from ys have ys': "sum_list ys = n - m" ``` wenzelm@52902 ` 2169` ``` by (simp add: natpermute_def) ``` wenzelm@60558 ` 2170` ``` show "l \ ?L" using leq xs ys h ``` haftmann@46131 ` 2171` ``` apply (clarsimp simp add: natpermute_def) ``` chaieb@29687 ` 2172` ``` unfolding xs' ys' ``` wenzelm@54452 ` 2173` ``` using assms xs ys ``` wenzelm@48757 ` 2174` ``` unfolding natpermute_def ``` wenzelm@48757 ` 2175` ``` apply simp ``` wenzelm@48757 ` 2176` ``` done ``` wenzelm@60558 ` 2177` ``` qed ``` wenzelm@60558 ` 2178` ``` show "?L \ ?R" ``` wenzelm@60558 ` 2179` ``` proof ``` wenzelm@52902 ` 2180` ``` fix l ``` wenzelm@52902 ` 2181` ``` assume l: "l \ natpermute n k" ``` chaieb@29687 ` 2182` ``` let ?xs = "take h l" ``` chaieb@29687 ` 2183` ``` let ?ys = "drop h l" ``` nipkow@63882 ` 2184` ``` let ?m = "sum_list ?xs" ``` nipkow@63882 ` 2185` ``` from l have ls: "sum_list (?xs @ ?ys) = n" ``` wenzelm@52902 ` 2186` ``` by (simp add: natpermute_def) ``` wenzelm@54452 ` 2187` ``` have xs: "?xs \ natpermute ?m h" using l assms ``` wenzelm@52902 ` 2188` ``` by (simp add: natpermute_def) ``` nipkow@63882 ` 2189` ``` have l_take_drop: "sum_list l = sum_list (take h l @ drop h l)" ``` wenzelm@52902 ` 2190` ``` by simp ``` wenzelm@52902 ` 2191` ``` then have ys: "?ys \ natpermute (n - ?m) (k - h)" ``` wenzelm@54452 ` 2192` ``` using l assms ls by (auto simp add: natpermute_def simp del: append_take_drop_id) ``` wenzelm@52902 ` 2193` ``` from ls have m: "?m \ {0..n}" ``` wenzelm@52902 ` 2194` ``` by (simp add: l_take_drop del: append_take_drop_id) ``` wenzelm@60558 ` 2195` ``` from xs ys ls show "l \ ?R" ``` chaieb@29687 ` 2196` ``` apply auto ``` wenzelm@52902 ` 2197` ``` apply (rule bexI [where x = "?m"]) ``` wenzelm@52902 ` 2198` ``` apply (rule exI [where x = "?xs"]) ``` wenzelm@52902 ` 2199` ``` apply (rule exI [where x = "?ys"]) ``` wenzelm@52891 ` 2200` ``` using ls l ``` haftmann@46131 ` 2201` ``` apply (auto simp add: natpermute_def l_take_drop simp del: append_take_drop_id) ``` wenzelm@48757 ` 2202` ``` apply simp ``` wenzelm@48757 ` 2203` ``` done ``` wenzelm@60558 ` 2204` ``` qed ``` chaieb@29687 ` 2205` ```qed ``` chaieb@29687 ` 2206` chaieb@29687 ` 2207` ```lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" ``` chaieb@29687 ` 2208` ``` by (auto simp add: natpermute_def) ``` wenzelm@52902 ` 2209` chaieb@29687 ` 2210` ```lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" ``` chaieb@29687 ` 2211` ``` apply (auto simp add: set_replicate_conv_if natpermute_def) ``` chaieb@29687 ` 2212` ``` apply (rule nth_equalityI) ``` wenzelm@48757 ` 2213` ``` apply simp_all ``` wenzelm@48757 ` 2214` ``` done ``` chaieb@29687 ` 2215` chaieb@29687 ` 2216` ```lemma natpermute_finite: "finite (natpermute n k)" ``` wenzelm@52902 ` 2217` ```proof (induct k arbitrary: n) ``` wenzelm@52902 ` 2218` ``` case 0 ``` wenzelm@52902 ` 2219` ``` then show ?case ``` chaieb@29687 ` 2220` ``` apply (subst natpermute_split[of 0 0, simplified]) ``` wenzelm@52902 ` 2221` ``` apply (simp add: natpermute_0) ``` wenzelm@52902 ` 2222` ``` done ``` chaieb@29687 ` 2223` ```next ``` chaieb@29687 ` 2224` ``` case (Suc k) ``` wenzelm@52902 ` 2225` ``` then show ?case unfolding natpermute_split [of k "Suc k", simplified] ``` chaieb@29687 ` 2226` ``` apply - ``` chaieb@29687 ` 2227` ``` apply (rule finite_UN_I) ``` chaieb@29687 ` 2228` ``` apply simp ``` chaieb@29687 ` 2229` ``` unfolding One_nat_def[symmetric] natlist_trivial_1 ``` chaieb@29687 ` 2230` ``` apply simp ``` chaieb@29687 ` 2231` ``` done ``` chaieb@29687 ` 2232` ```qed ``` chaieb@29687 ` 2233` chaieb@29687 ` 2234` ```lemma natpermute_contain_maximal: ``` wenzelm@60558 ` 2235` ``` "{xs \ natpermute n (k + 1). n \ set xs} = (\i\{0 .. k}. {(replicate (k + 1) 0) [i:=n]})" ``` chaieb@29687 ` 2236` ``` (is "?A = ?B") ``` wenzelm@60558 ` 2237` ```proof ``` wenzelm@60558 ` 2238` ``` show "?A \ ?B" ``` wenzelm@60558 ` 2239` ``` proof ``` wenzelm@52902 ` 2240` ``` fix xs ``` wenzelm@60558 ` 2241` ``` assume "xs \ ?A" ``` wenzelm@60558 ` 2242` ``` then have H: "xs \ natpermute n (k + 1)" and n: "n \ set xs" ``` wenzelm@60558 ` 2243` ``` by blast+ ``` wenzelm@60558 ` 2244` ``` then obtain i where i: "i \ {0.. k}" "xs!i = n" ``` huffman@30488 ` 2245` ``` unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def) ``` wenzelm@52902 ` 2246` ``` have eqs: "({0..k} - {i}) \ {i} = {0..k}" ``` wenzelm@52902 ` 2247` ``` using i by auto ``` wenzelm@52902 ` 2248` ``` have f: "finite({0..k} - {i})" "finite {i}" ``` wenzelm@52902 ` 2249` ``` by auto ``` wenzelm@52902 ` 2250` ``` have d: "({0..k} - {i}) \ {i} = {}" ``` wenzelm@52902 ` 2251` ``` using i by auto ``` nipkow@64267 ` 2252` ``` from H have "n = sum (nth xs) {0..k}" ``` wenzelm@52902 ` 2253` ``` apply (simp add: natpermute_def) ``` nipkow@64267 ` 2254` ``` apply (auto simp add: atLeastLessThanSuc_atLeastAtMost sum_list_sum_nth) ``` wenzelm@52902 ` 2255` ``` done ``` nipkow@64267 ` 2256` ``` also have "\ = n + sum (nth xs) ({0..k} - {i})" ``` nipkow@64267 ` 2257` ``` unfolding sum.union_disjoint[OF f d, unfolded eqs] using i by simp ``` wenzelm@52902 ` 2258` ``` finally have zxs: "\ j\ {0..k} - {i}. xs!j = 0" ``` wenzelm@52902 ` 2259` ``` by auto ``` wenzelm@52902 ` 2260` ``` from H have xsl: "length xs = k+1" ``` wenzelm@52902 ` 2261` ``` by (simp add: natpermute_def) ``` chaieb@29687 ` 2262` ``` from i have i': "i < length (replicate (k+1) 0)" "i < k+1" ``` wenzelm@52902 ` 2263` ``` unfolding length_replicate by presburger+ ``` chaieb@29687 ` 2264` ``` have "xs = replicate (k+1) 0 [i := n]" ``` chaieb@29687 ` 2265` ``` apply (rule nth_equalityI) ``` chaieb@29687 ` 2266` ``` unfolding xsl length_list_update length_replicate ``` chaieb@29687 ` 2267` ``` apply simp ``` chaieb@29687 ` 2268` ``` apply clarify ``` chaieb@29687 ` 2269` ``` unfolding nth_list_update[OF i'(1)] ``` chaieb@29687 ` 2270` ``` using i zxs ``` wenzelm@52902 ` 2271` ``` apply (case_tac "ia = i") ``` wenzelm@52902 ` 2272` ``` apply (auto simp del: replicate.simps) ``` wenzelm@52902 ` 2273` ``` done ``` wenzelm@60558 ` 2274` ``` then show "xs \ ?B" using i by blast ``` wenzelm@60558 ` 2275` ``` qed ``` wenzelm@60558 ` 2276` ``` show "?B \ ?A" ``` wenzelm@60558 ` 2277` ``` proof ``` wenzelm@60558 ` 2278` ``` fix xs ``` wenzelm@60558 ` 2279` ``` assume "xs \ ?B" ``` wenzelm@60558 ` 2280` ``` then obtain i where i: "i \ {0..k}" and xs: "xs = replicate (k + 1) 0 [i:=n]" ``` wenzelm@60558 ` 2281` ``` by auto ``` wenzelm@60558 ` 2282` ``` have nxs: "n \ set xs" ``` wenzelm@60558 ` 2283` ``` unfolding xs ``` wenzelm@52902 ` 2284` ``` apply (rule set_update_memI) ``` wenzelm@52902 ` 2285` ``` using i apply simp ``` wenzelm@52902 ` 2286` ``` done ``` wenzelm@60558 ` 2287` ``` have xsl: "length xs = k + 1" ``` wenzelm@60558 ` 2288` ``` by (simp only: xs length_replicate length_list_update) ``` nipkow@64267 ` 2289` ``` have "sum_list xs = sum (nth xs) {0.. = sum (\j. if j = i then n else 0) {0..< k+1}" ``` nipkow@64267 ` 2292` ``` by (rule sum.cong) (simp_all add: xs del: replicate.simps) ``` nipkow@64267 ` 2293` ``` also have "\ = n" using i by (simp add: sum.delta) ``` wenzelm@60558 ` 2294` ``` finally have "xs \ natpermute n (k + 1)" ``` wenzelm@52902 ` 2295` ``` using xsl unfolding natpermute_def mem_Collect_eq by blast ``` wenzelm@60558 ` 2296` ``` then show "xs \ ?A" ``` wenzelm@60558 ` 2297` ``` using nxs by blast ``` wenzelm@60558 ` 2298` ``` qed ``` chaieb@29687 ` 2299` ```qed ``` chaieb@29687 ` 2300` wenzelm@60558 ` 2301` ```text \The general form.\ ``` nipkow@64272 ` 2302` ```lemma fps_prod_nth: ``` wenzelm@52902 ` 2303` ``` fixes m :: nat ``` wenzelm@54681 ` 2304` ``` and a :: "nat \ 'a::comm_ring_1 fps" ``` nipkow@64272 ` 2305` ``` shows "(prod a {0 .. m}) \$ n = ``` nipkow@64272 ` 2306` ``` sum (\v. prod (\j. (a j) \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` chaieb@29687 ` 2307` ``` (is "?P m n") ``` wenzelm@52902 ` 2308` ```proof (induct m arbitrary: n rule: nat_less_induct) ``` chaieb@29687 ` 2309` ``` fix m n assume H: "\m' < m. \n. ?P m' n" ``` wenzelm@53196 ` 2310` ``` show "?P m n" ``` wenzelm@53196 ` 2311` ``` proof (cases m) ``` wenzelm@53196 ` 2312` ``` case 0 ``` wenzelm@53196 ` 2313` ``` then show ?thesis ``` wenzelm@53196 ` 2314` ``` apply simp ``` wenzelm@53196 ` 2315` ``` unfolding natlist_trivial_1[where n = n, unfolded One_nat_def] ``` wenzelm@53196 ` 2316` ``` apply simp ``` wenzelm@53196 ` 2317` ``` done ``` wenzelm@53196 ` 2318` ``` next ``` wenzelm@53196 ` 2319` ``` case (Suc k) ``` wenzelm@53196 ` 2320` ``` then have km: "k < m" by arith ``` wenzelm@52902 ` 2321` ``` have u0: "{0 .. k} \ {m} = {0..m}" ``` wenzelm@54452 ` 2322` ``` using Suc by (simp add: set_eq_iff) presburger ``` chaieb@29687 ` 2323` ``` have f0: "finite {0 .. k}" "finite {m}" by auto ``` wenzelm@53196 ` 2324` ``` have d0: "{0 .. k} \ {m} = {}" using Suc by auto ``` nipkow@64272 ` 2325` ``` have "(prod a {0 .. m}) \$ n = (prod a {0 .. k} * a m) \$ n" ``` nipkow@64272 ` 2326` ``` unfolding prod.union_disjoint[OF f0 d0, unfolded u0] by simp ``` chaieb@29687 ` 2327` ``` also have "\ = (\i = 0..n. (\v\natpermute i (k + 1). \j\{0..k}. a j \$ v ! j) * a m \$ (n - i))" ``` chaieb@29687 ` 2328` ``` unfolding fps_mult_nth H[rule_format, OF km] .. ``` chaieb@29687 ` 2329` ``` also have "\ = (\v\natpermute n (m + 1). \j\{0..m}. a j \$ v ! j)" ``` wenzelm@53196 ` 2330` ``` apply (simp add: Suc) ``` wenzelm@48757 ` 2331` ``` unfolding natpermute_split[of m "m + 1", simplified, of n, ``` wenzelm@53196 ` 2332` ``` unfolded natlist_trivial_1[unfolded One_nat_def] Suc] ``` nipkow@64267 ` 2333` ``` apply (subst sum.UNION_disjoint) ``` huffman@30488 ` 2334` ``` apply simp ``` chaieb@29687 ` 2335` ``` apply simp ``` chaieb@29687 ` 2336` ``` unfolding image_Collect[symmetric] ``` chaieb@29687 ` 2337` ``` apply clarsimp ``` chaieb@29687 ` 2338` ``` apply (rule finite_imageI) ``` chaieb@29687 ` 2339` ``` apply (rule natpermute_finite) ``` nipkow@39302 ` 2340` ``` apply (clarsimp simp add: set_eq_iff) ``` chaieb@29687 ` 2341` ``` apply auto ``` nipkow@64267 ` 2342` ``` apply (rule sum.cong) ``` haftmann@57418 ` 2343` ``` apply (rule refl) ``` nipkow@64267 ` 2344` ``` unfolding sum_distrib_right ``` chaieb@29687 ` 2345` ``` apply (rule sym) ``` nipkow@64267 ` 2346` ``` apply (rule_tac l = "\xs. xs @ [n - x]" in sum.reindex_cong) ``` chaieb@29687 ` 2347` ``` apply (simp add: inj_on_def) ``` chaieb@29687 ` 2348` ``` apply auto ``` nipkow@64272 ` 2349` ``` unfolding prod.union_disjoint[OF f0 d0, unfolded u0, unfolded Suc] ``` chaieb@29687 ` 2350` ``` apply (clarsimp simp add: natpermute_def nth_append) ``` chaieb@29687 ` 2351` ``` done ``` wenzelm@53196 ` 2352` ``` finally show ?thesis . ``` wenzelm@53196 ` 2353` ``` qed ``` chaieb@29687 ` 2354` ```qed ``` chaieb@29687 ` 2355` wenzelm@60558 ` 2356` ```text \The special form for powers.\ ``` chaieb@29687 ` 2357` ```lemma fps_power_nth_Suc: ``` wenzelm@52903 ` 2358` ``` fixes m :: nat ``` wenzelm@54681 ` 2359` ``` and a :: "'a::comm_ring_1 fps" ``` nipkow@64272 ` 2360` ``` shows "(a ^ Suc m)\$n = sum (\v. prod (\j. a \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` wenzelm@52902 ` 2361` ```proof - ``` nipkow@64272 ` 2362` ``` have th0: "a^Suc m = prod (\i. a) {0..m}" ``` nipkow@64272 ` 2363` ``` by (simp add: prod_constant) ``` nipkow@64272 ` 2364` ``` show ?thesis unfolding th0 fps_prod_nth .. ``` chaieb@29687 ` 2365` ```qed ``` wenzelm@52902 ` 2366` chaieb@29687 ` 2367` ```lemma fps_power_nth: ``` wenzelm@54452 ` 2368` ``` fixes m :: nat ``` wenzelm@54681 ` 2369` ``` and a :: "'a::comm_ring_1 fps" ``` wenzelm@53196 ` 2370` ``` shows "(a ^m)\$n = ``` nipkow@64272 ` 2371` ``` (if m=0 then 1\$n else sum (\v. prod (\j. a \$ (v!j)) {0..m - 1}) (natpermute n m))" ``` wenzelm@52902 ` 2372` ``` by (cases m) (simp_all add: fps_power_nth_Suc del: power_Suc) ``` chaieb@29687 ` 2373` huffman@30488 ` 2374` ```lemma fps_nth_power_0: ``` wenzelm@54452 ` 2375` ``` fixes m :: nat ``` wenzelm@54681 ` 2376` ``` and a :: "'a::comm_ring_1 fps" ``` chaieb@29687 ` 2377` ``` shows "(a ^m)\$0 = (a\$0) ^ m" ``` wenzelm@53195 ` 2378` ```proof (cases m) ``` wenzelm@53195 ` 2379` ``` case 0 ``` wenzelm@53195 ` 2380` ``` then show ?thesis by simp ``` wenzelm@53195 ` 2381` ```next ``` wenzelm@53195 ` 2382` ``` case (Suc n) ``` wenzelm@53195 ` 2383` ``` then have c: "m = card {0..n}" by simp ``` nipkow@64272 ` 2384` ``` have "(a ^m)\$0 = prod (\i. a\$0) {0..n}" ``` wenzelm@53195 ` 2385` ``` by (simp add: Suc fps_power_nth del: replicate.simps power_Suc) ``` wenzelm@53195 ` 2386` ``` also have "\ = (a\$0) ^ m" ``` nipkow@64272 ` 2387` ``` unfolding c by (rule prod_constant) ``` wenzelm@53195 ` 2388` ``` finally show ?thesis . ``` chaieb@29687 ` 2389` ```qed ``` chaieb@29687 ` 2390` eberlm@63317 ` 2391` ```lemma natpermute_max_card: ``` eberlm@63317 ` 2392` ``` assumes n0: "n \ 0" ``` eberlm@63317 ` 2393` ``` shows "card {xs \ natpermute n (k + 1). n \ set xs} = k + 1" ``` eberlm@63317 ` 2394` ``` unfolding natpermute_contain_maximal ``` eberlm@63317 ` 2395` ```proof - ``` eberlm@63317 ` 2396` ``` let ?A = "\i. {replicate (k + 1) 0[i := n]}" ``` eberlm@63317 ` 2397` ``` let ?K = "{0 ..k}" ``` eberlm@63317 ` 2398` ``` have fK: "finite ?K" ``` eberlm@63317 ` 2399` ``` by simp ``` eberlm@63317 ` 2400` ``` have fAK: "\i\?K. finite (?A i)" ``` eberlm@63317 ` 2401` ``` by auto ``` eberlm@63317 ` 2402` ``` have d: "\i\ ?K. \j\ ?K. i \ j \ ``` eberlm@63317 ` 2403` ``` {replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` eberlm@63317 ` 2404` ``` proof clarify ``` eberlm@63317 ` 2405` ``` fix i j ``` eberlm@63317 ` 2406` ``` assume i: "i \ ?K" and j: "j \ ?K" and ij: "i \ j" ``` eberlm@63317 ` 2407` ``` have False if eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" ``` eberlm@63317 ` 2408` ``` proof - ``` eberlm@63317 ` 2409` ``` have "(replicate (k+1) 0 [i:=n] ! i) = n" ``` eberlm@63317 ` 2410` ``` using i by (simp del: replicate.simps) ``` eberlm@63317 ` 2411` ``` moreover ``` eberlm@63317 ` 2412` ``` have "(replicate (k+1) 0 [j:=n] ! i) = 0" ``` eberlm@63317 ` 2413` ``` using i ij by (simp del: replicate.simps) ``` eberlm@63317 ` 2414` ``` ultimately show ?thesis ``` eberlm@63317 ` 2415` ``` using eq n0 by (simp del: replicate.simps) ``` eberlm@63317 ` 2416` ``` qed ``` eberlm@63317 ` 2417` ``` then show "{replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` eberlm@63317 ` 2418` ``` by auto ``` eberlm@63317 ` 2419` ``` qed ``` eberlm@63317 ` 2420` ``` from card_UN_disjoint[OF fK fAK d] ``` eberlm@63317 ` 2421` ``` show "card (\i\{0..k}. {replicate (k + 1) 0[i := n]}) = k + 1" ``` eberlm@63317 ` 2422` ``` by simp ``` eberlm@63317 ` 2423` ```qed ``` eberlm@63317 ` 2424` eberlm@63317 ` 2425` ```lemma fps_power_Suc_nth: ``` eberlm@63317 ` 2426` ``` fixes f :: "'a :: comm_ring_1 fps" ``` eberlm@63317 ` 2427` ``` assumes k: "k > 0" ``` eberlm@63317 ` 2428` ``` shows "(f ^ Suc m) \$ k = ``` eberlm@63317 ` 2429` ``` of_nat (Suc m) * (f \$ k * (f \$ 0) ^ m) + ``` eberlm@63317 ` 2430` ``` (\v\{v\natpermute k (m+1). k \ set v}. \j = 0..m. f \$ v ! j)" ``` eberlm@63317 ` 2431` ```proof - ``` eberlm@63317 ` 2432` ``` define A B ``` eberlm@63317 ` 2433` ``` where "A = {v\natpermute k (m+1). k \ set v}" ``` eberlm@63317 ` 2434` ``` and "B = {v\natpermute k (m+1). k \ set v}" ``` eberlm@63317 ` 2435` ``` have [simp]: "finite A" "finite B" "A \ B = {}" by (auto simp: A_def B_def natpermute_finite) ``` eberlm@63317 ` 2436` eberlm@63317 ` 2437` ``` from natpermute_max_card[of k m] k have card_A: "card A = m + 1" by (simp add: A_def) ``` eberlm@63317 ` 2438` ``` { ``` eberlm@63317 ` 2439` ``` fix v assume v: "v \ A" ``` eberlm@63317 ` 2440` ``` from v have [simp]: "length v = Suc m" by (simp add: A_def natpermute_def) ``` eberlm@63317 ` 2441` ``` from v have "\j. j \ m \ v ! j = k" ``` eberlm@63317 ` 2442` ``` by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le) ``` eberlm@63317 ` 2443` ``` then guess j by (elim exE conjE) note j = this ``` eberlm@63317 ` 2444` ``` ``` nipkow@63882 ` 2445` ``` from v have "k = sum_list v" by (simp add: A_def natpermute_def) ``` eberlm@63317 ` 2446` ``` also have "\ = (\i=0..m. v ! i)" ``` nipkow@64267 ` 2447` ``` by (simp add: sum_list_sum_nth atLeastLessThanSuc_atLeastAtMost del: sum_op_ivl_Suc) ``` eberlm@63317 ` 2448` ``` also from j have "{0..m} = insert j ({0..m}-{j})" by auto ``` eberlm@63317 ` 2449` ``` also from j have "(\i\\. v ! i) = k + (\i\{0..m}-{j}. v ! i)" ``` nipkow@64267 ` 2450` ``` by (subst sum.insert) simp_all ``` eberlm@63317 ` 2451` ``` finally have "(\i\{0..m}-{j}. v ! i) = 0" by simp ``` eberlm@63317 ` 2452` ``` hence zero: "v ! i = 0" if "i \ {0..m}-{j}" for i using that ``` nipkow@64267 ` 2453` ``` by (subst (asm) sum_eq_0_iff) auto ``` eberlm@63317 ` 2454` ``` ``` eberlm@63317 ` 2455` ``` from j have "{0..m} = insert j ({0..m} - {j})" by auto ``` eberlm@63317 ` 2456` ``` also from j have "(\i\\. f \$ (v ! i)) = f \$ k * (\i\{0..m} - {j}. f \$ (v ! i))" ``` nipkow@64272 ` 2457` ``` by (subst prod.insert) auto ``` eberlm@63317 ` 2458` ``` also have "(\i\{0..m} - {j}. f \$ (v ! i)) = (\i\{0..m} - {j}. f \$ 0)" ``` nipkow@64272 ` 2459` ``` by (intro prod.cong) (simp_all add: zero) ``` nipkow@64272 ` 2460` ``` also from j have "\ = (f \$ 0) ^ m" by (subst prod_constant) simp_all ``` eberlm@63317 ` 2461` ``` finally have "(\j = 0..m. f \$ (v ! j)) = f \$ k * (f \$ 0) ^ m" . ```