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