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