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