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