src/HOL/Library/Formal_Power_Series.thy
 author haftmann Wed Apr 22 19:09:21 2009 +0200 (2009-04-22) changeset 30960 fec1a04b7220 parent 30952 7ab2716dd93b child 30971 7fbebf75b3ef permissions -rw-r--r--
power operation defined generic
 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 ``` haftmann@30661 ` 8` ```imports Main Fact Parity ``` 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) ``` huffman@29911 ` 332` chaieb@29687 ` 333` ```lemma fps_const_mult[simp]: "fps_const (c::'a\ring) * fps_const d = fps_const (c * d)" ``` huffman@29911 ` 334` ``` by (simp add: fps_eq_iff fps_mult_nth setsum_0') ``` chaieb@29687 ` 335` chaieb@29687 ` 336` ```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 ` 337` ``` by (simp add: fps_ext) ``` huffman@29911 ` 338` chaieb@29687 ` 339` ```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 ` 340` ``` by (simp add: fps_ext) ``` chaieb@29687 ` 341` chaieb@29687 ` 342` ```lemma fps_const_mult_left: "fps_const (c::'a\semiring_0) * f = Abs_fps (\n. c * f\$n)" ``` huffman@29911 ` 343` ``` unfolding fps_eq_iff fps_mult_nth ``` huffman@29913 ` 344` ``` by (simp add: fps_const_def mult_delta_left setsum_delta) ``` huffman@29911 ` 345` chaieb@29687 ` 346` ```lemma fps_const_mult_right: "f * fps_const (c::'a\semiring_0) = Abs_fps (\n. f\$n * c)" ``` huffman@29911 ` 347` ``` unfolding fps_eq_iff fps_mult_nth ``` huffman@29913 ` 348` ``` by (simp add: fps_const_def mult_delta_right setsum_delta') ``` chaieb@29687 ` 349` huffman@29911 ` 350` ```lemma fps_mult_left_const_nth [simp]: "(fps_const (c::'a::semiring_1) * f)\$n = c* f\$n" ``` huffman@29913 ` 351` ``` by (simp add: fps_mult_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 352` huffman@29911 ` 353` ```lemma fps_mult_right_const_nth [simp]: "(f * fps_const (c::'a::semiring_1))\$n = f\$n * c" ``` huffman@29913 ` 354` ``` by (simp add: fps_mult_nth mult_delta_right setsum_delta') ``` chaieb@29687 ` 355` huffman@29906 ` 356` ```subsection {* Formal power series form an integral domain*} ``` chaieb@29687 ` 357` huffman@29911 ` 358` ```instance fps :: (ring) ring .. ``` chaieb@29687 ` 359` huffman@29911 ` 360` ```instance fps :: (ring_1) ring_1 ``` huffman@29911 ` 361` ``` by (intro_classes, auto simp add: diff_minus left_distrib) ``` chaieb@29687 ` 362` huffman@29911 ` 363` ```instance fps :: (comm_ring_1) comm_ring_1 ``` huffman@29911 ` 364` ``` by (intro_classes, auto simp add: diff_minus left_distrib) ``` chaieb@29687 ` 365` huffman@29911 ` 366` ```instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors ``` chaieb@29687 ` 367` ```proof ``` chaieb@29687 ` 368` ``` fix a b :: "'a fps" ``` chaieb@29687 ` 369` ``` assume a0: "a \ 0" and b0: "b \ 0" ``` chaieb@29687 ` 370` ``` then obtain i j where i: "a\$i\0" "\k0" "\kk=0..i+j. a\$k * b\$(i+j-k))" ``` chaieb@29687 ` 374` ``` by (rule fps_mult_nth) ``` huffman@29911 ` 375` ``` also have "\ = (a\$i * b\$(i+j-i)) + (\k\{0..i+j}-{i}. a\$k * b\$(i+j-k))" ``` huffman@29911 ` 376` ``` by (rule setsum_diff1') simp_all ``` huffman@29911 ` 377` ``` also have "(\k\{0..i+j}-{i}. a\$k * b\$(i+j-k)) = 0" ``` huffman@29911 ` 378` ``` proof (rule setsum_0' [rule_format]) ``` huffman@29911 ` 379` ``` fix k assume "k \ {0..i+j} - {i}" ``` huffman@29911 ` 380` ``` then have "k < i \ i+j-k < j" by auto ``` huffman@29911 ` 381` ``` then show "a\$k * b\$(i+j-k) = 0" using i j by auto ``` huffman@29911 ` 382` ``` qed ``` huffman@29911 ` 383` ``` also have "a\$i * b\$(i+j-i) + 0 = a\$i * b\$j" by simp ``` huffman@29911 ` 384` ``` also have "a\$i * b\$j \ 0" using i j by simp ``` huffman@29911 ` 385` ``` finally have "(a*b) \$ (i+j) \ 0" . ``` chaieb@29687 ` 386` ``` then show "a*b \ 0" unfolding fps_nonzero_nth by blast ``` chaieb@29687 ` 387` ```qed ``` chaieb@29687 ` 388` huffman@29911 ` 389` ```instance fps :: (idom) idom .. ``` chaieb@29687 ` 390` chaieb@30746 ` 391` ```instantiation fps :: (comm_ring_1) number_ring ``` chaieb@30746 ` 392` ```begin ``` chaieb@30746 ` 393` ```definition number_of_fps_def: "(number_of k::'a fps) = of_int k" ``` chaieb@30746 ` 394` chaieb@30746 ` 395` ```instance ``` chaieb@30746 ` 396` ```by (intro_classes, rule number_of_fps_def) ``` chaieb@30746 ` 397` ```end ``` chaieb@30746 ` 398` huffman@29906 ` 399` ```subsection{* Inverses of formal power series *} ``` chaieb@29687 ` 400` chaieb@29687 ` 401` ```declare setsum_cong[fundef_cong] ``` chaieb@29687 ` 402` chaieb@29687 ` 403` chaieb@29687 ` 404` ```instantiation fps :: ("{comm_monoid_add,inverse, times, uminus}") inverse ``` chaieb@29687 ` 405` ```begin ``` chaieb@29687 ` 406` huffman@30488 ` 407` ```fun natfun_inverse:: "'a fps \ nat \ 'a" where ``` chaieb@29687 ` 408` ``` "natfun_inverse f 0 = inverse (f\$0)" ``` huffman@30488 ` 409` ```| "natfun_inverse f n = - inverse (f\$0) * setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n}" ``` chaieb@29687 ` 410` huffman@30488 ` 411` ```definition fps_inverse_def: ``` chaieb@29687 ` 412` ``` "inverse f = (if f\$0 = 0 then 0 else Abs_fps (natfun_inverse f))" ``` huffman@29911 ` 413` ```definition fps_divide_def: "divide = (\(f::'a fps) g. f * inverse g)" ``` chaieb@29687 ` 414` ```instance .. ``` chaieb@29687 ` 415` ```end ``` chaieb@29687 ` 416` huffman@30488 ` 417` ```lemma fps_inverse_zero[simp]: ``` chaieb@29687 ` 418` ``` "inverse (0 :: 'a::{comm_monoid_add,inverse, times, uminus} fps) = 0" ``` huffman@29911 ` 419` ``` by (simp add: fps_ext fps_inverse_def) ``` chaieb@29687 ` 420` chaieb@29687 ` 421` ```lemma fps_inverse_one[simp]: "inverse (1 :: 'a::{division_ring,zero_neq_one} fps) = 1" ``` huffman@29911 ` 422` ``` apply (auto simp add: expand_fps_eq fps_inverse_def) ``` huffman@29911 ` 423` ``` by (case_tac n, auto) ``` chaieb@29687 ` 424` huffman@29911 ` 425` ```instance fps :: ("{comm_monoid_add,inverse, times, uminus}") division_by_zero ``` huffman@29911 ` 426` ``` by default (rule fps_inverse_zero) ``` chaieb@29687 ` 427` chaieb@29687 ` 428` ```lemma inverse_mult_eq_1[intro]: assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 429` ``` shows "inverse f * f = 1" ``` chaieb@29687 ` 430` ```proof- ``` chaieb@29687 ` 431` ``` have c: "inverse f * f = f * inverse f" by (simp add: mult_commute) ``` huffman@30488 ` 432` ``` from f0 have ifn: "\n. inverse f \$ n = natfun_inverse f n" ``` chaieb@29687 ` 433` ``` by (simp add: fps_inverse_def) ``` chaieb@29687 ` 434` ``` from f0 have th0: "(inverse f * f) \$ 0 = 1" ``` huffman@29911 ` 435` ``` by (simp add: fps_mult_nth fps_inverse_def) ``` chaieb@29687 ` 436` ``` {fix n::nat assume np: "n >0 " ``` chaieb@29687 ` 437` ``` from np have eq: "{0..n} = {0} \ {1 .. n}" by auto ``` chaieb@29687 ` 438` ``` have d: "{0} \ {1 .. n} = {}" by auto ``` chaieb@29687 ` 439` ``` have f: "finite {0::nat}" "finite {1..n}" by auto ``` huffman@30488 ` 440` ``` from f0 np have th0: "- (inverse f\$n) = ``` chaieb@29687 ` 441` ``` (setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n}) / (f\$0)" ``` huffman@29911 ` 442` ``` by (cases n, simp, simp add: divide_inverse fps_inverse_def) ``` chaieb@29687 ` 443` ``` from th0[symmetric, unfolded nonzero_divide_eq_eq[OF f0]] ``` huffman@30488 ` 444` ``` have th1: "setsum (\i. f\$i * natfun_inverse f (n - i)) {1..n} = ``` huffman@30488 ` 445` ``` - (f\$0) * (inverse f)\$n" ``` chaieb@29687 ` 446` ``` by (simp add: ring_simps) ``` huffman@30488 ` 447` ``` have "(f * inverse f) \$ n = (\i = 0..n. f \$i * natfun_inverse f (n - i))" ``` chaieb@29687 ` 448` ``` unfolding fps_mult_nth ifn .. ``` huffman@30488 ` 449` ``` also have "\ = f\$0 * natfun_inverse f n ``` chaieb@29687 ` 450` ``` + (\i = 1..n. f\$i * natfun_inverse f (n-i))" ``` chaieb@29687 ` 451` ``` unfolding setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] ``` chaieb@29687 ` 452` ``` by simp ``` chaieb@29687 ` 453` ``` also have "\ = 0" unfolding th1 ifn by simp ``` chaieb@29687 ` 454` ``` finally have "(inverse f * f)\$n = 0" unfolding c . } ``` chaieb@29687 ` 455` ``` with th0 show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 456` ```qed ``` chaieb@29687 ` 457` chaieb@29687 ` 458` ```lemma fps_inverse_0_iff[simp]: "(inverse f)\$0 = (0::'a::division_ring) \ f\$0 = 0" ``` huffman@29911 ` 459` ``` by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) ``` chaieb@29687 ` 460` chaieb@29687 ` 461` ```lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \ f \$0 = 0" ``` chaieb@29687 ` 462` ```proof- ``` chaieb@29687 ` 463` ``` {assume "f\$0 = 0" hence "inverse f = 0" by (simp add: fps_inverse_def)} ``` chaieb@29687 ` 464` ``` moreover ``` chaieb@29687 ` 465` ``` {assume h: "inverse f = 0" and c: "f \$0 \ 0" ``` chaieb@29687 ` 466` ``` from inverse_mult_eq_1[OF c] h have False by simp} ``` chaieb@29687 ` 467` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 468` ```qed ``` chaieb@29687 ` 469` chaieb@29687 ` 470` ```lemma fps_inverse_idempotent[intro]: assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 471` ``` shows "inverse (inverse f) = f" ``` chaieb@29687 ` 472` ```proof- ``` chaieb@29687 ` 473` ``` from f0 have if0: "inverse f \$ 0 \ 0" by simp ``` huffman@30488 ` 474` ``` from inverse_mult_eq_1[OF f0] inverse_mult_eq_1[OF if0] ``` chaieb@29687 ` 475` ``` have th0: "inverse f * f = inverse f * inverse (inverse f)" by (simp add: mult_ac) ``` chaieb@29687 ` 476` ``` then show ?thesis using f0 unfolding mult_cancel_left by simp ``` chaieb@29687 ` 477` ```qed ``` chaieb@29687 ` 478` huffman@30488 ` 479` ```lemma fps_inverse_unique: assumes f0: "f\$0 \ (0::'a::field)" and fg: "f*g = 1" ``` chaieb@29687 ` 480` ``` shows "inverse f = g" ``` chaieb@29687 ` 481` ```proof- ``` chaieb@29687 ` 482` ``` from inverse_mult_eq_1[OF f0] fg ``` chaieb@29687 ` 483` ``` have th0: "inverse f * f = g * f" by (simp add: mult_ac) ``` chaieb@29687 ` 484` ``` then show ?thesis using f0 unfolding mult_cancel_right ``` huffman@29911 ` 485` ``` by (auto simp add: expand_fps_eq) ``` chaieb@29687 ` 486` ```qed ``` chaieb@29687 ` 487` huffman@30488 ` 488` ```lemma fps_inverse_gp: "inverse (Abs_fps(\n. (1::'a::field))) ``` chaieb@29687 ` 489` ``` = Abs_fps (\n. if n= 0 then 1 else if n=1 then - 1 else 0)" ``` chaieb@29687 ` 490` ``` apply (rule fps_inverse_unique) ``` chaieb@29687 ` 491` ``` apply simp ``` huffman@29911 ` 492` ``` apply (simp add: fps_eq_iff fps_mult_nth) ``` chaieb@29687 ` 493` ```proof(clarsimp) ``` chaieb@29687 ` 494` ``` fix n::nat assume n: "n > 0" ``` chaieb@29687 ` 495` ``` let ?f = "\i. if n = i then (1\'a) else if n - i = 1 then - 1 else 0" ``` chaieb@29687 ` 496` ``` let ?g = "\i. if i = n then 1 else if i=n - 1 then - 1 else 0" ``` chaieb@29687 ` 497` ``` let ?h = "\i. if i=n - 1 then - 1 else 0" ``` huffman@30488 ` 498` ``` have th1: "setsum ?f {0..n} = setsum ?g {0..n}" ``` chaieb@29687 ` 499` ``` by (rule setsum_cong2) auto ``` huffman@30488 ` 500` ``` have th2: "setsum ?g {0..n - 1} = setsum ?h {0..n - 1}" ``` chaieb@29687 ` 501` ``` using n apply - by (rule setsum_cong2) auto ``` chaieb@29687 ` 502` ``` have eq: "{0 .. n} = {0.. n - 1} \ {n}" by auto ``` huffman@30488 ` 503` ``` from n have d: "{0.. n - 1} \ {n} = {}" by auto ``` chaieb@29687 ` 504` ``` have f: "finite {0.. n - 1}" "finite {n}" by auto ``` chaieb@29687 ` 505` ``` show "setsum ?f {0..n} = 0" ``` huffman@30488 ` 506` ``` unfolding th1 ``` chaieb@29687 ` 507` ``` apply (simp add: setsum_Un_disjoint[OF f d, unfolded eq[symmetric]] del: One_nat_def) ``` chaieb@29687 ` 508` ``` unfolding th2 ``` chaieb@29687 ` 509` ``` by(simp add: setsum_delta) ``` chaieb@29687 ` 510` ```qed ``` chaieb@29687 ` 511` huffman@29912 ` 512` ```subsection{* Formal Derivatives, and the MacLaurin theorem around 0*} ``` chaieb@29687 ` 513` chaieb@29687 ` 514` ```definition "fps_deriv f = Abs_fps (\n. of_nat (n + 1) * f \$ (n + 1))" ``` chaieb@29687 ` 515` chaieb@29687 ` 516` ```lemma fps_deriv_nth[simp]: "fps_deriv f \$ n = of_nat (n +1) * f \$ (n+1)" by (simp add: fps_deriv_def) ``` chaieb@29687 ` 517` chaieb@29687 ` 518` ```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 ` 519` ``` unfolding fps_eq_iff fps_add_nth fps_const_mult_left fps_deriv_nth by (simp add: ring_simps) ``` chaieb@29687 ` 520` huffman@30488 ` 521` ```lemma fps_deriv_mult[simp]: ``` chaieb@29687 ` 522` ``` fixes f :: "('a :: comm_ring_1) fps" ``` chaieb@29687 ` 523` ``` shows "fps_deriv (f * g) = f * fps_deriv g + fps_deriv f * g" ``` chaieb@29687 ` 524` ```proof- ``` chaieb@29687 ` 525` ``` let ?D = "fps_deriv" ``` chaieb@29687 ` 526` ``` {fix n::nat ``` chaieb@29687 ` 527` ``` let ?Zn = "{0 ..n}" ``` chaieb@29687 ` 528` ``` let ?Zn1 = "{0 .. n + 1}" ``` chaieb@29687 ` 529` ``` let ?f = "\i. i + 1" ``` chaieb@29687 ` 530` ``` have fi: "inj_on ?f {0..n}" by (simp add: inj_on_def) ``` chaieb@29687 ` 531` ``` have eq: "{1.. n+1} = ?f ` {0..n}" by auto ``` chaieb@29687 ` 532` ``` let ?g = "\i. of_nat (i+1) * g \$ (i+1) * f \$ (n - i) + ``` chaieb@29687 ` 533` ``` of_nat (i+1)* f \$ (i+1) * g \$ (n - i)" ``` chaieb@29687 ` 534` ``` let ?h = "\i. of_nat i * g \$ i * f \$ ((n+1) - i) + ``` chaieb@29687 ` 535` ``` of_nat i* f \$ i * g \$ ((n + 1) - i)" ``` chaieb@29687 ` 536` ``` {fix k assume k: "k \ {0..n}" ``` chaieb@29687 ` 537` ``` have "?h (k + 1) = ?g k" using k by auto} ``` chaieb@29687 ` 538` ``` note th0 = this ``` chaieb@29687 ` 539` ``` have eq': "{0..n +1}- {1 .. n+1} = {0}" by auto ``` chaieb@29687 ` 540` ``` 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 ` 541` ``` apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) ``` chaieb@29687 ` 542` ``` apply (simp add: inj_on_def Ball_def) ``` chaieb@29687 ` 543` ``` apply presburger ``` chaieb@29687 ` 544` ``` apply (rule set_ext) ``` chaieb@29687 ` 545` ``` apply (presburger add: image_iff) ``` chaieb@29687 ` 546` ``` by simp ``` chaieb@29687 ` 547` ``` have s1: "setsum (\i. f \$ i * g \$ (n + 1 - i)) ?Zn1 = setsum (\i. f \$ (n + 1 - i) * g \$ i) ?Zn1" ``` chaieb@29687 ` 548` ``` apply (rule setsum_reindex_cong[where f="\i. n + 1 - i"]) ``` chaieb@29687 ` 549` ``` apply (simp add: inj_on_def Ball_def) ``` chaieb@29687 ` 550` ``` apply presburger ``` chaieb@29687 ` 551` ``` apply (rule set_ext) ``` chaieb@29687 ` 552` ``` apply (presburger add: image_iff) ``` chaieb@29687 ` 553` ``` by simp ``` chaieb@29687 ` 554` ``` have "(f * ?D g + ?D f * g)\$n = (?D g * f + ?D f * g)\$n" by (simp only: mult_commute) ``` chaieb@29687 ` 555` ``` also have "\ = (\i = 0..n. ?g i)" ``` chaieb@29687 ` 556` ``` by (simp add: fps_mult_nth setsum_addf[symmetric]) ``` chaieb@29687 ` 557` ``` also have "\ = setsum ?h {1..n+1}" ``` chaieb@29687 ` 558` ``` using th0 setsum_reindex_cong[OF fi eq, of "?g" "?h"] by auto ``` chaieb@29687 ` 559` ``` also have "\ = setsum ?h {0..n+1}" ``` chaieb@29687 ` 560` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 561` ``` apply simp ``` chaieb@29687 ` 562` ``` apply (simp add: subset_eq) ``` chaieb@29687 ` 563` ``` unfolding eq' ``` chaieb@29687 ` 564` ``` by simp ``` chaieb@29687 ` 565` ``` also have "\ = (fps_deriv (f * g)) \$ n" ``` chaieb@29687 ` 566` ``` apply (simp only: fps_deriv_nth fps_mult_nth setsum_addf) ``` chaieb@29687 ` 567` ``` unfolding s0 s1 ``` chaieb@29687 ` 568` ``` unfolding setsum_addf[symmetric] setsum_right_distrib ``` chaieb@29687 ` 569` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 570` ``` by (auto simp add: of_nat_diff ring_simps) ``` chaieb@29687 ` 571` ``` finally have "(f * ?D g + ?D f * g) \$ n = ?D (f*g) \$ n" .} ``` huffman@30488 ` 572` ``` then show ?thesis unfolding fps_eq_iff by auto ``` chaieb@29687 ` 573` ```qed ``` chaieb@29687 ` 574` chaieb@29687 ` 575` ```lemma fps_deriv_neg[simp]: "fps_deriv (- (f:: ('a:: comm_ring_1) fps)) = - (fps_deriv f)" ``` huffman@29911 ` 576` ``` by (simp add: fps_eq_iff fps_deriv_def) ``` chaieb@29687 ` 577` ```lemma fps_deriv_add[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) + g) = fps_deriv f + fps_deriv g" ``` chaieb@29687 ` 578` ``` using fps_deriv_linear[of 1 f 1 g] by simp ``` chaieb@29687 ` 579` chaieb@29687 ` 580` ```lemma fps_deriv_sub[simp]: "fps_deriv ((f:: ('a::comm_ring_1) fps) - g) = fps_deriv f - fps_deriv g" ``` huffman@30488 ` 581` ``` unfolding diff_minus by simp ``` chaieb@29687 ` 582` chaieb@29687 ` 583` ```lemma fps_deriv_const[simp]: "fps_deriv (fps_const c) = 0" ``` huffman@29911 ` 584` ``` by (simp add: fps_ext fps_deriv_def fps_const_def) ``` chaieb@29687 ` 585` chaieb@29687 ` 586` ```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 ` 587` ``` by simp ``` chaieb@29687 ` 588` chaieb@29687 ` 589` ```lemma fps_deriv_0[simp]: "fps_deriv 0 = 0" ``` chaieb@29687 ` 590` ``` by (simp add: fps_deriv_def fps_eq_iff) ``` chaieb@29687 ` 591` chaieb@29687 ` 592` ```lemma fps_deriv_1[simp]: "fps_deriv 1 = 0" ``` chaieb@29687 ` 593` ``` by (simp add: fps_deriv_def fps_eq_iff ) ``` chaieb@29687 ` 594` chaieb@29687 ` 595` ```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 ` 596` ``` by simp ``` chaieb@29687 ` 597` chaieb@29687 ` 598` ```lemma fps_deriv_setsum: "fps_deriv (setsum f S) = setsum (\i. fps_deriv (f i :: ('a::comm_ring_1) fps)) S" ``` chaieb@29687 ` 599` ```proof- ``` chaieb@29687 ` 600` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 601` ``` moreover ``` chaieb@29687 ` 602` ``` {assume fS: "finite S" ``` chaieb@29687 ` 603` ``` have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} ``` chaieb@29687 ` 604` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 605` ```qed ``` chaieb@29687 ` 606` chaieb@29687 ` 607` ```lemma fps_deriv_eq_0_iff[simp]: "fps_deriv f = 0 \ (f = fps_const (f\$0 :: 'a::{idom,semiring_char_0}))" ``` chaieb@29687 ` 608` ```proof- ``` chaieb@29687 ` 609` ``` {assume "f= fps_const (f\$0)" hence "fps_deriv f = fps_deriv (fps_const (f\$0))" by simp ``` chaieb@29687 ` 610` ``` hence "fps_deriv f = 0" by simp } ``` chaieb@29687 ` 611` ``` moreover ``` chaieb@29687 ` 612` ``` {assume z: "fps_deriv f = 0" ``` chaieb@29687 ` 613` ``` hence "\n. (fps_deriv f)\$n = 0" by simp ``` chaieb@29687 ` 614` ``` hence "\n. f\$(n+1) = 0" by (simp del: of_nat_Suc of_nat_add One_nat_def) ``` chaieb@29687 ` 615` ``` hence "f = fps_const (f\$0)" ``` chaieb@29687 ` 616` ``` apply (clarsimp simp add: fps_eq_iff fps_const_def) ``` chaieb@29687 ` 617` ``` apply (erule_tac x="n - 1" in allE) ``` chaieb@29687 ` 618` ``` by simp} ``` chaieb@29687 ` 619` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 620` ```qed ``` chaieb@29687 ` 621` huffman@30488 ` 622` ```lemma fps_deriv_eq_iff: ``` chaieb@29687 ` 623` ``` fixes f:: "('a::{idom,semiring_char_0}) fps" ``` chaieb@29687 ` 624` ``` shows "fps_deriv f = fps_deriv g \ (f = fps_const(f\$0 - g\$0) + g)" ``` chaieb@29687 ` 625` ```proof- ``` chaieb@29687 ` 626` ``` have "fps_deriv f = fps_deriv g \ fps_deriv (f - g) = 0" by simp ``` chaieb@29687 ` 627` ``` also have "\ \ f - g = fps_const ((f-g)\$0)" unfolding fps_deriv_eq_0_iff .. ``` chaieb@29687 ` 628` ``` finally show ?thesis by (simp add: ring_simps) ``` chaieb@29687 ` 629` ```qed ``` chaieb@29687 ` 630` chaieb@29687 ` 631` ```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 ` 632` ``` apply auto unfolding fps_deriv_eq_iff by blast ``` huffman@30488 ` 633` chaieb@29687 ` 634` chaieb@29687 ` 635` ```fun fps_nth_deriv :: "nat \ ('a::semiring_1) fps \ 'a fps" where ``` chaieb@29687 ` 636` ``` "fps_nth_deriv 0 f = f" ``` chaieb@29687 ` 637` ```| "fps_nth_deriv (Suc n) f = fps_nth_deriv n (fps_deriv f)" ``` chaieb@29687 ` 638` chaieb@29687 ` 639` ```lemma fps_nth_deriv_commute: "fps_nth_deriv (Suc n) f = fps_deriv (fps_nth_deriv n f)" ``` chaieb@29687 ` 640` ``` by (induct n arbitrary: f, auto) ``` chaieb@29687 ` 641` chaieb@29687 ` 642` ```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 ` 643` ``` by (induct n arbitrary: f g, auto simp add: fps_nth_deriv_commute) ``` chaieb@29687 ` 644` chaieb@29687 ` 645` ```lemma fps_nth_deriv_neg[simp]: "fps_nth_deriv n (- (f:: ('a:: comm_ring_1) fps)) = - (fps_nth_deriv n f)" ``` chaieb@29687 ` 646` ``` by (induct n arbitrary: f, simp_all) ``` chaieb@29687 ` 647` chaieb@29687 ` 648` ```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 ` 649` ``` using fps_nth_deriv_linear[of n 1 f 1 g] by simp ``` chaieb@29687 ` 650` chaieb@29687 ` 651` ```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 ` 652` ``` unfolding diff_minus fps_nth_deriv_add by simp ``` chaieb@29687 ` 653` chaieb@29687 ` 654` ```lemma fps_nth_deriv_0[simp]: "fps_nth_deriv n 0 = 0" ``` chaieb@29687 ` 655` ``` by (induct n, simp_all ) ``` chaieb@29687 ` 656` chaieb@29687 ` 657` ```lemma fps_nth_deriv_1[simp]: "fps_nth_deriv n 1 = (if n = 0 then 1 else 0)" ``` chaieb@29687 ` 658` ``` by (induct n, simp_all ) ``` chaieb@29687 ` 659` chaieb@29687 ` 660` ```lemma fps_nth_deriv_const[simp]: "fps_nth_deriv n (fps_const c) = (if n = 0 then fps_const c else 0)" ``` chaieb@29687 ` 661` ``` by (cases n, simp_all) ``` chaieb@29687 ` 662` chaieb@29687 ` 663` ```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 ` 664` ``` using fps_nth_deriv_linear[of n "c" f 0 0 ] by simp ``` chaieb@29687 ` 665` chaieb@29687 ` 666` ```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 ` 667` ``` using fps_nth_deriv_linear[of n "c" f 0 0] by (simp add: mult_commute) ``` chaieb@29687 ` 668` chaieb@29687 ` 669` ```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 ` 670` ```proof- ``` chaieb@29687 ` 671` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 672` ``` moreover ``` chaieb@29687 ` 673` ``` {assume fS: "finite S" ``` chaieb@29687 ` 674` ``` have ?thesis by (induct rule: finite_induct[OF fS], simp_all)} ``` chaieb@29687 ` 675` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 676` ```qed ``` chaieb@29687 ` 677` chaieb@29687 ` 678` ```lemma fps_deriv_maclauren_0: "(fps_nth_deriv k (f:: ('a::comm_semiring_1) fps)) \$ 0 = of_nat (fact k) * f\$(k)" ``` chaieb@29687 ` 679` ``` by (induct k arbitrary: f) (auto simp add: ring_simps of_nat_mult) ``` chaieb@29687 ` 680` huffman@29906 ` 681` ```subsection {* Powers*} ``` chaieb@29687 ` 682` haftmann@30960 ` 683` ```instance fps :: (semiring_1) recpower .. ``` chaieb@29687 ` 684` chaieb@29687 ` 685` ```lemma fps_power_zeroth_eq_one: "a\$0 =1 \ a^n \$ 0 = (1::'a::semiring_1)" ``` haftmann@30960 ` 686` ``` by (induct n, auto simp add: expand_fps_eq fps_mult_nth) ``` chaieb@29687 ` 687` chaieb@29687 ` 688` ```lemma fps_power_first_eq: "(a:: 'a::comm_ring_1 fps)\$0 =1 \ a^n \$ 1 = of_nat n * a\$1" ``` chaieb@29687 ` 689` ```proof(induct n) ``` haftmann@30960 ` 690` ``` case 0 thus ?case by simp ``` chaieb@29687 ` 691` ```next ``` chaieb@29687 ` 692` ``` case (Suc n) ``` chaieb@29687 ` 693` ``` note h = Suc.hyps[OF `a\$0 = 1`] ``` huffman@30488 ` 694` ``` show ?case unfolding power_Suc fps_mult_nth ``` chaieb@29687 ` 695` ``` using h `a\$0 = 1` fps_power_zeroth_eq_one[OF `a\$0=1`] by (simp add: ring_simps) ``` chaieb@29687 ` 696` ```qed ``` chaieb@29687 ` 697` chaieb@29687 ` 698` ```lemma startsby_one_power:"a \$ 0 = (1::'a::comm_ring_1) \ a^n \$ 0 = 1" ``` haftmann@30960 ` 699` ``` by (induct n, auto simp add: fps_mult_nth) ``` chaieb@29687 ` 700` chaieb@29687 ` 701` ```lemma startsby_zero_power:"a \$0 = (0::'a::comm_ring_1) \ n > 0 \ a^n \$0 = 0" ``` haftmann@30960 ` 702` ``` by (induct n, auto simp add: fps_mult_nth) ``` chaieb@29687 ` 703` chaieb@29687 ` 704` ```lemma startsby_power:"a \$0 = (v::'a::{comm_ring_1, recpower}) \ a^n \$0 = v^n" ``` haftmann@30960 ` 705` ``` by (induct n, auto simp add: fps_mult_nth power_Suc) ``` chaieb@29687 ` 706` chaieb@29687 ` 707` ```lemma startsby_zero_power_iff[simp]: ``` chaieb@29687 ` 708` ``` "a^n \$0 = (0::'a::{idom, recpower}) \ (n \ 0 \ a\$0 = 0)" ``` chaieb@29687 ` 709` ```apply (rule iffI) ``` chaieb@29687 ` 710` ```apply (induct n, auto simp add: power_Suc fps_mult_nth) ``` chaieb@29687 ` 711` ```by (rule startsby_zero_power, simp_all) ``` chaieb@29687 ` 712` huffman@30488 ` 713` ```lemma startsby_zero_power_prefix: ``` chaieb@29687 ` 714` ``` assumes a0: "a \$0 = (0::'a::idom)" ``` chaieb@29687 ` 715` ``` shows "\n < k. a ^ k \$ n = 0" ``` huffman@30488 ` 716` ``` using a0 ``` chaieb@29687 ` 717` ```proof(induct k rule: nat_less_induct) ``` chaieb@29687 ` 718` ``` fix k assume H: "\m (\n'a)" ``` chaieb@29687 ` 719` ``` let ?ths = "\m 0" ``` chaieb@29687 ` 728` ``` have "a ^k \$ m = (a^l * a) \$m" by (simp add: k power_Suc mult_commute) ``` chaieb@29687 ` 729` ``` also have "\ = (\i = 0..m. a ^ l \$ i * a \$ (m - i))" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 730` ``` also have "\ = 0" apply (rule setsum_0') ``` chaieb@29687 ` 731` ``` apply auto ``` chaieb@29687 ` 732` ``` apply (case_tac "aa = m") ``` chaieb@29687 ` 733` ``` using a0 ``` chaieb@29687 ` 734` ``` apply simp ``` chaieb@29687 ` 735` ``` apply (rule H[rule_format]) ``` huffman@30488 ` 736` ``` using a0 k mk by auto ``` chaieb@29687 ` 737` ``` finally have "a^k \$ m = 0" .} ``` chaieb@29687 ` 738` ``` ultimately have "a^k \$ m = 0" by blast} ``` chaieb@29687 ` 739` ``` hence ?ths by blast} ``` chaieb@29687 ` 740` ``` ultimately show ?ths by (cases k, auto) ``` chaieb@29687 ` 741` ```qed ``` chaieb@29687 ` 742` huffman@30488 ` 743` ```lemma startsby_zero_setsum_depends: ``` chaieb@29687 ` 744` ``` assumes a0: "a \$0 = (0::'a::idom)" and kn: "n \ k" ``` chaieb@29687 ` 745` ``` shows "setsum (\i. (a ^ i)\$k) {0 .. n} = setsum (\i. (a ^ i)\$k) {0 .. k}" ``` chaieb@29687 ` 746` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 747` ``` using kn apply auto ``` chaieb@29687 ` 748` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` chaieb@29687 ` 749` ``` by arith ``` chaieb@29687 ` 750` chaieb@29687 ` 751` ```lemma startsby_zero_power_nth_same: assumes a0: "a\$0 = (0::'a::{recpower, idom})" ``` chaieb@29687 ` 752` ``` shows "a^n \$ n = (a\$1) ^ n" ``` chaieb@29687 ` 753` ```proof(induct n) ``` chaieb@29687 ` 754` ``` case 0 thus ?case by (simp add: power_0) ``` chaieb@29687 ` 755` ```next ``` chaieb@29687 ` 756` ``` case (Suc n) ``` chaieb@29687 ` 757` ``` have "a ^ Suc n \$ (Suc n) = (a^n * a)\$(Suc n)" by (simp add: ring_simps power_Suc) ``` chaieb@29687 ` 758` ``` also have "\ = setsum (\i. a^n\$i * a \$ (Suc n - i)) {0.. Suc n}" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 759` ``` also have "\ = setsum (\i. a^n\$i * a \$ (Suc n - i)) {n .. Suc n}" ``` chaieb@29687 ` 760` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 761` ``` apply simp ``` chaieb@29687 ` 762` ``` apply clarsimp ``` chaieb@29687 ` 763` ``` apply clarsimp ``` chaieb@29687 ` 764` ``` apply (rule startsby_zero_power_prefix[rule_format, OF a0]) ``` chaieb@29687 ` 765` ``` apply arith ``` chaieb@29687 ` 766` ``` done ``` chaieb@29687 ` 767` ``` also have "\ = a^n \$ n * a\$1" using a0 by simp ``` chaieb@29687 ` 768` ``` finally show ?case using Suc.hyps by (simp add: power_Suc) ``` chaieb@29687 ` 769` ```qed ``` chaieb@29687 ` 770` chaieb@29687 ` 771` ```lemma fps_inverse_power: ``` chaieb@29687 ` 772` ``` fixes a :: "('a::{field, recpower}) fps" ``` chaieb@29687 ` 773` ``` shows "inverse (a^n) = inverse a ^ n" ``` chaieb@29687 ` 774` ```proof- ``` chaieb@29687 ` 775` ``` {assume a0: "a\$0 = 0" ``` chaieb@29687 ` 776` ``` hence eq: "inverse a = 0" by (simp add: fps_inverse_def) ``` chaieb@29687 ` 777` ``` {assume "n = 0" hence ?thesis by simp} ``` chaieb@29687 ` 778` ``` moreover ``` chaieb@29687 ` 779` ``` {assume n: "n > 0" ``` huffman@30488 ` 780` ``` from startsby_zero_power[OF a0 n] eq a0 n have ?thesis ``` chaieb@29687 ` 781` ``` by (simp add: fps_inverse_def)} ``` chaieb@29687 ` 782` ``` ultimately have ?thesis by blast} ``` chaieb@29687 ` 783` ``` moreover ``` chaieb@29687 ` 784` ``` {assume a0: "a\$0 \ 0" ``` chaieb@29687 ` 785` ``` have ?thesis ``` chaieb@29687 ` 786` ``` apply (rule fps_inverse_unique) ``` chaieb@29687 ` 787` ``` apply (simp add: a0) ``` chaieb@29687 ` 788` ``` unfolding power_mult_distrib[symmetric] ``` chaieb@29687 ` 789` ``` apply (rule ssubst[where t = "a * inverse a" and s= 1]) ``` chaieb@29687 ` 790` ``` apply simp_all ``` chaieb@29687 ` 791` ``` apply (subst mult_commute) ``` chaieb@29687 ` 792` ``` by (rule inverse_mult_eq_1[OF a0])} ``` chaieb@29687 ` 793` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 794` ```qed ``` chaieb@29687 ` 795` chaieb@29687 ` 796` ```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 ` 797` ``` apply (induct n, auto simp add: power_Suc ring_simps fps_const_add[symmetric] simp del: fps_const_add) ``` chaieb@29687 ` 798` ``` by (case_tac n, auto simp add: power_Suc ring_simps) ``` chaieb@29687 ` 799` huffman@30488 ` 800` ```lemma fps_inverse_deriv: ``` chaieb@29687 ` 801` ``` fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 802` ``` assumes a0: "a\$0 \ 0" ``` chaieb@29687 ` 803` ``` shows "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" ``` chaieb@29687 ` 804` ```proof- ``` chaieb@29687 ` 805` ``` from inverse_mult_eq_1[OF a0] ``` chaieb@29687 ` 806` ``` have "fps_deriv (inverse a * a) = 0" by simp ``` chaieb@29687 ` 807` ``` hence "inverse a * fps_deriv a + fps_deriv (inverse a) * a = 0" by simp ``` chaieb@29687 ` 808` ``` hence "inverse a * (inverse a * fps_deriv a + fps_deriv (inverse a) * a) = 0" by simp ``` chaieb@29687 ` 809` ``` with inverse_mult_eq_1[OF a0] ``` chaieb@29687 ` 810` ``` have "inverse a ^ 2 * fps_deriv a + fps_deriv (inverse a) = 0" ``` chaieb@29687 ` 811` ``` unfolding power2_eq_square ``` chaieb@29687 ` 812` ``` apply (simp add: ring_simps) ``` chaieb@29687 ` 813` ``` by (simp add: mult_assoc[symmetric]) ``` chaieb@29687 ` 814` ``` 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 ` 815` ``` by simp ``` chaieb@29687 ` 816` ``` then show "fps_deriv (inverse a) = - fps_deriv a * inverse a ^ 2" by (simp add: ring_simps) ``` chaieb@29687 ` 817` ```qed ``` chaieb@29687 ` 818` huffman@30488 ` 819` ```lemma fps_inverse_mult: ``` chaieb@29687 ` 820` ``` fixes a::"('a :: field) fps" ``` chaieb@29687 ` 821` ``` shows "inverse (a * b) = inverse a * inverse b" ``` chaieb@29687 ` 822` ```proof- ``` chaieb@29687 ` 823` ``` {assume a0: "a\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 824` ``` from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all ``` chaieb@29687 ` 825` ``` have ?thesis unfolding th by simp} ``` chaieb@29687 ` 826` ``` moreover ``` chaieb@29687 ` 827` ``` {assume b0: "b\$0 = 0" hence ab0: "(a*b)\$0 = 0" by (simp add: fps_mult_nth) ``` chaieb@29687 ` 828` ``` from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all ``` chaieb@29687 ` 829` ``` have ?thesis unfolding th by simp} ``` chaieb@29687 ` 830` ``` moreover ``` chaieb@29687 ` 831` ``` {assume a0: "a\$0 \ 0" and b0: "b\$0 \ 0" ``` chaieb@29687 ` 832` ``` from a0 b0 have ab0:"(a*b) \$ 0 \ 0" by (simp add: fps_mult_nth) ``` huffman@30488 ` 833` ``` from inverse_mult_eq_1[OF ab0] ``` chaieb@29687 ` 834` ``` have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp ``` chaieb@29687 ` 835` ``` then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" ``` chaieb@29687 ` 836` ``` by (simp add: ring_simps) ``` chaieb@29687 ` 837` ``` then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp} ``` chaieb@29687 ` 838` ```ultimately show ?thesis by blast ``` chaieb@29687 ` 839` ```qed ``` chaieb@29687 ` 840` huffman@30488 ` 841` ```lemma fps_inverse_deriv': ``` chaieb@29687 ` 842` ``` fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 843` ``` assumes a0: "a\$0 \ 0" ``` chaieb@29687 ` 844` ``` shows "fps_deriv (inverse a) = - fps_deriv a / a ^ 2" ``` chaieb@29687 ` 845` ``` using fps_inverse_deriv[OF a0] ``` chaieb@29687 ` 846` ``` unfolding power2_eq_square fps_divide_def ``` chaieb@29687 ` 847` ``` fps_inverse_mult by simp ``` chaieb@29687 ` 848` chaieb@29687 ` 849` ```lemma inverse_mult_eq_1': assumes f0: "f\$0 \ (0::'a::field)" ``` chaieb@29687 ` 850` ``` shows "f * inverse f= 1" ``` chaieb@29687 ` 851` ``` by (metis mult_commute inverse_mult_eq_1 f0) ``` chaieb@29687 ` 852` chaieb@29687 ` 853` ```lemma fps_divide_deriv: fixes a:: "('a :: field) fps" ``` chaieb@29687 ` 854` ``` assumes a0: "b\$0 \ 0" ``` chaieb@29687 ` 855` ``` shows "fps_deriv (a / b) = (fps_deriv a * b - a * fps_deriv b) / b ^ 2" ``` chaieb@29687 ` 856` ``` using fps_inverse_deriv[OF a0] ``` chaieb@29687 ` 857` ``` by (simp add: fps_divide_def ring_simps power2_eq_square fps_inverse_mult inverse_mult_eq_1'[OF a0]) ``` huffman@30488 ` 858` huffman@29906 ` 859` ```subsection{* The eXtractor series X*} ``` chaieb@29687 ` 860` chaieb@29687 ` 861` ```lemma minus_one_power_iff: "(- (1::'a :: {recpower, comm_ring_1})) ^ n = (if even n then 1 else - 1)" ``` chaieb@29687 ` 862` ``` by (induct n, auto) ``` chaieb@29687 ` 863` chaieb@29687 ` 864` ```definition "X = Abs_fps (\n. if n = 1 then 1 else 0)" ``` chaieb@29687 ` 865` huffman@30488 ` 866` ```lemma fps_inverse_gp': "inverse (Abs_fps(\n. (1::'a::field))) ``` chaieb@29687 ` 867` ``` = 1 - X" ``` huffman@29911 ` 868` ``` by (simp add: fps_inverse_gp fps_eq_iff X_def) ``` chaieb@29687 ` 869` chaieb@29687 ` 870` ```lemma X_mult_nth[simp]: "(X * (f :: ('a::semiring_1) fps)) \$n = (if n = 0 then 0 else f \$ (n - 1))" ``` chaieb@29687 ` 871` ```proof- ``` chaieb@29687 ` 872` ``` {assume n: "n \ 0" ``` chaieb@29687 ` 873` ``` have fN: "finite {0 .. n}" by simp ``` chaieb@29687 ` 874` ``` have "(X * f) \$n = (\i = 0..n. X \$ i * f \$ (n - i))" by (simp add: fps_mult_nth) ``` huffman@29913 ` 875` ``` also have "\ = f \$ (n - 1)" ``` huffman@29913 ` 876` ``` using n by (simp add: X_def mult_delta_left setsum_delta [OF fN]) ``` chaieb@29687 ` 877` ``` finally have ?thesis using n by simp } ``` chaieb@29687 ` 878` ``` moreover ``` chaieb@29687 ` 879` ``` {assume n: "n=0" hence ?thesis by (simp add: fps_mult_nth X_def)} ``` chaieb@29687 ` 880` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 881` ```qed ``` chaieb@29687 ` 882` chaieb@29687 ` 883` ```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 ` 884` ``` by (metis X_mult_nth mult_commute) ``` chaieb@29687 ` 885` chaieb@29687 ` 886` ```lemma X_power_iff: "X^k = Abs_fps (\n. if n = k then (1::'a::comm_ring_1) else 0)" ``` chaieb@29687 ` 887` ```proof(induct k) ``` haftmann@30960 ` 888` ``` case 0 thus ?case by (simp add: X_def fps_eq_iff) ``` chaieb@29687 ` 889` ```next ``` chaieb@29687 ` 890` ``` case (Suc k) ``` huffman@30488 ` 891` ``` {fix m ``` chaieb@29687 ` 892` ``` have "(X^Suc k) \$ m = (if m = 0 then (0::'a) else (X^k) \$ (m - 1))" ``` chaieb@29687 ` 893` ``` by (simp add: power_Suc del: One_nat_def) ``` chaieb@29687 ` 894` ``` then have "(X^Suc k) \$ m = (if m = Suc k then (1::'a) else 0)" ``` chaieb@29687 ` 895` ``` using Suc.hyps by (auto cong del: if_weak_cong)} ``` chaieb@29687 ` 896` ``` then show ?case by (simp add: fps_eq_iff) ``` chaieb@29687 ` 897` ```qed ``` chaieb@29687 ` 898` chaieb@29687 ` 899` ```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 ` 900` ``` apply (induct k arbitrary: n) ``` chaieb@29687 ` 901` ``` apply (simp) ``` huffman@30488 ` 902` ``` unfolding power_Suc mult_assoc ``` chaieb@29687 ` 903` ``` by (case_tac n, auto) ``` chaieb@29687 ` 904` chaieb@29687 ` 905` ```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 ` 906` ``` by (metis X_power_mult_nth mult_commute) ``` chaieb@29687 ` 907` ```lemma fps_deriv_X[simp]: "fps_deriv X = 1" ``` chaieb@29687 ` 908` ``` by (simp add: fps_deriv_def X_def fps_eq_iff) ``` chaieb@29687 ` 909` chaieb@29687 ` 910` ```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 ` 911` ``` by (cases "n", simp_all) ``` chaieb@29687 ` 912` chaieb@29687 ` 913` ```lemma X_nth[simp]: "X\$n = (if n = 1 then 1 else 0)" by (simp add: X_def) ``` chaieb@29687 ` 914` ```lemma X_power_nth[simp]: "(X^k) \$n = (if n = k then 1 else (0::'a::comm_ring_1))" ``` chaieb@29687 ` 915` ``` by (simp add: X_power_iff) ``` chaieb@29687 ` 916` chaieb@29687 ` 917` ```lemma fps_inverse_X_plus1: ``` chaieb@29687 ` 918` ``` "inverse (1 + X) = Abs_fps (\n. (- (1::'a::{recpower, field})) ^ n)" (is "_ = ?r") ``` chaieb@29687 ` 919` ```proof- ``` chaieb@29687 ` 920` ``` have eq: "(1 + X) * ?r = 1" ``` chaieb@29687 ` 921` ``` unfolding minus_one_power_iff ``` chaieb@29687 ` 922` ``` apply (auto simp add: ring_simps fps_eq_iff) ``` chaieb@29687 ` 923` ``` by presburger+ ``` chaieb@29687 ` 924` ``` show ?thesis by (auto simp add: eq intro: fps_inverse_unique) ``` chaieb@29687 ` 925` ```qed ``` chaieb@29687 ` 926` huffman@30488 ` 927` huffman@29906 ` 928` ```subsection{* Integration *} ``` chaieb@29687 ` 929` ```definition "fps_integral a a0 = Abs_fps (\n. if n = 0 then a0 else (a\$(n - 1) / of_nat n))" ``` chaieb@29687 ` 930` chaieb@29687 ` 931` ```lemma fps_deriv_fps_integral: "fps_deriv (fps_integral a (a0 :: 'a :: {field, ring_char_0})) = a" ``` chaieb@29687 ` 932` ``` by (simp add: fps_integral_def fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) ``` chaieb@29687 ` 933` chaieb@29687 ` 934` ```lemma fps_integral_linear: "fps_integral (fps_const (a::'a::{field, ring_char_0}) * f + fps_const b * g) (a*a0 + b*b0) = fps_const a * fps_integral f a0 + fps_const b * fps_integral g b0" (is "?l = ?r") ``` chaieb@29687 ` 935` ```proof- ``` chaieb@29687 ` 936` ``` have "fps_deriv ?l = fps_deriv ?r" by (simp add: fps_deriv_fps_integral) ``` chaieb@29687 ` 937` ``` moreover have "?l\$0 = ?r\$0" by (simp add: fps_integral_def) ``` chaieb@29687 ` 938` ``` ultimately show ?thesis ``` chaieb@29687 ` 939` ``` unfolding fps_deriv_eq_iff by auto ``` chaieb@29687 ` 940` ```qed ``` huffman@30488 ` 941` huffman@29906 ` 942` ```subsection {* Composition of FPSs *} ``` chaieb@29687 ` 943` ```definition fps_compose :: "('a::semiring_1) fps \ 'a fps \ 'a fps" (infixl "oo" 55) where ``` chaieb@29687 ` 944` ``` fps_compose_def: "a oo b = Abs_fps (\n. setsum (\i. a\$i * (b^i\$n)) {0..n})" ``` chaieb@29687 ` 945` chaieb@29687 ` 946` ```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 ` 947` chaieb@29687 ` 948` ```lemma fps_compose_X[simp]: "a oo X = (a :: ('a :: comm_ring_1) fps)" ``` huffman@29913 ` 949` ``` by (simp add: fps_ext fps_compose_def mult_delta_right setsum_delta') ``` huffman@30488 ` 950` huffman@30488 ` 951` ```lemma fps_const_compose[simp]: ``` chaieb@29687 ` 952` ``` "fps_const (a::'a::{comm_ring_1}) oo b = fps_const (a)" ``` huffman@29913 ` 953` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 954` chaieb@29687 ` 955` ```lemma X_fps_compose_startby0[simp]: "a\$0 = 0 \ X oo a = (a :: ('a :: comm_ring_1) fps)" ``` huffman@29913 ` 956` ``` by (simp add: fps_eq_iff fps_compose_def mult_delta_left setsum_delta ``` huffman@29913 ` 957` ``` power_Suc not_le) ``` chaieb@29687 ` 958` chaieb@29687 ` 959` huffman@29906 ` 960` ```subsection {* Rules from Herbert Wilf's Generatingfunctionology*} ``` chaieb@29687 ` 961` huffman@29906 ` 962` ```subsubsection {* Rule 1 *} ``` chaieb@29687 ` 963` ``` (* {a_{n+k}}_0^infty Corresponds to (f - setsum (\i. a_i * x^i))/x^h, for h>0*) ``` chaieb@29687 ` 964` huffman@30488 ` 965` ```lemma fps_power_mult_eq_shift: ``` chaieb@29687 ` 966` ``` "X^Suc k * Abs_fps (\n. a (n + Suc k)) = Abs_fps a - setsum (\i. fps_const (a i :: 'a:: field) * X^i) {0 .. k}" (is "?lhs = ?rhs") ``` chaieb@29687 ` 967` ```proof- ``` chaieb@29687 ` 968` ``` {fix n:: nat ``` huffman@30488 ` 969` ``` have "?lhs \$ n = (if n < Suc k then 0 else a n)" ``` chaieb@29687 ` 970` ``` unfolding X_power_mult_nth by auto ``` chaieb@29687 ` 971` ``` also have "\ = ?rhs \$ n" ``` chaieb@29687 ` 972` ``` proof(induct k) ``` chaieb@29687 ` 973` ``` case 0 thus ?case by (simp add: fps_setsum_nth power_Suc) ``` chaieb@29687 ` 974` ``` next ``` chaieb@29687 ` 975` ``` case (Suc k) ``` chaieb@29687 ` 976` ``` note th = Suc.hyps[symmetric] ``` chaieb@29687 ` 977` ``` have "(Abs_fps a - setsum (\i. fps_const (a i :: 'a:: field) * X^i) {0 .. Suc k})\$n = (Abs_fps a - setsum (\i. fps_const (a i :: 'a:: field) * X^i) {0 .. k} - fps_const (a (Suc k)) * X^ Suc k) \$ n" by (simp add: ring_simps) ``` chaieb@29687 ` 978` ``` also have "\ = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)\$n" ``` huffman@30488 ` 979` ``` using th ``` chaieb@29687 ` 980` ``` unfolding fps_sub_nth by simp ``` chaieb@29687 ` 981` ``` also have "\ = (if n < Suc (Suc k) then 0 else a n)" ``` chaieb@29687 ` 982` ``` unfolding X_power_mult_right_nth ``` chaieb@29687 ` 983` ``` apply (auto simp add: not_less fps_const_def) ``` chaieb@29687 ` 984` ``` apply (rule cong[of a a, OF refl]) ``` chaieb@29687 ` 985` ``` by arith ``` chaieb@29687 ` 986` ``` finally show ?case by simp ``` chaieb@29687 ` 987` ``` qed ``` chaieb@29687 ` 988` ``` finally have "?lhs \$ n = ?rhs \$ n" .} ``` chaieb@29687 ` 989` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 990` ```qed ``` chaieb@29687 ` 991` huffman@29906 ` 992` ```subsubsection{* Rule 2*} ``` chaieb@29687 ` 993` chaieb@29687 ` 994` ``` (* We can not reach the form of Wilf, but still near to it using rewrite rules*) ``` huffman@30488 ` 995` ``` (* If f reprents {a_n} and P is a polynomial, then ``` chaieb@29687 ` 996` ``` P(xD) f represents {P(n) a_n}*) ``` chaieb@29687 ` 997` chaieb@29687 ` 998` ```definition "XD = op * X o fps_deriv" ``` chaieb@29687 ` 999` chaieb@29687 ` 1000` ```lemma XD_add[simp]:"XD (a + b) = XD a + XD (b :: ('a::comm_ring_1) fps)" ``` chaieb@29687 ` 1001` ``` by (simp add: XD_def ring_simps) ``` chaieb@29687 ` 1002` chaieb@29687 ` 1003` ```lemma XD_mult_const[simp]:"XD (fps_const (c::'a::comm_ring_1) * a) = fps_const c * XD a" ``` chaieb@29687 ` 1004` ``` by (simp add: XD_def ring_simps) ``` chaieb@29687 ` 1005` chaieb@29687 ` 1006` ```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 ` 1007` ``` by simp ``` chaieb@29687 ` 1008` haftmann@30952 ` 1009` ```lemma XDN_linear: ``` haftmann@30952 ` 1010` ``` "(XD o^ n) (fps_const c * a + fps_const d * b) = fps_const c * (XD o^ n) a + fps_const d * (XD o^ n) (b :: ('a::comm_ring_1) fps)" ``` chaieb@29687 ` 1011` ``` by (induct n, simp_all) ``` chaieb@29687 ` 1012` chaieb@29687 ` 1013` ```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 ` 1014` haftmann@30952 ` 1015` ```lemma fps_mult_XD_shift: ``` haftmann@30952 ` 1016` ``` "(XD o^ k) (a:: ('a::{comm_ring_1, recpower, ring_char_0}) fps) = Abs_fps (\n. (of_nat n ^ k) * a\$n)" ``` haftmann@30952 ` 1017` ``` by (induct k arbitrary: a) (simp_all add: power_Suc XD_def fps_eq_iff ring_simps del: One_nat_def) ``` chaieb@29687 ` 1018` huffman@29906 ` 1019` ```subsubsection{* Rule 3 is trivial and is given by @{text fps_times_def}*} ``` huffman@29906 ` 1020` ```subsubsection{* Rule 5 --- summation and "division" by (1 - X)*} ``` chaieb@29687 ` 1021` chaieb@29687 ` 1022` ```lemma fps_divide_X_minus1_setsum_lemma: ``` chaieb@29687 ` 1023` ``` "a = ((1::('a::comm_ring_1) fps) - X) * Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1024` ```proof- ``` chaieb@29687 ` 1025` ``` let ?X = "X::('a::comm_ring_1) fps" ``` chaieb@29687 ` 1026` ``` let ?sa = "Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1027` ``` 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 ` 1028` ``` {fix n:: nat ``` huffman@30488 ` 1029` ``` {assume "n=0" hence "a\$n = ((1 - ?X) * ?sa) \$ n" ``` chaieb@29687 ` 1030` ``` by (simp add: fps_mult_nth)} ``` chaieb@29687 ` 1031` ``` moreover ``` chaieb@29687 ` 1032` ``` {assume n0: "n \ 0" ``` chaieb@29687 ` 1033` ``` then have u: "{0} \ ({1} \ {2..n}) = {0..n}" "{1}\{2..n} = {1..n}" ``` chaieb@29687 ` 1034` ``` "{0..n - 1}\{n} = {0..n}" ``` chaieb@29687 ` 1035` ``` apply (simp_all add: expand_set_eq) by presburger+ ``` huffman@30488 ` 1036` ``` have d: "{0} \ ({1} \ {2..n}) = {}" "{1} \ {2..n} = {}" ``` chaieb@29687 ` 1037` ``` "{0..n - 1}\{n} ={}" using n0 ``` chaieb@29687 ` 1038` ``` by (simp_all add: expand_set_eq, presburger+) ``` huffman@30488 ` 1039` ``` have f: "finite {0}" "finite {1}" "finite {2 .. n}" ``` huffman@30488 ` 1040` ``` "finite {0 .. n - 1}" "finite {n}" by simp_all ``` chaieb@29687 ` 1041` ``` have "((1 - ?X) * ?sa) \$ n = setsum (\i. (1 - ?X)\$ i * ?sa \$ (n - i)) {0 .. n}" ``` chaieb@29687 ` 1042` ``` by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1043` ``` also have "\ = a\$n" unfolding th0 ``` chaieb@29687 ` 1044` ``` unfolding setsum_Un_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] ``` chaieb@29687 ` 1045` ``` unfolding setsum_Un_disjoint[OF f(2) f(3) d(2)] ``` chaieb@29687 ` 1046` ``` apply (simp) ``` chaieb@29687 ` 1047` ``` unfolding setsum_Un_disjoint[OF f(4,5) d(3), unfolded u(3)] ``` chaieb@29687 ` 1048` ``` by simp ``` chaieb@29687 ` 1049` ``` finally have "a\$n = ((1 - ?X) * ?sa) \$ n" by simp} ``` chaieb@29687 ` 1050` ``` ultimately have "a\$n = ((1 - ?X) * ?sa) \$ n" by blast} ``` huffman@30488 ` 1051` ```then show ?thesis ``` chaieb@29687 ` 1052` ``` unfolding fps_eq_iff by blast ``` chaieb@29687 ` 1053` ```qed ``` chaieb@29687 ` 1054` chaieb@29687 ` 1055` ```lemma fps_divide_X_minus1_setsum: ``` chaieb@29687 ` 1056` ``` "a /((1::('a::field) fps) - X) = Abs_fps (\n. setsum (\i. a \$ i) {0..n})" ``` chaieb@29687 ` 1057` ```proof- ``` chaieb@29687 ` 1058` ``` let ?X = "1 - (X::('a::field) fps)" ``` chaieb@29687 ` 1059` ``` have th0: "?X \$ 0 \ 0" by simp ``` chaieb@29687 ` 1060` ``` have "a /?X = ?X * Abs_fps (\n\nat. setsum (op \$ a) {0..n}) * inverse ?X" ``` chaieb@29687 ` 1061` ``` using fps_divide_X_minus1_setsum_lemma[of a, symmetric] th0 ``` chaieb@29687 ` 1062` ``` by (simp add: fps_divide_def mult_assoc) ``` chaieb@29687 ` 1063` ``` also have "\ = (inverse ?X * ?X) * Abs_fps (\n\nat. setsum (op \$ a) {0..n}) " ``` chaieb@29687 ` 1064` ``` by (simp add: mult_ac) ``` chaieb@29687 ` 1065` ``` finally show ?thesis by (simp add: inverse_mult_eq_1[OF th0]) ``` chaieb@29687 ` 1066` ```qed ``` chaieb@29687 ` 1067` huffman@30488 ` 1068` ```subsubsection{* Rule 4 in its more general form: generalizes Rule 3 for an arbitrary ``` chaieb@29687 ` 1069` ``` finite product of FPS, also the relvant instance of powers of a FPS*} ``` chaieb@29687 ` 1070` chaieb@29687 ` 1071` ```definition "natpermute n k = {l:: nat list. length l = k \ foldl op + 0 l = n}" ``` chaieb@29687 ` 1072` chaieb@29687 ` 1073` ```lemma natlist_trivial_1: "natpermute n 1 = {[n]}" ``` chaieb@29687 ` 1074` ``` apply (auto simp add: natpermute_def) ``` chaieb@29687 ` 1075` ``` apply (case_tac x, auto) ``` chaieb@29687 ` 1076` ``` done ``` chaieb@29687 ` 1077` huffman@30488 ` 1078` ```lemma foldl_add_start0: ``` chaieb@29687 ` 1079` ``` "foldl op + x xs = x + foldl op + (0::nat) xs" ``` chaieb@29687 ` 1080` ``` apply (induct xs arbitrary: x) ``` chaieb@29687 ` 1081` ``` apply simp ``` chaieb@29687 ` 1082` ``` unfolding foldl.simps ``` chaieb@29687 ` 1083` ``` apply atomize ``` chaieb@29687 ` 1084` ``` apply (subgoal_tac "\x\nat. foldl op + x xs = x + foldl op + (0\nat) xs") ``` chaieb@29687 ` 1085` ``` apply (erule_tac x="x + a" in allE) ``` chaieb@29687 ` 1086` ``` apply (erule_tac x="a" in allE) ``` chaieb@29687 ` 1087` ``` apply simp ``` chaieb@29687 ` 1088` ``` apply assumption ``` chaieb@29687 ` 1089` ``` done ``` chaieb@29687 ` 1090` chaieb@29687 ` 1091` ```lemma foldl_add_append: "foldl op + (x::nat) (xs@ys) = foldl op + x xs + foldl op + 0 ys" ``` chaieb@29687 ` 1092` ``` apply (induct ys arbitrary: x xs) ``` chaieb@29687 ` 1093` ``` apply auto ``` chaieb@29687 ` 1094` ``` apply (subst (2) foldl_add_start0) ``` chaieb@29687 ` 1095` ``` apply simp ``` chaieb@29687 ` 1096` ``` apply (subst (2) foldl_add_start0) ``` chaieb@29687 ` 1097` ``` by simp ``` chaieb@29687 ` 1098` chaieb@29687 ` 1099` ```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 ` 1123` ```proof- ``` chaieb@29687 ` 1124` ``` {from h have "foldl op + 0 (xs@ ys) = n" by (simp add: natpermute_def) ``` chaieb@29687 ` 1125` ``` hence "foldl op + 0 xs + foldl op + 0 ys = n" unfolding foldl_add_append .} ``` chaieb@29687 ` 1126` ``` note th = this ``` chaieb@29687 ` 1127` ``` {from th show "foldl op + 0 xs \ n" by simp} ``` chaieb@29687 ` 1128` ``` {from th show "foldl op + 0 ys \ n" by simp} ``` chaieb@29687 ` 1129` ```qed ``` chaieb@29687 ` 1130` chaieb@29687 ` 1131` ```lemma natpermute_split: ``` chaieb@29687 ` 1132` ``` assumes mn: "h \ k" ``` chaieb@29687 ` 1133` ``` 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 ` 1134` ```proof- ``` huffman@30488 ` 1135` ``` {fix l assume l: "l \ ?R" ``` chaieb@29687 ` 1136` ``` 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 ` 1137` ``` from xs have xs': "foldl op + 0 xs = m" by (simp add: natpermute_def) ``` chaieb@29687 ` 1138` ``` from ys have ys': "foldl op + 0 ys = n - m" by (simp add: natpermute_def) ``` huffman@30488 ` 1139` ``` have "l \ ?L" using leq xs ys h ``` chaieb@29687 ` 1140` ``` apply simp ``` chaieb@29687 ` 1141` ``` apply (clarsimp simp add: natpermute_def simp del: foldl_append) ``` chaieb@29687 ` 1142` ``` apply (simp add: foldl_add_append[unfolded foldl_append]) ``` chaieb@29687 ` 1143` ``` unfolding xs' ys' ``` huffman@30488 ` 1144` ``` using mn xs ys ``` chaieb@29687 ` 1145` ``` unfolding natpermute_def by simp} ``` chaieb@29687 ` 1146` ``` moreover ``` chaieb@29687 ` 1147` ``` {fix l assume l: "l \ natpermute n k" ``` chaieb@29687 ` 1148` ``` let ?xs = "take h l" ``` chaieb@29687 ` 1149` ``` let ?ys = "drop h l" ``` chaieb@29687 ` 1150` ``` let ?m = "foldl op + 0 ?xs" ``` chaieb@29687 ` 1151` ``` from l have ls: "foldl op + 0 (?xs @ ?ys) = n" by (simp add: natpermute_def) ``` huffman@30488 ` 1152` ``` have xs: "?xs \ natpermute ?m h" using l mn by (simp add: natpermute_def) ``` chaieb@29687 ` 1153` ``` have ys: "?ys \ natpermute (n - ?m) (k - h)" using l mn ls[unfolded foldl_add_append] ``` chaieb@29687 ` 1154` ``` by (simp add: natpermute_def) ``` chaieb@29687 ` 1155` ``` from ls have m: "?m \ {0..n}" unfolding foldl_add_append by simp ``` huffman@30488 ` 1156` ``` from xs ys ls have "l \ ?R" ``` chaieb@29687 ` 1157` ``` apply auto ``` chaieb@29687 ` 1158` ``` apply (rule bexI[where x = "?m"]) ``` chaieb@29687 ` 1159` ``` apply (rule exI[where x = "?xs"]) ``` chaieb@29687 ` 1160` ``` apply (rule exI[where x = "?ys"]) ``` huffman@30488 ` 1161` ``` using ls l unfolding foldl_add_append ``` chaieb@29687 ` 1162` ``` by (auto simp add: natpermute_def)} ``` chaieb@29687 ` 1163` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1164` ```qed ``` chaieb@29687 ` 1165` chaieb@29687 ` 1166` ```lemma natpermute_0: "natpermute n 0 = (if n = 0 then {[]} else {})" ``` chaieb@29687 ` 1167` ``` by (auto simp add: natpermute_def) ``` chaieb@29687 ` 1168` ```lemma natpermute_0'[simp]: "natpermute 0 k = (if k = 0 then {[]} else {replicate k 0})" ``` chaieb@29687 ` 1169` ``` apply (auto simp add: set_replicate_conv_if natpermute_def) ``` chaieb@29687 ` 1170` ``` apply (rule nth_equalityI) ``` chaieb@29687 ` 1171` ``` by simp_all ``` chaieb@29687 ` 1172` chaieb@29687 ` 1173` ```lemma natpermute_finite: "finite (natpermute n k)" ``` chaieb@29687 ` 1174` ```proof(induct k arbitrary: n) ``` huffman@30488 ` 1175` ``` case 0 thus ?case ``` chaieb@29687 ` 1176` ``` apply (subst natpermute_split[of 0 0, simplified]) ``` chaieb@29687 ` 1177` ``` by (simp add: natpermute_0) ``` chaieb@29687 ` 1178` ```next ``` chaieb@29687 ` 1179` ``` case (Suc k) ``` chaieb@29687 ` 1180` ``` then show ?case unfolding natpermute_split[of k "Suc k", simplified] ``` chaieb@29687 ` 1181` ``` apply - ``` chaieb@29687 ` 1182` ``` apply (rule finite_UN_I) ``` chaieb@29687 ` 1183` ``` apply simp ``` chaieb@29687 ` 1184` ``` unfolding One_nat_def[symmetric] natlist_trivial_1 ``` chaieb@29687 ` 1185` ``` apply simp ``` chaieb@29687 ` 1186` ``` unfolding image_Collect[symmetric] ``` chaieb@29687 ` 1187` ``` unfolding Collect_def mem_def ``` chaieb@29687 ` 1188` ``` apply (rule finite_imageI) ``` chaieb@29687 ` 1189` ``` apply blast ``` chaieb@29687 ` 1190` ``` done ``` chaieb@29687 ` 1191` ```qed ``` chaieb@29687 ` 1192` chaieb@29687 ` 1193` ```lemma natpermute_contain_maximal: ``` chaieb@29687 ` 1194` ``` "{xs \ natpermute n (k+1). n \ set xs} = UNION {0 .. k} (\i. {(replicate (k+1) 0) [i:=n]})" ``` chaieb@29687 ` 1195` ``` (is "?A = ?B") ``` chaieb@29687 ` 1196` ```proof- ``` chaieb@29687 ` 1197` ``` {fix xs assume H: "xs \ natpermute n (k+1)" and n: "n \ set xs" ``` chaieb@29687 ` 1198` ``` from n obtain i where i: "i \ {0.. k}" "xs!i = n" using H ``` huffman@30488 ` 1199` ``` unfolding in_set_conv_nth by (auto simp add: less_Suc_eq_le natpermute_def) ``` chaieb@29687 ` 1200` ``` have eqs: "({0..k} - {i}) \ {i} = {0..k}" using i by auto ``` chaieb@29687 ` 1201` ``` have f: "finite({0..k} - {i})" "finite {i}" by auto ``` chaieb@29687 ` 1202` ``` have d: "({0..k} - {i}) \ {i} = {}" using i by auto ``` chaieb@29687 ` 1203` ``` from H have "n = setsum (nth xs) {0..k}" apply (simp add: natpermute_def) ``` chaieb@29687 ` 1204` ``` unfolding foldl_add_setsum by (auto simp add: atLeastLessThanSuc_atLeastAtMost) ``` chaieb@29687 ` 1205` ``` also have "\ = n + setsum (nth xs) ({0..k} - {i})" ``` chaieb@29687 ` 1206` ``` unfolding setsum_Un_disjoint[OF f d, unfolded eqs] using i by simp ``` chaieb@29687 ` 1207` ``` finally have zxs: "\ j\ {0..k} - {i}. xs!j = 0" by auto ``` chaieb@29687 ` 1208` ``` from H have xsl: "length xs = k+1" by (simp add: natpermute_def) ``` chaieb@29687 ` 1209` ``` from i have i': "i < length (replicate (k+1) 0)" "i < k+1" ``` chaieb@29687 ` 1210` ``` unfolding length_replicate by arith+ ``` chaieb@29687 ` 1211` ``` have "xs = replicate (k+1) 0 [i := n]" ``` chaieb@29687 ` 1212` ``` apply (rule nth_equalityI) ``` chaieb@29687 ` 1213` ``` unfolding xsl length_list_update length_replicate ``` chaieb@29687 ` 1214` ``` apply simp ``` chaieb@29687 ` 1215` ``` apply clarify ``` chaieb@29687 ` 1216` ``` unfolding nth_list_update[OF i'(1)] ``` chaieb@29687 ` 1217` ``` using i zxs ``` chaieb@29687 ` 1218` ``` by (case_tac "ia=i", auto simp del: replicate.simps) ``` chaieb@29687 ` 1219` ``` then have "xs \ ?B" using i by blast} ``` chaieb@29687 ` 1220` ``` moreover ``` chaieb@29687 ` 1221` ``` {fix i assume i: "i \ {0..k}" ``` chaieb@29687 ` 1222` ``` let ?xs = "replicate (k+1) 0 [i:=n]" ``` chaieb@29687 ` 1223` ``` have nxs: "n \ set ?xs" ``` chaieb@29687 ` 1224` ``` apply (rule set_update_memI) using i by simp ``` chaieb@29687 ` 1225` ``` have xsl: "length ?xs = k+1" by (simp only: length_replicate length_list_update) ``` chaieb@29687 ` 1226` ``` have "foldl op + 0 ?xs = setsum (nth ?xs) {0.. = setsum (\j. if j = i then n else 0) {0..< k+1}" ``` chaieb@29687 ` 1229` ``` apply (rule setsum_cong2) by (simp del: replicate.simps) ``` chaieb@29687 ` 1230` ``` also have "\ = n" using i by (simp add: setsum_delta) ``` huffman@30488 ` 1231` ``` finally ``` chaieb@29687 ` 1232` ``` have "?xs \ natpermute n (k+1)" using xsl unfolding natpermute_def Collect_def mem_def ``` chaieb@29687 ` 1233` ``` by blast ``` chaieb@29687 ` 1234` ``` then have "?xs \ ?A" using nxs by blast} ``` chaieb@29687 ` 1235` ``` ultimately show ?thesis by auto ``` chaieb@29687 ` 1236` ```qed ``` chaieb@29687 ` 1237` huffman@30488 ` 1238` ``` (* The general form *) ``` chaieb@29687 ` 1239` ```lemma fps_setprod_nth: ``` chaieb@29687 ` 1240` ``` fixes m :: nat and a :: "nat \ ('a::comm_ring_1) fps" ``` chaieb@29687 ` 1241` ``` shows "(setprod a {0 .. m})\$n = setsum (\v. setprod (\j. (a j) \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` chaieb@29687 ` 1242` ``` (is "?P m n") ``` chaieb@29687 ` 1243` ```proof(induct m arbitrary: n rule: nat_less_induct) ``` chaieb@29687 ` 1244` ``` fix m n assume H: "\m' < m. \n. ?P m' n" ``` chaieb@29687 ` 1245` ``` {assume m0: "m = 0" ``` chaieb@29687 ` 1246` ``` hence "?P m n" apply simp ``` chaieb@29687 ` 1247` ``` unfolding natlist_trivial_1[where n = n, unfolded One_nat_def] by simp} ``` chaieb@29687 ` 1248` ``` moreover ``` chaieb@29687 ` 1249` ``` {fix k assume k: "m = Suc k" ``` chaieb@29687 ` 1250` ``` have km: "k < m" using k by arith ``` chaieb@29687 ` 1251` ``` have u0: "{0 .. k} \ {m} = {0..m}" using k apply (simp add: expand_set_eq) by presburger ``` chaieb@29687 ` 1252` ``` have f0: "finite {0 .. k}" "finite {m}" by auto ``` chaieb@29687 ` 1253` ``` have d0: "{0 .. k} \ {m} = {}" using k by auto ``` chaieb@29687 ` 1254` ``` have "(setprod a {0 .. m}) \$ n = (setprod a {0 .. k} * a m) \$ n" ``` chaieb@29687 ` 1255` ``` unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0] by simp ``` chaieb@29687 ` 1256` ``` also have "\ = (\i = 0..n. (\v\natpermute i (k + 1). \j\{0..k}. a j \$ v ! j) * a m \$ (n - i))" ``` chaieb@29687 ` 1257` ``` unfolding fps_mult_nth H[rule_format, OF km] .. ``` chaieb@29687 ` 1258` ``` also have "\ = (\v\natpermute n (m + 1). \j\{0..m}. a j \$ v ! j)" ``` chaieb@29687 ` 1259` ``` apply (simp add: k) ``` chaieb@29687 ` 1260` ``` unfolding natpermute_split[of m "m + 1", simplified, of n, unfolded natlist_trivial_1[unfolded One_nat_def] k] ``` chaieb@29687 ` 1261` ``` apply (subst setsum_UN_disjoint) ``` huffman@30488 ` 1262` ``` apply simp ``` chaieb@29687 ` 1263` ``` apply simp ``` chaieb@29687 ` 1264` ``` unfolding image_Collect[symmetric] ``` chaieb@29687 ` 1265` ``` apply clarsimp ``` chaieb@29687 ` 1266` ``` apply (rule finite_imageI) ``` chaieb@29687 ` 1267` ``` apply (rule natpermute_finite) ``` chaieb@29687 ` 1268` ``` apply (clarsimp simp add: expand_set_eq) ``` chaieb@29687 ` 1269` ``` apply auto ``` chaieb@29687 ` 1270` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1271` ``` unfolding setsum_left_distrib ``` chaieb@29687 ` 1272` ``` apply (rule sym) ``` chaieb@29687 ` 1273` ``` apply (rule_tac f="\xs. xs @[n - x]" in setsum_reindex_cong) ``` chaieb@29687 ` 1274` ``` apply (simp add: inj_on_def) ``` chaieb@29687 ` 1275` ``` apply auto ``` chaieb@29687 ` 1276` ``` unfolding setprod_Un_disjoint[OF f0 d0, unfolded u0, unfolded k] ``` chaieb@29687 ` 1277` ``` apply (clarsimp simp add: natpermute_def nth_append) ``` chaieb@29687 ` 1278` ``` done ``` chaieb@29687 ` 1279` ``` finally have "?P m n" .} ``` chaieb@29687 ` 1280` ``` ultimately show "?P m n " by (cases m, auto) ``` chaieb@29687 ` 1281` ```qed ``` chaieb@29687 ` 1282` chaieb@29687 ` 1283` ```text{* The special form for powers *} ``` chaieb@29687 ` 1284` ```lemma fps_power_nth_Suc: ``` chaieb@29687 ` 1285` ``` fixes m :: nat and a :: "('a::comm_ring_1) fps" ``` chaieb@29687 ` 1286` ``` shows "(a ^ Suc m)\$n = setsum (\v. setprod (\j. a \$ (v!j)) {0..m}) (natpermute n (m+1))" ``` chaieb@29687 ` 1287` ```proof- ``` chaieb@29687 ` 1288` ``` have f: "finite {0 ..m}" by simp ``` chaieb@29687 ` 1289` ``` have th0: "a^Suc m = setprod (\i. a) {0..m}" unfolding setprod_constant[OF f, of a] by simp ``` chaieb@29687 ` 1290` ``` show ?thesis unfolding th0 fps_setprod_nth .. ``` chaieb@29687 ` 1291` ```qed ``` chaieb@29687 ` 1292` ```lemma fps_power_nth: ``` chaieb@29687 ` 1293` ``` fixes m :: nat and a :: "('a::comm_ring_1) fps" ``` chaieb@29687 ` 1294` ``` 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 ` 1295` ``` by (cases m, simp_all add: fps_power_nth_Suc del: power_Suc) ``` chaieb@29687 ` 1296` huffman@30488 ` 1297` ```lemma fps_nth_power_0: ``` chaieb@29687 ` 1298` ``` fixes m :: nat and a :: "('a::{comm_ring_1, recpower}) fps" ``` chaieb@29687 ` 1299` ``` shows "(a ^m)\$0 = (a\$0) ^ m" ``` chaieb@29687 ` 1300` ```proof- ``` chaieb@29687 ` 1301` ``` {assume "m=0" hence ?thesis by simp} ``` chaieb@29687 ` 1302` ``` moreover ``` chaieb@29687 ` 1303` ``` {fix n assume m: "m = Suc n" ``` chaieb@29687 ` 1304` ``` have c: "m = card {0..n}" using m by simp ``` chaieb@29687 ` 1305` ``` have "(a ^m)\$0 = setprod (\i. a\$0) {0..n}" ``` nipkow@30837 ` 1306` ``` by (simp add: m fps_power_nth del: replicate.simps power_Suc) ``` chaieb@29687 ` 1307` ``` also have "\ = (a\$0) ^ m" ``` chaieb@29687 ` 1308` ``` unfolding c by (rule setprod_constant, simp) ``` chaieb@29687 ` 1309` ``` finally have ?thesis .} ``` chaieb@29687 ` 1310` ``` ultimately show ?thesis by (cases m, auto) ``` chaieb@29687 ` 1311` ```qed ``` chaieb@29687 ` 1312` huffman@30488 ` 1313` ```lemma fps_compose_inj_right: ``` chaieb@29687 ` 1314` ``` assumes a0: "a\$0 = (0::'a::{recpower,idom})" ``` chaieb@29687 ` 1315` ``` and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1316` ``` shows "(b oo a = c oo a) \ b = c" (is "?lhs \?rhs") ``` chaieb@29687 ` 1317` ```proof- ``` chaieb@29687 ` 1318` ``` {assume ?rhs then have "?lhs" by simp} ``` chaieb@29687 ` 1319` ``` moreover ``` chaieb@29687 ` 1320` ``` {assume h: ?lhs ``` huffman@30488 ` 1321` ``` {fix n have "b\$n = c\$n" ``` chaieb@29687 ` 1322` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1323` ``` fix n assume H: "\m {n} = {0 .. n}" using n1 by auto ``` chaieb@29687 ` 1331` ``` have d: "{0 .. n1} \ {n} = {}" using n1 by auto ``` chaieb@29687 ` 1332` ``` have seq: "(\i = 0..n1. b \$ i * a ^ i \$ n) = (\i = 0..n1. c \$ i * a ^ i \$ n)" ``` chaieb@29687 ` 1333` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1334` ``` using H n1 by auto ``` chaieb@29687 ` 1335` ``` have th0: "(b oo a) \$n = (\i = 0..n1. c \$ i * a ^ i \$ n) + b\$n * (a\$1)^n" ``` chaieb@29687 ` 1336` ``` unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] seq ``` chaieb@29687 ` 1337` ``` using startsby_zero_power_nth_same[OF a0] ``` chaieb@29687 ` 1338` ``` by simp ``` chaieb@29687 ` 1339` ``` have th1: "(c oo a) \$n = (\i = 0..n1. c \$ i * a ^ i \$ n) + c\$n * (a\$1)^n" ``` chaieb@29687 ` 1340` ``` unfolding fps_compose_nth setsum_Un_disjoint[OF f d, unfolded eq] ``` chaieb@29687 ` 1341` ``` using startsby_zero_power_nth_same[OF a0] ``` chaieb@29687 ` 1342` ``` by simp ``` chaieb@29687 ` 1343` ``` from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 ``` chaieb@29687 ` 1344` ``` have "b\$n = c\$n" by auto} ``` chaieb@29687 ` 1345` ``` ultimately show "b\$n = c\$n" by (cases n, auto) ``` chaieb@29687 ` 1346` ``` qed} ``` chaieb@29687 ` 1347` ``` then have ?rhs by (simp add: fps_eq_iff)} ``` chaieb@29687 ` 1348` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1349` ```qed ``` chaieb@29687 ` 1350` chaieb@29687 ` 1351` huffman@29906 ` 1352` ```subsection {* Radicals *} ``` chaieb@29687 ` 1353` chaieb@29687 ` 1354` ```declare setprod_cong[fundef_cong] ``` chaieb@29687 ` 1355` ```function radical :: "(nat \ 'a \ 'a) \ nat \ ('a::{field, recpower}) fps \ nat \ 'a" where ``` chaieb@29687 ` 1356` ``` "radical r 0 a 0 = 1" ``` chaieb@29687 ` 1357` ```| "radical r 0 a (Suc n) = 0" ``` chaieb@29687 ` 1358` ```| "radical r (Suc k) a 0 = r (Suc k) (a\$0)" ``` chaieb@29687 ` 1359` ```| "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 ` 1360` ```by pat_completeness auto ``` chaieb@29687 ` 1361` chaieb@29687 ` 1362` ```termination radical ``` chaieb@29687 ` 1363` ```proof ``` chaieb@29687 ` 1364` ``` let ?R = "measure (\(r, k, a, n). n)" ``` chaieb@29687 ` 1365` ``` { ``` chaieb@29687 ` 1366` ``` show "wf ?R" by auto} ``` chaieb@29687 ` 1367` ``` {fix r k a n xs i ``` chaieb@29687 ` 1368` ``` assume xs: "xs \ {xs \ natpermute (Suc n) (Suc k). Suc n \ set xs}" and i: "i \ {0..k}" ``` chaieb@29687 ` 1369` ``` {assume c: "Suc n \ xs ! i" ``` chaieb@29687 ` 1370` ``` from xs i have "xs !i \ Suc n" by (auto simp add: in_set_conv_nth natpermute_def) ``` chaieb@29687 ` 1371` ``` with c have c': "Suc n < xs!i" by arith ``` chaieb@29687 ` 1372` ``` have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1.. ({i} \ {i+1 ..< Suc k}) = {}" "{i} \ {i+1..< Suc k} = {}" by auto ``` chaieb@29687 ` 1374` ``` have eqs: "{0.. ({i} \ {i+1 ..< Suc k})" using i by auto ``` chaieb@29687 ` 1375` ``` from xs have "Suc n = foldl op + 0 xs" by (simp add: natpermute_def) ``` chaieb@29687 ` 1376` ``` also have "\ = setsum (nth xs) {0.. = xs!i + setsum (nth xs) {0.. ?R" ``` chaieb@29687 ` 1384` ``` apply auto by (metis not_less)} ``` huffman@30488 ` 1385` ``` {fix r k a n ``` chaieb@29687 ` 1386` ``` show "((r,Suc k, a, 0),r, Suc k, a, Suc n) \ ?R" by simp} ``` chaieb@29687 ` 1387` ```qed ``` chaieb@29687 ` 1388` chaieb@29687 ` 1389` ```definition "fps_radical r n a = Abs_fps (radical r n a)" ``` chaieb@29687 ` 1390` chaieb@29687 ` 1391` ```lemma fps_radical0[simp]: "fps_radical r 0 a = 1" ``` chaieb@29687 ` 1392` ``` apply (auto simp add: fps_eq_iff fps_radical_def) by (case_tac n, auto) ``` chaieb@29687 ` 1393` chaieb@29687 ` 1394` ```lemma fps_radical_nth_0[simp]: "fps_radical r n a \$ 0 = (if n=0 then 1 else r n (a\$0))" ``` chaieb@29687 ` 1395` ``` by (cases n, simp_all add: fps_radical_def) ``` chaieb@29687 ` 1396` huffman@30488 ` 1397` ```lemma fps_radical_power_nth[simp]: ``` chaieb@29687 ` 1398` ``` assumes r: "(r k (a\$0)) ^ k = a\$0" ``` chaieb@29687 ` 1399` ``` shows "fps_radical r k a ^ k \$ 0 = (if k = 0 then 1 else a\$0)" ``` chaieb@29687 ` 1400` ```proof- ``` chaieb@29687 ` 1401` ``` {assume "k=0" hence ?thesis by simp } ``` chaieb@29687 ` 1402` ``` moreover ``` huffman@30488 ` 1403` ``` {fix h assume h: "k = Suc h" ``` chaieb@29687 ` 1404` ``` have fh: "finite {0..h}" by simp ``` chaieb@29687 ` 1405` ``` have eq1: "fps_radical r k a ^ k \$ 0 = (\j\{0..h}. fps_radical r k a \$ (replicate k 0) ! j)" ``` chaieb@29687 ` 1406` ``` unfolding fps_power_nth h by simp ``` chaieb@29687 ` 1407` ``` also have "\ = (\j\{0..h}. r k (a\$0))" ``` chaieb@29687 ` 1408` ``` apply (rule setprod_cong) ``` chaieb@29687 ` 1409` ``` apply simp ``` chaieb@29687 ` 1410` ``` using h ``` chaieb@29687 ` 1411` ``` apply (subgoal_tac "replicate k (0::nat) ! x = 0") ``` chaieb@29687 ` 1412` ``` by (auto intro: nth_replicate simp del: replicate.simps) ``` chaieb@29687 ` 1413` ``` also have "\ = a\$0" ``` chaieb@29687 ` 1414` ``` unfolding setprod_constant[OF fh] using r by (simp add: h) ``` chaieb@29687 ` 1415` ``` finally have ?thesis using h by simp} ``` chaieb@29687 ` 1416` ``` ultimately show ?thesis by (cases k, auto) ``` huffman@30488 ` 1417` ```qed ``` chaieb@29687 ` 1418` huffman@30488 ` 1419` ```lemma natpermute_max_card: assumes n0: "n\0" ``` chaieb@29687 ` 1420` ``` shows "card {xs \ natpermute n (k+1). n \ set xs} = k+1" ``` chaieb@29687 ` 1421` ``` unfolding natpermute_contain_maximal ``` chaieb@29687 ` 1422` ```proof- ``` chaieb@29687 ` 1423` ``` let ?A= "\i. {replicate (k + 1) 0[i := n]}" ``` chaieb@29687 ` 1424` ``` let ?K = "{0 ..k}" ``` chaieb@29687 ` 1425` ``` have fK: "finite ?K" by simp ``` chaieb@29687 ` 1426` ``` have fAK: "\i\?K. finite (?A i)" by auto ``` chaieb@29687 ` 1427` ``` have d: "\i\ ?K. \j\ ?K. i \ j \ {replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` chaieb@29687 ` 1428` ``` proof(clarify) ``` chaieb@29687 ` 1429` ``` fix i j assume i: "i \ ?K" and j: "j\ ?K" and ij: "i\j" ``` chaieb@29687 ` 1430` ``` {assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" ``` chaieb@29687 ` 1431` ``` have "(replicate (k+1) 0 [i:=n] ! i) = n" using i by (simp del: replicate.simps) ``` chaieb@29687 ` 1432` ``` moreover ``` chaieb@29687 ` 1433` ``` have "(replicate (k+1) 0 [j:=n] ! i) = 0" using i ij by (simp del: replicate.simps) ``` chaieb@29687 ` 1434` ``` ultimately have False using eq n0 by (simp del: replicate.simps)} ``` chaieb@29687 ` 1435` ``` then show "{replicate (k + 1) 0[i := n]} \ {replicate (k + 1) 0[j := n]} = {}" ``` chaieb@29687 ` 1436` ``` by auto ``` chaieb@29687 ` 1437` ``` qed ``` huffman@30488 ` 1438` ``` from card_UN_disjoint[OF fK fAK d] ``` chaieb@29687 ` 1439` ``` show "card (\i\{0..k}. {replicate (k + 1) 0[i := n]}) = k+1" by simp ``` chaieb@29687 ` 1440` ```qed ``` huffman@30488 ` 1441` huffman@30488 ` 1442` ```lemma power_radical: ``` chaieb@29687 ` 1443` ``` fixes a:: "'a ::{field, ring_char_0, recpower} fps" ``` chaieb@29687 ` 1444` ``` assumes r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0" and a0: "a\$0 \ 0" ``` huffman@30488 ` 1445` ``` shows "(fps_radical r (Suc k) a) ^ (Suc k) = a" ``` chaieb@29687 ` 1446` ```proof- ``` chaieb@29687 ` 1447` ``` let ?r = "fps_radical r (Suc k) a" ``` chaieb@29687 ` 1448` ``` from a0 r0 have r00: "r (Suc k) (a\$0) \ 0" by auto ``` chaieb@29687 ` 1449` ``` {fix z have "?r ^ Suc k \$ z = a\$z" ``` chaieb@29687 ` 1450` ``` proof(induct z rule: nat_less_induct) ``` chaieb@29687 ` 1451` ``` fix n assume H: "\m 0" using n1 by arith ``` chaieb@29687 ` 1458` ``` let ?Pnk = "natpermute n (k + 1)" ``` chaieb@29687 ` 1459` ``` let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1460` ``` let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1461` ``` have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast ``` chaieb@29687 ` 1462` ``` have d: "?Pnkn \ ?Pnknn = {}" by blast ``` huffman@30488 ` 1463` ``` have f: "finite ?Pnkn" "finite ?Pnknn" ``` chaieb@29687 ` 1464` ``` using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] ``` chaieb@29687 ` 1465` ``` by (metis natpermute_finite)+ ``` chaieb@29687 ` 1466` ``` let ?f = "\v. \j\{0..k}. ?r \$ v ! j" ``` huffman@30488 ` 1467` ``` have "setsum ?f ?Pnkn = setsum (\v. ?r \$ n * r (Suc k) (a \$ 0) ^ k) ?Pnkn" ``` chaieb@29687 ` 1468` ``` proof(rule setsum_cong2) ``` chaieb@29687 ` 1469` ``` fix v assume v: "v \ {xs \ natpermute n (k + 1). n \ set xs}" ``` chaieb@29687 ` 1470` ``` 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 ` 1471` ``` from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" ``` chaieb@29687 ` 1472` ``` unfolding natpermute_contain_maximal by auto ``` chaieb@29687 ` 1473` ``` 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 ` 1474` ``` apply (rule setprod_cong, simp) ``` chaieb@29687 ` 1475` ``` using i r0 by (simp del: replicate.simps) ``` chaieb@29687 ` 1476` ``` also have "\ = (fps_radical r (Suc k) a \$ n) * r (Suc k) (a\$0) ^ k" ``` chaieb@29687 ` 1477` ``` unfolding setprod_gen_delta[OF fK] using i r0 by simp ``` chaieb@29687 ` 1478` ``` finally show ?ths . ``` chaieb@29687 ` 1479` ``` qed ``` huffman@30488 ` 1480` ``` then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r \$ n * r (Suc k) (a \$ 0) ^ k" ``` huffman@30488 ` 1481` ``` by (simp add: natpermute_max_card[OF nz, simplified]) ``` chaieb@29687 ` 1482` ``` also have "\ = a\$n - setsum ?f ?Pnknn" ``` chaieb@29687 ` 1483` ``` unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc ) ``` chaieb@29687 ` 1484` ``` finally have fn: "setsum ?f ?Pnkn = a\$n - setsum ?f ?Pnknn" . ``` huffman@30488 ` 1485` ``` have "(?r ^ Suc k)\$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" ``` chaieb@29687 ` 1486` ``` unfolding fps_power_nth_Suc setsum_Un_disjoint[OF f d, unfolded eq] .. ``` chaieb@29687 ` 1487` ``` also have "\ = a\$n" unfolding fn by simp ``` chaieb@29687 ` 1488` ``` finally have "?r ^ Suc k \$ n = a \$n" .} ``` chaieb@29687 ` 1489` ``` ultimately show "?r ^ Suc k \$ n = a \$n" by (cases n, auto) ``` chaieb@29687 ` 1490` ``` qed } ``` chaieb@29687 ` 1491` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1492` ```qed ``` chaieb@29687 ` 1493` chaieb@29687 ` 1494` ```lemma eq_divide_imp': assumes c0: "(c::'a::field) ~= 0" and eq: "a * c = b" ``` huffman@30488 ` 1495` ``` shows "a = b / c" ``` chaieb@29687 ` 1496` ```proof- ``` chaieb@29687 ` 1497` ``` from eq have "a * c * inverse c = b * inverse c" by simp ``` chaieb@29687 ` 1498` ``` hence "a * (inverse c * c) = b/c" by (simp only: field_simps divide_inverse) ``` chaieb@29687 ` 1499` ``` then show "a = b/c" unfolding field_inverse[OF c0] by simp ``` chaieb@29687 ` 1500` ```qed ``` chaieb@29687 ` 1501` huffman@30488 ` 1502` ```lemma radical_unique: ``` huffman@30488 ` 1503` ``` assumes r0: "(r (Suc k) (b\$0)) ^ Suc k = b\$0" ``` chaieb@29687 ` 1504` ``` and a0: "r (Suc k) (b\$0 ::'a::{field, ring_char_0, recpower}) = a\$0" and b0: "b\$0 \ 0" ``` chaieb@29687 ` 1505` ``` shows "a^(Suc k) = b \ a = fps_radical r (Suc k) b" ``` chaieb@29687 ` 1506` ```proof- ``` chaieb@29687 ` 1507` ``` let ?r = "fps_radical r (Suc k) b" ``` chaieb@29687 ` 1508` ``` have r00: "r (Suc k) (b\$0) \ 0" using b0 r0 by auto ``` chaieb@29687 ` 1509` ``` {assume H: "a = ?r" ``` chaieb@29687 ` 1510` ``` from H have "a^Suc k = b" using power_radical[of r k, OF r0 b0] by simp} ``` chaieb@29687 ` 1511` ``` moreover ``` chaieb@29687 ` 1512` ``` {assume H: "a^Suc k = b" ``` chaieb@29687 ` 1513` ``` (* Generally a\$0 would need to be the k+1 st root of b\$0 *) ``` chaieb@29687 ` 1514` ``` have ceq: "card {0..k} = Suc k" by simp ``` chaieb@29687 ` 1515` ``` have fk: "finite {0..k}" by simp ``` chaieb@29687 ` 1516` ``` from a0 have a0r0: "a\$0 = ?r\$0" by simp ``` chaieb@29687 ` 1517` ``` {fix n have "a \$ n = ?r \$ n" ``` chaieb@29687 ` 1518` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1519` ``` fix n assume h: "\m 0" using n1 by arith ``` chaieb@29687 ` 1525` ``` let ?Pnk = "natpermute n (Suc k)" ``` chaieb@29687 ` 1526` ``` let ?Pnkn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1527` ``` let ?Pnknn = "{xs \ ?Pnk. n \ set xs}" ``` chaieb@29687 ` 1528` ``` have eq: "?Pnkn \ ?Pnknn = ?Pnk" by blast ``` chaieb@29687 ` 1529` ``` have d: "?Pnkn \ ?Pnknn = {}" by blast ``` huffman@30488 ` 1530` ``` have f: "finite ?Pnkn" "finite ?Pnknn" ``` chaieb@29687 ` 1531` ``` using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] ``` chaieb@29687 ` 1532` ``` by (metis natpermute_finite)+ ``` chaieb@29687 ` 1533` ``` let ?f = "\v. \j\{0..k}. ?r \$ v ! j" ``` chaieb@29687 ` 1534` ``` let ?g = "\v. \j\{0..k}. a \$ v ! j" ``` huffman@30488 ` 1535` ``` have "setsum ?g ?Pnkn = setsum (\v. a \$ n * (?r\$0)^k) ?Pnkn" ``` chaieb@29687 ` 1536` ``` proof(rule setsum_cong2) ``` chaieb@29687 ` 1537` ``` fix v assume v: "v \ {xs \ natpermute n (Suc k). n \ set xs}" ``` chaieb@29687 ` 1538` ``` let ?ths = "(\j\{0..k}. a \$ v ! j) = a \$ n * (?r\$0)^k" ``` chaieb@29687 ` 1539` ``` from v obtain i where i: "i \ {0..k}" "v = replicate (k+1) 0 [i:= n]" ``` chaieb@29687 ` 1540` ``` unfolding Suc_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps) ``` chaieb@29687 ` 1541` ``` have "(\j\{0..k}. a \$ v ! j) = (\j\{0..k}. if j = i then a \$ n else r (Suc k) (b\$0))" ``` chaieb@29687 ` 1542` ``` apply (rule setprod_cong, simp) ``` chaieb@29687 ` 1543` ``` using i a0 by (simp del: replicate.simps) ``` chaieb@29687 ` 1544` ``` also have "\ = a \$ n * (?r \$ 0)^k" ``` chaieb@29687 ` 1545` ``` unfolding setprod_gen_delta[OF fK] using i by simp ``` chaieb@29687 ` 1546` ``` finally show ?ths . ``` chaieb@29687 ` 1547` ``` qed ``` huffman@30488 ` 1548` ``` then have th0: "setsum ?g ?Pnkn = of_nat (k+1) * a \$ n * (?r \$ 0)^k" ``` chaieb@29687 ` 1549` ``` by (simp add: natpermute_max_card[OF nz, simplified]) ``` chaieb@29687 ` 1550` ``` have th1: "setsum ?g ?Pnknn = setsum ?f ?Pnknn" ``` chaieb@29687 ` 1551` ``` proof (rule setsum_cong2, rule setprod_cong, simp) ``` chaieb@29687 ` 1552` ``` fix xs i assume xs: "xs \ ?Pnknn" and i: "i \ {0..k}" ``` chaieb@29687 ` 1553` ``` {assume c: "n \ xs ! i" ``` chaieb@29687 ` 1554` ``` from xs i have "xs !i \ n" by (auto simp add: in_set_conv_nth natpermute_def) ``` chaieb@29687 ` 1555` ``` with c have c': "n < xs!i" by arith ``` chaieb@29687 ` 1556` ``` have fths: "finite {0 ..< i}" "finite {i}" "finite {i+1.. ({i} \ {i+1 ..< Suc k}) = {}" "{i} \ {i+1..< Suc k} = {}" by auto ``` chaieb@29687 ` 1558` ``` have eqs: "{0.. ({i} \ {i+1 ..< Suc k})" using i by auto ``` chaieb@29687 ` 1559` ``` from xs have "n = foldl op + 0 xs" by (simp add: natpermute_def) ``` chaieb@29687 ` 1560` ``` 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 ` 1572` ``` by (simp add: field_simps del: of_nat_Suc) ``` chaieb@29687 ` 1573` ``` from H have "b\$n = a^Suc k \$ n" by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1574` ``` also have "a ^ Suc k\$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" ``` huffman@30488 ` 1575` ``` unfolding fps_power_nth_Suc ``` huffman@30488 ` 1576` ``` using setsum_Un_disjoint[OF f d, unfolded Suc_plus1[symmetric], ``` chaieb@29687 ` 1577` ``` unfolded eq, of ?g] by simp ``` chaieb@29687 ` 1578` ``` also have "\ = of_nat (k+1) * a \$ n * (?r \$ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 .. ``` chaieb@29687 ` 1579` ``` finally have "of_nat (k+1) * a \$ n * (?r \$ 0)^k = b\$n - setsum ?f ?Pnknn" by simp ``` chaieb@29687 ` 1580` ``` then have "a\$n = (b\$n - setsum ?f ?Pnknn) / (of_nat (k+1) * (?r \$ 0)^k)" ``` huffman@30488 ` 1581` ``` apply - ``` chaieb@29687 ` 1582` ``` apply (rule eq_divide_imp') ``` chaieb@29687 ` 1583` ``` using r00 ``` chaieb@29687 ` 1584` ``` apply (simp del: of_nat_Suc) ``` chaieb@29687 ` 1585` ``` by (simp add: mult_ac) ``` chaieb@29687 ` 1586` ``` then have "a\$n = ?r \$n" ``` chaieb@29687 ` 1587` ``` apply (simp del: of_nat_Suc) ``` chaieb@29687 ` 1588` ``` unfolding fps_radical_def n1 ``` huffman@29911 ` 1589` ``` by (simp add: field_simps n1 th00 del: of_nat_Suc)} ``` chaieb@29687 ` 1590` ``` ultimately show "a\$n = ?r \$ n" by (cases n, auto) ``` chaieb@29687 ` 1591` ``` qed} ``` chaieb@29687 ` 1592` ``` then have "a = ?r" by (simp add: fps_eq_iff)} ``` chaieb@29687 ` 1593` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1594` ```qed ``` chaieb@29687 ` 1595` chaieb@29687 ` 1596` huffman@30488 ` 1597` ```lemma radical_power: ``` huffman@30488 ` 1598` ``` assumes r0: "r (Suc k) ((a\$0) ^ Suc k) = a\$0" ``` chaieb@29687 ` 1599` ``` and a0: "(a\$0 ::'a::{field, ring_char_0, recpower}) \ 0" ``` chaieb@29687 ` 1600` ``` shows "(fps_radical r (Suc k) (a ^ Suc k)) = a" ``` chaieb@29687 ` 1601` ```proof- ``` chaieb@29687 ` 1602` ``` let ?ak = "a^ Suc k" ``` huffman@30273 ` 1603` ``` have ak0: "?ak \$ 0 = (a\$0) ^ Suc k" by (simp add: fps_nth_power_0 del: power_Suc) ``` chaieb@29687 ` 1604` ``` from r0 have th0: "r (Suc k) (a ^ Suc k \$ 0) ^ Suc k = a ^ Suc k \$ 0" using ak0 by auto ``` chaieb@29687 ` 1605` ``` from r0 ak0 have th1: "r (Suc k) (a ^ Suc k \$ 0) = a \$ 0" by auto ``` chaieb@29687 ` 1606` ``` from ak0 a0 have ak00: "?ak \$ 0 \0 " by auto ``` chaieb@29687 ` 1607` ``` from radical_unique[of r k ?ak a, OF th0 th1 ak00] show ?thesis by metis ``` chaieb@29687 ` 1608` ```qed ``` chaieb@29687 ` 1609` huffman@30488 ` 1610` ```lemma fps_deriv_radical: ``` chaieb@29687 ` 1611` ``` fixes a:: "'a ::{field, ring_char_0, recpower} fps" ``` chaieb@29687 ` 1612` ``` assumes r0: "(r (Suc k) (a\$0)) ^ Suc k = a\$0" and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1613` ``` 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 ` 1614` ```proof- ``` chaieb@29687 ` 1615` ``` let ?r= "fps_radical r (Suc k) a" ``` chaieb@29687 ` 1616` ``` let ?w = "(fps_const (of_nat (Suc k)) * ?r ^ k)" ``` chaieb@29687 ` 1617` ``` from a0 r0 have r0': "r (Suc k) (a\$0) \ 0" by auto ``` chaieb@29687 ` 1618` ``` from r0' have w0: "?w \$ 0 \ 0" by (simp del: of_nat_Suc) ``` chaieb@29687 ` 1619` ``` note th0 = inverse_mult_eq_1[OF w0] ``` chaieb@29687 ` 1620` ``` let ?iw = "inverse ?w" ``` chaieb@29687 ` 1621` ``` from power_radical[of r, OF r0 a0] ``` chaieb@29687 ` 1622` ``` have "fps_deriv (?r ^ Suc k) = fps_deriv a" by simp ``` chaieb@29687 ` 1623` ``` hence "fps_deriv ?r * ?w = fps_deriv a" ``` huffman@30273 ` 1624` ``` by (simp add: fps_deriv_power mult_ac del: power_Suc) ``` chaieb@29687 ` 1625` ``` hence "?iw * fps_deriv ?r * ?w = ?iw * fps_deriv a" by simp ``` chaieb@29687 ` 1626` ``` hence "fps_deriv ?r * (?iw * ?w) = fps_deriv a / ?w" ``` chaieb@29687 ` 1627` ``` by (simp add: fps_divide_def) ``` huffman@30488 ` 1628` ``` then show ?thesis unfolding th0 by simp ``` chaieb@29687 ` 1629` ```qed ``` chaieb@29687 ` 1630` huffman@30488 ` 1631` ```lemma radical_mult_distrib: ``` chaieb@29687 ` 1632` ``` fixes a:: "'a ::{field, ring_char_0, recpower} fps" ``` huffman@30488 ` 1633` ``` assumes ``` huffman@30488 ` 1634` ``` ra0: "r (k) (a \$ 0) ^ k = a \$ 0" ``` chaieb@29687 ` 1635` ``` and rb0: "r (k) (b \$ 0) ^ k = b \$ 0" ``` chaieb@29687 ` 1636` ``` and r0': "r (k) ((a * b) \$ 0) = r (k) (a \$ 0) * r (k) (b \$ 0)" ``` chaieb@29687 ` 1637` ``` and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1638` ``` and b0: "b\$0 \ 0" ``` chaieb@29687 ` 1639` ``` shows "fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" ``` chaieb@29687 ` 1640` ```proof- ``` chaieb@29687 ` 1641` ``` from r0' have r0: "(r (k) ((a*b)\$0)) ^ k = (a*b)\$0" ``` chaieb@29687 ` 1642` ``` by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) ``` chaieb@29687 ` 1643` ``` {assume "k=0" hence ?thesis by simp} ``` chaieb@29687 ` 1644` ``` moreover ``` chaieb@29687 ` 1645` ``` {fix h assume k: "k = Suc h" ``` chaieb@29687 ` 1646` ``` let ?ra = "fps_radical r (Suc h) a" ``` chaieb@29687 ` 1647` ``` let ?rb = "fps_radical r (Suc h) b" ``` huffman@30488 ` 1648` ``` have th0: "r (Suc h) ((a * b) \$ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) \$ 0" ``` chaieb@29687 ` 1649` ``` using r0' k by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1650` ``` have ab0: "(a*b) \$ 0 \ 0" using a0 b0 by (simp add: fps_mult_nth) ``` huffman@30488 ` 1651` ``` 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 ` 1652` ``` power_radical[of r, OF ra0[unfolded k] a0] power_radical[of r, OF rb0[unfolded k] b0] k ``` huffman@30273 ` 1653` ``` have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc)} ``` chaieb@29687 ` 1654` ```ultimately show ?thesis by (cases k, auto) ``` chaieb@29687 ` 1655` ```qed ``` chaieb@29687 ` 1656` chaieb@29687 ` 1657` ```lemma radical_inverse: ``` chaieb@29687 ` 1658` ``` fixes a:: "'a ::{field, ring_char_0, recpower} fps" ``` huffman@30488 ` 1659` ``` assumes ``` huffman@30488 ` 1660` ``` ra0: "r (k) (a \$ 0) ^ k = a \$ 0" ``` chaieb@29687 ` 1661` ``` and ria0: "r (k) (inverse (a \$ 0)) = inverse (r (k) (a \$ 0))" ``` huffman@30488 ` 1662` ``` and r1: "(r (k) 1) = 1" ``` chaieb@29687 ` 1663` ``` and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1664` ``` shows "fps_radical r (k) (inverse a) = inverse (fps_radical r (k) a)" ``` chaieb@29687 ` 1665` ```proof- ``` chaieb@29687 ` 1666` ``` {assume "k=0" then have ?thesis by simp} ``` chaieb@29687 ` 1667` ``` moreover ``` chaieb@29687 ` 1668` ``` {fix h assume k[simp]: "k = Suc h" ``` chaieb@29687 ` 1669` ``` let ?ra = "fps_radical r (Suc h) a" ``` chaieb@29687 ` 1670` ``` let ?ria = "fps_radical r (Suc h) (inverse a)" ``` chaieb@29687 ` 1671` ``` from ra0 a0 have th00: "r (Suc h) (a\$0) \ 0" by auto ``` chaieb@29687 ` 1672` ``` have ria0': "r (Suc h) (inverse a \$ 0) ^ Suc h = inverse a\$0" ``` chaieb@29687 ` 1673` ``` using ria0 ra0 a0 ``` huffman@30273 ` 1674` ``` by (simp add: fps_inverse_def nonzero_power_inverse[OF th00, symmetric] ``` huffman@30273 ` 1675` ``` del: power_Suc) ``` huffman@30488 ` 1676` ``` from inverse_mult_eq_1[OF a0] have th0: "a * inverse a = 1" ``` chaieb@29687 ` 1677` ``` by (simp add: mult_commute) ``` chaieb@29687 ` 1678` ``` from radical_unique[where a=1 and b=1 and r=r and k=h, simplified, OF r1[unfolded k]] ``` chaieb@29687 ` 1679` ``` have th01: "fps_radical r (Suc h) 1 = 1" . ``` chaieb@29687 ` 1680` ``` have th1: "r (Suc h) ((a * inverse a) \$ 0) ^ Suc h = (a * inverse a) \$ 0" ``` chaieb@29687 ` 1681` ``` "r (Suc h) ((a * inverse a) \$ 0) = ``` chaieb@29687 ` 1682` ```r (Suc h) (a \$ 0) * r (Suc h) (inverse a \$ 0)" ``` chaieb@29687 ` 1683` ``` using r1 unfolding th0 apply (simp_all add: ria0[symmetric]) ``` chaieb@29687 ` 1684` ``` apply (simp add: fps_inverse_def a0) ``` chaieb@29687 ` 1685` ``` unfolding ria0[unfolded k] ``` chaieb@29687 ` 1686` ``` using th00 by simp ``` chaieb@29687 ` 1687` ``` from nonzero_imp_inverse_nonzero[OF a0] a0 ``` chaieb@29687 ` 1688` ``` have th2: "inverse a \$ 0 \ 0" by (simp add: fps_inverse_def) ``` chaieb@29687 ` 1689` ``` from radical_mult_distrib[of r "Suc h" a "inverse a", OF ra0[unfolded k] ria0' th1(2) a0 th2] ``` chaieb@29687 ` 1690` ``` have th3: "?ra * ?ria = 1" unfolding th0 th01 by simp ``` chaieb@29687 ` 1691` ``` from th00 have ra0: "?ra \$ 0 \ 0" by simp ``` chaieb@29687 ` 1692` ``` from fps_inverse_unique[OF ra0 th3] have ?thesis by simp} ``` chaieb@29687 ` 1693` ```ultimately show ?thesis by (cases k, auto) ``` chaieb@29687 ` 1694` ```qed ``` chaieb@29687 ` 1695` chaieb@29687 ` 1696` ```lemma fps_divide_inverse: "(a::('a::field) fps) / b = a * inverse b" ``` chaieb@29687 ` 1697` ``` by (simp add: fps_divide_def) ``` chaieb@29687 ` 1698` chaieb@29687 ` 1699` ```lemma radical_divide: ``` chaieb@29687 ` 1700` ``` fixes a:: "'a ::{field, ring_char_0, recpower} fps" ``` huffman@30488 ` 1701` ``` assumes ``` huffman@30488 ` 1702` ``` ra0: "r k (a \$ 0) ^ k = a \$ 0" ``` chaieb@29687 ` 1703` ``` and rb0: "r k (b \$ 0) ^ k = b \$ 0" ``` chaieb@29687 ` 1704` ``` and r1: "r k 1 = 1" ``` huffman@30488 ` 1705` ``` and rb0': "r k (inverse (b \$ 0)) = inverse (r k (b \$ 0))" ``` chaieb@29687 ` 1706` ``` and raib': "r k (a\$0 / (b\$0)) = r k (a\$0) / r k (b\$0)" ``` huffman@30488 ` 1707` ``` and a0: "a\$0 \ 0" ``` chaieb@29687 ` 1708` ``` and b0: "b\$0 \ 0" ``` chaieb@29687 ` 1709` ``` shows "fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" ``` chaieb@29687 ` 1710` ```proof- ``` chaieb@29687 ` 1711` ``` from raib' ``` chaieb@29687 ` 1712` ``` have raib: "r k (a\$0 / (b\$0)) = r k (a\$0) * r k (inverse (b\$0))" ``` chaieb@29687 ` 1713` ``` by (simp add: divide_inverse rb0'[symmetric]) ``` chaieb@29687 ` 1714` chaieb@29687 ` 1715` ``` {assume "k=0" hence ?thesis by (simp add: fps_divide_def)} ``` chaieb@29687 ` 1716` ``` moreover ``` chaieb@29687 ` 1717` ``` {assume k0: "k\ 0" ``` chaieb@29687 ` 1718` ``` from b0 k0 rb0 have rbn0: "r k (b \$0) \ 0" ``` chaieb@29687 ` 1719` ``` by (auto simp add: power_0_left) ``` huffman@30488 ` 1720` chaieb@29687 ` 1721` ``` from rb0 rb0' have rib0: "(r k (inverse (b \$ 0)))^k = inverse (b\$0)" ``` chaieb@29687 ` 1722` ``` by (simp add: nonzero_power_inverse[OF rbn0, symmetric]) ``` chaieb@29687 ` 1723` ``` from rib0 have th0: "r k (inverse b \$ 0) ^ k = inverse b \$ 0" ``` chaieb@29687 ` 1724` ``` by (simp add:fps_inverse_def b0) ``` huffman@30488 ` 1725` ``` from raib ``` chaieb@29687 ` 1726` ``` have th1: "r k ((a * inverse b) \$ 0) = r k (a \$ 0) * r k (inverse b \$ 0)" ``` chaieb@29687 ` 1727` ``` by (simp add: divide_inverse fps_inverse_def b0 fps_mult_nth) ``` chaieb@29687 ` 1728` ``` from nonzero_imp_inverse_nonzero[OF b0] b0 have th2: "inverse b \$ 0 \ 0" ``` chaieb@29687 ` 1729` ``` by (simp add: fps_inverse_def) ``` chaieb@29687 ` 1730` ``` from radical_mult_distrib[of r k a "inverse b", OF ra0 th0 th1 a0 th2] ``` chaieb@29687 ` 1731` ``` have th: "fps_radical r k (a/b) = fps_radical r k a * fps_radical r k (inverse b)" ``` chaieb@29687 ` 1732` ``` by (simp add: fps_divide_def) ``` chaieb@29687 ` 1733` ``` with radical_inverse[of r k b, OF rb0 rb0' r1 b0] ``` chaieb@29687 ` 1734` ``` have ?thesis by (simp add: fps_divide_def)} ``` chaieb@29687 ` 1735` ```ultimately show ?thesis by blast ``` chaieb@29687 ` 1736` ```qed ``` chaieb@29687 ` 1737` huffman@29906 ` 1738` ```subsection{* Derivative of composition *} ``` chaieb@29687 ` 1739` huffman@30488 ` 1740` ```lemma fps_compose_deriv: ``` chaieb@29687 ` 1741` ``` fixes a:: "('a::idom) fps" ``` chaieb@29687 ` 1742` ``` assumes b0: "b\$0 = 0" ``` chaieb@29687 ` 1743` ``` shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * (fps_deriv b)" ``` chaieb@29687 ` 1744` ```proof- ``` chaieb@29687 ` 1745` ``` {fix n ``` chaieb@29687 ` 1746` ``` have "(fps_deriv (a oo b))\$n = setsum (\i. a \$ i * (fps_deriv (b^i))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1747` ``` by (simp add: fps_compose_def ring_simps setsum_right_distrib del: of_nat_Suc) ``` chaieb@29687 ` 1748` ``` also have "\ = setsum (\i. a\$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1749` ``` by (simp add: ring_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) ``` chaieb@29687 ` 1750` ``` also have "\ = setsum (\i. of_nat i * a\$i * (((b^(i - 1)) * fps_deriv b))\$n) {0.. Suc n}" ``` chaieb@29687 ` 1751` ``` unfolding fps_mult_left_const_nth by (simp add: ring_simps) ``` chaieb@29687 ` 1752` ``` 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 ` 1753` ``` unfolding fps_mult_nth .. ``` chaieb@29687 ` 1754` ``` 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 ` 1755` ``` apply (rule setsum_mono_zero_right) ``` huffman@29913 ` 1756` ``` apply (auto simp add: mult_delta_left setsum_delta not_le) ``` huffman@29913 ` 1757` ``` done ``` chaieb@29687 ` 1758` ``` 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 ` 1759` ``` unfolding fps_deriv_nth ``` chaieb@29687 ` 1760` ``` apply (rule setsum_reindex_cong[where f="Suc"]) ``` chaieb@29687 ` 1761` ``` by (auto simp add: mult_assoc) ``` chaieb@29687 ` 1762` ``` 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 ` 1763` chaieb@29687 ` 1764` ``` 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 ` 1765` ``` unfolding fps_mult_nth by (simp add: mult_ac) ``` chaieb@29687 ` 1766` ``` 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 ` 1767` ``` unfolding fps_deriv_nth fps_compose_nth setsum_right_distrib mult_assoc ``` chaieb@29687 ` 1768` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1769` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 1770` ``` apply (simp_all add: subset_eq) ``` chaieb@29687 ` 1771` ``` apply clarify ``` chaieb@29687 ` 1772` ``` apply (subgoal_tac "b^i\$x = 0") ``` chaieb@29687 ` 1773` ``` apply simp ``` chaieb@29687 ` 1774` ``` apply (rule startsby_zero_power_prefix[OF b0, rule_format]) ``` chaieb@29687 ` 1775` ``` by simp ``` chaieb@29687 ` 1776` ``` 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 ` 1777` ``` unfolding setsum_right_distrib ``` chaieb@29687 ` 1778` ``` apply (subst setsum_commute) ``` chaieb@29687 ` 1779` ``` by ((rule setsum_cong2)+) simp ``` chaieb@29687 ` 1780` ``` finally have "(fps_deriv (a oo b))\$n = (((fps_deriv a) oo b) * (fps_deriv b)) \$n" ``` chaieb@29687 ` 1781` ``` unfolding th0 by simp} ``` chaieb@29687 ` 1782` ```then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1783` ```qed ``` chaieb@29687 ` 1784` chaieb@29687 ` 1785` ```lemma fps_mult_X_plus_1_nth: ``` chaieb@29687 ` 1786` ``` "((1+X)*a) \$n = (if n = 0 then (a\$n :: 'a::comm_ring_1) else a\$n + a\$(n - 1))" ``` chaieb@29687 ` 1787` ```proof- ``` chaieb@29687 ` 1788` ``` {assume "n = 0" hence ?thesis by (simp add: fps_mult_nth )} ``` chaieb@29687 ` 1789` ``` moreover ``` chaieb@29687 ` 1790` ``` {fix m assume m: "n = Suc m" ``` chaieb@29687 ` 1791` ``` have "((1+X)*a) \$n = setsum (\i. (1+X)\$i * a\$(n-i)) {0..n}" ``` chaieb@29687 ` 1792` ``` by (simp add: fps_mult_nth) ``` chaieb@29687 ` 1793` ``` also have "\ = setsum (\i. (1+X)\$i * a\$(n-i)) {0.. 1}" ``` chaieb@29687 ` 1794` ``` unfolding m ``` chaieb@29687 ` 1795` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 1796` ``` by (auto simp add: ) ``` chaieb@29687 ` 1797` ``` also have "\ = (if n = 0 then (a\$n :: 'a::comm_ring_1) else a\$n + a\$(n - 1))" ``` chaieb@29687 ` 1798` ``` unfolding m ``` chaieb@29687 ` 1799` ``` by (simp add: ) ``` chaieb@29687 ` 1800` ``` finally have ?thesis .} ``` chaieb@29687 ` 1801` ``` ultimately show ?thesis by (cases n, auto) ``` chaieb@29687 ` 1802` ```qed ``` chaieb@29687 ` 1803` huffman@29906 ` 1804` ```subsection{* Finite FPS (i.e. polynomials) and X *} ``` chaieb@29687 ` 1805` ```lemma fps_poly_sum_X: ``` huffman@30488 ` 1806` ``` assumes z: "\i > n. a\$i = (0::'a::comm_ring_1)" ``` chaieb@29687 ` 1807` ``` shows "a = setsum (\i. fps_const (a\$i) * X^i) {0..n}" (is "a = ?r") ``` chaieb@29687 ` 1808` ```proof- ``` chaieb@29687 ` 1809` ``` {fix i ``` huffman@30488 ` 1810` ``` have "a\$i = ?r\$i" ``` chaieb@29687 ` 1811` ``` unfolding fps_setsum_nth fps_mult_left_const_nth X_power_nth ``` huffman@29913 ` 1812` ``` by (simp add: mult_delta_right setsum_delta' z) ``` huffman@29913 ` 1813` ``` } ``` chaieb@29687 ` 1814` ``` then show ?thesis unfolding fps_eq_iff by blast ``` chaieb@29687 ` 1815` ```qed ``` chaieb@29687 ` 1816` huffman@29906 ` 1817` ```subsection{* Compositional inverses *} ``` chaieb@29687 ` 1818` chaieb@29687 ` 1819` chaieb@29687 ` 1820` ```fun compinv :: "'a fps \ nat \ 'a::{recpower,field}" where ``` chaieb@29687 ` 1821` ``` "compinv a 0 = X\$0" ``` chaieb@29687 ` 1822` ```| "compinv a (Suc n) = (X\$ Suc n - setsum (\i. (compinv a i) * (a^i)\$Suc n) {0 .. n}) / (a\$1) ^ Suc n" ``` chaieb@29687 ` 1823` chaieb@29687 ` 1824` ```definition "fps_inv a = Abs_fps (compinv a)" ``` chaieb@29687 ` 1825` chaieb@29687 ` 1826` ```lemma fps_inv: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1827` ``` shows "fps_inv a oo a = X" ``` chaieb@29687 ` 1828` ```proof- ``` chaieb@29687 ` 1829` ``` let ?i = "fps_inv a oo a" ``` chaieb@29687 ` 1830` ``` {fix n ``` huffman@30488 ` 1831` ``` have "?i \$n = X\$n" ``` chaieb@29687 ` 1832` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1833` ``` 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 ` 1839` ``` by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0] ``` huffman@30273 ` 1840` ``` del: power_Suc) ``` chaieb@29687 ` 1841` ``` 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 ` 1842` ``` using a0 a1 n1 by (simp add: fps_inv_def) ``` huffman@30488 ` 1843` ``` also have "\ = X\$n" using n1 by simp ``` chaieb@29687 ` 1844` ``` finally have "?i \$ n = X\$n" .} ``` chaieb@29687 ` 1845` ``` ultimately show "?i \$ n = X\$n" by (cases n, auto) ``` chaieb@29687 ` 1846` ``` qed} ``` chaieb@29687 ` 1847` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1848` ```qed ``` chaieb@29687 ` 1849` chaieb@29687 ` 1850` chaieb@29687 ` 1851` ```fun gcompinv :: "'a fps \ 'a fps \ nat \ 'a::{recpower,field}" where ``` chaieb@29687 ` 1852` ``` "gcompinv b a 0 = b\$0" ``` chaieb@29687 ` 1853` ```| "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 ` 1854` chaieb@29687 ` 1855` ```definition "fps_ginv b a = Abs_fps (gcompinv b a)" ``` chaieb@29687 ` 1856` chaieb@29687 ` 1857` ```lemma fps_ginv: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 1858` ``` shows "fps_ginv b a oo a = b" ``` chaieb@29687 ` 1859` ```proof- ``` chaieb@29687 ` 1860` ``` let ?i = "fps_ginv b a oo a" ``` chaieb@29687 ` 1861` ``` {fix n ``` huffman@30488 ` 1862` ``` have "?i \$n = b\$n" ``` chaieb@29687 ` 1863` ``` proof(induct n rule: nat_less_induct) ``` chaieb@29687 ` 1864` ``` 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 ` 1870` ``` by (simp add: fps_compose_nth n1 startsby_zero_power_nth_same[OF a0] ``` huffman@30273 ` 1871` ``` del: power_Suc) ``` chaieb@29687 ` 1872` ``` 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 ` 1873` ``` using a0 a1 n1 by (simp add: fps_ginv_def) ``` huffman@30488 ` 1874` ``` also have "\ = b\$n" using n1 by simp ``` chaieb@29687 ` 1875` ``` finally have "?i \$ n = b\$n" .} ``` chaieb@29687 ` 1876` ``` ultimately show "?i \$ n = b\$n" by (cases n, auto) ``` chaieb@29687 ` 1877` ``` qed} ``` chaieb@29687 ` 1878` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 1879` ```qed ``` chaieb@29687 ` 1880` chaieb@29687 ` 1881` ```lemma fps_inv_ginv: "fps_inv = fps_ginv X" ``` chaieb@29687 ` 1882` ``` apply (auto simp add: expand_fun_eq fps_eq_iff fps_inv_def fps_ginv_def) ``` chaieb@29687 ` 1883` ``` apply (induct_tac n rule: nat_less_induct, auto) ``` chaieb@29687 ` 1884` ``` apply (case_tac na) ``` chaieb@29687 ` 1885` ``` apply simp ``` chaieb@29687 ` 1886` ``` apply simp ``` chaieb@29687 ` 1887` ``` done ``` chaieb@29687 ` 1888` chaieb@29687 ` 1889` ```lemma fps_compose_1[simp]: "1 oo a = 1" ``` haftmann@30960 ` 1890` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta) ``` chaieb@29687 ` 1891` chaieb@29687 ` 1892` ```lemma fps_compose_0[simp]: "0 oo a = 0" ``` huffman@29913 ` 1893` ``` by (simp add: fps_eq_iff fps_compose_nth) ``` chaieb@29687 ` 1894` chaieb@29687 ` 1895` ```lemma fps_compose_0_right[simp]: "a oo 0 = fps_const (a\$0)" ``` haftmann@30960 ` 1896` ``` by (auto simp add: fps_eq_iff fps_compose_nth power_0_left setsum_0') ``` chaieb@29687 ` 1897` chaieb@29687 ` 1898` ```lemma fps_compose_add_distrib: "(a + b) oo c = (a oo c) + (b oo c)" ``` haftmann@30960 ` 1899` ``` by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_addf) ``` chaieb@29687 ` 1900` chaieb@29687 ` 1901` ```lemma fps_compose_setsum_distrib: "(setsum f S) oo a = setsum (\i. f i oo a) S" ``` chaieb@29687 ` 1902` ```proof- ``` chaieb@29687 ` 1903` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29687 ` 1904` ``` moreover ``` chaieb@29687 ` 1905` ``` {assume fS: "finite S" ``` chaieb@29687 ` 1906` ``` have ?thesis ``` chaieb@29687 ` 1907` ``` proof(rule finite_induct[OF fS]) ``` chaieb@29687 ` 1908` ``` show "setsum f {} oo a = (\i\{}. f i oo a)" by simp ``` chaieb@29687 ` 1909` ``` next ``` chaieb@29687 ` 1910` ``` 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 ` 1911` ``` show "setsum f (insert x F) oo a = setsum (\i. f i oo a) (insert x F)" ``` chaieb@29687 ` 1912` ``` using fF xF h by (simp add: fps_compose_add_distrib) ``` chaieb@29687 ` 1913` ``` qed} ``` huffman@30488 ` 1914` ``` ultimately show ?thesis by blast ``` chaieb@29687 ` 1915` ```qed ``` chaieb@29687 ` 1916` huffman@30488 ` 1917` ```lemma convolution_eq: ``` chaieb@29687 ` 1918` ``` "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 ` 1919` ``` apply (rule setsum_reindex_cong[where f=fst]) ``` chaieb@29687 ` 1920` ``` apply (clarsimp simp add: inj_on_def) ``` chaieb@29687 ` 1921` ``` apply (auto simp add: expand_set_eq image_iff) ``` chaieb@29687 ` 1922` ``` apply (rule_tac x= "x" in exI) ``` chaieb@29687 ` 1923` ``` apply clarsimp ``` chaieb@29687 ` 1924` ``` apply (rule_tac x="n - x" in exI) ``` chaieb@29687 ` 1925` ``` apply arith ``` chaieb@29687 ` 1926` ``` done ``` chaieb@29687 ` 1927` chaieb@29687 ` 1928` ```lemma product_composition_lemma: ``` chaieb@29687 ` 1929` ``` assumes c0: "c\$0 = (0::'a::idom)" and d0: "d\$0 = 0" ``` chaieb@29687 ` 1930` ``` 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 ` 1931` ```proof- ``` chaieb@29687 ` 1932` ``` let ?S = "{(k\nat, m\nat). k + m \ n}" ``` huffman@30488 ` 1933` ``` have s: "?S \ {0..n} <*> {0..n}" by (auto simp add: subset_eq) ``` huffman@30488 ` 1934` ``` have f: "finite {(k\nat, m\nat). k + m \ n}" ``` chaieb@29687 ` 1935` ``` apply (rule finite_subset[OF s]) ``` chaieb@29687 ` 1936` ``` by auto ``` chaieb@29687 ` 1937` ``` 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 ` 1938` ``` apply (simp add: fps_mult_nth setsum_right_distrib) ``` chaieb@29687 ` 1939` ``` apply (subst setsum_commute) ``` chaieb@29687 ` 1940` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1941` ``` by (auto simp add: ring_simps) ``` huffman@30488 ` 1942` ``` also have "\ = ?l" ``` chaieb@29687 ` 1943` ``` apply (simp add: fps_mult_nth fps_compose_nth setsum_product) ``` chaieb@29687 ` 1944` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 1945` ``` apply (simp add: setsum_cartesian_product mult_assoc) ``` chaieb@29687 ` 1946` ``` apply (rule setsum_mono_zero_right[OF f]) ``` chaieb@29687 ` 1947` ``` apply (simp add: subset_eq) apply presburger ``` chaieb@29687 ` 1948` ``` apply clarsimp ``` chaieb@29687 ` 1949` ``` apply (rule ccontr) ``` chaieb@29687 ` 1950` ``` apply (clarsimp simp add: not_le) ``` chaieb@29687 ` 1951` ``` apply (case_tac "x < aa") ``` chaieb@29687 ` 1952` ``` apply simp ``` chaieb@29687 ` 1953` ``` apply (frule_tac startsby_zero_power_prefix[rule_format, OF c0]) ``` chaieb@29687 ` 1954` ``` apply blast ``` chaieb@29687 ` 1955` ``` apply simp ``` chaieb@29687 ` 1956` ``` apply (frule_tac startsby_zero_power_prefix[rule_format, OF d0]) ``` chaieb@29687 ` 1957` ``` apply blast ``` chaieb@29687 ` 1958` ``` done ``` chaieb@29687 ` 1959` ``` finally show ?thesis by simp ``` chaieb@29687 ` 1960` ```qed ``` chaieb@29687 ` 1961` chaieb@29687 ` 1962` ```lemma product_composition_lemma': ``` chaieb@29687 ` 1963` ``` assumes c0: "c\$0 = (0::'a::idom)" and d0: "d\$0 = 0" ``` chaieb@29687 ` 1964` ``` 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 ` 1965` ``` unfolding product_composition_lemma[OF c0 d0] ``` chaieb@29687 ` 1966` ``` unfolding setsum_cartesian_product ``` chaieb@29687 ` 1967` ``` apply (rule setsum_mono_zero_left) ``` chaieb@29687 ` 1968` ``` apply simp ``` chaieb@29687 ` 1969` ``` apply (clarsimp simp add: subset_eq) ``` chaieb@29687 ` 1970` ``` apply clarsimp ``` chaieb@29687 ` 1971` ``` apply (rule ccontr) ``` chaieb@29687 ` 1972` ``` apply (subgoal_tac "(c^aa * d^ba) \$ n = 0") ``` chaieb@29687 ` 1973` ``` apply simp ``` chaieb@29687 ` 1974` ``` unfolding fps_mult_nth ``` chaieb@29687 ` 1975` ``` apply (rule setsum_0') ``` chaieb@29687 ` 1976` ``` apply (clarsimp simp add: not_le) ``` chaieb@29687 ` 1977` ``` apply (case_tac "aaa < aa") ``` chaieb@29687 ` 1978` ``` apply (rule startsby_zero_power_prefix[OF c0, rule_format]) ``` chaieb@29687 ` 1979` ``` apply simp ``` chaieb@29687 ` 1980` ``` apply (subgoal_tac "n - aaa < ba") ``` chaieb@29687 ` 1981` ``` apply (frule_tac k = "ba" in startsby_zero_power_prefix[OF d0, rule_format]) ``` chaieb@29687 ` 1982` ``` apply simp ``` chaieb@29687 ` 1983` ``` apply arith ``` chaieb@29687 ` 1984` ``` done ``` huffman@30488 ` 1985` chaieb@29687 ` 1986` huffman@30488 ` 1987` ```lemma setsum_pair_less_iff: ``` chaieb@29687 ` 1988` ``` "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 ` 1989` ```proof- ``` chaieb@29687 ` 1990` ``` let ?KM= "{(k,m). k + m \ n}" ``` chaieb@29687 ` 1991` ``` let ?f = "%s. UNION {(0::nat)..s} (%i. {(i,s - i)})" ``` chaieb@29687 ` 1992` ``` have th0: "?KM = UNION {0..n} ?f" ``` chaieb@29687 ` 1993` ``` apply (simp add: expand_set_eq) ``` huffman@29911 ` 1994` ``` apply arith (* FIXME: VERY slow! *) ``` chaieb@29687 ` 1995` ``` done ``` chaieb@29687 ` 1996` ``` show "?l = ?r " ``` chaieb@29687 ` 1997` ``` unfolding th0 ``` chaieb@29687 ` 1998` ``` apply (subst setsum_UN_disjoint) ``` chaieb@29687 ` 1999` ``` apply auto ``` chaieb@29687 ` 2000` ``` apply (subst setsum_UN_disjoint) ``` chaieb@29687 ` 2001` ``` apply auto ``` chaieb@29687 ` 2002` ``` done ``` chaieb@29687 ` 2003` ```qed ``` chaieb@29687 ` 2004` chaieb@29687 ` 2005` ```lemma fps_compose_mult_distrib_lemma: ``` chaieb@29687 ` 2006` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2007` ``` 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 ` 2008` ``` unfolding product_composition_lemma[OF c0 c0] power_add[symmetric] ``` chaieb@29687 ` 2009` ``` 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 ` 2010` chaieb@29687 ` 2011` huffman@30488 ` 2012` ```lemma fps_compose_mult_distrib: ``` chaieb@29687 ` 2013` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2014` ``` shows "(a * b) oo c = (a oo c) * (b oo c)" (is "?l = ?r") ``` chaieb@29687 ` 2015` ``` apply (simp add: fps_eq_iff fps_compose_mult_distrib_lemma[OF c0]) ``` chaieb@29687 ` 2016` ``` by (simp add: fps_compose_nth fps_mult_nth setsum_left_distrib) ``` huffman@30488 ` 2017` ```lemma fps_compose_setprod_distrib: ``` chaieb@29687 ` 2018` ``` assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2019` ``` shows "(setprod a S) oo c = setprod (%k. a k oo c) S" (is "?l = ?r") ``` chaieb@29687 ` 2020` ``` apply (cases "finite S") ``` chaieb@29687 ` 2021` ``` apply simp_all ``` chaieb@29687 ` 2022` ``` apply (induct S rule: finite_induct) ``` chaieb@29687 ` 2023` ``` apply simp ``` chaieb@29687 ` 2024` ``` apply (simp add: fps_compose_mult_distrib[OF c0]) ``` chaieb@29687 ` 2025` ``` done ``` chaieb@29687 ` 2026` chaieb@29687 ` 2027` ```lemma fps_compose_power: assumes c0: "c\$0 = (0::'a::idom)" ``` chaieb@29687 ` 2028` ``` shows "(a oo c)^n = a^n oo c" (is "?l = ?r") ``` chaieb@29687 ` 2029` ```proof- ``` chaieb@29687 ` 2030` ``` {assume "n=0" then have ?thesis by simp} ``` chaieb@29687 ` 2031` ``` moreover ``` chaieb@29687 ` 2032` ``` {fix m assume m: "n = Suc m" ``` chaieb@29687 ` 2033` ``` have th0: "a^n = setprod (%k. a) {0..m}" "(a oo c) ^ n = setprod (%k. a oo c) {0..m}" ``` chaieb@29687 ` 2034` ``` by (simp_all add: setprod_constant m) ``` chaieb@29687 ` 2035` ``` then have ?thesis ``` chaieb@29687 ` 2036` ``` by (simp add: fps_compose_setprod_distrib[OF c0])} ``` chaieb@29687 ` 2037` ``` ultimately show ?thesis by (cases n, auto) ``` chaieb@29687 ` 2038` ```qed ``` chaieb@29687 ` 2039` chaieb@29687 ` 2040` ```lemma fps_const_mult_apply_left: ``` chaieb@29687 ` 2041` ``` "fps_const c * (a oo b) = (fps_const c * a) oo b" ``` chaieb@29687 ` 2042` ``` by (simp add: fps_eq_iff fps_compose_nth setsum_right_distrib mult_assoc) ``` chaieb@29687 ` 2043` chaieb@29687 ` 2044` ```lemma fps_const_mult_apply_right: ``` chaieb@29687 ` 2045` ``` "(a oo b) * fps_const (c::'a::comm_semiring_1) = (fps_const c * a) oo b" ``` chaieb@29687 ` 2046` ``` by (auto simp add: fps_const_mult_apply_left mult_commute) ``` chaieb@29687 ` 2047` huffman@30488 ` 2048` ```lemma fps_compose_assoc: ``` chaieb@29687 ` 2049` ``` assumes c0: "c\$0 = (0::'a::idom)" and b0: "b\$0 = 0" ``` chaieb@29687 ` 2050` ``` shows "a oo (b oo c) = a oo b oo c" (is "?l = ?r") ``` chaieb@29687 ` 2051` ```proof- ``` chaieb@29687 ` 2052` ``` {fix n ``` chaieb@29687 ` 2053` ``` have "?l\$n = (setsum (\i. (fps_const (a\$i) * b^i) oo c) {0..n})\$n" ``` chaieb@29687 ` 2054` ``` 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 ` 2055` ``` also have "\ = ((setsum (\i. fps_const (a\$i) * b^i) {0..n}) oo c)\$n" ``` chaieb@29687 ` 2056` ``` by (simp add: fps_compose_setsum_distrib) ``` chaieb@29687 ` 2057` ``` also have "\ = ?r\$n" ``` chaieb@29687 ` 2058` ``` apply (simp add: fps_compose_nth fps_setsum_nth setsum_left_distrib mult_assoc) ``` chaieb@29687 ` 2059` ``` apply (rule setsum_cong2) ``` chaieb@29687 ` 2060` ``` apply (rule setsum_mono_zero_right) ``` chaieb@29687 ` 2061` ``` apply (auto simp add: not_le) ``` chaieb@29687 ` 2062` ``` by (erule startsby_zero_power_prefix[OF b0, rule_format]) ``` chaieb@29687 ` 2063` ``` finally have "?l\$n = ?r\$n" .} ``` chaieb@29687 ` 2064` ``` then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2065` ```qed ``` chaieb@29687 ` 2066` chaieb@29687 ` 2067` chaieb@29687 ` 2068` ```lemma fps_X_power_compose: ``` chaieb@29687 ` 2069` ``` assumes a0: "a\$0=0" shows "X^k oo a = (a::('a::idom fps))^k" (is "?l = ?r") ``` chaieb@29687 ` 2070` ```proof- ``` chaieb@29687 ` 2071` ``` {assume "k=0" hence ?thesis by simp} ``` chaieb@29687 ` 2072` ``` moreover ``` chaieb@29687 ` 2073` ``` {fix h assume h: "k = Suc h" ``` chaieb@29687 ` 2074` ``` {fix n ``` huffman@30488 ` 2075` ``` {assume kn: "k>n" hence "?l \$ n = ?r \$n" using a0 startsby_zero_power_prefix[OF a0] h ``` huffman@30273 ` 2076` ``` by (simp add: fps_compose_nth del: power_Suc)} ``` chaieb@29687 ` 2077` ``` moreover ``` chaieb@29687 ` 2078` ``` {assume kn: "k \ n" ``` huffman@29913 ` 2079` ``` hence "?l\$n = ?r\$n" ``` huffman@29913 ` 2080` ``` by (simp add: fps_compose_nth mult_delta_left setsum_delta)} ``` chaieb@29687 ` 2081` ``` moreover have "k >n \ k\ n" by arith ``` chaieb@29687 ` 2082` ``` ultimately have "?l\$n = ?r\$n" by blast} ``` chaieb@29687 ` 2083` ``` then have ?thesis unfolding fps_eq_iff by blast} ``` chaieb@29687 ` 2084` ``` ultimately show ?thesis by (cases k, auto) ``` chaieb@29687 ` 2085` ```qed ``` chaieb@29687 ` 2086` chaieb@29687 ` 2087` ```lemma fps_inv_right: assumes a0: "a\$0 = 0" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 2088` ``` shows "a oo fps_inv a = X" ``` chaieb@29687 ` 2089` ```proof- ``` chaieb@29687 ` 2090` ``` let ?ia = "fps_inv a" ``` chaieb@29687 ` 2091` ``` let ?iaa = "a oo fps_inv a" ``` chaieb@29687 ` 2092` ``` have th0: "?ia \$ 0 = 0" by (simp add: fps_inv_def) ``` huffman@30488 ` 2093` ``` have th1: "?iaa \$ 0 = 0" using a0 a1 ``` chaieb@29687 ` 2094` ``` by (simp add: fps_inv_def fps_compose_nth) ``` chaieb@29687 ` 2095` ``` have th2: "X\$0 = 0" by simp ``` chaieb@29687 ` 2096` ``` from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X" by simp ``` chaieb@29687 ` 2097` ``` then have "(a oo fps_inv a) oo a = X oo a" ``` chaieb@29687 ` 2098` ``` by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0]) ``` chaieb@29687 ` 2099` ``` with fps_compose_inj_right[OF a0 a1] ``` huffman@30488 ` 2100` ``` show ?thesis by simp ``` chaieb@29687 ` 2101` ```qed ``` chaieb@29687 ` 2102` chaieb@29687 ` 2103` ```lemma fps_inv_deriv: ``` chaieb@29687 ` 2104` ``` assumes a0:"a\$0 = (0::'a::{recpower,field})" and a1: "a\$1 \ 0" ``` chaieb@29687 ` 2105` ``` shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)" ``` chaieb@29687 ` 2106` ```proof- ``` chaieb@29687 ` 2107` ``` let ?ia = "fps_inv a" ``` chaieb@29687 ` 2108` ``` let ?d = "fps_deriv a oo ?ia" ``` chaieb@29687 ` 2109` ``` let ?dia = "fps_deriv ?ia" ``` chaieb@29687 ` 2110` ``` have ia0: "?ia\$0 = 0" by (simp add: fps_inv_def) ``` chaieb@29687 ` 2111` ``` have th0: "?d\$0 \ 0" using a1 by (simp add: fps_compose_nth fps_deriv_nth) ``` chaieb@29687 ` 2112` ``` from fps_inv_right[OF a0 a1] have "?d * ?dia = 1" ``` chaieb@29687 ` 2113` ``` by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] ) ``` chaieb@29687 ` 2114` ``` hence "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp ``` chaieb@29687 ` 2115` ``` with inverse_mult_eq_1[OF th0] ``` chaieb@29687 ` 2116` ``` show "?dia = inverse ?d" by simp ``` chaieb@29687 ` 2117` ```qed ``` chaieb@29687 ` 2118` huffman@29906 ` 2119` ```subsection{* Elementary series *} ``` chaieb@29687 ` 2120` huffman@29906 ` 2121` ```subsubsection{* Exponential series *} ``` huffman@30488 ` 2122` ```definition "E x = Abs_fps (\n. x^n / of_nat (fact n))" ``` chaieb@29687 ` 2123` chaieb@29687 ` 2124` ```lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::{field, recpower, ring_char_0}) * E a" (is "?l = ?r") ``` chaieb@29687 ` 2125` ```proof- ``` chaieb@29687 ` 2126` ``` {fix n ``` chaieb@29687 ` 2127` ``` have "?l\$n = ?r \$ n" ``` huffman@30273 ` 2128` ``` apply (auto simp add: E_def field_simps power_Suc[symmetric]simp del: fact_Suc of_nat_Suc power_Suc) ``` chaieb@29687 ` 2129` ``` by (simp add: of_nat_mult ring_simps)} ``` chaieb@29687 ` 2130` ```then show ?thesis by (simp add: fps_eq_iff) ``` chaieb@29687 ` 2131` ```qed ``` chaieb@29687 ` 2132` huffman@30488 ` 2133` ```lemma E_unique_ODE: ``` chaieb@29687 ` 2134` ``` "fps_deriv a = fps_const c * a \ a = fps_const (a\$0) * E (c :: 'a::{field, ring_char_0, recpower})" ``` chaieb@29687 ` 2135` ``` (is "?lhs \ ?rhs") ``` chaieb@29687 ` 2136` ```proof- ``` chaieb@29687 ` 2137` ``` {assume d: ?lhs ``` huffman@30488 ` 2138` ``` from d have th: "\n. a \$ Suc n = c * a\$n / of_nat (Suc n)" ``` chaieb@29687 ` 2139` ``` by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) ``` chaieb@29687 ` 2140` ``` {fix n have "a\$n = a\$0 * c ^ n/ (of_nat (fact n))" ``` chaieb@29687 ` 2141` ``` apply (induct n) ``` chaieb@29687 ` 2142` ``` apply simp ``` huffman@30488 ` 2143` ``` unfolding th ``` chaieb@29687 ` 2144` ``` using fact_gt_zero ``` chaieb@29687 ` 2145` ``` apply (simp add: field_simps del: of_nat_Suc fact.simps) ``` chaieb@29687 ` 2146` ``` apply (drule sym) ``` chaieb@29687 ` 2147` ``` by (simp add: ring_simps of_nat_mult power_Suc)} ``` chaieb@29687 ` 2148` ``` note th' = this ``` huffman@30488 ` 2149` ``` have ?rhs ``` chaieb@29687 ` 2150` ``` by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro : th')} ``` chaieb@29687 ` 2151` ```moreover ``` chaieb@29687 ` 2152` ```{assume h: ?rhs ``` huffman@30488 ` 2153` ``` have ?lhs ``` chaieb@29687 ` 2154` ``` apply (subst h) ``` chaieb@29687 ` 2155` ``` apply simp ``` chaieb@29687 ` 2156` ``` apply (simp only: h[symmetric]) ``` chaieb@29687 ` 2157` ``` by simp} ``` chaieb@29687 ` 2158` ```ultimately show ?thesis by blast ``` chaieb@29687 ` 2159` ```qed ``` chaieb@29687 ` 2160` chaieb@29687 ` 2161` ```lemma E_add_mult: "E (a + b) = E (a::'a::{ring_char_0, field, recpower}) * E b" (is "?l = ?r") ``` chaieb@29687 ` 2162` ```proof- ``` chaieb@29687 ` 2163` ``` have "fps_deriv (?r) = fps_const (a+b) * ?r" ``` chaieb@29687 ` 2164` ``` by (simp add: fps_const_add[symmetric] ring_simps del: fps_const_add) ``` chaieb@29687 ` 2165` ``` then have "?r = ?l" apply (simp only: E_unique_ODE) ``` chaieb@29687 ` 2166` ``` by (simp add: fps_mult_nth E_def) ``` chaieb@29687 ` 2167` ``` then show ?thesis .. ``` chaieb@29687 ` 2168` ```qed ``` chaieb@29687 ` 2169` chaieb@29687 ` 2170` ```lemma E_nth[simp]: "E a \$ n = a^n / of_nat (fact n)" ``` chaieb@29687 ` 2171` ``` by (simp add: E_def) ``` chaieb@29687 ` 2172` chaieb@29687 ` 2173` ```lemma E0[simp]: "E (0::'a::{field, recpower}) = 1" ``` chaieb@29687 ` 2174` ``` by (simp add: fps_eq_iff power_0_left) ``` chaieb@29687 ` 2175` chaieb@29687 ` 2176` ```lemma E_neg: "E (- a) = inverse (E (a::'a::{ring_char_0, field, recpower}))" ``` chaieb@29687 ` 2177` ```proof- ``` chaieb@29687 ` 2178` ``` from E_add_mult[of a "- a"] have th0: "E a * E (- a) = 1" ``` chaieb@29687 ` 2179` ``` by (simp ) ``` chaieb@29687 ` 2180` ``` have th1: "E a \$ 0 \ 0" by simp ``` chaieb@29687 ` 2181` ``` from fps_inverse_unique[OF th1 th0] show ?thesis by simp ``` chaieb@29687 ` 2182` ```qed ``` chaieb@29687 ` 2183` huffman@30488 ` 2184` ```lemma E_nth_deriv[simp]: "fps_nth_deriv n (E (a::'a::{field, recpower, ring_char_0})) = (fps_const a)^n * (E a)" ``` chaieb@29687 ` 2185` ``` by (induct n, auto simp add: power_Suc) ``` chaieb@29687 ` 2186` chaieb@29687 ` 2187` ```lemma fps_compose_uminus: "- (a::'a::ring_1 fps) oo c = - (a oo c)" ``` chaieb@29687 ` 2188` ``` by (simp add: fps_eq_iff fps_compose_nth ring_simps setsum_negf[symmetric]) ``` chaieb@29687 ` 2189` huffman@30488 ` 2190` ```lemma fps_compose_sub_distrib: ``` chaieb@29687 ` 2191` ``` shows "(a - b) oo (c::'a::ring_1 fps) = (a oo c) - (b oo c)" ``` chaieb@29687 ` 2192` ``` unfolding diff_minus fps_compose_uminus fps_compose_add_distrib .. ``` chaieb@29687 ` 2193` chaieb@29687 ` 2194` ```lemma X_fps_compose:"X oo a = Abs_fps (\n. if n = 0 then (0::'a::comm_ring_1) else a\$n)" ``` huffman@29913 ` 2195` ``` by (simp add: fps_eq_iff fps_compose_nth mult_delta_left setsum_delta power_Suc) ``` chaieb@29687 ` 2196` chaieb@29687 ` 2197` ```lemma X_compose_E[simp]: "X oo E (a::'a::{field, recpower}) = E a - 1" ``` chaieb@29687 ` 2198` ``` by (simp add: fps_eq_iff X_fps_compose) ``` chaieb@29687 ` 2199` huffman@30488 ` 2200` ```lemma LE_compose: ``` huffman@30488 ` 2201` ``` assumes a: "a\0" ``` chaieb@29687 ` 2202` ``` shows "fps_inv (E a - 1) oo (E a - 1) = X" ``` chaieb@29687 ` 2203` ``` and "(E a - 1) oo fps_inv (E a - 1) = X" ``` chaieb@29687 ` 2204` ```proof- ``` chaieb@29687 ` 2205` ``` let ?b = "E a - 1" ``` chaieb@29687 ` 2206` ``` have b0: "?b \$ 0 = 0" by simp ``` chaieb@29687 ` 2207` ``` have b1: "?b \$ 1 \ 0" by (simp add: a) ``` chaieb@29687 ` 2208` ``` from fps_inv[OF b0 b1] show "fps_inv (E a - 1) oo (E a - 1) = X" . ``` chaieb@29687 ` 2209` ``` from fps_inv_right[OF b0 b1] show "(E a - 1) oo fps_inv (E a - 1) = X" . ``` chaieb@29687 ` 2210` ```qed ``` chaieb@29687 ` 2211` chaieb@29687 ` 2212` huffman@30488 ` 2213` ```lemma fps_const_inverse: ``` chaieb@29687 ` 2214` ``` "inverse (fps_const (a::'a::{field, division_by_zero})) = fps_const (inverse a)" ``` chaieb@29687 ` 2215` ``` apply (auto simp add: fps_eq_iff fps_inverse_def) by (case_tac "n", auto) ``` chaieb@29687 ` 2216` chaieb@29687 ` 2217` huffman@30488 ` 2218` ```lemma inverse_one_plus_X: ``` chaieb@29687 ` 2219` ``` "inverse (1 + X) = Abs_fps (\n. (- 1 ::'a::{field, recpower})^n)" ``` chaieb@29687 ` 2220` ``` (is "inverse ?l = ?r") ``` chaieb@29687 ` 2221` ```proof- ``` chaieb@29687 ` 2222` ``` have th: "?l * ?r = 1" ``` chaieb@29687 ` 2223` ``` apply (auto simp add: ring_simps fps_eq_iff X_mult_nth minus_one_power_iff) ``` chaieb@29687 ` 2224` ``` apply presburger+ ``` chaieb@29687 ` 2225` ``` done ``` chaieb@29687 ` 2226` ``` have th': "?l \$ 0 \ 0" by (simp add: ) ``` chaieb@29687 ` 2227` ``` from fps_inverse_unique[OF th' th] show ?thesis . ``` chaieb@29687 ` 2228` ```qed ``` chaieb@29687 ` 2229` chaieb@29687 ` 2230` ```lemma E_power_mult: "(E (c::'a::{field,recpower,ring_char_0}))^n = E (of_nat n * c)" ``` chaieb@29687 ` 2231` ``` by (induct n, auto simp add: ring_simps E_add_mult power_Suc) ``` chaieb@29687 ` 2232` huffman@30488 ` 2233` ```subsubsection{* Logarithmic series *} ``` huffman@30488 ` 2234` ```definition "(L::'a::{field, ring_char_0,recpower} fps) ``` chaieb@29687 ` 2235` ``` = Abs_fps (\n. (- 1) ^ Suc n / of_nat n)" ``` chaieb@29687 ` 2236` chaieb@29687 ` 2237` ```lemma fps_deriv_L: "fps_deriv L = inverse (1 + X)" ``` chaieb@29687 ` 2238` ``` unfolding inverse_one_plus_X ``` chaieb@29687 ` 2239` ``` by (simp add: L_def fps_eq_iff power_Suc del: of_nat_Suc) ``` chaieb@29687 ` 2240` chaieb@29687 ` 2241` ```lemma L_nth: "L \$ n = (- 1) ^ Suc n / of_nat n" ``` chaieb@29687 ` 2242` ``` by (simp add: L_def) ``` chaieb@29687 ` 2243` chaieb@29687 ` 2244` ```lemma L_E_inv: ``` huffman@30488 ` 2245` ``` assumes a: "a\ (0::'a::{field,division_by_zero,ring_char_0,recpower})" ``` chaieb@29687 ` 2246` ``` shows "L = fps_const a * fps_inv (E a - 1)" (is "?l = ?r") ``` chaieb@29687 ` 2247` ```proof- ``` chaieb@29687 ` 2248` ``` let ?b = "E a - 1" ``` chaieb@29687 ` 2249` ``` have b0: "?b \$ 0 = 0" by simp ``` chaieb@29687 ` 2250` ``` have b1: "?b \$ 1 \ 0" by (simp add: a) ``` chaieb@29687 ` 2251` ``` have "fps_deriv (E a - 1) oo fps_inv (E a - 1) = (fps_const a * (E a - 1) + fps_const a) oo fps_inv (E a - 1)" ``` chaieb@29687 ` 2252` ``` by (simp add: ring_simps) ``` chaieb@29687 ` 2253` ``` also have "\ = fps_const a * (X + 1)" apply (simp add: fps_compose_add_distrib fps_const_mult_apply_left[symmetric] fps_inv_right[OF b0 b1]) ``` chaieb@29687 ` 2254` ``` by (simp add: ring_simps) ``` chaieb@29687 ` 2255` ``` finally have eq: "fps_deriv (E a - 1) oo fps_inv (E a - 1) = fps_const a * (X + 1)" . ``` chaieb@29687 ` 2256` ``` from fps_inv_deriv[OF b0 b1, unfolded eq] ``` chaieb@29687 ` 2257` ``` have "fps_deriv (fps_inv ?b) = fps_const (inverse a) / (X + 1)" ``` chaieb@29687 ` 2258` ``` by (simp add: fps_const_inverse eq fps_divide_def fps_inverse_mult) ``` chaieb@29687 ` 2259` ``` hence "fps_deriv (fps_const a * fps_inv ?b) = inverse (X + 1)" ``` chaieb@29687 ` 2260` ``` using a by (simp add: fps_divide_def field_simps) ``` huffman@30488 ` 2261` ``` hence "fps_deriv ?l = fps_deriv ?r" ``` chaieb@29687 ` 2262` ``` by (simp add: fps_deriv_L add_commute) ``` chaieb@29687 ` 2263` ``` then show ?thesis unfolding fps_deriv_eq_iff ``` chaieb@29687 ` 2264` ``` by (simp add: L_nth fps_inv_def) ``` chaieb@29687 ` 2265` ```qed ``` chaieb@29687 ` 2266` huffman@29906 ` 2267` ```subsubsection{* Formal trigonometric functions *} ``` chaieb@29687 ` 2268` huffman@30488 ` 2269` ```definition "fps_sin (c::'a::{field, recpower, ring_char_0}) = ``` chaieb@29687 ` 2270` ``` Abs_fps (\n. if even n then 0 else (- 1) ^((n - 1) div 2) * c^n /(of_nat (fact n)))" ``` chaieb@29687 ` 2271` chaieb@29687 ` 2272` ```definition "fps_cos (c::'a::{field, recpower, ring_char_0}) = Abs_fps (\n. if even n then (- 1) ^ (n div 2) * c^n / (of_nat (fact n)) else 0)" ``` chaieb@29687 ` 2273` huffman@30488 ` 2274` ```lemma fps_sin_deriv: ``` chaieb@29687 ` 2275` ``` "fps_deriv (fps_sin c) = fps_const c * fps_cos c" ``` chaieb@29687 ` 2276` ``` (is "?lhs = ?rhs") ``` chaieb@29687 ` 2277` ```proof- ``` chaieb@29687 ` 2278` ``` {fix n::nat ``` chaieb@29687 ` 2279` ``` {assume en: "even n" ``` chaieb@29687 ` 2280` ``` have "?lhs\$n = of_nat (n+1) * (fps_sin c \$ (n+1))" by simp ``` huffman@30488 ` 2281` ``` also have "\ = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))" ``` chaieb@29687 ` 2282` ``` using en by (simp add: fps_sin_def) ``` chaieb@29687 ` 2283` ``` also have "\ = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" ``` chaieb@29687 ` 2284` ``` unfolding fact_Suc of_nat_mult ``` chaieb@29687 ` 2285` ``` by (simp add: field_simps del: of_nat_add of_nat_Suc) ``` chaieb@29687 ` 2286` ``` also have "\ = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)" ``` chaieb@29687 ` 2287` ``` by (simp add: field_simps del: of_nat_add of_nat_Suc) ``` huffman@30488 ` 2288` ``` finally have "?lhs \$n = ?rhs\$n" using en ``` chaieb@29687 ` 2289` ``` by (simp add: fps_cos_def ring_simps power_Suc )} ``` huffman@30488 ` 2290` ``` then have "?lhs \$ n = ?rhs \$ n" ``` chaieb@29687 ` 2291` ``` by (cases "even n", simp_all add: fps_deriv_def fps_sin_def fps_cos_def) } ``` chaieb@29687 ` 2292` ``` then show ?thesis by (auto simp add: fps_eq_iff) ``` chaieb@29687 ` 2293` ```qed ``` chaieb@29687 ` 2294` huffman@30488 ` 2295` ```lemma fps_cos_deriv: ``` chaieb@29687 ` 2296` ``` "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)" ``` chaieb@29687 ` 2297` ``` (is "?lhs = ?rhs") ``` chaieb@29687 ` 2298` ```proof- ``` chaieb@29687 ` 2299` ``` have th0: "\n. - ((- 1::'a) ^ n) = (- 1)^Suc n" by (simp add: power_Suc) ``` huffman@29911 ` 2300` ``` have th1: "\n. odd n\ Suc ((n - 1) div 2) = Suc n div 2" by presburger (* FIXME: VERY slow! *) ``` chaieb@29687 ` 2301` ``` {fix n::nat ``` chaieb@29687 ` 2302` ``` {assume en: "odd n" ``` chaieb@29687 ` 2303` ``` from en have n0: "n \0 " by presburger ``` chaieb@29687 ` 2304` ``` have "?lhs\$n = of_nat (n+1) * (fps_cos c \$ (n+1))" by simp ``` huffman@30488 ` 2305` ``` also have "\ = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))" ``` chaieb@29687 ` 2306` ``` using en by (simp add: fps_cos_def) ``` chaieb@29687 ` 2307` ``` also have "\ = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" ``` chaieb@29687 ` 2308` ``` unfolding fact_Suc of_nat_mult ``` chaieb@29687 ` 2309` ``` by (simp add: field_simps del: of_nat_add of_nat_Suc) ``` chaieb@29687 ` 2310` ``` also have "\ = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" ``` chaieb@29687 ` 2311` ``` by (simp add: field_simps del: of_nat_add of_nat_Suc) ``` chaieb@29687 ` 2312` ``` also have "\ = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" ``` chaieb@29687 ` 2313` ``` unfolding th0 unfolding th1[OF en] by simp ``` huffman@30488 ` 2314` ``` finally have "?lhs \$n = ?rhs\$n" using en ``` huffman@29911 ` 2315` ``` by (simp add: fps_sin_def ring_simps power_Suc)} ``` huffman@30488 ` 2316` ``` then have "?lhs \$ n = ?rhs \$ n" ``` huffman@30488 ` 2317` ``` by (cases "even n", simp_all add: fps_deriv_def fps_sin_def ``` huffman@29911 ` 2318` ``` fps_cos_def) } ``` chaieb@29687 ` 2319` ``` then show ?thesis by (auto simp add: fps_eq_iff) ``` chaieb@29687 ` 2320` ```qed ``` chaieb@29687 ` 2321` chaieb@29687 ` 2322` ```lemma fps_sin_cos_sum_of_squares: ``` chaieb@29687 ` 2323` ``` "fps_cos c ^ 2 + fps_sin c ^ 2 = 1" (is "?lhs = 1") ``` chaieb@29687 ` 2324` ```proof- ``` chaieb@29687 ` 2325` ``` have "fps_deriv ?lhs = 0" ``` chaieb@29687 ` 2326` ``` apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv power_Suc) ``` haftmann@30960 ` 2327` ``` by (simp add: ring_simps fps_const_neg[symmetric] del: fps_const_neg) ``` chaieb@29687 ` 2328` ``` then have "?lhs = fps_const (?lhs \$ 0)" ``` chaieb@29687 ` 2329` ``` unfolding fps_deriv_eq_0_iff . ``` chaieb@29687 ` 2330` ``` also have "\ = 1" ``` haftmann@30960 ` 2331` ``` by (auto simp add: fps_eq_iff numeral_2_eq_2 fps_mult_nth fps_cos_def fps_sin_def) ``` chaieb@29687 ` 2332` ``` finally show ?thesis . ``` chaieb@29687 ` 2333` ```qed ``` chaieb@29687 ` 2334` chaieb@29687 ` 2335` ```definition "fps_tan c = fps_sin c / fps_cos c" ``` chaieb@29687 ` 2336` chaieb@29687 ` 2337` ```lemma fps_tan_deriv: "fps_deriv(fps_tan c) = fps_const c/ (fps_cos c ^ 2)" ``` chaieb@29687 ` 2338` ```proof- ``` chaieb@29687 ` 2339` ``` have th0: "fps_cos c \$ 0 \ 0" by (simp add: fps_cos_def) ``` huffman@30488 ` 2340` ``` show ?thesis ``` chaieb@29687 ` 2341` ``` using fps_sin_cos_sum_of_squares[of c] ``` chaieb@29687 ` 2342` ``` apply (simp add: fps_tan_def fps_divide_deriv[OF th0] fps_sin_deriv fps_cos_deriv add: fps_const_neg[symmetric] ring_simps power2_eq_square del: fps_const_neg) ``` chaieb@29687 ` 2343` ``` unfolding right_distrib[symmetric] ``` chaieb@29687 ` 2344` ``` by simp ``` chaieb@29687 ` 2345` ```qed ``` huffman@29911 ` 2346` huffman@29911 ` 2347` ```end ```