src/HOL/Library/Formal_Power_Series.thy
 author huffman Thu Jun 11 09:03:24 2009 -0700 (2009-06-11) changeset 31563 ded2364d14d4 parent 31370 a551bbe49659 child 31776 151c3f5f28f9 permissions -rw-r--r--
cleaned up some proofs
 chaieb@29687 ` 1` ```(* Title: Formal_Power_Series.thy ``` chaieb@29687 ` 2` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29687 ` 3` ```*) ``` chaieb@29687 ` 4` chaieb@29687 ` 5` ```header{* A formalization of formal power series *} ``` chaieb@29687 ` 6` chaieb@29687 ` 7` ```theory Formal_Power_Series ``` huffman@31273 ` 8` ```imports Main Fact Parity Rational ``` chaieb@29687 ` 9` ```begin ``` chaieb@29687 ` 10` huffman@29906 ` 11` ```subsection {* The type of formal power series*} ``` chaieb@29687 ` 12` huffman@29911 ` 13` ```typedef (open) 'a fps = "{f :: nat \ 'a. True}" ``` huffman@29911 ` 14` ``` morphisms fps_nth Abs_fps ``` chaieb@29687 ` 15` ``` by simp ``` chaieb@29687 ` 16` huffman@29911 ` 17` ```notation fps_nth (infixl "\$" 75) ``` huffman@29911 ` 18` huffman@29911 ` 19` ```lemma expand_fps_eq: "p = q \ (\n. p \$ n = q \$ n)" ``` huffman@29911 ` 20` ``` by (simp add: fps_nth_inject [symmetric] expand_fun_eq) ``` huffman@29911 ` 21` huffman@29911 ` 22` ```lemma fps_ext: "(\n. p \$ n = q \$ n) \ p = q" ``` huffman@29911 ` 23` ``` by (simp add: expand_fps_eq) ``` huffman@29911 ` 24` huffman@29911 ` 25` ```lemma fps_nth_Abs_fps [simp]: "Abs_fps f \$ n = f n" ``` huffman@29911 ` 26` ``` by (simp add: Abs_fps_inverse) ``` huffman@29911 ` 27` chaieb@29687 ` 28` ```text{* Definition of the basic elements 0 and 1 and the basic operations of addition, negation and multiplication *} ``` chaieb@29687 ` 29` chaieb@29687 ` 30` ```instantiation fps :: (zero) zero ``` chaieb@29687 ` 31` ```begin ``` chaieb@29687 ` 32` huffman@29911 ` 33` ```definition fps_zero_def: ``` huffman@29911 ` 34` ``` "0 = Abs_fps (\n. 0)" ``` huffman@29911 ` 35` chaieb@29687 ` 36` ```instance .. ``` chaieb@29687 ` 37` ```end ``` chaieb@29687 ` 38` huffman@29911 ` 39` ```lemma fps_zero_nth [simp]: "0 \$ n = 0" ``` huffman@29911 ` 40` ``` unfolding fps_zero_def by simp ``` huffman@29911 ` 41` chaieb@29687 ` 42` ```instantiation fps :: ("{one,zero}") one ``` chaieb@29687 ` 43` ```begin ``` chaieb@29687 ` 44` huffman@29911 ` 45` ```definition fps_one_def: ``` huffman@29911 ` 46` ``` "1 = Abs_fps (\n. if n = 0 then 1 else 0)" ``` huffman@29911 ` 47` chaieb@29687 ` 48` ```instance .. ``` chaieb@29687 ` 49` ```end ``` chaieb@29687 ` 50` huffman@30488 ` 51` ```lemma fps_one_nth [simp]: "1 \$ n = (if n = 0 then 1 else 0)" ``` huffman@29911 ` 52` ``` unfolding fps_one_def by simp ``` huffman@29911 ` 53` chaieb@29687 ` 54` ```instantiation fps :: (plus) plus ``` chaieb@29687 ` 55` ```begin ``` chaieb@29687 ` 56` huffman@29911 ` 57` ```definition fps_plus_def: ``` huffman@29911 ` 58` ``` "op + = (\f g. Abs_fps (\n. f \$ n + g \$ n))" ``` huffman@29911 ` 59` chaieb@29687 ` 60` ```instance .. ``` chaieb@29687 ` 61` ```end ``` chaieb@29687 ` 62` huffman@29911 ` 63` ```lemma fps_add_nth [simp]: "(f + g) \$ n = f \$ n + g \$ n" ``` huffman@29911 ` 64` ``` unfolding fps_plus_def by simp ``` huffman@29911 ` 65` huffman@29911 ` 66` ```instantiation fps :: (minus) minus ``` chaieb@29687 ` 67` ```begin ``` chaieb@29687 ` 68` huffman@29911 ` 69` ```definition fps_minus_def: ``` huffman@29911 ` 70` ``` "op - = (\f g. Abs_fps (\n. f \$ n - g \$ n))" ``` huffman@29911 ` 71` chaieb@29687 ` 72` ```instance .. ``` chaieb@29687 ` 73` ```end ``` chaieb@29687 ` 74` huffman@29911 ` 75` ```lemma fps_sub_nth [simp]: "(f - g) \$ n = f \$ n - g \$ n" ``` huffman@29911 ` 76` ``` unfolding fps_minus_def by simp ``` huffman@29911 ` 77` huffman@29911 ` 78` ```instantiation fps :: (uminus) uminus ``` chaieb@29687 ` 79` ```begin ``` chaieb@29687 ` 80` huffman@29911 ` 81` ```definition fps_uminus_def: ``` huffman@29911 ` 82` ``` "uminus = (\f. Abs_fps (\n. - (f \$ n)))" ``` huffman@29911 ` 83` chaieb@29687 ` 84` ```instance .. ``` chaieb@29687 ` 85` ```end ``` chaieb@29687 ` 86` huffman@29911 ` 87` ```lemma fps_neg_nth [simp]: "(- f) \$ n = - (f \$ n)" ``` huffman@29911 ` 88` ``` unfolding fps_uminus_def by simp ``` huffman@29911 ` 89` chaieb@29687 ` 90` ```instantiation fps :: ("{comm_monoid_add, times}") times ``` chaieb@29687 ` 91` ```begin ``` chaieb@29687 ` 92` huffman@29911 ` 93` ```definition fps_times_def: ``` huffman@29911 ` 94` ``` "op * = (\f g. Abs_fps (\n. \i=0..n. f \$ i * g \$ (n - i)))" ``` huffman@29911 ` 95` chaieb@29687 ` 96` ```instance .. ``` chaieb@29687 ` 97` ```end ``` chaieb@29687 ` 98` huffman@29911 ` 99` ```lemma fps_mult_nth: "(f * g) \$ n = (\i=0..n. f\$i * g\$(n - i))" ``` huffman@29911 ` 100` ``` unfolding fps_times_def by simp ``` chaieb@29687 ` 101` huffman@29911 ` 102` ```declare atLeastAtMost_iff[presburger] ``` chaieb@29687 ` 103` ```declare Bex_def[presburger] ``` chaieb@29687 ` 104` ```declare Ball_def[presburger] ``` chaieb@29687 ` 105` huffman@29913 ` 106` ```lemma mult_delta_left: ``` huffman@29913 ` 107` ``` fixes x y :: "'a::mult_zero" ``` huffman@29913 ` 108` ``` shows "(if b then x else 0) * y = (if b then x * y else 0)" ``` huffman@29913 ` 109` ``` by simp ``` huffman@29913 ` 110` huffman@29913 ` 111` ```lemma mult_delta_right: ``` huffman@29913 ` 112` ``` fixes x y :: "'a::mult_zero" ``` huffman@29913 ` 113` ``` shows "x * (if b then y else 0) = (if b then x * y else 0)" ``` huffman@29913 ` 114` ``` by simp ``` huffman@29913 ` 115` chaieb@29687 ` 116` ```lemma cond_value_iff: "f (if b then x else y) = (if b then f x else f y)" ``` chaieb@29687 ` 117` ``` by auto ``` chaieb@29687 ` 118` ```lemma cond_application_beta: "(if b then f else g) x = (if b then f x else g x)" ``` chaieb@29687 ` 119` ``` by auto ``` chaieb@29687 ` 120` huffman@30488 ` 121` ```subsection{* Formal power series form a commutative ring with unity, if the range of sequences ``` chaieb@29687 ` 122` ``` they represent is a commutative ring with unity*} ``` chaieb@29687 ` 123` huffman@29911 ` 124` ```instance fps :: (semigroup_add) semigroup_add ``` chaieb@29687 ` 125` ```proof ``` chaieb@29687 ` 126` ``` fix a b c :: "'a fps" show "a + b + c = a + (b + c)" ``` huffman@29911 ` 127` ``` by (simp add: fps_ext add_assoc) ``` huffman@29911 ` 128` ```qed ``` huffman@29911 ` 129` huffman@29911 ` 130` ```instance fps :: (ab_semigroup_add) ab_semigroup_add ``` huffman@29911 ` 131` ```proof ``` huffman@29911 ` 132` ``` fix a b :: "'a fps" show "a + b = b + a" ``` huffman@29911 ` 133` ``` by (simp add: fps_ext add_commute) ``` chaieb@29687 ` 134` ```qed ``` chaieb@29687 ` 135` huffman@29911 ` 136` ```lemma fps_mult_assoc_lemma: ``` huffman@29911 ` 137` ``` fixes k :: nat and f :: "nat \ nat \ nat \ 'a::comm_monoid_add" ``` huffman@29911 ` 138` ``` shows "(\j=0..k. \i=0..j. f i (j - i) (n - j)) = ``` huffman@29911 ` 139` ``` (\j=0..k. \i=0..k - j. f j i (n - j - i))" ``` huffman@29911 ` 140` ```proof (induct k) ``` huffman@29911 ` 141` ``` case 0 show ?case by simp ``` huffman@29911 ` 142` ```next ``` huffman@29911 ` 143` ``` case (Suc k) thus ?case ``` huffman@29911 ` 144` ``` by (simp add: Suc_diff_le setsum_addf add_assoc ``` huffman@29911 ` 145` ``` cong: strong_setsum_cong) ``` huffman@29911 ` 146` ```qed ``` chaieb@29687 ` 147` huffman@29911 ` 148` ```instance fps :: (semiring_0) semigroup_mult ``` chaieb@29687 ` 149` ```proof ``` chaieb@29687 ` 150` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 151` ``` show "(a * b) * c = a * (b * c)" ``` huffman@29911 ` 152` ``` proof (rule fps_ext) ``` huffman@29911 ` 153` ``` fix n :: nat ``` huffman@29911 ` 154` ``` have "(\j=0..n. \i=0..j. a\$i * b\$(j - i) * c\$(n - j)) = ``` huffman@29911 ` 155` ``` (\j=0..n. \i=0..n - j. a\$j * b\$i * c\$(n - j - i))" ``` huffman@29911 ` 156` ``` by (rule fps_mult_assoc_lemma) ``` huffman@29911 ` 157` ``` thus "((a * b) * c) \$ n = (a * (b * c)) \$ n" ``` huffman@29911 ` 158` ``` by (simp add: fps_mult_nth setsum_right_distrib ``` huffman@29911 ` 159` ``` setsum_left_distrib mult_assoc) ``` huffman@29911 ` 160` ``` qed ``` huffman@29911 ` 161` ```qed ``` huffman@29911 ` 162` huffman@29911 ` 163` ```lemma fps_mult_commute_lemma: ``` huffman@29911 ` 164` ``` fixes n :: nat and f :: "nat \ nat \ 'a::comm_monoid_add" ``` huffman@29911 ` 165` ``` shows "(\i=0..n. f i (n - i)) = (\i=0..n. f (n - i) i)" ``` huffman@29911 ` 166` ```proof (rule setsum_reindex_cong) ``` huffman@29911 ` 167` ``` show "inj_on (\i. n - i) {0..n}" ``` huffman@29911 ` 168` ``` by (rule inj_onI) simp ``` huffman@29911 ` 169` ``` show "{0..n} = (\i. n - i) ` {0..n}" ``` huffman@29911 ` 170` ``` by (auto, rule_tac x="n - x" in image_eqI, simp_all) ``` huffman@29911 ` 171` ```next ``` huffman@29911 ` 172` ``` fix i assume "i \ {0..n}" ``` huffman@29911 ` 173` ``` hence "n - (n - i) = i" by simp ``` huffman@29911 ` 174` ``` thus "f (n - i) i = f (n - i) (n - (n - i))" by simp ``` huffman@29911 ` 175` ```qed ``` huffman@29911 ` 176` huffman@29911 ` 177` ```instance fps :: (comm_semiring_0) ab_semigroup_mult ``` huffman@29911 ` 178` ```proof ``` huffman@29911 ` 179` ``` fix a b :: "'a fps" ``` huffman@29911 ` 180` ``` show "a * b = b * a" ``` huffman@29911 ` 181` ``` proof (rule fps_ext) ``` huffman@29911 ` 182` ``` fix n :: nat ``` huffman@29911 ` 183` ``` have "(\i=0..n. a\$i * b\$(n - i)) = (\i=0..n. a\$(n - i) * b\$i)" ``` huffman@29911 ` 184` ``` by (rule fps_mult_commute_lemma) ``` huffman@29911 ` 185` ``` thus "(a * b) \$ n = (b * a) \$ n" ``` huffman@29911 ` 186` ``` by (simp add: fps_mult_nth mult_commute) ``` chaieb@29687 ` 187` ``` qed ``` chaieb@29687 ` 188` ```qed ``` chaieb@29687 ` 189` huffman@29911 ` 190` ```instance fps :: (monoid_add) monoid_add ``` chaieb@29687 ` 191` ```proof ``` chaieb@29687 ` 192` ``` fix a :: "'a fps" show "0 + a = a " ``` huffman@29911 ` 193` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 194` ```next ``` chaieb@29687 ` 195` ``` fix a :: "'a fps" show "a + 0 = a " ``` huffman@29911 ` 196` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 197` ```qed ``` chaieb@29687 ` 198` huffman@29911 ` 199` ```instance fps :: (comm_monoid_add) comm_monoid_add ``` chaieb@29687 ` 200` ```proof ``` chaieb@29687 ` 201` ``` fix a :: "'a fps" show "0 + a = a " ``` huffman@29911 ` 202` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 203` ```qed ``` chaieb@29687 ` 204` huffman@29911 ` 205` ```instance fps :: (semiring_1) monoid_mult ``` chaieb@29687 ` 206` ```proof ``` chaieb@29687 ` 207` ``` fix a :: "'a fps" show "1 * a = a" ``` huffman@29913 ` 208` ``` by (simp add: fps_ext fps_mult_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 209` ```next ``` huffman@29911 ` 210` ``` fix a :: "'a fps" show "a * 1 = a" ``` huffman@29913 ` 211` ``` by (simp add: fps_ext fps_mult_nth mult_delta_right setsum_delta') ``` chaieb@29687 ` 212` ```qed ``` chaieb@29687 ` 213` huffman@29911 ` 214` ```instance fps :: (cancel_semigroup_add) cancel_semigroup_add ``` huffman@29911 ` 215` ```proof ``` huffman@29911 ` 216` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 217` ``` assume "a + b = a + c" then show "b = c" ``` huffman@29911 ` 218` ``` by (simp add: expand_fps_eq) ``` huffman@29911 ` 219` ```next ``` huffman@29911 ` 220` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 221` ``` assume "b + a = c + a" then show "b = c" ``` huffman@29911 ` 222` ``` by (simp add: expand_fps_eq) ``` huffman@29911 ` 223` ```qed ``` chaieb@29687 ` 224` huffman@29911 ` 225` ```instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add ``` huffman@29911 ` 226` ```proof ``` huffman@29911 ` 227` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 228` ``` assume "a + b = a + c" then show "b = c" ``` huffman@29911 ` 229` ``` by (simp add: expand_fps_eq) ``` huffman@29911 ` 230` ```qed ``` chaieb@29687 ` 231` huffman@29911 ` 232` ```instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. ``` huffman@29911 ` 233` huffman@29911 ` 234` ```instance fps :: (group_add) group_add ``` chaieb@29687 ` 235` ```proof ``` chaieb@29687 ` 236` ``` fix a :: "'a fps" show "- a + a = 0" ``` huffman@29911 ` 237` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 238` ```next ``` chaieb@29687 ` 239` ``` fix a b :: "'a fps" show "a - b = a + - b" ``` huffman@29911 ` 240` ``` by (simp add: fps_ext diff_minus) ``` chaieb@29687 ` 241` ```qed ``` chaieb@29687 ` 242` huffman@29911 ` 243` ```instance fps :: (ab_group_add) ab_group_add ``` huffman@29911 ` 244` ```proof ``` huffman@29911 ` 245` ``` fix a :: "'a fps" ``` huffman@29911 ` 246` ``` show "- a + a = 0" ``` huffman@29911 ` 247` ``` by (simp add: fps_ext) ``` huffman@29911 ` 248` ```next ``` huffman@29911 ` 249` ``` fix a b :: "'a fps" ``` huffman@29911 ` 250` ``` show "a - b = a + - b" ``` huffman@29911 ` 251` ``` by (simp add: fps_ext) ``` huffman@29911 ` 252` ```qed ``` chaieb@29687 ` 253` huffman@29911 ` 254` ```instance fps :: (zero_neq_one) zero_neq_one ``` huffman@29911 ` 255` ``` by default (simp add: expand_fps_eq) ``` chaieb@29687 ` 256` huffman@29911 ` 257` ```instance fps :: (semiring_0) semiring ``` chaieb@29687 ` 258` ```proof ``` chaieb@29687 ` 259` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 260` ``` show "(a + b) * c = a * c + b * c" ``` huffman@29911 ` 261` ``` by (simp add: expand_fps_eq fps_mult_nth left_distrib setsum_addf) ``` chaieb@29687 ` 262` ```next ``` chaieb@29687 ` 263` ``` fix a b c :: "'a fps" ``` huffman@29911 ` 264` ``` show "a * (b + c) = a * b + a * c" ``` huffman@29911 ` 265` ``` by (simp add: expand_fps_eq fps_mult_nth right_distrib setsum_addf) ``` chaieb@29687 ` 266` ```qed ``` chaieb@29687 ` 267` huffman@29911 ` 268` ```instance fps :: (semiring_0) semiring_0 ``` chaieb@29687 ` 269` ```proof ``` huffman@29911 ` 270` ``` fix a:: "'a fps" show "0 * a = 0" ``` huffman@29911 ` 271` ``` by (simp add: fps_ext fps_mult_nth) ``` chaieb@29687 ` 272` ```next ``` huffman@29911 ` 273` ``` fix a:: "'a fps" show "a * 0 = 0" ``` huffman@29911 ` 274` ``` by (simp add: fps_ext fps_mult_nth) ``` chaieb@29687 ` 275` ```qed ``` huffman@29911 ` 276` huffman@29911 ` 277` ```instance fps :: (semiring_0_cancel) semiring_0_cancel .. ``` huffman@29911 ` 278` huffman@29906 ` 279` ```subsection {* Selection of the nth power of the implicit variable in the infinite sum*} ``` chaieb@29687 ` 280` chaieb@29687 ` 281` ```lemma fps_nonzero_nth: "f \ 0 \ (\ n. f \$n \ 0)" ``` huffman@29911 ` 282` ``` by (simp add: expand_fps_eq) ``` chaieb@29687 ` 283` huffman@29911 ` 284` ```lemma fps_nonzero_nth_minimal: ``` huffman@29911 ` 285` ``` "f \ 0 \ (\n. f \$ n \ 0 \ (\m 0" ``` huffman@29911 ` 289` ``` then have "\n. f \$ n \ 0" ``` huffman@29911 ` 290` ``` by (simp add: fps_nonzero_nth) ``` huffman@29911 ` 291` ``` then have "f \$ ?n \ 0" ``` huffman@29911 ` 292` ``` by (rule LeastI_ex) ``` huffman@29911 ` 293` ``` moreover have "\m 0 \ (\mn. f \$ n \ 0 \ (\mn. f \$ n \ 0 \ (\m 0" by (auto simp add: expand_fps_eq) ``` chaieb@29687 ` 300` ```qed ``` chaieb@29687 ` 301` chaieb@29687 ` 302` ```lemma fps_eq_iff: "f = g \ (\n. f \$ n = g \$n)" ``` huffman@29911 ` 303` ``` by (rule expand_fps_eq) ``` chaieb@29687 ` 304` huffman@30488 ` 305` ```lemma fps_setsum_nth: "(setsum f S) \$ n = setsum (\k. (f k) \$ n) S" ``` huffman@29911 ` 306` ```proof (cases "finite S") ``` huffman@29911 ` 307` ``` assume "\ finite S" then show ?thesis by simp ``` huffman@29911 ` 308` ```next ``` huffman@29911 ` 309` ``` assume "finite S" ``` huffman@29911 ` 310` ``` then show ?thesis by (induct set: finite) auto ``` chaieb@29687 ` 311` ```qed ``` chaieb@29687 ` 312` huffman@29906 ` 313` ```subsection{* Injection of the basic ring elements and multiplication by scalars *} ``` chaieb@29687 ` 314` huffman@29911 ` 315` ```definition ``` huffman@29911 ` 316` ``` "fps_const c = Abs_fps (\n. if n = 0 then c else 0)" ``` huffman@29911 ` 317` huffman@29911 ` 318` ```lemma fps_nth_fps_const [simp]: "fps_const c \$ n = (if n = 0 then c else 0)" ``` huffman@29911 ` 319` ``` unfolding fps_const_def by simp ``` huffman@29911 ` 320` huffman@29911 ` 321` ```lemma fps_const_0_eq_0 [simp]: "fps_const 0 = 0" ``` huffman@29911 ` 322` ``` by (simp add: fps_ext) ``` huffman@29911 ` 323` huffman@29911 ` 324` ```lemma fps_const_1_eq_1 [simp]: "fps_const 1 = 1" ``` huffman@29911 ` 325` ``` by (simp add: fps_ext) ``` huffman@29911 ` 326` huffman@29911 ` 327` ```lemma fps_const_neg [simp]: "- (fps_const (c::'a::ring)) = fps_const (- c)" ``` huffman@29911 ` 328` ``` by (simp add: fps_ext) ``` huffman@29911 ` 329` huffman@29911 ` 330` ```lemma fps_const_add [simp]: "fps_const (c::'a\monoid_add) + fps_const d = fps_const (c + d)" ``` huffman@29911 ` 331` ``` by (simp add: fps_ext) ``` chaieb@31369 ` 332` ```lemma fps_const_sub [simp]: "fps_const (c::'a\group_add) - fps_const d = fps_const (c - d)" ``` chaieb@31369 ` 333` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 334` ```lemma fps_const_mult[simp]: "fps_const (c::'a\ring) * fps_const d = fps_const (c * d)" ``` huffman@29911 ` 335` ``` by (simp add: fps_eq_iff fps_mult_nth setsum_0') ``` chaieb@29687 ` 336` chaieb@29687 ` 337` ```lemma fps_const_add_left: "fps_const (c::'a\monoid_add) + f = Abs_fps (\n. if n = 0 then c + f\$0 else f\$n)" ``` huffman@29911 ` 338` ``` by (simp add: fps_ext) ``` huffman@29911 ` 339` chaieb@29687 ` 340` ```lemma fps_const_add_right: "f + fps_const (c::'a\monoid_add) = Abs_fps (\n. if n = 0 then f\$0 + c else f\$n)" ``` huffman@29911 ` 341` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 342` chaieb@29687 ` 343` ```lemma fps_const_mult_left: "fps_const (c::'a\semiring_0) * f = Abs_fps (\n. c * f\$n)" ``` huffman@29911 ` 344` ``` unfolding fps_eq_iff fps_mult_nth ``` huffman@29913 ` 345` ``` by (simp add: fps_const_def mult_delta_left setsum_delta) ``` huffman@29911 ` 346` chaieb@29687 ` 347` ```lemma fps_const_mult_right: "f * fps_const (c::'a\semiring_0) = Abs_fps (\n. f\$n * c)" ``` huffman@29911 ` 348` ``` unfolding fps_eq_iff fps_mult_nth ``` huffman@29913 ` 349` ``` by (simp add: fps_const_def mult_delta_right setsum_delta') ``` chaieb@29687 ` 350` huffman@29911 ` 351` ```lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)\$n = c* f\$n" ``` huffman@29913 ` 352` ``` by (simp add: fps_mult_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 353` huffman@29911 ` 354` ```lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c" ``` huffman@29913 ` 355` ``` by (simp add: fps_mult_nth mult_delta_right setsum_delta') ``` chaieb@29687 ` 356` huffman@29906 ` 357` ```subsection {* Formal power series form an integral domain*} ``` chaieb@29687 ` 358` huffman@29911 ` 359` ```instance fps :: (ring) ring .. ``` chaieb@29687 ` 360` huffman@29911 ` 361` ```instance fps :: (ring_1) ring_1 ``` huffman@29911 ` 362` ``` by (intro_classes, auto simp add: diff_minus left_distrib) ``` chaieb@29687 ` 363` huffman@29911 ` 364` ```instance fps :: (comm_ring_1) comm_ring_1 ``` huffman@29911 ` 365` ``` by (intro_classes, auto simp add: diff_minus left_distrib) ``` chaieb@29687 ` 366` huffman@29911 ` 367` ```instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ``` chaieb@29687 ` 368` ```proof ``` chaieb@29687 ` 369` ``` fix a b :: "'a fps" ``` chaieb@29687 ` 370` ``` assume a0: "a \ 0" and b0: "b \ 0" ``` chaieb@29687 ` 371` ``` then obtain i j where i: "a\$i\0" "\k0" "\kk=0..i+j. a\$k * b\$(i+j-k))" ``` chaieb@29687 ` 375` ``` by (rule fps_mult_nth) ``` huffman@29911 ` 376` ``` also have "\ = (a\$i * b\$(i+j-i)) + (\k\{0..i+j}-{i}. a\$k * b\$(i+j-k))" ``` huffman@29911 ` 377` ``` by (rule setsum_diff1') simp_all ``` huffman@29911 ` 378` ``` also have "(\k\{0..i+j}-{i}. a\$k * b\$(i+j-k)) = 0" ``` huffman@29911 ` 379` ``` proof (rule setsum_0' [rule_format]) ``` huffman@29911 ` 380` ``` fix k assume "k \ {0..i+j} - {i}" ``` huffman@29911 ` 381` ``` then have "k < i \ i+j-k < j" by auto ``` huffman@29911 ` 382` ``` then show "a\$k * b\$(i+j-k) = 0" using i j by auto ``` huffman@29911 ` 383` ``` qed ``` huffman@29911 ` 384` ``` also have "a\$i * b\$(i+j-i) + 0 = a\$i * b\$j" by simp ``` huffman@29911 ` 385` ``` also have "a\$i * b\$j \ 0" using i j by simp ``` huffman@29911 ` 386` ``` finally have "(a*b) \$ (i+j) \ 0" . ``` chaieb@29687 ` 387` ``` then show "a*b \ 0" unfolding fps_nonzero_nth by blast ``` chaieb@29687 ` 388` ```qed ``` chaieb@29687 ` 389` huffman@29911 ` 390` ```instance fps :: (idom) idom .. ``` chaieb@29687 ` 391` chaieb@30746 ` 392` ```instantiation fps :: (comm_ring_1) number_ring ``` chaieb@30746 ` 393` ```begin ``` chaieb@30746 ` 394` ```definition number_of_fps_def: "(number_of k::'a fps) = of_int k" ``` chaieb@30746 ` 395` huffman@31273 ` 396` ```instance proof ``` huffman@31273 ` 397` ```qed (rule number_of_fps_def) ``` chaieb@30746 ` 398` ```end ``` chaieb@30746 ` 399` chaieb@31369 ` 400` ```lemma number_of_fps_const: "(number_of k::('a::comm_ring_1) fps) = fps_const (of_int k)" ``` chaieb@31369 ` 401` ``` ``` chaieb@31369 ` 402` ```proof(induct k rule: int_induct[where k=0]) ``` chaieb@31369 ` 403` ``` case base thus ?case unfolding number_of_fps_def of_int_0 by simp ``` chaieb@31369 ` 404` ```next ``` chaieb@31369 ` 405` ``` case (step1 i) thus ?case unfolding number_of_fps_def ``` chaieb@31369 ` 406` ``` by (simp add: fps_const_add[symmetric] del: fps_const_add) ``` chaieb@31369 ` 407` ```next ``` chaieb@31369 ` 408` ``` case (step2 i) thus ?case unfolding number_of_fps_def ``` chaieb@31369 ` 409` ``` by (simp add: fps_const_sub[symmetric] del: fps_const_sub) ``` chaieb@31369 ` 410` ```qed ``` chaieb@31369 ` 411` ``` ``` huffman@29906 ` 412` ```subsection{* Inverses of formal power series *} ``` chaieb@29687 ` 413` chaieb@29687 ` 414` ```declare setsum_cong[fundef_cong] ``` chaieb@29687 ` 415` chaieb@29687 ` 416` chaieb@29687 ` 417` ```instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}") inverse ``` chaieb@29687 ` 418` ```begin ``` chaieb@29687 ` 419` huffman@30488 ` 420` ```fun natfun_inverse:: "'a fps \ nat \ 'a" where ``` chaieb@29687 ` 421` ``` "natfun_inverse f 0 = inverse (f\$0)" ``` huffman@30488 ` 422` ```| "natfun_inverse f n = - inverse (f\$0) * setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n}" ``` chaieb@29687 ` 423` huffman@30488 ` 424` ```definition fps_inverse_def: ``` chaieb@29687 ` 425` ``` "inverse f = (if f\$0 = 0 then 0 else Abs_fps (natfun_inverse f))" ``` huffman@29911 ` 426` ```definition fps_divide_def: "divide = (\(f::'a fps) g. f * inverse g)" ``` chaieb@29687 ` 427` ```instance .. ``` chaieb@29687 ` 428` ```end ``` chaieb@29687 ` 429` huffman@30488 ` 430` ```lemma fps_inverse_zero[simp]: ``` chaieb@29687 ` 431` ``` "inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0" ``` huffman@29911 ` 432` ``` by (simp add: fps_ext fps_inverse_def) ``` chaieb@29687 ` 433` chaieb@29687 ` 434` ```lemma fps_inverse_one[simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1" ``` huffman@29911 ` 435` ``` apply (auto simp add: expand_fps_eq fps_inverse_def) ``` huffman@29911 ` 436` ``` by (case_tac n, auto) ``` chaieb@29687 ` 437` huffman@29911 ` 438` ```instance fps :: ("{comm_monoid_add,inverse, times, uminus}") division_by_zero ``` huffman@29911 ` 439` ``` by default (rule fps_inverse_zero) ``` chaieb@29687 ` 440` chaieb@29687 ` 441` ```lemma inverse_mult_eq_1[intro]: assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 442` ``` shows "inverse f * f = 1" ``` chaieb@29687 ` 443` ```proof- ``` chaieb@29687 ` 444` ``` have c: "inverse f * f = f * inverse f" by (simp add: mult_commute) ``` huffman@30488 ` 445` ``` from f0 have ifn: "\n. inverse f \$ n = natfun_inverse f n" ``` chaieb@29687 ` 446` ``` by (simp add: fps_inverse_def) ``` chaieb@29687 ` 447` ``` from f0 have th0: "(inverse f * f) \$ 0 = 1" ``` huffman@29911 ` 448` ``` by (simp add: fps_mult_nth fps_inverse_def) ``` chaieb@29687 ` 449` ``` {fix n::nat assume np: "n >0 " ``` chaieb@29687 ` 450` ``` from np have eq: "{0..n} = {0} \ {1 .. n}" by auto ``` chaieb@29687 ` 451` ``` have d: "{0} \ {1 .. n} = {}" by auto ``` chaieb@29687 ` 452` ``` have f: "finite {0::nat}" "finite {1..n}" by auto ``` huffman@30488 ` 453` ``` from f0 np have th0: "- (inverse f\$n) = ``` chaieb@29687 ` 454` ``` (setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n}) / (f\$0)" ``` huffman@29911 ` 455` ``` by (cases n, simp, simp add: divide_inverse fps_inverse_def) ``` chaieb@29687 ` 456` ``` from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] ``` huffman@30488 ` 457` ``` have th1: "setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n} = ``` huffman@30488 ` 458` ``` - (f\$0) * (inverse f)\$n" ``` chaieb@29687 ` 459` ``` by (simp add: ring_simps) ``` huffman@30488 ` 460` ``` have "(f * inverse f) \$ n = (\i = 0..n. f \$i * natfun_inverse f (n - i))" ``` chaieb@29687 ` 461` ``` unfolding fps_mult_nth ifn .. ``` huffman@30488 ` 462` ``` also have "\ = f\$0 * natfun_inverse f n ``` chaieb@29687 ` 463` ``` + (\i = 1..n. f\$i * natfun_inverse f (n-i))" ``` chaieb@29687 ` 464` ``` unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] ``` chaieb@29687 ` 465` ``` by simp ``` chaieb@29687 ` 466` ``` also have "\ = 0" unfolding th1 ifn by simp ``` chaieb@29687 ` 467` ``` finally have "(inverse f * f)\$n = 0" unfolding c . } ``` chaieb@29687 ` 468` ``` with th0 show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 469` ```qed ``` chaieb@29687 ` 470` chaieb@29687 ` 471` ```lemma fps_inverse_0_iff[simp]: "(inverse f)\$0 = (0::'a::division_ring) \ f\$0 = 0" ``` huffman@29911 ` 472` ``` by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) ``` chaieb@29687 ` 473` chaieb@29687 ` 474` ```lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \ f \$0 = 0" ``` chaieb@29687 ` 475` ```proof- ``` chaieb@29687 ` 476` ``` {assume "f\$0 = 0" hence "inverse f = 0" by (simp add: fps_inverse_def)} ``` chaieb@29687 ` 477` ``` moreover ``` chaieb@29687 ` 478` ``` {assume h: "inverse f = 0" and c: "f \$0 \ 0" ``` chaieb@29687 ` 479` ``` from inverse_mult_eq_1[OF c] h have False by simp} ``` chaieb@29687 ` 480` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 481` ```qed ``` chaieb@29687 ` 482` chaieb@29687 ` 483` ```lemma fps_inverse_idempotent[intro]: assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 484` ``` shows "inverse (inverse f) = f" ``` chaieb@29687 ` 485` ```proof- ``` chaieb@29687 ` 486` ``` from f0 have if0: "inverse f \$ 0 \ 0" by simp ``` huffman@30488 ` 487` ``` from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] ``` chaieb@29687 ` 488` ``` have th0: "inverse f * f = inverse f * inverse (inverse f)" by (simp add: mult_ac) ``` chaieb@29687 ` 489` ``` then show ?thesis using f0 unfolding mult_cancel_left by simp ``` chaieb@29687 ` 490` ```qed ``` chaieb@29687 ` 491` huffman@30488 ` 492` ```lemma fps_inverse_unique: assumes f0: "f\$0 \ (0::'a::field)" and fg: "f*g = 1" ``` chaieb@29687 ` 493` ``` shows "inverse f = g" ``` chaieb@29687 ` 494` ```proof- ``` chaieb@29687 ` 495` ``` from inverse_mult_eq_1[OF f0] fg ``` chaieb@29687 ` 496` ``` have th0: "inverse f * f = g * f" by (simp add: mult_ac) ``` chaieb@29687 ` 497` ``` then show ?thesis using f0 unfolding mult_cancel_right ``` huffman@29911 ` 498` ``` by (auto simp add: expand_fps_eq) ``` chaieb@29687 ` 499` ```qed ``` chaieb@29687 ` 500` huffman@30488 ` 501` ```lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) ``` chaieb@29687 ` 502` ``` = Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" ``` chaieb@29687 ` 503` ``` apply (rule fps_inverse_unique) ``` chaieb@29687 ` 504` ``` apply simp ``` huffman@29911 ` 505` ``` apply (simp add: fps_eq_iff fps_mult_nth) ``` chaieb@29687 ` 506` ```proof(clarsimp) ``` chaieb@29687 ` 507` ``` fix n::nat assume n: "n > 0" ``` chaieb@29687 ` 508` ``` let ?f = "\i. if n = i then (1\'a) else if n - i = 1 then - 1 else 0" ``` chaieb@29687 ` 509` ``` let ?g = "\i. if i = n then 1 else if i=n - 1 then - 1 else 0" ``` chaieb@29687 ` 510` ``` let ?h = "\i. if i=n - 1 then - 1 else 0" ``` huffman@30488 ` 511` ``` have th1: "setsum ?f {0..n} = setsum ?g {0..n}" ``` chaieb@29687 ` 512` ``` by (rule setsum_cong2) auto ``` huffman@30488 ` 513` ``` have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}" ``` chaieb@29687 ` 514` ``` using n apply - by (rule setsum_cong2) auto ``` chaieb@29687 ` 515` ``` have eq: "{0 .. n} = {0.. n - 1} \ {n}" by auto ``` huffman@30488 ` 516` ``` from n have d: "{0.. n - 1} \ {n} = {}" by auto ``` chaieb@29687 ` 517` ``` have f: "finite {0.. n - 1}" "finite {n}" by auto ``` chaieb@29687 ` 518` ``` show "setsum ?f {0..n} = 0" ``` huffman@30488 ` 519` ``` unfolding th1 ``` chaieb@29687 ` 520` ``` apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) ``` chaieb@29687 ` 521` ``` unfolding th2 ``` chaieb@29687 ` 522` ``` by(simp add: setsum_delta) ``` chaieb@29687 ` 523` ```qed ``` chaieb@29687 ` 524` huffman@29912 ` 525` ```subsection{* Formal Derivatives, and the MacLaurin theorem around 0*} ``` chaieb@29687 ` 526` chaieb@29687 ` 527` ```definition "fps_deriv f = Abs_fps (\n. of_nat (n + 1) * f \$ (n + 1))" ``` chaieb@29687 ` 528` chaieb@29687 ` 529` ```lemma fps_deriv_nth[simp]: "fps_deriv f \$ n = of_nat (n +1) * f \$ (n+1)" by (simp add: fps_deriv_def) ``` chaieb@29687 ` 530` chaieb@29687 ` 531` ```lemma fps_deriv_linear[simp]: "fps_deriv (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_deriv f + fps_const b * fps_deriv g" ``` chaieb@29687 ` 532` ``` unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: ring_simps) ``` chaieb@29687 ` 533` huffman@30488 ` 534` ```lemma fps_deriv_mult[simp]: ``` chaieb@29687 ` 535` ``` fixes f :: "('a :: comm_ring_1) fps" ``` chaieb@29687 ` 536` ``` shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" ``` chaieb@29687 ` 537` ```proof- ``` chaieb@29687 ` 538` ``` let ?D = "fps_deriv" ``` chaieb@29687 ` 539` ``` {fix n::nat ``` chaieb@29687 ` 540` ``` let ?Zn = "{0 ..n}" ``` chaieb@29687 ` 541` ``` let ?Zn1 = "{0 .. n + 1}" ``` chaieb@29687 ` 542` ``` let ?f = "\i. i + 1" ``` chaieb@29687 ` 543` ``` have fi: "inj_on ?f {0..n}" by (simp add: inj_on_def) ``` chaieb@29687 ` 544` ``` have eq: "{1.. n+1} = ?f ` {0..n}" by auto ``` chaieb@29687 ` 545` ``` let ?g = "\i. of_nat (i+1) * g \$ (i+1) * f \$ (n - i) + ``` chaieb@29687 ` 546` ``` of_nat (i+1)* f \$ (i+1) * g \$ (n - i)" ``` chaieb@29687 ` 547` ``` let ?h = "\i. of_nat i * g \$ i * f \$ ((n+1) - i) + ``` chaieb@29687 ` 548` ``` of_nat i* f \$ i * g \$ ((n + 1) - i)" ``` chaieb@29687 ` 549` ``` {fix k assume k: "k \ {0..n}" ``` chaieb@29687 ` 550` ``` have "?h (k + 1) = ?g k" using k by auto} ``` chaieb@29687 ` 551` ``` note th0 = this ``` chaieb@29687 ` 552` ``` have eq': "{0..n +1}- {1 .. n+1} = {0}" by auto ``` chaieb@29687 ` 553` ``` have s0: "setsum (\i. of_nat i * f \$ i * g \$ (n + 1 - i)) ?Zn1 = setsum (\i. of_nat (n + 1 - i) * f \$ (n + 1 - i) * g \$ i) ?Zn1" ``` chaieb@29687 ` 554` ``` apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) ``` chaieb@29687 ` 555` ``` apply (simp add: inj_on_def Ball_def) ``` chaieb@29687 ` 556` ``` apply presburger ``` chaieb@29687 ` 557` ``` apply (rule set_ext) ``` chaieb@29687 ` 558` ``` apply (presburger add: image_iff) ``` chaieb@29687 ` 559` ``` by simp ``` chaieb@29687 ` 560` ``` have s1: "setsum (\i. f \$ i * g \$ (n + 1 - i)) ?Zn1 = setsum (\i. f \$ (n + 1 - i) * g \$ i) ?Zn1" ``` chaieb@29687 ` 561` ``` apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) ``` chaieb@29687 ` 562` ``` apply (simp add: inj_on_def Ball_def) ``` chaieb@29687 ` 563` ``` apply presburger ``` chaieb@29687 ` 564` ``` apply (rule set_ext) ``` chaieb@29687 ` 565` ``` apply (presburger add: image_iff) ``` chaieb@29687 ` 566` ``` by simp ``` chaieb@29687 ` 567` ``` have "(f * ?D g + ?D f * g)\$n = (?D g * f + ?D f * g)\$n" by (simp only: mult_commute) ``` chaieb@29687 ` 568` ``` also have "\ = (\i = 0..n. ?g i)" ``` chaieb@29687 ` 569` ``` by (simp add: fps_mult_nth setsum_addf[symmetric]) ``` chaieb@29687 ` 570` ``` also have "\ = setsum ?h {1..n+1}" ``` chaieb@29687 ` 571` ``` using th0 setsum_reindex_cong[OF fi eq, of "?g" "?h"] by auto ``` chaieb@29687 ` 572` ``` also have "\ = setsum ?h {0..n+1}" ``` chaieb@29687 ` 573` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 574` ``` apply simp ``` chaieb@29687 ` 575` ``` apply (simp add: subset_eq) ``` chaieb@29687 ` 576` ``` unfolding eq' ``` chaieb@29687 ` 577` ``` by simp ``` chaieb@29687 ` 578` ``` also have "\ = (fps_deriv (f * g)) \$ n" ``` chaieb@29687 ` 579` ``` apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf) ``` chaieb@29687 ` 580` ``` unfolding s0 s1 ``` chaieb@29687 ` 581` ``` unfolding setsum_addf[symmetric] setsum_right_distrib ``` chaieb@29687 ` 582` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 583` ``` by (auto simp add: of_nat_diff ring_simps) ``` chaieb@29687 ` 584` ``` finally have "(f * ?D g + ?D f * g) \$ n = ?D (f*g) \$ n" .} ``` huffman@30488 ` 585` ``` then show ?thesis unfolding fps_eq_iff by auto ``` chaieb@29687 ` 586` ```qed ``` chaieb@29687 ` 587` chaieb@29687 ` 588` ```lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: ('a:: comm_ring_1) fps)) = - (fps_deriv f)" ``` huffman@29911 ` 589` ``` by (simp add: fps_eq_iff fps_deriv_def) ``` chaieb@29687 ` 590` ```lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g" ``` chaieb@29687 ` 591` ``` using fps_deriv_linear[of 1 f 1 g] by simp ``` chaieb@29687 ` 592` chaieb@29687 ` 593` ```lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g" ``` huffman@30488 ` 594` ``` unfolding diff_minus by simp ``` chaieb@29687 ` 595` chaieb@29687 ` 596` ```lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0" ``` huffman@29911 ` 597` ``` by (simp add: fps_ext fps_deriv_def fps_const_def) ``` chaieb@29687 ` 598` chaieb@29687 ` 599` ```lemma fps_deriv_mult_const_left[simp]: "fps_deriv (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_deriv f" ``` chaieb@29687 ` 600` ``` by simp ``` chaieb@29687 ` 601` chaieb@29687 ` 602` ```lemma fps_deriv_0[simp]: "fps_deriv 0 = 0" ``` chaieb@29687 ` 603` ``` by (simp add: fps_deriv_def fps_eq_iff) ``` chaieb@29687 ` 604` chaieb@29687 ` 605` ```lemma fps_deriv_1[simp]: "fps_deriv 1 = 0" ``` chaieb@29687 ` 606` ``` by (simp add: fps_deriv_def fps_eq_iff ) ``` chaieb@29687 ` 607` chaieb@29687 ` 608` ```lemma fps_deriv_mult_const_right[simp]: "fps_deriv (f * fps_const (c::'a::comm_ring_1)) = fps_deriv f * fps_const c" ``` chaieb@29687 ` 609` ``` by simp ``` chaieb@29687 ` 610` chaieb@29687 ` 611` ```lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S" ``` chaieb@29687 ` 612` ```proof- ``` chaieb@29687 ` 613` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 614` ``` moreover ``` chaieb@29687 ` 615` ``` {assume fS: "finite S" ``` chaieb@29687 ` 616` ``` have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} ``` chaieb@29687 ` 617` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 618` ```qed ``` chaieb@29687 ` 619` chaieb@29687 ` 620` ```lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \ (f = fps_const (f\$0 :: 'a::{idom,semiring_char_0}))" ``` chaieb@29687 ` 621` ```proof- ``` chaieb@29687 ` 622` ``` {assume "f= fps_const (f\$0)" hence "fps_deriv f = fps_deriv (fps_const (f\$0))" by simp ``` chaieb@29687 ` 623` ``` hence "fps_deriv f = 0" by simp } ``` chaieb@29687 ` 624` ``` moreover ``` chaieb@29687 ` 625` ``` {assume z: "fps_deriv f = 0" ``` chaieb@29687 ` 626` ``` hence "\n. (fps_deriv f)\$n = 0" by simp ``` chaieb@29687 ` 627` ``` hence "\n. f\$(n+1) = 0" by (simp del: of_nat_Suc of_nat_add One_nat_def) ``` chaieb@29687 ` 628` ``` hence "f = fps_const (f\$0)" ``` chaieb@29687 ` 629` ``` apply (clarsimp simp add: fps_eq_iff fps_const_def) ``` chaieb@29687 ` 630` ``` apply (erule_tac x="n - 1" in allE) ``` chaieb@29687 ` 631` ``` by simp} ``` chaieb@29687 ` 632` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 633` ```qed ``` chaieb@29687 ` 634` huffman@30488 ` 635` ```lemma fps_deriv_eq_iff: ``` chaieb@29687 ` 636` ``` fixes f:: "('a::{idom,semiring_char_0}) fps" ``` chaieb@29687 ` 637` ``` shows "fps_deriv f = fps_deriv g \ (f = fps_const(f\$0 - g\$0) + g)" ``` chaieb@29687 ` 638` ```proof- ``` chaieb@29687 ` 639` ``` have "fps_deriv f = fps_deriv g \ fps_deriv (f - g) = 0" by simp ``` chaieb@29687 ` 640` ``` also have "\ \ f - g = fps_const ((f-g)\$0)" unfolding fps_deriv_eq_0_iff .. ``` chaieb@29687 ` 641` ``` finally show ?thesis by (simp add: ring_simps) ``` chaieb@29687 ` 642` ```qed ``` chaieb@29687 ` 643` chaieb@29687 ` 644` ```lemma fps_deriv_eq_iff_ex: "(fps_deriv f = fps_deriv g) \ (\(c::'a::{idom,semiring_char_0}). f = fps_const c + g)" ``` chaieb@29687 ` 645` ``` apply auto unfolding fps_deriv_eq_iff by blast ``` huffman@30488 ` 646` chaieb@29687 ` 647` chaieb@29687 ` 648` ```fun fps_nth_deriv :: "nat \ ('a::semiring_1) fps \ 'a fps" where ``` chaieb@29687 ` 649` ``` "fps_nth_deriv 0 f = f" ``` chaieb@29687 ` 650` ```| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" ``` chaieb@29687 ` 651` chaieb@29687 ` 652` ```lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)" ``` chaieb@29687 ` 653` ``` by (induct n arbitrary: f, auto) ``` chaieb@29687 ` 654` chaieb@29687 ` 655` ```lemma fps_nth_deriv_linear[simp]: "fps_nth_deriv n (fps_const (a::'a::comm_semiring_1) * f + fps_const b * g) = fps_const a * fps_nth_deriv n f + fps_const b * fps_nth_deriv n g" ``` chaieb@29687 ` 656` ``` by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute) ``` chaieb@29687 ` 657` chaieb@29687 ` 658` ```lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)" ``` chaieb@29687 ` 659` ``` by (induct n arbitrary: f, simp_all) ``` chaieb@29687 ` 660` chaieb@29687 ` 661` ```lemma fps_nth_deriv_add[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) + g) = fps_nth_deriv n f + fps_nth_deriv n g" ``` chaieb@29687 ` 662` ``` using fps_nth_deriv_linear[of n 1 f 1 g] by simp ``` chaieb@29687 ` 663` chaieb@29687 ` 664` ```lemma fps_nth_deriv_sub[simp]: "fps_nth_deriv n ((f:: ('a::comm_ring_1) fps) - g) = fps_nth_deriv n f - fps_nth_deriv n g" ``` huffman@30488 ` 665` ``` unfolding diff_minus fps_nth_deriv_add by simp ``` chaieb@29687 ` 666` chaieb@29687 ` 667` ```lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0" ``` chaieb@29687 ` 668` ``` by (induct n, simp_all ) ``` chaieb@29687 ` 669` chaieb@29687 ` 670` ```lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)" ``` chaieb@29687 ` 671` ``` by (induct n, simp_all ) ``` chaieb@29687 ` 672` chaieb@29687 ` 673` ```lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)" ``` chaieb@29687 ` 674` ``` by (cases n, simp_all) ``` chaieb@29687 ` 675` chaieb@29687 ` 676` ```lemma fps_nth_deriv_mult_const_left[simp]: "fps_nth_deriv n (fps_const (c::'a::comm_ring_1) * f) = fps_const c * fps_nth_deriv n f" ``` chaieb@29687 ` 677` ``` using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp ``` chaieb@29687 ` 678` chaieb@29687 ` 679` ```lemma fps_nth_deriv_mult_const_right[simp]: "fps_nth_deriv n (f * fps_const (c::'a::comm_ring_1)) = fps_nth_deriv n f * fps_const c" ``` chaieb@29687 ` 680` ``` using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute) ``` chaieb@29687 ` 681` chaieb@29687 ` 682` ```lemma fps_nth_deriv_setsum: "fps_nth_deriv n (setsum f S) = setsum (\i. fps_nth_deriv n (f i :: ('a::comm_ring_1) fps)) S" ``` chaieb@29687 ` 683` ```proof- ``` chaieb@29687 ` 684` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 685` ``` moreover ``` chaieb@29687 ` 686` ``` {assume fS: "finite S" ``` chaieb@29687 ` 687` ``` have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} ``` chaieb@29687 ` 688` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 689` ```qed ``` chaieb@29687 ` 690` chaieb@29687 ` 691` ```lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) \$ 0 = of_nat (fact k) * f\$(k)" ``` chaieb@29687 ` 692` ``` by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult) ``` chaieb@29687 ` 693` huffman@29906 ` 694` ```subsection {* Powers*} ``` chaieb@29687 ` 695` chaieb@29687 ` 696` ```lemma fps_power_zeroth_eq_one: "a\$0 =1 \ a^n \$ 0 = (1::'a::semiring_1)" ``` haftmann@30960 ` 697` ``` by (induct n, auto simp add: expand_fps_eq fps_mult_nth) ``` chaieb@29687 ` 698` chaieb@29687 ` 699` ```lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)\$0 =1 \ a^n \$ 1 = of_nat n * a\$1" ``` chaieb@29687 ` 700` ```proof(induct n) ``` haftmann@30960 ` 701` ``` case 0 thus ?case by simp ``` chaieb@29687 ` 702` ```next ``` chaieb@29687 ` 703` ``` case (Suc n) ``` chaieb@29687 ` 704` ``` note h = Suc.hyps[OF `a\$0 = 1`] ``` huffman@30488 ` 705` ``` show ?case unfolding power_Suc fps_mult_nth ``` chaieb@29687 ` 706` ``` using h `a\$0 = 1` fps_power_zeroth_eq_one[OF `a\$0=1`] by (simp add: ring_simps) ``` chaieb@29687 ` 707` ```qed ``` chaieb@29687 ` 708` chaieb@29687 ` 709` ```lemma startsby_one_power:"a \$ 0 = (1::'a::comm_ring_1) \ a^n \$ 0 = 1" ``` haftmann@30960 ` 710` ``` by (induct n, auto simp add: fps_mult_nth) ``` chaieb@29687 ` 711` chaieb@29687 ` 712` ```lemma startsby_zero_power:"a \$0 = (0::'a::comm_ring_1) \ n > 0 \ a^n \$0 = 0" ``` haftmann@30960 ` 713` ``` by (induct n, auto simp add: fps_mult_nth) ``` chaieb@29687 ` 714` haftmann@31021 ` 715` ```lemma startsby_power:"a \$0 = (v::'a::{comm_ring_1}) \ a^n \$0 = v^n" ``` haftmann@30960 ` 716` ``` by (induct n, auto simp add: fps_mult_nth power_Suc) ``` chaieb@29687 ` 717` chaieb@29687 ` 718` ```lemma startsby_zero_power_iff[simp]: ``` haftmann@31021 ` 719` ``` "a^n \$0 = (0::'a::{idom}) \ (n \ 0 \ a\$0 = 0)" ``` chaieb@29687 ` 720` ```apply (rule iffI) ``` chaieb@29687 ` 721` ```apply (induct n, auto simp add: power_Suc fps_mult_nth) ``` chaieb@29687 ` 722` ```by (rule startsby_zero_power, simp_all) ``` chaieb@29687 ` 723` huffman@30488 ` 724` ```lemma startsby_zero_power_prefix: ``` chaieb@29687 ` 725` ``` assumes a0: "a \$0 = (0::'a::idom)" ``` chaieb@29687 ` 726` ``` shows "\n < k. a ^ k \$ n = 0" ``` huffman@30488 ` 727` ``` using a0 ``` chaieb@29687 ` 728` ```proof(induct k rule: nat_less_induct) ``` chaieb@29687 ` 729` ``` fix k assume H: "\m (\n'a)" ``` chaieb@29687 ` 730` ``` let ?ths = "\m 0" ``` chaieb@29687 ` 739` ``` have "a ^k \$ m = (a^l * a) \$m" by (simp add: k power_Suc mult_commute) ``` chaieb@29687 ` 740` ``` also have "\ = (\i = 0..m. a ^ l \$ i * a \$ (m - i))" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 741` ``` also have "\ = 0" apply (rule setsum_0') ``` chaieb@29687 ` 742` ``` apply auto ``` chaieb@29687 ` 743` ``` apply (case_tac "aa = m") ``` chaieb@29687 ` 744` ``` using a0 ``` chaieb@29687 ` 745` ``` apply simp ``` chaieb@29687 ` 746` ``` apply (rule H[rule_format]) ``` huffman@30488 ` 747` ``` using a0 k mk by auto ``` chaieb@29687 ` 748` ``` finally have "a^k \$ m = 0" .} ``` chaieb@29687 ` 749` ``` ultimately have "a^k \$ m = 0" by blast} ``` chaieb@29687 ` 750` ``` hence ?ths by blast} ``` chaieb@29687 ` 751` ``` ultimately show ?ths by (cases k, auto) ``` chaieb@29687 ` 752` ```qed ``` chaieb@29687 ` 753` huffman@30488 ` 754` ```lemma startsby_zero_setsum_depends: ``` chaieb@29687 ` 755` ``` assumes a0: "a \$0 = (0::'a::idom)" and kn: "n \ k" ``` chaieb@29687 ` 756` ``` shows "setsum (\i. (a ^ i)\$k) {0 .. n} = setsum (\i. (a ^ i)\$k) {0 .. k}" ``` chaieb@29687 ` 757` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 758` ``` using kn apply auto ``` chaieb@29687 ` 759` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` chaieb@29687 ` 760` ``` by arith ``` chaieb@29687 ` 761` haftmann@31021 ` 762` ```lemma startsby_zero_power_nth_same: assumes a0: "a\$0 = (0::'a::{idom})" ``` chaieb@29687 ` 763` ``` shows "a^n \$ n = (a\$1) ^ n" ``` chaieb@29687 ` 764` ```proof(induct n) ``` chaieb@29687 ` 765` ``` case 0 thus ?case by (simp add: power_0) ``` chaieb@29687 ` 766` ```next ``` chaieb@29687 ` 767` ``` case (Suc n) ``` chaieb@29687 ` 768` ``` have "a ^ Suc n \$ (Suc n) = (a^n * a)\$(Suc n)" by (simp add: ring_simps power_Suc) ``` chaieb@29687 ` 769` ``` also have "\ = setsum (\i. a^n\$i * a \$ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 770` ``` also have "\ = setsum (\i. a^n\$i * a \$ (Suc n - i)) {n .. Suc n}" ``` chaieb@29687 ` 771` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 772` ``` apply simp ``` chaieb@29687 ` 773` ``` apply clarsimp ``` chaieb@29687 ` 774` ``` apply clarsimp ``` chaieb@29687 ` 775` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` chaieb@29687 ` 776` ``` apply arith ``` chaieb@29687 ` 777` ``` done ``` chaieb@29687 ` 778` ``` also have "\ = a^n \$ n * a\$1" using a0 by simp ``` chaieb@29687 ` 779` ``` finally show ?case using Suc.hyps by (simp add: power_Suc) ``` chaieb@29687 ` 780` ```qed ``` chaieb@29687 ` 781` chaieb@29687 ` 782` ```lemma fps_inverse_power: ``` haftmann@31021 ` 783` ``` fixes a :: "('a::{field}) fps" ``` chaieb@29687 ` 784` ``` shows "inverse (a^n) = inverse a ^ n" ``` chaieb@29687 ` 785` ```proof- ``` chaieb@29687 ` 786` ``` {assume a0: "a\$0 = 0" ``` chaieb@29687 ` 787` ``` hence eq: "inverse a = 0" by (simp add: fps_inverse_def) ``` chaieb@29687 ` 788` ``` {assume "n = 0" hence ?thesis by simp} ``` chaieb@29687 ` 789` ``` moreover ``` chaieb@29687 ` 790` ``` {assume n: "n > 0" ``` huffman@30488 ` 791` ``` from startsby_zero_power[OF a0 n] eq a0 n have ?thesis ``` chaieb@29687 ` 792` ``` by (simp add: fps_inverse_def)} ``` chaieb@29687 ` 793` ``` ultimately have ?thesis by blast} ``` chaieb@29687 ` 794` ``` moreover ``` chaieb@29687 ` 795` ``` {assume a0: "a\$0 \ 0" ``` chaieb@29687 ` 796` ``` have ?thesis ``` chaieb@29687 ` 797` ``` apply (rule fps_inverse_unique) ``` chaieb@29687 ` 798` ``` apply (simp add: a0) ``` chaieb@29687 ` 799` ``` unfolding power_mult_distrib[symmetric] ``` chaieb@29687 ` 800` ``` apply (rule ssubst[where t = "a * inverse a" and s= 1]) ``` chaieb@29687 ` 801` ``` apply simp_all ``` chaieb@29687 ` 802` ``` apply (subst mult_commute) ``` chaieb@29687 ` 803` ``` by (rule inverse_mult_eq_1[OF a0])} ``` chaieb@29687 ` 804` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 805` ```qed ``` chaieb@29687 ` 806` chaieb@29687 ` 807` ```lemma fps_deriv_power: "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a:: comm_ring_1) * fps_deriv a * a ^ (n - 1)" ``` chaieb@29687 ` 808` ``` apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add) ``` chaieb@29687 ` 809` ``` by (case_tac n, auto simp add: power_Suc ring_simps) ``` chaieb@29687 ` 810` huffman@30488 ` 811` ```lemma fps_inverse_deriv: ``` chaieb@29687 ` 812` ``` fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 813` ``` assumes a0: "a\$0 \ 0" ``` chaieb@29687 ` 814` ``` shows "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" ``` chaieb@29687 ` 815` ```proof- ``` chaieb@29687 ` 816` ``` from inverse_mult_eq_1[OF a0] ``` chaieb@29687 ` 817` ``` have "fps_deriv (inverse a * a) = 0" by simp ``` chaieb@29687 ` 818` ``` hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp ``` chaieb@29687 ` 819` ``` hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" by simp ``` chaieb@29687 ` 820` ``` with inverse_mult_eq_1[OF a0] ``` chaieb@29687 ` 821` ``` have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0" ``` chaieb@29687 ` 822` ``` unfolding power2_eq_square ``` chaieb@29687 ` 823` ``` apply (simp add: ring_simps) ``` chaieb@29687 ` 824` ``` by (simp add: mult_assoc[symmetric]) ``` chaieb@29687 ` 825` ``` hence "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) - fps_deriv a * inverse a ^ 2 = 0 - fps_deriv a * inverse a ^ 2" ``` chaieb@29687 ` 826` ``` by simp ``` chaieb@29687 ` 827` ``` then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: ring_simps) ``` chaieb@29687 ` 828` ```qed ``` chaieb@29687 ` 829` huffman@30488 ` 830` ```lemma fps_inverse_mult: ``` chaieb@29687 ` 831` ``` fixes a::"('a :: field) fps" ``` chaieb@29687 ` 832` ``` shows "inverse (a * b) = inverse a * inverse b" ``` chaieb@29687 ` 833` ```proof- ``` chaieb@29687 ` 834` ``` {assume a0: "a\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 835` ``` from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all ``` chaieb@29687 ` 836` ``` have ?thesis unfolding th by simp} ``` chaieb@29687 ` 837` ``` moreover ``` chaieb@29687 ` 838` ``` {assume b0: "b\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 839` ``` from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all ``` chaieb@29687 ` 840` ``` have ?thesis unfolding th by simp} ``` chaieb@29687 ` 841` ``` moreover ``` chaieb@29687 ` 842` ``` {assume a0: "a\$0 \ 0" and b0: "b\$0 \ 0" ``` chaieb@29687 ` 843` ``` from a0 b0 have ab0:"(a*b) \$ 0 \ 0" by (simp add: fps_mult_nth) ``` huffman@30488 ` 844` ``` from inverse_mult_eq_1[OF ab0] ``` chaieb@29687 ` 845` ``` have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp ``` chaieb@29687 ` 846` ``` then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" ``` chaieb@29687 ` 847` ``` by (simp add: ring_simps) ``` chaieb@29687 ` 848` ``` then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp} ``` chaieb@29687 ` 849` ```ultimately show ?thesis by blast ``` chaieb@29687 ` 850` ```qed ``` chaieb@29687 ` 851` huffman@30488 ` 852` ```lemma fps_inverse_deriv': ``` chaieb@29687 ` 853` ``` fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 854` ``` assumes a0: "a\$0 \ 0" ``` chaieb@29687 ` 855` ``` shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2" ``` chaieb@29687 ` 856` ``` using fps_inverse_deriv[OF a0] ``` chaieb@29687 ` 857` ``` unfolding power2_eq_square fps_divide_def ``` chaieb@29687 ` 858` ``` fps_inverse_mult by simp ``` chaieb@29687 ` 859` chaieb@29687 ` 860` ```lemma inverse_mult_eq_1': assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 861` ``` shows "f * inverse f= 1" ``` chaieb@29687 ` 862` ``` by (metis mult_commute inverse_mult_eq_1 f0) ``` chaieb@29687 ` 863` chaieb@29687 ` 864` ```lemma fps_divide_deriv: fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 865` ``` assumes a0: "b\$0 \ 0" ``` chaieb@29687 ` 866` ``` shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2" ``` chaieb@29687 ` 867` ``` using fps_inverse_deriv[OF a0] ``` chaieb@29687 ` 868` ``` by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) ``` huffman@30488 ` 869` huffman@29906 ` 870` ```subsection{* The eXtractor series X*} ``` chaieb@29687 ` 871` haftmann@31021 ` 872` ```lemma minus_one_power_iff: "(- (1::'a :: {comm_ring_1})) ^ n = (if even n then 1 else - 1)" ``` chaieb@29687 ` 873` ``` by (induct n, auto) ``` chaieb@29687 ` 874` chaieb@29687 ` 875` ```definition "X = Abs_fps (\n. if n = 1 then 1 else 0)" ``` chaieb@29687 ` 876` huffman@30488 ` 877` ```lemma fps_inverse_gp': "inverse (Abs_fps(\n. (1::'a::field))) ``` chaieb@29687 ` 878` ``` = 1 - X" ``` huffman@29911 ` 879` ``` by (simp add: fps_inverse_gp fps_eq_iff X_def) ``` chaieb@29687 ` 880` chaieb@29687 ` 881` ```lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))" ``` chaieb@29687 ` 882` ```proof- ``` chaieb@29687 ` 883` ``` {assume n: "n \ 0" ``` chaieb@29687 ` 884` ``` have fN: "finite {0 .. n}" by simp ``` chaieb@29687 ` 885` ``` have "(X * f) \$n = (\i = 0..n. X \$ i * f \$ (n - i))" by (simp add: fps_mult_nth) ``` huffman@29913 ` 886` ``` also have "\ = f \$ (n - 1)" ``` huffman@29913 ` 887` ``` using n by (simp add: X_def mult_delta_left setsum_delta [OF fN]) ``` chaieb@29687 ` 888` ``` finally have ?thesis using n by simp } ``` chaieb@29687 ` 889` ``` moreover ``` chaieb@29687 ` 890` ``` {assume n: "n=0" hence ?thesis by (simp add: fps_mult_nth X_def)} ``` chaieb@29687 ` 891` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 892` ```qed ``` chaieb@29687 ` 893` chaieb@29687 ` 894` ```lemma X_mult_right_nth[simp]: "((f :: ('a::comm_semiring_1) fps) * X) \$n = (if n = 0 then 0 else f \$ (n - 1))" ``` chaieb@29687 ` 895` ``` by (metis X_mult_nth mult_commute) ``` chaieb@29687 ` 896` chaieb@29687 ` 897` ```lemma X_power_iff: "X^k = Abs_fps (\n. if n = k then (1::'a::comm_ring_1) else 0)" ``` chaieb@29687 ` 898` ```proof(induct k) ``` haftmann@30960 ` 899` ``` case 0 thus ?case by (simp add: X_def fps_eq_iff) ``` chaieb@29687 ` 900` ```next ``` chaieb@29687 ` 901` ``` case (Suc k) ``` huffman@30488 ` 902` ``` {fix m ``` chaieb@29687 ` 903` ``` have "(X^Suc k) \$ m = (if m = 0 then (0::'a) else (X^k) \$ (m - 1))" ``` chaieb@29687 ` 904` ``` by (simp add: power_Suc del: One_nat_def) ``` chaieb@29687 ` 905` ``` then have "(X^Suc k) \$ m = (if m = Suc k then (1::'a) else 0)" ``` chaieb@29687 ` 906` ``` using Suc.hyps by (auto cong del: if_weak_cong)} ``` chaieb@29687 ` 907` ``` then show ?case by (simp add: fps_eq_iff) ``` chaieb@29687 ` 908` ```qed ``` chaieb@29687 ` 909` chaieb@29687 ` 910` ```lemma X_power_mult_nth: "(X^k * (f :: ('a::comm_ring_1) fps)) \$n = (if n < k then 0 else f \$ (n - k))" ``` chaieb@29687 ` 911` ``` apply (induct k arbitrary: n) ``` chaieb@29687 ` 912` ``` apply (simp) ``` huffman@30488 ` 913` ``` unfolding power_Suc mult_assoc ``` chaieb@29687 ` 914` ``` by (case_tac n, auto) ``` chaieb@29687 ` 915` chaieb@29687 ` 916` ```lemma X_power_mult_right_nth: "((f :: ('a::comm_ring_1) fps) * X^k) \$n = (if n < k then 0 else f \$ (n - k))" ``` chaieb@29687 ` 917` ``` by (metis X_power_mult_nth mult_commute) ``` chaieb@29687 ` 918` ```lemma fps_deriv_X[simp]: "fps_deriv X = 1" ``` chaieb@29687 ` 919` ``` by (simp add: fps_deriv_def X_def fps_eq_iff) ``` chaieb@29687 ` 920` chaieb@29687 ` 921` ```lemma fps_nth_deriv_X[simp]: "fps_nth_deriv n X = (if n = 0 then X else if n=1 then 1 else 0)" ``` chaieb@29687 ` 922` ``` by (cases "n", simp_all) ``` chaieb@29687 ` 923` chaieb@29687 ` 924` ```lemma X_nth[simp]: "X\$n = (if n = 1 then 1 else 0)" by (simp add: X_def) ``` chaieb@29687 ` 925` ```lemma X_power_nth[simp]: "(X^k) \$n = (if n = k then 1 else (0::'a::comm_ring_1))" ``` chaieb@29687 ` 926` ``` by (simp add: X_power_iff) ``` chaieb@29687 ` 927` chaieb@29687 ` 928` ```lemma fps_inverse_X_plus1: ``` haftmann@31021 ` 929` ``` "inverse (1 + X) = Abs_fps (\n. (- (1::'a::{field})) ^ n)" (is "_ = ?r") ``` chaieb@29687 ` 930` ```proof- ``` chaieb@29687 ` 931` ``` have eq: "(1 + X) * ?r = 1" ``` chaieb@29687 ` 932` ``` unfolding minus_one_power_iff ``` nipkow@31148 ` 933` ``` by (auto simp add: ring_simps fps_eq_iff) ``` chaieb@29687 ` 934` ``` show ?thesis by (auto simp add: eq intro: fps_inverse_unique) ``` chaieb@29687 ` 935` ```qed ``` chaieb@29687 ` 936` huffman@30488 ` 937` huffman@29906 ` 938` ```subsection{* Integration *} ``` huffman@31273 ` 939` huffman@31273 ` 940` ```definition ``` huffman@31273 ` 941` ``` fps_integral :: "'a::field_char_0 fps \ 'a \ 'a fps" where ``` huffman@31273 ` 942` ``` "fps_integral a a0 = Abs_fps (\n. if n = 0 then a0 else (a\$(n - 1) / of_nat n))" ``` chaieb@29687 ` 943` huffman@31273 ` 944` ```lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a a0) = a" ``` huffman@31273 ` 945` ``` unfolding fps_integral_def fps_deriv_def ``` huffman@31273 ` 946` ``` by (simp add: fps_eq_iff del: of_nat_Suc) ``` chaieb@29687 ` 947` huffman@31273 ` 948` ```lemma fps_integral_linear: ``` huffman@31273 ` 949` ``` "fps_integral (fps_const a * f + fps_const b * g) (a*a0 + b*b0) = ``` huffman@31273 ` 950` ``` fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0" ``` huffman@31273 ` 951` ``` (is "?l = ?r") ``` chaieb@29687 ` 952` ```proof- ``` chaieb@29687 ` 953` ``` have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral) ``` chaieb@29687 ` 954` ``` moreover have "?l\$0 = ?r\$0" by (simp add: fps_integral_def) ``` chaieb@29687 ` 955` ``` ultimately show ?thesis ``` chaieb@29687 ` 956` ``` unfolding fps_deriv_eq_iff by auto ``` chaieb@29687 ` 957` ```qed ``` huffman@30488 ` 958` huffman@29906 ` 959` ```subsection {* Composition of FPSs *} ``` chaieb@29687 ` 960` ```definition fps_compose :: "('a::semiring_1) fps \ 'a fps \ 'a fps" (infixl "oo" 55) where ``` chaieb@29687 ` 961` ``` fps_compose_def: "a oo b = Abs_fps (\n. setsum (\i. a\$i * (b^i\$n)) {0..n})" ``` chaieb@29687 ` 962` chaieb@29687 ` 963` ```lemma fps_compose_nth: "(a oo b)\$n = setsum (\i. a\$i * (b^i\$n)) {0..n}" by (simp add: fps_compose_def) ``` chaieb@29687 ` 964` chaieb@29687 ` 965` ```lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)" ``` huffman@29913 ` 966` ``` by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta') ``` huffman@30488 ` 967` huffman@30488 ` 968` ```lemma fps_const_compose[simp]: ``` chaieb@29687 ` 969` ``` "fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)" ``` huffman@29913 ` 970` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 971` chaieb@31369 ` 972` ```lemma number_of_compose[simp]: "(number_of k::('a::{comm_ring_1}) fps) oo b = number_of k" ``` chaieb@31369 ` 973` ``` unfolding number_of_fps_const by simp ``` chaieb@31369 ` 974` chaieb@29687 ` 975` ```lemma X_fps_compose_startby0[simp]: "a\$0 = 0 \ X oo a = (a :: ('a :: comm_ring_1) fps)" ``` huffman@29913 ` 976` ``` by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta ``` huffman@29913 ` 977` ``` power_Suc not_le) ``` chaieb@29687 ` 978` chaieb@29687 ` 979` huffman@29906 ` 980` ```subsection {* Rules from Herbert Wilf's Generatingfunctionology*} ``` chaieb@29687 ` 981` huffman@29906 ` 982` ```subsubsection {* Rule 1 *} ``` chaieb@29687 ` 983` ``` (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\i. a_i * x^i))/x^h, for h>0*) ``` chaieb@29687 ` 984` huffman@30488 ` 985` ```lemma fps_power_mult_eq_shift: ``` chaieb@30992 ` 986` ``` "X^Suc k * Abs_fps (\n. a (n + Suc k)) = Abs_fps a - setsum (\i. fps_const (a i :: 'a:: comm_ring_1) * X^i) {0 .. k}" (is "?lhs = ?rhs") ``` chaieb@29687 ` 987` ```proof- ``` chaieb@29687 ` 988` ``` {fix n:: nat ``` huffman@30488 ` 989` ``` have "?lhs \$ n = (if n < Suc k then 0 else a n)" ``` chaieb@29687 ` 990` ``` unfolding X_power_mult_nth by auto ``` chaieb@29687 ` 991` ``` also have "\ = ?rhs \$ n" ``` chaieb@29687 ` 992` ``` proof(induct k) ``` chaieb@29687 ` 993` ``` case 0 thus ?case by (simp add: fps_setsum_nth power_Suc) ``` chaieb@29687 ` 994` ``` next ``` chaieb@29687 ` 995` ``` case (Suc k) ``` chaieb@29687 ` 996` ``` note th = Suc.hyps[symmetric] ``` chaieb@30992 ` 997` ``` have "(Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})\$n = (Abs_fps a - setsum (\i. fps_const (a i :: 'a) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) \$ n" by (simp add: ring_simps) ``` chaieb@29687 ` 998` ``` also have "\ = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)\$n" ``` huffman@30488 ` 999` ``` using th ``` chaieb@29687 ` 1000` ``` unfolding fps_sub_nth by simp ``` chaieb@29687 ` 1001` ``` also have "\ = (if n < Suc (Suc k) then 0 else a n)" ``` chaieb@29687 ` 1002` ``` unfolding X_power_mult_right_nth ``` chaieb@29687 ` 1003` ``` apply (auto simp add: not_less fps_const_def) ``` chaieb@29687 ` 1004` ``` apply (rule cong[of a a, OF refl]) ``` chaieb@29687 ` 1005` ``` by arith ``` chaieb@29687 ` 1006` ``` finally show ?case by simp ``` chaieb@29687 ` 1007` ``` qed ``` chaieb@29687 ` 1008` ``` finally have "?lhs \$ n = ?rhs \$ n" .} ``` chaieb@29687 ` 1009` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1010` ```qed ``` chaieb@29687 ` 1011` huffman@29906 ` 1012` ```subsubsection{* Rule 2*} ``` chaieb@29687 ` 1013` chaieb@29687 ` 1014` ``` (* We can not reach the form of Wilf, but still near to it using rewrite rules*) ``` huffman@30488 ` 1015` ``` (* If f reprents {a_n} and P is a polynomial, then ``` chaieb@29687 ` 1016` ``` P(xD) f represents {P(n) a_n}*) ``` chaieb@29687 ` 1017` chaieb@29687 ` 1018` ```definition "XD = op * X o fps_deriv" ``` chaieb@29687 ` 1019` chaieb@29687 ` 1020` ```lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)" ``` chaieb@29687 ` 1021` ``` by (simp add: XD_def ring_simps) ``` chaieb@29687 ` 1022` chaieb@29687 ` 1023` ```lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a" ``` chaieb@29687 ` 1024` ``` by (simp add: XD_def ring_simps) ``` chaieb@29687 ` 1025` chaieb@29687 ` 1026` ```lemma XD_linear[simp]: "XD (fps_const c * a + fps_const d * b) = fps_const c * XD a + fps_const d * XD (b :: ('a::comm_ring_1) fps)" ``` chaieb@29687 ` 1027` ``` by simp ``` chaieb@29687 ` 1028` haftmann@30952 ` 1029` ```lemma XDN_linear: ``` haftmann@30971 ` 1030` ``` "(XD ^^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD ^^ n) a + fps_const d * (XD ^^ n) (b :: ('a::comm_ring_1) fps)" ``` chaieb@29687 ` 1031` ``` by (induct n, simp_all) ``` chaieb@29687 ` 1032` chaieb@29687 ` 1033` ```lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\n. of_nat n* a\$n)" by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1034` chaieb@30994 ` 1035` haftmann@30952 ` 1036` ```lemma fps_mult_XD_shift: ``` haftmann@31021 ` 1037` ``` "(XD ^^ k) (a:: ('a::{comm_ring_1}) fps) = Abs_fps (\n. (of_nat n ^ k) * a\$n)" ``` haftmann@30952 ` 1038` ``` by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def) ``` chaieb@29687 ` 1039` huffman@29906 ` 1040` ```subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} ``` huffman@29906 ` 1041` ```subsubsection{* Rule 5 --- summation and "division" by (1 - X)*} ``` chaieb@29687 ` 1042` chaieb@29687 ` 1043` ```lemma fps_divide_X_minus1_setsum_lemma: ``` chaieb@29687 ` 1044` ``` "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1045` ```proof- ``` chaieb@29687 ` 1046` ``` let ?X = "X::('a::comm_ring_1) fps" ``` chaieb@29687 ` 1047` ``` let ?sa = "Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1048` ``` have th0: "\i. (1 - (X::'a fps)) \$ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" by simp ``` chaieb@29687 ` 1049` ``` {fix n:: nat ``` huffman@30488 ` 1050` ``` {assume "n=0" hence "a\$n = ((1 - ?X) * ?sa) \$ n" ``` chaieb@29687 ` 1051` ``` by (simp add: fps_mult_nth)} ``` chaieb@29687 ` 1052` ``` moreover ``` chaieb@29687 ` 1053` ``` {assume n0: "n \ 0" ``` chaieb@29687 ` 1054` ``` then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1}\{2..n} = {1..n}" ``` chaieb@29687 ` 1055` ``` "{0..n - 1}\{n} = {0..n}" ``` chaieb@29687 ` 1056` ``` apply (simp_all add: expand_set_eq) by presburger+ ``` huffman@30488 ` 1057` ``` have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" ``` chaieb@29687 ` 1058` ``` "{0..n - 1}\{n} ={}" using n0 ``` chaieb@29687 ` 1059` ``` by (simp_all add: expand_set_eq, presburger+) ``` huffman@30488 ` 1060` ``` have f: "finite {0}" "finite {1}" "finite {2 .. n}" ``` huffman@30488 ` 1061` ``` "finite {0 .. n - 1}" "finite {n}" by simp_all ``` chaieb@29687 ` 1062` ``` have "((1 - ?X) * ?sa) \$ n = setsum (\i. (1 - ?X)\$ i * ?sa \$ (n - i)) {0 .. n}" ``` chaieb@29687 ` 1063` ``` by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1064` ``` also have "\ = a\$n" unfolding th0 ``` chaieb@29687 ` 1065` ``` unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] ``` chaieb@29687 ` 1066` ``` unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] ``` chaieb@29687 ` 1067` ``` apply (simp) ``` chaieb@29687 ` 1068` ``` unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)] ``` chaieb@29687 ` 1069` ``` by simp ``` chaieb@29687 ` 1070` ``` finally have "a\$n = ((1 - ?X) * ?sa) \$ n" by simp} ``` chaieb@29687 ` 1071` ``` ultimately have "a\$n = ((1 - ?X) * ?sa) \$ n" by blast} ``` huffman@30488 ` 1072` ```then show ?thesis ``` chaieb@29687 ` 1073` ``` unfolding fps_eq_iff by blast ``` chaieb@29687 ` 1074` ```qed ``` chaieb@29687 ` 1075` chaieb@29687 ` 1076` ```lemma fps_divide_X_minus1_setsum: ``` chaieb@29687 ` 1077` ``` "a /((1::('a::field) fps) - X) = Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1078` ```proof- ``` chaieb@29687 ` 1079` ``` let ?X = "1 - (X::('a::field) fps)" ``` chaieb@29687 ` 1080` ``` have th0: "?X \$ 0 \ 0" by simp ``` chaieb@29687 ` 1081` ``` have "a /?X = ?X * Abs_fps (\n\nat. setsum (op \$ a) {0..n}) * inverse ?X" ``` chaieb@29687 ` 1082` ``` using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0 ``` chaieb@29687 ` 1083` ``` by (simp add: fps_divide_def mult_assoc) ``` chaieb@29687 ` 1084` ``` also have "\ = (inverse ?X * ?X) * Abs_fps (\n\nat. setsum (op \$ a) {0..n}) " ``` chaieb@29687 ` 1085` ``` by (simp add: mult_ac) ``` chaieb@29687 ` 1086` ``` finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) ``` chaieb@29687 ` 1087` ```qed ``` chaieb@29687 ` 1088` huffman@30488 ` 1089` ```subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary ``` chaieb@29687 ` 1090` ``` finite product of FPS, also the relvant instance of powers of a FPS*} ``` chaieb@29687 ` 1091` chaieb@29687 ` 1092` ```definition "natpermute n k = {l:: nat list. length l = k \ foldl op + 0 l = n}" ``` chaieb@29687 ` 1093` chaieb@29687 ` 1094` ```lemma natlist_trivial_1: "natpermute n 1 = {[n]}" ``` chaieb@29687 ` 1095` ``` apply (auto simp add: natpermute_def) ``` chaieb@29687 ` 1096` ``` apply (case_tac x, auto) ``` chaieb@29687 ` 1097` ``` done ``` chaieb@29687 ` 1098` huffman@30488 ` 1099` ```lemma foldl_add_start0: ``` chaieb@29687 ` 1100` ``` "foldl op + x xs = x + foldl op + (0::nat) xs" ``` chaieb@29687 ` 1101` ``` apply (induct xs arbitrary: x) ``` chaieb@29687 ` 1102` ``` apply simp ``` chaieb@29687 ` 1103` ``` unfolding foldl.simps ``` chaieb@29687 ` 1104` ``` apply atomize ``` chaieb@29687 ` 1105` ``` apply (subgoal_tac "\x\nat. foldl op + x xs = x + foldl op + (0\nat) xs") ``` chaieb@29687 ` 1106` ``` apply (erule_tac x="x + a" in allE) ``` chaieb@29687 ` 1107` ``` apply (erule_tac x="a" in allE) ``` chaieb@29687 ` 1108` ``` apply simp ``` chaieb@29687 ` 1109` ``` apply assumption ``` chaieb@29687 ` 1110` ``` done ``` chaieb@29687 ` 1111` chaieb@29687 ` 1112` ```lemma foldl_add_append: "foldl op + (x::nat) (xs@ys) = foldl op + x xs + foldl op + 0 ys" ``` chaieb@29687 ` 1113` ``` apply (induct ys arbitrary: x xs) ``` chaieb@29687 ` 1114` ``` apply auto ``` chaieb@29687 ` 1115` ``` apply (subst (2) foldl_add_start0) ``` chaieb@29687 ` 1116` ``` apply simp ``` chaieb@29687 ` 1117` ``` apply (subst (2) foldl_add_start0) ``` chaieb@29687 ` 1118` ``` by simp ``` chaieb@29687 ` 1119` chaieb@29687 ` 1120` ```lemma foldl_add_setsum: "foldl op + (x::nat) xs = x + setsum (nth xs) {0.. {1.. {1.. = x + a + setsum (op ! as) {0.. = x + setsum (op ! (a#as)) {0.. natpermute n k" shows "foldl op + 0 xs \ n" and "foldl op + 0 ys \ n" ``` chaieb@29687 ` 1144` ```proof- ``` chaieb@29687 ` 1145` ``` {from h have "foldl op + 0 (xs@ ys) = n" by (simp add: natpermute_def) ``` chaieb@29687 ` 1146` ``` hence "foldl op + 0 xs + foldl op + 0 ys = n" unfolding foldl_add_append .} ``` chaieb@29687 ` 1147` ``` note th = this ``` chaieb@29687 ` 1148` ``` {from th show "foldl op + 0 xs \ n" by simp} ``` chaieb@29687 ` 1149` ``` {from th show "foldl op + 0 ys \ n" by simp} ``` chaieb@29687 ` 1150` ```qed ``` chaieb@29687 ` 1151` chaieb@29687 ` 1152` ```lemma natpermute_split: ``` chaieb@29687 ` 1153` ``` assumes mn: "h \ k" ``` chaieb@29687 ` 1154` ``` shows "natpermute n k = (\m \{0..n}. {l1 @ l2 |l1 l2. l1 \ natpermute m h \ l2 \ natpermute (n - m) (k - h)})" (is "?L = ?R" is "?L = (\m \{0..n}. ?S m)") ``` chaieb@29687 ` 1155` ```proof- ``` huffman@30488 ` 1156` ``` {fix l assume l: "l \ ?R" ``` chaieb@29687 ` 1157` ``` from l obtain m xs ys where h: "m \ {0..n}" and xs: "xs \ natpermute m h" and ys: "ys \ natpermute (n - m) (k - h)" and leq: "l = xs@ys" by blast ``` chaieb@29687 ` 1158` ``` from xs have xs': "foldl op + 0 xs = m" by (simp add: natpermute_def) ``` chaieb@29687 ` 1159` ``` from ys have ys': "foldl op + 0 ys = n - m" by (simp add: natpermute_def) ``` huffman@30488 ` 1160` ``` have "l \ ?L" using leq xs ys h ``` chaieb@29687 ` 1161` ``` apply simp ``` chaieb@29687 ` 1162` ``` apply (clarsimp simp add: natpermute_def simp del: foldl_append) ``` chaieb@29687 ` 1163` ``` apply (simp add: foldl_add_append[unfolded foldl_append]) ``` chaieb@29687 ` 1164` ``` unfolding xs' ys' ``` huffman@30488 ` 1165` ``` using mn xs ys ``` chaieb@29687 ` 1166` ``` unfolding natpermute_def by simp} ``` chaieb@29687 ` 1167` ``` moreover ``` chaieb@29687 ` 1168` ``` {fix l assume l: "l \ natpermute n k" ``` chaieb@29687 ` 1169` ``` let ?xs = "take h l" ``` chaieb@29687 ` 1170` ``` let ?ys = "drop h l" ``` chaieb@29687 ` 1171` ``` let ?m = "foldl op + 0 ?xs" ``` chaieb@29687 ` 1172` ``` from l have ls: "foldl op + 0 (?xs @ ?ys) = n" by (simp add: natpermute_def) ``` huffman@30488 ` 1173` ``` have xs: "?xs \ natpermute ?m h" using l mn by (simp add: natpermute_def) ``` chaieb@29687 ` 1174` ``` have ys: "?ys \ natpermute (n - ?m) (k - h)" using l mn ls[unfolded foldl_add_append] ``` chaieb@29687 ` 1175` ``` by (simp add: natpermute_def) ``` chaieb@29687 ` 1176` ``` from ls have m: "?m \ {0..n}" unfolding foldl_add_append by simp ``` huffman@30488 ` 1177` ``` from xs ys ls have "l \ ?R" ``` chaieb@29687 ` 1178` ``` apply auto ``` chaieb@29687 ` 1179` ``` apply (rule bexI[where x = "?m"]) ``` chaieb@29687 ` 1180` ``` apply (rule exI[where x = "?xs"]) ``` chaieb@29687 ` 1181` ``` apply (rule exI[where x = "?ys"]) ``` huffman@30488 ` 1182` ``` using ls l unfolding foldl_add_append ``` chaieb@29687 ` 1183` ``` by (auto simp add: natpermute_def)} ``` chaieb@29687 ` 1184` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1185` ```qed ``` chaieb@29687 ` 1186` chaieb@29687 ` 1187` ```lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" ``` chaieb@29687 ` 1188` ``` by (auto simp add: natpermute_def) ``` chaieb@29687 ` 1189` ```lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" ``` chaieb@29687 ` 1190` ``` apply (auto simp add: set_replicate_conv_if natpermute_def) ``` chaieb@29687 ` 1191` ``` apply (rule nth_equalityI) ``` chaieb@29687 ` 1192` ``` by simp_all ``` chaieb@29687 ` 1193` chaieb@29687 ` 1194` ```lemma natpermute_finite: "finite (natpermute n k)" ``` chaieb@29687 ` 1195` ```proof(induct k arbitrary: n) ``` huffman@30488 ` 1196` ``` case 0 thus ?case ``` chaieb@29687 ` 1197` ``` apply (subst natpermute_split[of 0 0, simplified]) ``` chaieb@29687 ` 1198` ``` by (simp add: natpermute_0) ``` chaieb@29687 ` 1199` ```next ``` chaieb@29687 ` 1200` ``` case (Suc k) ``` chaieb@29687 ` 1201` ``` then show ?case unfolding natpermute_split[of k "Suc k", simplified] ``` chaieb@29687 ` 1202` ``` apply - ``` chaieb@29687 ` 1203` ``` apply (rule finite_UN_I) ``` chaieb@29687 ` 1204` ``` apply simp ``` chaieb@29687 ` 1205` ``` unfolding One_nat_def[symmetric] natlist_trivial_1 ``` chaieb@29687 ` 1206` ``` apply simp ``` chaieb@29687 ` 1207` ``` unfolding image_Collect[symmetric] ``` chaieb@29687 ` 1208` ``` unfolding Collect_def mem_def ``` chaieb@29687 ` 1209` ``` apply (rule finite_imageI) ``` chaieb@29687 ` 1210` ``` apply blast ``` chaieb@29687 ` 1211` ``` done ``` chaieb@29687 ` 1212` ```qed ``` chaieb@29687 ` 1213` chaieb@29687 ` 1214` ```lemma natpermute_contain_maximal: ``` chaieb@29687 ` 1215` ``` "{xs \ natpermute n (k+1). n \ set xs} = UNION {0 .. k} (\i. {(replicate (k+1) 0) [i:=n]})" ``` chaieb@29687 ` 1216` ``` (is "?A = ?B") ``` chaieb@29687 ` 1217` ```proof- ``` chaieb@29687 ` 1218` ``` {fix xs assume H: "xs \ natpermute n (k+1)" and n: "n \ set xs" ``` chaieb@29687 ` 1219` ``` from n obtain i where i: "i \ {0.. k}" "xs!i = n" using H ``` huffman@30488 ` 1220` ``` unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def) ``` chaieb@29687 ` 1221` ``` have eqs: "({0..k} - {i}) \ {i} = {0..k}" using i by auto ``` chaieb@29687 ` 1222` ``` have f: "finite({0..k} - {i})" "finite {i}" by auto ``` chaieb@29687 ` 1223` ``` have d: "({0..k} - {i}) \ {i} = {}" using i by auto ``` chaieb@29687 ` 1224` ``` from H have "n = setsum (nth xs) {0..k}" apply (simp add: natpermute_def) ``` chaieb@29687 ` 1225` ``` unfolding foldl_add_setsum by (auto simp add: atLeastLessThanSuc_atLeastAtMost) ``` chaieb@29687 ` 1226` ``` also have "\ = n + setsum (nth xs) ({0..k} - {i})" ``` chaieb@29687 ` 1227` ``` unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp ``` chaieb@29687 ` 1228` ``` finally have zxs: "\ j\ {0..k} - {i}. xs!j = 0" by auto ``` chaieb@29687 ` 1229` ``` from H have xsl: "length xs = k+1" by (simp add: natpermute_def) ``` chaieb@29687 ` 1230` ``` from i have i': "i < length (replicate (k+1) 0)" "i < k+1" ``` chaieb@29687 ` 1231` ``` unfolding length_replicate by arith+ ``` chaieb@29687 ` 1232` ``` have "xs = replicate (k+1) 0 [i := n]" ``` chaieb@29687 ` 1233` ``` apply (rule nth_equalityI) ``` chaieb@29687 ` 1234` ``` unfolding xsl length_list_update length_replicate ``` chaieb@29687 ` 1235` ``` apply simp ``` chaieb@29687 ` 1236` ``` apply clarify ``` chaieb@29687 ` 1237` ``` unfolding nth_list_update[OF i'(1)] ``` chaieb@29687 ` 1238` ``` using i zxs ``` chaieb@29687 ` 1239` ``` by (case_tac "ia=i", auto simp del: replicate.simps) ``` chaieb@29687 ` 1240` ``` then have "xs \ ?B" using i by blast} ``` chaieb@29687 ` 1241` ``` moreover ``` chaieb@29687 ` 1242` ``` {fix i assume i: "i \ {0..k}" ``` chaieb@29687 ` 1243` ``` let ?xs = "replicate (k+1) 0 [i:=n]" ``` chaieb@29687 ` 1244` ``` have nxs: "n \ set ?xs" ``` chaieb@29687 ` 1245` ``` apply (rule set_update_memI) using i by simp ``` chaieb@29687 ` 1246` ``` have xsl: "length ?xs = k+1" by (simp only: length_replicate length_list_update) ``` chaieb@29687 ` 1247` ``` have "foldl op + 0 ?xs = setsum (nth ?xs) {0.. = setsum (\j. if j = i then n else 0) {0..< k+1}" ``` chaieb@29687 ` 1250` ``` apply (rule setsum_cong2) by (simp del: replicate.simps) ``` chaieb@29687 ` 1251` ``` also have "\ = n" using i by (simp add: setsum_delta) ``` huffman@30488 ` 1252` ``` finally ``` chaieb@29687 ` 1253` ``` have "?xs \ natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def ``` chaieb@29687 ` 1254` ``` by blast ``` chaieb@29687 ` 1255` ``` then have "?xs \ ?A" using nxs by blast} ``` chaieb@29687 ` 1256` ``` ultimately show ?thesis by auto ``` chaieb@29687 ` 1257` ```qed ``` chaieb@29687 ` 1258` huffman@30488 ` 1259` ``` (* The general form *) ``` chaieb@29687 ` 1260` ```lemma fps_setprod_nth: ``` chaieb@29687 ` 1261` ``` fixes m :: nat and a :: "nat \ ('a::comm_ring_1) fps" ``` chaieb@29687 ` 1262` ``` shows "(setprod a {0 .. m})\$n = setsum (\v. setprod (\j. (a j) \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` chaieb@29687 ` 1263` ``` (is "?P m n") ``` chaieb@29687 ` 1264` ```proof(induct m arbitrary: n rule: nat_less_induct) ``` chaieb@29687 ` 1265` ``` fix m n assume H: "\m' < m. \n. ?P m' n" ``` chaieb@29687 ` 1266` ``` {assume m0: "m = 0" ``` chaieb@29687 ` 1267` ``` hence "?P m n" apply simp ``` chaieb@29687 ` 1268` ``` unfolding natlist_trivial_1[where n = n, unfolded One_nat_def] by simp} ``` chaieb@29687 ` 1269` ``` moreover ``` chaieb@29687 ` 1270` ``` {fix k assume k: "m = Suc k" ``` chaieb@29687 ` 1271` ``` have km: "k < m" using k by arith ``` chaieb@29687 ` 1272` ``` have u0: "{0 .. k} \ {m} = {0..m}" using k apply (simp add: expand_set_eq) by presburger ``` chaieb@29687 ` 1273` ``` have f0: "finite {0 .. k}" "finite {m}" by auto ``` chaieb@29687 ` 1274` ``` have d0: "{0 .. k} \ {m} = {}" using k by auto ``` chaieb@29687 ` 1275` ``` have "(setprod a {0 .. m}) \$ n = (setprod a {0 .. k} * a m) \$ n" ``` chaieb@29687 ` 1276` ``` unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0] by simp ``` chaieb@29687 ` 1277` ``` also have "\ = (\i = 0..n. (\v\natpermute i (k + 1). \j\{0..k}. a j \$ v ! j) * a m \$ (n - i))" ``` chaieb@29687 ` 1278` ``` unfolding fps_mult_nth H[rule_format, OF km] .. ``` chaieb@29687 ` 1279` ``` also have "\ = (\v\natpermute n (m + 1). \j\{0..m}. a j \$ v ! j)" ``` chaieb@29687 ` 1280` ``` apply (simp add: k) ``` chaieb@29687 ` 1281` ``` unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k] ``` chaieb@29687 ` 1282` ``` apply (subst setsum_UN_disjoint) ``` huffman@30488 ` 1283` ``` apply simp ``` chaieb@29687 ` 1284` ``` apply simp ``` chaieb@29687 ` 1285` ``` unfolding image_Collect[symmetric] ``` chaieb@29687 ` 1286` ``` apply clarsimp ``` chaieb@29687 ` 1287` ``` apply (rule finite_imageI) ``` chaieb@29687 ` 1288` ``` apply (rule natpermute_finite) ``` chaieb@29687 ` 1289` ``` apply (clarsimp simp add: expand_set_eq) ``` chaieb@29687 ` 1290` ``` apply auto ``` chaieb@29687 ` 1291` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1292` ``` unfolding setsum_left_distrib ``` chaieb@29687 ` 1293` ``` apply (rule sym) ``` chaieb@29687 ` 1294` ``` apply (rule_tac f="\xs. xs @[n - x]" in setsum_reindex_cong) ``` chaieb@29687 ` 1295` ``` apply (simp add: inj_on_def) ``` chaieb@29687 ` 1296` ``` apply auto ``` chaieb@29687 ` 1297` ``` unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k] ``` chaieb@29687 ` 1298` ``` apply (clarsimp simp add: natpermute_def nth_append) ``` chaieb@29687 ` 1299` ``` done ``` chaieb@29687 ` 1300` ``` finally have "?P m n" .} ``` chaieb@29687 ` 1301` ``` ultimately show "?P m n " by (cases m, auto) ``` chaieb@29687 ` 1302` ```qed ``` chaieb@29687 ` 1303` chaieb@29687 ` 1304` ```text{* The special form for powers *} ``` chaieb@29687 ` 1305` ```lemma fps_power_nth_Suc: ``` chaieb@29687 ` 1306` ``` fixes m :: nat and a :: "('a::comm_ring_1) fps" ``` chaieb@29687 ` 1307` ``` shows "(a ^ Suc m)\$n = setsum (\v. setprod (\j. a \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` chaieb@29687 ` 1308` ```proof- ``` chaieb@29687 ` 1309` ``` have f: "finite {0 ..m}" by simp ``` chaieb@29687 ` 1310` ``` have th0: "a^Suc m = setprod (\i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp ``` chaieb@29687 ` 1311` ``` show ?thesis unfolding th0 fps_setprod_nth .. ``` chaieb@29687 ` 1312` ```qed ``` chaieb@29687 ` 1313` ```lemma fps_power_nth: ``` chaieb@29687 ` 1314` ``` fixes m :: nat and a :: "('a::comm_ring_1) fps" ``` chaieb@29687 ` 1315` ``` shows "(a ^m)\$n = (if m=0 then 1\$n else setsum (\v. setprod (\j. a \$ (v!j)) {0..m - 1}) (natpermute n m))" ``` huffman@30273 ` 1316` ``` by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc) ``` chaieb@29687 ` 1317` huffman@30488 ` 1318` ```lemma fps_nth_power_0: ``` haftmann@31021 ` 1319` ``` fixes m :: nat and a :: "('a::{comm_ring_1}) fps" ``` chaieb@29687 ` 1320` ``` shows "(a ^m)\$0 = (a\$0) ^ m" ``` chaieb@29687 ` 1321` ```proof- ``` chaieb@29687 ` 1322` ``` {assume "m=0" hence ?thesis by simp} ``` chaieb@29687 ` 1323` ``` moreover ``` chaieb@29687 ` 1324` ``` {fix n assume m: "m = Suc n" ``` chaieb@29687 ` 1325` ``` have c: "m = card {0..n}" using m by simp ``` chaieb@29687 ` 1326` ``` have "(a ^m)\$0 = setprod (\i. a\$0) {0..n}" ``` nipkow@30837 ` 1327` ``` by (simp add: m fps_power_nth del: replicate.simps power_Suc) ``` chaieb@29687 ` 1328` ``` also have "\ = (a\$0) ^ m" ``` chaieb@29687 ` 1329` ``` unfolding c by (rule setprod_constant, simp) ``` chaieb@29687 ` 1330` ``` finally have ?thesis .} ``` chaieb@29687 ` 1331` ``` ultimately show ?thesis by (cases m, auto) ``` chaieb@29687 ` 1332` ```qed ``` chaieb@29687 ` 1333` huffman@30488 ` 1334` ```lemma fps_compose_inj_right: ``` haftmann@31021 ` 1335` ``` assumes a0: "a\$0 = (0::'a::{idom})" ``` chaieb@29687 ` 1336` ``` and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1337` ``` shows "(b oo a = c oo a) \ b = c" (is "?lhs \?rhs") ``` chaieb@29687 ` 1338` ```proof- ``` chaieb@29687 ` 1339` ``` {assume ?rhs then have "?lhs" by simp} ``` chaieb@29687 ` 1340` ``` moreover ``` chaieb@29687 ` 1341` ``` {assume h: ?lhs ``` huffman@30488 ` 1342` ``` {fix n have "b\$n = c\$n" ``` chaieb@29687 ` 1343` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1344` ``` fix n assume H: "\m {n} = {0 .. n}" using n1 by auto ``` chaieb@29687 ` 1352` ``` have d: "{0 .. n1} \ {n} = {}" using n1 by auto ``` chaieb@29687 ` 1353` ``` have seq: "(\i = 0..n1. b \$ i * a ^ i \$ n) = (\i = 0..n1. c \$ i * a ^ i \$ n)" ``` chaieb@29687 ` 1354` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1355` ``` using H n1 by auto ``` chaieb@29687 ` 1356` ``` have th0: "(b oo a) \$n = (\i = 0..n1. c \$ i * a ^ i \$ n) + b\$n * (a\$1)^n" ``` chaieb@29687 ` 1357` ``` unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] seq ``` chaieb@29687 ` 1358` ``` using startsby_zero_power_nth_same[OF a0] ``` chaieb@29687 ` 1359` ``` by simp ``` chaieb@29687 ` 1360` ``` have th1: "(c oo a) \$n = (\i = 0..n1. c \$ i * a ^ i \$ n) + c\$n * (a\$1)^n" ``` chaieb@29687 ` 1361` ``` unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] ``` chaieb@29687 ` 1362` ``` using startsby_zero_power_nth_same[OF a0] ``` chaieb@29687 ` 1363` ``` by simp ``` chaieb@29687 ` 1364` ``` from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 ``` chaieb@29687 ` 1365` ``` have "b\$n = c\$n" by auto} ``` chaieb@29687 ` 1366` ``` ultimately show "b\$n = c\$n" by (cases n, auto) ``` chaieb@29687 ` 1367` ``` qed} ``` chaieb@29687 ` 1368` ``` then have ?rhs by (simp add: fps_eq_iff)} ``` chaieb@29687 ` 1369` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1370` ```qed ``` chaieb@29687 ` 1371` chaieb@29687 ` 1372` huffman@29906 ` 1373` ```subsection {* Radicals *} ``` chaieb@29687 ` 1374` chaieb@29687 ` 1375` ```declare setprod_cong[fundef_cong] ``` haftmann@31021 ` 1376` ```function radical :: "(nat \ 'a \ 'a) \ nat \ ('a::{field}) fps \ nat \ 'a" where ``` chaieb@29687 ` 1377` ``` "radical r 0 a 0 = 1" ``` chaieb@29687 ` 1378` ```| "radical r 0 a (Suc n) = 0" ``` chaieb@29687 ` 1379` ```| "radical r (Suc k) a 0 = r (Suc k) (a\$0)" ``` chaieb@29687 ` 1380` ```| "radical r (Suc k) a (Suc n) = (a\$ Suc n - setsum (\xs. setprod (\j. radical r (Suc k) a (xs ! j)) {0..k}) {xs. xs \ natpermute (Suc n) (Suc k) \ Suc n \ set xs}) / (of_nat (Suc k) * (radical r (Suc k) a 0)^k)" ``` chaieb@29687 ` 1381` ```by pat_completeness auto ``` chaieb@29687 ` 1382` chaieb@29687 ` 1383` ```termination radical ``` chaieb@29687 ` 1384` ```proof ``` chaieb@29687 ` 1385` ``` let ?R = "measure (\(r, k, a, n). n)" ``` chaieb@29687 ` 1386` ``` { ``` chaieb@29687 ` 1387` ``` show "wf ?R" by auto} ``` chaieb@29687 ` 1388` ``` {fix r k a n xs i ``` chaieb@29687 ` 1389` ``` assume xs: "xs \ {xs \ natpermute (Suc n) (Suc k). Suc n \ set xs}" and i: "i \ {0..k}" ``` chaieb@29687 ` 1390` ``` {assume c: "Suc n \ xs ! i" ``` chaieb@29687 ` 1391` ``` from xs i have "xs !i \ Suc n" by (auto simp add: in_set_conv_nth natpermute_def) ``` chaieb@29687 ` 1392` ``` with c have c': "Suc n < xs!i" by arith ``` chaieb@29687 ` 1393` ``` have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1.. ({i} \ {i+1 ..< Suc k}) = {}" "{i} \ {i+1..< Suc k} = {}" by auto ``` chaieb@29687 ` 1395` ``` have eqs: "{0.. ({i} \ {i+1 ..< Suc k})" using i by auto ``` chaieb@29687 ` 1396` ``` from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def) ``` chaieb@29687 ` 1397` ``` also have "\ = setsum (nth xs) {0.. = xs!i + setsum (nth xs) {0.. ?R" ``` chaieb@29687 ` 1405` ``` apply auto by (metis not_less)} ``` huffman@30488 ` 1406` ``` {fix r k a n ``` chaieb@29687 ` 1407` ``` show "((r,Suc k, a, 0),r, Suc k, a, Suc n) \ ?R" by simp} ``` chaieb@29687 ` 1408` ```qed ``` chaieb@29687 ` 1409` chaieb@29687 ` 1410` ```definition "fps_radical r n a = Abs_fps (radical r n a)" ``` chaieb@29687 ` 1411` chaieb@29687 ` 1412` ```lemma fps_radical0[simp]: "fps_radical r 0 a = 1" ``` chaieb@29687 ` 1413` ``` apply (auto simp add: fps_eq_iff fps_radical_def) by (case_tac n, auto) ``` chaieb@29687 ` 1414` chaieb@29687 ` 1415` ```lemma fps_radical_nth_0[simp]: "fps_radical r n a \$ 0 = (if n=0 then 1 else r n (a\$0))" ``` chaieb@29687 ` 1416` ``` by (cases n, simp_all add: fps_radical_def) ``` chaieb@29687 ` 1417` huffman@30488 ` 1418` ```lemma fps_radical_power_nth[simp]: ``` chaieb@29687 ` 1419` ``` assumes r: "(r k (a\$0)) ^ k = a\$0" ``` chaieb@29687 ` 1420` ``` shows "fps_radical r k a ^ k \$ 0 = (if k = 0 then 1 else a\$0)" ``` chaieb@29687 ` 1421` ```proof- ``` chaieb@29687 ` 1422` ``` {assume "k=0" hence ?thesis by simp } ``` chaieb@29687 ` 1423` ``` moreover ``` huffman@30488 ` 1424` ``` {fix h assume h: "k = Suc h" ``` chaieb@29687 ` 1425` ``` have fh: "finite {0..h}" by simp ``` chaieb@29687 ` 1426` ``` have eq1: "fps_radical r k a ^ k \$ 0 = (\j\{0..h}. fps_radical r k a \$ (replicate k 0) ! j)" ``` chaieb@29687 ` 1427` ``` unfolding fps_power_nth h by simp ``` chaieb@29687 ` 1428` ``` also have "\ = (\j\{0..h}. r k (a\$0))" ``` chaieb@29687 ` 1429` ``` apply (rule setprod_cong) ``` chaieb@29687 ` 1430` ``` apply simp ``` chaieb@29687 ` 1431` ``` using h ``` chaieb@29687 ` 1432` ``` apply (subgoal_tac "replicate k (0::nat) ! x = 0") ``` chaieb@29687 ` 1433` ``` by (auto intro: nth_replicate simp del: replicate.simps) ``` chaieb@29687 ` 1434` ``` also have "\ = a\$0" ``` chaieb@29687 ` 1435` ``` unfolding setprod_constant[OF fh] using r by (simp add: h) ``` chaieb@29687 ` 1436` ``` finally have ?thesis using h by simp} ``` chaieb@29687 ` 1437` ``` ultimately show ?thesis by (cases k, auto) ``` huffman@30488 ` 1438` ```qed ``` chaieb@29687 ` 1439` huffman@30488 ` 1440` ```lemma natpermute_max_card: assumes n0: "n\0" ``` chaieb@29687 ` 1441` ``` shows "card {xs \ natpermute n (k+1). n \ set xs} = k+1" ``` chaieb@29687 ` 1442` ``` unfolding natpermute_contain_maximal ``` chaieb@29687 ` 1443` ```proof- ``` chaieb@29687 ` 1444` ``` let ?A= "\i. {replicate (k + 1) 0[i := n]}" ``` chaieb@29687 ` 1445` ``` let ?K = "{0 ..k}" ``` chaieb@29687 ` 1446` ``` have fK: "finite ?K" by simp ``` chaieb@29687 ` 1447` ``` have fAK: "\i\?K. finite (?A i)" by auto ``` chaieb@29687 ` 1448` ``` have d: "\i\ ?K. \j\ ?K. i \ j \ {replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` chaieb@29687 ` 1449` ``` proof(clarify) ``` chaieb@29687 ` 1450` ``` fix i j assume i: "i \ ?K" and j: "j\ ?K" and ij: "i\j" ``` chaieb@29687 ` 1451` ``` {assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" ``` chaieb@29687 ` 1452` ``` have "(replicate (k+1) 0 [i:=n] ! i) = n" using i by (simp del: replicate.simps) ``` chaieb@29687 ` 1453` ``` moreover ``` chaieb@29687 ` 1454` ``` have "(replicate (k+1) 0 [j:=n] ! i) = 0" using i ij by (simp del: replicate.simps) ``` chaieb@29687 ` 1455` ``` ultimately have False using eq n0 by (simp del: replicate.simps)} ``` chaieb@29687 ` 1456` ``` then show "{replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` chaieb@29687 ` 1457` ``` by auto ``` chaieb@29687 ` 1458` ``` qed ``` huffman@30488 ` 1459` ``` from card_UN_disjoint[OF fK fAK d] ``` chaieb@29687 ` 1460` ``` show "card (\i\{0..k}. {replicate (k + 1) 0[i := n]}) = k+1" by simp ``` chaieb@29687 ` 1461` ```qed ``` huffman@30488 ` 1462` huffman@30488 ` 1463` ```lemma power_radical: ``` huffman@31273 ` 1464` ``` fixes a:: "'a::field_char_0 fps" ``` chaieb@31073 ` 1465` ``` assumes a0: "a\$0 \ 0" ``` chaieb@31073 ` 1466` ``` shows "(r (Suc k) (a\$0)) ^ Suc k = a\$0 \ (fps_radical r (Suc k) a) ^ (Suc k) = a" ``` chaieb@31073 ` 1467` ```proof- ``` chaieb@31073 ` 1468` ``` let ?r = "fps_radical r (Suc k) a" ``` chaieb@31073 ` 1469` ``` {assume r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0" ``` chaieb@31073 ` 1470` ``` from a0 r0 have r00: "r (Suc k) (a\$0) \ 0" by auto ``` chaieb@31073 ` 1471` ``` {fix z have "?r ^ Suc k \$ z = a\$z" ``` chaieb@31073 ` 1472` ``` proof(induct z rule: nat_less_induct) ``` chaieb@31073 ` 1473` ``` fix n assume H: "\m 0" using n1 by arith ``` chaieb@31073 ` 1480` ``` let ?Pnk = "natpermute n (k + 1)" ``` chaieb@31073 ` 1481` ``` let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@31073 ` 1482` ``` let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@31073 ` 1483` ``` have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast ``` chaieb@31073 ` 1484` ``` have d: "?Pnkn \ ?Pnknn = {}" by blast ``` chaieb@31073 ` 1485` ``` have f: "finite ?Pnkn" "finite ?Pnknn" ``` chaieb@31073 ` 1486` ``` using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] ``` chaieb@31073 ` 1487` ``` by (metis natpermute_finite)+ ``` chaieb@31073 ` 1488` ``` let ?f = "\v. \j\{0..k}. ?r \$ v ! j" ``` chaieb@31073 ` 1489` ``` have "setsum ?f ?Pnkn = setsum (\v. ?r \$ n * r (Suc k) (a \$ 0) ^ k) ?Pnkn" ``` chaieb@31073 ` 1490` ``` proof(rule setsum_cong2) ``` chaieb@31073 ` 1491` ``` fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" ``` chaieb@31073 ` 1492` ``` let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a \$ v ! j) = fps_radical r (Suc k) a \$ n * r (Suc k) (a \$ 0) ^ k" ``` chaieb@31073 ` 1493` ``` from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" ``` chaieb@31073 ` 1494` ``` unfolding natpermute_contain_maximal by auto ``` chaieb@31073 ` 1495` ``` have "(\j\{0..k}. fps_radical r (Suc k) a \$ v ! j) = (\j\{0..k}. if j = i then fps_radical r (Suc k) a \$ n else r (Suc k) (a\$0))" ``` chaieb@31073 ` 1496` ``` apply (rule setprod_cong, simp) ``` chaieb@31073 ` 1497` ``` using i r0 by (simp del: replicate.simps) ``` chaieb@31073 ` 1498` ``` also have "\ = (fps_radical r (Suc k) a \$ n) * r (Suc k) (a\$0) ^ k" ``` chaieb@31073 ` 1499` ``` unfolding setprod_gen_delta[OF fK] using i r0 by simp ``` chaieb@31073 ` 1500` ``` finally show ?ths . ``` chaieb@31073 ` 1501` ``` qed ``` chaieb@31073 ` 1502` ``` then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r \$ n * r (Suc k) (a \$ 0) ^ k" ``` chaieb@31073 ` 1503` ``` by (simp add: natpermute_max_card[OF nz, simplified]) ``` chaieb@31073 ` 1504` ``` also have "\ = a\$n - setsum ?f ?Pnknn" ``` chaieb@31073 ` 1505` ``` unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) ``` chaieb@31073 ` 1506` ``` finally have fn: "setsum ?f ?Pnkn = a\$n - setsum ?f ?Pnknn" . ``` chaieb@31073 ` 1507` ``` have "(?r ^ Suc k)\$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" ``` chaieb@31073 ` 1508` ``` unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. ``` chaieb@31073 ` 1509` ``` also have "\ = a\$n" unfolding fn by simp ``` chaieb@31073 ` 1510` ``` finally have "?r ^ Suc k \$ n = a \$n" .} ``` chaieb@31073 ` 1511` ``` ultimately show "?r ^ Suc k \$ n = a \$n" by (cases n, auto) ``` chaieb@31073 ` 1512` ``` qed } ``` chaieb@31073 ` 1513` ``` then have ?thesis using r0 by (simp add: fps_eq_iff)} ``` chaieb@31073 ` 1514` ```moreover ``` chaieb@31073 ` 1515` ```{ assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" ``` chaieb@31073 ` 1516` ``` hence "((fps_radical r (Suc k) a) ^ (Suc k))\$0 = a\$0" by simp ``` chaieb@31073 ` 1517` ``` then have "(r (Suc k) (a\$0)) ^ Suc k = a\$0" ``` chaieb@31073 ` 1518` ``` unfolding fps_power_nth_Suc ``` chaieb@31073 ` 1519` ``` by (simp add: setprod_constant del: replicate.simps)} ``` chaieb@31073 ` 1520` ```ultimately show ?thesis by blast ``` chaieb@31073 ` 1521` ```qed ``` chaieb@31073 ` 1522` chaieb@31073 ` 1523` ```(* ``` chaieb@31073 ` 1524` ```lemma power_radical: ``` huffman@31273 ` 1525` ``` fixes a:: "'a::field_char_0 fps" ``` chaieb@29687 ` 1526` ``` assumes r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0" and a0: "a\$0 \ 0" ``` huffman@30488 ` 1527` ``` shows "(fps_radical r (Suc k) a) ^ (Suc k) = a" ``` chaieb@29687 ` 1528` ```proof- ``` chaieb@29687 ` 1529` ``` let ?r = "fps_radical r (Suc k) a" ``` chaieb@29687 ` 1530` ``` from a0 r0 have r00: "r (Suc k) (a\$0) \ 0" by auto ``` chaieb@29687 ` 1531` ``` {fix z have "?r ^ Suc k \$ z = a\$z" ``` chaieb@29687 ` 1532` ``` proof(induct z rule: nat_less_induct) ``` chaieb@29687 ` 1533` ``` fix n assume H: "\m 0" using n1 by arith ``` chaieb@29687 ` 1540` ``` let ?Pnk = "natpermute n (k + 1)" ``` chaieb@29687 ` 1541` ``` let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1542` ``` let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1543` ``` have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast ``` chaieb@29687 ` 1544` ``` have d: "?Pnkn \ ?Pnknn = {}" by blast ``` huffman@30488 ` 1545` ``` have f: "finite ?Pnkn" "finite ?Pnknn" ``` chaieb@29687 ` 1546` ``` using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] ``` chaieb@29687 ` 1547` ``` by (metis natpermute_finite)+ ``` chaieb@29687 ` 1548` ``` let ?f = "\v. \j\{0..k}. ?r \$ v ! j" ``` huffman@30488 ` 1549` ``` have "setsum ?f ?Pnkn = setsum (\v. ?r \$ n * r (Suc k) (a \$ 0) ^ k) ?Pnkn" ``` chaieb@29687 ` 1550` ``` proof(rule setsum_cong2) ``` chaieb@29687 ` 1551` ``` fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" ``` chaieb@29687 ` 1552` ``` let ?ths = "(\j\{0..k}. fps_radical r (Suc k) a \$ v ! j) = fps_radical r (Suc k) a \$ n * r (Suc k) (a \$ 0) ^ k" ``` chaieb@29687 ` 1553` ``` from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" ``` chaieb@29687 ` 1554` ``` unfolding natpermute_contain_maximal by auto ``` chaieb@29687 ` 1555` ``` have "(\j\{0..k}. fps_radical r (Suc k) a \$ v ! j) = (\j\{0..k}. if j = i then fps_radical r (Suc k) a \$ n else r (Suc k) (a\$0))" ``` chaieb@29687 ` 1556` ``` apply (rule setprod_cong, simp) ``` chaieb@29687 ` 1557` ``` using i r0 by (simp del: replicate.simps) ``` chaieb@29687 ` 1558` ``` also have "\ = (fps_radical r (Suc k) a \$ n) * r (Suc k) (a\$0) ^ k" ``` chaieb@29687 ` 1559` ``` unfolding setprod_gen_delta[OF fK] using i r0 by simp ``` chaieb@29687 ` 1560` ``` finally show ?ths . ``` chaieb@29687 ` 1561` ``` qed ``` huffman@30488 ` 1562` ``` then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r \$ n * r (Suc k) (a \$ 0) ^ k" ``` huffman@30488 ` 1563` ``` by (simp add: natpermute_max_card[OF nz, simplified]) ``` chaieb@29687 ` 1564` ``` also have "\ = a\$n - setsum ?f ?Pnknn" ``` chaieb@29687 ` 1565` ``` unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) ``` chaieb@29687 ` 1566` ``` finally have fn: "setsum ?f ?Pnkn = a\$n - setsum ?f ?Pnknn" . ``` huffman@30488 ` 1567` ``` have "(?r ^ Suc k)\$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" ``` chaieb@29687 ` 1568` ``` unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. ``` chaieb@29687 ` 1569` ``` also have "\ = a\$n" unfolding fn by simp ``` chaieb@29687 ` 1570` ``` finally have "?r ^ Suc k \$ n = a \$n" .} ``` chaieb@29687 ` 1571` ``` ultimately show "?r ^ Suc k \$ n = a \$n" by (cases n, auto) ``` chaieb@29687 ` 1572` ``` qed } ``` chaieb@29687 ` 1573` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1574` ```qed ``` chaieb@29687 ` 1575` chaieb@31073 ` 1576` ```*) ``` chaieb@29687 ` 1577` ```lemma eq_divide_imp': assumes c0: "(c::'a::field) ~= 0" and eq: "a * c = b" ``` huffman@30488 ` 1578` ``` shows "a = b / c" ``` chaieb@29687 ` 1579` ```proof- ``` chaieb@29687 ` 1580` ``` from eq have "a * c * inverse c = b * inverse c" by simp ``` chaieb@29687 ` 1581` ``` hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse) ``` chaieb@29687 ` 1582` ``` then show "a = b/c" unfolding field_inverse[OF c0] by simp ``` chaieb@29687 ` 1583` ```qed ``` chaieb@29687 ` 1584` huffman@30488 ` 1585` ```lemma radical_unique: ``` huffman@30488 ` 1586` ``` assumes r0: "(r (Suc k) (b\$0)) ^ Suc k = b\$0" ``` huffman@31273 ` 1587` ``` and a0: "r (Suc k) (b\$0 ::'a::field_char_0) = a\$0" and b0: "b\$0 \ 0" ``` chaieb@29687 ` 1588` ``` shows "a^(Suc k) = b \ a = fps_radical r (Suc k) b" ``` chaieb@29687 ` 1589` ```proof- ``` chaieb@29687 ` 1590` ``` let ?r = "fps_radical r (Suc k) b" ``` chaieb@29687 ` 1591` ``` have r00: "r (Suc k) (b\$0) \ 0" using b0 r0 by auto ``` chaieb@29687 ` 1592` ``` {assume H: "a = ?r" ``` chaieb@31073 ` 1593` ``` from H have "a^Suc k = b" using power_radical[OF b0, of r k, unfolded r0] by simp} ``` chaieb@29687 ` 1594` ``` moreover ``` chaieb@29687 ` 1595` ``` {assume H: "a^Suc k = b" ``` chaieb@29687 ` 1596` ``` have ceq: "card {0..k} = Suc k" by simp ``` chaieb@29687 ` 1597` ``` have fk: "finite {0..k}" by simp ``` chaieb@29687 ` 1598` ``` from a0 have a0r0: "a\$0 = ?r\$0" by simp ``` chaieb@29687 ` 1599` ``` {fix n have "a \$ n = ?r \$ n" ``` chaieb@29687 ` 1600` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1601` ``` fix n assume h: "\m 0" using n1 by arith ``` chaieb@29687 ` 1607` ``` let ?Pnk = "natpermute n (Suc k)" ``` chaieb@29687 ` 1608` ``` let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1609` ``` let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1610` ``` have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast ``` chaieb@29687 ` 1611` ``` have d: "?Pnkn \ ?Pnknn = {}" by blast ``` huffman@30488 ` 1612` ``` have f: "finite ?Pnkn" "finite ?Pnknn" ``` chaieb@29687 ` 1613` ``` using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] ``` chaieb@29687 ` 1614` ``` by (metis natpermute_finite)+ ``` chaieb@29687 ` 1615` ``` let ?f = "\v. \j\{0..k}. ?r \$ v ! j" ``` chaieb@29687 ` 1616` ``` let ?g = "\v. \j\{0..k}. a \$ v ! j" ``` huffman@30488 ` 1617` ``` have "setsum ?g ?Pnkn = setsum (\v. a \$ n * (?r\$0)^k) ?Pnkn" ``` chaieb@29687 ` 1618` ``` proof(rule setsum_cong2) ``` chaieb@29687 ` 1619` ``` fix v assume v: "v \ {xs \ natpermute n (Suc k). n \ set xs}" ``` chaieb@29687 ` 1620` ``` let ?ths = "(\j\{0..k}. a \$ v ! j) = a \$ n * (?r\$0)^k" ``` chaieb@29687 ` 1621` ``` from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" ``` chaieb@29687 ` 1622` ``` unfolding Suc_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps) ``` chaieb@29687 ` 1623` ``` have "(\j\{0..k}. a \$ v ! j) = (\j\{0..k}. if j = i then a \$ n else r (Suc k) (b\$0))" ``` chaieb@29687 ` 1624` ``` apply (rule setprod_cong, simp) ``` chaieb@29687 ` 1625` ``` using i a0 by (simp del: replicate.simps) ``` chaieb@29687 ` 1626` ``` also have "\ = a \$ n * (?r \$ 0)^k" ``` chaieb@29687 ` 1627` ``` unfolding setprod_gen_delta[OF fK] using i by simp ``` chaieb@29687 ` 1628` ``` finally show ?ths . ``` chaieb@29687 ` 1629` ``` qed ``` huffman@30488 ` 1630` ``` then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a \$ n * (?r \$ 0)^k" ``` chaieb@29687 ` 1631` ``` by (simp add: natpermute_max_card[OF nz, simplified]) ``` chaieb@29687 ` 1632` ``` have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn" ``` chaieb@29687 ` 1633` ``` proof (rule setsum_cong2, rule setprod_cong, simp) ``` chaieb@29687 ` 1634` ``` fix xs i assume xs: "xs \ ?Pnknn" and i: "i \ {0..k}" ``` chaieb@29687 ` 1635` ``` {assume c: "n \ xs ! i" ``` chaieb@29687 ` 1636` ``` from xs i have "xs !i \ n" by (auto simp add: in_set_conv_nth natpermute_def) ``` chaieb@29687 ` 1637` ``` with c have c': "n < xs!i" by arith ``` chaieb@29687 ` 1638` ``` have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1.. ({i} \ {i+1 ..< Suc k}) = {}" "{i} \ {i+1..< Suc k} = {}" by auto ``` chaieb@29687 ` 1640` ``` have eqs: "{0.. ({i} \ {i+1 ..< Suc k})" using i by auto ``` chaieb@29687 ` 1641` ``` from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def) ``` chaieb@29687 ` 1642` ``` also have "\ = setsum (nth xs) {0.. = xs!i + setsum (nth xs) {0..(x::'a). of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" ``` chaieb@29687 ` 1654` ``` by (simp add: field_simps del: of_nat_Suc) ``` chaieb@29687 ` 1655` ``` from H have "b\$n = a^Suc k \$ n" by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1656` ``` also have "a ^ Suc k\$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" ``` huffman@30488 ` 1657` ``` unfolding fps_power_nth_Suc ``` huffman@30488 ` 1658` ``` using setsum_Un_disjoint[OF f d, unfolded Suc_plus1[symmetric], ``` chaieb@29687 ` 1659` ``` unfolded eq, of ?g] by simp ``` chaieb@29687 ` 1660` ``` also have "\ = of_nat (k+1) * a \$ n * (?r \$ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 .. ``` chaieb@29687 ` 1661` ``` finally have "of_nat (k+1) * a \$ n * (?r \$ 0)^k = b\$n - setsum ?f ?Pnknn" by simp ``` chaieb@29687 ` 1662` ``` then have "a\$n = (b\$n - setsum ?f ?Pnknn) / (of_nat (k+1) * (?r \$ 0)^k)" ``` huffman@30488 ` 1663` ``` apply - ``` chaieb@29687 ` 1664` ``` apply (rule eq_divide_imp') ``` chaieb@29687 ` 1665` ``` using r00 ``` chaieb@29687 ` 1666` ``` apply (simp del: of_nat_Suc) ``` chaieb@29687 ` 1667` ``` by (simp add: mult_ac) ``` chaieb@29687 ` 1668` ``` then have "a\$n = ?r \$n" ``` chaieb@29687 ` 1669` ``` apply (simp del: of_nat_Suc) ``` chaieb@29687 ` 1670` ``` unfolding fps_radical_def n1 ``` huffman@29911 ` 1671` ``` by (simp add: field_simps n1 th00 del: of_nat_Suc)} ``` chaieb@29687 ` 1672` ``` ultimately show "a\$n = ?r \$ n" by (cases n, auto) ``` chaieb@29687 ` 1673` ``` qed} ``` chaieb@29687 ` 1674` ``` then have "a = ?r" by (simp add: fps_eq_iff)} ``` chaieb@29687 ` 1675` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1676` ```qed ``` chaieb@29687 ` 1677` chaieb@29687 ` 1678` huffman@30488 ` 1679` ```lemma radical_power: ``` huffman@30488 ` 1680` ``` assumes r0: "r (Suc k) ((a\$0) ^ Suc k) = a\$0" ``` huffman@31273 ` 1681` ``` and a0: "(a\$0 ::'a::field_char_0) \ 0" ``` chaieb@29687 ` 1682` ``` shows "(fps_radical r (Suc k) (a ^ Suc k)) = a" ``` chaieb@29687 ` 1683` ```proof- ``` chaieb@29687 ` 1684` ``` let ?ak = "a^ Suc k" ``` huffman@30273 ` 1685` ``` have ak0: "?ak \$ 0 = (a\$0) ^ Suc k" by (simp add: fps_nth_power_0 del: power_Suc) ``` chaieb@29687 ` 1686` ``` from r0 have th0: "r (Suc k) (a ^ Suc k \$ 0) ^ Suc k = a ^ Suc k \$ 0" using ak0 by auto ``` chaieb@29687 ` 1687` ``` from r0 ak0 have th1: "r (Suc k) (a ^ Suc k \$ 0) = a \$ 0" by auto ``` chaieb@29687 ` 1688` ``` from ak0 a0 have ak00: "?ak \$ 0 \0 " by auto ``` chaieb@29687 ` 1689` ``` from radical_unique[of r k ?ak a, OF th0 th1 ak00] show ?thesis by metis ``` chaieb@29687 ` 1690` ```qed ``` chaieb@29687 ` 1691` huffman@30488 ` 1692` ```lemma fps_deriv_radical: ``` huffman@31273 ` 1693` ``` fixes a:: "'a::field_char_0 fps" ``` chaieb@29687 ` 1694` ``` assumes r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0" and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1695` ``` shows "fps_deriv (fps_radical r (Suc k) a) = fps_deriv a / (fps_const (of_nat (Suc k)) * (fps_radical r (Suc k) a) ^ k)" ``` chaieb@29687 ` 1696` ```proof- ``` chaieb@29687 ` 1697` ``` let ?r= "fps_radical r (Suc k) a" ``` chaieb@29687 ` 1698` ``` let ?w = "(fps_const (of_nat (Suc k)) * ?r ^ k)" ``` chaieb@29687 ` 1699` ``` from a0 r0 have r0': "r (Suc k) (a\$0) \ 0" by auto ``` chaieb@29687 ` 1700` ``` from r0' have w0: "?w \$ 0 \ 0" by (simp del: of_nat_Suc) ``` chaieb@29687 ` 1701` ``` note th0 = inverse_mult_eq_1[OF w0] ``` chaieb@29687 ` 1702` ``` let ?iw = "inverse ?w" ``` chaieb@31073 ` 1703` ``` from iffD1[OF power_radical[of a r], OF a0 r0] ``` chaieb@29687 ` 1704` ``` have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp ``` chaieb@29687 ` 1705` ``` hence "fps_deriv ?r * ?w = fps_deriv a" ``` huffman@30273 ` 1706` ``` by (simp add: fps_deriv_power mult_ac del: power_Suc) ``` chaieb@29687 ` 1707` ``` hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a" by simp ``` chaieb@29687 ` 1708` ``` hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w" ``` chaieb@29687 ` 1709` ``` by (simp add: fps_divide_def) ``` huffman@30488 ` 1710` ``` then show ?thesis unfolding th0 by simp ``` chaieb@29687 ` 1711` ```qed ``` chaieb@29687 ` 1712` huffman@30488 ` 1713` ```lemma radical_mult_distrib: ``` huffman@31273 ` 1714` ``` fixes a:: "'a::field_char_0 fps" ``` huffman@30488 ` 1715` ``` assumes ``` chaieb@31073 ` 1716` ``` k: "k > 0" ``` chaieb@31073 ` 1717` ``` and ra0: "r k (a \$ 0) ^ k = a \$ 0" ``` chaieb@31073 ` 1718` ``` and rb0: "r k (b \$ 0) ^ k = b \$ 0" ``` chaieb@31073 ` 1719` ``` and a0: "a\$0 \ 0" ``` chaieb@31073 ` 1720` ``` and b0: "b\$0 \ 0" ``` chaieb@31073 ` 1721` ``` shows "r k ((a * b) \$ 0) = r k (a \$ 0) * r k (b \$ 0) \ fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" ``` chaieb@31073 ` 1722` ```proof- ``` chaieb@31073 ` 1723` ``` {assume r0': "r k ((a * b) \$ 0) = r k (a \$ 0) * r k (b \$ 0)" ``` chaieb@31073 ` 1724` ``` from r0' have r0: "(r (k) ((a*b)\$0)) ^ k = (a*b)\$0" ``` chaieb@31073 ` 1725` ``` by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) ``` chaieb@31073 ` 1726` ``` {assume "k=0" hence ?thesis using r0' by simp} ``` chaieb@31073 ` 1727` ``` moreover ``` chaieb@31073 ` 1728` ``` {fix h assume k: "k = Suc h" ``` chaieb@31073 ` 1729` ``` let ?ra = "fps_radical r (Suc h) a" ``` chaieb@31073 ` 1730` ``` let ?rb = "fps_radical r (Suc h) b" ``` chaieb@31073 ` 1731` ``` have th0: "r (Suc h) ((a * b) \$ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) \$ 0" ``` chaieb@31073 ` 1732` ``` using r0' k by (simp add: fps_mult_nth) ``` chaieb@31073 ` 1733` ``` have ab0: "(a*b) \$ 0 \ 0" using a0 b0 by (simp add: fps_mult_nth) ``` chaieb@31073 ` 1734` ``` from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric] ``` chaieb@31073 ` 1735` ``` iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded k]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded k]] k r0' ``` chaieb@31073 ` 1736` ``` have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)} ``` chaieb@31073 ` 1737` ```ultimately have ?thesis by (cases k, auto)} ``` chaieb@31073 ` 1738` ```moreover ``` chaieb@31073 ` 1739` ```{assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b" ``` chaieb@31073 ` 1740` ``` hence "(fps_radical r k (a*b))\$0 = (fps_radical r k a * fps_radical r k b)\$0" by simp ``` chaieb@31073 ` 1741` ``` then have "r k ((a * b) \$ 0) = r k (a \$ 0) * r k (b \$ 0)" ``` chaieb@31073 ` 1742` ``` using k by (simp add: fps_mult_nth)} ``` chaieb@31073 ` 1743` ```ultimately show ?thesis by blast ``` chaieb@31073 ` 1744` ```qed ``` chaieb@31073 ` 1745` chaieb@31073 ` 1746` ```(* ``` chaieb@31073 ` 1747` ```lemma radical_mult_distrib: ``` huffman@31273 ` 1748` ``` fixes a:: "'a::field_char_0 fps" ``` chaieb@31073 ` 1749` ``` assumes ``` chaieb@31073 ` 1750` ``` ra0: "r k (a \$ 0) ^ k = a \$ 0" ``` chaieb@31073 ` 1751` ``` and rb0: "r k (b \$ 0) ^ k = b \$ 0" ``` chaieb@31073 ` 1752` ``` and r0': "r k ((a * b) \$ 0) = r k (a \$ 0) * r k (b \$ 0)" ``` chaieb@29687 ` 1753` ``` and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1754` ``` and b0: "b\$0 \ 0" ``` chaieb@29687 ` 1755` ``` shows "fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" ``` chaieb@29687 ` 1756` ```proof- ``` chaieb@29687 ` 1757` ``` from r0' have r0: "(r (k) ((a*b)\$0)) ^ k = (a*b)\$0" ``` chaieb@29687 ` 1758` ``` by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) ``` chaieb@29687 ` 1759` ``` {assume "k=0" hence ?thesis by simp} ``` chaieb@29687 ` 1760` ``` moreover ``` chaieb@29687 ` 1761` ``` {fix h assume k: "k = Suc h" ``` chaieb@29687 ` 1762` ``` let ?ra = "fps_radical r (Suc h) a" ``` chaieb@29687 ` 1763` ``` let ?rb = "fps_radical r (Suc h) b" ``` huffman@30488 ` 1764` ``` have th0: "r (Suc h) ((a * b) \$ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) \$ 0" ``` chaieb@29687 ` 1765` ``` using r0' k by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1766` ``` have ab0: "(a*b) \$ 0 \ 0" using a0 b0 by (simp add: fps_mult_nth) ``` huffman@30488 ` 1767` ``` from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric] ``` chaieb@29687 ` 1768` ``` power_radical[of r, OF ra0[unfolded k] a0] power_radical[of r, OF rb0[unfolded k] b0] k ``` huffman@30273 ` 1769` ``` have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)} ``` chaieb@29687 ` 1770` ```ultimately show ?thesis by (cases k, auto) ``` chaieb@29687 ` 1771` ```qed ``` chaieb@31073 ` 1772` ```*) ``` chaieb@29687 ` 1773` chaieb@31073 ` 1774` ```lemma fps_divide_1[simp]: "(a:: ('a::field) fps) / 1 = a" ``` chaieb@29687 ` 1775` ``` by (simp add: fps_divide_def) ``` chaieb@29687 ` 1776` chaieb@29687 ` 1777` ```lemma radical_divide: ``` huffman@31273 ` 1778` ``` fixes a :: "'a::field_char_0 fps" ``` huffman@30488 ` 1779` ``` assumes ``` chaieb@31073 ` 1780` ``` kp: "k>0" ``` chaieb@31073 ` 1781` ``` and ra0: "(r k (a \$ 0)) ^ k = a \$ 0" ``` chaieb@31073 ` 1782` ``` and rb0: "(r k (b \$ 0)) ^ k = b \$ 0" ``` huffman@30488 ` 1783` ``` and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1784` ``` and b0: "b\$0 \ 0" ``` chaieb@31073 ` 1785` ``` shows "r k ((a \$ 0) / (b\$0)) = r k (a\$0) / r k (b \$ 0) \ fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" (is "?lhs = ?rhs") ``` chaieb@29687 ` 1786` ```proof- ``` chaieb@31073 ` 1787` ``` let ?r = "fps_radical r k" ``` chaieb@31073 ` 1788` ``` from kp obtain h where k: "k = Suc h" by (cases k, auto) ``` chaieb@31073 ` 1789` ``` have ra0': "r k (a\$0) \ 0" using a0 ra0 k by auto ``` chaieb@31073 ` 1790` ``` have rb0': "r k (b\$0) \ 0" using b0 rb0 k by auto ``` huffman@30488 ` 1791` chaieb@31073 ` 1792` ``` {assume ?rhs ``` chaieb@31073 ` 1793` ``` then have "?r (a/b) \$ 0 = (?r a / ?r b)\$0" by simp ``` chaieb@31073 ` 1794` ``` then have ?lhs using k a0 b0 rb0' ``` chaieb@31073 ` 1795` ``` by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) } ``` chaieb@31073 ` 1796` ``` moreover ``` chaieb@31073 ` 1797` ``` {assume h: ?lhs ``` chaieb@31073 ` 1798` ``` from a0 b0 have ab0[simp]: "(a/b)\$0 = a\$0 / b\$0" ``` chaieb@31073 ` 1799` ``` by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def) ``` chaieb@31073 ` 1800` ``` have th0: "r k ((a/b)\$0) ^ k = (a/b)\$0" ``` chaieb@31073 ` 1801` ``` by (simp add: h nonzero_power_divide[OF rb0'] ra0 rb0 del: k) ``` chaieb@31073 ` 1802` ``` from a0 b0 ra0' rb0' kp h ``` chaieb@31073 ` 1803` ``` have th1: "r k ((a / b) \$ 0) = (fps_radical r k a / fps_radical r k b) \$ 0" ``` chaieb@31073 ` 1804` ``` by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse del: k) ``` chaieb@31073 ` 1805` ``` from a0 b0 ra0' rb0' kp have ab0': "(a / b) \$ 0 \ 0" ``` chaieb@31073 ` 1806` ``` by (simp add: fps_divide_def fps_mult_nth fps_inverse_def nonzero_imp_inverse_nonzero) ``` chaieb@31073 ` 1807` ``` note tha[simp] = iffD1[OF power_radical[where r=r and k=h], OF a0 ra0[unfolded k], unfolded k[symmetric]] ``` chaieb@31073 ` 1808` ``` note thb[simp] = iffD1[OF power_radical[where r=r and k=h], OF b0 rb0[unfolded k], unfolded k[symmetric]] ``` chaieb@31073 ` 1809` ``` have th2: "(?r a / ?r b)^k = a/b" ``` chaieb@31073 ` 1810` ``` by (simp add: fps_divide_def power_mult_distrib fps_inverse_power[symmetric]) ``` chaieb@31073 ` 1811` ``` from iffD1[OF radical_unique[where r=r and a="?r a / ?r b" and b="a/b" and k=h], symmetric, unfolded k[symmetric], OF th0 th1 ab0' th2] have ?rhs .} ``` chaieb@31073 ` 1812` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1813` ```qed ``` chaieb@29687 ` 1814` chaieb@31073 ` 1815` ```lemma radical_inverse: ``` huffman@31273 ` 1816` ``` fixes a :: "'a::field_char_0 fps" ``` chaieb@31073 ` 1817` ``` assumes ``` chaieb@31073 ` 1818` ``` k: "k>0" ``` chaieb@31073 ` 1819` ``` and ra0: "r k (a \$ 0) ^ k = a \$ 0" ``` chaieb@31073 ` 1820` ``` and r1: "(r k 1)^k = 1" ``` chaieb@31073 ` 1821` ``` and a0: "a\$0 \ 0" ``` chaieb@31073 ` 1822` ``` shows "r k (inverse (a \$ 0)) = r k 1 / (r k (a \$ 0)) \ fps_radical r k (inverse a) = fps_radical r k 1 / fps_radical r k a" ``` chaieb@31073 ` 1823` ``` using radical_divide[where k=k and r=r and a=1 and b=a, OF k ] ra0 r1 a0 ``` chaieb@31073 ` 1824` ``` by (simp add: divide_inverse fps_divide_def) ``` chaieb@31073 ` 1825` huffman@29906 ` 1826` ```subsection{* Derivative of composition *} ``` chaieb@29687 ` 1827` huffman@30488 ` 1828` ```lemma fps_compose_deriv: ``` chaieb@29687 ` 1829` ``` fixes a:: "('a::idom) fps" ``` chaieb@29687 ` 1830` ``` assumes b0: "b\$0 = 0" ``` chaieb@29687 ` 1831` ``` shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * (fps_deriv b)" ``` chaieb@29687 ` 1832` ```proof- ``` chaieb@29687 ` 1833` ``` {fix n ``` chaieb@29687 ` 1834` ``` have "(fps_deriv (a oo b))\$n = setsum (\i. a \$ i * (fps_deriv (b^i))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1835` ``` by (simp add: fps_compose_def ring_simps setsum_right_distrib del: of_nat_Suc) ``` chaieb@29687 ` 1836` ``` also have "\ = setsum (\i. a\$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1837` ``` by (simp add: ring_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) ``` chaieb@29687 ` 1838` ``` also have "\ = setsum (\i. of_nat i * a\$i * (((b^(i - 1)) * fps_deriv b))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1839` ``` unfolding fps_mult_left_const_nth by (simp add: ring_simps) ``` chaieb@29687 ` 1840` ``` also have "\ = setsum (\i. of_nat i * a\$i * (setsum (\j. (b^ (i - 1))\$j * (fps_deriv b)\$(n - j)) {0..n})) {0.. Suc n}" ``` chaieb@29687 ` 1841` ``` unfolding fps_mult_nth .. ``` chaieb@29687 ` 1842` ``` also have "\ = setsum (\i. of_nat i * a\$i * (setsum (\j. (b^ (i - 1))\$j * (fps_deriv b)\$(n - j)) {0..n})) {1.. Suc n}" ``` chaieb@29687 ` 1843` ``` apply (rule setsum_mono_zero_right) ``` huffman@29913 ` 1844` ``` apply (auto simp add: mult_delta_left setsum_delta not_le) ``` huffman@29913 ` 1845` ``` done ``` chaieb@29687 ` 1846` ``` also have "\ = setsum (\i. of_nat (i + 1) * a\$(i+1) * (setsum (\j. (b^ i)\$j * of_nat (n - j + 1) * b\$(n - j + 1)) {0..n})) {0.. n}" ``` chaieb@29687 ` 1847` ``` unfolding fps_deriv_nth ``` chaieb@29687 ` 1848` ``` apply (rule setsum_reindex_cong[where f="Suc"]) ``` chaieb@29687 ` 1849` ``` by (auto simp add: mult_assoc) ``` chaieb@29687 ` 1850` ``` finally have th0: "(fps_deriv (a oo b))\$n = setsum (\i. of_nat (i + 1) * a\$(i+1) * (setsum (\j. (b^ i)\$j * of_nat (n - j + 1) * b\$(n - j + 1)) {0..n})) {0.. n}" . ``` huffman@30488 ` 1851` chaieb@29687 ` 1852` ``` have "(((fps_deriv a) oo b) * (fps_deriv b))\$n = setsum (\i. (fps_deriv b)\$ (n - i) * ((fps_deriv a) oo b)\$i) {0..n}" ``` chaieb@29687 ` 1853` ``` unfolding fps_mult_nth by (simp add: mult_ac) ``` chaieb@29687 ` 1854` ``` also have "\ = setsum (\i. setsum (\j. of_nat (n - i +1) * b\$(n - i + 1) * of_nat (j + 1) * a\$(j+1) * (b^j)\$i) {0..n}) {0..n}" ``` chaieb@29687 ` 1855` ``` unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult_assoc ``` chaieb@29687 ` 1856` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1857` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 1858` ``` apply (simp_all add: subset_eq) ``` chaieb@29687 ` 1859` ``` apply clarify ``` chaieb@29687 ` 1860` ``` apply (subgoal_tac "b^i\$x = 0") ``` chaieb@29687 ` 1861` ``` apply simp ``` chaieb@29687 ` 1862` ``` apply (rule startsby_zero_power_prefix[OF b0, rule_format]) ``` chaieb@29687 ` 1863` ``` by simp ``` chaieb@29687 ` 1864` ``` also have "\ = setsum (\i. of_nat (i + 1) * a\$(i+1) * (setsum (\j. (b^ i)\$j * of_nat (n - j + 1) * b\$(n - j + 1)) {0..n})) {0.. n}" ``` chaieb@29687 ` 1865` ``` unfolding setsum_right_distrib ``` chaieb@29687 ` 1866` ``` apply (subst setsum_commute) ``` chaieb@29687 ` 1867` ``` by ((rule setsum_cong2)+) simp ``` chaieb@29687 ` 1868` ``` finally have "(fps_deriv (a oo b))\$n = (((fps_deriv a) oo b) * (fps_deriv b)) \$n" ``` chaieb@29687 ` 1869` ``` unfolding th0 by simp} ``` chaieb@29687 ` 1870` ```then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1871` ```qed ``` chaieb@29687 ` 1872` chaieb@29687 ` 1873` ```lemma fps_mult_X_plus_1_nth: ``` chaieb@29687 ` 1874` ``` "((1+X)*a) \$n = (if n = 0 then (a\$n :: 'a::comm_ring_1) else a\$n + a\$(n - 1))" ``` chaieb@29687 ` 1875` ```proof- ``` chaieb@29687 ` 1876` ``` {assume "n = 0" hence ?thesis by (simp add: fps_mult_nth )} ``` chaieb@29687 ` 1877` ``` moreover ``` chaieb@29687 ` 1878` ``` {fix m assume m: "n = Suc m" ``` chaieb@29687 ` 1879` ``` have "((1+X)*a) \$n = setsum (\i. (1+X)\$i * a\$(n-i)) {0..n}" ``` chaieb@29687 ` 1880` ``` by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1881` ``` also have "\ = setsum (\i. (1+X)\$i * a\$(n-i)) {0.. 1}" ``` chaieb@29687 ` 1882` ``` unfolding m ``` chaieb@29687 ` 1883` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 1884` ``` by (auto simp add: ) ``` chaieb@29687 ` 1885` ``` also have "\ = (if n = 0 then (a\$n :: 'a::comm_ring_1) else a\$n + a\$(n - 1))" ``` chaieb@29687 ` 1886` ``` unfolding m ``` chaieb@29687 ` 1887` ``` by (simp add: ) ``` chaieb@29687 ` 1888` ``` finally have ?thesis .} ``` chaieb@29687 ` 1889` ``` ultimately show ?thesis by (cases n, auto) ``` chaieb@29687 ` 1890` ```qed ``` chaieb@29687 ` 1891` huffman@29906 ` 1892` ```subsection{* Finite FPS (i.e. polynomials) and X *} ``` chaieb@29687 ` 1893` ```lemma fps_poly_sum_X: ``` huffman@30488 ` 1894` ``` assumes z: "\i > n. a\$i = (0::'a::comm_ring_1)" ``` chaieb@29687 ` 1895` ``` shows "a = setsum (\i. fps_const (a\$i) * X^i) {0..n}" (is "a = ?r") ``` chaieb@29687 ` 1896` ```proof- ``` chaieb@29687 ` 1897` ``` {fix i ``` huffman@30488 ` 1898` ``` have "a\$i = ?r\$i" ``` chaieb@29687 ` 1899` ``` unfolding fps_setsum_nth fps_mult_left_const_nth X_power_nth ``` huffman@29913 ` 1900` ``` by (simp add: mult_delta_right setsum_delta' z) ``` huffman@29913 ` 1901` ``` } ``` chaieb@29687 ` 1902` ``` then show ?thesis unfolding fps_eq_iff by blast ``` chaieb@29687 ` 1903` ```qed ``` chaieb@29687 ` 1904` huffman@29906 ` 1905` ```subsection{* Compositional inverses *} ``` chaieb@29687 ` 1906` chaieb@29687 ` 1907` haftmann@31021 ` 1908` ```fun compinv :: "'a fps \ nat \ 'a::{field}" where ``` chaieb@29687 ` 1909` ``` "compinv a 0 = X\$0" ``` chaieb@29687 ` 1910` ```| "compinv a (Suc n) = (X\$ Suc n - setsum (\i. (compinv a i) * (a^i)\$Suc n) {0 .. n}) / (a\$1) ^ Suc n" ``` chaieb@29687 ` 1911` chaieb@29687 ` 1912` ```definition "fps_inv a = Abs_fps (compinv a)" ``` chaieb@29687 ` 1913` chaieb@29687 ` 1914` ```lemma fps_inv: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1915` ``` shows "fps_inv a oo a = X" ``` chaieb@29687 ` 1916` ```proof- ``` chaieb@29687 ` 1917` ``` let ?i = "fps_inv a oo a" ``` chaieb@29687 ` 1918` ``` {fix n ``` huffman@30488 ` 1919` ``` have "?i \$n = X\$n" ``` chaieb@29687 ` 1920` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1921` ``` fix n assume h: "\mi. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + fps_inv a \$ Suc n1 * (a \$ 1)^ Suc n1" ``` huffman@30273 ` 1927` ``` by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0] ``` huffman@30273 ` 1928` ``` del: power_Suc) ``` chaieb@29687 ` 1929` ``` also have "\ = setsum (\i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1} + (X\$ Suc n1 - setsum (\i. (fps_inv a \$ i) * (a^i)\$n) {0 .. n1})" ``` huffman@29911 ` 1930` ``` using a0 a1 n1 by (simp add: fps_inv_def) ``` huffman@30488 ` 1931` ``` also have "\ = X\$n" using n1 by simp ``` chaieb@29687 ` 1932` ``` finally have "?i \$ n = X\$n" .} ``` chaieb@29687 ` 1933` ``` ultimately show "?i \$ n = X\$n" by (cases n, auto) ``` chaieb@29687 ` 1934` ``` qed} ``` chaieb@29687 ` 1935` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1936` ```qed ``` chaieb@29687 ` 1937` chaieb@29687 ` 1938` haftmann@31021 ` 1939` ```fun gcompinv :: "'a fps \ 'a fps \ nat \ 'a::{field}" where ``` chaieb@29687 ` 1940` ``` "gcompinv b a 0 = b\$0" ``` chaieb@29687 ` 1941` ```| "gcompinv b a (Suc n) = (b\$ Suc n - setsum (\i. (gcompinv b a i) * (a^i)\$Suc n) {0 .. n}) / (a\$1) ^ Suc n" ``` chaieb@29687 ` 1942` chaieb@29687 ` 1943` ```definition "fps_ginv b a = Abs_fps (gcompinv b a)" ``` chaieb@29687 ` 1944` chaieb@29687 ` 1945` ```lemma fps_ginv: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1946` ``` shows "fps_ginv b a oo a = b" ``` chaieb@29687 ` 1947` ```proof- ``` chaieb@29687 ` 1948` ``` let ?i = "fps_ginv b a oo a" ``` chaieb@29687 ` 1949` ``` {fix n ``` huffman@30488 ` 1950` ``` have "?i \$n = b\$n" ``` chaieb@29687 ` 1951` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1952` ``` fix n assume h: "\mi. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + fps_ginv b a \$ Suc n1 * (a \$ 1)^ Suc n1" ``` huffman@30273 ` 1958` ``` by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0] ``` huffman@30273 ` 1959` ``` del: power_Suc) ``` chaieb@29687 ` 1960` ``` also have "\ = setsum (\i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1} + (b\$ Suc n1 - setsum (\i. (fps_ginv b a \$ i) * (a^i)\$n) {0 .. n1})" ``` huffman@29911 ` 1961` ``` using a0 a1 n1 by (simp add: fps_ginv_def) ``` huffman@30488 ` 1962` ``` also have "\ = b\$n" using n1 by simp ``` chaieb@29687 ` 1963` ``` finally have "?i \$ n = b\$n" .} ``` chaieb@29687 ` 1964` ``` ultimately show "?i \$ n = b\$n" by (cases n, auto) ``` chaieb@29687 ` 1965` ``` qed} ``` chaieb@29687 ` 1966` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1967` ```qed ``` chaieb@29687 ` 1968` chaieb@29687 ` 1969` ```lemma fps_inv_ginv: "fps_inv = fps_ginv X" ``` chaieb@29687 ` 1970` ``` apply (auto simp add: expand_fun_eq fps_eq_iff fps_inv_def fps_ginv_def) ``` chaieb@29687 ` 1971` ``` apply (induct_tac n rule: nat_less_induct, auto) ``` chaieb@29687 ` 1972` ``` apply (case_tac na) ``` chaieb@29687 ` 1973` ``` apply simp ``` chaieb@29687 ` 1974` ``` apply simp ``` chaieb@29687 ` 1975` ``` done ``` chaieb@29687 ` 1976` chaieb@29687 ` 1977` ```lemma fps_compose_1[simp]: "1 oo a = 1" ``` haftmann@30960 ` 1978` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 1979` chaieb@29687 ` 1980` ```lemma fps_compose_0[simp]: "0 oo a = 0" ``` huffman@29913 ` 1981` ``` by (simp add: fps_eq_iff fps_compose_nth) ``` chaieb@29687 ` 1982` chaieb@29687 ` 1983` ```lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a\$0)" ``` haftmann@30960 ` 1984` ``` by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0') ``` chaieb@29687 ` 1985` chaieb@29687 ` 1986` ```lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)" ``` haftmann@30960 ` 1987` ``` by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf) ``` chaieb@29687 ` 1988` chaieb@29687 ` 1989` ```lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\i. f i oo a) S" ``` chaieb@29687 ` 1990` ```proof- ``` chaieb@29687 ` 1991` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 1992` ``` moreover ``` chaieb@29687 ` 1993` ``` {assume fS: "finite S" ``` chaieb@29687 ` 1994` ``` have ?thesis ``` chaieb@29687 ` 1995` ``` proof(rule finite_induct[OF fS]) ``` chaieb@29687 ` 1996` ``` show "setsum f {} oo a = (\i\{}. f i oo a)" by simp ``` chaieb@29687 ` 1997` ``` next ``` chaieb@29687 ` 1998` ``` fix x F assume fF: "finite F" and xF: "x \ F" and h: "setsum f F oo a = setsum (\i. f i oo a) F" ``` chaieb@29687 ` 1999` ``` show "setsum f (insert x F) oo a = setsum (\i. f i oo a) (insert x F)" ``` chaieb@29687 ` 2000` ``` using fF xF h by (simp add: fps_compose_add_distrib) ``` chaieb@29687 ` 2001` ``` qed} ``` huffman@30488 ` 2002` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 2003` ```qed ``` chaieb@29687 ` 2004` huffman@30488 ` 2005` ```lemma convolution_eq: ``` chaieb@29687 ` 2006` ``` "setsum (%i. a (i :: nat) * b (n - i)) {0 .. n} = setsum (%(i,j). a i * b j) {(i,j). i <= n \ j \ n \ i + j = n}" ``` chaieb@29687 ` 2007` ``` apply (rule setsum_reindex_cong[where f=fst]) ``` chaieb@29687 ` 2008` ``` apply (clarsimp simp add: inj_on_def) ``` chaieb@29687 ` 2009` ``` apply (auto simp add: expand_set_eq image_iff) ``` chaieb@29687 ` 2010` ``` apply (rule_tac x= "x" in exI) ``` chaieb@29687 ` 2011` ``` apply clarsimp ``` chaieb@29687 ` 2012` ``` apply (rule_tac x="n - x" in exI) ``` chaieb@29687 ` 2013` ``` apply arith ``` chaieb@29687 ` 2014` ``` done ``` chaieb@29687 ` 2015` chaieb@29687 ` 2016` ```lemma product_composition_lemma: ``` chaieb@29687 ` 2017` ``` assumes c0: "c\$0 = (0::'a::idom)" and d0: "d\$0 = 0" ``` chaieb@29687 ` 2018` ``` shows "((a oo c) * (b oo d))\$n = setsum (%(k,m). a\$k * b\$m * (c^k * d^m) \$ n) {(k,m). k + m \ n}" (is "?l = ?r") ``` chaieb@29687 ` 2019` ```proof- ``` chaieb@29687 ` 2020` ``` let ?S = "{(k\nat, m\nat). k + m \ n}" ``` huffman@30488 ` 2021` ``` have s: "?S \ {0..n} <*> {0..n}" by (auto simp add: subset_eq) ``` huffman@30488 ` 2022` ``` have f: "finite {(k\nat, m\nat). k + m \ n}" ``` chaieb@29687 ` 2023` ``` apply (rule finite_subset[OF s]) ``` chaieb@29687 ` 2024` ``` by auto ``` chaieb@29687 ` 2025` ``` have "?r = setsum (%i. setsum (%(k,m). a\$k * (c^k)\$i * b\$m * (d^m) \$ (n - i)) {(k,m). k + m \ n}) {0..n}" ``` chaieb@29687 ` 2026` ``` apply (simp add: fps_mult_nth setsum_right_distrib) ``` chaieb@29687 ` 2027` ``` apply (subst setsum_commute) ``` chaieb@29687 ` 2028` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 2029` ``` by (auto simp add: ring_simps) ``` huffman@30488 ` 2030` ``` also have "\ = ?l" ``` chaieb@29687 ` 2031` ``` apply (simp add: fps_mult_nth fps_compose_nth setsum_product) ``` chaieb@29687 ` 2032` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 2033` ``` apply (simp add: setsum_cartesian_product mult_assoc) ``` chaieb@29687 ` 2034` ``` apply (rule setsum_mono_zero_right[OF f]) ``` chaieb@29687 ` 2035` ``` apply (simp add: subset_eq) apply presburger ``` chaieb@29687 ` 2036` ``` apply clarsimp ``` chaieb@29687 ` 2037` ``` apply (rule ccontr) ``` chaieb@29687 ` 2038` ``` apply (clarsimp simp add: not_le) ``` chaieb@29687 ` 2039` ``` apply (case_tac "x < aa") ``` chaieb@29687 ` 2040` ``` apply simp ``` chaieb@29687 ` 2041` ``` apply (frule_tac startsby_zero_power_prefix[rule_format, OF c0]) ``` chaieb@29687 ` 2042` ``` apply blast ``` chaieb@29687 ` 2043` ``` apply simp ``` chaieb@29687 ` 2044` ``` apply (frule_tac startsby_zero_power_prefix[rule_format, OF d0]) ``` chaieb@29687 ` 2045` ``` apply blast ``` chaieb@29687 ` 2046` ``` done ``` chaieb@29687 ` 2047` ``` finally show ?thesis by simp ``` chaieb@29687 ` 2048` ```qed ``` chaieb@29687 ` 2049` chaieb@29687 ` 2050` ```lemma product_composition_lemma': ``` chaieb@29687 ` 2051` ``` assumes c0: "c\$0 = (0::'a::idom)" and d0: "d\$0 = 0" ``` chaieb@29687 ` 2052` ``` shows "((a oo c) * (b oo d))\$n = setsum (%k. setsum (%m. a\$k * b\$m * (c^k * d^m) \$ n) {0..n}) {0..n}" (is "?l = ?r") ``` chaieb@29687 ` 2053` ``` unfolding product_composition_lemma[OF c0 d0] ``` chaieb@29687 ` 2054` ``` unfolding setsum_cartesian_product ``` chaieb@29687 ` 2055` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 2056` ``` apply simp ``` chaieb@29687 ` 2057` ``` apply (clarsimp simp add: subset_eq) ``` chaieb@29687 ` 2058` ``` apply clarsimp ``` chaieb@29687 ` 2059` ``` apply (rule ccontr) ``` chaieb@29687 ` 2060` ``` apply (subgoal_tac "(c^aa * d^ba) \$ n = 0") ``` chaieb@29687 ` 2061` ``` apply simp ``` chaieb@29687 ` 2062` ``` unfolding fps_mult_nth ``` chaieb@29687 ` 2063` ``` apply (rule setsum_0') ``` chaieb@29687 ` 2064` ``` apply (clarsimp simp add: not_le) ``` chaieb@29687 ` 2065` ``` apply (case_tac "aaa < aa") ``` chaieb@29687 ` 2066` ``` apply (rule startsby_zero_power_prefix[OF c0, rule_format]) ``` chaieb@29687 ` 2067` ``` apply simp ``` chaieb@29687 ` 2068` ``` apply (subgoal_tac "n - aaa < ba") ``` chaieb@29687 ` 2069` ``` apply (frule_tac k = "ba" in startsby_zero_power_prefix[OF d0, rule_format]) ``` chaieb@29687 ` 2070` ``` apply simp ``` chaieb@29687 ` 2071` ``` apply arith ``` chaieb@29687 ` 2072` ``` done ``` huffman@30488 ` 2073` chaieb@29687 ` 2074` huffman@30488 ` 2075` ```lemma setsum_pair_less_iff: ``` chaieb@29687 ` 2076` ``` "setsum (%((k::nat),m). a k * b m * c (k + m)) {(k,m). k + m \ n} = setsum (%s. setsum (%i. a i * b (s - i) * c s) {0..s}) {0..n}" (is "?l = ?r") ``` chaieb@29687 ` 2077` ```proof- ``` chaieb@29687 ` 2078` ``` let ?KM= "{(k,m). k + m \ n}" ``` chaieb@29687 ` 2079` ``` let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})" ``` chaieb@29687 ` 2080` ``` have th0: "?KM = UNION {0..n} ?f" ``` chaieb@29687 ` 2081` ``` apply (simp add: expand_set_eq) ``` huffman@29911 ` 2082` ``` apply arith (* FIXME: VERY slow! *) ``` chaieb@29687 ` 2083` ``` done ``` chaieb@29687 ` 2084` ``` show "?l = ?r " ``` chaieb@29687 ` 2085` ``` unfolding th0 ``` chaieb@29687 ` 2086` ``` apply (subst setsum_UN_disjoint) ``` chaieb@29687 ` 2087` ``` apply auto ``` chaieb@29687 ` 2088` ``` apply (subst setsum_UN_disjoint) ``` chaieb@29687 ` 2089` ``` apply auto ``` chaieb@29687 ` 2090` ``` done ``` chaieb@29687 ` 2091` ```qed ``` chaieb@29687 ` 2092` chaieb@29687 ` 2093` ```lemma fps_compose_mult_distrib_lemma: ``` chaieb@29687 ` 2094` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2095` ``` shows "((a oo c) * (b oo c))\$n = setsum (%s. setsum (%i. a\$i * b\$(s - i) * (c^s) \$ n) {0..s}) {0..n}" (is "?l = ?r") ``` chaieb@29687 ` 2096` ``` unfolding product_composition_lemma[OF c0 c0] power_add[symmetric] ``` chaieb@29687 ` 2097` ``` unfolding setsum_pair_less_iff[where a = "%k. a\$k" and b="%m. b\$m" and c="%s. (c ^ s)\$n" and n = n] .. ``` chaieb@29687 ` 2098` chaieb@29687 ` 2099` huffman@30488 ` 2100` ```lemma fps_compose_mult_distrib: ``` chaieb@29687 ` 2101` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2102` ``` shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r") ``` chaieb@29687 ` 2103` ``` apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0]) ``` chaieb@29687 ` 2104` ``` by (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib) ``` huffman@30488 ` 2105` ```lemma fps_compose_setprod_distrib: ``` chaieb@29687 ` 2106` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2107` ``` shows "(setprod a S) oo c = setprod (%k. a k oo c) S" (is "?l = ?r") ``` chaieb@29687 ` 2108` ``` apply (cases "finite S") ``` chaieb@29687 ` 2109` ``` apply simp_all ``` chaieb@29687 ` 2110` ``` apply (induct S rule: finite_induct) ``` chaieb@29687 ` 2111` ``` apply simp ``` chaieb@29687 ` 2112` ``` apply (simp add: fps_compose_mult_distrib[OF c0]) ``` chaieb@29687 ` 2113` ``` done ``` chaieb@29687 ` 2114` chaieb@29687 ` 2115` ```lemma fps_compose_power: assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2116` ``` shows "(a oo c)^n = a^n oo c" (is "?l = ?r") ``` chaieb@29687 ` 2117` ```proof- ``` chaieb@29687 ` 2118` ``` {assume "n=0" then have ?thesis by simp} ``` chaieb@29687 ` 2119` ``` moreover ``` chaieb@29687 ` 2120` ``` {fix m assume m: "n = Suc m" ``` chaieb@29687 ` 2121` ``` have th0: "a^n = setprod (%k. a) {0..m}" "(a oo c) ^ n = setprod (%k. a oo c) {0..m}" ``` chaieb@29687 ` 2122` ``` by (simp_all add: setprod_constant m) ``` chaieb@29687 ` 2123` ``` then have ?thesis ``` chaieb@29687 ` 2124` ``` by (simp add: fps_compose_setprod_distrib[OF c0])} ``` chaieb@29687 ` 2125` ``` ultimately show ?thesis by (cases n, auto) ``` chaieb@29687 ` 2126` ```qed ``` chaieb@29687 ` 2127` chaieb@31199 ` 2128` ```lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" ``` chaieb@31199 ` 2129` ``` by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) ``` chaieb@31199 ` 2130` chaieb@31199 ` 2131` ```lemma fps_compose_sub_distrib: ``` chaieb@31199 ` 2132` ``` shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" ``` chaieb@31199 ` 2133` ``` unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. ``` chaieb@31199 ` 2134` chaieb@31199 ` 2135` ```lemma X_fps_compose:"X oo a = Abs_fps (\n. if n = 0 then (0::'a::comm_ring_1) else a\$n)" ``` chaieb@31199 ` 2136` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) ``` chaieb@31199 ` 2137` chaieb@31199 ` 2138` ```lemma fps_inverse_compose: ``` chaieb@31199 ` 2139` ``` assumes b0: "(b\$0 :: 'a::field) = 0" and a0: "a\$0 \ 0" ``` chaieb@31199 ` 2140` ``` shows "inverse a oo b = inverse (a oo b)" ``` chaieb@31199 ` 2141` ```proof- ``` chaieb@31199 ` 2142` ``` let ?ia = "inverse a" ``` chaieb@31199 ` 2143` ``` let ?ab = "a oo b" ``` chaieb@31199 ` 2144` ``` let ?iab = "inverse ?ab" ``` chaieb@31199 ` 2145` chaieb@31199 ` 2146` ```from a0 have ia0: "?ia \$ 0 \ 0" by (simp ) ``` chaieb@31199 ` 2147` ```from a0 have ab0: "?ab \$ 0 \ 0" by (simp add: fps_compose_def) ``` chaieb@31199 ` 2148` ```thm inverse_mult_eq_1[OF ab0] ``` chaieb@31199 ` 2149` ```have "(?ia oo b) * (a oo b) = 1" ``` chaieb@31199 ` 2150` ```unfolding fps_compose_mult_distrib[OF b0, symmetric] ``` chaieb@31199 ` 2151` ```unfolding inverse_mult_eq_1[OF a0] ``` chaieb@31199 ` 2152` ```fps_compose_1 .. ``` chaieb@31199 ` 2153` chaieb@31199 ` 2154` ```then have "(?ia oo b) * (a oo b) * ?iab = 1 * ?iab" by simp ``` chaieb@31199 ` 2155` ```then have "(?ia oo b) * (?iab * (a oo b)) = ?iab" by simp ``` chaieb@31199 ` 2156` ```then show ?thesis ``` chaieb@31199 ` 2157` ``` unfolding inverse_mult_eq_1[OF ab0] by simp ``` chaieb@31199 ` 2158` ```qed ``` chaieb@31199 ` 2159` chaieb@31199 ` 2160` ```lemma fps_divide_compose: ``` chaieb@31199 ` 2161` ``` assumes c0: "(c\$0 :: 'a::field) = 0" and b0: "b\$0 \ 0" ``` chaieb@31199 ` 2162` ``` shows "(a/b) oo c = (a oo c) / (b oo c)" ``` chaieb@31199 ` 2163` ``` unfolding fps_divide_def fps_compose_mult_distrib[OF c0] ``` chaieb@31199 ` 2164` ``` fps_inverse_compose[OF c0 b0] .. ``` chaieb@31199 ` 2165` chaieb@31199 ` 2166` ```lemma gp: assumes a0: "a\$0 = (0::'a::field)" ``` chaieb@31199 ` 2167` ``` shows "(Abs_fps (\n. 1)) oo a = 1/(1 - a)" (is "?one oo a = _") ``` chaieb@31199 ` 2168` ```proof- ``` chaieb@31199 ` 2169` ``` have o0: "?one \$ 0 \ 0" by simp ``` chaieb@31199 ` 2170` ``` have th0: "(1 - X) \$ 0 \ (0::'a)" by simp ``` chaieb@31199 ` 2171` ``` from fps_inverse_gp[where ?'a = 'a] ``` chaieb@31199 ` 2172` ``` have "inverse ?one = 1 - X" by (simp add: fps_eq_iff) ``` chaieb@31199 ` 2173` ``` hence "inverse (inverse ?one) = inverse (1 - X)" by simp ``` chaieb@31199 ` 2174` ``` hence th: "?one = 1/(1 - X)" unfolding fps_inverse_idempotent[OF o0] ``` chaieb@31199 ` 2175` ``` by (simp add: fps_divide_def) ``` chaieb@31199 ` 2176` ``` show ?thesis unfolding th ``` chaieb@31199 ` 2177` ``` unfolding fps_divide_compose[OF a0 th0] ``` chaieb@31199 ` 2178` ``` fps_compose_1 fps_compose_sub_distrib X_fps_compose_startby0[OF a0] .. ``` chaieb@31199 ` 2179` ```qed ``` chaieb@31199 ` 2180` chaieb@31199 ` 2181` ```lemma fps_const_power[simp]: "fps_const (c::'a::ring_1) ^ n = fps_const (c^n)" ``` chaieb@31199 ` 2182` ```by (induct n, auto) ``` chaieb@31199 ` 2183` chaieb@31199 ` 2184` ```lemma fps_compose_radical: ``` huffman@31273 ` 2185` ``` assumes b0: "b\$0 = (0::'a::field_char_0)" ``` chaieb@31199 ` 2186` ``` and ra0: "r (Suc k) (a\$0) ^ Suc k = a\$0" ``` chaieb@31199 ` 2187` ``` and a0: "a\$0 \ 0" ``` chaieb@31199 ` 2188` ``` shows "fps_radical r (Suc k) a oo b = fps_radical r (Suc k) (a oo b)" ``` chaieb@31199 ` 2189` ```proof- ``` chaieb@31199 ` 2190` ``` let ?r = "fps_radical r (Suc k)" ``` chaieb@31199 ` 2191` ``` let ?ab = "a oo b" ``` chaieb@31199 ` 2192` ``` have ab0: "?ab \$ 0 = a\$0" by (simp add: fps_compose_def) ``` chaieb@31199 ` 2193` ``` from ab0 a0 ra0 have rab0: "?ab \$ 0 \ 0" "r (Suc k) (?ab \$ 0) ^ Suc k = ?ab \$ 0" by simp_all ``` chaieb@31199 ` 2194` ``` have th00: "r (Suc k) ((a oo b) \$ 0) = (fps_radical r (Suc k) a oo b) \$ 0" ``` chaieb@31199 ` 2195` ``` by (simp add: ab0 fps_compose_def) ``` chaieb@31199 ` 2196` ``` have th0: "(?r a oo b) ^ (Suc k) = a oo b" ``` chaieb@31199 ` 2197` ``` unfolding fps_compose_power[OF b0] ``` chaieb@31199 ` 2198` ``` unfolding iffD1[OF power_radical[of a r k], OF a0 ra0] .. ``` chaieb@31199 ` 2199` ``` from iffD1[OF radical_unique[where r=r and k=k and b= ?ab and a = "?r a oo b", OF rab0(2) th00 rab0(1)], OF th0] show ?thesis . ``` chaieb@31199 ` 2200` ```qed ``` chaieb@31199 ` 2201` chaieb@29687 ` 2202` ```lemma fps_const_mult_apply_left: ``` chaieb@29687 ` 2203` ``` "fps_const c * (a oo b) = (fps_const c * a) oo b" ``` chaieb@29687 ` 2204` ``` by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc) ``` chaieb@29687 ` 2205` chaieb@29687 ` 2206` ```lemma fps_const_mult_apply_right: ``` chaieb@29687 ` 2207` ``` "(a oo b) * fps_const (c::'a::comm_semiring_1) = (fps_const c * a) oo b" ``` chaieb@29687 ` 2208` ``` by (auto simp add: fps_const_mult_apply_left mult_commute) ``` chaieb@29687 ` 2209` huffman@30488 ` 2210` ```lemma fps_compose_assoc: ``` chaieb@29687 ` 2211` ``` assumes c0: "c\$0 = (0::'a::idom)" and b0: "b\$0 = 0" ``` chaieb@29687 ` 2212` ``` shows "a oo (b oo c) = a oo b oo c" (is "?l = ?r") ``` chaieb@29687 ` 2213` ```proof- ``` chaieb@29687 ` 2214` ``` {fix n ``` chaieb@29687 ` 2215` ``` have "?l\$n = (setsum (\i. (fps_const (a\$i) * b^i) oo c) {0..n})\$n" ``` chaieb@29687 ` 2216` ``` by (simp add: fps_compose_nth fps_compose_power[OF c0] fps_const_mult_apply_left setsum_right_distrib mult_assoc fps_setsum_nth) ``` chaieb@29687 ` 2217` ``` also have "\ = ((setsum (\i. fps_const (a\$i) * b^i) {0..n}) oo c)\$n" ``` chaieb@29687 ` 2218` ``` by (simp add: fps_compose_setsum_distrib) ``` chaieb@29687 ` 2219` ``` also have "\ = ?r\$n" ``` chaieb@29687 ` 2220` ``` apply (simp add: fps_compose_nth fps_setsum_nth setsum_left_distrib mult_assoc) ``` chaieb@29687 ` 2221` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 2222` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 2223` ``` apply (auto simp add: not_le) ``` chaieb@29687 ` 2224` ``` by (erule startsby_zero_power_prefix[OF b0, rule_format]) ``` chaieb@29687 ` 2225` ``` finally have "?l\$n = ?r\$n" .} ``` chaieb@29687 ` 2226` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2227` ```qed ``` chaieb@29687 ` 2228` chaieb@29687 ` 2229` chaieb@29687 ` 2230` ```lemma fps_X_power_compose: ``` chaieb@29687 ` 2231` ``` assumes a0: "a\$0=0" shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r") ``` chaieb@29687 ` 2232` ```proof- ``` chaieb@29687 ` 2233` ``` {assume "k=0" hence ?thesis by simp} ``` chaieb@29687 ` 2234` ``` moreover ``` chaieb@29687 ` 2235` ``` {fix h assume h: "k = Suc h" ``` chaieb@29687 ` 2236` ``` {fix n ``` huffman@30488 ` 2237` ``` {assume kn: "k>n" hence "?l \$ n = ?r \$n" using a0 startsby_zero_power_prefix[OF a0] h ``` huffman@30273 ` 2238` ``` by (simp add: fps_compose_nth del: power_Suc)} ``` chaieb@29687 ` 2239` ``` moreover ``` chaieb@29687 ` 2240` ``` {assume kn: "k \ n" ``` huffman@29913 ` 2241` ``` hence "?l\$n = ?r\$n" ``` huffman@29913 ` 2242` ``` by (simp add: fps_compose_nth mult_delta_left setsum_delta)} ``` chaieb@29687 ` 2243` ``` moreover have "k >n \ k\ n" by arith ``` chaieb@29687 ` 2244` ``` ultimately have "?l\$n = ?r\$n" by blast} ``` chaieb@29687 ` 2245` ``` then have ?thesis unfolding fps_eq_iff by blast} ``` chaieb@29687 ` 2246` ``` ultimately show ?thesis by (cases k, auto) ``` chaieb@29687 ` 2247` ```qed ``` chaieb@29687 ` 2248` chaieb@29687 ` 2249` ```lemma fps_inv_right: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 2250` ``` shows "a oo fps_inv a = X" ``` chaieb@29687 ` 2251` ```proof- ``` chaieb@29687 ` 2252` ``` let ?ia = "fps_inv a" ``` chaieb@29687 ` 2253` ``` let ?iaa = "a oo fps_inv a" ``` chaieb@29687 ` 2254` ``` have th0: "?ia \$ 0 = 0" by (simp add: fps_inv_def) ``` huffman@30488 ` 2255` ``` have th1: "?iaa \$ 0 = 0" using a0 a1 ``` chaieb@29687 ` 2256` ``` by (simp add: fps_inv_def fps_compose_nth) ``` chaieb@29687 ` 2257` ``` have th2: "X\$0 = 0" by simp ``` chaieb@29687 ` 2258` ``` from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X" by simp ``` chaieb@29687 ` 2259` ``` then have "(a oo fps_inv a) oo a = X oo a" ``` chaieb@29687 ` 2260` ``` by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0]) ``` chaieb@29687 ` 2261` ``` with fps_compose_inj_right[OF a0 a1] ``` huffman@30488 ` 2262` ``` show ?thesis by simp ``` chaieb@29687 ` 2263` ```qed ``` chaieb@29687 ` 2264` chaieb@29687 ` 2265` ```lemma fps_inv_deriv: ``` haftmann@31021 ` 2266` ``` assumes a0:"a\$0 = (0::'a::{field})" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 2267` ``` shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)" ``` chaieb@29687 ` 2268` ```proof- ``` chaieb@29687 ` 2269` ``` let ?ia = "fps_inv a" ``` chaieb@29687 ` 2270` ``` let ?d = "fps_deriv a oo ?ia" ``` chaieb@29687 ` 2271` ``` let ?dia = "fps_deriv ?ia" ``` chaieb@29687 ` 2272` ``` have ia0: "?ia\$0 = 0" by (simp add: fps_inv_def) ``` chaieb@29687 ` 2273` ``` have th0: "?d\$0 \ 0" using a1 by (simp add: fps_compose_nth fps_deriv_nth) ``` chaieb@29687 ` 2274` ``` from fps_inv_right[OF a0 a1] have "?d * ?dia = 1" ``` chaieb@29687 ` 2275` ``` by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] ) ``` chaieb@29687 ` 2276` ``` hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp ``` chaieb@29687 ` 2277` ``` with inverse_mult_eq_1[OF th0] ``` chaieb@29687 ` 2278` ``` show "?dia = inverse ?d" by simp ``` chaieb@29687 ` 2279` ```qed ``` chaieb@29687 ` 2280` chaieb@31369 ` 2281` ```lemma fps_inv_idempotent: ``` chaieb@31369 ` 2282` ``` assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@31369 ` 2283` ``` shows "fps_inv (fps_inv a) = a" ``` chaieb@31369 ` 2284` ```proof- ``` chaieb@31369 ` 2285` ``` let ?r = "fps_inv" ``` chaieb@31369 ` 2286` ``` have ra0: "?r a \$ 0 = 0" by (simp add: fps_inv_def) ``` chaieb@31369 ` 2287` ``` from a1 have ra1: "?r a \$ 1 \ 0" by (simp add: fps_inv_def field_simps) ``` chaieb@31369 ` 2288` ``` have X0: "X\$0 = 0" by simp ``` chaieb@31369 ` 2289` ``` from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" . ``` chaieb@31369 ` 2290` ``` then have "?r (?r a) oo ?r a oo a = X oo a" by simp ``` chaieb@31369 ` 2291` ``` then have "?r (?r a) oo (?r a oo a) = a" ``` chaieb@31369 ` 2292` ``` unfolding X_fps_compose_startby0[OF a0] ``` chaieb@31369 ` 2293` ``` unfolding fps_compose_assoc[OF a0 ra0, symmetric] . ``` chaieb@31369 ` 2294` ``` then show ?thesis unfolding fps_inv[OF a0 a1] by simp ``` chaieb@31369 ` 2295` ```qed ``` chaieb@31369 ` 2296` chaieb@31369 ` 2297` ```lemma fps_ginv_ginv: ``` chaieb@31369 ` 2298` ``` assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@31369 ` 2299` ``` and c0: "c\$0 = 0" and c1: "c\$1 \ 0" ``` chaieb@31369 ` 2300` ``` shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c" ``` chaieb@31369 ` 2301` ```proof- ``` chaieb@31369 ` 2302` ``` let ?r = "fps_ginv" ``` chaieb@31369 ` 2303` ``` from c0 have rca0: "?r c a \$0 = 0" by (simp add: fps_ginv_def) ``` chaieb@31369 ` 2304` ``` from a1 c1 have rca1: "?r c a \$ 1 \ 0" by (simp add: fps_ginv_def field_simps) ``` chaieb@31369 ` 2305` ``` from fps_ginv[OF rca0 rca1] ``` chaieb@31369 ` 2306` ``` have "?r b (?r c a) oo ?r c a = b" . ``` chaieb@31369 ` 2307` ``` then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp ``` chaieb@31369 ` 2308` ``` then have "?r b (?r c a) oo (?r c a oo a) = b oo a" ``` chaieb@31369 ` 2309` ``` apply (subst fps_compose_assoc) ``` chaieb@31369 ` 2310` ``` using a0 c0 by (auto simp add: fps_ginv_def) ``` chaieb@31369 ` 2311` ``` then have "?r b (?r c a) oo c = b oo a" ``` chaieb@31369 ` 2312` ``` unfolding fps_ginv[OF a0 a1] . ``` chaieb@31369 ` 2313` ``` then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp ``` chaieb@31369 ` 2314` ``` then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" ``` chaieb@31369 ` 2315` ``` apply (subst fps_compose_assoc) ``` chaieb@31369 ` 2316` ``` using a0 c0 by (auto simp add: fps_inv_def) ``` chaieb@31369 ` 2317` ``` then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp ``` chaieb@31369 ` 2318` ```qed ``` chaieb@31369 ` 2319` huffman@29906 ` 2320` ```subsection{* Elementary series *} ``` chaieb@29687 ` 2321` huffman@29906 ` 2322` ```subsubsection{* Exponential series *} ``` huffman@30488 ` 2323` ```definition "E x = Abs_fps (\n. x^n / of_nat (fact n))" ``` chaieb@29687 ` 2324` huffman@31273 ` 2325` ```lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r") ``` chaieb@29687 ` 2326` ```proof- ``` chaieb@29687 ` 2327` ``` {fix n ``` chaieb@29687 ` 2328` ``` have "?l\$n = ?r \$ n" ``` huffman@30273 ` 2329` ``` apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) ``` chaieb@29687 ` 2330` ``` by (simp add: of_nat_mult ring_simps)} ``` chaieb@29687 ` 2331` ```then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2332` ```qed ``` chaieb@29687 ` 2333` huffman@30488 ` 2334` ```lemma E_unique_ODE: ``` huffman@31273 ` 2335` ``` "fps_deriv a = fps_const c * a \ a = fps_const (a\$0) * E (c :: 'a::field_char_0)" ``` chaieb@29687 ` 2336` ``` (is "?lhs \ ?rhs") ``` chaieb@29687 ` 2337` ```proof- ``` chaieb@29687 ` 2338` ``` {assume d: ?lhs ``` huffman@30488 ` 2339` ``` from d have th: "\n. a \$ Suc n = c * a\$n / of_nat (Suc n)" ``` chaieb@29687 ` 2340` ``` by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) ``` chaieb@29687 ` 2341` ``` {fix n have "a\$n = a\$0 * c ^ n/ (of_nat (fact n))" ``` chaieb@29687 ` 2342` ``` apply (induct n) ``` chaieb@29687 ` 2343` ``` apply simp ``` huffman@30488 ` 2344` ``` unfolding th ``` chaieb@29687 ` 2345` ``` using fact_gt_zero ``` chaieb@29687 ` 2346` ``` apply (simp add: field_simps del: of_nat_Suc fact.simps) ``` chaieb@29687 ` 2347` ``` apply (drule sym) ``` chaieb@29687 ` 2348` ``` by (simp add: ring_simps of_nat_mult power_Suc)} ``` chaieb@29687 ` 2349` ``` note th' = this ``` huffman@30488 ` 2350` ``` have ?rhs ``` chaieb@29687 ` 2351` ``` by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')} ``` chaieb@29687 ` 2352` ```moreover ``` chaieb@29687 ` 2353` ```{assume h: ?rhs ``` huffman@30488 ` 2354` ``` have ?lhs ``` chaieb@29687 ` 2355` ``` apply (subst h) ``` chaieb@29687 ` 2356` ``` apply simp ``` chaieb@29687 ` 2357` ``` apply (simp only: h[symmetric]) ``` chaieb@29687 ` 2358` ``` by simp} ``` chaieb@29687 ` 2359` ```ultimately show ?thesis by blast ``` chaieb@29687 ` 2360` ```qed ``` chaieb@29687 ` 2361` huffman@31273 ` 2362` ```lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") ``` chaieb@29687 ` 2363` ```proof- ``` chaieb@29687 ` 2364` ``` have "fps_deriv (?r) = fps_const (a+b) * ?r" ``` chaieb@29687 ` 2365` ``` by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add) ``` chaieb@29687 ` 2366` ``` then have "?r = ?l" apply (simp only: E_unique_ODE) ``` chaieb@29687 ` 2367` ``` by (simp add: fps_mult_nth E_def) ``` chaieb@29687 ` 2368` ``` then show ?thesis .. ``` chaieb@29687 ` 2369` ```qed ``` chaieb@29687 ` 2370` chaieb@29687 ` 2371` ```lemma E_nth[simp]: "E a \$ n = a^n / of_nat (fact n)" ``` chaieb@29687 ` 2372` ``` by (simp add: E_def) ``` chaieb@29687 ` 2373` haftmann@31021 ` 2374` ```lemma E0[simp]: "E (0::'a::{field}) = 1" ``` chaieb@29687 ` 2375` ``` by (simp add: fps_eq_iff power_0_left) ``` chaieb@29687 ` 2376` huffman@31273 ` 2377` ```lemma E_neg: "E (- a) = inverse (E (a::'a::field_char_0))" ``` chaieb@29687 ` 2378` ```proof- ``` chaieb@29687 ` 2379` ``` from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1" ``` chaieb@29687 ` 2380` ``` by (simp ) ``` chaieb@29687 ` 2381` ``` have th1: "E a \$ 0 \ 0" by simp ``` chaieb@29687 ` 2382` ``` from fps_inverse_unique[OF th1 th0] show ?thesis by simp ``` chaieb@29687 ` 2383` ```qed ``` chaieb@29687 ` 2384` huffman@31273 ` 2385` ```lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::field_char_0)) = (fps_const a)^n * (E a)" ``` chaieb@29687 ` 2386` ``` by (induct n, auto simp add: power_Suc) ``` chaieb@29687 ` 2387` haftmann@31021 ` 2388` ```lemma X_compose_E[simp]: "X oo E (a::'a::{field}) = E a - 1" ``` chaieb@29687 ` 2389` ``` by (simp add: fps_eq_iff X_fps_compose) ``` chaieb@29687 ` 2390` huffman@30488 ` 2391` ```lemma LE_compose: ``` huffman@30488 ` 2392` ``` assumes a: "a\0" ``` chaieb@29687 ` 2393` ``` shows "fps_inv (E a - 1) oo (E a - 1) = X" ``` chaieb@29687 ` 2394` ``` and "(E a - 1) oo fps_inv (E a - 1) = X" ``` chaieb@29687 ` 2395` ```proof- ``` chaieb@29687 ` 2396` ``` let ?b = "E a - 1" ``` chaieb@29687 ` 2397` ``` have b0: "?b \$ 0 = 0" by simp ``` chaieb@29687 ` 2398` ``` have b1: "?b \$ 1 \ 0" by (simp add: a) ``` chaieb@29687 ` 2399` ``` from fps_inv[OF b0 b1] show "fps_inv (E a - 1) oo (E a - 1) = X" . ``` chaieb@29687 ` 2400` ``` from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" . ``` chaieb@29687 ` 2401` ```qed ``` chaieb@29687 ` 2402` chaieb@29687 ` 2403` huffman@30488 ` 2404` ```lemma fps_const_inverse: ``` chaieb@31369 ` 2405` ``` "a \ 0 \ inverse (fps_const (a::'a::field)) = fps_const (inverse a)" ``` chaieb@29687 ` 2406` ``` apply (auto simp add: fps_eq_iff fps_inverse_def) by (case_tac "n", auto) ``` chaieb@29687 ` 2407` huffman@30488 ` 2408` ```lemma inverse_one_plus_X: ``` haftmann@31021 ` 2409` ``` "inverse (1 + X) = Abs_fps (\n. (- 1 ::'a::{field})^n)" ``` chaieb@29687 ` 2410` ``` (is "inverse ?l = ?r") ``` chaieb@29687 ` 2411` ```proof- ``` chaieb@29687 ` 2412` ``` have th: "?l * ?r = 1" ``` nipkow@31148 ` 2413` ``` by (auto simp add: ring_simps fps_eq_iff minus_one_power_iff) ``` chaieb@29687 ` 2414` ``` have th': "?l \$ 0 \ 0" by (simp add: ) ``` chaieb@29687 ` 2415` ``` from fps_inverse_unique[OF th' th] show ?thesis . ``` chaieb@29687 ` 2416` ```qed ``` chaieb@29687 ` 2417` huffman@31273 ` 2418` ```lemma E_power_mult: "(E (c::'a::field_char_0))^n = E (of_nat n * c)" ``` chaieb@29687 ` 2419` ``` by (induct n, auto simp add: ring_simps E_add_mult power_Suc) ``` chaieb@29687 ` 2420` chaieb@31369 ` 2421` ```lemma assumes r: "r (Suc k) 1 = 1" ``` chaieb@31370 ` 2422` ``` shows "fps_radical r (Suc k) (E (c::'a::{field_char_0})) = E (c / of_nat (Suc k))" ``` chaieb@31369 ` 2423` ```proof- ``` chaieb@31369 ` 2424` ``` let ?ck = "(c / of_nat (Suc k))" ``` chaieb@31369 ` 2425` ``` let ?r = "fps_radical r (Suc k)" ``` chaieb@31369 ` 2426` ``` have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c" ``` chaieb@31369 ` 2427` ``` by (simp_all del: of_nat_Suc) ``` chaieb@31369 ` 2428` ``` have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 .. ``` chaieb@31369 ` 2429` ``` have th: "r (Suc k) (E c \$0) ^ Suc k = E c \$ 0" ``` chaieb@31369 ` 2430` ``` "r (Suc k) (E c \$ 0) = E ?ck \$ 0" "E c \$ 0 \ 0" using r by simp_all ``` chaieb@31369 ` 2431` ``` from th0 radical_unique[where r=r and k=k, OF th] ``` chaieb@31369 ` 2432` ``` show ?thesis by auto ``` chaieb@31369 ` 2433` ```qed ``` chaieb@29687 ` 2434` chaieb@31369 ` 2435` ```lemma Ec_E1_eq: ```