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