src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
 author wenzelm Tue Mar 18 10:00:23 2014 +0100 (2014-03-18) changeset 56198 21dd034523e5 parent 56073 29e308b56d23 child 56207 52d5067ca06a 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` wenzelm@56043 ` 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 ``` wenzelm@56043 ` 145` ``` "polymul (C c) (C c') = C (c *\<^sub>N c')" ``` 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` ``` done ``` wenzelm@52803 ` 477` ``` } ``` wenzelm@56009 ` 478` ``` ultimately have ?case by blast ``` wenzelm@56009 ` 479` ``` } ``` chaieb@33154 ` 480` ``` ultimately show ?case by blast ``` chaieb@33154 ` 481` ```qed simp_all ``` chaieb@33154 ` 482` chaieb@33154 ` 483` ```lemma polymul_properties: ``` wenzelm@56000 ` 484` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 485` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 486` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 487` ``` and m: "m \ min n0 n1" ``` wenzelm@52803 ` 488` ``` shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" ``` wenzelm@56009 ` 489` ``` and "p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p" ``` wenzelm@56009 ` 490` ``` 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 ` 491` ``` using np nq m ``` wenzelm@52658 ` 492` ```proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) ``` wenzelm@52803 ` 493` ``` case (2 c c' n' p') ``` wenzelm@56009 ` 494` ``` { ``` wenzelm@56009 ` 495` ``` case (1 n0 n1) ``` wenzelm@56009 ` 496` ``` with "2.hyps"(4-6)[of n' n' n'] and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n'] ``` krauss@41811 ` 497` ``` show ?case by (auto simp add: min_def) ``` chaieb@33154 ` 498` ``` next ``` wenzelm@56009 ` 499` ``` case (2 n0 n1) ``` wenzelm@56009 ` 500` ``` then show ?case by auto ``` chaieb@33154 ` 501` ``` next ``` wenzelm@56009 ` 502` ``` case (3 n0 n1) ``` wenzelm@56009 ` 503` ``` then show ?case using "2.hyps" by auto ``` wenzelm@56009 ` 504` ``` } ``` chaieb@33154 ` 505` ```next ``` krauss@41813 ` 506` ``` case (3 c n p c') ``` wenzelm@56009 ` 507` ``` { ``` wenzelm@56009 ` 508` ``` case (1 n0 n1) ``` wenzelm@56009 ` 509` ``` with "3.hyps"(4-6)[of n n n] and "3.hyps"(1-3)[of "Suc n" "Suc n" n] ``` krauss@41811 ` 510` ``` show ?case by (auto simp add: min_def) ``` chaieb@33154 ` 511` ``` next ``` wenzelm@56009 ` 512` ``` case (2 n0 n1) ``` wenzelm@56009 ` 513` ``` then show ?case by auto ``` chaieb@33154 ` 514` ``` next ``` wenzelm@56009 ` 515` ``` case (3 n0 n1) ``` wenzelm@56009 ` 516` ``` then show ?case using "3.hyps" by auto ``` wenzelm@56009 ` 517` ``` } ``` chaieb@33154 ` 518` ```next ``` chaieb@33154 ` 519` ``` case (4 c n p c' n' p') ``` chaieb@33154 ` 520` ``` let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'" ``` wenzelm@56009 ` 521` ``` { ``` wenzelm@56009 ` 522` ``` case (1 n0 n1) ``` wenzelm@56009 ` 523` ``` then have cnp: "isnpolyh ?cnp n" ``` wenzelm@56009 ` 524` ``` and cnp': "isnpolyh ?cnp' n'" ``` wenzelm@56009 ` 525` ``` and np: "isnpolyh p n" ``` wenzelm@56009 ` 526` ``` and nc: "isnpolyh c (Suc n)" ``` wenzelm@56009 ` 527` ``` and np': "isnpolyh p' n'" ``` wenzelm@56009 ` 528` ``` and nc': "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 529` ``` and nn0: "n \ n0" ``` wenzelm@56009 ` 530` ``` and nn1: "n' \ n1" ``` wenzelm@56009 ` 531` ``` by simp_all ``` krauss@41811 ` 532` ``` { ``` wenzelm@56009 ` 533` ``` assume "n < n'" ``` wenzelm@56009 ` 534` ``` with "4.hyps"(4-5)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp ``` wenzelm@56009 ` 535` ``` have ?case by (simp add: min_def) ``` wenzelm@56009 ` 536` ``` } moreover { ``` wenzelm@56009 ` 537` ``` assume "n' < n" ``` wenzelm@56009 ` 538` ``` with "4.hyps"(16-17)[OF cnp np', of "n'"] and "4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' ``` wenzelm@56009 ` 539` ``` have ?case by (cases "Suc n' = n") (simp_all add: min_def) ``` wenzelm@56009 ` 540` ``` } moreover { ``` wenzelm@56009 ` 541` ``` assume "n' = n" ``` wenzelm@56009 ` 542` ``` 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 ` 543` ``` have ?case ``` wenzelm@56009 ` 544` ``` apply (auto intro!: polyadd_normh) ``` wenzelm@56009 ` 545` ``` apply (simp_all add: min_def isnpolyh_mono[OF nn0]) ``` wenzelm@56009 ` 546` ``` done ``` wenzelm@56009 ` 547` ``` } ``` wenzelm@56009 ` 548` ``` ultimately show ?case by arith ``` wenzelm@56009 ` 549` ``` next ``` wenzelm@56009 ` 550` ``` fix n0 n1 m ``` wenzelm@56009 ` 551` ``` assume np: "isnpolyh ?cnp n0" ``` wenzelm@56009 ` 552` ``` assume np':"isnpolyh ?cnp' n1" ``` wenzelm@56009 ` 553` ``` assume m: "m \ min n0 n1" ``` wenzelm@56009 ` 554` ``` let ?d = "degreen (?cnp *\<^sub>p ?cnp') m" ``` wenzelm@56009 ` 555` ``` let ?d1 = "degreen ?cnp m" ``` wenzelm@56009 ` 556` ``` let ?d2 = "degreen ?cnp' m" ``` wenzelm@56009 ` 557` ``` let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)" ``` wenzelm@56043 ` 558` ``` have "n' < n \ n < n' \ n' = n" by auto ``` wenzelm@56009 ` 559` ``` moreover ``` wenzelm@56009 ` 560` ``` { ``` wenzelm@56009 ` 561` ``` assume "n' < n \ n < n'" ``` wenzelm@56009 ` 562` ``` with "4.hyps"(3,6,18) np np' m have ?eq ``` wenzelm@56009 ` 563` ``` by auto ``` wenzelm@56009 ` 564` ``` } ``` wenzelm@56009 ` 565` ``` moreover ``` wenzelm@56009 ` 566` ``` { ``` wenzelm@56009 ` 567` ``` assume nn': "n' = n" ``` wenzelm@56009 ` 568` ``` then have nn: "\ n' < n \ \ n < n'" by arith ``` wenzelm@56009 ` 569` ``` from "4.hyps"(16,18)[of n n' n] ``` wenzelm@56009 ` 570` ``` "4.hyps"(13,14)[of n "Suc n'" n] ``` wenzelm@56009 ` 571` ``` np np' nn' ``` wenzelm@56043 ` 572` ``` have norm: ``` wenzelm@56043 ` 573` ``` "isnpolyh ?cnp n" ``` wenzelm@56043 ` 574` ``` "isnpolyh c' (Suc n)" ``` wenzelm@56043 ` 575` ``` "isnpolyh (?cnp *\<^sub>p c') n" ``` wenzelm@56043 ` 576` ``` "isnpolyh p' n" ``` wenzelm@56043 ` 577` ``` "isnpolyh (?cnp *\<^sub>p p') n" ``` wenzelm@56043 ` 578` ``` "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56043 ` 579` ``` "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p" ``` wenzelm@56043 ` 580` ``` "?cnp *\<^sub>p p' \ 0\<^sub>p" ``` wenzelm@56043 ` 581` ``` by (auto simp add: min_def) ``` wenzelm@56009 ` 582` ``` { ``` wenzelm@56009 ` 583` ``` assume mn: "m = n" ``` wenzelm@56009 ` 584` ``` from "4.hyps"(17,18)[OF norm(1,4), of n] ``` wenzelm@56009 ` 585` ``` "4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn ``` wenzelm@56009 ` 586` ``` have degs: ``` wenzelm@56009 ` 587` ``` "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else ?d1 + degreen c' n)" ``` wenzelm@56009 ` 588` ``` "degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" ``` wenzelm@56009 ` 589` ``` by (simp_all add: min_def) ``` wenzelm@56009 ` 590` ``` from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 591` ``` by simp ``` wenzelm@56009 ` 592` ``` then have neq: "degreen (?cnp *\<^sub>p c') n \ degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 593` ``` by simp ``` wenzelm@56009 ` 594` ``` have nmin: "n \ min n n" ``` wenzelm@56009 ` 595` ``` by (simp add: min_def) ``` wenzelm@56009 ` 596` ``` from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 ``` wenzelm@56009 ` 597` ``` 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 ` 598` ``` degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 599` ``` by simp ``` wenzelm@56009 ` 600` ``` from "4.hyps"(16-18)[OF norm(1,4), of n] ``` wenzelm@56009 ` 601` ``` "4.hyps"(13-15)[OF norm(1,2), of n] ``` wenzelm@56009 ` 602` ``` mn norm m nn' deg ``` wenzelm@56009 ` 603` ``` have ?eq by simp ``` krauss@41811 ` 604` ``` } ``` chaieb@33154 ` 605` ``` moreover ``` wenzelm@56009 ` 606` ``` { ``` wenzelm@56009 ` 607` ``` assume mn: "m \ n" ``` wenzelm@56009 ` 608` ``` then have mn': "m < n" ``` wenzelm@56009 ` 609` ``` using m np by auto ``` wenzelm@56009 ` 610` ``` from nn' m np have max1: "m \ max n n" ``` wenzelm@56009 ` 611` ``` by simp ``` wenzelm@56009 ` 612` ``` then have min1: "m \ min n n" ``` wenzelm@56009 ` 613` ``` by simp ``` wenzelm@56009 ` 614` ``` then have min2: "m \ min n (Suc n)" ``` wenzelm@56009 ` 615` ``` by simp ``` wenzelm@56009 ` 616` ``` from "4.hyps"(16-18)[OF norm(1,4) min1] ``` wenzelm@56009 ` 617` ``` "4.hyps"(13-15)[OF norm(1,2) min2] ``` wenzelm@56009 ` 618` ``` degreen_polyadd[OF norm(3,6) max1] ``` wenzelm@56009 ` 619` ``` have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m \ ``` wenzelm@56009 ` 620` ``` max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" ``` wenzelm@56009 ` 621` ``` using mn nn' np np' by simp ``` wenzelm@56009 ` 622` ``` with "4.hyps"(16-18)[OF norm(1,4) min1] ``` wenzelm@56009 ` 623` ``` "4.hyps"(13-15)[OF norm(1,2) min2] ``` wenzelm@56009 ` 624` ``` degreen_0[OF norm(3) mn'] ``` wenzelm@56009 ` 625` ``` have ?eq using nn' mn np np' by clarsimp ``` wenzelm@56009 ` 626` ``` } ``` wenzelm@56009 ` 627` ``` ultimately have ?eq by blast ``` wenzelm@56009 ` 628` ``` } ``` wenzelm@56009 ` 629` ``` ultimately show ?eq by blast ``` wenzelm@56009 ` 630` ``` } ``` wenzelm@56009 ` 631` ``` { ``` wenzelm@56009 ` 632` ``` case (2 n0 n1) ``` wenzelm@56009 ` 633` ``` then have np: "isnpolyh ?cnp n0" ``` wenzelm@56009 ` 634` ``` and np': "isnpolyh ?cnp' n1" ``` wenzelm@56043 ` 635` ``` and m: "m \ min n0 n1" ``` wenzelm@56043 ` 636` ``` by simp_all ``` wenzelm@56009 ` 637` ``` then have mn: "m \ n" by simp ``` wenzelm@56009 ` 638` ``` let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" ``` wenzelm@56009 ` 639` ``` { ``` wenzelm@56009 ` 640` ``` assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n" ``` wenzelm@56009 ` 641` ``` then have nn: "\ n' < n \ \ n < n'" ``` wenzelm@56009 ` 642` ``` by simp ``` wenzelm@56009 ` 643` ``` from "4.hyps"(16-18) [of n n n] ``` wenzelm@56009 ` 644` ``` "4.hyps"(13-15)[of n "Suc n" n] ``` wenzelm@56009 ` 645` ``` np np' C(2) mn ``` wenzelm@56009 ` 646` ``` have norm: ``` wenzelm@56009 ` 647` ``` "isnpolyh ?cnp n" ``` wenzelm@56009 ` 648` ``` "isnpolyh c' (Suc n)" ``` wenzelm@56009 ` 649` ``` "isnpolyh (?cnp *\<^sub>p c') n" ``` wenzelm@56009 ` 650` ``` "isnpolyh p' n" ``` wenzelm@56009 ` 651` ``` "isnpolyh (?cnp *\<^sub>p p') n" ``` wenzelm@56009 ` 652` ``` "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 653` ``` "?cnp *\<^sub>p c' = 0\<^sub>p \ c' = 0\<^sub>p" ``` wenzelm@56009 ` 654` ``` "?cnp *\<^sub>p p' \ 0\<^sub>p" ``` wenzelm@56009 ` 655` ``` "degreen (?cnp *\<^sub>p c') n = (if c' = 0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" ``` wenzelm@56009 ` 656` ``` "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" ``` wenzelm@56009 ` 657` ``` by (simp_all add: min_def) ``` wenzelm@56009 ` 658` ``` from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" ``` wenzelm@56009 ` 659` ``` by simp ``` wenzelm@56009 ` 660` ``` have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" ``` wenzelm@56009 ` 661` ``` using norm by simp ``` wenzelm@56009 ` 662` ``` from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq ``` wenzelm@56009 ` 663` ``` have False by simp ``` wenzelm@56009 ` 664` ``` } ``` wenzelm@56009 ` 665` ``` then show ?case using "4.hyps" by clarsimp ``` wenzelm@56009 ` 666` ``` } ``` chaieb@33154 ` 667` ```qed auto ``` chaieb@33154 ` 668` wenzelm@56009 ` 669` ```lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q" ``` wenzelm@52658 ` 670` ``` by (induct p q rule: polymul.induct) (auto simp add: field_simps) ``` chaieb@33154 ` 671` wenzelm@52803 ` 672` ```lemma polymul_normh: ``` wenzelm@56000 ` 673` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56009 ` 674` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (p *\<^sub>p q) (min n0 n1)" ``` wenzelm@52803 ` 675` ``` using polymul_properties(1) by blast ``` wenzelm@52658 ` 676` wenzelm@52803 ` 677` ```lemma polymul_eq0_iff: ``` wenzelm@56000 ` 678` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56009 ` 679` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ p *\<^sub>p q = 0\<^sub>p \ p = 0\<^sub>p \ q = 0\<^sub>p" ``` wenzelm@52803 ` 680` ``` using polymul_properties(2) by blast ``` wenzelm@52658 ` 681` wenzelm@52658 ` 682` ```lemma polymul_degreen: (* FIXME duplicate? *) ``` wenzelm@56000 ` 683` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56009 ` 684` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ m \ min n0 n1 \ ``` wenzelm@56009 ` 685` ``` 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 ` 686` ``` using polymul_properties(3) by blast ``` wenzelm@52658 ` 687` wenzelm@52803 ` 688` ```lemma polymul_norm: ``` wenzelm@56000 ` 689` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56009 ` 690` ``` shows "isnpoly p \ isnpoly q \ isnpoly (polymul p q)" ``` chaieb@33154 ` 691` ``` using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp ``` chaieb@33154 ` 692` chaieb@33154 ` 693` ```lemma headconst_zero: "isnpolyh p n0 \ headconst p = 0\<^sub>N \ p = 0\<^sub>p" ``` wenzelm@52658 ` 694` ``` by (induct p arbitrary: n0 rule: headconst.induct) auto ``` chaieb@33154 ` 695` chaieb@33154 ` 696` ```lemma headconst_isnormNum: "isnpolyh p n0 \ isnormNum (headconst p)" ``` wenzelm@52658 ` 697` ``` by (induct p arbitrary: n0) auto ``` chaieb@33154 ` 698` wenzelm@52658 ` 699` ```lemma monic_eqI: ``` wenzelm@52803 ` 700` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 701` ``` shows "INum (headconst p) * Ipoly bs (fst (monic p)) = ``` wenzelm@56000 ` 702` ``` (Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})" ``` chaieb@33154 ` 703` ``` unfolding monic_def Let_def ``` wenzelm@52658 ` 704` ```proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) ``` chaieb@33154 ` 705` ``` let ?h = "headconst p" ``` chaieb@33154 ` 706` ``` assume pz: "p \ 0\<^sub>p" ``` wenzelm@56000 ` 707` ``` { ``` wenzelm@56000 ` 708` ``` assume hz: "INum ?h = (0::'a)" ``` wenzelm@56043 ` 709` ``` from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" ``` wenzelm@56043 ` 710` ``` by simp_all ``` wenzelm@56043 ` 711` ``` from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" ``` wenzelm@56043 ` 712` ``` by simp ``` wenzelm@56043 ` 713` ``` with headconst_zero[OF np] have "p = 0\<^sub>p" ``` wenzelm@56043 ` 714` ``` by blast ``` wenzelm@56043 ` 715` ``` with pz have False ``` wenzelm@56043 ` 716` ``` by blast ``` wenzelm@56043 ` 717` ``` } ``` wenzelm@56043 ` 718` ``` then show "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0" ``` wenzelm@56043 ` 719` ``` by blast ``` chaieb@33154 ` 720` ```qed ``` chaieb@33154 ` 721` chaieb@33154 ` 722` krauss@41404 ` 723` ```text{* polyneg is a negation and preserves normal forms *} ``` chaieb@33154 ` 724` chaieb@33154 ` 725` ```lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p" ``` wenzelm@52658 ` 726` ``` by (induct p rule: polyneg.induct) auto ``` chaieb@33154 ` 727` wenzelm@56009 ` 728` ```lemma polyneg0: "isnpolyh p n \ (~\<^sub>p p) = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 729` ``` by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def) ``` wenzelm@56009 ` 730` chaieb@33154 ` 731` ```lemma polyneg_polyneg: "isnpolyh p n0 \ ~\<^sub>p (~\<^sub>p p) = p" ``` wenzelm@52658 ` 732` ``` by (induct p arbitrary: n0 rule: polyneg.induct) auto ``` wenzelm@56009 ` 733` wenzelm@56009 ` 734` ```lemma polyneg_normh: "isnpolyh p n \ isnpolyh (polyneg p) n" ``` wenzelm@56009 ` 735` ``` by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0) ``` chaieb@33154 ` 736` chaieb@33154 ` 737` ```lemma polyneg_norm: "isnpoly p \ isnpoly (polyneg p)" ``` chaieb@33154 ` 738` ``` using isnpoly_def polyneg_normh by simp ``` chaieb@33154 ` 739` chaieb@33154 ` 740` krauss@41404 ` 741` ```text{* polysub is a substraction and preserves normal forms *} ``` krauss@41404 ` 742` wenzelm@56009 ` 743` ```lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p - Ipoly bs q" ``` wenzelm@52658 ` 744` ``` by (simp add: polysub_def) ``` wenzelm@56009 ` 745` wenzelm@56009 ` 746` ```lemma polysub_normh: "isnpolyh p n0 \ isnpolyh q n1 \ isnpolyh (polysub p q) (min n0 n1)" ``` wenzelm@52658 ` 747` ``` by (simp add: polysub_def polyneg_normh polyadd_normh) ``` chaieb@33154 ` 748` wenzelm@56009 ` 749` ```lemma polysub_norm: "isnpoly p \ isnpoly q \ isnpoly (polysub p q)" ``` wenzelm@52803 ` 750` ``` using polyadd_norm polyneg_norm by (simp add: polysub_def) ``` wenzelm@56009 ` 751` wenzelm@52658 ` 752` ```lemma polysub_same_0[simp]: ``` wenzelm@56000 ` 753` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` krauss@41814 ` 754` ``` shows "isnpolyh p n0 \ polysub p p = 0\<^sub>p" ``` wenzelm@52658 ` 755` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@52658 ` 756` ``` by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def]) ``` chaieb@33154 ` 757` wenzelm@52803 ` 758` ```lemma polysub_0: ``` wenzelm@56000 ` 759` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56009 ` 760` ``` shows "isnpolyh p n0 \ isnpolyh q n1 \ p -\<^sub>p q = 0\<^sub>p \ p = q" ``` chaieb@33154 ` 761` ``` unfolding polysub_def split_def fst_conv snd_conv ``` krauss@41763 ` 762` ``` by (induct p q arbitrary: n0 n1 rule:polyadd.induct) ``` wenzelm@52658 ` 763` ``` (auto simp: Nsub0[simplified Nsub_def] Let_def) ``` chaieb@33154 ` 764` chaieb@33154 ` 765` ```text{* polypow is a power function and preserves normal forms *} ``` krauss@41404 ` 766` wenzelm@56009 ` 767` ```lemma polypow[simp]: ``` wenzelm@56009 ` 768` ``` "Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n" ``` wenzelm@52658 ` 769` ```proof (induct n rule: polypow.induct) ``` wenzelm@52658 ` 770` ``` case 1 ``` wenzelm@56043 ` 771` ``` then show ?case ``` wenzelm@56043 ` 772` ``` by simp ``` chaieb@33154 ` 773` ```next ``` chaieb@33154 ` 774` ``` case (2 n) ``` chaieb@33154 ` 775` ``` let ?q = "polypow ((Suc n) div 2) p" ``` krauss@41813 ` 776` ``` let ?d = "polymul ?q ?q" ``` wenzelm@56043 ` 777` ``` have "odd (Suc n) \ even (Suc n)" ``` wenzelm@56043 ` 778` ``` by simp ``` wenzelm@52803 ` 779` ``` moreover ``` wenzelm@56043 ` 780` ``` { ``` wenzelm@56043 ` 781` ``` assume odd: "odd (Suc n)" ``` wenzelm@56000 ` 782` ``` have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" ``` wenzelm@52658 ` 783` ``` by arith ``` wenzelm@56043 ` 784` ``` from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" ``` wenzelm@56043 ` 785` ``` by (simp add: Let_def) ``` wenzelm@56043 ` 786` ``` also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2) * (Ipoly bs p)^(Suc n div 2)" ``` chaieb@33154 ` 787` ``` using "2.hyps" by simp ``` chaieb@33154 ` 788` ``` also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" ``` wenzelm@52658 ` 789` ``` by (simp only: power_add power_one_right) simp ``` wenzelm@56000 ` 790` ``` also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" ``` chaieb@33154 ` 791` ``` by (simp only: th) ``` wenzelm@52803 ` 792` ``` finally have ?case ``` wenzelm@56043 ` 793` ``` using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp ``` wenzelm@56043 ` 794` ``` } ``` wenzelm@52803 ` 795` ``` moreover ``` wenzelm@56043 ` 796` ``` { ``` wenzelm@56043 ` 797` ``` assume even: "even (Suc n)" ``` wenzelm@56000 ` 798` ``` have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2" ``` wenzelm@52658 ` 799` ``` by arith ``` wenzelm@56043 ` 800` ``` from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" ``` wenzelm@56043 ` 801` ``` by (simp add: Let_def) ``` chaieb@33154 ` 802` ``` also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)" ``` wenzelm@56043 ` 803` ``` using "2.hyps" by (simp only: power_add) simp ``` wenzelm@56043 ` 804` ``` finally have ?case using even_nat_div_two_times_two[OF even] ``` wenzelm@56043 ` 805` ``` by (simp only: th) ``` wenzelm@56043 ` 806` ``` } ``` chaieb@33154 ` 807` ``` ultimately show ?case by blast ``` chaieb@33154 ` 808` ```qed ``` chaieb@33154 ` 809` wenzelm@52803 ` 810` ```lemma polypow_normh: ``` wenzelm@56000 ` 811` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 812` ``` shows "isnpolyh p n \ isnpolyh (polypow k p) n" ``` chaieb@33154 ` 813` ```proof (induct k arbitrary: n rule: polypow.induct) ``` wenzelm@56043 ` 814` ``` case 1 ``` wenzelm@56043 ` 815` ``` then show ?case by auto ``` wenzelm@56043 ` 816` ```next ``` chaieb@33154 ` 817` ``` case (2 k n) ``` chaieb@33154 ` 818` ``` let ?q = "polypow (Suc k div 2) p" ``` krauss@41813 ` 819` ``` let ?d = "polymul ?q ?q" ``` wenzelm@56043 ` 820` ``` from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n" ``` wenzelm@56043 ` 821` ``` by blast+ ``` wenzelm@56043 ` 822` ``` from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" ``` wenzelm@56043 ` 823` ``` by simp ``` wenzelm@56043 ` 824` ``` from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" ``` wenzelm@56043 ` 825` ``` by simp ``` wenzelm@56043 ` 826` ``` from dn on show ?case ``` wenzelm@56043 ` 827` ``` by (simp add: Let_def) ``` wenzelm@56043 ` 828` ```qed ``` chaieb@33154 ` 829` wenzelm@52803 ` 830` ```lemma polypow_norm: ``` wenzelm@56000 ` 831` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 832` ``` shows "isnpoly p \ isnpoly (polypow k p)" ``` chaieb@33154 ` 833` ``` by (simp add: polypow_normh isnpoly_def) ``` chaieb@33154 ` 834` krauss@41404 ` 835` ```text{* Finally the whole normalization *} ``` chaieb@33154 ` 836` wenzelm@52658 ` 837` ```lemma polynate [simp]: ``` wenzelm@56000 ` 838` ``` "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 839` ``` by (induct p rule:polynate.induct) auto ``` chaieb@33154 ` 840` wenzelm@52803 ` 841` ```lemma polynate_norm[simp]: ``` wenzelm@56000 ` 842` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 843` ``` shows "isnpoly (polynate p)" ``` wenzelm@52658 ` 844` ``` by (induct p rule: polynate.induct) ``` wenzelm@52658 ` 845` ``` (simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, ``` wenzelm@52658 ` 846` ``` simp_all add: isnpoly_def) ``` chaieb@33154 ` 847` chaieb@33154 ` 848` ```text{* shift1 *} ``` chaieb@33154 ` 849` chaieb@33154 ` 850` chaieb@33154 ` 851` ```lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" ``` wenzelm@52658 ` 852` ``` by (simp add: shift1_def) ``` chaieb@33154 ` 853` wenzelm@52803 ` 854` ```lemma shift1_isnpoly: ``` wenzelm@52658 ` 855` ``` assumes pn: "isnpoly p" ``` wenzelm@52658 ` 856` ``` and pnz: "p \ 0\<^sub>p" ``` wenzelm@52658 ` 857` ``` shows "isnpoly (shift1 p) " ``` wenzelm@52658 ` 858` ``` using pn pnz by (simp add: shift1_def isnpoly_def) ``` chaieb@33154 ` 859` chaieb@33154 ` 860` ```lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p" ``` chaieb@33154 ` 861` ``` by (simp add: shift1_def) ``` wenzelm@56043 ` 862` wenzelm@56043 ` 863` ```lemma funpow_shift1_isnpoly: "isnpoly p \ p \ 0\<^sub>p \ isnpoly (funpow n shift1 p)" ``` haftmann@39246 ` 864` ``` by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) ``` chaieb@33154 ` 865` wenzelm@52803 ` 866` ```lemma funpow_isnpolyh: ``` wenzelm@56043 ` 867` ``` assumes f: "\p. isnpolyh p n \ isnpolyh (f p) n" ``` wenzelm@52658 ` 868` ``` and np: "isnpolyh p n" ``` chaieb@33154 ` 869` ``` shows "isnpolyh (funpow k f p) n" ``` wenzelm@52658 ` 870` ``` using f np by (induct k arbitrary: p) auto ``` chaieb@33154 ` 871` wenzelm@52658 ` 872` ```lemma funpow_shift1: ``` wenzelm@56000 ` 873` ``` "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) = ``` wenzelm@52658 ` 874` ``` Ipoly bs (Mul (Pw (Bound 0) n) p)" ``` wenzelm@52658 ` 875` ``` by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) ``` chaieb@33154 ` 876` wenzelm@56043 ` 877` ```lemma shift1_isnpolyh: "isnpolyh p n0 \ p \ 0\<^sub>p \ isnpolyh (shift1 p) 0" ``` chaieb@33154 ` 878` ``` using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) ``` chaieb@33154 ` 879` wenzelm@52803 ` 880` ```lemma funpow_shift1_1: ``` wenzelm@56000 ` 881` ``` "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) = ``` wenzelm@52658 ` 882` ``` Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" ``` chaieb@33154 ` 883` ``` by (simp add: funpow_shift1) ``` chaieb@33154 ` 884` chaieb@33154 ` 885` ```lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)" ``` wenzelm@45129 ` 886` ``` by (induct p rule: poly_cmul.induct) (auto simp add: field_simps) ``` chaieb@33154 ` 887` chaieb@33154 ` 888` ```lemma behead: ``` chaieb@33154 ` 889` ``` assumes np: "isnpolyh p n" ``` wenzelm@52658 ` 890` ``` shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = ``` wenzelm@56000 ` 891` ``` (Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 892` ``` using np ``` chaieb@33154 ` 893` ```proof (induct p arbitrary: n rule: behead.induct) ``` wenzelm@56009 ` 894` ``` case (1 c p n) ``` wenzelm@56009 ` 895` ``` then have pn: "isnpolyh p n" by simp ``` wenzelm@52803 ` 896` ``` from 1(1)[OF pn] ``` wenzelm@52803 ` 897` ``` have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . ``` wenzelm@52658 ` 898` ``` then show ?case using "1.hyps" ``` wenzelm@52658 ` 899` ``` apply (simp add: Let_def,cases "behead p = 0\<^sub>p") ``` wenzelm@52658 ` 900` ``` apply (simp_all add: th[symmetric] field_simps) ``` wenzelm@52658 ` 901` ``` done ``` chaieb@33154 ` 902` ```qed (auto simp add: Let_def) ``` chaieb@33154 ` 903` chaieb@33154 ` 904` ```lemma behead_isnpolyh: ``` wenzelm@52658 ` 905` ``` assumes np: "isnpolyh p n" ``` wenzelm@52658 ` 906` ``` shows "isnpolyh (behead p) n" ``` wenzelm@52658 ` 907` ``` using np by (induct p rule: behead.induct) (auto simp add: Let_def isnpolyh_mono) ``` wenzelm@52658 ` 908` chaieb@33154 ` 909` krauss@41404 ` 910` ```subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *} ``` wenzelm@52658 ` 911` chaieb@33154 ` 912` ```lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ polybound0 p" ``` wenzelm@52658 ` 913` ```proof (induct p arbitrary: n rule: poly.induct, auto) ``` chaieb@33154 ` 914` ``` case (goal1 c n p n') ``` wenzelm@56009 ` 915` ``` then have "n = Suc (n - 1)" ``` wenzelm@56009 ` 916` ``` by simp ``` wenzelm@56009 ` 917` ``` then have "isnpolyh p (Suc (n - 1))" ``` wenzelm@56009 ` 918` ``` using `isnpolyh p n` by simp ``` wenzelm@56009 ` 919` ``` with goal1(2) show ?case ``` wenzelm@56009 ` 920` ``` by simp ``` chaieb@33154 ` 921` ```qed ``` chaieb@33154 ` 922` chaieb@33154 ` 923` ```lemma isconstant_polybound0: "isnpolyh p n0 \ isconstant p \ polybound0 p" ``` wenzelm@52658 ` 924` ``` by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0) ``` chaieb@33154 ` 925` wenzelm@52658 ` 926` ```lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 927` ``` by (induct p) auto ``` chaieb@33154 ` 928` chaieb@33154 ` 929` ```lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)" ``` wenzelm@52658 ` 930` ``` apply (induct p arbitrary: n0) ``` wenzelm@52658 ` 931` ``` apply auto ``` wenzelm@56043 ` 932` ``` apply atomize ``` chaieb@33154 ` 933` ``` apply (erule_tac x = "Suc nat" in allE) ``` chaieb@33154 ` 934` ``` apply auto ``` chaieb@33154 ` 935` ``` done ``` chaieb@33154 ` 936` chaieb@33154 ` 937` ```lemma head_polybound0: "isnpolyh p n0 \ polybound0 (head p)" ``` wenzelm@52658 ` 938` ``` by (induct p arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0) ``` chaieb@33154 ` 939` chaieb@33154 ` 940` ```lemma polybound0_I: ``` chaieb@33154 ` 941` ``` assumes nb: "polybound0 a" ``` wenzelm@56009 ` 942` ``` shows "Ipoly (b # bs) a = Ipoly (b' # bs) a" ``` wenzelm@52658 ` 943` ``` using nb ``` wenzelm@52803 ` 944` ``` by (induct a rule: poly.induct) auto ``` wenzelm@52658 ` 945` wenzelm@56009 ` 946` ```lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t" ``` chaieb@33154 ` 947` ``` by (induct t) simp_all ``` chaieb@33154 ` 948` chaieb@33154 ` 949` ```lemma polysubst0_I': ``` chaieb@33154 ` 950` ``` assumes nb: "polybound0 a" ``` wenzelm@56009 ` 951` ``` shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t" ``` chaieb@33154 ` 952` ``` by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"]) ``` chaieb@33154 ` 953` wenzelm@52658 ` 954` ```lemma decrpoly: ``` wenzelm@52658 ` 955` ``` assumes nb: "polybound0 t" ``` wenzelm@56043 ` 956` ``` shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)" ``` wenzelm@52658 ` 957` ``` using nb by (induct t rule: decrpoly.induct) simp_all ``` chaieb@33154 ` 958` wenzelm@52658 ` 959` ```lemma polysubst0_polybound0: ``` wenzelm@52658 ` 960` ``` assumes nb: "polybound0 t" ``` chaieb@33154 ` 961` ``` shows "polybound0 (polysubst0 t a)" ``` wenzelm@52658 ` 962` ``` using nb by (induct a rule: poly.induct) auto ``` chaieb@33154 ` 963` chaieb@33154 ` 964` ```lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p" ``` wenzelm@52658 ` 965` ``` by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) ``` chaieb@33154 ` 966` wenzelm@56043 ` 967` ```primrec maxindex :: "poly \ nat" ``` wenzelm@56043 ` 968` ```where ``` chaieb@33154 ` 969` ``` "maxindex (Bound n) = n + 1" ``` chaieb@33154 ` 970` ```| "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" ``` chaieb@33154 ` 971` ```| "maxindex (Add p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 972` ```| "maxindex (Sub p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 973` ```| "maxindex (Mul p q) = max (maxindex p) (maxindex q)" ``` chaieb@33154 ` 974` ```| "maxindex (Neg p) = maxindex p" ``` chaieb@33154 ` 975` ```| "maxindex (Pw p n) = maxindex p" ``` chaieb@33154 ` 976` ```| "maxindex (C x) = 0" ``` chaieb@33154 ` 977` wenzelm@52658 ` 978` ```definition wf_bs :: "'a list \ poly \ bool" ``` wenzelm@56000 ` 979` ``` where "wf_bs bs p \ length bs \ maxindex p" ``` chaieb@33154 ` 980` wenzelm@56043 ` 981` ```lemma wf_bs_coefficients: "wf_bs bs p \ \c \ set (coefficients p). wf_bs bs c" ``` wenzelm@52658 ` 982` ```proof (induct p rule: coefficients.induct) ``` wenzelm@52803 ` 983` ``` case (1 c p) ``` wenzelm@52803 ` 984` ``` show ?case ``` chaieb@33154 ` 985` ``` proof ``` wenzelm@56009 ` 986` ``` fix x ``` wenzelm@56009 ` 987` ``` assume xc: "x \ set (coefficients (CN c 0 p))" ``` wenzelm@56009 ` 988` ``` then have "x = c \ x \ set (coefficients p)" ``` wenzelm@56009 ` 989` ``` by simp ``` wenzelm@52803 ` 990` ``` moreover ``` wenzelm@56009 ` 991` ``` { ``` wenzelm@56009 ` 992` ``` assume "x = c" ``` wenzelm@56009 ` 993` ``` then have "wf_bs bs x" ``` wenzelm@56043 ` 994` ``` using "1.prems" unfolding wf_bs_def by simp ``` wenzelm@56009 ` 995` ``` } ``` wenzelm@56009 ` 996` ``` moreover ``` wenzelm@56009 ` 997` ``` { ``` wenzelm@56009 ` 998` ``` assume H: "x \ set (coefficients p)" ``` wenzelm@56009 ` 999` ``` from "1.prems" have "wf_bs bs p" ``` wenzelm@56009 ` 1000` ``` unfolding wf_bs_def by simp ``` wenzelm@56009 ` 1001` ``` with "1.hyps" H have "wf_bs bs x" ``` wenzelm@56009 ` 1002` ``` by blast ``` wenzelm@56009 ` 1003` ``` } ``` wenzelm@56066 ` 1004` ``` ultimately show "wf_bs bs x" ``` wenzelm@56009 ` 1005` ``` by blast ``` chaieb@33154 ` 1006` ``` qed ``` chaieb@33154 ` 1007` ```qed simp_all ``` chaieb@33154 ` 1008` wenzelm@56043 ` 1009` ```lemma maxindex_coefficients: "\c \ set (coefficients p). maxindex c \ maxindex p" ``` wenzelm@52658 ` 1010` ``` by (induct p rule: coefficients.induct) auto ``` chaieb@33154 ` 1011` wenzelm@56000 ` 1012` ```lemma wf_bs_I: "wf_bs bs p \ Ipoly (bs @ bs') p = Ipoly bs p" ``` wenzelm@52658 ` 1013` ``` unfolding wf_bs_def by (induct p) (auto simp add: nth_append) ``` chaieb@33154 ` 1014` wenzelm@52658 ` 1015` ```lemma take_maxindex_wf: ``` wenzelm@52803 ` 1016` ``` assumes wf: "wf_bs bs p" ``` chaieb@33154 ` 1017` ``` shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" ``` wenzelm@56009 ` 1018` ```proof - ``` chaieb@33154 ` 1019` ``` let ?ip = "maxindex p" ``` chaieb@33154 ` 1020` ``` let ?tbs = "take ?ip bs" ``` wenzelm@56009 ` 1021` ``` from wf have "length ?tbs = ?ip" ``` wenzelm@56009 ` 1022` ``` unfolding wf_bs_def by simp ``` wenzelm@56009 ` 1023` ``` then have wf': "wf_bs ?tbs p" ``` wenzelm@56009 ` 1024` ``` unfolding wf_bs_def by simp ``` wenzelm@56043 ` 1025` ``` have eq: "bs = ?tbs @ drop ?ip bs" ``` wenzelm@56009 ` 1026` ``` by simp ``` wenzelm@56009 ` 1027` ``` from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis ``` wenzelm@56009 ` 1028` ``` using eq by simp ``` chaieb@33154 ` 1029` ```qed ``` chaieb@33154 ` 1030` chaieb@33154 ` 1031` ```lemma decr_maxindex: "polybound0 p \ maxindex (decrpoly p) = maxindex p - 1" ``` wenzelm@52658 ` 1032` ``` by (induct p) auto ``` chaieb@33154 ` 1033` chaieb@33154 ` 1034` ```lemma wf_bs_insensitive: "length bs = length bs' \ wf_bs bs p = wf_bs bs' p" ``` chaieb@33154 ` 1035` ``` unfolding wf_bs_def by simp ``` chaieb@33154 ` 1036` chaieb@33154 ` 1037` ```lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p" ``` chaieb@33154 ` 1038` ``` unfolding wf_bs_def by simp ``` chaieb@33154 ` 1039` chaieb@33154 ` 1040` ```lemma wf_bs_coefficients': "\c \ set (coefficients p). wf_bs bs c \ wf_bs (x#bs) p" ``` wenzelm@52658 ` 1041` ``` by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) ``` wenzelm@56043 ` 1042` chaieb@33154 ` 1043` ```lemma coefficients_Nil[simp]: "coefficients p \ []" ``` wenzelm@52658 ` 1044` ``` by (induct p rule: coefficients.induct) simp_all ``` chaieb@33154 ` 1045` chaieb@33154 ` 1046` ```lemma coefficients_head: "last (coefficients p) = head p" ``` wenzelm@52658 ` 1047` ``` by (induct p rule: coefficients.induct) auto ``` chaieb@33154 ` 1048` chaieb@33154 ` 1049` ```lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \ wf_bs (x#bs) p" ``` wenzelm@52658 ` 1050` ``` unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto ``` chaieb@33154 ` 1051` wenzelm@56043 ` 1052` ```lemma length_le_list_ex: "length xs \ n \ \ys. length (xs @ ys) = n" ``` chaieb@33154 ` 1053` ``` apply (rule exI[where x="replicate (n - length xs) z"]) ``` wenzelm@52658 ` 1054` ``` apply simp ``` wenzelm@52658 ` 1055` ``` done ``` wenzelm@52658 ` 1056` wenzelm@56043 ` 1057` ```lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \ isconstant p" ``` wenzelm@52658 ` 1058` ``` apply (cases p) ``` wenzelm@52658 ` 1059` ``` apply auto ``` wenzelm@52658 ` 1060` ``` apply (case_tac "nat") ``` wenzelm@52658 ` 1061` ``` apply simp_all ``` wenzelm@52658 ` 1062` ``` done ``` chaieb@33154 ` 1063` chaieb@33154 ` 1064` ```lemma wf_bs_polyadd: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p +\<^sub>p q)" ``` wenzelm@56066 ` 1065` ``` unfolding wf_bs_def by (induct p q rule: polyadd.induct) (auto simp add: Let_def) ``` chaieb@33154 ` 1066` chaieb@33154 ` 1067` ```lemma wf_bs_polyul: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p *\<^sub>p q)" ``` wenzelm@52803 ` 1068` ``` unfolding wf_bs_def ``` wenzelm@52803 ` 1069` ``` apply (induct p q arbitrary: bs rule: polymul.induct) ``` chaieb@33154 ` 1070` ``` apply (simp_all add: wf_bs_polyadd) ``` chaieb@33154 ` 1071` ``` apply clarsimp ``` chaieb@33154 ` 1072` ``` apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format]) ``` chaieb@33154 ` 1073` ``` apply auto ``` chaieb@33154 ` 1074` ``` done ``` chaieb@33154 ` 1075` chaieb@33154 ` 1076` ```lemma wf_bs_polyneg: "wf_bs bs p \ wf_bs bs (~\<^sub>p p)" ``` wenzelm@52658 ` 1077` ``` unfolding wf_bs_def by (induct p rule: polyneg.induct) auto ``` chaieb@33154 ` 1078` chaieb@33154 ` 1079` ```lemma wf_bs_polysub: "wf_bs bs p \ wf_bs bs q \ wf_bs bs (p -\<^sub>p q)" ``` wenzelm@56043 ` 1080` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@56043 ` 1081` ``` using wf_bs_polyadd wf_bs_polyneg by blast ``` chaieb@33154 ` 1082` wenzelm@52658 ` 1083` wenzelm@56043 ` 1084` ```subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *} ``` chaieb@33154 ` 1085` chaieb@33154 ` 1086` ```definition "polypoly bs p = map (Ipoly bs) (coefficients p)" ``` wenzelm@56043 ` 1087` ```definition "polypoly' bs p = map (Ipoly bs \ decrpoly) (coefficients p)" ``` wenzelm@56043 ` 1088` ```definition "poly_nate bs p = map (Ipoly bs \ decrpoly) (coefficients (polynate p))" ``` chaieb@33154 ` 1089` wenzelm@56043 ` 1090` ```lemma coefficients_normh: "isnpolyh p n0 \ \q \ set (coefficients p). isnpolyh q n0" ``` chaieb@33154 ` 1091` ```proof (induct p arbitrary: n0 rule: coefficients.induct) ``` chaieb@33154 ` 1092` ``` case (1 c p n0) ``` wenzelm@56009 ` 1093` ``` have cp: "isnpolyh (CN c 0 p) n0" ``` wenzelm@56009 ` 1094` ``` by fact ``` wenzelm@56009 ` 1095` ``` then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \ 0\<^sub>p" "n0 = 0" ``` chaieb@33154 ` 1096` ``` by (auto simp add: isnpolyh_mono[where n'=0]) ``` wenzelm@56009 ` 1097` ``` from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case ``` wenzelm@56009 ` 1098` ``` by simp ``` chaieb@33154 ` 1099` ```qed auto ``` chaieb@33154 ` 1100` wenzelm@56043 ` 1101` ```lemma coefficients_isconst: "isnpolyh p n \ \q \ set (coefficients p). isconstant q" ``` wenzelm@56043 ` 1102` ``` by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const) ``` chaieb@33154 ` 1103` chaieb@33154 ` 1104` ```lemma polypoly_polypoly': ``` chaieb@33154 ` 1105` ``` assumes np: "isnpolyh p n0" ``` wenzelm@56043 ` 1106` ``` shows "polypoly (x # bs) p = polypoly' bs p" ``` wenzelm@56043 ` 1107` ```proof - ``` chaieb@33154 ` 1108` ``` let ?cf = "set (coefficients p)" ``` chaieb@33154 ` 1109` ``` from coefficients_normh[OF np] have cn_norm: "\ q\ ?cf. isnpolyh q n0" . ``` wenzelm@56043 ` 1110` ``` { ``` wenzelm@56043 ` 1111` ``` fix q ``` wenzelm@56043 ` 1112` ``` assume q: "q \ ?cf" ``` wenzelm@56043 ` 1113` ``` from q cn_norm have th: "isnpolyh q n0" ``` wenzelm@56043 ` 1114` ``` by blast ``` wenzelm@56043 ` 1115` ``` from coefficients_isconst[OF np] q have "isconstant q" ``` wenzelm@56043 ` 1116` ``` by blast ``` wenzelm@56043 ` 1117` ``` with isconstant_polybound0[OF th] have "polybound0 q" ``` wenzelm@56043 ` 1118` ``` by blast ``` wenzelm@56043 ` 1119` ``` } ``` wenzelm@56009 ` 1120` ``` then have "\q \ ?cf. polybound0 q" .. ``` wenzelm@56043 ` 1121` ``` then have "\q \ ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)" ``` chaieb@33154 ` 1122` ``` using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] ``` chaieb@33154 ` 1123` ``` by auto ``` wenzelm@56043 ` 1124` ``` then show ?thesis ``` wenzelm@56043 ` 1125` ``` unfolding polypoly_def polypoly'_def by simp ``` chaieb@33154 ` 1126` ```qed ``` chaieb@33154 ` 1127` chaieb@33154 ` 1128` ```lemma polypoly_poly: ``` wenzelm@56043 ` 1129` ``` assumes "isnpolyh p n0" ``` wenzelm@56043 ` 1130` ``` shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x" ``` wenzelm@56043 ` 1131` ``` using assms ``` wenzelm@52658 ` 1132` ``` by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) ``` chaieb@33154 ` 1133` wenzelm@52803 ` 1134` ```lemma polypoly'_poly: ``` wenzelm@56043 ` 1135` ``` assumes "isnpolyh p n0" ``` wenzelm@52658 ` 1136` ``` shows "\p\\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" ``` wenzelm@56043 ` 1137` ``` using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] . ``` chaieb@33154 ` 1138` chaieb@33154 ` 1139` chaieb@33154 ` 1140` ```lemma polypoly_poly_polybound0: ``` wenzelm@56043 ` 1141` ``` assumes "isnpolyh p n0" ``` wenzelm@56043 ` 1142` ``` and "polybound0 p" ``` chaieb@33154 ` 1143` ``` shows "polypoly bs p = [Ipoly bs p]" ``` wenzelm@56043 ` 1144` ``` using assms ``` wenzelm@56043 ` 1145` ``` unfolding polypoly_def ``` wenzelm@52658 ` 1146` ``` apply (cases p) ``` wenzelm@52658 ` 1147` ``` apply auto ``` wenzelm@52658 ` 1148` ``` apply (case_tac nat) ``` wenzelm@52658 ` 1149` ``` apply auto ``` wenzelm@52658 ` 1150` ``` done ``` chaieb@33154 ` 1151` wenzelm@52803 ` 1152` ```lemma head_isnpolyh: "isnpolyh p n0 \ isnpolyh (head p) n0" ``` wenzelm@52658 ` 1153` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1154` wenzelm@56043 ` 1155` ```lemma headn_nz[simp]: "isnpolyh p n0 \ headn p m = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 1156` ``` by (cases p) auto ``` chaieb@33154 ` 1157` chaieb@33154 ` 1158` ```lemma head_eq_headn0: "head p = headn p 0" ``` wenzelm@52658 ` 1159` ``` by (induct p rule: head.induct) simp_all ``` chaieb@33154 ` 1160` wenzelm@56043 ` 1161` ```lemma head_nz[simp]: "isnpolyh p n0 \ head p = 0\<^sub>p \ p = 0\<^sub>p" ``` chaieb@33154 ` 1162` ``` by (simp add: head_eq_headn0) ``` chaieb@33154 ` 1163` wenzelm@52803 ` 1164` ```lemma isnpolyh_zero_iff: ``` wenzelm@52658 ` 1165` ``` assumes nq: "isnpolyh p n0" ``` wenzelm@56000 ` 1166` ``` and eq :"\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0,field_inverse_zero, power})" ``` chaieb@33154 ` 1167` ``` shows "p = 0\<^sub>p" ``` wenzelm@52658 ` 1168` ``` using nq eq ``` berghofe@34915 ` 1169` ```proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) ``` berghofe@34915 ` 1170` ``` case less ``` berghofe@34915 ` 1171` ``` note np = `isnpolyh p n0` and zp = `\bs. wf_bs bs p \ \p\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` ``` wenzelm@56000 ` 1172` ``` { ``` wenzelm@56000 ` 1173` ``` assume nz: "maxindex p = 0" ``` wenzelm@56000 ` 1174` ``` then obtain c where "p = C c" ``` wenzelm@56000 ` 1175` ``` using np by (cases p) auto ``` wenzelm@56000 ` 1176` ``` with zp np have "p = 0\<^sub>p" ``` wenzelm@56000 ` 1177` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1178` ``` } ``` chaieb@33154 ` 1179` ``` moreover ``` wenzelm@56000 ` 1180` ``` { ``` wenzelm@56000 ` 1181` ``` assume nz: "maxindex p \ 0" ``` chaieb@33154 ` 1182` ``` let ?h = "head p" ``` chaieb@33154 ` 1183` ``` let ?hd = "decrpoly ?h" ``` chaieb@33154 ` 1184` ``` let ?ihd = "maxindex ?hd" ``` wenzelm@56000 ` 1185` ``` from head_isnpolyh[OF np] head_polybound0[OF np] ``` wenzelm@56000 ` 1186` ``` have h: "isnpolyh ?h n0" "polybound0 ?h" ``` chaieb@33154 ` 1187` ``` by simp_all ``` wenzelm@56000 ` 1188` ``` then have nhd: "isnpolyh ?hd (n0 - 1)" ``` wenzelm@56000 ` 1189` ``` using decrpoly_normh by blast ``` wenzelm@52803 ` 1190` chaieb@33154 ` 1191` ``` from maxindex_coefficients[of p] coefficients_head[of p, symmetric] ``` wenzelm@56000 ` 1192` ``` have mihn: "maxindex ?h \ maxindex p" ``` wenzelm@56000 ` 1193` ``` by auto ``` wenzelm@56000 ` 1194` ``` with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" ``` wenzelm@56000 ` 1195` ``` by auto ``` wenzelm@56000 ` 1196` ``` { ``` wenzelm@56000 ` 1197` ``` fix bs :: "'a list" ``` wenzelm@56000 ` 1198` ``` assume bs: "wf_bs bs ?hd" ``` chaieb@33154 ` 1199` ``` let ?ts = "take ?ihd bs" ``` chaieb@33154 ` 1200` ``` let ?rs = "drop ?ihd bs" ``` wenzelm@56000 ` 1201` ``` have ts: "wf_bs ?ts ?hd" ``` wenzelm@56000 ` 1202` ``` using bs unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1203` ``` have bs_ts_eq: "?ts @ ?rs = bs" ``` wenzelm@56000 ` 1204` ``` by simp ``` wenzelm@56000 ` 1205` ``` from wf_bs_decrpoly[OF ts] have tsh: " \x. wf_bs (x # ?ts) ?h" ``` wenzelm@56000 ` 1206` ``` by simp ``` wenzelm@56000 ` 1207` ``` from ihd_lt_n have "\x. length (x # ?ts) \ maxindex p" ``` wenzelm@56000 ` 1208` ``` by simp ``` wenzelm@56000 ` 1209` ``` with length_le_list_ex obtain xs where xs: "length ((x # ?ts) @ xs) = maxindex p" ``` wenzelm@56000 ` 1210` ``` by blast ``` wenzelm@56000 ` 1211` ``` then have "\x. wf_bs ((x # ?ts) @ xs) p" ``` wenzelm@56000 ` 1212` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1213` ``` with zp have "\x. Ipoly ((x # ?ts) @ xs) p = 0" ``` wenzelm@56000 ` 1214` ``` by blast ``` wenzelm@56000 ` 1215` ``` then have "\x. Ipoly (x # (?ts @ xs)) p = 0" ``` wenzelm@56000 ` 1216` ``` by simp ``` chaieb@33154 ` 1217` ``` with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a] ``` wenzelm@56000 ` 1218` ``` have "\x. poly (polypoly' (?ts @ xs) p) x = poly [] x" ``` wenzelm@56000 ` 1219` ``` by simp ``` wenzelm@56000 ` 1220` ``` then have "poly (polypoly' (?ts @ xs) p) = poly []" ``` wenzelm@56000 ` 1221` ``` by auto ``` wenzelm@56000 ` 1222` ``` then have "\c \ set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0" ``` wenzelm@33268 ` 1223` ``` using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) ``` chaieb@33154 ` 1224` ``` with coefficients_head[of p, symmetric] ``` wenzelm@56000 ` 1225` ``` have th0: "Ipoly (?ts @ xs) ?hd = 0" ``` wenzelm@56000 ` 1226` ``` by simp ``` wenzelm@56000 ` 1227` ``` from bs have wf'': "wf_bs ?ts ?hd" ``` wenzelm@56000 ` 1228` ``` unfolding wf_bs_def by simp ``` wenzelm@56000 ` 1229` ``` with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" ``` wenzelm@56000 ` 1230` ``` by simp ``` wenzelm@56000 ` 1231` ``` with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\?hd\\<^sub>p\<^bsup>bs\<^esup> = 0" ``` wenzelm@56000 ` 1232` ``` by simp ``` wenzelm@56000 ` 1233` ``` } ``` wenzelm@56000 ` 1234` ``` then have hdz: "\bs. wf_bs bs ?hd \ \?hd\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" ``` wenzelm@56000 ` 1235` ``` by blast ``` wenzelm@56000 ` 1236` ``` from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" ``` wenzelm@56000 ` 1237` ``` by blast ``` wenzelm@56000 ` 1238` ``` then have "?h = 0\<^sub>p" by simp ``` wenzelm@56000 ` 1239` ``` with head_nz[OF np] have "p = 0\<^sub>p" by simp ``` wenzelm@56000 ` 1240` ``` } ``` wenzelm@56000 ` 1241` ``` ultimately show "p = 0\<^sub>p" ``` wenzelm@56000 ` 1242` ``` by blast ``` chaieb@33154 ` 1243` ```qed ``` chaieb@33154 ` 1244` wenzelm@52803 ` 1245` ```lemma isnpolyh_unique: ``` wenzelm@56000 ` 1246` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1247` ``` and nq: "isnpolyh q n1" ``` wenzelm@56000 ` 1248` ``` 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 ` 1249` ```proof auto ``` wenzelm@56000 ` 1250` ``` assume H: "\bs. (\p\\<^sub>p\<^bsup>bs\<^esup> ::'a) = \q\\<^sub>p\<^bsup>bs\<^esup>" ``` wenzelm@56000 ` 1251` ``` then have "\bs.\p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" ``` wenzelm@56000 ` 1252` ``` by simp ``` wenzelm@56000 ` 1253` ``` then have "\bs. wf_bs bs (p -\<^sub>p q) \ \p -\<^sub>p q\\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" ``` chaieb@33154 ` 1254` ``` using wf_bs_polysub[where p=p and q=q] by auto ``` wenzelm@56000 ` 1255` ``` with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq] show "p = q" ``` wenzelm@56000 ` 1256` ``` by blast ``` chaieb@33154 ` 1257` ```qed ``` chaieb@33154 ` 1258` chaieb@33154 ` 1259` krauss@41404 ` 1260` ```text{* consequences of unicity on the algorithms for polynomial normalization *} ``` chaieb@33154 ` 1261` wenzelm@52658 ` 1262` ```lemma polyadd_commute: ``` wenzelm@56000 ` 1263` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1264` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1265` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 1266` ``` shows "p +\<^sub>p q = q +\<^sub>p p" ``` wenzelm@56000 ` 1267` ``` using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] ``` wenzelm@56000 ` 1268` ``` by simp ``` chaieb@33154 ` 1269` wenzelm@56000 ` 1270` ```lemma zero_normh: "isnpolyh 0\<^sub>p n" ``` wenzelm@56000 ` 1271` ``` by simp ``` wenzelm@56000 ` 1272` wenzelm@56000 ` 1273` ```lemma one_normh: "isnpolyh (1)\<^sub>p n" ``` wenzelm@56000 ` 1274` ``` by simp ``` wenzelm@52658 ` 1275` wenzelm@52803 ` 1276` ```lemma polyadd_0[simp]: ``` wenzelm@56000 ` 1277` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1278` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1279` ``` shows "p +\<^sub>p 0\<^sub>p = p" ``` wenzelm@56000 ` 1280` ``` and "0\<^sub>p +\<^sub>p p = p" ``` wenzelm@52803 ` 1281` ``` using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] ``` chaieb@33154 ` 1282` ``` isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all ``` chaieb@33154 ` 1283` wenzelm@52803 ` 1284` ```lemma polymul_1[simp]: ``` wenzelm@56000 ` 1285` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1286` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1287` ``` shows "p *\<^sub>p (1)\<^sub>p = p" ``` wenzelm@56000 ` 1288` ``` and "(1)\<^sub>p *\<^sub>p p = p" ``` wenzelm@52803 ` 1289` ``` using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] ``` chaieb@33154 ` 1290` ``` isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all ``` wenzelm@52658 ` 1291` wenzelm@52803 ` 1292` ```lemma polymul_0[simp]: ``` wenzelm@56000 ` 1293` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1294` ``` and np: "isnpolyh p n0" ``` wenzelm@56000 ` 1295` ``` shows "p *\<^sub>p 0\<^sub>p = 0\<^sub>p" ``` wenzelm@56000 ` 1296` ``` and "0\<^sub>p *\<^sub>p p = 0\<^sub>p" ``` wenzelm@52803 ` 1297` ``` using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] ``` chaieb@33154 ` 1298` ``` isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all ``` chaieb@33154 ` 1299` wenzelm@52803 ` 1300` ```lemma polymul_commute: ``` wenzelm@56000 ` 1301` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56000 ` 1302` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1303` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1304` ``` shows "p *\<^sub>p q = q *\<^sub>p p" ``` wenzelm@56043 ` 1305` ``` using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], ``` wenzelm@56043 ` 1306` ``` where ?'a = "'a::{field_char_0,field_inverse_zero, power}"] ``` wenzelm@52658 ` 1307` ``` by simp ``` chaieb@33154 ` 1308` wenzelm@52658 ` 1309` ```declare polyneg_polyneg [simp] ``` wenzelm@52803 ` 1310` wenzelm@52803 ` 1311` ```lemma isnpolyh_polynate_id [simp]: ``` wenzelm@56000 ` 1312` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56000 ` 1313` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1314` ``` shows "polynate p = p" ``` wenzelm@56043 ` 1315` ``` using isnpolyh_unique[where ?'a= "'a::{field_char_0,field_inverse_zero}", ``` wenzelm@56043 ` 1316` ``` OF polynate_norm[of p, unfolded isnpoly_def] np] ``` wenzelm@56043 ` 1317` ``` polynate[where ?'a = "'a::{field_char_0,field_inverse_zero}"] ``` wenzelm@52658 ` 1318` ``` by simp ``` chaieb@33154 ` 1319` wenzelm@52803 ` 1320` ```lemma polynate_idempotent[simp]: ``` wenzelm@56000 ` 1321` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 1322` ``` shows "polynate (polynate p) = polynate p" ``` chaieb@33154 ` 1323` ``` using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . ``` chaieb@33154 ` 1324` chaieb@33154 ` 1325` ```lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)" ``` chaieb@33154 ` 1326` ``` unfolding poly_nate_def polypoly'_def .. ``` wenzelm@52658 ` 1327` wenzelm@52658 ` 1328` ```lemma poly_nate_poly: ``` wenzelm@56000 ` 1329` ``` "poly (poly_nate bs p) = (\x:: 'a ::{field_char_0,field_inverse_zero}. \p\\<^sub>p\<^bsup>x # bs\<^esup>)" ``` chaieb@33154 ` 1330` ``` using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] ``` wenzelm@52658 ` 1331` ``` unfolding poly_nate_polypoly' by auto ``` wenzelm@52658 ` 1332` chaieb@33154 ` 1333` chaieb@33154 ` 1334` ```subsection{* heads, degrees and all that *} ``` wenzelm@52658 ` 1335` chaieb@33154 ` 1336` ```lemma degree_eq_degreen0: "degree p = degreen p 0" ``` wenzelm@52658 ` 1337` ``` by (induct p rule: degree.induct) simp_all ``` chaieb@33154 ` 1338` wenzelm@52658 ` 1339` ```lemma degree_polyneg: ``` wenzelm@56043 ` 1340` ``` assumes "isnpolyh p n" ``` chaieb@33154 ` 1341` ``` shows "degree (polyneg p) = degree p" ``` wenzelm@56043 ` 1342` ``` apply (induct p rule: polyneg.induct) ``` wenzelm@56043 ` 1343` ``` using assms ``` wenzelm@56043 ` 1344` ``` apply simp_all ``` wenzelm@52658 ` 1345` ``` apply (case_tac na) ``` wenzelm@52658 ` 1346` ``` apply auto ``` wenzelm@52658 ` 1347` ``` done ``` chaieb@33154 ` 1348` chaieb@33154 ` 1349` ```lemma degree_polyadd: ``` wenzelm@56043 ` 1350` ``` assumes np: "isnpolyh p n0" ``` wenzelm@56043 ` 1351` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1352` ``` shows "degree (p +\<^sub>p q) \ max (degree p) (degree q)" ``` wenzelm@52658 ` 1353` ``` using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp ``` chaieb@33154 ` 1354` chaieb@33154 ` 1355` wenzelm@52658 ` 1356` ```lemma degree_polysub: ``` wenzelm@52658 ` 1357` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1358` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1359` ``` shows "degree (p -\<^sub>p q) \ max (degree p) (degree q)" ``` chaieb@33154 ` 1360` ```proof- ``` wenzelm@56043 ` 1361` ``` from nq have nq': "isnpolyh (~\<^sub>p q) n1" ``` wenzelm@56043 ` 1362` ``` using polyneg_normh by simp ``` wenzelm@56043 ` 1363` ``` from degree_polyadd[OF np nq'] show ?thesis ``` wenzelm@56043 ` 1364` ``` by (simp add: polysub_def degree_polyneg[OF nq]) ``` chaieb@33154 ` 1365` ```qed ``` chaieb@33154 ` 1366` wenzelm@52803 ` 1367` ```lemma degree_polysub_samehead: ``` wenzelm@56000 ` 1368` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56043 ` 1369` ``` and np: "isnpolyh p n0" ``` wenzelm@56043 ` 1370` ``` and nq: "isnpolyh q n1" ``` wenzelm@56043 ` 1371` ``` and h: "head p = head q" ``` wenzelm@52658 ` 1372` ``` and d: "degree p = degree q" ``` chaieb@33154 ` 1373` ``` shows "degree (p -\<^sub>p q) < degree p \ (p -\<^sub>p q = 0\<^sub>p)" ``` wenzelm@52658 ` 1374` ``` unfolding polysub_def split_def fst_conv snd_conv ``` wenzelm@52658 ` 1375` ``` using np nq h d ``` wenzelm@52658 ` 1376` ```proof (induct p q rule: polyadd.induct) ``` wenzelm@52658 ` 1377` ``` case (1 c c') ``` wenzelm@56009 ` 1378` ``` then show ?case ``` wenzelm@56009 ` 1379` ``` by (simp add: Nsub_def Nsub0[simplified Nsub_def]) ``` chaieb@33154 ` 1380` ```next ``` wenzelm@52803 ` 1381` ``` case (2 c c' n' p') ``` wenzelm@56009 ` 1382` ``` from 2 have "degree (C c) = degree (CN c' n' p')" ``` wenzelm@56009 ` 1383` ``` by simp ``` wenzelm@56009 ` 1384` ``` then have nz: "n' > 0" ``` wenzelm@56009 ` 1385` ``` by (cases n') auto ``` wenzelm@56009 ` 1386` ``` then have "head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1387` ``` by (cases n') auto ``` wenzelm@56009 ` 1388` ``` with 2 show ?case ``` wenzelm@56009 ` 1389` ``` by simp ``` chaieb@33154 ` 1390` ```next ``` wenzelm@52803 ` 1391` ``` case (3 c n p c') ``` wenzelm@56009 ` 1392` ``` then have "degree (C c') = degree (CN c n p)" ``` wenzelm@56009 ` 1393` ``` by simp ``` wenzelm@56009 ` 1394` ``` then have nz: "n > 0" ``` wenzelm@56009 ` 1395` ``` by (cases n) auto ``` wenzelm@56009 ` 1396` ``` then have "head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1397` ``` by (cases n) auto ``` wenzelm@41807 ` 1398` ``` with 3 show ?case by simp ``` chaieb@33154 ` 1399` ```next ``` chaieb@33154 ` 1400` ``` case (4 c n p c' n' p') ``` wenzelm@56009 ` 1401` ``` then have H: ``` wenzelm@56009 ` 1402` ``` "isnpolyh (CN c n p) n0" ``` wenzelm@56009 ` 1403` ``` "isnpolyh (CN c' n' p') n1" ``` wenzelm@56009 ` 1404` ``` "head (CN c n p) = head (CN c' n' p')" ``` wenzelm@56009 ` 1405` ``` "degree (CN c n p) = degree (CN c' n' p')" ``` wenzelm@56009 ` 1406` ``` by simp_all ``` wenzelm@56009 ` 1407` ``` then have degc: "degree c = 0" and degc': "degree c' = 0" ``` wenzelm@56009 ` 1408` ``` by simp_all ``` wenzelm@56009 ` 1409` ``` then have degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" ``` chaieb@33154 ` 1410` ``` using H(1-2) degree_polyneg by auto ``` wenzelm@56009 ` 1411` ``` from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" ``` wenzelm@56009 ` 1412` ``` by simp_all ``` wenzelm@56009 ` 1413` ``` from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' ``` wenzelm@56009 ` 1414` ``` have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" ``` wenzelm@56009 ` 1415` ``` by simp ``` wenzelm@56009 ` 1416` ``` from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" ``` wenzelm@56009 ` 1417` ``` by auto ``` wenzelm@56009 ` 1418` ``` have "n = n' \ n < n' \ n > n'" ``` wenzelm@56009 ` 1419` ``` by arith ``` chaieb@33154 ` 1420` ``` moreover ``` wenzelm@56009 ` 1421` ``` { ``` wenzelm@56009 ` 1422` ``` assume nn': "n = n'" ``` wenzelm@56009 ` 1423` ``` have "n = 0 \ n > 0" by arith ``` wenzelm@56066 ` 1424` ``` moreover ``` wenzelm@56066 ` 1425` ``` { ``` wenzelm@56009 ` 1426` ``` assume nz: "n = 0" ``` wenzelm@56009 ` 1427` ``` then have ?case using 4 nn' ``` wenzelm@56009 ` 1428` ``` by (auto simp add: Let_def degcmc') ``` wenzelm@56009 ` 1429` ``` } ``` wenzelm@56066 ` 1430` ``` moreover ``` wenzelm@56066 ` 1431` ``` { ``` wenzelm@56009 ` 1432` ``` assume nz: "n > 0" ``` wenzelm@56009 ` 1433` ``` with nn' H(3) have cc': "c = c'" and pp': "p = p'" ``` wenzelm@56009 ` 1434` ``` by (cases n, auto)+ ``` wenzelm@56009 ` 1435` ``` then have ?case ``` wenzelm@56009 ` 1436` ``` using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] ``` wenzelm@56009 ` 1437` ``` using polysub_same_0[OF c'nh, simplified polysub_def] ``` wenzelm@56009 ` 1438` ``` using nn' 4 by (simp add: Let_def) ``` wenzelm@56009 ` 1439` ``` } ``` wenzelm@56009 ` 1440` ``` ultimately have ?case by blast ``` wenzelm@56009 ` 1441` ``` } ``` chaieb@33154 ` 1442` ``` moreover ``` wenzelm@56009 ` 1443` ``` { ``` wenzelm@56009 ` 1444` ``` assume nn': "n < n'" ``` wenzelm@56009 ` 1445` ``` then have n'p: "n' > 0" ``` wenzelm@56009 ` 1446` ``` by simp ``` wenzelm@56009 ` 1447` ``` then have headcnp':"head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1448` ``` by (cases n') simp_all ``` wenzelm@56009 ` 1449` ``` have degcnp': "degree (CN c' n' p') = 0" ``` wenzelm@56009 ` 1450` ``` and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" ``` wenzelm@52658 ` 1451` ``` using 4 nn' by (cases n', simp_all) ``` wenzelm@56009 ` 1452` ``` then have "n > 0" ``` wenzelm@56009 ` 1453` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1454` ``` then have headcnp: "head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1455` ``` by (cases n) auto ``` wenzelm@56009 ` 1456` ``` from H(3) headcnp headcnp' nn' have ?case ``` wenzelm@56009 ` 1457` ``` by auto ``` wenzelm@56009 ` 1458` ``` } ``` chaieb@33154 ` 1459` ``` moreover ``` wenzelm@56009 ` 1460` ``` { ``` wenzelm@56009 ` 1461` ``` assume nn': "n > n'" ``` wenzelm@56009 ` 1462` ``` then have np: "n > 0" by simp ``` wenzelm@56009 ` 1463` ``` then have headcnp:"head (CN c n p) = CN c n p" ``` wenzelm@56009 ` 1464` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1465` ``` from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" ``` wenzelm@56009 ` 1466` ``` by simp ``` wenzelm@56009 ` 1467` ``` from np have degcnp: "degree (CN c n p) = 0" ``` wenzelm@56009 ` 1468` ``` by (cases n) simp_all ``` wenzelm@56009 ` 1469` ``` with degcnpeq have "n' > 0" ``` wenzelm@56009 ` 1470` ``` by (cases n') simp_all ``` wenzelm@56009 ` 1471` ``` then have headcnp': "head (CN c' n' p') = CN c' n' p'" ``` wenzelm@56009 ` 1472` ``` by (cases n') auto ``` wenzelm@56009 ` 1473` ``` from H(3) headcnp headcnp' nn' have ?case by auto ``` wenzelm@56009 ` 1474` ``` } ``` wenzelm@56009 ` 1475` ``` ultimately show ?case by blast ``` krauss@41812 ` 1476` ```qed auto ``` wenzelm@52803 ` 1477` chaieb@33154 ` 1478` ```lemma shift1_head : "isnpolyh p n0 \ head (shift1 p) = head p" ``` wenzelm@52658 ` 1479` ``` by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) ``` chaieb@33154 ` 1480` chaieb@33154 ` 1481` ```lemma funpow_shift1_head: "isnpolyh p n0 \ p\ 0\<^sub>p \ head (funpow k shift1 p) = head p" ``` wenzelm@52658 ` 1482` ```proof (induct k arbitrary: n0 p) ``` wenzelm@52658 ` 1483` ``` case 0 ``` wenzelm@56198 ` 1484` ``` then show ?case ``` wenzelm@56198 ` 1485` ``` by auto ``` wenzelm@52658 ` 1486` ```next ``` wenzelm@52658 ` 1487` ``` case (Suc k n0 p) ``` wenzelm@56066 ` 1488` ``` then have "isnpolyh (shift1 p) 0" ``` wenzelm@56066 ` 1489` ``` by (simp add: shift1_isnpolyh) ``` wenzelm@41807 ` 1490` ``` with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" ``` wenzelm@56066 ` 1491` ``` and "head (shift1 p) = head p" ``` wenzelm@56066 ` 1492` ``` by (simp_all add: shift1_head) ``` wenzelm@56066 ` 1493` ``` then show ?case ``` wenzelm@56066 ` 1494` ``` by (simp add: funpow_swap1) ``` wenzelm@52658 ` 1495` ```qed ``` chaieb@33154 ` 1496` chaieb@33154 ` 1497` ```lemma shift1_degree: "degree (shift1 p) = 1 + degree p" ``` chaieb@33154 ` 1498` ``` by (simp add: shift1_def) ``` wenzelm@56009 ` 1499` chaieb@33154 ` 1500` ```lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p " ``` wenzelm@46991 ` 1501` ``` by (induct k arbitrary: p) (auto simp add: shift1_degree) ``` chaieb@33154 ` 1502` chaieb@33154 ` 1503` ```lemma funpow_shift1_nz: "p \ 0\<^sub>p \ funpow n shift1 p \ 0\<^sub>p" ``` wenzelm@52658 ` 1504` ``` by (induct n arbitrary: p) simp_all ``` chaieb@33154 ` 1505` chaieb@33154 ` 1506` ```lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ head p = p" ``` wenzelm@52658 ` 1507` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1508` ```lemma headn_0[simp]: "isnpolyh p n \ m < n \ headn p m = p" ``` wenzelm@52658 ` 1509` ``` by (induct p arbitrary: n rule: degreen.induct) auto ``` chaieb@33154 ` 1510` ```lemma head_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ head p = p" ``` wenzelm@52658 ` 1511` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1512` ```lemma head_head[simp]: "isnpolyh p n0 \ head (head p) = head p" ``` wenzelm@52658 ` 1513` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1514` wenzelm@52803 ` 1515` ```lemma polyadd_eq_const_degree: ``` wenzelm@52658 ` 1516` ``` "isnpolyh p n0 \ isnpolyh q n1 \ polyadd p q = C c \ degree p = degree q" ``` chaieb@33154 ` 1517` ``` using polyadd_eq_const_degreen degree_eq_degreen0 by simp ``` chaieb@33154 ` 1518` wenzelm@52658 ` 1519` ```lemma polyadd_head: ``` wenzelm@52658 ` 1520` ``` assumes np: "isnpolyh p n0" ``` wenzelm@52658 ` 1521` ``` and nq: "isnpolyh q n1" ``` wenzelm@52658 ` 1522` ``` and deg: "degree p \ degree q" ``` chaieb@33154 ` 1523` ``` shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)" ``` wenzelm@52658 ` 1524` ``` using np nq deg ``` wenzelm@52658 ` 1525` ``` apply (induct p q arbitrary: n0 n1 rule: polyadd.induct) ``` wenzelm@52658 ` 1526` ``` apply simp_all ``` wenzelm@52658 ` 1527` ``` apply (case_tac n', simp, simp) ``` wenzelm@52658 ` 1528` ``` apply (case_tac n, simp, simp) ``` wenzelm@52658 ` 1529` ``` apply (case_tac n, case_tac n', simp add: Let_def) ``` haftmann@54489 ` 1530` ``` apply (auto simp add: polyadd_eq_const_degree)[2] ``` wenzelm@52658 ` 1531` ``` apply (metis head_nz) ``` wenzelm@52658 ` 1532` ``` apply (metis head_nz) ``` wenzelm@52658 ` 1533` ``` apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) ``` wenzelm@52658 ` 1534` ``` done ``` chaieb@33154 ` 1535` wenzelm@52803 ` 1536` ```lemma polymul_head_polyeq: ``` wenzelm@56000 ` 1537` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56066 ` 1538` ``` 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 ` 1539` ```proof (induct p q arbitrary: n0 n1 rule: polymul.induct) ``` krauss@41813 ` 1540` ``` case (2 c c' n' p' n0 n1) ``` wenzelm@56009 ` 1541` ``` then have "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" ``` wenzelm@56009 ` 1542` ``` by (simp_all add: head_isnpolyh) ``` wenzelm@56009 ` 1543` ``` then show ?case ``` wenzelm@56009 ` 1544` ``` using 2 by (cases n') auto ``` wenzelm@52803 ` 1545` ```next ``` wenzelm@52803 ` 1546` ``` case (3 c n p c' n0 n1) ``` wenzelm@56009 ` 1547` ``` then have "isnpolyh (head (CN c n p)) n0" "isnormNum c'" ``` wenzelm@56009 ` 1548` ``` by (simp_all add: head_isnpolyh) ``` wenzelm@56066 ` 1549` ``` then show ?case ``` wenzelm@56066 ` 1550` ``` using 3 by (cases n) auto ``` chaieb@33154 ` 1551` ```next ``` chaieb@33154 ` 1552` ``` case (4 c n p c' n' p' n0 n1) ``` wenzelm@56066 ` 1553` ``` then have norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" ``` chaieb@33154 ` 1554` ``` "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'" ``` chaieb@33154 ` 1555` ``` by simp_all ``` chaieb@33154 ` 1556` ``` have "n < n' \ n' < n \ n = n'" by arith ``` wenzelm@52803 ` 1557` ``` moreover ``` wenzelm@56009 ` 1558` ``` { ``` wenzelm@56009 ` 1559` ``` assume nn': "n < n'" ``` wenzelm@56009 ` 1560` ``` then have ?case ``` wenzelm@52658 ` 1561` ``` using norm "4.hyps"(2)[OF norm(1,6)] "4.hyps"(1)[OF norm(2,6)] ``` wenzelm@52658 ` 1562` ``` apply simp ``` wenzelm@52658 ` 1563` ``` apply (cases n) ``` wenzelm@52658 ` 1564` ``` apply simp ``` wenzelm@52658 ` 1565` ``` apply (cases n') ``` wenzelm@52658 ` 1566` ``` apply simp_all ``` wenzelm@56009 ` 1567` ``` done ``` wenzelm@56009 ` 1568` ``` } ``` wenzelm@56009 ` 1569` ``` moreover { ``` wenzelm@56009 ` 1570` ``` assume nn': "n'< n" ``` wenzelm@56009 ` 1571` ``` then have ?case ``` wenzelm@52803 ` 1572` ``` using norm "4.hyps"(6) [OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] ``` wenzelm@52658 ` 1573` ``` apply simp ``` wenzelm@52658 ` 1574` ``` apply (cases n') ``` wenzelm@52658 ` 1575` ``` apply simp ``` wenzelm@52658 ` 1576` ``` apply (cases n) ``` wenzelm@52658 ` 1577` ``` apply auto ``` wenzelm@56009 ` 1578` ``` done ``` wenzelm@56009 ` 1579` ``` } ``` wenzelm@56066 ` 1580` ``` moreover ``` wenzelm@56066 ` 1581` ``` { ``` wenzelm@56009 ` 1582` ``` assume nn': "n' = n" ``` wenzelm@52803 ` 1583` ``` from nn' polymul_normh[OF norm(5,4)] ``` chaieb@33154 ` 1584` ``` have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def) ``` wenzelm@52803 ` 1585` ``` from nn' polymul_normh[OF norm(5,3)] norm ``` chaieb@33154 ` 1586` ``` have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp ``` chaieb@33154 ` 1587` ``` from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6) ``` wenzelm@52803 ` 1588` ``` have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp ``` wenzelm@52803 ` 1589` ``` from polyadd_normh[OF ncnpc' ncnpp0'] ``` wenzelm@52803 ` 1590` ``` 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 ` 1591` ``` by (simp add: min_def) ``` wenzelm@56009 ` 1592` ``` { ``` wenzelm@56009 ` 1593` ``` assume np: "n > 0" ``` chaieb@33154 ` 1594` ``` with nn' head_isnpolyh_Suc'[OF np nth] ``` wenzelm@33268 ` 1595` ``` head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] ``` wenzelm@56009 ` 1596` ``` have ?case by simp ``` wenzelm@56009 ` 1597` ``` } ``` chaieb@33154 ` 1598` ``` moreover ``` wenzelm@56009 ` 1599` ``` { ``` wenzelm@56009 ` 1600` ``` assume nz: "n = 0" ``` chaieb@33154 ` 1601` ``` from polymul_degreen[OF norm(5,4), where m="0"] ``` wenzelm@33268 ` 1602` ``` polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 ``` chaieb@33154 ` 1603` ``` norm(5,6) degree_npolyhCN[OF norm(6)] ``` wenzelm@56066 ` 1604` ``` have dth: "degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" ``` wenzelm@56066 ` 1605` ``` by simp ``` wenzelm@56066 ` 1606` ``` then have dth': "degree (CN c 0 p *\<^sub>p c') \ degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" ``` wenzelm@56066 ` 1607` ``` by simp ``` chaieb@33154 ` 1608` ``` from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth ``` wenzelm@56066 ` 1609` ``` have ?case ``` wenzelm@56066 ` 1610` ``` using norm "4.hyps"(6)[OF norm(5,3)] "4.hyps"(5)[OF norm(5,4)] nn' nz ``` wenzelm@56066 ` 1611` ``` by simp ``` wenzelm@56009 ` 1612` ``` } ``` wenzelm@56066 ` 1613` ``` ultimately have ?case ``` wenzelm@56066 ` 1614` ``` by (cases n) auto ``` wenzelm@56009 ` 1615` ``` } ``` chaieb@33154 ` 1616` ``` ultimately show ?case by blast ``` chaieb@33154 ` 1617` ```qed simp_all ``` chaieb@33154 ` 1618` chaieb@33154 ` 1619` ```lemma degree_coefficients: "degree p = length (coefficients p) - 1" ``` wenzelm@52658 ` 1620` ``` by (induct p rule: degree.induct) auto ``` chaieb@33154 ` 1621` chaieb@33154 ` 1622` ```lemma degree_head[simp]: "degree (head p) = 0" ``` wenzelm@52658 ` 1623` ``` by (induct p rule: head.induct) auto ``` chaieb@33154 ` 1624` krauss@41812 ` 1625` ```lemma degree_CN: "isnpolyh p n \ degree (CN c n p) \ 1 + degree p" ``` wenzelm@52658 ` 1626` ``` by (cases n) simp_all ``` wenzelm@56066 ` 1627` chaieb@33154 ` 1628` ```lemma degree_CN': "isnpolyh p n \ degree (CN c n p) \ degree p" ``` wenzelm@52658 ` 1629` ``` by (cases n) simp_all ``` chaieb@33154 ` 1630` wenzelm@52658 ` 1631` ```lemma polyadd_different_degree: ``` wenzelm@56066 ` 1632` ``` "isnpolyh p n0 \ isnpolyh q n1 \ degree p \ degree q \ ``` wenzelm@52658 ` 1633` ``` degree (polyadd p q) = max (degree p) (degree q)" ``` chaieb@33154 ` 1634` ``` using polyadd_different_degreen degree_eq_degreen0 by simp ``` chaieb@33154 ` 1635` chaieb@33154 ` 1636` ```lemma degreen_polyneg: "isnpolyh p n0 \ degreen (~\<^sub>p p) m = degreen p m" ``` wenzelm@52658 ` 1637` ``` by (induct p arbitrary: n0 rule: polyneg.induct) auto ``` chaieb@33154 ` 1638` chaieb@33154 ` 1639` ```lemma degree_polymul: ``` wenzelm@56000 ` 1640` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1641` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1642` ``` and nq: "isnpolyh q n1" ``` chaieb@33154 ` 1643` ``` shows "degree (p *\<^sub>p q) \ degree p + degree q" ``` chaieb@33154 ` 1644` ``` using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp ``` chaieb@33154 ` 1645` chaieb@33154 ` 1646` ```lemma polyneg_degree: "isnpolyh p n \ degree (polyneg p) = degree p" ``` wenzelm@52658 ` 1647` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` chaieb@33154 ` 1648` chaieb@33154 ` 1649` ```lemma polyneg_head: "isnpolyh p n \ head(polyneg p) = polyneg (head p)" ``` wenzelm@52658 ` 1650` ``` by (induct p arbitrary: n rule: degree.induct) auto ``` wenzelm@52658 ` 1651` chaieb@33154 ` 1652` chaieb@33154 ` 1653` ```subsection {* Correctness of polynomial pseudo division *} ``` chaieb@33154 ` 1654` chaieb@33154 ` 1655` ```lemma polydivide_aux_properties: ``` wenzelm@56000 ` 1656` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@52658 ` 1657` ``` and np: "isnpolyh p n0" ``` wenzelm@52658 ` 1658` ``` and ns: "isnpolyh s n1" ``` wenzelm@52658 ` 1659` ``` and ap: "head p = a" ``` wenzelm@56198 ` 1660` ``` and ndp: "degree p = n" ``` wenzelm@56198 ` 1661` ``` and pnz: "p \ 0\<^sub>p" ``` wenzelm@56198 ` 1662` ``` shows "polydivide_aux a n p k s = (k', r) \ k' \ k \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1663` ``` (\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 ` 1664` ``` using ns ``` wenzelm@52658 ` 1665` ```proof (induct "degree s" arbitrary: s k k' r n1 rule: less_induct) ``` berghofe@34915 ` 1666` ``` case less ``` chaieb@33154 ` 1667` ``` let ?qths = "\q n1. isnpolyh q n1 \ (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@56066 ` 1668` ``` let ?ths = "polydivide_aux a n p k s = (k', r) \ k \ k' \ ``` wenzelm@56066 ` 1669` ``` (degree r = 0 \ degree r < degree p) \ (\nr. isnpolyh r nr) \ ?qths" ``` chaieb@33154 ` 1670` ``` let ?b = "head s" ``` berghofe@34915 ` 1671` ``` let ?p' = "funpow (degree s - n) shift1 p" ``` wenzelm@50282 ` 1672` ``` let ?xdn = "funpow (degree s - n) shift1 (1)\<^sub>p" ``` chaieb@33154 ` 1673` ``` let ?akk' = "a ^\<^sub>p (k' - k)" ``` berghofe@34915 ` 1674` ``` note ns = `isnpolyh s n1` ``` wenzelm@52803 ` 1675` ``` from np have np0: "isnpolyh p 0" ``` wenzelm@52803 ` 1676` ``` using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by simp ``` wenzelm@52803 ` 1677` ``` have np': "isnpolyh ?p' 0" ``` wenzelm@52803 ` 1678` ``` using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="degree s - n"] isnpoly_def ``` wenzelm@52803 ` 1679` ``` by simp ``` wenzelm@52803 ` 1680` ``` have headp': "head ?p' = head p" ``` wenzelm@52803 ` 1681` ``` using funpow_shift1_head[OF np pnz] by simp ``` wenzelm@52803 ` 1682` ``` from funpow_shift1_isnpoly[where p="(1)\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" ``` wenzelm@52803 ` 1683` ``` by (simp add: isnpoly_def) ``` wenzelm@52803 ` 1684` ``` from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap ``` chaieb@33154 ` 1685` ``` have nakk':"isnpolyh ?akk' 0" by blast ``` wenzelm@56066 ` 1686` ``` { ``` wenzelm@56066 ` 1687` ``` assume sz: "s = 0\<^sub>p" ``` wenzelm@56066 ` 1688` ``` then have ?ths ``` wenzelm@56066 ` 1689` ``` using np polydivide_aux.simps ``` wenzelm@52658 ` 1690` ``` apply clarsimp ``` wenzelm@52658 ` 1691` ``` apply (rule exI[where x="0\<^sub>p"]) ``` wenzelm@52658 ` 1692` ``` apply simp ``` wenzelm@56066 ` 1693` ``` done ``` wenzelm@56066 ` 1694` ``` } ``` chaieb@33154 ` 1695` ``` moreover ``` wenzelm@56066 ` 1696` ``` { ``` wenzelm@56066 ` 1697` ``` assume sz: "s \ 0\<^sub>p" ``` wenzelm@56066 ` 1698` ``` { ``` wenzelm@56066 ` 1699` ``` assume dn: "degree s < n" ``` wenzelm@56066 ` 1700` ``` then have "?ths" ``` wenzelm@56066 ` 1701` ``` using ns ndp np polydivide_aux.simps ``` wenzelm@52658 ` 1702` ``` apply auto ``` wenzelm@52658 ` 1703` ``` apply (rule exI[where x="0\<^sub>p"]) ``` wenzelm@52658 ` 1704` ``` apply simp ``` wenzelm@56066 ` 1705` ``` done ``` wenzelm@56066 ` 1706` ``` } ``` wenzelm@52803 ` 1707` ``` moreover ``` wenzelm@56066 ` 1708` ``` { ``` wenzelm@56066 ` 1709` ``` assume dn': "\ degree s < n" ``` wenzelm@56066 ` 1710` ``` then have dn: "degree s \ n" ``` wenzelm@56066 ` 1711` ``` by arith ``` wenzelm@52803 ` 1712` ``` have degsp': "degree s = degree ?p'" ``` wenzelm@56066 ` 1713` ``` using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] ``` wenzelm@56066 ` 1714` ``` by simp ``` wenzelm@56066 ` 1715` ``` { ``` wenzelm@56066 ` 1716` ``` assume ba: "?b = a" ``` wenzelm@56066 ` 1717` ``` then have headsp': "head s = head ?p'" ``` wenzelm@52803 ` 1718` ``` using ap headp' by simp ``` wenzelm@52803 ` 1719` ``` have nr: "isnpolyh (s -\<^sub>p ?p') 0" ``` wenzelm@52803 ` 1720` ``` using polysub_normh[OF ns np'] by simp ``` berghofe@34915 ` 1721` ``` from degree_polysub_samehead[OF ns np' headsp' degsp'] ``` berghofe@34915 ` 1722` ``` have "degree (s -\<^sub>p ?p') < degree s \ s -\<^sub>p ?p' = 0\<^sub>p" by simp ``` wenzelm@52803 ` 1723` ``` moreover ``` wenzelm@56066 ` 1724` ``` { ``` wenzelm@56066 ` 1725` ``` assume deglt:"degree (s -\<^sub>p ?p') < degree s" ``` krauss@41403 ` 1726` ``` from polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1727` ``` have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" ``` wenzelm@33268 ` 1728` ``` by (simp add: Let_def) ``` wenzelm@56066 ` 1729` ``` { ``` wenzelm@56066 ` 1730` ``` assume h1: "polydivide_aux a n p k s = (k', r)" ``` wenzelm@52803 ` 1731` ``` from less(1)[OF deglt nr, of k k' r] trans[OF eq[symmetric] h1] ``` wenzelm@52803 ` 1732` ``` have kk': "k \ k'" ``` wenzelm@56066 ` 1733` ``` and nr: "\nr. isnpolyh r nr" ``` wenzelm@52803 ` 1734` ``` and dr: "degree r = 0 \ degree r < degree p" ``` wenzelm@56066 ` 1735` ``` 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 ` 1736` ``` by auto ``` wenzelm@52803 ` 1737` ``` from q1 obtain q n1 where nq: "isnpolyh q n1" ``` wenzelm@56066 ` 1738` ``` and asp: "a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r" ``` wenzelm@56066 ` 1739` ``` by blast ``` wenzelm@56066 ` 1740` ``` from nr obtain nr where nr': "isnpolyh r nr" ``` wenzelm@56066 ` 1741` ``` by blast ``` wenzelm@52803 ` 1742` ``` from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" ``` wenzelm@52803 ` 1743` ``` by simp ``` wenzelm@33268 ` 1744` ``` from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq] ``` wenzelm@33268 ` 1745` ``` have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp ``` wenzelm@52803 ` 1746` ``` from polyadd_normh[OF polymul_normh[OF np ``` wenzelm@33268 ` 1747` ``` polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr'] ``` wenzelm@52803 ` 1748` ``` have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" ``` wenzelm@52803 ` 1749` ``` by simp ``` wenzelm@56066 ` 1750` ``` from asp have "\bs :: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1751` ``` Ipoly bs (a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p')) = Ipoly bs (p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@56066 ` 1752` ``` by simp ``` wenzelm@56066 ` 1753` ``` then have "\bs :: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1754` ``` Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = ``` wenzelm@52803 ` 1755` ``` Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" ``` haftmann@36349 ` 1756` ``` by (simp add: field_simps) ``` wenzelm@56066 ` 1757` ``` then have "\bs :: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1758` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1759` ``` Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p *\<^sub>p p) + ``` wenzelm@52803 ` 1760` ``` Ipoly bs p * Ipoly bs q + Ipoly bs r" ``` wenzelm@52803 ` 1761` ``` by (auto simp only: funpow_shift1_1) ``` wenzelm@56066 ` 1762` ``` then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1763` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1764` ``` Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 (1)\<^sub>p) + ``` wenzelm@52803 ` 1765` ``` Ipoly bs q) + Ipoly bs r" ``` wenzelm@52803 ` 1766` ``` by (simp add: field_simps) ``` wenzelm@56066 ` 1767` ``` then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1768` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1769` ``` 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 ` 1770` ``` by simp ``` wenzelm@33268 ` 1771` ``` with isnpolyh_unique[OF nakks' nqr'] ``` wenzelm@52803 ` 1772` ``` have "a ^\<^sub>p (k' - k) *\<^sub>p s = ``` wenzelm@52803 ` 1773` ``` 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 ` 1774` ``` by blast ``` wenzelm@56066 ` 1775` ``` then have ?qths using nq' ``` wenzelm@50282 ` 1776` ``` 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 ` 1777` ``` apply (rule_tac x="0" in exI) ``` wenzelm@52803 ` 1778` ``` apply simp ``` wenzelm@52803 ` 1779` ``` done ``` wenzelm@56066 ` 1780` ``` with kk' nr dr have "k \ k' \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1781` ``` (\nr. isnpolyh r nr) \ ?qths" ``` wenzelm@52803 ` 1782` ``` by blast ``` wenzelm@52803 ` 1783` ``` } ``` wenzelm@56066 ` 1784` ``` then have ?ths by blast ``` wenzelm@52803 ` 1785` ``` } ``` wenzelm@52803 ` 1786` ``` moreover ``` wenzelm@56066 ` 1787` ``` { ``` wenzelm@56066 ` 1788` ``` assume spz:"s -\<^sub>p ?p' = 0\<^sub>p" ``` wenzelm@56000 ` 1789` ``` 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@56066 ` 1790` ``` have "\bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs ?p'" ``` wenzelm@52803 ` 1791` ``` by simp ``` wenzelm@56066 ` 1792` ``` then have "\bs:: 'a::{field_char_0,field_inverse_zero} list. Ipoly bs s = Ipoly bs (?xdn *\<^sub>p p)" ``` wenzelm@52658 ` 1793` ``` using np nxdn ``` wenzelm@52658 ` 1794` ``` apply simp ``` wenzelm@52658 ` 1795` ``` apply (simp only: funpow_shift1_1) ``` wenzelm@52658 ` 1796` ``` apply simp ``` wenzelm@52658 ` 1797` ``` done ``` wenzelm@56066 ` 1798` ``` then have sp': "s = ?xdn *\<^sub>p p" ``` wenzelm@56066 ` 1799` ``` using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] ``` wenzelm@52658 ` 1800` ``` by blast ``` wenzelm@56066 ` 1801` ``` { ``` wenzelm@56066 ` 1802` ``` assume h1: "polydivide_aux a n p k s = (k',r)" ``` krauss@41403 ` 1803` ``` from polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1804` ``` have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')" ``` wenzelm@33268 ` 1805` ``` by (simp add: Let_def) ``` wenzelm@52803 ` 1806` ``` also have "\ = (k,0\<^sub>p)" ``` wenzelm@52803 ` 1807` ``` using polydivide_aux.simps spz by simp ``` wenzelm@56066 ` 1808` ``` finally have "(k', r) = (k, 0\<^sub>p)" ``` wenzelm@56066 ` 1809` ``` using h1 by simp ``` berghofe@34915 ` 1810` ``` with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]] ``` krauss@41403 ` 1811` ``` polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths ``` wenzelm@33268 ` 1812` ``` apply auto ``` wenzelm@52803 ` 1813` ``` apply (rule exI[where x="?xdn"]) ``` berghofe@34915 ` 1814` ``` apply (auto simp add: polymul_commute[of p]) ``` wenzelm@52803 ` 1815` ``` done ``` wenzelm@52803 ` 1816` ``` } ``` wenzelm@52803 ` 1817` ``` } ``` wenzelm@52803 ` 1818` ``` ultimately have ?ths by blast ``` wenzelm@52803 ` 1819` ``` } ``` chaieb@33154 ` 1820` ``` moreover ``` wenzelm@56066 ` 1821` ``` { ``` wenzelm@56066 ` 1822` ``` assume ba: "?b \ a" ``` wenzelm@52803 ` 1823` ``` from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] ``` wenzelm@33268 ` 1824` ``` polymul_normh[OF head_isnpolyh[OF ns] np']] ``` wenzelm@52803 ` 1825` ``` have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" ``` wenzelm@52803 ` 1826` ``` by (simp add: min_def) ``` wenzelm@33268 ` 1827` ``` have nzths: "a *\<^sub>p s \ 0\<^sub>p" "?b *\<^sub>p ?p' \ 0\<^sub>p" ``` wenzelm@52803 ` 1828` ``` using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] ``` wenzelm@33268 ` 1829` ``` polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns] ``` wenzelm@52803 ` 1830` ``` funpow_shift1_nz[OF pnz] ``` wenzelm@52803 ` 1831` ``` by simp_all ``` wenzelm@33268 ` 1832` ``` from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz ``` berghofe@34915 ` 1833` ``` 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 ` 1834` ``` have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" ``` wenzelm@33268 ` 1835` ``` using head_head[OF ns] funpow_shift1_head[OF np pnz] ``` wenzelm@33268 ` 1836` ``` polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]] ``` wenzelm@33268 ` 1837` ``` by (simp add: ap) ``` wenzelm@33268 ` 1838` ``` from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"] ``` wenzelm@33268 ` 1839` ``` head_nz[OF np] pnz sz ap[symmetric] ``` berghofe@34915 ` 1840` ``` funpow_shift1_nz[OF pnz, where n="degree s - n"] ``` wenzelm@52803 ` 1841` ``` polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"] head_nz[OF ns] ``` berghofe@34915 ` 1842` ``` ndp dn ``` wenzelm@52803 ` 1843` ``` have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p')" ``` wenzelm@33268 ` 1844` ``` by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree) ``` wenzelm@56066 ` 1845` ``` { ``` wenzelm@56066 ` 1846` ``` assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s" ``` wenzelm@52803 ` 1847` ``` from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] ``` wenzelm@52803 ` 1848` ``` polymul_normh[OF head_isnpolyh[OF ns]np']] ap ``` wenzelm@52803 ` 1849` ``` have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" ``` wenzelm@52803 ` 1850` ``` by simp ``` wenzelm@56066 ` 1851` ``` { ``` wenzelm@56066 ` 1852` ``` assume h1:"polydivide_aux a n p k s = (k', r)" ``` krauss@41403 ` 1853` ``` from h1 polydivide_aux.simps sz dn' ba ``` krauss@41403 ` 1854` ``` have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)" ``` wenzelm@33268 ` 1855` ``` by (simp add: Let_def) ``` berghofe@34915 ` 1856` ``` with less(1)[OF dth nasbp', of "Suc k" k' r] ``` wenzelm@52803 ` 1857` ``` obtain q nq nr where kk': "Suc k \ k'" ``` wenzelm@52803 ` 1858` ``` and nr: "isnpolyh r nr" ``` wenzelm@52803 ` 1859` ``` and nq: "isnpolyh q nq" ``` wenzelm@33268 ` 1860` ``` and dr: "degree r = 0 \ degree r < degree p" ``` wenzelm@52803 ` 1861` ``` 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 ` 1862` ``` by auto ``` wenzelm@56066 ` 1863` ``` from kk' have kk'': "Suc (k' - Suc k) = k' - k" ``` wenzelm@56066 ` 1864` ``` by arith ``` wenzelm@52803 ` 1865` ``` { ``` wenzelm@56066 ` 1866` ``` fix bs :: "'a::{field_char_0,field_inverse_zero} list" ``` wenzelm@52803 ` 1867` ``` from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric] ``` wenzelm@52803 ` 1868` ``` 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 ` 1869` ``` by simp ``` wenzelm@56066 ` 1870` ``` then have "Ipoly bs a ^ (Suc (k' - Suc k)) * Ipoly bs s = ``` wenzelm@52803 ` 1871` ``` Ipoly bs p * Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?p' + Ipoly bs r" ``` wenzelm@52803 ` 1872` ``` by (simp add: field_simps) ``` wenzelm@56066 ` 1873` ``` then have "Ipoly bs a ^ (k' - k) * Ipoly bs s = ``` wenzelm@52803 ` 1874` ``` 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 ` 1875` ``` by (simp add: kk'' funpow_shift1_1[where n="degree s - n" and p="p"]) ``` wenzelm@56066 ` 1876` ``` then have "Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1877` ``` Ipoly bs p * (Ipoly bs q + Ipoly bs a ^ (k' - Suc k) * Ipoly bs ?b * Ipoly bs ?xdn) + Ipoly bs r" ``` wenzelm@52803 ` 1878` ``` by (simp add: field_simps) ``` wenzelm@52803 ` 1879` ``` } ``` wenzelm@56066 ` 1880` ``` then have ieq:"\bs :: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1881` ``` Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = ``` wenzelm@52803 ` 1882` ``` 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 ` 1883` ``` by auto ``` wenzelm@33268 ` 1884` ``` let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)" ``` wenzelm@33268 ` 1885` ``` 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 ` 1886` ``` have nqw: "isnpolyh ?q 0" ``` wenzelm@52803 ` 1887` ``` by simp ``` wenzelm@33268 ` 1888` ``` 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 ` 1889` ``` 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 ` 1890` ``` by blast ``` wenzelm@52803 ` 1891` ``` from dr kk' nr h1 asth nqw have ?ths ``` wenzelm@52803 ` 1892` ``` apply simp ``` wenzelm@33268 ` 1893` ``` apply (rule conjI) ``` wenzelm@33268 ` 1894` ``` apply (rule exI[where x="nr"], simp) ``` wenzelm@33268 ` 1895` ``` apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp) ``` wenzelm@33268 ` 1896` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@52803 ` 1897` ``` done ``` wenzelm@52803 ` 1898` ``` } ``` wenzelm@56066 ` 1899` ``` then have ?ths by blast ``` wenzelm@52803 ` 1900` ``` } ``` wenzelm@52803 ` 1901` ``` moreover ``` wenzelm@56066 ` 1902` ``` { ``` wenzelm@56066 ` 1903` ``` assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p" ``` wenzelm@52803 ` 1904` ``` { ``` wenzelm@56000 ` 1905` ``` fix bs :: "'a::{field_char_0,field_inverse_zero} list" ``` wenzelm@33268 ` 1906` ``` from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz ``` wenzelm@52803 ` 1907` ``` have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" ``` wenzelm@52803 ` 1908` ``` by simp ``` wenzelm@56066 ` 1909` ``` then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" ``` wenzelm@52803 ` 1910` ``` by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"]) ``` wenzelm@56066 ` 1911` ``` then have "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" ``` wenzelm@52803 ` 1912` ``` by simp ``` wenzelm@52803 ` 1913` ``` } ``` wenzelm@56066 ` 1914` ``` then have hth: "\bs :: 'a::{field_char_0,field_inverse_zero} list. ``` wenzelm@56066 ` 1915` ``` Ipoly bs (a *\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" .. ``` wenzelm@52803 ` 1916` ``` from hth have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" ``` wenzelm@56000 ` 1917` ``` using isnpolyh_unique[where ?'a = "'a::{field_char_0,field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] ``` chaieb@33154 ` 1918` ``` polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]], ``` wenzelm@56066 ` 1919` ``` simplified ap] ``` wenzelm@56066 ` 1920` ``` by simp ``` wenzelm@56066 ` 1921` ``` { ``` wenzelm@56066 ` 1922` ``` assume h1: "polydivide_aux a n p k s = (k', r)" ``` wenzelm@52803 ` 1923` ``` from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps ``` wenzelm@56066 ` 1924` ``` have "(k', r) = (Suc k, 0\<^sub>p)" ``` wenzelm@56066 ` 1925` ``` by (simp add: Let_def) ``` wenzelm@52803 ` 1926` ``` with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn] ``` wenzelm@52803 ` 1927` ``` polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq ``` wenzelm@52803 ` 1928` ``` have ?ths ``` wenzelm@52803 ` 1929` ``` apply (clarsimp simp add: Let_def) ``` wenzelm@52803 ` 1930` ``` apply (rule exI[where x="?b *\<^sub>p ?xdn"]) ``` wenzelm@52803 ` 1931` ``` apply simp ``` wenzelm@52803 ` 1932` ``` apply (rule exI[where x="0"], simp) ``` wenzelm@52803 ` 1933` ``` done ``` wenzelm@52803 ` 1934` ``` } ``` wenzelm@56066 ` 1935` ``` then have ?ths by blast ``` wenzelm@52803 ` 1936` ``` } ``` wenzelm@52658 ` 1937` ``` ultimately have ?ths ``` wenzelm@56066 ` 1938` ``` 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 ` 1939` ``` head_nz[OF np] pnz sz ap[symmetric] ``` wenzelm@56066 ` 1940` ``` by (auto simp add: degree_eq_degreen0[symmetric]) ``` wenzelm@52803 ` 1941` ``` } ``` chaieb@33154 ` 1942` ``` ultimately have ?ths by blast ``` chaieb@33154 ` 1943` ``` } ``` wenzelm@52803 ` 1944` ``` ultimately have ?ths by blast ``` wenzelm@52803 ` 1945` ``` } ``` chaieb@33154 ` 1946` ``` ultimately show ?ths by blast ``` chaieb@33154 ` 1947` ```qed ``` chaieb@33154 ` 1948` wenzelm@52803 ` 1949` ```lemma polydivide_properties: ``` wenzelm@56000 ` 1950` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` wenzelm@56066 ` 1951` ``` and np: "isnpolyh p n0" ``` wenzelm@56066 ` 1952` ``` and ns: "isnpolyh s n1" ``` wenzelm@56066 ` 1953` ``` and pnz: "p \ 0\<^sub>p" ``` wenzelm@56066 ` 1954` ``` shows "\k r. polydivide s p = (k, r) \ ``` wenzelm@52803 ` 1955` ``` (\nr. isnpolyh r nr) \ (degree r = 0 \ degree r < degree p) \ ``` wenzelm@56066 ` 1956` ``` (\q n1. isnpolyh q n1 \ polypow k (head p) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)" ``` wenzelm@52803 ` 1957` ```proof - ``` wenzelm@52803 ` 1958` ``` have trv: "head p = head p" "degree p = degree p" ``` wenzelm@52803 ` 1959` ``` by simp_all ``` wenzelm@52803 ` 1960` ``` from polydivide_def[where s="s" and p="p"] have ex: "\ k r. polydivide s p = (k,r)" ``` wenzelm@52803 ` 1961` ``` by auto ``` wenzelm@52803 ` 1962` ``` then obtain k r where kr: "polydivide s p = (k,r)" ``` wenzelm@52803 ` 1963` ``` by blast ``` wenzelm@56000 ` 1964` ``` from trans[OF polydivide_def[where s="s"and p="p", symmetric] kr] ``` chaieb@33154 ` 1965` ``` polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"] ``` chaieb@33154 ` 1966` ``` have "(degree r = 0 \ degree r < degree p) \ ``` wenzelm@52803 ` 1967` ``` (\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 ` 1968` ``` by blast ``` wenzelm@52803 ` 1969` ``` with kr show ?thesis ``` chaieb@33154 ` 1970` ``` apply - ``` chaieb@33154 ` 1971` ``` apply (rule exI[where x="k"]) ``` chaieb@33154 ` 1972` ``` apply (rule exI[where x="r"]) ``` chaieb@33154 ` 1973` ``` apply simp ``` chaieb@33154 ` 1974` ``` done ``` chaieb@33154 ` 1975` ```qed ``` chaieb@33154 ` 1976` wenzelm@52658 ` 1977` wenzelm@56066 ` 1978` ```subsection {* More about polypoly and pnormal etc *} ``` chaieb@33154 ` 1979` wenzelm@56000 ` 1980` ```definition "isnonconstant p \ \ isconstant p" ``` chaieb@33154 ` 1981` wenzelm@52658 ` 1982` ```lemma isnonconstant_pnormal_iff: ``` wenzelm@56198 ` 1983` ``` assumes "isnonconstant p" ``` wenzelm@52803 ` 1984` ``` shows "pnormal (polypoly bs p) \ Ipoly bs (head p) \ 0" ``` chaieb@33154 ` 1985` ```proof ``` wenzelm@52803 ` 1986` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 1987` ``` assume H: "pnormal ?p" ``` wenzelm@56066 ` 1988` ``` have csz: "coefficients p \ []" ``` wenzelm@56198 ` 1989` ``` using assms by (cases p) auto ``` wenzelm@56066 ` 1990` ``` from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] pnormal_last_nonzero[OF H] ``` wenzelm@56066 ` 1991` ``` show "Ipoly bs (head p) \ 0" ``` wenzelm@56066 ` 1992` ``` by (simp add: polypoly_def) ``` chaieb@33154 ` 1993` ```next ``` chaieb@33154 ` 1994` ``` assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` chaieb@33154 ` 1995` ``` let ?p = "polypoly bs p" ``` wenzelm@56066 ` 1996` ``` have csz: "coefficients p \ []" ``` wenzelm@56198 ` 1997` ``` using assms by (cases p) auto ``` wenzelm@56066 ` 1998` ``` then have pz: "?p \ []" ``` wenzelm@56066 ` 1999` ``` by (simp add: polypoly_def) ``` wenzelm@56066 ` 2000` ``` then have lg: "length ?p > 0" ``` wenzelm@56066 ` 2001` ``` by simp ``` wenzelm@52803 ` 2002` ``` from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] ``` wenzelm@56066 ` 2003` ``` have lz: "last ?p \ 0" ``` wenzelm@56066 ` 2004` ``` by (simp add: polypoly_def) ``` chaieb@33154 ` 2005` ``` from pnormal_last_length[OF lg lz] show "pnormal ?p" . ``` chaieb@33154 ` 2006` ```qed ``` chaieb@33154 ` 2007` chaieb@33154 ` 2008` ```lemma isnonconstant_coefficients_length: "isnonconstant p \ length (coefficients p) > 1" ``` chaieb@33154 ` 2009` ``` unfolding isnonconstant_def ``` wenzelm@52658 ` 2010` ``` apply (cases p) ``` wenzelm@52658 ` 2011` ``` apply simp_all ``` wenzelm@52658 ` 2012` ``` apply (case_tac nat) ``` wenzelm@52658 ` 2013` ``` apply auto ``` chaieb@33154 ` 2014` ``` done ``` wenzelm@52658 ` 2015` wenzelm@52658 ` 2016` ```lemma isnonconstant_nonconstant: ``` wenzelm@56198 ` 2017` ``` assumes "isnonconstant p" ``` chaieb@33154 ` 2018` ``` shows "nonconstant (polypoly bs p) \ Ipoly bs (head p) \ 0" ``` chaieb@33154 ` 2019` ```proof ``` chaieb@33154 ` 2020` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2021` ``` assume nc: "nonconstant ?p" ``` wenzelm@56198 ` 2022` ``` from isnonconstant_pnormal_iff[OF assms, of bs] nc ``` wenzelm@56066 ` 2023` ``` show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56066 ` 2024` ``` unfolding nonconstant_def by blast ``` chaieb@33154 ` 2025` ```next ``` chaieb@33154 ` 2026` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2027` ``` assume h: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56198 ` 2028` ``` from isnonconstant_pnormal_iff[OF assms, of bs] h ``` wenzelm@56066 ` 2029` ``` have pn: "pnormal ?p" ``` wenzelm@56066 ` 2030` ``` by blast ``` wenzelm@56009 ` 2031` ``` { ``` wenzelm@56009 ` 2032` ``` fix x ``` wenzelm@56009 ` 2033` ``` assume H: "?p = [x]" ``` wenzelm@56009 ` 2034` ``` from H have "length (coefficients p) = 1" ``` wenzelm@56009 ` 2035` ``` unfolding polypoly_def by auto ``` wenzelm@56198 ` 2036` ``` with isnonconstant_coefficients_length[OF assms] ``` wenzelm@56198 ` 2037` ``` have False by arith ``` wenzelm@56009 ` 2038` ``` } ``` wenzelm@56009 ` 2039` ``` then show "nonconstant ?p" ``` wenzelm@56009 ` 2040` ``` using pn unfolding nonconstant_def by blast ``` chaieb@33154 ` 2041` ```qed ``` chaieb@33154 ` 2042` wenzelm@56066 ` 2043` ```lemma pnormal_length: "p \ [] \ pnormal p \ length (pnormalize p) = length p" ``` wenzelm@52658 ` 2044` ``` apply (induct p) ``` wenzelm@52658 ` 2045` ``` apply (simp_all add: pnormal_def) ``` wenzelm@52658 ` 2046` ``` apply (case_tac "p = []") ``` wenzelm@52658 ` 2047` ``` apply simp_all ``` wenzelm@52658 ` 2048` ``` done ``` chaieb@33154 ` 2049` wenzelm@52658 ` 2050` ```lemma degree_degree: ``` wenzelm@52658 ` 2051` ``` assumes inc: "isnonconstant p" ``` chaieb@33154 ` 2052` ``` shows "degree p = Polynomial_List.degree (polypoly bs p) \ \head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` chaieb@33154 ` 2053` ```proof ``` wenzelm@52803 ` 2054` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2055` ``` assume H: "degree p = Polynomial_List.degree ?p" ``` chaieb@33154 ` 2056` ``` from isnonconstant_coefficients_length[OF inc] have pz: "?p \ []" ``` chaieb@33154 ` 2057` ``` unfolding polypoly_def by auto ``` chaieb@33154 ` 2058` ``` from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc] ``` wenzelm@56066 ` 2059` ``` have lg: "length (pnormalize ?p) = length ?p" ``` chaieb@33154 ` 2060` ``` unfolding Polynomial_List.degree_def polypoly_def by simp ``` wenzelm@56066 ` 2061` ``` then have "pnormal ?p" ``` wenzelm@56066 ` 2062` ``` using pnormal_length[OF pz] by blast ``` wenzelm@56066 ` 2063` ``` with isnonconstant_pnormal_iff[OF inc] show "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56066 ` 2064` ``` by blast ``` chaieb@33154 ` 2065` ```next ``` wenzelm@56066 ` 2066` ``` let ?p = "polypoly bs p" ``` chaieb@33154 ` 2067` ``` assume H: "\head p\\<^sub>p\<^bsup>bs\<^esup> \ 0" ``` wenzelm@56066 ` 2068` ``` with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" ``` wenzelm@56066 ` 2069` ``` by blast ``` chaieb@33154 ` 2070` ``` with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc] ``` wenzelm@52803 ` 2071` ``` show "degree p = Polynomial_List.degree ?p" ``` chaieb@33154 ` 2072` ``` unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto ``` chaieb@33154 ` 2073` ```qed ``` chaieb@33154 ` 2074` wenzelm@52658 ` 2075` wenzelm@52803 ` 2076` ```section {* Swaps ; Division by a certain variable *} ``` wenzelm@52658 ` 2077` wenzelm@56066 ` 2078` ```primrec swap :: "nat \ nat \ poly \ poly" ``` wenzelm@56066 ` 2079` ```where ``` chaieb@33154 ` 2080` ``` "swap n m (C x) = C x" ``` wenzelm@56198 ` 2081` ```| "swap n m (Bound k) = Bound (if k = n then m else if k = m then n else k)" ``` haftmann@39246 ` 2082` ```| "swap n m (Neg t) = Neg (swap n m t)" ``` haftmann@39246 ` 2083` ```| "swap n m (Add s t) = Add (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2084` ```| "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2085` ```| "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)" ``` haftmann@39246 ` 2086` ```| "swap n m (Pw t k) = Pw (swap n m t) k" ``` wenzelm@56066 ` 2087` ```| "swap n m (CN c k p) = CN (swap n m c) (if k = n then m else if k=m then n else k) (swap n m p)" ``` chaieb@33154 ` 2088` wenzelm@52658 ` 2089` ```lemma swap: ``` wenzelm@56066 ` 2090` ``` assumes "n < length bs" ``` wenzelm@56066 ` 2091` ``` and "m < length bs" ``` chaieb@33154 ` 2092` ``` shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" ``` chaieb@33154 ` 2093` ```proof (induct t) ``` wenzelm@52658 ` 2094` ``` case (Bound k) ``` wenzelm@56066 ` 2095` ``` then show ?case ``` wenzelm@56066 ` 2096` ``` using assms by simp ``` chaieb@33154 ` 2097` ```next ``` wenzelm@52658 ` 2098` ``` case (CN c k p) ``` wenzelm@56066 ` 2099` ``` then show ?case ``` wenzelm@56066 ` 2100` ``` using assms by simp ``` chaieb@33154 ` 2101` ```qed simp_all ``` chaieb@33154 ` 2102` wenzelm@52658 ` 2103` ```lemma swap_swap_id [simp]: "swap n m (swap m n t) = t" ``` wenzelm@52658 ` 2104` ``` by (induct t) simp_all ``` wenzelm@52658 ` 2105` wenzelm@52658 ` 2106` ```lemma swap_commute: "swap n m p = swap m n p" ``` wenzelm@52658 ` 2107` ``` by (induct p) simp_all ``` chaieb@33154 ` 2108` chaieb@33154 ` 2109` ```lemma swap_same_id[simp]: "swap n n t = t" ``` wenzelm@52658 ` 2110` ``` by (induct t) simp_all ``` chaieb@33154 ` 2111` chaieb@33154 ` 2112` ```definition "swapnorm n m t = polynate (swap n m t)" ``` chaieb@33154 ` 2113` wenzelm@52658 ` 2114` ```lemma swapnorm: ``` wenzelm@52658 ` 2115` ``` assumes nbs: "n < length bs" ``` wenzelm@52658 ` 2116` ``` and mbs: "m < length bs" ``` wenzelm@56000 ` 2117` ``` shows "((Ipoly bs (swapnorm n m t) :: 'a::{field_char_0,field_inverse_zero})) = ``` wenzelm@52658 ` 2118` ``` Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" ``` wenzelm@41807 ` 2119` ``` using swap[OF assms] swapnorm_def by simp ``` chaieb@33154 ` 2120` wenzelm@52658 ` 2121` ```lemma swapnorm_isnpoly [simp]: ``` wenzelm@56000 ` 2122` ``` assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" ``` chaieb@33154 ` 2123` ``` shows "isnpoly (swapnorm n m p)" ``` chaieb@33154 ` 2124` ``` unfolding swapnorm_def by simp ``` chaieb@33154 ` 2125` wenzelm@52803 ` 2126` ```definition "polydivideby n s p = ``` wenzelm@56000 ` 2127` ``` (let ``` wenzelm@56000 ` 2128` ``` ss = swapnorm 0 n s; ``` wenzelm@56000 ` 2129` ``` sp = swapnorm 0 n p; ``` wenzelm@56000 ` 2130` ``` h = head sp; ``` wenzelm@56000 ` 2131` ``` (k, r) = polydivide ss sp ``` wenzelm@56000 ` 2132` ``` in (k, swapnorm 0 n h, swapnorm 0 n r))" ``` chaieb@33154 ` 2133` wenzelm@56000 ` 2134` ```lemma swap_nz [simp]: "swap n m p = 0\<^sub>p \ p = 0\<^sub>p" ``` wenzelm@52658 ` 2135` ``` by (induct p) simp_all ``` chaieb@33154 ` 2136` krauss@41808 ` 2137` ```fun isweaknpoly :: "poly \ bool" ``` krauss@41808 ` 2138` ```where ``` chaieb@33154 ` 2139` ``` "isweaknpoly (C c) = True" ``` krauss@41808 ` 2140` ```| "isweaknpoly (CN c n p) \ isweaknpoly c \ isweaknpoly p" ``` krauss@41808 ` 2141` ```| "isweaknpoly p = False" ``` chaieb@33154 ` 2142` wenzelm@52803 ` 2143` ```lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \ isweaknpoly p" ``` wenzelm@52658 ` 2144` ``` by (induct p arbitrary: n0) auto ``` chaieb@33154 ` 2145` wenzelm@52803 ` 2146` ```lemma swap_isweanpoly: "isweaknpoly p \ isweaknpoly (swap n m p)" ``` wenzelm@52658 ` 2147` ``` by (induct p) auto ``` chaieb@33154 ` 2148` chaieb@33154 ` 2149` `end`