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