src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
author chaieb
Sun Oct 25 08:57:36 2009 +0100 (2009-10-25)
changeset 33154 daa6ddece9f0
child 33268 02de0317f66f
permissions -rw-r--r--
Multivariate polynomials library over fields
     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 n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)
   991   fix n p n0
   992   assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>
   993     (\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p"
   994     and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p"
   995   {assume nz: "n = 0"
   996     then obtain c where "p = C c" using n np by (cases p, auto)
   997     with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   998   moreover
   999   {assume nz: "n \<noteq> 0"
  1000     let ?h = "head p"
  1001     let ?hd = "decrpoly ?h"
  1002     let ?ihd = "maxindex ?hd"
  1003     from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" 
  1004       by simp_all
  1005     hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
  1006     
  1007     from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
  1008     have mihn: "maxindex ?h \<le> n" unfolding n by auto
  1009     with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < n" by auto
  1010     {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
  1011       let ?ts = "take ?ihd bs"
  1012       let ?rs = "drop ?ihd bs"
  1013       have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
  1014       have bs_ts_eq: "?ts@ ?rs = bs" by simp
  1015       from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
  1016       from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp
  1017       with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast
  1018       hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp
  1019       with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
  1020       hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
  1021       with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
  1022       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
  1023       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
  1024       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
  1025 	thm poly_zero
  1026 	using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
  1027       with coefficients_head[of p, symmetric]
  1028       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
  1029       from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
  1030       with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp
  1031       with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
  1032     then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
  1033     
  1034     from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
  1035     hence "?h = 0\<^sub>p" by simp
  1036     with head_nz[OF np] have "p = 0\<^sub>p" by simp}
  1037   ultimately show "p = 0\<^sub>p" by blast
  1038 qed
  1039 
  1040 lemma isnpolyh_unique:  
  1041   assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1042   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"
  1043 proof(auto)
  1044   assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
  1045   hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
  1046   hence "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" 
  1047     using wf_bs_polysub[where p=p and q=q] by auto
  1048   with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
  1049   show "p = q" by blast
  1050 qed
  1051 
  1052 
  1053 text{* consequenses of unicity on the algorithms for polynomial normalization *}
  1054 
  1055 lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1056   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
  1057   using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
  1058 
  1059 lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
  1060 lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
  1061 lemma polyadd_0[simp]: 
  1062   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1063   and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
  1064   using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
  1065     isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
  1066 
  1067 lemma polymul_1[simp]: 
  1068     assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1069   and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
  1070   using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
  1071     isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
  1072 lemma polymul_0[simp]: 
  1073   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1074   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"
  1075   using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
  1076     isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
  1077 
  1078 lemma polymul_commute: 
  1079     assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1080   and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1081   shows "p *\<^sub>p q = q *\<^sub>p p"
  1082 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
  1083 
  1084 declare polyneg_polyneg[simp]
  1085   
  1086 lemma isnpolyh_polynate_id[simp]: 
  1087   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1088   and np:"isnpolyh p n0" shows "polynate p = p"
  1089   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
  1090 
  1091 lemma polynate_idempotent[simp]: 
  1092     assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1093   shows "polynate (polynate p) = polynate p"
  1094   using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
  1095 
  1096 lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
  1097   unfolding poly_nate_def polypoly'_def ..
  1098 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>)"
  1099   using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
  1100   unfolding poly_nate_polypoly' by (auto intro: ext)
  1101 
  1102 subsection{* heads, degrees and all that *}
  1103 lemma degree_eq_degreen0: "degree p = degreen p 0"
  1104   by (induct p rule: degree.induct, simp_all)
  1105 
  1106 lemma degree_polyneg: assumes n: "isnpolyh p n"
  1107   shows "degree (polyneg p) = degree p"
  1108   using n
  1109   by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
  1110 
  1111 lemma degree_polyadd:
  1112   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1113   shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
  1114 using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
  1115 
  1116 
  1117 lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1118   shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
  1119 proof-
  1120   from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
  1121   from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])
  1122 qed
  1123 
  1124 lemma degree_polysub_samehead: 
  1125   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1126   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
  1127   and d: "degree p = degree q"
  1128   shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
  1129 unfolding polysub_def split_def fst_conv snd_conv
  1130 using np nq h d
  1131 proof(induct p q rule:polyadd.induct)
  1132   case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
  1133 next
  1134   case (2 a b c' n' p') 
  1135   let ?c = "(a,b)"
  1136   from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
  1137   hence nz:"n' > 0" by (cases n', auto)
  1138   hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
  1139   with prems show ?case by simp
  1140 next
  1141   case (3 c n p a' b') 
  1142   let ?c' = "(a',b')"
  1143   from prems have "degree (C ?c') = degree (CN c n p)" by simp
  1144   hence nz:"n > 0" by (cases n, auto)
  1145   hence "head (CN c n p) = CN c n p" by (cases n, auto)
  1146   with prems show ?case by simp
  1147 next
  1148   case (4 c n p c' n' p')
  1149   hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
  1150     "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+
  1151   hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all  
  1152   hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" 
  1153     using H(1-2) degree_polyneg by auto
  1154   from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"  by simp+
  1155   from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"  by simp
  1156   from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto
  1157   have "n = n' \<or> n < n' \<or> n > n'" by arith
  1158   moreover
  1159   {assume nn': "n = n'"
  1160     have "n = 0 \<or> n >0" by arith
  1161     moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
  1162     moreover {assume nz: "n > 0"
  1163       with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
  1164       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)}
  1165     ultimately have ?case by blast}
  1166   moreover
  1167   {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
  1168     hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
  1169     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)
  1170     hence "n > 0" by (cases n, simp_all)
  1171     hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
  1172     from H(3) headcnp headcnp' nn' have ?case by auto}
  1173   moreover
  1174   {assume nn': "n > n'"  hence np: "n > 0" by simp 
  1175     hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
  1176     from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
  1177     from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
  1178     with degcnpeq have "n' > 0" by (cases n', simp_all)
  1179     hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
  1180     from H(3) headcnp headcnp' nn' have ?case by auto}
  1181   ultimately show ?case  by blast
  1182 qed auto 
  1183  
  1184 lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
  1185 by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
  1186 
  1187 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
  1188 proof(induct k arbitrary: n0 p)
  1189   case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
  1190   with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
  1191     and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
  1192   thus ?case by simp
  1193 qed auto  
  1194 
  1195 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
  1196   by (simp add: shift1_def)
  1197 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
  1198   by (induct k arbitrary: p, auto simp add: shift1_degree)
  1199 
  1200 lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
  1201   by (induct n arbitrary: p, simp_all add: funpow_def)
  1202 
  1203 lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
  1204   by (induct p arbitrary: n rule: degree.induct, auto)
  1205 lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"
  1206   by (induct p arbitrary: n rule: degreen.induct, auto)
  1207 lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"
  1208   by (induct p arbitrary: n rule: degree.induct, auto)
  1209 lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p"
  1210   by (induct p rule: head.induct, auto)
  1211 
  1212 lemma polyadd_eq_const_degree: 
  1213   "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
  1214   using polyadd_eq_const_degreen degree_eq_degreen0 by simp
  1215 
  1216 lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1217   and deg: "degree p \<noteq> degree q"
  1218   shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
  1219 using np nq deg
  1220 apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)
  1221 apply (case_tac n', simp, simp)
  1222 apply (case_tac n, simp, simp)
  1223 apply (case_tac n, case_tac n', simp add: Let_def)
  1224 apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
  1225 apply (clarsimp simp add: polyadd_eq_const_degree)
  1226 apply clarsimp
  1227 apply (erule_tac impE,blast)
  1228 apply (erule_tac impE,blast)
  1229 apply clarsimp
  1230 apply simp
  1231 apply (case_tac n', simp_all)
  1232 done
  1233 
  1234 lemma polymul_head_polyeq: 
  1235    assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1236   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"
  1237 proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
  1238   case (2 a b c' n' p' n0 n1)
  1239   hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
  1240   thus ?case using prems by (cases n', auto) 
  1241 next 
  1242   case (3 c n p a' b' n0 n1) 
  1243   hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
  1244   thus ?case using prems by (cases n, auto)
  1245 next
  1246   case (4 c n p c' n' p' n0 n1)
  1247   hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
  1248     "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
  1249     by simp_all
  1250   have "n < n' \<or> n' < n \<or> n = n'" by arith
  1251   moreover 
  1252   {assume nn': "n < n'" hence ?case 
  1253       thm prems
  1254       using norm 
  1255     prems(6)[rule_format, OF nn' norm(1,6)]
  1256     prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
  1257   moreover {assume nn': "n'< n"
  1258     hence stupid: "n' < n \<and> \<not> n < n'" by simp
  1259     hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
  1260       prems(5)[rule_format, OF stupid norm(5,4)] 
  1261       by (simp,cases n',simp,cases n,auto)}
  1262   moreover {assume nn': "n' = n"
  1263     hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
  1264     from nn' polymul_normh[OF norm(5,4)] 
  1265     have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
  1266     from nn' polymul_normh[OF norm(5,3)] norm 
  1267     have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp
  1268     from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)
  1269     have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
  1270     from polyadd_normh[OF ncnpc' ncnpp0'] 
  1271     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" 
  1272       by (simp add: min_def)
  1273     {assume np: "n > 0"
  1274       with nn' head_isnpolyh_Suc'[OF np nth]
  1275 	head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
  1276       have ?case by simp}
  1277     moreover
  1278     {moreover assume nz: "n = 0"
  1279       from polymul_degreen[OF norm(5,4), where m="0"]
  1280 	polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
  1281       norm(5,6) degree_npolyhCN[OF norm(6)]
  1282     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
  1283     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
  1284     from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
  1285     have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
  1286 	prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
  1287     ultimately have ?case by (cases n) auto} 
  1288   ultimately show ?case by blast
  1289 qed simp_all
  1290 
  1291 lemma degree_coefficients: "degree p = length (coefficients p) - 1"
  1292   by(induct p rule: degree.induct, auto)
  1293 
  1294 lemma degree_head[simp]: "degree (head p) = 0"
  1295   by (induct p rule: head.induct, auto)
  1296 
  1297 lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"
  1298   by (cases n, simp_all)
  1299 lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
  1300   by (cases n, simp_all)
  1301 
  1302 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)"
  1303   using polyadd_different_degreen degree_eq_degreen0 by simp
  1304 
  1305 lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
  1306   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
  1307 
  1308 lemma degree_polymul:
  1309   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1310   and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1311   shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
  1312   using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
  1313 
  1314 lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
  1315   by (induct p arbitrary: n rule: degree.induct, auto)
  1316 
  1317 lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
  1318   by (induct p arbitrary: n rule: degree.induct, auto)
  1319 
  1320 subsection {* Correctness of polynomial pseudo division *}
  1321 
  1322 lemma polydivide_aux_real_domintros:
  1323   assumes call1: "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a = head s\<rbrakk> 
  1324   \<Longrightarrow> polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
  1325   and call2 : "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a \<noteq> head s\<rbrakk> 
  1326   \<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))"
  1327   shows "polydivide_aux_dom (a, n, p, k, s)"
  1328 proof (rule accpI, erule polydivide_aux_rel.cases)
  1329   fix y aa ka na pa sa x xa xb
  1330   assume eqs: "y = (aa, na, pa, ka, sa -\<^sub>p xb)" "(a, n, p, k, s) = (aa, na, pa, ka, sa)"
  1331      and \<Gamma>1': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na" 
  1332     "xb = funpow (xa - na) shift1 pa" "aa = x"
  1333 
  1334   hence \<Gamma>1: "s \<noteq> 0\<^sub>p" "a = head s" "xa = degree s" "\<not> degree s < n" "\<not> xa < na" 
  1335     "xb = funpow (xa - na) shift1 pa" "aa = x" by auto
  1336 
  1337   with call1 have "polydivide_aux_dom (a, n, p, k, s -\<^sub>p funpow (degree s - n) shift1 p)"
  1338     by auto
  1339   with eqs \<Gamma>1 show "polydivide_aux_dom y" by auto
  1340 next
  1341   fix y aa ka na pa sa x xa xb
  1342   assume eqs: "y = (aa, na, pa, Suc ka, aa *\<^sub>p sa -\<^sub>p (x *\<^sub>p xb))" 
  1343     "(a, n, p, k, s) =(aa, na, pa, ka, sa)"
  1344     and \<Gamma>2': "sa \<noteq> 0\<^sub>p" "x = head sa" "xa = degree sa" "\<not> xa < na"
  1345     "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x"
  1346   hence \<Gamma>2: "s \<noteq> 0\<^sub>p" "a \<noteq> head s" "xa = degree s" "\<not> degree s < n"
  1347     "xb = funpow (xa - na) shift1 pa" "aa \<noteq> x" by auto
  1348   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
  1349   with eqs \<Gamma>2'  show "polydivide_aux_dom y" by auto
  1350 qed
  1351 
  1352 lemma polydivide_aux_properties:
  1353   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1354   and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
  1355   and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
  1356   shows "polydivide_aux_dom (a,n,p,k,s) \<and> 
  1357   (polydivide_aux (a,n,p,k,s) = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
  1358           \<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)))"
  1359   using ns
  1360 proof(induct d\<equiv>"degree s" arbitrary: s k k' r n1 rule: nat_less_induct)
  1361   fix d s k k' r n1
  1362   let ?D = "polydivide_aux_dom"
  1363   let ?dths = "?D (a, n, p, k, s)"
  1364   let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
  1365   let ?qrths = "polydivide_aux (a, n, p, k, s) = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) 
  1366     \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
  1367   let ?ths = "?dths \<and> ?qrths"
  1368   let ?b = "head s"
  1369   let ?p' = "funpow (d - n) shift1 p"
  1370   let ?xdn = "funpow (d - n) shift1 1\<^sub>p"
  1371   let ?akk' = "a ^\<^sub>p (k' - k)"
  1372   assume H: "\<forall>m<d. \<forall>x xa xb xc xd.
  1373     isnpolyh x xd \<longrightarrow>
  1374     m = degree x \<longrightarrow> ?D (a, n, p, xa, x) \<and>
  1375     (polydivide_aux (a, n, p, xa, x) = (xb, xc) \<longrightarrow>
  1376     xa \<le> xb \<and> (degree xc = 0 \<or> degree xc < degree p) \<and> 
  1377     (\<exists> nr. isnpolyh xc nr) \<and>
  1378     (\<exists>q n1. isnpolyh q n1 \<and> a ^\<^sub>p xb - xa *\<^sub>p x = p *\<^sub>p q +\<^sub>p xc))"
  1379     and ns: "isnpolyh s n1" and ds: "d = degree s"
  1380   from np have np0: "isnpolyh p 0" 
  1381     using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
  1382   have np': "isnpolyh ?p' 0" using funpow_shift1_isnpoly[OF np0[simplified isnpoly_def[symmetric]] pnz, where n="d -n"] isnpoly_def by simp
  1383   have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
  1384   from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
  1385   from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
  1386   have nakk':"isnpolyh ?akk' 0" by blast
  1387   {assume sz: "s = 0\<^sub>p"
  1388     hence dom: ?dths apply - apply (rule polydivide_aux_real_domintros) apply simp_all done
  1389     from polydivide_aux.psimps[OF dom] sz
  1390     have ?qrths using np apply clarsimp by (rule exI[where x="0\<^sub>p"], simp)
  1391     hence ?ths using dom by blast}
  1392   moreover
  1393   {assume sz: "s \<noteq> 0\<^sub>p"
  1394     {assume dn: "d < n"
  1395       with sz ds  have dom:"?dths" by - (rule polydivide_aux_real_domintros,simp_all) 
  1396       from polydivide_aux.psimps[OF dom] sz dn ds
  1397       have "?qrths" using ns ndp np by auto (rule exI[where x="0\<^sub>p"],simp)
  1398       with dom have ?ths by blast}
  1399     moreover 
  1400     {assume dn': "\<not> d < n" hence dn: "d \<ge> n" by arith
  1401       have degsp': "degree s = degree ?p'" 
  1402 	using ds dn ndp funpow_shift1_degree[where k = "d - n" and p="p"] by simp
  1403       {assume ba: "?b = a"
  1404 	hence headsp': "head s = head ?p'" using ap headp' by simp
  1405 	have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
  1406 	from ds degree_polysub_samehead[OF ns np' headsp' degsp']
  1407 	have "degree (s -\<^sub>p ?p') < d \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
  1408 	moreover 
  1409 	{assume deglt:"degree (s -\<^sub>p ?p') < d"
  1410 	  from  H[rule_format, OF deglt nr,simplified] 
  1411 	  have domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" by blast 
  1412 	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
  1413 	    using ba ds dn' domsp by simp_all
  1414 	  from polydivide_aux.psimps[OF dom] sz dn' ba ds
  1415 	  have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
  1416 	    by (simp add: Let_def)
  1417 	  {assume h1: "polydivide_aux (a, n, p, k, s) = (k', r)"
  1418 	    from H[rule_format, OF deglt nr, where xa = "k" and xb="k'" and xc="r", simplified]
  1419 	      trans[OF eq[symmetric] h1]
  1420 	    have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
  1421 	      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
  1422 	    from q1 obtain q n1 where nq: "isnpolyh q n1" 
  1423 	      and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
  1424 	    from nr obtain nr where nr': "isnpolyh r nr" by blast
  1425 	    from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
  1426 	    from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
  1427 	    have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
  1428 	    from polyadd_normh[OF polymul_normh[OF np 
  1429 	      polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
  1430 	    have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
  1431 	    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')) = 
  1432 	      Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
  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 (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
  1435 	      by (simp add: ring_simps)
  1436 	    hence " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1437 	      Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p *\<^sub>p p) 
  1438 	      + Ipoly bs p * Ipoly bs q + Ipoly bs r"
  1439 	      by (auto simp only: funpow_shift1_1) 
  1440 	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1441 	      Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (d - n) shift1 1\<^sub>p) 
  1442 	      + Ipoly bs q) + Ipoly bs r" by (simp add: ring_simps)
  1443 	    hence "\<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1444 	      Ipoly bs (p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r)" by simp
  1445 	    with isnpolyh_unique[OF nakks' nqr']
  1446 	    have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
  1447 	      p *\<^sub>p ((a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q) +\<^sub>p r" by blast
  1448 	    hence ?qths using nq'
  1449 	      apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (d - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
  1450 	      apply (rule_tac x="0" in exI) by simp
  1451 	    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"
  1452 	      by blast } hence ?qrths by blast
  1453 	  with dom have ?ths by blast} 
  1454 	moreover 
  1455 	{assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
  1456 	  hence domsp: "?D (a, n, p, k, s -\<^sub>p ?p')" 
  1457 	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
  1458 	  have dom: ?dths apply (rule polydivide_aux_real_domintros) 
  1459 	    using ba ds dn' domsp by simp_all
  1460 	  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}"]
  1461 	  have " \<forall>(bs:: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs s = Ipoly bs ?p'" by simp
  1462 	  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
  1463 	    by (simp only: funpow_shift1_1) simp
  1464 	  hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
  1465 	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k',r)"
  1466 	    from polydivide_aux.psimps[OF dom] sz dn' ba ds
  1467 	    have eq: "polydivide_aux (a,n,p,k,s) = polydivide_aux (a,n,p,k, s -\<^sub>p ?p')"
  1468 	      by (simp add: Let_def)
  1469 	    also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.psimps[OF domsp] spz by simp
  1470 	    finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
  1471 	    with sp' ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
  1472 	      polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?qrths
  1473 	      apply auto
  1474 	      apply (rule exI[where x="?xdn"]) 	      
  1475 	      apply auto
  1476 	      apply (rule polymul_commute)
  1477 	      apply simp_all
  1478 	      done}
  1479 	  with dom have ?ths by blast}
  1480 	ultimately have ?ths by blast }
  1481       moreover
  1482       {assume ba: "?b \<noteq> a"
  1483 	from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
  1484 	  polymul_normh[OF head_isnpolyh[OF ns] np']]
  1485 	have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
  1486 	have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
  1487 	  using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
  1488 	    polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
  1489 	    funpow_shift1_nz[OF pnz] by simp_all
  1490 	from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
  1491 	  polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="d - n"]
  1492 	have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
  1493 	  using head_head[OF ns] funpow_shift1_head[OF np pnz]
  1494 	    polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
  1495 	  by (simp add: ap)
  1496 	from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
  1497 	  head_nz[OF np] pnz sz ap[symmetric]
  1498 	  funpow_shift1_nz[OF pnz, where n="d - n"]
  1499 	  polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
  1500 	  ndp ds[symmetric] dn
  1501 	have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
  1502 	  by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
  1503 	{assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < d"
  1504 	  have th: "?D (a, n, p, Suc k, (a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p'))"
  1505 	    using H[rule_format, OF dth nth, simplified] by blast 
  1506 	  have dom: ?dths
  1507 	    using ba ds dn' th apply simp apply (rule polydivide_aux_real_domintros)  
  1508 	    using ba ds dn'  by simp_all
  1509 	  from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
  1510 	  ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
  1511 	  {assume h1:"polydivide_aux (a,n,p,k,s) = (k', r)"
  1512 	    from h1  polydivide_aux.psimps[OF dom] sz dn' ba ds
  1513 	    have eq:"polydivide_aux (a,n,p,Suc k,(a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
  1514 	      by (simp add: Let_def)
  1515 	    with H[rule_format, OF dth nasbp', simplified, where xa="Suc k" and xb="k'" and xc="r"]
  1516 	    obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
  1517 	      and dr: "degree r = 0 \<or> degree r < degree p"
  1518 	      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
  1519 	    from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
  1520 	    {fix bs:: "'a::{ring_char_0,division_by_zero,field} list"
  1521 	      
  1522 	    from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
  1523 	    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
  1524 	    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"
  1525 	      by (simp add: ring_simps power_Suc)
  1526 	    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"
  1527 	      by (simp add:kk'' funpow_shift1_1[where n="d - n" and p="p"])
  1528 	    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"
  1529 	      by (simp add: ring_simps)}
  1530 	    hence ieq:"\<forall>(bs :: 'a::{ring_char_0,division_by_zero,field} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1531 	      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 
  1532 	    let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
  1533 	    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]]
  1534 	    have nqw: "isnpolyh ?q 0" by simp
  1535 	    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]]
  1536 	    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
  1537 	    from dr kk' nr h1 asth nqw have ?qrths apply simp
  1538 	      apply (rule conjI)
  1539 	      apply (rule exI[where x="nr"], simp)
  1540 	      apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
  1541 	      apply (rule exI[where x="0"], simp)
  1542 	      done}
  1543 	  hence ?qrths by blast
  1544 	  with dom have ?ths by blast}
  1545 	moreover 
  1546 	{assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
  1547 	  hence domsp: "?D (a, n, p, Suc k, a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p'))" 
  1548 	    apply (simp) by (rule polydivide_aux_real_domintros, simp_all)
  1549 	  have dom: ?dths using sz ba dn' ds domsp 
  1550 	    by - (rule polydivide_aux_real_domintros, simp_all)
  1551 	  {fix bs :: "'a::{ring_char_0,division_by_zero,field} list"
  1552 	    from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
  1553 	  have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
  1554 	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
  1555 	    by (simp add: funpow_shift1_1[where n="d - n" and p="p"])
  1556 	  hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
  1557 	}
  1558 	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))" ..
  1559 	  from hth
  1560 	  have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
  1561 	    using isnpolyh_unique[where ?'a = "'a::{ring_char_0,division_by_zero,field}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
  1562                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
  1563 	      simplified ap] by simp
  1564 	  {assume h1: "polydivide_aux (a,n,p,k,s) = (k', r)"
  1565 	  from h1 sz ds ba dn' spz polydivide_aux.psimps[OF dom] polydivide_aux.psimps[OF domsp] 
  1566 	  have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
  1567 	  with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
  1568 	    polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
  1569 	  have ?qrths apply (clarsimp simp add: Let_def)
  1570 	    apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
  1571 	    apply (rule exI[where x="0"], simp)
  1572 	    done}
  1573 	hence ?qrths by blast
  1574 	with dom have ?ths by blast}
  1575 	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"]
  1576 	  head_nz[OF np] pnz sz ap[symmetric] ds[symmetric] 
  1577 	  by (simp add: degree_eq_degreen0[symmetric]) blast }
  1578       ultimately have ?ths by blast
  1579     }
  1580     ultimately have ?ths by blast}
  1581   ultimately show ?ths by blast
  1582 qed
  1583 
  1584 lemma polydivide_properties: 
  1585   assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1586   and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
  1587   shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p) 
  1588   \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
  1589 proof-
  1590   have trv: "head p = head p" "degree p = degree p" by simp_all
  1591   from polydivide_aux_properties[OF np ns trv pnz, where k="0"] 
  1592   have d: "polydivide_aux_dom (head p, degree p, p, 0, s)" by blast
  1593   from polydivide_def[where s="s" and p="p"] polydivide_aux.psimps[OF d]
  1594   have ex: "\<exists> k r. polydivide s p = (k,r)" by auto
  1595   then obtain k r where kr: "polydivide s p = (k,r)" by blast
  1596   from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s" and p="p"], symmetric] kr]
  1597     polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
  1598   have "(degree r = 0 \<or> degree r < degree p) \<and>
  1599    (\<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
  1600   with kr show ?thesis 
  1601     apply -
  1602     apply (rule exI[where x="k"])
  1603     apply (rule exI[where x="r"])
  1604     apply simp
  1605     done
  1606 qed
  1607 
  1608 subsection{* More about polypoly and pnormal etc *}
  1609 
  1610 definition "isnonconstant p = (\<not> isconstant p)"
  1611 
  1612 lemma last_map: "xs \<noteq> [] ==> last (map f xs) = f (last xs)" by (induct xs, auto)
  1613 
  1614 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" 
  1615   shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" 
  1616 proof
  1617   let ?p = "polypoly bs p"  
  1618   assume H: "pnormal ?p"
  1619   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  1620   
  1621   from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]  
  1622     pnormal_last_nonzero[OF H]
  1623   show "Ipoly bs (head p) \<noteq> 0" by (simp add: polypoly_def)
  1624 next
  1625   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1626   let ?p = "polypoly bs p"
  1627   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  1628   hence pz: "?p \<noteq> []" by (simp add: polypoly_def) 
  1629   hence lg: "length ?p > 0" by simp
  1630   from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] 
  1631   have lz: "last ?p \<noteq> 0" by (simp add: polypoly_def)
  1632   from pnormal_last_length[OF lg lz] show "pnormal ?p" .
  1633 qed
  1634 
  1635 lemma isnonconstant_coefficients_length: "isnonconstant p \<Longrightarrow> length (coefficients p) > 1"
  1636   unfolding isnonconstant_def
  1637   apply (cases p, simp_all)
  1638   apply (case_tac nat, auto)
  1639   done
  1640 lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p"
  1641   shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
  1642 proof
  1643   let ?p = "polypoly bs p"
  1644   assume nc: "nonconstant ?p"
  1645   from isnonconstant_pnormal_iff[OF inc, of bs] nc
  1646   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" unfolding nonconstant_def by blast
  1647 next
  1648   let ?p = "polypoly bs p"
  1649   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1650   from isnonconstant_pnormal_iff[OF inc, of bs] h
  1651   have pn: "pnormal ?p" by blast
  1652   {fix x assume H: "?p = [x]" 
  1653     from H have "length (coefficients p) = 1" unfolding polypoly_def by auto
  1654     with isnonconstant_coefficients_length[OF inc] have False by arith}
  1655   thus "nonconstant ?p" using pn unfolding nonconstant_def by blast  
  1656 qed
  1657 
  1658 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
  1659   unfolding pnormal_def
  1660  apply (induct p rule: pnormalize.induct, simp_all)
  1661  apply (case_tac "p=[]", simp_all)
  1662  done
  1663 
  1664 lemma degree_degree: assumes inc: "isnonconstant p"
  1665   shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1666 proof
  1667   let  ?p = "polypoly bs p"
  1668   assume H: "degree p = Polynomial_List.degree ?p"
  1669   from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
  1670     unfolding polypoly_def by auto
  1671   from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
  1672   have lg:"length (pnormalize ?p) = length ?p"
  1673     unfolding Polynomial_List.degree_def polypoly_def by simp
  1674   hence "pnormal ?p" using pnormal_length[OF pz] by blast 
  1675   with isnonconstant_pnormal_iff[OF inc]  
  1676   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" by blast
  1677 next
  1678   let  ?p = "polypoly bs p"  
  1679   assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1680   with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" by blast
  1681   with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
  1682   show "degree p = Polynomial_List.degree ?p" 
  1683     unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
  1684 qed
  1685 
  1686 section{* Swaps ; Division by a certain variable *}
  1687 consts swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly"
  1688 primrec
  1689   "swap n m (C x) = C x"
  1690   "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
  1691   "swap n m (Neg t) = Neg (swap n m t)"
  1692   "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
  1693   "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
  1694   "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
  1695   "swap n m (Pw t k) = Pw (swap n m t) k"
  1696   "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)
  1697   (swap n m p)"
  1698 
  1699 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
  1700   shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  1701 proof (induct t)
  1702   case (Bound k) thus ?case using nbs mbs by simp 
  1703 next
  1704   case (CN c k p) thus ?case using nbs mbs by simp 
  1705 qed simp_all
  1706 lemma swap_swap_id[simp]: "swap n m (swap m n t) = t"
  1707   by (induct t,simp_all)
  1708 
  1709 lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all)
  1710 
  1711 lemma swap_same_id[simp]: "swap n n t = t"
  1712   by (induct t, simp_all)
  1713 
  1714 definition "swapnorm n m t = polynate (swap n m t)"
  1715 
  1716 lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
  1717   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"
  1718   using swap[OF prems] swapnorm_def by simp
  1719 
  1720 lemma swapnorm_isnpoly[simp]: 
  1721     assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"
  1722   shows "isnpoly (swapnorm n m p)"
  1723   unfolding swapnorm_def by simp
  1724 
  1725 definition "polydivideby n s p = 
  1726     (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
  1727      in (k,swapnorm 0 n h,swapnorm 0 n r))"
  1728 
  1729 lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
  1730 
  1731 consts isweaknpoly :: "poly \<Rightarrow> bool"
  1732 recdef isweaknpoly "measure size"
  1733   "isweaknpoly (C c) = True"
  1734   "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
  1735   "isweaknpoly p = False"	
  1736 
  1737 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
  1738   by (induct p arbitrary: n0, auto)
  1739 
  1740 lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
  1741   by (induct p, auto)
  1742 
  1743 end