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