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