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