src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 author wenzelm Thu Nov 05 10:39:59 2015 +0100 (2015-11-05) changeset 61586 5197a2ecb658 parent 61166 5976fe402824 child 62390 842917225d56 permissions -rw-r--r--
isabelle update_cartouches -c -t;
 chaieb@33154 ` 1` ```(* Title: HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy ``` chaieb@33154 ` 2` ``` Author: Amine Chaieb ``` chaieb@33154 ` 3` ```*) ``` chaieb@33154 ` 4` wenzelm@60533 ` 5` ```section \Implementation and verification of multivariate polynomials\ ``` chaieb@33154 ` 6` chaieb@33154 ` 7` ```theory Reflected_Multivariate_Polynomial ``` haftmann@54220 ` 8` ```imports Complex_Main Rat_Pair Polynomial_List ``` chaieb@33154 ` 9` ```begin ``` chaieb@33154 ` 10` wenzelm@60698 ` 11` ```subsection \Datatype of polynomial expressions\ ``` chaieb@33154 ` 12` blanchet@58310 ` 13` ```datatype poly = C Num | Bound nat | Add poly poly | Sub poly poly ``` chaieb@33154 ` 14` ``` | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly ``` chaieb@33154 ` 15` wenzelm@35054 ` 16` ```abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)" ``` wenzelm@50282 ` 17` ```abbreviation poly_p :: "int \ poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \ C (i)\<^sub>N" ``` chaieb@33154 ` 18` wenzelm@52658 ` 19` wenzelm@60533 ` 20` ```subsection\Boundedness, substitution and all that\ ``` wenzelm@52658 ` 21` wenzelm@52658 ` 22` ```primrec polysize:: "poly \ nat" ``` wenzelm@52658 ` 23` ```where ``` chaieb@33154 ` 24` ``` "polysize (C c) = 1" ``` haftmann@39246 ` 25` ```| "polysize (Bound n) = 1" ``` haftmann@39246 ` 26` ```| "polysize (Neg p) = 1 + polysize p" ``` haftmann@39246 ` 27` ```| "polysize (Add p q) = 1 + polysize p + polysize q" ``` haftmann@39246 ` 28` ```| "polysize (Sub p q) = 1 + polysize p + polysize q" ``` haftmann@39246 ` 29` ```| "polysize (Mul p q) = 1 + polysize p + polysize q" ``` haftmann@39246 ` 30` ```| "polysize (Pw p n) = 1 + polysize p" ``` haftmann@39246 ` 31` ```| "polysize (CN c n p) = 4 + polysize c + polysize p" ``` chaieb@33154 ` 32` wenzelm@61586 ` 33` ```primrec polybound0:: "poly \ bool" \ \a poly is INDEPENDENT of Bound 0\ ``` wenzelm@52658 ` 34` ```where ``` wenzelm@56000 ` 35` ``` "polybound0 (C c) \ True" ``` wenzelm@56000 ` 36` ```| "polybound0 (Bound n) \ n > 0" ``` wenzelm@56000 ` 37` ```| "polybound0 (Neg a) \ polybound0 a" ``` wenzelm@56000 ` 38` ```| "polybound0 (Add a b) \ polybound0 a \ polybound0 b" ``` wenzelm@56000 ` 39` ```| "polybound0 (Sub a b) \ polybound0 a \ polybound0 b" ``` wenzelm@56000 ` 40` ```| "polybound0 (Mul a b) \ polybound0 a \ polybound0 b" ``` wenzelm@56000 ` 41` ```| "polybound0 (Pw p n) \ polybound0 p" ``` wenzelm@56000 ` 42` ```| "polybound0 (CN c n p) \ n \ 0 \ polybound0 c \ polybound0 p" ``` haftmann@39246 ` 43` wenzelm@61586 ` 44` ```primrec polysubst0:: "poly \ poly \ poly" \ \substitute a poly into a poly for Bound 0\ ``` wenzelm@52658 ` 45` ```where ``` wenzelm@56000 ` 46` ``` "polysubst0 t (C c) = C c" ``` wenzelm@56000 ` 47` ```| "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)" ``` haftmann@39246 ` 48` ```| "polysubst0 t (Neg a) = Neg (polysubst0 t a)" ``` haftmann@39246 ` 49` ```| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" ``` wenzelm@52803 ` 50` ```| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" ``` haftmann@39246 ` 51` ```| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" ``` haftmann@39246 ` 52` ```| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" ``` wenzelm@56000 ` 53` ```| "polysubst0 t (CN c n p) = ``` wenzelm@56000 ` 54` ``` (if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) ``` wenzelm@56000 ` 55` ``` else CN (polysubst0 t c) n (polysubst0 t p))" ``` chaieb@33154 ` 56` wenzelm@52803 ` 57` ```fun decrpoly:: "poly \ poly" ``` krauss@41808 ` 58` ```where ``` chaieb@33154 ` 59` ``` "decrpoly (Bound n) = Bound (n - 1)" ``` krauss@41808 ` 60` ```| "decrpoly (Neg a) = Neg (decrpoly a)" ``` krauss@41808 ` 61` ```| "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" ``` krauss@41808 ` 62` ```| "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)" ``` krauss@41808 ` 63` ```| "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)" ``` krauss@41808 ` 64` ```| "decrpoly (Pw p n) = Pw (decrpoly p) n" ``` krauss@41808 ` 65` ```| "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)" ``` krauss@41808 ` 66` ```| "decrpoly a = a" ``` chaieb@33154 ` 67` wenzelm@52658 ` 68` wenzelm@60698 ` 69` ```subsection \Degrees and heads and coefficients\ ``` chaieb@33154 ` 70` wenzelm@56207 ` 71` ```fun degree :: "poly \ nat" ``` krauss@41808 ` 72` ```where ``` chaieb@33154 ` 73` ``` "degree (CN c 0 p) = 1 + degree p" ``` krauss@41808 ` 74` ```| "degree p = 0" ``` chaieb@33154 ` 75` wenzelm@56207 ` 76` ```fun head :: "poly \ poly" ``` krauss@41808 ` 77` ```where ``` chaieb@33154 ` 78` ``` "head (CN c 0 p) = head p" ``` krauss@41808 ` 79` ```| "head p = p" ``` krauss@41808 ` 80` wenzelm@60698 ` 81` ```text \More general notions of degree and head.\ ``` wenzelm@60698 ` 82` wenzelm@56207 ` 83` ```fun degreen :: "poly \ nat \ nat" ``` krauss@41808 ` 84` ```where ``` wenzelm@56000 ` 85` ``` "degreen (CN c n p) = (\m. if n = m then 1 + degreen p n else 0)" ``` wenzelm@56000 ` 86` ```| "degreen p = (\m. 0)" ``` chaieb@33154 ` 87` wenzelm@56207 ` 88` ```fun headn :: "poly \ nat \ poly" ``` krauss@41808 ` 89` ```where ``` krauss@41808 ` 90` ``` "headn (CN c n p) = (\m. if n \ m then headn p m else CN c n p)" ``` krauss@41808 ` 91` ```| "headn p = (\m. p)" ``` chaieb@33154 ` 92` wenzelm@56207 ` 93` ```fun coefficients :: "poly \ poly list" ``` krauss@41808 ` 94` ```where ``` wenzelm@56000 ` 95` ``` "coefficients (CN c 0 p) = c # coefficients p" ``` krauss@41808 ` 96` ```| "coefficients p = [p]" ``` chaieb@33154 ` 97` wenzelm@56207 ` 98` ```fun isconstant :: "poly \ bool" ``` krauss@41808 ` 99` ```where ``` krauss@41808 ` 100` ``` "isconstant (CN c 0 p) = False" ``` krauss@41808 ` 101` ```| "isconstant p = True" ``` chaieb@33154 ` 102` wenzelm@56207 ` 103` ```fun behead :: "poly \ poly" ``` krauss@41808 ` 104` ```where ``` krauss@41808 ` 105` ``` "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')" ``` krauss@41808 ` 106` ```| "behead p = 0\<^sub>p" ``` krauss@41808 ` 107` wenzelm@56207 ` 108` ```fun headconst :: "poly \ Num" ``` krauss@41808 ` 109` ```where ``` chaieb@33154 ` 110` ``` "headconst (CN c n p) = headconst p" ``` krauss@41808 ` 111` ```| "headconst (C n) = n" ``` chaieb@33154 ` 112` wenzelm@52658 ` 113` wenzelm@60698 ` 114` ```subsection \Operations for normalization\ ``` krauss@41812 ` 115` krauss@41812 ` 116` ```declare if_cong[fundef_cong del] ``` krauss@41812 ` 117` ```declare let_cong[fundef_cong del] ``` krauss@41812 ` 118` krauss@41812 ` 119` ```fun polyadd :: "poly \ poly \ poly" (infixl "+\<^sub>p" 60) ``` krauss@41812 ` 120` ```where ``` wenzelm@56000 ` 121` ``` "polyadd (C c) (C c') = C (c +\<^sub>N c')" ``` wenzelm@52803 ` 122` ```| "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" ``` krauss@41812 ` 123` ```| "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" ``` krauss@41812 ` 124` ```| "polyadd (CN c n p) (CN c' n' p') = ``` krauss@41812 ` 125` ``` (if n < n' then CN (polyadd c (CN c' n' p')) n p ``` wenzelm@56000 ` 126` ``` else if n' < n then CN (polyadd (CN c n p) c') n' p' ``` wenzelm@56000 ` 127` ``` else ``` wenzelm@56000 ` 128` ``` let ``` wenzelm@56000 ` 129` ``` cc' = polyadd c c'; ``` wenzelm@56000 ` 130` ``` pp' = polyadd p p' ``` wenzelm@56000 ` 131` ``` in if pp' = 0\<^sub>p then cc' else CN cc' n pp')" ``` krauss@41812 ` 132` ```| "polyadd a b = Add a b" ``` krauss@41812 ` 133` chaieb@33154 ` 134` krauss@41808 ` 135` ```fun polyneg :: "poly \ poly" ("~\<^sub>p") ``` krauss@41808 ` 136` ```where ``` chaieb@33154 ` 137` ``` "polyneg (C c) = C (~\<^sub>N c)" ``` krauss@41808 ` 138` ```| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)" ``` krauss@41808 ` 139` ```| "polyneg a = Neg a" ``` chaieb@33154 ` 140` krauss@41814 ` 141` ```definition polysub :: "poly \ poly \ poly" (infixl "-\<^sub>p" 60) ``` wenzelm@52658 ` 142` ``` where "p -\<^sub>p q = polyadd p (polyneg q)" ``` krauss@41813 ` 143` krauss@41813 ` 144` ```fun polymul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60) ``` krauss@41813 ` 145` ```where ``` wenzelm@56043 ` 146` ``` "polymul (C c) (C c') = C (c *\<^sub>N c')" ``` wenzelm@52803 ` 147` ```| "polymul (C c) (CN c' n' p') = ``` wenzelm@56000 ` 148` ``` (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" ``` wenzelm@52803 ` 149` ```| "polymul (CN c n p) (C c') = ``` wenzelm@56000 ` 150` ``` (if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))" ``` wenzelm@52803 ` 151` ```| "polymul (CN c n p) (CN c' n' p') = ``` wenzelm@56000 ` 152` ``` (if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p')) ``` wenzelm@56000 ` 153` ``` else if n' < n then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p') ``` wenzelm@56000 ` 154` ``` else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))" ``` krauss@41813 ` 155` ```| "polymul a b = Mul a b" ``` krauss@41808 ` 156` krauss@41812 ` 157` ```declare if_cong[fundef_cong] ``` krauss@41812 ` 158` ```declare let_cong[fundef_cong] ``` krauss@41812 ` 159` krauss@41808 ` 160` ```fun polypow :: "nat \ poly \ poly" ``` krauss@41808 ` 161` ```where ``` wenzelm@50282 ` 162` ``` "polypow 0 = (\p. (1)\<^sub>p)" ``` wenzelm@56000 ` 163` ```| "polypow n = ``` wenzelm@56000 ` 164` ``` (\p. ``` wenzelm@56000 ` 165` ``` let ``` wenzelm@56000 ` 166` ``` q = polypow (n div 2) p; ``` wenzelm@56000 ` 167` ``` d = polymul q q ``` wenzelm@56000 ` 168` ``` in if even n then d else polymul p d)" ``` chaieb@33154 ` 169` wenzelm@35054 ` 170` ```abbreviation poly_pow :: "poly \ nat \ poly" (infixl "^\<^sub>p" 60) ``` wenzelm@35054 ` 171` ``` where "a ^\<^sub>p k \ polypow k a" ``` chaieb@33154 ` 172` krauss@41808 ` 173` ```function polynate :: "poly \ poly" ``` krauss@41808 ` 174` ```where ``` wenzelm@50282 ` 175` ``` "polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p" ``` wenzelm@56000 ` 176` ```| "polynate (Add p q) = polynate p +\<^sub>p polynate q" ``` wenzelm@56000 ` 177` ```| "polynate (Sub p q) = polynate p -\<^sub>p polynate q" ``` wenzelm@56000 ` 178` ```| "polynate (Mul p q) = polynate p *\<^sub>p polynate q" ``` wenzelm@56000 ` 179` ```| "polynate (Neg p) = ~\<^sub>p (polynate p)" ``` wenzelm@56000 ` 180` ```| "polynate (Pw p n) = polynate p ^\<^sub>p n" ``` krauss@41808 ` 181` ```| "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" ``` krauss@41808 ` 182` ```| "polynate (C c) = C (normNum c)" ``` wenzelm@60698 ` 183` ``` by pat_completeness auto ``` krauss@41808 ` 184` ```termination by (relation "measure polysize") auto ``` chaieb@33154 ` 185` wenzelm@52658 ` 186` ```fun poly_cmul :: "Num \ poly \ poly" ``` wenzelm@52658 ` 187` ```where ``` chaieb@33154 ` 188` ``` "poly_cmul y (C x) = C (y *\<^sub>N x)" ``` chaieb@33154 ` 189` ```| "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" ``` chaieb@33154 ` 190` ```| "poly_cmul y p = C y *\<^sub>p p" ``` chaieb@33154 ` 191` wenzelm@56009 ` 192` ```definition monic :: "poly \ poly \ bool" ``` wenzelm@56000 ` 193` ```where ``` wenzelm@56000 ` 194` ``` "monic p = ``` wenzelm@56000 ` 195` ``` (let h = headconst p ``` wenzelm@56000 ` 196` ``` in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))" ``` chaieb@33154 ` 197` wenzelm@52658 ` 198` wenzelm@60533 ` 199` ```subsection \Pseudo-division\ ``` chaieb@33154 ` 200` wenzelm@52658 ` 201` ```definition shift1 :: "poly \ poly" ``` wenzelm@56000 ` 202` ``` where "shift1 p = CN 0\<^sub>p 0 p" ``` chaieb@33154 ` 203` wenzelm@56009 ` 204` ```abbreviation funpow :: "nat \ ('a \ 'a) \ 'a \ 'a" ``` wenzelm@52658 ` 205` ``` where "funpow \ compow" ``` haftmann@39246 ` 206` krauss@41403 ` 207` ```partial_function (tailrec) polydivide_aux :: "poly \ nat \ poly \ nat \ poly \ nat \ poly" ``` wenzelm@52658 ` 208` ```where ``` wenzelm@52803 ` 209` ``` "polydivide_aux a n p k s = ``` wenzelm@56000 ` 210` ``` (if s = 0\<^sub>p then (k, s) ``` wenzelm@52803 ` 211` ``` else ``` wenzelm@56000 ` 212` ``` let ``` wenzelm@56000 ` 213` ``` b = head s; ``` wenzelm@56000 ` 214` ``` m = degree s ``` wenzelm@56000 ` 215` ``` in ``` wenzelm@56000 ` 216` ``` if m < n then (k,s) ``` wenzelm@56000 ` 217` ``` else ``` wenzelm@56000 ` 218` ``` let p' = funpow (m - n) shift1 p ``` wenzelm@56000 ` 219` ``` in ``` wenzelm@56000 ` 220` ``` if a = b then polydivide_aux a n p k (s -\<^sub>p p') ``` wenzelm@56000 ` 221` ``` else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))" ``` chaieb@33154 ` 222` wenzelm@56000 ` 223` ```definition polydivide :: "poly \ poly \ nat \ poly" ``` wenzelm@56000 ` 224` ``` where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s" ``` chaieb@33154 ` 225` wenzelm@52658 ` 226` ```fun poly_deriv_aux :: "nat \ poly \ poly" ``` wenzelm@52658 ` 227` ```where ``` chaieb@33154 ` 228` ``` "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)" ``` chaieb@33154 ` 229` ```| "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p" ``` chaieb@33154 ` 230` wenzelm@52658 ` 231` ```fun poly_deriv :: "poly \ poly" ``` wenzelm@52658 ` 232` ```where ``` chaieb@33154 ` 233` ``` "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" ``` chaieb@33154 ` 234` ```| "poly_deriv p = 0\<^sub>p" ``` chaieb@33154 ` 235` wenzelm@52658 ` 236` wenzelm@60698 ` 237` ```subsection \Semantics of the polynomial representation\ ``` chaieb@33154 ` 238` haftmann@59867 ` 239` ```primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0,field,power}" ``` wenzelm@56000 ` 240` ```where ``` chaieb@33154 ` 241` ``` "Ipoly bs (C c) = INum c" ``` haftmann@39246 ` 242` ```| "Ipoly bs (Bound n) = bs!n" ``` haftmann@39246 ` 243` ```| "Ipoly bs (Neg a) = - Ipoly bs a" ``` haftmann@39246 ` 244` ```| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b" ``` haftmann@39246 ` 245` ```| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b" ``` haftmann@39246 ` 246` ```| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b" ``` wenzelm@56000 ` 247` ```| "Ipoly bs (Pw t n) = Ipoly bs t ^ n" ``` wenzelm@56000 ` 248` ```| "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p" ``` haftmann@39246 ` 249` wenzelm@60698 ` 250` ```abbreviation Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0,field,power}" ("\_\\<^sub>p\<^bsup>_\<^esup>") ``` wenzelm@35054 ` 251` ``` where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p" ``` chaieb@33154 ` 252` wenzelm@56009 ` 253` ```lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" ``` chaieb@33154 ` 254` ``` by (simp add: INum_def) ``` wenzelm@56000 ` 255` wenzelm@52803 ` 256` ```lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" ``` chaieb@33154 ` 257` ``` by (simp add: INum_def) ``` chaieb@33154 ` 258` chaieb@33154 ` 259` ```lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat ``` chaieb@33154 ` 260` wenzelm@52658 ` 261` wenzelm@60533 ` 262` ```subsection \Normal form and normalization\ ``` chaieb@33154 ` 263` krauss@41808 ` 264` ```fun isnpolyh:: "poly \ nat \ bool" ``` krauss@41808 ` 265` ```where ``` chaieb@33154 ` 266` ``` "isnpolyh (C c) = (\k. isnormNum c)" ``` wenzelm@56000 ` 267` ```| "isnpolyh (CN c n p) = (\k. n \ k \ isnpolyh c (Suc n) \ isnpolyh p n \ p \ 0\<^sub>p)" ``` krauss@41808 ` 268` ```| "isnpolyh p = (\k. False)" ``` chaieb@33154 ` 269` wenzelm@56000 ` 270` ```lemma isnpolyh_mono: "n' \ n \ isnpolyh p n \ isnpolyh p n'" ``` wenzelm@52658 ` 271` ``` by (induct p rule: isnpolyh.induct) auto ``` chaieb@33154 ` 272` wenzelm@52658 ` 273` ```definition isnpoly :: "poly \ bool" ``` wenzelm@56000 ` 274` ``` where "isnpoly p = isnpolyh p 0" ``` chaieb@33154 ` 275` wenzelm@60698 ` 276` ```text \polyadd preserves normal forms\ ``` chaieb@33154 ` 277` wenzelm@56000 ` 278` ```lemma polyadd_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polyadd p q) (min n0 n1)" ``` wenzelm@52803 ` 279` ```proof (induct p q arbitrary: n0 n1 rule: polyadd.induct) ``` krauss@41812 ` 280` ``` case (2 ab c' n' p' n0 n1) ``` wenzelm@56009 ` 281` ``` from 2 have th1: "isnpolyh (C ab) (Suc n')" ``` wenzelm@56009 ` 282` ``` by simp ``` wenzelm@60698 ` 283` ``` from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" ``` wenzelm@56009 ` 284` ``` by simp_all ``` wenzelm@56009 ` 285` ``` with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 286` ``` by simp ``` wenzelm@56009 ` 287` ``` with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" ``` wenzelm@56009 ` 288` ``` by simp ``` wenzelm@56009 ` 289` ``` from nplen1 have n01len1: "min n0 n1 \ n'" ``` wenzelm@56009 ` 290` ``` by simp ``` wenzelm@56009 ` 291` ``` then show ?case using 2 th3 ``` wenzelm@56009 ` 292` ``` by simp ``` chaieb@33154 ` 293` ```next ``` krauss@41812 ` 294` ``` case (3 c' n' p' ab n1 n0) ``` wenzelm@56009 ` 295` ``` from 3 have th1: "isnpolyh (C ab) (Suc n')" ``` wenzelm@56009 ` 296` ``` by simp ``` wenzelm@56009 ` 297` ``` from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" ``` wenzelm@56009 ` 298` ``` by simp_all ``` wenzelm@56009 ` 299` ``` with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 300` ``` by simp ``` wenzelm@56009 ` 301` ``` with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" ``` wenzelm@56009 ` 302` ``` by simp ``` wenzelm@56009 ` 303` ``` from nplen1 have n01len1: "min n0 n1 \ n'" ``` wenzelm@56009 ` 304` ``` by simp ``` wenzelm@56009 ` 305` ``` then show ?case using 3 th3 ``` wenzelm@56009 ` 306` ``` by simp ``` chaieb@33154 ` 307` ```next ``` chaieb@33154 ` 308` ``` case (4 c n p c' n' p' n0 n1) ``` wenzelm@56009 ` 309` ``` then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" ``` wenzelm@56009 ` 310` ``` by simp_all ``` wenzelm@56009 ` 311` ``` from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" ``` wenzelm@56009 ` 312` ``` by simp_all ``` wenzelm@56009 ` 313` ``` from 4 have ngen0: "n \ n0" ``` wenzelm@56009 ` 314` ``` by simp ``` wenzelm@56009 ` 315` ``` from 4 have n'gen1: "n' \ n1" ``` wenzelm@56009 ` 316` ``` by simp ``` wenzelm@60698 ` 317` ``` consider (eq) "n = n'" | (lt) "n < n'" | (gt) "n > n'" ``` wenzelm@60698 ` 318` ``` by arith ``` wenzelm@60698 ` 319` ``` then show ?case ``` wenzelm@60698 ` 320` ``` proof cases ``` wenzelm@60698 ` 321` ``` case eq ``` wenzelm@52803 ` 322` ``` with "4.hyps"(3)[OF nc nc'] ``` wenzelm@56009 ` 323` ``` have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" ``` wenzelm@56009 ` 324` ``` by auto ``` wenzelm@56009 ` 325` ``` then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" ``` wenzelm@56009 ` 326` ``` using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 ``` wenzelm@56009 ` 327` ``` by auto ``` wenzelm@56009 ` 328` ``` from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" ``` wenzelm@56009 ` 329` ``` by simp ``` wenzelm@56009 ` 330` ``` have minle: "min n0 n1 \ n'" ``` wenzelm@56009 ` 331` ``` using ngen0 n'gen1 eq by simp ``` wenzelm@60698 ` 332` ``` from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' show ?thesis ``` wenzelm@56009 ` 333` ``` by (simp add: Let_def) ``` wenzelm@60698 ` 334` ``` next ``` wenzelm@60698 ` 335` ``` case lt ``` wenzelm@56009 ` 336` ``` have "min n0 n1 \ n0" ``` wenzelm@56009 ` 337` ``` by simp ``` wenzelm@56009 ` 338` ``` with 4 lt have th1:"min n0 n1 \ n" ``` wenzelm@56009 ` 339` ``` by auto ``` wenzelm@56009 ` 340` ``` from 4 have th21: "isnpolyh c (Suc n)" ``` wenzelm@56009 ` 341` ``` by simp ``` wenzelm@56009 ` 342` ``` from 4 have th22: "isnpolyh (CN c' n' p') n'" ``` wenzelm@56009 ` 343` ``` by simp ``` wenzelm@56009 ` 344` ``` from lt have th23: "min (Suc n) n' = Suc n" ``` wenzelm@56009 ` 345` ``` by arith ``` wenzelm@56009 ` 346` ``` from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" ``` wenzelm@56009 ` 347` ``` using th23 by simp ``` wenzelm@60698 ` 348` ``` with 4 lt th1 show ?thesis ``` wenzelm@56009 ` 349` ``` by simp ``` wenzelm@60698 ` 350` ``` next ``` wenzelm@60698 ` 351` ``` case gt ``` wenzelm@56009 ` 352` ``` then have gt': "n' < n \ \ n < n'" ``` wenzelm@56009 ` 353` ``` by simp ``` wenzelm@56009 ` 354` ``` have "min n0 n1 \ n1" ``` wenzelm@56009 ` 355` ``` by simp ``` wenzelm@56009 ` 356` ``` with 4 gt have th1: "min n0 n1 \ n'" ``` wenzelm@56009 ` 357` ``` by auto ``` wenzelm@56009 ` 358` ``` from 4 have th21: "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 359` ``` by simp_all ``` wenzelm@56009 ` 360` ``` from 4 have th22: "isnpolyh (CN c n p) n" ``` wenzelm@56009 ` 361` ``` by simp ``` wenzelm@56009 ` 362` ``` from gt have th23: "min n (Suc n') = Suc n'" ``` wenzelm@56009 ` 363` ``` by arith ``` wenzelm@56009 ` 364` ``` from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')" ``` wenzelm@56009 ` 365` ``` using th23 by simp ``` wenzelm@60698 ` 366` ``` with 4 gt th1 show ?thesis ``` wenzelm@56009 ` 367` ``` by simp ``` wenzelm@60698 ` 368` ``` qed ``` chaieb@33154 ` 369` ```qed auto ``` chaieb@33154 ` 370` krauss@41812 ` 371` ```lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" ``` wenzelm@52658 ` 372` ``` by (induct p q rule: polyadd.induct) ``` hoelzl@58776 ` 373` ``` (auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left_NO_MATCH) ``` chaieb@33154 ` 374` wenzelm@56009 ` 375` ```lemma polyadd_norm: "isnpoly p \ isnpoly q \ isnpoly (polyadd p q)" ``` wenzelm@60698 ` 376` ``` using polyadd_normh[of p 0 q 0] isnpoly_def by simp ``` chaieb@33154 ` 377` wenzelm@60698 ` 378` ```text \The degree of addition and other general lemmas needed for the normal form of polymul.\ ``` chaieb@33154 ` 379` wenzelm@52803 ` 380` ```lemma polyadd_different_degreen: ``` wenzelm@56009 ` 381` ``` assumes "isnpolyh p n0" ``` wenzelm@56009 ` 382` ``` and "isnpolyh q n1" ``` wenzelm@56009 ` 383` ``` and "degreen p m \ degreen q m" ``` wenzelm@56009 ` 384` ``` and "m \ min n0 n1" ``` wenzelm@56009 ` 385` ``` shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)" ``` wenzelm@56009 ` 386` ``` using assms ``` chaieb@33154 ` 387` ```proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) ``` chaieb@33154 ` 388` ``` case (4 c n p c' n' p' m n0 n1) ``` wenzelm@60698 ` 389` ``` show ?case ``` wenzelm@60698 ` 390` ``` proof (cases "n = n'") ``` wenzelm@60698 ` 391` ``` case True ``` wenzelm@60698 ` 392` ``` with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) ``` krauss@41763 ` 393` ``` show ?thesis by (auto simp: Let_def) ``` krauss@41763 ` 394` ``` next ``` wenzelm@60698 ` 395` ``` case False ``` krauss@41763 ` 396` ``` with 4 show ?thesis by auto ``` krauss@41763 ` 397` ``` qed ``` krauss@41763 ` 398` ```qed auto ``` chaieb@33154 ` 399` wenzelm@56009 ` 400` ```lemma headnz[simp]: "isnpolyh p n \ p \ 0\<^sub>p \ headn p m \ 0\<^sub>p" ``` wenzelm@52658 ` 401` ``` by (induct p arbitrary: n rule: headn.induct) auto ``` wenzelm@56009 ` 402` chaieb@33154 ` 403` ```lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ degree p = 0" ``` wenzelm@52658 ` 404` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` wenzelm@56009 ` 405` chaieb@33154 ` 406` ```lemma degreen_0[simp]: "isnpolyh p n \ m < n \ degreen p m = 0" ``` wenzelm@52658 ` 407` ``` by (induct p arbitrary: n rule: degreen.induct) auto ``` chaieb@33154 ` 408` chaieb@33154 ` 409` ```lemma degree_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ degree p = 0" ``` wenzelm@52658 ` 410` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 411` chaieb@33154 ` 412` ```lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degree c = 0" ``` chaieb@33154 ` 413` ``` using degree_isnpolyh_Suc by auto ``` wenzelm@56009 ` 414` chaieb@33154 ` 415` ```lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degreen c n = 0" ``` chaieb@33154 ` 416` ``` using degreen_0 by auto ``` chaieb@33154 ` 417` chaieb@33154 ` 418` chaieb@33154 ` 419` ```lemma degreen_polyadd: ``` wenzelm@56009 ` 420` ``` assumes np: "isnpolyh p n0" ``` wenzelm@56009 ` 421` ``` and nq: "isnpolyh q n1" ``` wenzelm@56009 ` 422` ``` and m: "m \ max n0 n1" ``` chaieb@33154 ` 423` ``` shows "degreen (p +\<^sub>p q) m \ max (degreen p m) (degreen q m)" ``` chaieb@33154 ` 424` ``` using np nq m ``` chaieb@33154 ` 425` ```proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct) ``` wenzelm@52803 ` 426` ``` case (2 c c' n' p' n0 n1) ``` wenzelm@56009 ` 427` ``` then show ?case ``` wenzelm@56009 ` 428` ``` by (cases n') simp_all ``` chaieb@33154 ` 429` ```next ``` wenzelm@52803 ` 430` ``` case (3 c n p c' n0 n1) ``` wenzelm@56009 ` 431` ``` then show ?case ``` wenzelm@56009 ` 432` ``` by (cases n) auto ``` chaieb@33154 ` 433` ```next ``` wenzelm@52803 ` 434` ``` case (4 c n p c' n' p' n0 n1 m) ``` wenzelm@60698 ` 435` ``` show ?case ``` wenzelm@60698 ` 436` ``` proof (cases "n = n'") ``` wenzelm@60698 ` 437` ``` case True ``` wenzelm@60698 ` 438` ``` with 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(5-7) ``` krauss@41763 ` 439` ``` show ?thesis by (auto simp: Let_def) ``` wenzelm@60698 ` 440` ``` next ``` wenzelm@60698 ` 441` ``` case False ``` wenzelm@60698 ` 442` ``` then show ?thesis by simp ``` wenzelm@60698 ` 443` ``` qed ``` chaieb@33154 ` 444` ```qed auto ``` chaieb@33154 ` 445` wenzelm@56009 ` 446` ```lemma polyadd_eq_const_degreen: ``` wenzelm@56009 ` 447` ``` assumes "isnpolyh p n0" ``` wenzelm@56009 ` 448` ``` and "isnpolyh q n1" ``` wenzelm@56009 ` 449` ``` and "polyadd p q = C c" ``` wenzelm@56009 ` 450` ``` shows "degreen p m = degreen q m" ``` wenzelm@56009 ` 451` ``` using assms ``` chaieb@33154 ` 452` ```proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) ``` wenzelm@52803 ` 453` ``` case (4 c n p c' n' p' m n0 n1 x) ``` wenzelm@60698 ` 454` ``` consider "n = n'" | "n > n' \ n < n'" by arith ``` wenzelm@60698 ` 455` ``` then show ?case ``` wenzelm@60698 ` 456` ``` proof cases ``` wenzelm@60698 ` 457` ``` case 1 ``` wenzelm@60698 ` 458` ``` with 4 show ?thesis ``` wenzelm@60698 ` 459` ``` by (cases "p +\<^sub>p p' = 0\<^sub>p") (auto simp add: Let_def) ``` wenzelm@60698 ` 460` ``` next ``` wenzelm@60698 ` 461` ``` case 2 ``` wenzelm@60698 ` 462` ``` with 4 show ?thesis by auto ``` wenzelm@60698 ` 463` ``` qed ``` chaieb@33154 ` 464` ```qed simp_all ``` chaieb@33154 ` 465` chaieb@33154 ` 466` ```lemma polymul_properties: ``` haftmann@59867 ` 467` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 468` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 469` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 470` ``` and m: "m \ min n0 n1" ``` wenzelm@52803 ` 471` ``` shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" ``` wenzelm@56009 ` 472` ``` and "p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p" ``` wenzelm@56009 ` 473` ``` and "degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \ q = 0\<^sub>p then 0 else degreen p m + degreen q m)" ``` chaieb@33154 ` 474` ``` using np nq m ``` wenzelm@52658 ` 475` ```proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) ``` wenzelm@52803 ` 476` ``` case (2 c c' n' p') ``` wenzelm@56009 ` 477` ``` { ``` wenzelm@56009 ` 478` ``` case (1 n0 n1) ``` wenzelm@56009 ` 479` ``` with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n'] ``` krauss@41811 ` 480` ``` show ?case by (auto simp add: min_def) ``` chaieb@33154 ` 481` ``` next ``` wenzelm@56009 ` 482` ``` case (2 n0 n1) ``` wenzelm@56009 ` 483` ``` then show ?case by auto ``` chaieb@33154 ` 484` ``` next ``` wenzelm@56009 ` 485` ``` case (3 n0 n1) ``` wenzelm@60698 ` 486` ``` then show ?case using "2.hyps" by auto ``` wenzelm@56009 ` 487` ``` } ``` chaieb@33154 ` 488` ```next ``` krauss@41813 ` 489` ``` case (3 c n p c') ``` wenzelm@56009 ` 490` ``` { ``` wenzelm@56009 ` 491` ``` case (1 n0 n1) ``` wenzelm@56009 ` 492` ``` with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n] ``` krauss@41811 ` 493` ``` show ?case by (auto simp add: min_def) ``` chaieb@33154 ` 494` ``` next ``` wenzelm@56009 ` 495` ``` case (2 n0 n1) ``` wenzelm@56009 ` 496` ``` then show ?case by auto ``` chaieb@33154 ` 497` ``` next ``` wenzelm@56009 ` 498` ``` case (3 n0 n1) ``` wenzelm@56009 ` 499` ``` then show ?case using "3.hyps" by auto ``` wenzelm@56009 ` 500` ``` } ``` chaieb@33154 ` 501` ```next ``` chaieb@33154 ` 502` ``` case (4 c n p c' n' p') ``` chaieb@33154 ` 503` ``` let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'" ``` wenzelm@56009 ` 504` ``` { ``` wenzelm@56009 ` 505` ``` case (1 n0 n1) ``` wenzelm@56009 ` 506` ``` then have cnp: "isnpolyh ?cnp n" ``` wenzelm@56009 ` 507` ``` and cnp': "isnpolyh ?cnp' n'" ``` wenzelm@56009 ` 508` ``` and np: "isnpolyh p n" ``` wenzelm@56009 ` 509` ``` and nc: "isnpolyh c (Suc n)" ``` wenzelm@56009 ` 510` ``` and np': "isnpolyh p' n'" ``` wenzelm@56009 ` 511` ``` and nc': "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 512` ``` and nn0: "n \ n0" ``` wenzelm@56009 ` 513` ``` and nn1: "n' \ n1" ``` wenzelm@56009 ` 514` ``` by simp_all ``` krauss@41811 ` 515` ``` { ``` wenzelm@56009 ` 516` ``` assume "n < n'" ``` wenzelm@56009 ` 517` ``` with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp ``` wenzelm@56009 ` 518` ``` have ?case by (simp add: min_def) ``` wenzelm@56009 ` 519` ``` } moreover { ``` wenzelm@56009 ` 520` ``` assume "n' < n" ``` wenzelm@56009 ` 521` ``` with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' ``` wenzelm@56009 ` 522` ``` have ?case by (cases "Suc n' = n") (simp_all add: min_def) ``` wenzelm@56009 ` 523` ``` } moreover { ``` wenzelm@56009 ` 524` ``` assume "n' = n" ``` wenzelm@56009 ` 525` ``` with "4.hyps"(16-17)[OF cnp np', of n] and "4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 ``` wenzelm@56009 ` 526` ``` have ?case ``` wenzelm@56009 ` 527` ``` apply (auto intro!: polyadd_normh) ``` wenzelm@56009 ` 528` ``` apply (simp_all add: min_def isnpolyh_mono[OF nn0]) ``` wenzelm@56009 ` 529` ``` done ``` wenzelm@56009 ` 530` ``` } ``` wenzelm@56009 ` 531` ``` ultimately show ?case by arith ``` wenzelm@56009 ` 532` ``` next ``` wenzelm@56009 ` 533` ``` fix n0 n1 m ``` wenzelm@56009 ` 534` ``` assume np: "isnpolyh ?cnp n0" ``` wenzelm@56009 ` 535` ``` assume np':"isnpolyh ?cnp' n1" ``` wenzelm@56009 ` 536` ``` assume m: "m \ min n0 n1" ``` wenzelm@56009 ` 537` ``` let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" ``` wenzelm@56009 ` 538` ``` let ?d1 = "degreen ?cnp m" ``` wenzelm@56009 ` 539` ``` let ?d2 = "degreen ?cnp' m" ``` wenzelm@56009 ` 540` ``` let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" ``` wenzelm@56043 ` 541` ``` have "n' < n \ n < n' \ n' = n" by auto ``` wenzelm@56009 ` 542` ``` moreover ``` wenzelm@56009 ` 543` ``` { ``` wenzelm@56009 ` 544` ``` assume "n' < n \ n < n'" ``` wenzelm@56009 ` 545` ``` with "4.hyps"(3,6,18) np np' m have ?eq ``` wenzelm@56009 ` 546` ``` by auto ``` wenzelm@56009 ` 547` ``` } ``` wenzelm@56009 ` 548` ``` moreover ``` wenzelm@56009 ` 549` ``` { ``` wenzelm@56009 ` 550` ``` assume nn': "n' = n" ``` wenzelm@56009 ` 551` ``` then have nn: "\ n' < n \ \ n < n'" by arith ``` wenzelm@56009 ` 552` ``` from "4.hyps"(16,18)[of n n' n] ``` wenzelm@56009 ` 553` ``` "4.hyps"(13,14)[of n "Suc n'" n] ``` wenzelm@56009 ` 554` ``` np np' nn' ``` wenzelm@56043 ` 555` ``` have norm: ``` wenzelm@56043 ` 556` ``` "isnpolyh ?cnp n" ``` wenzelm@56043 ` 557` ``` "isnpolyh c' (Suc n)" ``` wenzelm@56043 ` 558` ``` "isnpolyh (?cnp *\<^sub>p c') n" ``` wenzelm@56043 ` 559` ``` "isnpolyh p' n" ``` wenzelm@56043 ` 560` ``` "isnpolyh (?cnp *\<^sub>p p') n" ``` wenzelm@56043 ` 561` ``` "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56043 ` 562` ``` "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p" ``` wenzelm@56043 ` 563` ``` "?cnp *\<^sub>p p' \ 0\<^sub>p" ``` wenzelm@56043 ` 564` ``` by (auto simp add: min_def) ``` wenzelm@56009 ` 565` ``` { ``` wenzelm@56009 ` 566` ``` assume mn: "m = n" ``` wenzelm@56009 ` 567` ``` from "4.hyps"(17,18)[OF norm(1,4), of n] ``` wenzelm@56009 ` 568` ``` "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn ``` wenzelm@56009 ` 569` ``` have degs: ``` wenzelm@56009 ` 570` ``` "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)" ``` wenzelm@56009 ` 571` ``` "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" ``` wenzelm@56009 ` 572` ``` by (simp_all add: min_def) ``` wenzelm@56009 ` 573` ``` from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 574` ``` by simp ``` wenzelm@56009 ` 575` ``` then have neq: "degreen (?cnp *\<^sub>p c') n \ degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 576` ``` by simp ``` wenzelm@56009 ` 577` ``` have nmin: "n \ min n n" ``` wenzelm@56009 ` 578` ``` by (simp add: min_def) ``` wenzelm@56009 ` 579` ``` from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 ``` wenzelm@56009 ` 580` ``` have deg: "degreen (CN c n p *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n = ``` wenzelm@56009 ` 581` ``` degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 582` ``` by simp ``` wenzelm@56009 ` 583` ``` from "4.hyps"(16-18)[OF norm(1,4), of n] ``` wenzelm@56009 ` 584` ``` "4.hyps"(13-15)[OF norm(1,2), of n] ``` wenzelm@56009 ` 585` ``` mn norm m nn' deg ``` wenzelm@56009 ` 586` ``` have ?eq by simp ``` krauss@41811 ` 587` ``` } ``` chaieb@33154 ` 588` ``` moreover ``` wenzelm@56009 ` 589` ``` { ``` wenzelm@56009 ` 590` ``` assume mn: "m \ n" ``` wenzelm@56009 ` 591` ``` then have mn': "m < n" ``` wenzelm@56009 ` 592` ``` using m np by auto ``` wenzelm@56009 ` 593` ``` from nn' m np have max1: "m \ max n n" ``` wenzelm@56009 ` 594` ``` by simp ``` wenzelm@56009 ` 595` ``` then have min1: "m \ min n n" ``` wenzelm@56009 ` 596` ``` by simp ``` wenzelm@56009 ` 597` ``` then have min2: "m \ min n (Suc n)" ``` wenzelm@56009 ` 598` ``` by simp ``` wenzelm@56009 ` 599` ``` from "4.hyps"(16-18)[OF norm(1,4) min1] ``` wenzelm@56009 ` 600` ``` "4.hyps"(13-15)[OF norm(1,2) min2] ``` wenzelm@56009 ` 601` ``` degreen_polyadd[OF norm(3,6) max1] ``` wenzelm@56009 ` 602` ``` have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \ ``` wenzelm@56009 ` 603` ``` max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" ``` wenzelm@56009 ` 604` ``` using mn nn' np np' by simp ``` wenzelm@56009 ` 605` ``` with "4.hyps"(16-18)[OF norm(1,4) min1] ``` wenzelm@56009 ` 606` ``` "4.hyps"(13-15)[OF norm(1,2) min2] ``` wenzelm@56009 ` 607` ``` degreen_0[OF norm(3) mn'] ``` wenzelm@56009 ` 608` ``` have ?eq using nn' mn np np' by clarsimp ``` wenzelm@56009 ` 609` ``` } ``` wenzelm@56009 ` 610` ``` ultimately have ?eq by blast ``` wenzelm@56009 ` 611` ``` } ``` wenzelm@56009 ` 612` ``` ultimately show ?eq by blast ``` wenzelm@56009 ` 613` ``` } ``` wenzelm@56009 ` 614` ``` { ``` wenzelm@56009 ` 615` ``` case (2 n0 n1) ``` wenzelm@56009 ` 616` ``` then have np: "isnpolyh ?cnp n0" ``` wenzelm@56009 ` 617` ``` and np': "isnpolyh ?cnp' n1" ``` wenzelm@56043 ` 618` ``` and m: "m \ min n0 n1" ``` wenzelm@56043 ` 619` ``` by simp_all ``` wenzelm@56009 ` 620` ``` then have mn: "m \ n" by simp ``` wenzelm@56009 ` 621` ``` let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" ``` wenzelm@56009 ` 622` ``` { ``` wenzelm@56009 ` 623` ``` assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n" ``` wenzelm@56009 ` 624` ``` then have nn: "\ n' < n \ \ n < n'" ``` wenzelm@56009 ` 625` ``` by simp ``` wenzelm@56009 ` 626` ``` from "4.hyps"(16-18) [of n n n] ``` wenzelm@56009 ` 627` ``` "4.hyps"(13-15)[of n "Suc n" n] ``` wenzelm@56009 ` 628` ``` np np' C(2) mn ``` wenzelm@56009 ` 629` ``` have norm: ``` wenzelm@56009 ` 630` ``` "isnpolyh ?cnp n" ``` wenzelm@56009 ` 631` ``` "isnpolyh c' (Suc n)" ``` wenzelm@56009 ` 632` ``` "isnpolyh (?cnp *\<^sub>p c') n" ``` wenzelm@56009 ` 633` ``` "isnpolyh p' n" ``` wenzelm@56009 ` 634` ``` "isnpolyh (?cnp *\<^sub>p p') n" ``` wenzelm@56009 ` 635` ``` "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 636` ``` "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p" ``` wenzelm@56009 ` 637` ``` "?cnp *\<^sub>p p' \ 0\<^sub>p" ``` wenzelm@56009 ` 638` ``` "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" ``` wenzelm@56009 ` 639` ``` "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" ``` wenzelm@56009 ` 640` ``` by (simp_all add: min_def) ``` wenzelm@56009 ` 641` ``` from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 642` ``` by simp ``` wenzelm@56009 ` 643` ``` have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 644` ``` using norm by simp ``` wenzelm@56009 ` 645` ``` from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq ``` wenzelm@56009 ` 646` ``` have False by simp ``` wenzelm@56009 ` 647` ``` } ``` wenzelm@56009 ` 648` ``` then show ?case using "4.hyps" by clarsimp ``` wenzelm@56009 ` 649` ``` } ``` chaieb@33154 ` 650` ```qed auto ``` chaieb@33154 ` 651` wenzelm@56009 ` 652` ```lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q" ``` wenzelm@52658 ` 653` ``` by (induct p q rule: polymul.induct) (auto simp add: field_simps) ``` chaieb@33154 ` 654` wenzelm@52803 ` 655` ```lemma polymul_normh: ``` haftmann@59867 ` 656` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56009 ` 657` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (p *\<^sub>p q) (min n0 n1)" ``` wenzelm@52803 ` 658` ``` using polymul_properties(1) by blast ``` wenzelm@52658 ` 659` wenzelm@52803 ` 660` ```lemma polymul_eq0_iff: ``` haftmann@59867 ` 661` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56009 ` 662` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p" ``` wenzelm@52803 ` 663` ``` using polymul_properties(2) by blast ``` wenzelm@52658 ` 664` wenzelm@56207 ` 665` ```lemma polymul_degreen: ``` haftmann@59867 ` 666` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56009 ` 667` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ m \ min n0 n1 \ ``` wenzelm@56009 ` 668` ``` degreen (p *\<^sub>p q) m = (if p = 0\<^sub>p \ q = 0\<^sub>p then 0 else degreen p m + degreen q m)" ``` wenzelm@56207 ` 669` ``` by (fact polymul_properties(3)) ``` wenzelm@52658 ` 670` wenzelm@52803 ` 671` ```lemma polymul_norm: ``` haftmann@59867 ` 672` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56009 ` 673` ``` shows "isnpoly p \ isnpoly q \ isnpoly (polymul p q)" ``` chaieb@33154 ` 674` ``` using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp ``` chaieb@33154 ` 675` chaieb@33154 ` 676` ```lemma headconst_zero: "isnpolyh p n0 \ headconst p = 0\<^sub>N \ p = 0\<^sub>p" ``` wenzelm@52658 ` 677` ``` by (induct p arbitrary: n0 rule: headconst.induct) auto ``` chaieb@33154 ` 678` chaieb@33154 ` 679` ```lemma headconst_isnormNum: "isnpolyh p n0 \ isnormNum (headconst p)" ``` wenzelm@52658 ` 680` ``` by (induct p arbitrary: n0) auto ``` chaieb@33154 ` 681` wenzelm@52658 ` 682` ```lemma monic_eqI: ``` wenzelm@52803 ` 683` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 684` ``` shows "INum (headconst p) * Ipoly bs (fst (monic p)) = ``` haftmann@59867 ` 685` ``` (Ipoly bs p ::'a::{field_char_0,field, power})" ``` chaieb@33154 ` 686` ``` unfolding monic_def Let_def ``` wenzelm@52658 ` 687` ```proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) ``` chaieb@33154 ` 688` ``` let ?h = "headconst p" ``` chaieb@33154 ` 689` ``` assume pz: "p \ 0\<^sub>p" ``` wenzelm@56000 ` 690` ``` { ``` wenzelm@56000 ` 691` ``` assume hz: "INum ?h = (0::'a)" ``` wenzelm@56043 ` 692` ``` from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" ``` wenzelm@56043 ` 693` ``` by simp_all ``` wenzelm@56043 ` 694` ``` from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" ``` wenzelm@56043 ` 695` ``` by simp ``` wenzelm@56043 ` 696` ``` with headconst_zero[OF np] have "p = 0\<^sub>p" ``` wenzelm@56043 ` 697` ``` by blast ``` wenzelm@56043 ` 698` ``` with pz have False ``` wenzelm@56043 ` 699` ``` by blast ``` wenzelm@56043 ` 700` ``` } ``` wenzelm@56043 ` 701` ``` then show "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0" ``` wenzelm@56043 ` 702` ``` by blast ``` chaieb@33154 ` 703` ```qed ``` chaieb@33154 ` 704` chaieb@33154 ` 705` wenzelm@60698 ` 706` ```text \polyneg is a negation and preserves normal forms\ ``` chaieb@33154 ` 707` chaieb@33154 ` 708` ```lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" ``` wenzelm@52658 ` 709` ``` by (induct p rule: polyneg.induct) auto ``` chaieb@33154 ` 710` wenzelm@56009 ` 711` ```lemma polyneg0: "isnpolyh p n \ (~\<^sub>p p) = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 712` ``` by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def) ``` wenzelm@56009 ` 713` chaieb@33154 ` 714` ```lemma polyneg_polyneg: "isnpolyh p n0 \ ~\<^sub>p (~\<^sub>p p) = p" ``` wenzelm@52658 ` 715` ``` by (induct p arbitrary: n0 rule: polyneg.induct) auto ``` wenzelm@56009 ` 716` wenzelm@56009 ` 717` ```lemma polyneg_normh: "isnpolyh p n \ isnpolyh (polyneg p) n" ``` wenzelm@56009 ` 718` ``` by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0) ``` chaieb@33154 ` 719` chaieb@33154 ` 720` ```lemma polyneg_norm: "isnpoly p \ isnpoly (polyneg p)" ``` chaieb@33154 ` 721` ``` using isnpoly_def polyneg_normh by simp ``` chaieb@33154 ` 722` chaieb@33154 ` 723` wenzelm@60698 ` 724` ```text \polysub is a substraction and preserves normal forms\ ``` krauss@41404 ` 725` wenzelm@56009 ` 726` ```lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q" ``` wenzelm@52658 ` 727` ``` by (simp add: polysub_def) ``` wenzelm@56009 ` 728` wenzelm@56009 ` 729` ```lemma polysub_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polysub p q) (min n0 n1)" ``` wenzelm@52658 ` 730` ``` by (simp add: polysub_def polyneg_normh polyadd_normh) ``` chaieb@33154 ` 731` wenzelm@56009 ` 732` ```lemma polysub_norm: "isnpoly p \ isnpoly q \ isnpoly (polysub p q)" ``` wenzelm@52803 ` 733` ``` using polyadd_norm polyneg_norm by (simp add: polysub_def) ``` wenzelm@56009 ` 734` wenzelm@52658 ` 735` ```lemma polysub_same_0[simp]: ``` haftmann@59867 ` 736` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` krauss@41814 ` 737` ``` shows "isnpolyh p n0 \ polysub p p = 0\<^sub>p" ``` wenzelm@52658 ` 738` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@52658 ` 739` ``` by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def]) ``` chaieb@33154 ` 740` wenzelm@52803 ` 741` ```lemma polysub_0: ``` haftmann@59867 ` 742` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56009 ` 743` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ p -\<^sub>p q = 0\<^sub>p \ p = q" ``` chaieb@33154 ` 744` ``` unfolding polysub_def split_def fst_conv snd_conv ``` krauss@41763 ` 745` ``` by (induct p q arbitrary: n0 n1 rule:polyadd.induct) ``` wenzelm@52658 ` 746` ``` (auto simp: Nsub0[simplified Nsub_def] Let_def) ``` chaieb@33154 ` 747` wenzelm@60698 ` 748` ```text \polypow is a power function and preserves normal forms\ ``` krauss@41404 ` 749` wenzelm@56009 ` 750` ```lemma polypow[simp]: ``` haftmann@59867 ` 751` ``` "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field}) ^ n" ``` wenzelm@52658 ` 752` ```proof (induct n rule: polypow.induct) ``` wenzelm@52658 ` 753` ``` case 1 ``` wenzelm@56043 ` 754` ``` then show ?case ``` wenzelm@56043 ` 755` ``` by simp ``` chaieb@33154 ` 756` ```next ``` chaieb@33154 ` 757` ``` case (2 n) ``` chaieb@33154 ` 758` ``` let ?q = "polypow ((Suc n) div 2) p" ``` krauss@41813 ` 759` ``` let ?d = "polymul ?q ?q" ``` wenzelm@56043 ` 760` ``` have "odd (Suc n) \ even (Suc n)" ``` wenzelm@56043 ` 761` ``` by simp ``` wenzelm@52803 ` 762` ``` moreover ``` wenzelm@56043 ` 763` ``` { ``` wenzelm@56043 ` 764` ``` assume odd: "odd (Suc n)" ``` wenzelm@56000 ` 765` ``` have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" ``` wenzelm@52658 ` 766` ``` by arith ``` wenzelm@56043 ` 767` ``` from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" ``` wenzelm@56043 ` 768` ``` by (simp add: Let_def) ``` wenzelm@56043 ` 769` ``` also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)" ``` chaieb@33154 ` 770` ``` using "2.hyps" by simp ``` chaieb@33154 ` 771` ``` also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" ``` wenzelm@52658 ` 772` ``` by (simp only: power_add power_one_right) simp ``` wenzelm@56000 ` 773` ``` also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" ``` chaieb@33154 ` 774` ``` by (simp only: th) ``` haftmann@58710 ` 775` ``` finally have ?case unfolding numeral_2_eq_2 [symmetric] ``` haftmann@58834 ` 776` ``` using odd_two_times_div_two_nat [OF odd] by simp ``` wenzelm@56043 ` 777` ``` } ``` wenzelm@52803 ` 778` ``` moreover ``` wenzelm@56043 ` 779` ``` { ``` wenzelm@56043 ` 780` ``` assume even: "even (Suc n)" ``` wenzelm@56043 ` 781` ``` from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" ``` wenzelm@56043 ` 782` ``` by (simp add: Let_def) ``` haftmann@58710 ` 783` ``` also have "\ = (Ipoly bs p) ^ (2 * (Suc n div 2))" ``` haftmann@58710 ` 784` ``` using "2.hyps" by (simp only: mult_2 power_add) simp ``` haftmann@58710 ` 785` ``` finally have ?case using even_two_times_div_two [OF even] ``` haftmann@58710 ` 786` ``` by simp ``` wenzelm@56043 ` 787` ``` } ``` chaieb@33154 ` 788` ``` ultimately show ?case by blast ``` chaieb@33154 ` 789` ```qed ``` chaieb@33154 ` 790` wenzelm@52803 ` 791` ```lemma polypow_normh: ``` haftmann@59867 ` 792` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` chaieb@33154 ` 793` ``` shows "isnpolyh p n \ isnpolyh (polypow k p) n" ``` chaieb@33154 ` 794` ```proof (induct k arbitrary: n rule: polypow.induct) ``` wenzelm@56043 ` 795` ``` case 1 ``` wenzelm@56043 ` 796` ``` then show ?case by auto ``` wenzelm@56043 ` 797` ```next ``` chaieb@33154 ` 798` ``` case (2 k n) ``` chaieb@33154 ` 799` ``` let ?q = "polypow (Suc k div 2) p" ``` krauss@41813 ` 800` ``` let ?d = "polymul ?q ?q" ``` wenzelm@56043 ` 801` ``` from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n" ``` wenzelm@56043 ` 802` ``` by blast+ ``` wenzelm@56043 ` 803` ``` from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" ``` wenzelm@56043 ` 804` ``` by simp ``` wenzelm@56043 ` 805` ``` from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" ``` wenzelm@56043 ` 806` ``` by simp ``` haftmann@58710 ` 807` ``` from dn on show ?case by (simp, unfold Let_def) auto ``` haftmann@58710 ` 808` ``` ``` wenzelm@56043 ` 809` ```qed ``` chaieb@33154 ` 810` wenzelm@52803 ` 811` ```lemma polypow_norm: ``` haftmann@59867 ` 812` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` chaieb@33154 ` 813` ``` shows "isnpoly p \ isnpoly (polypow k p)" ``` chaieb@33154 ` 814` ``` by (simp add: polypow_normh isnpoly_def) ``` chaieb@33154 ` 815` wenzelm@60698 ` 816` ```text \Finally the whole normalization\ ``` chaieb@33154 ` 817` wenzelm@52658 ` 818` ```lemma polynate [simp]: ``` haftmann@59867 ` 819` ``` "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field})" ``` wenzelm@52658 ` 820` ``` by (induct p rule:polynate.induct) auto ``` chaieb@33154 ` 821` wenzelm@52803 ` 822` ```lemma polynate_norm[simp]: ``` haftmann@59867 ` 823` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` chaieb@33154 ` 824` ``` shows "isnpoly (polynate p)" ``` wenzelm@52658 ` 825` ``` by (induct p rule: polynate.induct) ``` wenzelm@52658 ` 826` ``` (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, ``` wenzelm@52658 ` 827` ``` simp_all add: isnpoly_def) ``` chaieb@33154 ` 828` wenzelm@60698 ` 829` ```text \shift1\ ``` chaieb@33154 ` 830` chaieb@33154 ` 831` chaieb@33154 ` 832` ```lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" ``` wenzelm@52658 ` 833` ``` by (simp add: shift1_def) ``` chaieb@33154 ` 834` wenzelm@52803 ` 835` ```lemma shift1_isnpoly: ``` wenzelm@56207 ` 836` ``` assumes "isnpoly p" ``` wenzelm@56207 ` 837` ``` and "p \ 0\<^sub>p" ``` wenzelm@52658 ` 838` ``` shows "isnpoly (shift1 p) " ``` wenzelm@56207 ` 839` ``` using assms by (simp add: shift1_def isnpoly_def) ``` chaieb@33154 ` 840` chaieb@33154 ` 841` ```lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p" ``` chaieb@33154 ` 842` ``` by (simp add: shift1_def) ``` wenzelm@56043 ` 843` wenzelm@56043 ` 844` ```lemma funpow_shift1_isnpoly: "isnpoly p \ p \ 0\<^sub>p \ isnpoly (funpow n shift1 p)" ``` haftmann@39246 ` 845` ``` by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) ``` chaieb@33154 ` 846` wenzelm@52803 ` 847` ```lemma funpow_isnpolyh: ``` wenzelm@56207 ` 848` ``` assumes "\p. isnpolyh p n \ isnpolyh (f p) n" ``` wenzelm@56207 ` 849` ``` and "isnpolyh p n" ``` chaieb@33154 ` 850` ``` shows "isnpolyh (funpow k f p) n" ``` wenzelm@56207 ` 851` ``` using assms by (induct k arbitrary: p) auto ``` chaieb@33154 ` 852` wenzelm@52658 ` 853` ```lemma funpow_shift1: ``` haftmann@59867 ` 854` ``` "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) = ``` wenzelm@52658 ` 855` ``` Ipoly bs (Mul (Pw (Bound 0) n) p)" ``` wenzelm@52658 ` 856` ``` by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) ``` chaieb@33154 ` 857` wenzelm@56043 ` 858` ```lemma shift1_isnpolyh: "isnpolyh p n0 \ p \ 0\<^sub>p \ isnpolyh (shift1 p) 0" ``` chaieb@33154 ` 859` ``` using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) ``` chaieb@33154 ` 860` wenzelm@52803 ` 861` ```lemma funpow_shift1_1: ``` haftmann@59867 ` 862` ``` "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field}) = ``` wenzelm@52658 ` 863` ``` Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" ``` chaieb@33154 ` 864` ``` by (simp add: funpow_shift1) ``` chaieb@33154 ` 865` chaieb@33154 ` 866` ```lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" ``` wenzelm@45129 ` 867` ``` by (induct p rule: poly_cmul.induct) (auto simp add: field_simps) ``` chaieb@33154 ` 868` chaieb@33154 ` 869` ```lemma behead: ``` wenzelm@56207 ` 870` ``` assumes "isnpolyh p n" ``` wenzelm@52658 ` 871` ``` shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = ``` haftmann@59867 ` 872` ``` (Ipoly bs p :: 'a :: {field_char_0,field})" ``` wenzelm@56207 ` 873` ``` using assms ``` chaieb@33154 ` 874` ```proof (induct p arbitrary: n rule: behead.induct) ``` wenzelm@56009 ` 875` ``` case (1 c p n) ``` wenzelm@56009 ` 876` ``` then have pn: "isnpolyh p n" by simp ``` wenzelm@52803 ` 877` ``` from 1(1)[OF pn] ``` wenzelm@52803 ` 878` ``` have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . ``` wenzelm@52658 ` 879` ``` then show ?case using "1.hyps" ``` wenzelm@52658 ` 880` ``` apply (simp add: Let_def,cases "behead p = 0\<^sub>p") ``` wenzelm@52658 ` 881` ``` apply (simp_all add: th[symmetric] field_simps) ``` wenzelm@52658 ` 882` ``` done ``` chaieb@33154 ` 883` ```qed (auto simp add: Let_def) ``` chaieb@33154 ` 884` chaieb@33154 ` 885` ```lemma behead_isnpolyh: ``` wenzelm@56207 ` 886` ``` assumes "isnpolyh p n" ``` wenzelm@52658 ` 887` ``` shows "isnpolyh (behead p) n" ``` wenzelm@56207 ` 888` ``` using assms by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono) ``` wenzelm@52658 ` 889` chaieb@33154 ` 890` wenzelm@60533 ` 891` ```subsection \Miscellaneous lemmas about indexes, decrementation, substitution etc ...\ ``` wenzelm@52658 ` 892` chaieb@33154 ` 893` ```lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ polybound0 p" ``` wenzelm@61166 ` 894` ```proof (induct p arbitrary: n rule: poly.induct, auto, goal_cases) ``` wenzelm@60580 ` 895` ``` case prems: (1 c n p n') ``` wenzelm@56009 ` 896` ``` then have "n = Suc (n - 1)" ``` wenzelm@56009 ` 897` ``` by simp ``` wenzelm@56009 ` 898` ``` then have "isnpolyh p (Suc (n - 1))" ``` wenzelm@60533 ` 899` ``` using \isnpolyh p n\ by simp ``` wenzelm@60580 ` 900` ``` with prems(2) show ?case ``` wenzelm@56009 ` 901` ``` by simp ``` chaieb@33154 ` 902` ```qed ``` chaieb@33154 ` 903` chaieb@33154 ` 904` ```lemma isconstant_polybound0: "isnpolyh p n0 \ isconstant p \ polybound0 p" ``` wenzelm@52658 ` 905` ``` by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0) ``` chaieb@33154 ` 906` wenzelm@52658 ` 907` ```lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 908` ``` by (induct p) auto ``` chaieb@33154 ` 909` chaieb@33154 ` 910` ```lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)" ``` wenzelm@52658 ` 911` ``` apply (induct p arbitrary: n0) ``` wenzelm@52658 ` 912` ``` apply auto ``` wenzelm@56043 ` 913` ``` apply atomize ``` blanchet@58259 ` 914` ``` apply (rename_tac nat a b, erule_tac x = "Suc nat" in allE) ``` chaieb@33154 ` 915` ``` apply auto ``` chaieb@33154 ` 916` ``` done ``` chaieb@33154 ` 917` chaieb@33154 ` 918` ```lemma head_polybound0: "isnpolyh p n0 \ polybound0 (head p)" ``` wenzelm@52658 ` 919` ``` by (induct p arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0) ``` chaieb@33154 ` 920` chaieb@33154 ` 921` ```lemma polybound0_I: ``` wenzelm@56207 ` 922` ``` assumes "polybound0 a" ``` wenzelm@56009 ` 923` ``` shows "Ipoly (b # bs) a = Ipoly (b' # bs) a" ``` wenzelm@56207 ` 924` ``` using assms by (induct a rule: poly.induct) auto ``` wenzelm@52658 ` 925` wenzelm@56009 ` 926` ```lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t" ``` chaieb@33154 ` 927` ``` by (induct t) simp_all ``` chaieb@33154 ` 928` chaieb@33154 ` 929` ```lemma polysubst0_I': ``` wenzelm@56207 ` 930` ``` assumes "polybound0 a" ``` wenzelm@56009 ` 931` ``` shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t" ``` wenzelm@56207 ` 932` ``` by (induct t) (simp_all add: polybound0_I[OF assms, where b="b" and b'="b'"]) ``` chaieb@33154 ` 933` wenzelm@52658 ` 934` ```lemma decrpoly: ``` wenzelm@56207 ` 935` ``` assumes "polybound0 t" ``` wenzelm@56043 ` 936` ``` shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)" ``` wenzelm@56207 ` 937` ``` using assms by (induct t rule: decrpoly.induct) simp_all ``` chaieb@33154 ` 938` wenzelm@52658 ` 939` ```lemma polysubst0_polybound0: ``` wenzelm@56207 ` 940` ``` assumes "polybound0 t" ``` chaieb@33154 ` 941` ``` shows "polybound0 (polysubst0 t a)" ``` wenzelm@56207 ` 942` ``` using assms by (induct a rule: poly.induct) auto ``` chaieb@33154 ` 943` chaieb@33154 ` 944` ```lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p" ``` wenzelm@52658 ` 945` ``` by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) ``` chaieb@33154 ` 946` wenzelm@56043 ` 947` ```primrec maxindex :: "poly \ nat" ``` wenzelm@56043 ` 948` ```where ``` chaieb@33154 ` 949` ``` "maxindex (Bound n) = n + 1" ``` chaieb@33154 ` 950` ```| "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" ``` chaieb@33154 ` 951` ```| "maxindex (Add p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 952` ```| "maxindex (Sub p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 953` ```| "maxindex (Mul p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 954` ```| "maxindex (Neg p) = maxindex p" ``` chaieb@33154 ` 955` ```| "maxindex (Pw p n) = maxindex p" ``` chaieb@33154 ` 956` ```| "maxindex (C x) = 0" ``` chaieb@33154 ` 957` wenzelm@52658 ` 958` ```definition wf_bs :: "'a list \ poly \ bool" ``` wenzelm@56000 ` 959` ``` where "wf_bs bs p \ length bs \ maxindex p" ``` chaieb@33154 ` 960` wenzelm@56043 ` 961` ```lemma wf_bs_coefficients: "wf_bs bs p \ \c \ set (coefficients p). wf_bs bs c" ``` wenzelm@52658 ` 962` ```proof (induct p rule: coefficients.induct) ``` wenzelm@52803 ` 963` ``` case (1 c p) ``` wenzelm@52803 ` 964` ``` show ?case ``` chaieb@33154 ` 965` ``` proof ``` wenzelm@56009 ` 966` ``` fix x ``` wenzelm@56009 ` 967` ``` assume xc: "x \ set (coefficients (CN c 0 p))" ``` wenzelm@56009 ` 968` ``` then have "x = c \ x \ set (coefficients p)" ``` wenzelm@56009 ` 969` ``` by simp ``` wenzelm@52803 ` 970` ``` moreover ``` wenzelm@56009 ` 971` ``` { ``` wenzelm@56009 ` 972` ``` assume "x = c" ``` wenzelm@56009 ` 973` ``` then have "wf_bs bs x" ``` wenzelm@56043 ` 974` ``` using "1.prems" unfolding wf_bs_def by simp ``` wenzelm@56009 ` 975` ``` } ``` wenzelm@56009 ` 976` ``` moreover ``` wenzelm@56009 ` 977` ``` { ``` wenzelm@56009 ` 978` ``` assume H: "x \ set (coefficients p)" ``` wenzelm@56009 ` 979` ``` from "1.prems" have "wf_bs bs p" ``` wenzelm@56009 ` 980` ``` unfolding wf_bs_def by simp ``` wenzelm@56009 ` 981` ``` with "1.hyps" H have "wf_bs bs x" ``` wenzelm@56009 ` 982` ``` by blast ``` wenzelm@56009 ` 983` ``` } ``` wenzelm@56066 ` 984` ``` ultimately show "wf_bs bs x" ``` wenzelm@56009 ` 985` ``` by blast ``` chaieb@33154 ` 986` ``` qed ``` chaieb@33154 ` 987` ```qed simp_all ``` chaieb@33154 ` 988` wenzelm@56043 ` 989` ```lemma maxindex_coefficients: "\c \ set (coefficients p). maxindex c \ maxindex p" ``` wenzelm@52658 ` 990` ``` by (induct p rule: coefficients.induct) auto ``` chaieb@33154 ` 991` wenzelm@56000 ` 992` ```lemma wf_bs_I: "wf_bs bs p \ Ipoly (bs @ bs') p = Ipoly bs p" ``` wenzelm@52658 ` 993` ``` unfolding wf_bs_def by (induct p) (auto simp add: nth_append) ``` chaieb@33154 ` 994` wenzelm@52658 ` 995` ```lemma take_maxindex_wf: ``` wenzelm@52803 ` 996` ``` assumes wf: "wf_bs bs p" ``` chaieb@33154 ` 997` ``` shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" ``` wenzelm@56009 ` 998` ```proof - ``` chaieb@33154 ` 999` ``` let ?ip = "maxindex p" ``` chaieb@33154 ` 1000` ``` let ?tbs = "take ?ip bs" ``` wenzelm@56009 ` 1001` ``` from wf have "length ?tbs = ?ip" ``` wenzelm@56009 ` 1002` ``` unfolding wf_bs_def by simp ``` wenzelm@56009 ` 1003` ``` then have wf': "wf_bs ?tbs p" ``` wenzelm@56009 ` 1004` ``` unfolding wf_bs_def by simp ``` wenzelm@56043 ` 1005` ``` have eq: "bs = ?tbs @ drop ?ip bs" ``` wenzelm@56009 ` 1006` ``` by simp ``` wenzelm@56009 ` 1007` ``` from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis ``` wenzelm@56009 ` 1008` ``` using eq by simp ``` chaieb@33154 ` 1009` ```qed ``` chaieb@33154 ` 1010` chaieb@33154 ` 1011` ```lemma decr_maxindex: "polybound0 p \ maxindex (decrpoly p) = maxindex p - 1" ``` wenzelm@52658 ` 1012` ``` by (induct p) auto ``` chaieb@33154 ` 1013` chaieb@33154 ` 1014` ```lemma wf_bs_insensitive: "length bs = length bs' \ wf_bs bs p = wf_bs bs' p" ``` chaieb@33154 ` 1015` ``` unfolding wf_bs_def by simp ``` chaieb@33154 ` 1016` wenzelm@56207 ` 1017` ```lemma wf_bs_insensitive': "wf_bs (x # bs) p = wf_bs (y # bs) p" ``` chaieb@33154 ` 1018` ``` unfolding wf_bs_def by simp ``` chaieb@33154 ` 1019` wenzelm@56207 ` 1020` ```lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x # bs) p" ``` wenzelm@52658 ` 1021` ``` by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) ``` wenzelm@56043 ` 1022` chaieb@33154 ` 1023` ```lemma coefficients_Nil[simp]: "coefficients p \ []" ``` wenzelm@52658 ` 1024` ``` by (induct p rule: coefficients.induct) simp_all ``` chaieb@33154 ` 1025` chaieb@33154 ` 1026` ```lemma coefficients_head: "last (coefficients p) = head p" ``` wenzelm@52658 ` 1027` ``` by (induct p rule: coefficients.induct) auto ``` chaieb@33154 ` 1028` wenzelm@56207 ` 1029` ```lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x # bs) p" ``` wenzelm@52658 ` 1030` ``` unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto ``` chaieb@33154 ` 1031` wenzelm@56043 ` 1032` ```lemma length_le_list_ex: "length xs \ n \ \ys. length (xs @ ys) = n" ``` wenzelm@56207 ` 1033` ``` apply (rule exI[where x="replicate (n - length xs) z" for z]) ``` wenzelm@52658 ` 1034` ``` apply simp ``` wenzelm@52658 ` 1035` ``` done ``` wenzelm@52658 ` 1036` wenzelm@56043 ` 1037` ```lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \ isconstant p" ``` wenzelm@52658 ` 1038` ``` apply (cases p) ``` wenzelm@52658 ` 1039` ``` apply auto ``` blanchet@58259 ` 1040` ``` apply (rename_tac nat a, case_tac "nat") ``` wenzelm@52658 ` 1041` ``` apply simp_all ``` wenzelm@52658 ` 1042` ``` done ``` chaieb@33154 ` 1043` chaieb@33154 ` 1044` ```lemma wf_bs_polyadd: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p +\<^sub>p q)" ``` wenzelm@56066 ` 1045` ``` unfolding wf_bs_def by (induct p q rule: polyadd.induct) (auto simp add: Let_def) ``` chaieb@33154 ` 1046` chaieb@33154 ` 1047` ```lemma wf_bs_polyul: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p *\<^sub>p q)" ``` wenzelm@52803 ` 1048` ``` unfolding wf_bs_def ``` wenzelm@52803 ` 1049` ``` apply (induct p q arbitrary: bs rule: polymul.induct) ``` chaieb@33154 ` 1050` ``` apply (simp_all add: wf_bs_polyadd) ``` chaieb@33154 ` 1051` ``` apply clarsimp ``` chaieb@33154 ` 1052` ``` apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format]) ``` chaieb@33154 ` 1053` ``` apply auto ``` chaieb@33154 ` 1054` ``` done ``` chaieb@33154 ` 1055` chaieb@33154 ` 1056` ```lemma wf_bs_polyneg: "wf_bs bs p \ wf_bs bs (~\<^sub>p p)" ``` wenzelm@52658 ` 1057` ``` unfolding wf_bs_def by (induct p rule: polyneg.induct) auto ``` chaieb@33154 ` 1058` chaieb@33154 ` 1059` ```lemma wf_bs_polysub: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p -\<^sub>p q)" ``` wenzelm@56043 ` 1060` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@56043 ` 1061` ``` using wf_bs_polyadd wf_bs_polyneg by blast ``` chaieb@33154 ` 1062` wenzelm@52658 ` 1063` wenzelm@60533 ` 1064` ```subsection \Canonicity of polynomial representation, see lemma isnpolyh_unique\ ``` chaieb@33154 ` 1065` chaieb@33154 ` 1066` ```definition "polypoly bs p = map (Ipoly bs) (coefficients p)" ``` wenzelm@56043 ` 1067` ```definition "polypoly' bs p = map (Ipoly bs \ decrpoly) (coefficients p)" ``` wenzelm@56043 ` 1068` ```definition "poly_nate bs p = map (Ipoly bs \ decrpoly) (coefficients (polynate p))" ``` chaieb@33154 ` 1069` wenzelm@56043 ` 1070` ```lemma coefficients_normh: "isnpolyh p n0 \ \q \ set (coefficients p). isnpolyh q n0" ``` chaieb@33154 ` 1071` ```proof (induct p arbitrary: n0 rule: coefficients.induct) ``` chaieb@33154 ` 1072` ``` case (1 c p n0) ``` wenzelm@56009 ` 1073` ``` have cp: "isnpolyh (CN c 0 p) n0" ``` wenzelm@56009 ` 1074` ``` by fact ``` wenzelm@56009 ` 1075` ``` then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \ 0\<^sub>p" "n0 = 0" ``` chaieb@33154 ` 1076` ``` by (auto simp add: isnpolyh_mono[where n'=0]) ``` wenzelm@56009 ` 1077` ``` from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case ``` wenzelm@56009 ` 1078` ``` by simp ``` chaieb@33154 ` 1079` ```qed auto ``` chaieb@33154 ` 1080` wenzelm@56043 ` 1081` ```lemma coefficients_isconst: "isnpolyh p n \ \q \ set (coefficients p). isconstant q" ``` wenzelm@56043 ` 1082` ``` by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const) ``` chaieb@33154 ` 1083` chaieb@33154 ` 1084` ```lemma polypoly_polypoly': ``` chaieb@33154 ` 1085` ``` assumes np: "isnpolyh p n0" ``` wenzelm@56043 ` 1086` ``` shows "polypoly (x # bs) p = polypoly' bs p" ``` wenzelm@56043 ` 1087` ```proof - ``` chaieb@33154 ` 1088` ``` let ?cf = "set (coefficients p)" ``` chaieb@33154 ` 1089` ``` from coefficients_normh[OF np] have cn_norm: "\ q\ ?cf. isnpolyh q n0" . ``` wenzelm@56043 ` 1090` ``` { ``` wenzelm@56043 ` 1091` ``` fix q ``` wenzelm@56043 ` 1092` ``` assume q: "q \ ?cf" ``` wenzelm@56043 ` 1093` ``` from q cn_norm have th: "isnpolyh q n0" ``` wenzelm@56043 ` 1094` ``` by blast ``` wenzelm@56043 ` 1095` ``` from coefficients_isconst[OF np] q have "isconstant q" ``` wenzelm@56043 ` 1096` ``` by blast ``` wenzelm@56043 ` 1097` ``` with isconstant_polybound0[OF th] have "polybound0 q" ``` wenzelm@56043 ` 1098` ``` by blast ``` wenzelm@56043 ` 1099` ``` } ``` wenzelm@56009 ` 1100` ``` then have "\q \ ?cf. polybound0 q" .. ``` wenzelm@56043 ` 1101` ``` then have "\q \ ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)" ``` chaieb@33154 ` 1102` ``` using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] ``` chaieb@33154 ` 1103` ``` by auto ``` wenzelm@56043 ` 1104` ``` then show ?thesis ``` wenzelm@56043 ` 1105` ``` unfolding polypoly_def polypoly'_def by simp ``` chaieb@33154 ` 1106` ```qed ``` chaieb@33154 ` 1107` chaieb@33154 ` 1108` ```lemma polypoly_poly: ``` wenzelm@56043 ` 1109` ``` assumes "isnpolyh p n0" ``` wenzelm@56043 ` 1110` ``` shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x" ``` wenzelm@56043 ` 1111` ``` using assms ``` wenzelm@52658 ` 1112` ``` by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) ``` chaieb@33154 ` 1113` wenzelm@52803 ` 1114` ```lemma polypoly'_poly: ``` wenzelm@56043 ` 1115` ``` assumes "isnpolyh p n0" ``` wenzelm@52658 ` 1116` ``` shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" ``` wenzelm@56043 ` 1117` ``` using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] . ``` chaieb@33154 ` 1118` chaieb@33154 ` 1119` chaieb@33154 ` 1120` ```lemma polypoly_poly_polybound0: ``` wenzelm@56043 ` 1121` ``` assumes "isnpolyh p n0" ``` wenzelm@56043 ` 1122` ``` and "polybound0 p" ``` chaieb@33154 ` 1123` ``` shows "polypoly bs p = [Ipoly bs p]" ``` wenzelm@56043 ` 1124` ``` using assms ``` wenzelm@56043 ` 1125` ``` unfolding polypoly_def ``` wenzelm@52658 ` 1126` ``` apply (cases p) ``` wenzelm@52658 ` 1127` ``` apply auto ``` blanchet@58259 ` 1128` ``` apply (rename_tac nat a, case_tac nat) ``` wenzelm@52658 ` 1129` ``` apply auto ``` wenzelm@52658 ` 1130` ``` done ``` chaieb@33154 ` 1131` wenzelm@52803 ` 1132` ```lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" ``` wenzelm@52658 ` 1133` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1134` wenzelm@56043 ` 1135` ```lemma headn_nz[simp]: "isnpolyh p n0 \ headn p m = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 1136` ``` by (cases p) auto ``` chaieb@33154 ` 1137` chaieb@33154 ` 1138` ```lemma head_eq_headn0: "head p = headn p 0" ``` wenzelm@52658 ` 1139` ``` by (induct p rule: head.induct) simp_all ``` chaieb@33154 ` 1140` wenzelm@56043 ` 1141` ```lemma head_nz[simp]: "isnpolyh p n0 \ head p = 0\<^sub>p \ p = 0\<^sub>p" ``` chaieb@33154 ` 1142` ``` by (simp add: head_eq_headn0) ``` chaieb@33154 ` 1143` wenzelm@52803 ` 1144` ```lemma isnpolyh_zero_iff: ``` wenzelm@52658 ` 1145` ``` assumes nq: "isnpolyh p n0" ``` haftmann@59867 ` 1146` ``` and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field, power})" ``` chaieb@33154 ` 1147` ``` shows "p = 0\<^sub>p" ``` wenzelm@52658 ` 1148` ``` using nq eq ``` berghofe@34915 ` 1149` ```proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) ``` berghofe@34915 ` 1150` ``` case less ``` wenzelm@60533 ` 1151` ``` note np = \isnpolyh p n0\ and zp = \\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)\ ``` wenzelm@56000 ` 1152` ``` { ``` wenzelm@56000 ` 1153` ``` assume nz: "maxindex p = 0" ``` wenzelm@56000 ` 1154` ``` then obtain c where "p = C c" ``` wenzelm@56000 ` 1155` ``` using np by (cases p) auto ``` wenzelm@56000 ` 1156` ``` with zp np have "p = 0\<^sub>p" ``` wenzelm@56000 ` 1157` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1158` ``` } ``` chaieb@33154 ` 1159` ``` moreover ``` wenzelm@56000 ` 1160` ``` { ``` wenzelm@56000 ` 1161` ``` assume nz: "maxindex p \ 0" ``` chaieb@33154 ` 1162` ``` let ?h = "head p" ``` chaieb@33154 ` 1163` ``` let ?hd = "decrpoly ?h" ``` chaieb@33154 ` 1164` ``` let ?ihd = "maxindex ?hd" ``` wenzelm@56000 ` 1165` ``` from head_isnpolyh[OF np] head_polybound0[OF np] ``` wenzelm@56000 ` 1166` ``` have h: "isnpolyh ?h n0" "polybound0 ?h" ``` chaieb@33154 ` 1167` ``` by simp_all ``` wenzelm@56000 ` 1168` ``` then have nhd: "isnpolyh ?hd (n0 - 1)" ``` wenzelm@56000 ` 1169` ``` using decrpoly_normh by blast ``` wenzelm@52803 ` 1170` chaieb@33154 ` 1171` ``` from maxindex_coefficients[of p] coefficients_head[of p, symmetric] ``` wenzelm@56000 ` 1172` ``` have mihn: "maxindex ?h \ maxindex p" ``` wenzelm@56000 ` 1173` ``` by auto ``` wenzelm@56000 ` 1174` ``` with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" ``` wenzelm@56000 ` 1175` ``` by auto ``` wenzelm@56000 ` 1176` ``` { ``` wenzelm@56000 ` 1177` ``` fix bs :: "'a list" ``` wenzelm@56000 ` 1178` ``` assume bs: "wf_bs bs ?hd" ``` chaieb@33154 ` 1179` ``` let ?ts = "take ?ihd bs" ``` chaieb@33154 ` 1180` ``` let ?rs = "drop ?ihd bs" ``` wenzelm@56000 ` 1181` ``` have ts: "wf_bs ?ts ?hd" ``` wenzelm@56000 ` 1182` ``` using bs unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1183` ``` have bs_ts_eq: "?ts @ ?rs = bs" ``` wenzelm@56000 ` 1184` ``` by simp ``` wenzelm@56000 ` 1185` ``` from wf_bs_decrpoly[OF ts] have tsh: " \x. wf_bs (x # ?ts) ?h" ``` wenzelm@56000 ` 1186` ``` by simp ``` wenzelm@56000 ` 1187` ``` from ihd_lt_n have "\x. length (x # ?ts) \ maxindex p" ``` wenzelm@56000 ` 1188` ``` by simp ``` wenzelm@56000 ` 1189` ``` with length_le_list_ex obtain xs where xs: "length ((x # ?ts) @ xs) = maxindex p" ``` wenzelm@56000 ` 1190` ``` by blast ``` wenzelm@56000 ` 1191` ``` then have "\x. wf_bs ((x # ?ts) @ xs) p" ``` wenzelm@56000 ` 1192` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1193` ``` with zp have "\x. Ipoly ((x # ?ts) @ xs) p = 0" ``` wenzelm@56000 ` 1194` ``` by blast ``` wenzelm@56000 ` 1195` ``` then have "\x. Ipoly (x # (?ts @ xs)) p = 0" ``` wenzelm@56000 ` 1196` ``` by simp ``` chaieb@33154 ` 1197` ``` with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] ``` wenzelm@56000 ` 1198` ``` have "\x. poly (polypoly' (?ts @ xs) p) x = poly [] x" ``` wenzelm@56000 ` 1199` ``` by simp ``` wenzelm@56000 ` 1200` ``` then have "poly (polypoly' (?ts @ xs) p) = poly []" ``` wenzelm@56000 ` 1201` ``` by auto ``` wenzelm@56000 ` 1202` ``` then have "\c \ set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" ``` wenzelm@60537 ` 1203` ``` using poly_zero[where ?'a='a] by (simp add: polypoly'_def) ``` chaieb@33154 ` 1204` ``` with coefficients_head[of p, symmetric] ``` wenzelm@56000 ` 1205` ``` have th0: "Ipoly (?ts @ xs) ?hd = 0" ``` wenzelm@56000 ` 1206` ``` by simp ``` wenzelm@56000 ` 1207` ``` from bs have wf'': "wf_bs ?ts ?hd" ``` wenzelm@56000 ` 1208` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1209` ``` with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" ``` wenzelm@56000 ` 1210` ``` by simp ``` wenzelm@56000 ` 1211` ``` with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\?hd\\<^sub>p\<^bsup>bs\<^esup> = 0" ``` wenzelm@56000 ` 1212` ``` by simp ``` wenzelm@56000 ` 1213` ``` } ``` wenzelm@56000 ` 1214` ``` then have hdz: "\bs. wf_bs bs ?hd \ \?hd\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" ``` wenzelm@56000 ` 1215` ``` by blast ``` wenzelm@56000 ` 1216` ``` from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" ``` wenzelm@56000 ` 1217` ``` by blast ``` wenzelm@56000 ` 1218` ``` then have "?h = 0\<^sub>p" by simp ``` wenzelm@56000 ` 1219` ``` with head_nz[OF np] have "p = 0\<^sub>p" by simp ``` wenzelm@56000 ` 1220` ``` } ``` wenzelm@56000 ` 1221` ``` ultimately show "p = 0\<^sub>p" ``` wenzelm@56000 ` 1222` ``` by blast ``` chaieb@33154 ` 1223` ```qed ``` chaieb@33154 ` 1224` wenzelm@52803 ` 1225` ```lemma isnpolyh_unique: ``` wenzelm@56000 ` 1226` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1227` ``` and nq: "isnpolyh q n1" ``` haftmann@59867 ` 1228` ``` shows "(\bs. \p\\<^sub>p\<^bsup>bs\<^esup> = (\q\\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0,field,power})) \ p = q" ``` wenzelm@56000 ` 1229` ```proof auto ``` wenzelm@56000 ` 1230` ``` assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a) = \q\\<^sub>p\<^bsup>bs\<^esup>" ``` wenzelm@56000 ` 1231` ``` then have "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" ``` wenzelm@56000 ` 1232` ``` by simp ``` wenzelm@56000 ` 1233` ``` then have "\bs. wf_bs bs (p -\<^sub>p q) \ \p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" ``` chaieb@33154 ` 1234` ``` using wf_bs_polysub[where p=p and q=q] by auto ``` wenzelm@56000 ` 1235` ``` with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q" ``` wenzelm@56000 ` 1236` ``` by blast ``` chaieb@33154 ` 1237` ```qed ``` chaieb@33154 ` 1238` chaieb@33154 ` 1239` wenzelm@60698 ` 1240` ```text \consequences of unicity on the algorithms for polynomial normalization\ ``` chaieb@33154 ` 1241` wenzelm@52658 ` 1242` ```lemma polyadd_commute: ``` haftmann@59867 ` 1243` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1244` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1245` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 1246` ``` shows "p +\<^sub>p q = q +\<^sub>p p" ``` wenzelm@56000 ` 1247` ``` using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] ``` wenzelm@56000 ` 1248` ``` by simp ``` chaieb@33154 ` 1249` wenzelm@56000 ` 1250` ```lemma zero_normh: "isnpolyh 0\<^sub>p n" ``` wenzelm@56000 ` 1251` ``` by simp ``` wenzelm@56000 ` 1252` wenzelm@56000 ` 1253` ```lemma one_normh: "isnpolyh (1)\<^sub>p n" ``` wenzelm@56000 ` 1254` ``` by simp ``` wenzelm@52658 ` 1255` wenzelm@52803 ` 1256` ```lemma polyadd_0[simp]: ``` haftmann@59867 ` 1257` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1258` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1259` ``` shows "p +\<^sub>p 0\<^sub>p = p" ``` wenzelm@56000 ` 1260` ``` and "0\<^sub>p +\<^sub>p p = p" ``` wenzelm@52803 ` 1261` ``` using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] ``` chaieb@33154 ` 1262` ``` isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all ``` chaieb@33154 ` 1263` wenzelm@52803 ` 1264` ```lemma polymul_1[simp]: ``` haftmann@59867 ` 1265` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1266` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1267` ``` shows "p *\<^sub>p (1)\<^sub>p = p" ``` wenzelm@56000 ` 1268` ``` and "(1)\<^sub>p *\<^sub>p p = p" ``` wenzelm@52803 ` 1269` ``` using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] ``` chaieb@33154 ` 1270` ``` isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all ``` wenzelm@52658 ` 1271` wenzelm@52803 ` 1272` ```lemma polymul_0[simp]: ``` haftmann@59867 ` 1273` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1274` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1275` ``` shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" ``` wenzelm@56000 ` 1276` ``` and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" ``` wenzelm@52803 ` 1277` ``` using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] ``` chaieb@33154 ` 1278` ``` isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all ``` chaieb@33154 ` 1279` wenzelm@52803 ` 1280` ```lemma polymul_commute: ``` haftmann@59867 ` 1281` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56000 ` 1282` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1283` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1284` ``` shows "p *\<^sub>p q = q *\<^sub>p p" ``` wenzelm@56043 ` 1285` ``` using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], ``` haftmann@59867 ` 1286` ``` where ?'a = "'a::{field_char_0,field, power}"] ``` wenzelm@52658 ` 1287` ``` by simp ``` chaieb@33154 ` 1288` wenzelm@52658 ` 1289` ```declare polyneg_polyneg [simp] ``` wenzelm@52803 ` 1290` wenzelm@52803 ` 1291` ```lemma isnpolyh_polynate_id [simp]: ``` haftmann@59867 ` 1292` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56000 ` 1293` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1294` ``` shows "polynate p = p" ``` haftmann@59867 ` 1295` ``` using isnpolyh_unique[where ?'a= "'a::{field_char_0,field}", ``` wenzelm@56043 ` 1296` ``` OF polynate_norm[of p, unfolded isnpoly_def] np] ``` haftmann@59867 ` 1297` ``` polynate[where ?'a = "'a::{field_char_0,field}"] ``` wenzelm@52658 ` 1298` ``` by simp ``` chaieb@33154 ` 1299` wenzelm@52803 ` 1300` ```lemma polynate_idempotent[simp]: ``` haftmann@59867 ` 1301` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` chaieb@33154 ` 1302` ``` shows "polynate (polynate p) = polynate p" ``` chaieb@33154 ` 1303` ``` using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . ``` chaieb@33154 ` 1304` chaieb@33154 ` 1305` ```lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)" ``` chaieb@33154 ` 1306` ``` unfolding poly_nate_def polypoly'_def .. ``` wenzelm@52658 ` 1307` wenzelm@52658 ` 1308` ```lemma poly_nate_poly: ``` haftmann@59867 ` 1309` ``` "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0,field}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" ``` chaieb@33154 ` 1310` ``` using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] ``` wenzelm@52658 ` 1311` ``` unfolding poly_nate_polypoly' by auto ``` wenzelm@52658 ` 1312` chaieb@33154 ` 1313` wenzelm@60698 ` 1314` ```subsection \heads, degrees and all that\ ``` wenzelm@52658 ` 1315` chaieb@33154 ` 1316` ```lemma degree_eq_degreen0: "degree p = degreen p 0" ``` wenzelm@52658 ` 1317` ``` by (induct p rule: degree.induct) simp_all ``` chaieb@33154 ` 1318` wenzelm@52658 ` 1319` ```lemma degree_polyneg: ``` wenzelm@56043 ` 1320` ``` assumes "isnpolyh p n" ``` chaieb@33154 ` 1321` ``` shows "degree (polyneg p) = degree p" ``` wenzelm@56043 ` 1322` ``` apply (induct p rule: polyneg.induct) ``` wenzelm@56043 ` 1323` ``` using assms ``` wenzelm@56043 ` 1324` ``` apply simp_all ``` wenzelm@52658 ` 1325` ``` apply (case_tac na) ``` wenzelm@52658 ` 1326` ``` apply auto ``` wenzelm@52658 ` 1327` ``` done ``` chaieb@33154 ` 1328` chaieb@33154 ` 1329` ```lemma degree_polyadd: ``` wenzelm@56043 ` 1330` ``` assumes np: "isnpolyh p n0" ``` wenzelm@56043 ` 1331` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1332` ``` shows "degree (p +\<^sub>p q) \ max (degree p) (degree q)" ``` wenzelm@52658 ` 1333` ``` using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp ``` chaieb@33154 ` 1334` chaieb@33154 ` 1335` wenzelm@52658 ` 1336` ```lemma degree_polysub: ``` wenzelm@52658 ` 1337` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1338` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1339` ``` shows "degree (p -\<^sub>p q) \ max (degree p) (degree q)" ``` chaieb@33154 ` 1340` ```proof- ``` wenzelm@56043 ` 1341` ``` from nq have nq': "isnpolyh (~\<^sub>p q) n1" ``` wenzelm@56043 ` 1342` ``` using polyneg_normh by simp ``` wenzelm@56043 ` 1343` ``` from degree_polyadd[OF np nq'] show ?thesis ``` wenzelm@56043 ` 1344` ``` by (simp add: polysub_def degree_polyneg[OF nq]) ``` chaieb@33154 ` 1345` ```qed ``` chaieb@33154 ` 1346` wenzelm@52803 ` 1347` ```lemma degree_polysub_samehead: ``` haftmann@59867 ` 1348` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56043 ` 1349` ``` and np: "isnpolyh p n0" ``` wenzelm@56043 ` 1350` ``` and nq: "isnpolyh q n1" ``` wenzelm@56043 ` 1351` ``` and h: "head p = head q" ``` wenzelm@52658 ` 1352` ``` and d: "degree p = degree q" ``` chaieb@33154 ` 1353` ``` shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" ``` wenzelm@52658 ` 1354` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@52658 ` 1355` ``` using np nq h d ``` wenzelm@52658 ` 1356` ```proof (induct p q rule: polyadd.induct) ``` wenzelm@52658 ` 1357` ``` case (1 c c') ``` wenzelm@56009 ` 1358` ``` then show ?case ``` wenzelm@56009 ` 1359` ``` by (simp add: Nsub_def Nsub0[simplified Nsub_def]) ``` chaieb@33154 ` 1360` ```next ``` wenzelm@52803 ` 1361` ``` case (2 c c' n' p') ``` wenzelm@56009 ` 1362` ``` from 2 have "degree (C c) = degree (CN c' n' p')" ``` wenzelm@56009 ` 1363` ``` by simp ``` wenzelm@56009 ` 1364` ``` then have nz: "n' > 0" ``` wenzelm@56009 ` 1365` ``` by (cases n') auto ``` wenzelm@56009 ` 1366` ``` then have "head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1367` ``` by (cases n') auto ``` wenzelm@56009 ` 1368` ``` with 2 show ?case ``` wenzelm@56009 ` 1369` ``` by simp ``` chaieb@33154 ` 1370` ```next ``` wenzelm@52803 ` 1371` ``` case (3 c n p c') ``` wenzelm@56009 ` 1372` ``` then have "degree (C c') = degree (CN c n p)" ``` wenzelm@56009 ` 1373` ``` by simp ``` wenzelm@56009 ` 1374` ``` then have nz: "n > 0" ``` wenzelm@56009 ` 1375` ``` by (cases n) auto ``` wenzelm@56009 ` 1376` ``` then have "head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1377` ``` by (cases n) auto ``` wenzelm@41807 ` 1378` ``` with 3 show ?case by simp ``` chaieb@33154 ` 1379` ```next ``` chaieb@33154 ` 1380` ``` case (4 c n p c' n' p') ``` wenzelm@56009 ` 1381` ``` then have H: ``` wenzelm@56009 ` 1382` ``` "isnpolyh (CN c n p) n0" ``` wenzelm@56009 ` 1383` ``` "isnpolyh (CN c' n' p') n1" ``` wenzelm@56009 ` 1384` ``` "head (CN c n p) = head (CN c' n' p')" ``` wenzelm@56009 ` 1385` ``` "degree (CN c n p) = degree (CN c' n' p')" ``` wenzelm@56009 ` 1386` ``` by simp_all ``` wenzelm@56009 ` 1387` ``` then have degc: "degree c = 0" and degc': "degree c' = 0" ``` wenzelm@56009 ` 1388` ``` by simp_all ``` wenzelm@56009 ` 1389` ``` then have degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" ``` chaieb@33154 ` 1390` ``` using H(1-2) degree_polyneg by auto ``` wenzelm@56009 ` 1391` ``` from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 1392` ``` by simp_all ``` wenzelm@56009 ` 1393` ``` from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' ``` wenzelm@56009 ` 1394` ``` have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" ``` wenzelm@56009 ` 1395` ``` by simp ``` wenzelm@56009 ` 1396` ``` from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" ``` wenzelm@56009 ` 1397` ``` by auto ``` wenzelm@56009 ` 1398` ``` have "n = n' \ n < n' \ n > n'" ``` wenzelm@56009 ` 1399` ``` by arith ``` chaieb@33154 ` 1400` ``` moreover ``` wenzelm@56009 ` 1401` ``` { ``` wenzelm@56009 ` 1402` ``` assume nn': "n = n'" ``` wenzelm@56009 ` 1403` ``` have "n = 0 \ n > 0" by arith ``` wenzelm@56066 ` 1404` ``` moreover ``` wenzelm@56066 ` 1405` ``` { ``` wenzelm@56009 ` 1406` ``` assume nz: "n = 0" ``` wenzelm@56009 ` 1407` ``` then have ?case using 4 nn' ``` wenzelm@56009 ` 1408` ``` by (auto simp add: Let_def degcmc') ``` wenzelm@56009 ` 1409` ``` } ``` wenzelm@56066 ` 1410` ``` moreover ``` wenzelm@56066 ` 1411` ``` { ``` wenzelm@56009 ` 1412` ``` assume nz: "n > 0" ``` wenzelm@56009 ` 1413` ``` with nn' H(3) have cc': "c = c'" and pp': "p = p'" ``` wenzelm@56009 ` 1414` ``` by (cases n, auto)+ ``` wenzelm@56009 ` 1415` ``` then have ?case ``` wenzelm@56009 ` 1416` ``` using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] ``` wenzelm@56009 ` 1417` ``` using polysub_same_0[OF c'nh, simplified polysub_def] ``` wenzelm@56009 ` 1418` ``` using nn' 4 by (simp add: Let_def) ``` wenzelm@56009 ` 1419` ``` } ``` wenzelm@56009 ` 1420` ``` ultimately have ?case by blast ``` wenzelm@56009 ` 1421` ``` } ``` chaieb@33154 ` 1422` ``` moreover ``` wenzelm@56009 ` 1423` ``` { ``` wenzelm@56009 ` 1424` ``` assume nn': "n < n'" ``` wenzelm@56009 ` 1425` ``` then have n'p: "n' > 0" ``` wenzelm@56009 ` 1426` ``` by simp ``` wenzelm@56009 ` 1427` ``` then have headcnp':"head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1428` ``` by (cases n') simp_all ``` wenzelm@56009 ` 1429` ``` have degcnp': "degree (CN c' n' p') = 0" ``` wenzelm@56009 ` 1430` ``` and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" ``` wenzelm@52658 ` 1431` ``` using 4 nn' by (cases n', simp_all) ``` wenzelm@56009 ` 1432` ``` then have "n > 0" ``` wenzelm@56009 ` 1433` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1434` ``` then have headcnp: "head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1435` ``` by (cases n) auto ``` wenzelm@56009 ` 1436` ``` from H(3) headcnp headcnp' nn' have ?case ``` wenzelm@56009 ` 1437` ``` by auto ``` wenzelm@56009 ` 1438` ``` } ``` chaieb@33154 ` 1439` ``` moreover ``` wenzelm@56009 ` 1440` ``` { ``` wenzelm@56009 ` 1441` ``` assume nn': "n > n'" ``` wenzelm@56009 ` 1442` ``` then have np: "n > 0" by simp ``` wenzelm@56009 ` 1443` ``` then have headcnp:"head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1444` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1445` ``` from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" ``` wenzelm@56009 ` 1446` ``` by simp ``` wenzelm@56009 ` 1447` ``` from np have degcnp: "degree (CN c n p) = 0" ``` wenzelm@56009 ` 1448` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1449` ``` with degcnpeq have "n' > 0" ``` wenzelm@56009 ` 1450` ``` by (cases n') simp_all ``` wenzelm@56009 ` 1451` ``` then have headcnp': "head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1452` ``` by (cases n') auto ``` wenzelm@56009 ` 1453` ``` from H(3) headcnp headcnp' nn' have ?case by auto ``` wenzelm@56009 ` 1454` ``` } ``` wenzelm@56009 ` 1455` ``` ultimately show ?case by blast ``` krauss@41812 ` 1456` ```qed auto ``` wenzelm@52803 ` 1457` chaieb@33154 ` 1458` ```lemma shift1_head : "isnpolyh p n0 \ head (shift1 p) = head p" ``` wenzelm@52658 ` 1459` ``` by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) ``` chaieb@33154 ` 1460` chaieb@33154 ` 1461` ```lemma funpow_shift1_head: "isnpolyh p n0 \ p\ 0\<^sub>p \ head (funpow k shift1 p) = head p" ``` wenzelm@52658 ` 1462` ```proof (induct k arbitrary: n0 p) ``` wenzelm@52658 ` 1463` ``` case 0 ``` wenzelm@56198 ` 1464` ``` then show ?case ``` wenzelm@56198 ` 1465` ``` by auto ``` wenzelm@52658 ` 1466` ```next ``` wenzelm@52658 ` 1467` ``` case (Suc k n0 p) ``` wenzelm@56066 ` 1468` ``` then have "isnpolyh (shift1 p) 0" ``` wenzelm@56066 ` 1469` ``` by (simp add: shift1_isnpolyh) ``` wenzelm@41807 ` 1470` ``` with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" ``` wenzelm@56066 ` 1471` ``` and "head (shift1 p) = head p" ``` wenzelm@56066 ` 1472` ``` by (simp_all add: shift1_head) ``` wenzelm@56066 ` 1473` ``` then show ?case ``` wenzelm@56066 ` 1474` ``` by (simp add: funpow_swap1) ``` wenzelm@52658 ` 1475` ```qed ``` chaieb@33154 ` 1476` chaieb@33154 ` 1477` ```lemma shift1_degree: "degree (shift1 p) = 1 + degree p" ``` chaieb@33154 ` 1478` ``` by (simp add: shift1_def) ``` wenzelm@56009 ` 1479` chaieb@33154 ` 1480` ```lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " ``` wenzelm@46991 ` 1481` ``` by (induct k arbitrary: p) (auto simp add: shift1_degree) ``` chaieb@33154 ` 1482` chaieb@33154 ` 1483` ```lemma funpow_shift1_nz: "p \ 0\<^sub>p \ funpow n shift1 p \ 0\<^sub>p" ``` wenzelm@52658 ` 1484` ``` by (induct n arbitrary: p) simp_all ``` chaieb@33154 ` 1485` chaieb@33154 ` 1486` ```lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ head p = p" ``` wenzelm@52658 ` 1487` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1488` ```lemma headn_0[simp]: "isnpolyh p n \ m < n \ headn p m = p" ``` wenzelm@52658 ` 1489` ``` by (induct p arbitrary: n rule: degreen.induct) auto ``` chaieb@33154 ` 1490` ```lemma head_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ head p = p" ``` wenzelm@52658 ` 1491` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1492` ```lemma head_head[simp]: "isnpolyh p n0 \ head (head p) = head p" ``` wenzelm@52658 ` 1493` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1494` wenzelm@52803 ` 1495` ```lemma polyadd_eq_const_degree: ``` wenzelm@52658 ` 1496` ``` "isnpolyh p n0 \ isnpolyh q n1 \ polyadd p q = C c \ degree p = degree q" ``` chaieb@33154 ` 1497` ``` using polyadd_eq_const_degreen degree_eq_degreen0 by simp ``` chaieb@33154 ` 1498` wenzelm@52658 ` 1499` ```lemma polyadd_head: ``` wenzelm@52658 ` 1500` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1501` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 1502` ``` and deg: "degree p \ degree q" ``` chaieb@33154 ` 1503` ``` shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)" ``` wenzelm@52658 ` 1504` ``` using np nq deg ``` wenzelm@52658 ` 1505` ``` apply (induct p q arbitrary: n0 n1 rule: polyadd.induct) ``` wenzelm@52658 ` 1506` ``` apply simp_all ``` wenzelm@52658 ` 1507` ``` apply (case_tac n', simp, simp) ``` wenzelm@52658 ` 1508` ``` apply (case_tac n, simp, simp) ``` wenzelm@52658 ` 1509` ``` apply (case_tac n, case_tac n', simp add: Let_def) ``` haftmann@54489 ` 1510` ``` apply (auto simp add: polyadd_eq_const_degree)[2] ``` wenzelm@52658 ` 1511` ``` apply (metis head_nz) ``` wenzelm@52658 ` 1512` ``` apply (metis head_nz) ``` wenzelm@52658 ` 1513` ``` apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) ``` wenzelm@52658 ` 1514` ``` done ``` chaieb@33154 ` 1515` wenzelm@52803 ` 1516` ```lemma polymul_head_polyeq: ``` haftmann@59867 ` 1517` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56066 ` 1518` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ p \ 0\<^sub>p \ q \ 0\<^sub>p \ head (p *\<^sub>p q) = head p *\<^sub>p head q" ``` chaieb@33154 ` 1519` ```proof (induct p q arbitrary: n0 n1 rule: polymul.induct) ``` krauss@41813 ` 1520` ``` case (2 c c' n' p' n0 n1) ``` wenzelm@56009 ` 1521` ``` then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" ``` wenzelm@56009 ` 1522` ``` by (simp_all add: head_isnpolyh) ``` wenzelm@56009 ` 1523` ``` then show ?case ``` wenzelm@56009 ` 1524` ``` using 2 by (cases n') auto ``` wenzelm@52803 ` 1525` ```next ``` wenzelm@52803 ` 1526` ``` case (3 c n p c' n0 n1) ``` wenzelm@56009 ` 1527` ``` then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'" ``` wenzelm@56009 ` 1528` ``` by (simp_all add: head_isnpolyh) ``` wenzelm@56066 ` 1529` ``` then show ?case ``` wenzelm@56066 ` 1530` ``` using 3 by (cases n) auto ``` chaieb@33154 ` 1531` ```next ``` chaieb@33154 ` 1532` ``` case (4 c n p c' n' p' n0 n1) ``` wenzelm@56066 ` 1533` ``` then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" ``` chaieb@33154 ` 1534` ``` "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" ``` chaieb@33154 ` 1535` ``` by simp_all ``` chaieb@33154 ` 1536` ``` have "n < n' \ n' < n \ n = n'" by arith ``` wenzelm@52803 ` 1537` ``` moreover ``` wenzelm@56009 ` 1538` ``` { ``` wenzelm@56009 ` 1539` ``` assume nn': "n < n'" ``` wenzelm@56009 ` 1540` ``` then have ?case ``` wenzelm@52658 ` 1541` ``` using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] ``` wenzelm@52658 ` 1542` ``` apply simp ``` wenzelm@52658 ` 1543` ``` apply (cases n) ``` wenzelm@52658 ` 1544` ``` apply simp ``` wenzelm@52658 ` 1545` ``` apply (cases n') ``` wenzelm@52658 ` 1546` ``` apply simp_all ``` wenzelm@56009 ` 1547` ``` done ``` wenzelm@56009 ` 1548` ``` } ``` wenzelm@56009 ` 1549` ``` moreover { ``` wenzelm@56009 ` 1550` ``` assume nn': "n'< n" ``` wenzelm@56009 ` 1551` ``` then have ?case ``` wenzelm@52803 ` 1552` ``` using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] ``` wenzelm@52658 ` 1553` ``` apply simp ``` wenzelm@52658 ` 1554` ``` apply (cases n') ``` wenzelm@52658 ` 1555` ``` apply simp ``` wenzelm@52658 ` 1556` ``` apply (cases n) ``` wenzelm@52658 ` 1557` ``` apply auto ``` wenzelm@56009 ` 1558` ``` done ``` wenzelm@56009 ` 1559` ``` } ``` wenzelm@56066 ` 1560` ``` moreover ``` wenzelm@56066 ` 1561` ``` { ``` wenzelm@56009 ` 1562` ``` assume nn': "n' = n" ``` wenzelm@52803 ` 1563` ``` from nn' polymul_normh[OF norm(5,4)] ``` chaieb@33154 ` 1564` ``` have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) ``` wenzelm@52803 ` 1565` ``` from nn' polymul_normh[OF norm(5,3)] norm ``` chaieb@33154 ` 1566` ``` have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp ``` chaieb@33154 ` 1567` ``` from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) ``` wenzelm@52803 ` 1568` ``` have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp ``` wenzelm@52803 ` 1569` ``` from polyadd_normh[OF ncnpc' ncnpp0'] ``` wenzelm@52803 ` 1570` ``` have nth: "isnpolyh ((CN c n p *\<^sub>p c') +\<^sub>p (CN 0\<^sub>p n (CN c n p *\<^sub>p p'))) n" ``` chaieb@33154 ` 1571` ``` by (simp add: min_def) ``` wenzelm@56009 ` 1572` ``` { ``` wenzelm@56009 ` 1573` ``` assume np: "n > 0" ``` chaieb@33154 ` 1574` ``` with nn' head_isnpolyh_Suc'[OF np nth] ``` wenzelm@33268 ` 1575` ``` head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] ``` wenzelm@56009 ` 1576` ``` have ?case by simp ``` wenzelm@56009 ` 1577` ``` } ``` chaieb@33154 ` 1578` ``` moreover ``` wenzelm@56009 ` 1579` ``` { ``` wenzelm@56009 ` 1580` ``` assume nz: "n = 0" ``` chaieb@33154 ` 1581` ``` from polymul_degreen[OF norm(5,4), where m="0"] ``` wenzelm@33268 ` 1582` ``` polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 ``` chaieb@33154 ` 1583` ``` norm(5,6) degree_npolyhCN[OF norm(6)] ``` wenzelm@56066 ` 1584` ``` have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" ``` wenzelm@56066 ` 1585` ``` by simp ``` wenzelm@56066 ` 1586` ``` then have dth': "degree (CN c 0 p *\<^sub>p c') \ degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" ``` wenzelm@56066 ` 1587` ``` by simp ``` chaieb@33154 ` 1588` ``` from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth ``` wenzelm@56066 ` 1589` ``` have ?case ``` wenzelm@56066 ` 1590` ``` using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz ``` wenzelm@56066 ` 1591` ``` by simp ``` wenzelm@56009 ` 1592` ``` } ``` wenzelm@56066 ` 1593` ``` ultimately have ?case ``` wenzelm@56066 ` 1594` ``` by (cases n) auto ``` wenzelm@56009 ` 1595` ``` } ``` chaieb@33154 ` 1596` ``` ultimately show ?case by blast ``` chaieb@33154 ` 1597` ```qed simp_all ``` chaieb@33154 ` 1598` chaieb@33154 ` 1599` ```lemma degree_coefficients: "degree p = length (coefficients p) - 1" ``` wenzelm@52658 ` 1600` ``` by (induct p rule: degree.induct) auto ``` chaieb@33154 ` 1601` chaieb@33154 ` 1602` ```lemma degree_head[simp]: "degree (head p) = 0" ``` wenzelm@52658 ` 1603` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1604` krauss@41812 ` 1605` ```lemma degree_CN: "isnpolyh p n \ degree (CN c n p) \ 1 + degree p" ``` wenzelm@52658 ` 1606` ``` by (cases n) simp_all ``` wenzelm@56066 ` 1607` chaieb@33154 ` 1608` ```lemma degree_CN': "isnpolyh p n \ degree (CN c n p) \ degree p" ``` wenzelm@52658 ` 1609` ``` by (cases n) simp_all ``` chaieb@33154 ` 1610` wenzelm@52658 ` 1611` ```lemma polyadd_different_degree: ``` wenzelm@56066 ` 1612` ``` "isnpolyh p n0 \ isnpolyh q n1 \ degree p \ degree q \ ``` wenzelm@52658 ` 1613` ``` degree (polyadd p q) = max (degree p) (degree q)" ``` chaieb@33154 ` 1614` ``` using polyadd_different_degreen degree_eq_degreen0 by simp ``` chaieb@33154 ` 1615` chaieb@33154 ` 1616` ```lemma degreen_polyneg: "isnpolyh p n0 \ degreen (~\<^sub>p p) m = degreen p m" ``` wenzelm@52658 ` 1617` ``` by (induct p arbitrary: n0 rule: polyneg.induct) auto ``` chaieb@33154 ` 1618` chaieb@33154 ` 1619` ```lemma degree_polymul: ``` haftmann@59867 ` 1620` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1621` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1622` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1623` ``` shows "degree (p *\<^sub>p q) \ degree p + degree q" ``` chaieb@33154 ` 1624` ``` using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp ``` chaieb@33154 ` 1625` chaieb@33154 ` 1626` ```lemma polyneg_degree: "isnpolyh p n \ degree (polyneg p) = degree p" ``` wenzelm@52658 ` 1627` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1628` wenzelm@56207 ` 1629` ```lemma polyneg_head: "isnpolyh p n \ head (polyneg p) = polyneg (head p)" ``` wenzelm@52658 ` 1630` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` wenzelm@52658 ` 1631` chaieb@33154 ` 1632` wenzelm@60533 ` 1633` ```subsection \Correctness of polynomial pseudo division\ ``` chaieb@33154 ` 1634` chaieb@33154 ` 1635` ```lemma polydivide_aux_properties: ``` haftmann@59867 ` 1636` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@52658 ` 1637` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1638` ``` and ns: "isnpolyh s n1" ``` wenzelm@52658 ` 1639` ``` and ap: "head p = a" ``` wenzelm@56198 ` 1640` ``` and ndp: "degree p = n" ``` wenzelm@56198 ` 1641` ``` and pnz: "p \ 0\<^sub>p" ``` wenzelm@56198 ` 1642` ``` shows "polydivide_aux a n p k s = (k', r) \ k' \ k \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1643` ``` (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ (polypow (k' - k) a) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` chaieb@33154 ` 1644` ``` using ns ``` wenzelm@52658 ` 1645` ```proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct) ``` berghofe@34915 ` 1646` ``` case less ``` chaieb@33154 ` 1647` ``` let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@56066 ` 1648` ``` let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \ ``` wenzelm@56066 ` 1649` ``` (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" ``` chaieb@33154 ` 1650` ``` let ?b = "head s" ``` berghofe@34915 ` 1651` ``` let ?p' = "funpow (degree s - n) shift1 p" ``` wenzelm@50282 ` 1652` ``` let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p" ``` chaieb@33154 ` 1653` ``` let ?akk' = "a ^\<^sub>p (k' - k)" ``` wenzelm@60533 ` 1654` ``` note ns = \isnpolyh s n1\ ``` wenzelm@52803 ` 1655` ``` from np have np0: "isnpolyh p 0" ``` wenzelm@52803 ` 1656` ``` using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp ``` wenzelm@52803 ` 1657` ``` have np': "isnpolyh ?p' 0" ``` wenzelm@52803 ` 1658` ``` using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def ``` wenzelm@52803 ` 1659` ``` by simp ``` wenzelm@52803 ` 1660` ``` have headp': "head ?p' = head p" ``` wenzelm@52803 ` 1661` ``` using funpow_shift1_head[OF np pnz] by simp ``` wenzelm@52803 ` 1662` ``` from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" ``` wenzelm@52803 ` 1663` ``` by (simp add: isnpoly_def) ``` wenzelm@52803 ` 1664` ``` from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap ``` chaieb@33154 ` 1665` ``` have nakk':"isnpolyh ?akk' 0" by blast ``` wenzelm@56066 ` 1666` ``` { ``` wenzelm@56066 ` 1667` ``` assume sz: "s = 0\<^sub>p" ``` wenzelm@56066 ` 1668` ``` then have ?ths ``` wenzelm@56066 ` 1669` ``` using np polydivide_aux.simps ``` wenzelm@52658 ` 1670` ``` apply clarsimp ``` wenzelm@52658 ` 1671` ``` apply (rule exI[where x="0\<^sub>p"]) ``` wenzelm@52658 ` 1672` ``` apply simp ``` wenzelm@56066 ` 1673` ``` done ``` wenzelm@56066 ` 1674` ``` } ``` chaieb@33154 ` 1675` ``` moreover ``` wenzelm@56066 ` 1676` ``` { ``` wenzelm@56066 ` 1677` ``` assume sz: "s \ 0\<^sub>p" ``` wenzelm@56066 ` 1678` ``` { ``` wenzelm@56066 ` 1679` ``` assume dn: "degree s < n" ``` wenzelm@56066 ` 1680` ``` then have "?ths" ``` wenzelm@56066 ` 1681` ``` using ns ndp np polydivide_aux.simps ``` wenzelm@52658 ` 1682` ``` apply auto ``` wenzelm@52658 ` 1683` ``` apply (rule exI[where x="0\<^sub>p"]) ``` wenzelm@52658 ` 1684` ``` apply simp ``` wenzelm@56066 ` 1685` ``` done ``` wenzelm@56066 ` 1686` ``` } ``` wenzelm@52803 ` 1687` ``` moreover ``` wenzelm@56066 ` 1688` ``` { ``` wenzelm@56066 ` 1689` ``` assume dn': "\ degree s < n" ``` wenzelm@56066 ` 1690` ``` then have dn: "degree s \ n" ``` wenzelm@56066 ` 1691` ``` by arith ``` wenzelm@52803 ` 1692` ``` have degsp': "degree s = degree ?p'" ``` wenzelm@56066 ` 1693` ``` using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] ``` wenzelm@56066 ` 1694` ``` by simp ``` wenzelm@56066 ` 1695` ``` { ``` wenzelm@56066 ` 1696` ``` assume ba: "?b = a" ``` wenzelm@56066 ` 1697` ``` then have headsp': "head s = head ?p'" ``` wenzelm@52803 ` 1698` ``` using ap headp' by simp ``` wenzelm@52803 ` 1699` ``` have nr: "isnpolyh (s -\<^sub>p ?p') 0" ``` wenzelm@52803 ` 1700` ``` using polysub_normh[OF ns np'] by simp ``` berghofe@34915 ` 1701` ``` from degree_polysub_samehead[OF ns np' headsp' degsp'] ``` wenzelm@56207 ` 1702` ``` have "degree (s -\<^sub>p ?p') < degree s \ s -\<^sub>p ?p' = 0\<^sub>p" ``` wenzelm@56207 ` 1703` ``` by simp ``` wenzelm@52803 ` 1704` ``` moreover ``` wenzelm@56066 ` 1705` ``` { ``` wenzelm@56066 ` 1706` ``` assume deglt:"degree (s -\<^sub>p ?p') < degree s" ``` krauss@41403 ` 1707` ``` from polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1708` ``` have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" ``` wenzelm@33268 ` 1709` ``` by (simp add: Let_def) ``` wenzelm@56066 ` 1710` ``` { ``` wenzelm@56066 ` 1711` ``` assume h1: "polydivide_aux a n p k s = (k', r)" ``` wenzelm@52803 ` 1712` ``` from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] ``` wenzelm@52803 ` 1713` ``` have kk': "k \ k'" ``` wenzelm@56066 ` 1714` ``` and nr: "\nr. isnpolyh r nr" ``` wenzelm@52803 ` 1715` ``` and dr: "degree r = 0 \ degree r < degree p" ``` wenzelm@56066 ` 1716` ``` and q1: "\q nq. isnpolyh q nq \ a ^\<^sub>p k' - k *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" ``` wenzelm@52803 ` 1717` ``` by auto ``` wenzelm@52803 ` 1718` ``` from q1 obtain q n1 where nq: "isnpolyh q n1" ``` wenzelm@56066 ` 1719` ``` and asp: "a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" ``` wenzelm@56066 ` 1720` ``` by blast ``` wenzelm@56066 ` 1721` ``` from nr obtain nr where nr': "isnpolyh r nr" ``` wenzelm@56066 ` 1722` ``` by blast ``` wenzelm@52803 ` 1723` ``` from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" ``` wenzelm@52803 ` 1724` ``` by simp ``` wenzelm@33268 ` 1725` ``` from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq] ``` wenzelm@33268 ` 1726` ``` have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp ``` wenzelm@52803 ` 1727` ``` from polyadd_normh[OF polymul_normh[OF np ``` wenzelm@33268 ` 1728` ``` polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr'] ``` wenzelm@52803 ` 1729` ``` have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" ``` wenzelm@52803 ` 1730` ``` by simp ``` haftmann@59867 ` 1731` ``` from asp have "\bs :: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1732` ``` Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@56066 ` 1733` ``` by simp ``` haftmann@59867 ` 1734` ``` then have "\bs :: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1735` ``` Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = ``` wenzelm@52803 ` 1736` ``` Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" ``` haftmann@36349 ` 1737` ``` by (simp add: field_simps) ``` haftmann@59867 ` 1738` ``` then have "\bs :: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1739` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1740` ``` Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) + ``` wenzelm@52803 ` 1741` ``` Ipoly bs p * Ipoly bs q + Ipoly bs r" ``` wenzelm@52803 ` 1742` ``` by (auto simp only: funpow_shift1_1) ``` haftmann@59867 ` 1743` ``` then have "\bs:: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1744` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1745` ``` Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) + ``` wenzelm@52803 ` 1746` ``` Ipoly bs q) + Ipoly bs r" ``` wenzelm@52803 ` 1747` ``` by (simp add: field_simps) ``` haftmann@59867 ` 1748` ``` then have "\bs:: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1749` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1750` ``` Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r)" ``` wenzelm@52803 ` 1751` ``` by simp ``` wenzelm@33268 ` 1752` ``` with isnpolyh_unique[OF nakks' nqr'] ``` wenzelm@52803 ` 1753` ``` have "a ^\<^sub>p (k' - k) *\<^sub>p s = ``` wenzelm@52803 ` 1754` ``` p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q) +\<^sub>p r" ``` wenzelm@52803 ` 1755` ``` by blast ``` wenzelm@56066 ` 1756` ``` then have ?qths using nq' ``` wenzelm@50282 ` 1757` ``` apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 (1)\<^sub>p) +\<^sub>p q" in exI) ``` wenzelm@52803 ` 1758` ``` apply (rule_tac x="0" in exI) ``` wenzelm@52803 ` 1759` ``` apply simp ``` wenzelm@52803 ` 1760` ``` done ``` wenzelm@56066 ` 1761` ``` with kk' nr dr have "k \ k' \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1762` ``` (\nr. isnpolyh r nr) \ ?qths" ``` wenzelm@52803 ` 1763` ``` by blast ``` wenzelm@52803 ` 1764` ``` } ``` wenzelm@56066 ` 1765` ``` then have ?ths by blast ``` wenzelm@52803 ` 1766` ``` } ``` wenzelm@52803 ` 1767` ``` moreover ``` wenzelm@56066 ` 1768` ``` { ``` wenzelm@56066 ` 1769` ``` assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" ``` haftmann@59867 ` 1770` ``` from spz isnpolyh_unique[OF polysub_normh[OF ns np'], where q="0\<^sub>p", symmetric, where ?'a = "'a::{field_char_0,field}"] ``` haftmann@59867 ` 1771` ``` have "\bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs ?p'" ``` wenzelm@52803 ` 1772` ``` by simp ``` haftmann@59867 ` 1773` ``` then have "\bs:: 'a::{field_char_0,field} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" ``` wenzelm@52658 ` 1774` ``` using np nxdn ``` wenzelm@52658 ` 1775` ``` apply simp ``` wenzelm@52658 ` 1776` ``` apply (simp only: funpow_shift1_1) ``` wenzelm@52658 ` 1777` ``` apply simp ``` wenzelm@52658 ` 1778` ``` done ``` wenzelm@56066 ` 1779` ``` then have sp': "s = ?xdn *\<^sub>p p" ``` wenzelm@56066 ` 1780` ``` using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] ``` wenzelm@52658 ` 1781` ``` by blast ``` wenzelm@56066 ` 1782` ``` { ``` wenzelm@56207 ` 1783` ``` assume h1: "polydivide_aux a n p k s = (k', r)" ``` krauss@41403 ` 1784` ``` from polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1785` ``` have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" ``` wenzelm@33268 ` 1786` ``` by (simp add: Let_def) ``` wenzelm@52803 ` 1787` ``` also have "\ = (k,0\<^sub>p)" ``` wenzelm@52803 ` 1788` ``` using polydivide_aux.simps spz by simp ``` wenzelm@56066 ` 1789` ``` finally have "(k', r) = (k, 0\<^sub>p)" ``` wenzelm@56066 ` 1790` ``` using h1 by simp ``` berghofe@34915 ` 1791` ``` with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] ``` krauss@41403 ` 1792` ``` polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths ``` wenzelm@33268 ` 1793` ``` apply auto ``` wenzelm@52803 ` 1794` ``` apply (rule exI[where x="?xdn"]) ``` berghofe@34915 ` 1795` ``` apply (auto simp add: polymul_commute[of p]) ``` wenzelm@52803 ` 1796` ``` done ``` wenzelm@52803 ` 1797` ``` } ``` wenzelm@52803 ` 1798` ``` } ``` wenzelm@52803 ` 1799` ``` ultimately have ?ths by blast ``` wenzelm@52803 ` 1800` ``` } ``` chaieb@33154 ` 1801` ``` moreover ``` wenzelm@56066 ` 1802` ``` { ``` wenzelm@56066 ` 1803` ``` assume ba: "?b \ a" ``` wenzelm@52803 ` 1804` ``` from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] ``` wenzelm@33268 ` 1805` ``` polymul_normh[OF head_isnpolyh[OF ns] np']] ``` wenzelm@52803 ` 1806` ``` have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" ``` wenzelm@52803 ` 1807` ``` by (simp add: min_def) ``` wenzelm@33268 ` 1808` ``` have nzths: "a *\<^sub>p s \ 0\<^sub>p" "?b *\<^sub>p ?p' \ 0\<^sub>p" ``` wenzelm@52803 ` 1809` ``` using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] ``` wenzelm@33268 ` 1810` ``` polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] ``` wenzelm@52803 ` 1811` ``` funpow_shift1_nz[OF pnz] ``` wenzelm@52803 ` 1812` ``` by simp_all ``` wenzelm@33268 ` 1813` ``` from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz ``` berghofe@34915 ` 1814` ``` polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"] ``` wenzelm@52803 ` 1815` ``` have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" ``` wenzelm@33268 ` 1816` ``` using head_head[OF ns] funpow_shift1_head[OF np pnz] ``` wenzelm@33268 ` 1817` ``` polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] ``` wenzelm@33268 ` 1818` ``` by (simp add: ap) ``` wenzelm@33268 ` 1819` ``` from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] ``` wenzelm@33268 ` 1820` ``` head_nz[OF np] pnz sz ap[symmetric] ``` berghofe@34915 ` 1821` ``` funpow_shift1_nz[OF pnz, where n="degree s - n"] ``` wenzelm@52803 ` 1822` ``` polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] ``` berghofe@34915 ` 1823` ``` ndp dn ``` wenzelm@52803 ` 1824` ``` have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p')" ``` wenzelm@33268 ` 1825` ``` by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) ``` wenzelm@56066 ` 1826` ``` { ``` wenzelm@56066 ` 1827` ``` assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" ``` wenzelm@52803 ` 1828` ``` from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] ``` wenzelm@52803 ` 1829` ``` polymul_normh[OF head_isnpolyh[OF ns]np']] ap ``` wenzelm@52803 ` 1830` ``` have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" ``` wenzelm@52803 ` 1831` ``` by simp ``` wenzelm@56066 ` 1832` ``` { ``` wenzelm@56066 ` 1833` ``` assume h1:"polydivide_aux a n p k s = (k', r)" ``` krauss@41403 ` 1834` ``` from h1 polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1835` ``` have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" ``` wenzelm@33268 ` 1836` ``` by (simp add: Let_def) ``` berghofe@34915 ` 1837` ``` with less(1)[OF dth nasbp', of "Suc k" k' r] ``` wenzelm@52803 ` 1838` ``` obtain q nq nr where kk': "Suc k \ k'" ``` wenzelm@52803 ` 1839` ``` and nr: "isnpolyh r nr" ``` wenzelm@52803 ` 1840` ``` and nq: "isnpolyh q nq" ``` wenzelm@33268 ` 1841` ``` and dr: "degree r = 0 \ degree r < degree p" ``` wenzelm@52803 ` 1842` ``` and qr: "a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = p *\<^sub>p q +\<^sub>p r" ``` wenzelm@52803 ` 1843` ``` by auto ``` wenzelm@56066 ` 1844` ``` from kk' have kk'': "Suc (k' - Suc k) = k' - k" ``` wenzelm@56066 ` 1845` ``` by arith ``` wenzelm@52803 ` 1846` ``` { ``` haftmann@59867 ` 1847` ``` fix bs :: "'a::{field_char_0,field} list" ``` wenzelm@52803 ` 1848` ``` from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] ``` wenzelm@52803 ` 1849` ``` have "Ipoly bs (a ^\<^sub>p (k' - Suc k) *\<^sub>p ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@52803 ` 1850` ``` by simp ``` wenzelm@56066 ` 1851` ``` then have "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = ``` wenzelm@52803 ` 1852` ``` Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" ``` wenzelm@52803 ` 1853` ``` by (simp add: field_simps) ``` wenzelm@56066 ` 1854` ``` then have "Ipoly bs a ^ (k' - k) * Ipoly bs s = ``` wenzelm@52803 ` 1855` ``` Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn * Ipoly bs p + Ipoly bs r" ``` wenzelm@52803 ` 1856` ``` by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) ``` wenzelm@56066 ` 1857` ``` then have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1858` ``` Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" ``` wenzelm@52803 ` 1859` ``` by (simp add: field_simps) ``` wenzelm@52803 ` 1860` ``` } ``` haftmann@59867 ` 1861` ``` then have ieq:"\bs :: 'a::{field_char_0,field} list. ``` wenzelm@56207 ` 1862` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@56207 ` 1863` ``` Ipoly bs (p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r)" ``` wenzelm@52803 ` 1864` ``` by auto ``` wenzelm@33268 ` 1865` ``` let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" ``` wenzelm@56207 ` 1866` ``` from polyadd_normh[OF nq polymul_normh[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k"] head_isnpolyh[OF ns], simplified ap] nxdn]] ``` wenzelm@52803 ` 1867` ``` have nqw: "isnpolyh ?q 0" ``` wenzelm@52803 ` 1868` ``` by simp ``` wenzelm@33268 ` 1869` ``` from ieq isnpolyh_unique[OF polymul_normh[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - k"] ns, simplified ap] polyadd_normh[OF polymul_normh[OF np nqw] nr]] ``` wenzelm@52803 ` 1870` ``` have asth: "(a ^\<^sub>p (k' - k) *\<^sub>p s) = p *\<^sub>p (q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)) +\<^sub>p r" ``` wenzelm@52803 ` 1871` ``` by blast ``` wenzelm@52803 ` 1872` ``` from dr kk' nr h1 asth nqw have ?ths ``` wenzelm@52803 ` 1873` ``` apply simp ``` wenzelm@33268 ` 1874` ``` apply (rule conjI) ``` wenzelm@33268 ` 1875` ``` apply (rule exI[where x="nr"], simp) ``` wenzelm@33268 ` 1876` ``` apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp) ``` wenzelm@33268 ` 1877` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@52803 ` 1878` ``` done ``` wenzelm@52803 ` 1879` ``` } ``` wenzelm@56066 ` 1880` ``` then have ?ths by blast ``` wenzelm@52803 ` 1881` ``` } ``` wenzelm@52803 ` 1882` ``` moreover ``` wenzelm@56066 ` 1883` ``` { ``` wenzelm@56066 ` 1884` ``` assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" ``` wenzelm@52803 ` 1885` ``` { ``` haftmann@59867 ` 1886` ``` fix bs :: "'a::{field_char_0,field} list" ``` wenzelm@33268 ` 1887` ``` from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz ``` wenzelm@52803 ` 1888` ``` have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" ``` wenzelm@52803 ` 1889` ``` by simp ``` wenzelm@56066 ` 1890` ``` then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" ``` wenzelm@52803 ` 1891` ``` by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) ``` wenzelm@56066 ` 1892` ``` then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ``` wenzelm@52803 ` 1893` ``` by simp ``` wenzelm@52803 ` 1894` ``` } ``` haftmann@59867 ` 1895` ``` then have hth: "\bs :: 'a::{field_char_0,field} list. ``` wenzelm@56066 ` 1896` ``` Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. ``` wenzelm@52803 ` 1897` ``` from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" ``` haftmann@59867 ` 1898` ``` using isnpolyh_unique[where ?'a = "'a::{field_char_0,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] ``` chaieb@33154 ` 1899` ``` polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], ``` wenzelm@56066 ` 1900` ``` simplified ap] ``` wenzelm@56066 ` 1901` ``` by simp ``` wenzelm@56066 ` 1902` ``` { ``` wenzelm@56066 ` 1903` ``` assume h1: "polydivide_aux a n p k s = (k', r)" ``` wenzelm@52803 ` 1904` ``` from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps ``` wenzelm@56066 ` 1905` ``` have "(k', r) = (Suc k, 0\<^sub>p)" ``` wenzelm@56066 ` 1906` ``` by (simp add: Let_def) ``` wenzelm@52803 ` 1907` ``` with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] ``` wenzelm@52803 ` 1908` ``` polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq ``` wenzelm@52803 ` 1909` ``` have ?ths ``` wenzelm@52803 ` 1910` ``` apply (clarsimp simp add: Let_def) ``` wenzelm@52803 ` 1911` ``` apply (rule exI[where x="?b *\<^sub>p ?xdn"]) ``` wenzelm@52803 ` 1912` ``` apply simp ``` wenzelm@52803 ` 1913` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@52803 ` 1914` ``` done ``` wenzelm@52803 ` 1915` ``` } ``` wenzelm@56066 ` 1916` ``` then have ?ths by blast ``` wenzelm@52803 ` 1917` ``` } ``` wenzelm@52658 ` 1918` ``` ultimately have ?ths ``` wenzelm@56066 ` 1919` ``` using degree_polysub_samehead[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] polymul_normh[OF head_isnpolyh[OF ns] np'] hdth degth] polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] ``` wenzelm@52658 ` 1920` ``` head_nz[OF np] pnz sz ap[symmetric] ``` wenzelm@56066 ` 1921` ``` by (auto simp add: degree_eq_degreen0[symmetric]) ``` wenzelm@52803 ` 1922` ``` } ``` chaieb@33154 ` 1923` ``` ultimately have ?ths by blast ``` chaieb@33154 ` 1924` ``` } ``` wenzelm@52803 ` 1925` ``` ultimately have ?ths by blast ``` wenzelm@52803 ` 1926` ``` } ``` chaieb@33154 ` 1927` ``` ultimately show ?ths by blast ``` chaieb@33154 ` 1928` ```qed ``` chaieb@33154 ` 1929` wenzelm@52803 ` 1930` ```lemma polydivide_properties: ``` haftmann@59867 ` 1931` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` wenzelm@56066 ` 1932` ``` and np: "isnpolyh p n0" ``` wenzelm@56066 ` 1933` ``` and ns: "isnpolyh s n1" ``` wenzelm@56066 ` 1934` ``` and pnz: "p \ 0\<^sub>p" ``` wenzelm@56066 ` 1935` ``` shows "\k r. polydivide s p = (k, r) \ ``` wenzelm@52803 ` 1936` ``` (\nr. isnpolyh r nr) \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1937` ``` (\q n1. isnpolyh q n1 \ polypow k (head p) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@52803 ` 1938` ```proof - ``` wenzelm@52803 ` 1939` ``` have trv: "head p = head p" "degree p = degree p" ``` wenzelm@52803 ` 1940` ``` by simp_all ``` wenzelm@52803 ` 1941` ``` from polydivide_def[where s="s" and p="p"] have ex: "\ k r. polydivide s p = (k,r)" ``` wenzelm@52803 ` 1942` ``` by auto ``` wenzelm@52803 ` 1943` ``` then obtain k r where kr: "polydivide s p = (k,r)" ``` wenzelm@52803 ` 1944` ``` by blast ``` wenzelm@56000 ` 1945` ``` from trans[OF polydivide_def[where s="s"and p="p", symmetric] kr] ``` chaieb@33154 ` 1946` ``` polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"] ``` chaieb@33154 ` 1947` ``` have "(degree r = 0 \ degree r < degree p) \ ``` wenzelm@52803 ` 1948` ``` (\nr. isnpolyh r nr) \ (\q n1. isnpolyh q n1 \ head p ^\<^sub>p k - 0 *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@52803 ` 1949` ``` by blast ``` wenzelm@52803 ` 1950` ``` with kr show ?thesis ``` chaieb@33154 ` 1951` ``` apply - ``` chaieb@33154 ` 1952` ``` apply (rule exI[where x="k"]) ``` chaieb@33154 ` 1953` ``` apply (rule exI[where x="r"]) ``` chaieb@33154 ` 1954` ``` apply simp ``` chaieb@33154 ` 1955` ``` done ``` chaieb@33154 ` 1956` ```qed ``` chaieb@33154 ` 1957` wenzelm@52658 ` 1958` wenzelm@60533 ` 1959` ```subsection \More about polypoly and pnormal etc\ ``` chaieb@33154 ` 1960` wenzelm@56000 ` 1961` ```definition "isnonconstant p \ \ isconstant p" ``` chaieb@33154 ` 1962` wenzelm@52658 ` 1963` ```lemma isnonconstant_pnormal_iff: ``` wenzelm@56198 ` 1964` ``` assumes "isnonconstant p" ``` wenzelm@52803 ` 1965` ``` shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" ``` chaieb@33154 ` 1966` ```proof ``` wenzelm@52803 ` 1967` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 1968` ``` assume H: "pnormal ?p" ``` wenzelm@56066 ` 1969` ``` have csz: "coefficients p \ []" ``` wenzelm@56198 ` 1970` ``` using assms by (cases p) auto ``` wenzelm@56066 ` 1971` ``` from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H] ``` wenzelm@56066 ` 1972` ``` show "Ipoly bs (head p) \ 0" ``` wenzelm@56066 ` 1973` ``` by (simp add: polypoly_def) ``` chaieb@33154 ` 1974` ```next ``` chaieb@33154 ` 1975` ``` assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` chaieb@33154 ` 1976` ``` let ?p = "polypoly bs p" ``` wenzelm@56066 ` 1977` ``` have csz: "coefficients p \ []" ``` wenzelm@56198 ` 1978` ``` using assms by (cases p) auto ``` wenzelm@56066 ` 1979` ``` then have pz: "?p \ []" ``` wenzelm@56066 ` 1980` ``` by (simp add: polypoly_def) ``` wenzelm@56066 ` 1981` ``` then have lg: "length ?p > 0" ``` wenzelm@56066 ` 1982` ``` by simp ``` wenzelm@52803 ` 1983` ``` from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] ``` wenzelm@56066 ` 1984` ``` have lz: "last ?p \ 0" ``` wenzelm@56066 ` 1985` ``` by (simp add: polypoly_def) ``` chaieb@33154 ` 1986` ``` from pnormal_last_length[OF lg lz] show "pnormal ?p" . ``` chaieb@33154 ` 1987` ```qed ``` chaieb@33154 ` 1988` chaieb@33154 ` 1989` ```lemma isnonconstant_coefficients_length: "isnonconstant p \ length (coefficients p) > 1" ``` chaieb@33154 ` 1990` ``` unfolding isnonconstant_def ``` wenzelm@52658 ` 1991` ``` apply (cases p) ``` wenzelm@52658 ` 1992` ``` apply simp_all ``` blanchet@58259 ` 1993` ``` apply (rename_tac nat a, case_tac nat) ``` wenzelm@52658 ` 1994` ``` apply auto ``` chaieb@33154 ` 1995` ``` done ``` wenzelm@52658 ` 1996` wenzelm@52658 ` 1997` ```lemma isnonconstant_nonconstant: ``` wenzelm@56198 ` 1998` ``` assumes "isnonconstant p" ``` chaieb@33154 ` 1999` ``` shows "nonconstant (polypoly bs p) \ Ipoly bs (head p) \ 0" ``` chaieb@33154 ` 2000` ```proof ``` chaieb@33154 ` 2001` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2002` ``` assume nc: "nonconstant ?p" ``` wenzelm@56198 ` 2003` ``` from isnonconstant_pnormal_iff[OF assms, of bs] nc ``` wenzelm@56066 ` 2004` ``` show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56066 ` 2005` ``` unfolding nonconstant_def by blast ``` chaieb@33154 ` 2006` ```next ``` chaieb@33154 ` 2007` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2008` ``` assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56198 ` 2009` ``` from isnonconstant_pnormal_iff[OF assms, of bs] h ``` wenzelm@56066 ` 2010` ``` have pn: "pnormal ?p" ``` wenzelm@56066 ` 2011` ``` by blast ``` wenzelm@56009 ` 2012` ``` { ``` wenzelm@56009 ` 2013` ``` fix x ``` wenzelm@56009 ` 2014` ``` assume H: "?p = [x]" ``` wenzelm@56009 ` 2015` ``` from H have "length (coefficients p) = 1" ``` wenzelm@56009 ` 2016` ``` unfolding polypoly_def by auto ``` wenzelm@56198 ` 2017` ``` with isnonconstant_coefficients_length[OF assms] ``` wenzelm@56198 ` 2018` ``` have False by arith ``` wenzelm@56009 ` 2019` ``` } ``` wenzelm@56009 ` 2020` ``` then show "nonconstant ?p" ``` wenzelm@56009 ` 2021` ``` using pn unfolding nonconstant_def by blast ``` chaieb@33154 ` 2022` ```qed ``` chaieb@33154 ` 2023` wenzelm@56066 ` 2024` ```lemma pnormal_length: "p \ [] \ pnormal p \ length (pnormalize p) = length p" ``` wenzelm@52658 ` 2025` ``` apply (induct p) ``` wenzelm@52658 ` 2026` ``` apply (simp_all add: pnormal_def) ``` wenzelm@52658 ` 2027` ``` apply (case_tac "p = []") ``` wenzelm@52658 ` 2028` ``` apply simp_all ``` wenzelm@52658 ` 2029` ``` done ``` chaieb@33154 ` 2030` wenzelm@52658 ` 2031` ```lemma degree_degree: ``` wenzelm@56207 ` 2032` ``` assumes "isnonconstant p" ``` chaieb@33154 ` 2033` ``` shows "degree p = Polynomial_List.degree (polypoly bs p) \ \head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` chaieb@33154 ` 2034` ```proof ``` wenzelm@52803 ` 2035` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2036` ``` assume H: "degree p = Polynomial_List.degree ?p" ``` wenzelm@56207 ` 2037` ``` from isnonconstant_coefficients_length[OF assms] have pz: "?p \ []" ``` chaieb@33154 ` 2038` ``` unfolding polypoly_def by auto ``` wenzelm@56207 ` 2039` ``` from H degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] ``` wenzelm@56066 ` 2040` ``` have lg: "length (pnormalize ?p) = length ?p" ``` chaieb@33154 ` 2041` ``` unfolding Polynomial_List.degree_def polypoly_def by simp ``` wenzelm@56066 ` 2042` ``` then have "pnormal ?p" ``` wenzelm@56066 ` 2043` ``` using pnormal_length[OF pz] by blast ``` wenzelm@56207 ` 2044` ``` with isnonconstant_pnormal_iff[OF assms] show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56066 ` 2045` ``` by blast ``` chaieb@33154 ` 2046` ```next ``` wenzelm@56066 ` 2047` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2048` ``` assume H: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56207 ` 2049` ``` with isnonconstant_pnormal_iff[OF assms] have "pnormal ?p" ``` wenzelm@56066 ` 2050` ``` by blast ``` wenzelm@56207 ` 2051` ``` with degree_coefficients[of p] isnonconstant_coefficients_length[OF assms] ``` wenzelm@52803 ` 2052` ``` show "degree p = Polynomial_List.degree ?p" ``` chaieb@33154 ` 2053` ``` unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto ``` chaieb@33154 ` 2054` ```qed ``` chaieb@33154 ` 2055` wenzelm@52658 ` 2056` wenzelm@60533 ` 2057` ```section \Swaps ; Division by a certain variable\ ``` wenzelm@52658 ` 2058` wenzelm@56066 ` 2059` ```primrec swap :: "nat \ nat \ poly \ poly" ``` wenzelm@56066 ` 2060` ```where ``` chaieb@33154 ` 2061` ``` "swap n m (C x) = C x" ``` wenzelm@56198 ` 2062` ```| "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)" ``` haftmann@39246 ` 2063` ```| "swap n m (Neg t) = Neg (swap n m t)" ``` haftmann@39246 ` 2064` ```| "swap n m (Add s t) = Add (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2065` ```| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2066` ```| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2067` ```| "swap n m (Pw t k) = Pw (swap n m t) k" ``` wenzelm@56066 ` 2068` ```| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)" ``` chaieb@33154 ` 2069` wenzelm@52658 ` 2070` ```lemma swap: ``` wenzelm@56066 ` 2071` ``` assumes "n < length bs" ``` wenzelm@56066 ` 2072` ``` and "m < length bs" ``` chaieb@33154 ` 2073` ``` shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" ``` chaieb@33154 ` 2074` ```proof (induct t) ``` wenzelm@52658 ` 2075` ``` case (Bound k) ``` wenzelm@56066 ` 2076` ``` then show ?case ``` wenzelm@56066 ` 2077` ``` using assms by simp ``` chaieb@33154 ` 2078` ```next ``` wenzelm@52658 ` 2079` ``` case (CN c k p) ``` wenzelm@56066 ` 2080` ``` then show ?case ``` wenzelm@56066 ` 2081` ``` using assms by simp ``` chaieb@33154 ` 2082` ```qed simp_all ``` chaieb@33154 ` 2083` wenzelm@52658 ` 2084` ```lemma swap_swap_id [simp]: "swap n m (swap m n t) = t" ``` wenzelm@52658 ` 2085` ``` by (induct t) simp_all ``` wenzelm@52658 ` 2086` wenzelm@52658 ` 2087` ```lemma swap_commute: "swap n m p = swap m n p" ``` wenzelm@52658 ` 2088` ``` by (induct p) simp_all ``` chaieb@33154 ` 2089` chaieb@33154 ` 2090` ```lemma swap_same_id[simp]: "swap n n t = t" ``` wenzelm@52658 ` 2091` ``` by (induct t) simp_all ``` chaieb@33154 ` 2092` chaieb@33154 ` 2093` ```definition "swapnorm n m t = polynate (swap n m t)" ``` chaieb@33154 ` 2094` wenzelm@52658 ` 2095` ```lemma swapnorm: ``` wenzelm@52658 ` 2096` ``` assumes nbs: "n < length bs" ``` wenzelm@52658 ` 2097` ``` and mbs: "m < length bs" ``` haftmann@59867 ` 2098` ``` shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field})) = ``` wenzelm@52658 ` 2099` ``` Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" ``` wenzelm@41807 ` 2100` ``` using swap[OF assms] swapnorm_def by simp ``` chaieb@33154 ` 2101` wenzelm@52658 ` 2102` ```lemma swapnorm_isnpoly [simp]: ``` haftmann@59867 ` 2103` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field})" ``` chaieb@33154 ` 2104` ``` shows "isnpoly (swapnorm n m p)" ``` chaieb@33154 ` 2105` ``` unfolding swapnorm_def by simp ``` chaieb@33154 ` 2106` wenzelm@52803 ` 2107` ```definition "polydivideby n s p = ``` wenzelm@56000 ` 2108` ``` (let ``` wenzelm@56000 ` 2109` ``` ss = swapnorm 0 n s; ``` wenzelm@56000 ` 2110` ``` sp = swapnorm 0 n p; ``` wenzelm@56000 ` 2111` ``` h = head sp; ``` wenzelm@56000 ` 2112` ``` (k, r) = polydivide ss sp ``` wenzelm@56000 ` 2113` ``` in (k, swapnorm 0 n h, swapnorm 0 n r))" ``` chaieb@33154 ` 2114` wenzelm@56000 ` 2115` ```lemma swap_nz [simp]: "swap n m p = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 2116` ``` by (induct p) simp_all ``` chaieb@33154 ` 2117` krauss@41808 ` 2118` ```fun isweaknpoly :: "poly \ bool" ``` krauss@41808 ` 2119` ```where ``` chaieb@33154 ` 2120` ``` "isweaknpoly (C c) = True" ``` krauss@41808 ` 2121` ```| "isweaknpoly (CN c n p) \ isweaknpoly c \ isweaknpoly p" ``` krauss@41808 ` 2122` ```| "isweaknpoly p = False" ``` chaieb@33154 ` 2123` wenzelm@52803 ` 2124` ```lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \ isweaknpoly p" ``` wenzelm@52658 ` 2125` ``` by (induct p arbitrary: n0) auto ``` chaieb@33154 ` 2126` wenzelm@52803 ` 2127` ```lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" ``` wenzelm@52658 ` 2128` ``` by (induct p) auto ``` chaieb@33154 ` 2129` chaieb@33154 ` 2130` `end`