src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 41404 aae9f912cca8
child 41763 8ce56536fda7
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     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 "~~/src/HOL/Library/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 partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> 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 
   209 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
   210   "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
   211 
   212 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
   213   "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
   214 | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
   215 
   216 fun poly_deriv :: "poly \<Rightarrow> poly" where
   217   "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
   218 | "poly_deriv p = 0\<^sub>p"
   219 
   220   (* Verification *)
   221 lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
   222 using Nat.gr0_conv_Suc
   223 by clarsimp
   224 
   225 subsection{* Semantics of the polynomial representation *}
   226 
   227 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
   228   "Ipoly bs (C c) = INum c"
   229 | "Ipoly bs (Bound n) = bs!n"
   230 | "Ipoly bs (Neg a) = - Ipoly bs a"
   231 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   232 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   233 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   234 | "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   235 | "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   236 
   237 abbreviation
   238   Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   239   where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
   240 
   241 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
   242   by (simp add: INum_def)
   243 lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" 
   244   by (simp  add: INum_def)
   245 
   246 lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
   247 
   248 subsection {* Normal form and normalization *}
   249 
   250 consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   251 recdef isnpolyh "measure size"
   252   "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
   253   "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))"
   254   "isnpolyh p = (\<lambda>k. False)"
   255 
   256 lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
   257 by (induct p rule: isnpolyh.induct, auto)
   258 
   259 definition isnpoly :: "poly \<Rightarrow> bool" where
   260   "isnpoly p \<equiv> isnpolyh p 0"
   261 
   262 text{* polyadd preserves normal forms *}
   263 
   264 lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> 
   265       \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
   266 proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
   267   case (2 a b c' n' p' n0 n1)
   268   from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
   269   from prems(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   270   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
   271   with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
   272   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   273   thus ?case using prems th3 by simp
   274 next
   275   case (3 c' n' p' a b n1 n0)
   276   from prems have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
   277   from prems(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   278   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
   279   with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
   280   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   281   thus ?case using prems th3 by simp
   282 next
   283   case (4 c n p c' n' p' n0 n1)
   284   hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
   285   from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
   286   from prems have ngen0: "n \<ge> n0" by simp
   287   from prems have n'gen1: "n' \<ge> n1" by simp 
   288   have "n < n' \<or> n' < n \<or> n = n'" by auto
   289   moreover {assume eq: "n = n'" hence eq': "\<not> n' < n \<and> \<not> n < n'" by simp
   290     with prems(2)[rule_format, OF eq' nc nc'] 
   291     have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
   292     hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
   293       using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
   294     from eq prems(1)[rule_format, OF eq' np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
   295     have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
   296     from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
   297   moreover {assume lt: "n < n'"
   298     have "min n0 n1 \<le> n0" by simp
   299     with prems have th1:"min n0 n1 \<le> n" by auto 
   300     from prems have th21: "isnpolyh c (Suc n)" by simp
   301     from prems have th22: "isnpolyh (CN c' n' p') n'" by simp
   302     from lt have th23: "min (Suc n) n' = Suc n" by arith
   303     from prems(4)[rule_format, OF lt th21 th22]
   304     have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
   305     with prems th1 have ?case by simp } 
   306   moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
   307     have "min n0 n1 \<le> n1"  by simp
   308     with prems have th1:"min n0 n1 \<le> n'" by auto
   309     from prems have th21: "isnpolyh c' (Suc n')" by simp_all
   310     from prems have th22: "isnpolyh (CN c n p) n" by simp
   311     from gt have th23: "min n (Suc n') = Suc n'" by arith
   312     from prems(3)[rule_format, OF  gt' th22 th21]
   313     have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
   314     with prems th1 have ?case by simp}
   315       ultimately show ?case by blast
   316 qed auto
   317 
   318 lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
   319 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
   320 
   321 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
   322   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   323 
   324 text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
   325 
   326 lemma polyadd_different_degreen: 
   327   "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 
   328   degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
   329 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
   330   case (4 c n p c' n' p' m n0 n1)
   331   thus ?case 
   332     apply (cases "n' < n", simp_all add: Let_def)
   333     apply (cases "n = n'", simp_all)
   334     apply (cases "n' = m", simp_all add: Let_def)
   335     by (erule allE[where x="m"], erule allE[where x="Suc m"], 
   336            erule allE[where x="m"], erule allE[where x="Suc m"], 
   337            clarsimp,erule allE[where x="m"],erule allE[where x="Suc m"], simp)
   338 qed simp_all 
   339 
   340 lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
   341   by (induct p arbitrary: n rule: headn.induct, auto)
   342 lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
   343   by (induct p arbitrary: n rule: degree.induct, auto)
   344 lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
   345   by (induct p arbitrary: n rule: degreen.induct, auto)
   346 
   347 lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
   348   by (induct p arbitrary: n rule: degree.induct, auto)
   349 
   350 lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
   351   using degree_isnpolyh_Suc by auto
   352 lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"
   353   using degreen_0 by auto
   354 
   355 
   356 lemma degreen_polyadd:
   357   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1"
   358   shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
   359   using np nq m
   360 proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
   361   case (2 c c' n' p' n0 n1) thus ?case  by (cases n', simp_all)
   362 next
   363   case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
   364 next
   365   case (4 c n p c' n' p' n0 n1 m) 
   366   thus ?case 
   367     apply (cases "n < n'", simp_all add: Let_def)
   368     apply (cases "n' < n", simp_all)
   369     apply (erule allE[where x="n"],erule allE[where x="Suc n"],clarify)
   370     apply (erule allE[where x="n'"],erule allE[where x="Suc n'"],clarify)
   371     by (erule allE[where x="m"],erule allE[where x="m"], auto)
   372 qed auto
   373 
   374 
   375 lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> 
   376   \<Longrightarrow> degreen p m = degreen q m"
   377 proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   378   case (4 c n p c' n' p' m n0 n1 x) 
   379   hence z: "CN c n p +\<^sub>p CN c' n' p' = C x" by simp
   380   {assume nn': "n' < n" hence ?case using prems by simp}
   381   moreover 
   382   {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
   383     moreover {assume "n < n'" with prems have ?case by simp }
   384     moreover {assume eq: "n = n'" hence ?case using prems 
   385         by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }
   386     ultimately have ?case by blast}
   387   ultimately show ?case by blast
   388 qed simp_all
   389 
   390 lemma polymul_properties:
   391   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   392   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
   393   shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
   394   and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
   395   and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 
   396                              else degreen p m + degreen q m)"
   397   using np nq m
   398 proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
   399   case (2 a b c' n' p') 
   400   let ?c = "(a,b)"
   401   { case (1 n0 n1) 
   402     hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c" 
   403       "isnpolyh (CN c' n' p') n1"
   404       by simp_all
   405     {assume "?c = 0\<^sub>N" hence ?case by auto}
   406       moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 
   407         from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
   408           "2.hyps"(2)[rule_format, where x="Suc n'" 
   409           and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
   410           by (auto simp add: min_def)}
   411       ultimately show ?case by blast
   412   next
   413     case (2 n0 n1) thus ?case by auto 
   414   next
   415     case (3 n0 n1) thus ?case  using "2.hyps" by auto } 
   416 next
   417   case (3 c n p a b){
   418     let ?c' = "(a,b)"
   419     case (1 n0 n1) 
   420     hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'" 
   421       "isnpolyh (CN c n p) n0"
   422       by simp_all
   423     {assume "?c' = 0\<^sub>N" hence ?case by auto}
   424       moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
   425         from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
   426           "3.hyps"(2)[rule_format, where x="Suc n" 
   427           and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
   428           by (auto simp add: min_def)}
   429       ultimately show ?case by blast
   430   next
   431     case (2 n0 n1) thus ?case apply auto done
   432   next
   433     case (3 n0 n1) thus ?case  using "3.hyps" by auto } 
   434 next
   435   case (4 c n p c' n' p')
   436   let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
   437     {fix n0 n1
   438       assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
   439       hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
   440         and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
   441         and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
   442         and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
   443         by simp_all
   444       have "n < n' \<or> n' < n \<or> n' = n" by auto
   445       moreover
   446       {assume nn': "n < n'"
   447         with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
   448           "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
   449         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   450           by (simp add: min_def) }
   451       moreover
   452 
   453       {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
   454         with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
   455           "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
   456           nn' nn0 nn1 cnp'
   457         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   458           by (cases "Suc n' = n", simp_all add: min_def)}
   459       moreover
   460       {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
   461         from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
   462           "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
   463         
   464         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   465           by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
   466       ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
   467     note th = this
   468     {fix n0 n1 m
   469       assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
   470       and m: "m \<le> min n0 n1"
   471       let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
   472       let ?d1 = "degreen ?cnp m"
   473       let ?d2 = "degreen ?cnp' m"
   474       let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
   475       have "n'<n \<or> n < n' \<or> n' = n" by auto
   476       moreover 
   477       {assume "n' < n \<or> n < n'"
   478         with "4.hyps" np np' m 
   479         have ?eq apply (cases "n' < n", simp_all)
   480         apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
   481         done }
   482       moreover
   483       {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
   484         from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
   485           "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
   486           np np' nn'
   487         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   488           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   489           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   490           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   491         {assume mn: "m = n" 
   492           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   493             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
   494           have degs:  "degreen (?cnp *\<^sub>p c') n = 
   495             (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   496             "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   497           from degs norm
   498           have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
   499           hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   500             by simp
   501           have nmin: "n \<le> min n n" by (simp add: min_def)
   502           from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   503           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 
   504           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   505             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
   506             mn norm m nn' deg
   507           have ?eq by simp}
   508         moreover
   509         {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
   510           from nn' m np have max1: "m \<le> max n n"  by simp 
   511           hence min1: "m \<le> min n n" by simp     
   512           hence min2: "m \<le> min n (Suc n)" by simp
   513           {assume "c' = 0\<^sub>p"
   514             from `c' = 0\<^sub>p` have ?eq
   515               using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   516             "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
   517               apply simp
   518               done}
   519           moreover
   520           {assume cnz: "c' \<noteq> 0\<^sub>p"
   521             from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   522               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   523               degreen_polyadd[OF norm(3,6) max1]
   524 
   525             have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   526               \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   527               using mn nn' cnz np np' by simp
   528             with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   529               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   530               degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
   531           ultimately have ?eq by blast }
   532         ultimately have ?eq by blast}
   533       ultimately show ?eq by blast}
   534     note degth = this
   535     { case (2 n0 n1)
   536       hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 
   537         and m: "m \<le> min n0 n1" by simp_all
   538       hence mn: "m \<le> n" by simp
   539       let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   540       {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   541         hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   542         from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
   543           "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
   544           np np' C(2) mn
   545         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   546           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   547           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   548           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
   549           "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   550             "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   551           by (simp_all add: min_def)
   552             
   553           from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   554           have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
   555             using norm by simp
   556         from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
   557         have "False" by simp }
   558       thus ?case using "4.hyps" by clarsimp}
   559 qed auto
   560 
   561 lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
   562 by(induct p q rule: polymul.induct, auto simp add: field_simps)
   563 
   564 lemma polymul_normh: 
   565     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   566   shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   567   using polymul_properties(1)  by blast
   568 lemma polymul_eq0_iff: 
   569   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   570   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) "
   571   using polymul_properties(2)  by blast
   572 lemma polymul_degreen:  
   573   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   574   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)"
   575   using polymul_properties(3) by blast
   576 lemma polymul_norm:   
   577   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   578   shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
   579   using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   580 
   581 lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
   582   by (induct p arbitrary: n0 rule: headconst.induct, auto)
   583 
   584 lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"
   585   by (induct p arbitrary: n0, auto)
   586 
   587 lemma monic_eqI: assumes np: "isnpolyh p n0" 
   588   shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
   589   unfolding monic_def Let_def
   590 proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   591   let ?h = "headconst p"
   592   assume pz: "p \<noteq> 0\<^sub>p"
   593   {assume hz: "INum ?h = (0::'a)"
   594     from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
   595     from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
   596     with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
   597   thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
   598 qed
   599 
   600 
   601 text{* polyneg is a negation and preserves normal forms *}
   602 
   603 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
   604 by (induct p rule: polyneg.induct, auto)
   605 
   606 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
   607   by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
   608 lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
   609   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   610 lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
   611 by (induct p rule: polyneg.induct, auto simp add: polyneg0)
   612 
   613 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
   614   using isnpoly_def polyneg_normh by simp
   615 
   616 
   617 text{* polysub is a substraction and preserves normal forms *}
   618 
   619 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
   620 by (simp add: polysub_def polyneg polyadd)
   621 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
   622 by (simp add: polysub_def polyneg_normh polyadd_normh)
   623 
   624 lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
   625   using polyadd_norm polyneg_norm by (simp add: polysub_def) 
   626 lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   627   shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
   628 unfolding polysub_def split_def fst_conv snd_conv
   629 by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
   630 
   631 lemma polysub_0: 
   632   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   633   shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   634   unfolding polysub_def split_def fst_conv snd_conv
   635   apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])
   636   apply (clarsimp simp add: Let_def)
   637   apply (case_tac "n < n'", simp_all)
   638   apply (case_tac "n' < n", simp_all)
   639   apply (erule impE)+
   640   apply (rule_tac x="Suc n" in exI, simp)
   641   apply (rule_tac x="n" in exI, simp)
   642   apply (erule impE)+
   643   apply (rule_tac x="n" in exI, simp)
   644   apply (rule_tac x="Suc n" in exI, simp)
   645   apply (erule impE)+
   646   apply (rule_tac x="Suc n" in exI, simp)
   647   apply (rule_tac x="n" in exI, simp)
   648   apply (erule impE)+
   649   apply (rule_tac x="Suc n" in exI, simp)
   650   apply clarsimp
   651   done
   652 
   653 text{* polypow is a power function and preserves normal forms *}
   654 
   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{* Miscellaneous 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 wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
   846   unfolding wf_bs_def by (induct p, auto simp add: nth_append)
   847 
   848 lemma take_maxindex_wf: assumes wf: "wf_bs bs p" 
   849   shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
   850 proof-
   851   let ?ip = "maxindex p"
   852   let ?tbs = "take ?ip bs"
   853   from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp
   854   hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by  simp
   855   have eq: "bs = ?tbs @ (drop ?ip bs)" by simp
   856   from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp
   857 qed
   858 
   859 lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   860   by (induct p, auto)
   861 
   862 lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   863   unfolding wf_bs_def by simp
   864 
   865 lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
   866   unfolding wf_bs_def by simp
   867 
   868 
   869 
   870 lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
   871 by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)
   872 lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
   873   by (induct p rule: coefficients.induct, simp_all)
   874 
   875 
   876 lemma coefficients_head: "last (coefficients p) = head p"
   877   by (induct p rule: coefficients.induct, auto)
   878 
   879 lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
   880   unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)
   881 
   882 lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
   883   apply (rule exI[where x="replicate (n - length xs) z"])
   884   by simp
   885 lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   886 by (cases p, auto) (case_tac "nat", simp_all)
   887 
   888 lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
   889   unfolding wf_bs_def 
   890   apply (induct p q rule: polyadd.induct)
   891   apply (auto simp add: Let_def)
   892   done
   893 
   894 lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
   895 
   896  unfolding wf_bs_def 
   897   apply (induct p q arbitrary: bs rule: polymul.induct) 
   898   apply (simp_all add: wf_bs_polyadd)
   899   apply clarsimp
   900   apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])
   901   apply auto
   902   done
   903 
   904 lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
   905   unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)
   906 
   907 lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
   908   unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
   909 
   910 subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
   911 
   912 definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
   913 definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)"
   914 definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))"
   915 
   916 lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
   917 proof (induct p arbitrary: n0 rule: coefficients.induct)
   918   case (1 c p n0)
   919   have cp: "isnpolyh (CN c 0 p) n0" by fact
   920   hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
   921     by (auto simp add: isnpolyh_mono[where n'=0])
   922   from "1.hyps"[OF norm(2)] norm(1) norm(4)  show ?case by simp 
   923 qed auto
   924 
   925 lemma coefficients_isconst:
   926   "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
   927   by (induct p arbitrary: n rule: coefficients.induct, 
   928     auto simp add: isnpolyh_Suc_const)
   929 
   930 lemma polypoly_polypoly':
   931   assumes np: "isnpolyh p n0"
   932   shows "polypoly (x#bs) p = polypoly' bs p"
   933 proof-
   934   let ?cf = "set (coefficients p)"
   935   from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
   936   {fix q assume q: "q \<in> ?cf"
   937     from q cn_norm have th: "isnpolyh q n0" by blast
   938     from coefficients_isconst[OF np] q have "isconstant q" by blast
   939     with isconstant_polybound0[OF th] have "polybound0 q" by blast}
   940   hence "\<forall>q \<in> ?cf. polybound0 q" ..
   941   hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
   942     using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
   943     by auto
   944   
   945   thus ?thesis unfolding polypoly_def polypoly'_def by simp 
   946 qed
   947 
   948 lemma polypoly_poly:
   949   assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
   950   using np 
   951 by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)
   952 
   953 lemma polypoly'_poly: 
   954   assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
   955   using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
   956 
   957 
   958 lemma polypoly_poly_polybound0:
   959   assumes np: "isnpolyh p n0" and nb: "polybound0 p"
   960   shows "polypoly bs p = [Ipoly bs p]"
   961   using np nb unfolding polypoly_def 
   962   by (cases p, auto, case_tac nat, auto)
   963 
   964 lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 
   965   by (induct p rule: head.induct, auto)
   966 
   967 lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
   968   by (cases p,auto)
   969 
   970 lemma head_eq_headn0: "head p = headn p 0"
   971   by (induct p rule: head.induct, simp_all)
   972 
   973 lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
   974   by (simp add: head_eq_headn0)
   975 
   976 lemma isnpolyh_zero_iff: 
   977   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})"
   978   shows "p = 0\<^sub>p"
   979 using nq eq
   980 proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   981   case less
   982   note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
   983   {assume nz: "maxindex p = 0"
   984     then obtain c where "p = C c" using np by (cases p, auto)
   985     with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   986   moreover
   987   {assume nz: "maxindex p \<noteq> 0"
   988     let ?h = "head p"
   989     let ?hd = "decrpoly ?h"
   990     let ?ihd = "maxindex ?hd"
   991     from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" 
   992       by simp_all
   993     hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
   994     
   995     from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
   996     have mihn: "maxindex ?h \<le> maxindex p" by auto
   997     with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
   998     {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
   999       let ?ts = "take ?ihd bs"
  1000       let ?rs = "drop ?ihd bs"
  1001       have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
  1002       have bs_ts_eq: "?ts@ ?rs = bs" by simp
  1003       from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
  1004       from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
  1005       with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
  1006       hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
  1007       with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
  1008       hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
  1009       with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
  1010       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
  1011       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
  1012       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
  1013         using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
  1014       with coefficients_head[of p, symmetric]
  1015       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
  1016       from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
  1017       with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp
  1018       with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
  1019     then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
  1020     
  1021     from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
  1022     hence "?h = 0\<^sub>p" by simp
  1023     with head_nz[OF np] have "p = 0\<^sub>p" by simp}
  1024   ultimately show "p = 0\<^sub>p" by blast
  1025 qed
  1026 
  1027 lemma isnpolyh_unique:  
  1028   assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1029   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"
  1030 proof(auto)
  1031   assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
  1032   hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
  1033   hence "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" 
  1034     using wf_bs_polysub[where p=p and q=q] by auto
  1035   with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
  1036   show "p = q" by blast
  1037 qed
  1038 
  1039 
  1040 text{* consequences of unicity on the algorithms for polynomial normalization *}
  1041 
  1042 lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1043   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
  1044   using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
  1045 
  1046 lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
  1047 lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
  1048 lemma polyadd_0[simp]: 
  1049   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1050   and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
  1051   using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
  1052     isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
  1053 
  1054 lemma polymul_1[simp]: 
  1055     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1056   and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
  1057   using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
  1058     isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
  1059 lemma polymul_0[simp]: 
  1060   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1061   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"
  1062   using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
  1063     isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
  1064 
  1065 lemma polymul_commute: 
  1066     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1067   and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1068   shows "p *\<^sub>p q = q *\<^sub>p p"
  1069 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
  1070 
  1071 declare polyneg_polyneg[simp]
  1072   
  1073 lemma isnpolyh_polynate_id[simp]: 
  1074   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1075   and np:"isnpolyh p n0" shows "polynate p = p"
  1076   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
  1077 
  1078 lemma polynate_idempotent[simp]: 
  1079     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1080   shows "polynate (polynate p) = polynate p"
  1081   using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
  1082 
  1083 lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
  1084   unfolding poly_nate_def polypoly'_def ..
  1085 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>)"
  1086   using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
  1087   unfolding poly_nate_polypoly' by (auto intro: ext)
  1088 
  1089 subsection{* heads, degrees and all that *}
  1090 lemma degree_eq_degreen0: "degree p = degreen p 0"
  1091   by (induct p rule: degree.induct, simp_all)
  1092 
  1093 lemma degree_polyneg: assumes n: "isnpolyh p n"
  1094   shows "degree (polyneg p) = degree p"
  1095   using n
  1096   by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
  1097 
  1098 lemma degree_polyadd:
  1099   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1100   shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
  1101 using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
  1102 
  1103 
  1104 lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1105   shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
  1106 proof-
  1107   from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
  1108   from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])
  1109 qed
  1110 
  1111 lemma degree_polysub_samehead: 
  1112   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1113   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
  1114   and d: "degree p = degree q"
  1115   shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
  1116 unfolding polysub_def split_def fst_conv snd_conv
  1117 using np nq h d
  1118 proof(induct p q rule:polyadd.induct)
  1119   case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
  1120 next
  1121   case (2 a b c' n' p') 
  1122   let ?c = "(a,b)"
  1123   from prems have "degree (C ?c) = degree (CN c' n' p')" by simp
  1124   hence nz:"n' > 0" by (cases n', auto)
  1125   hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
  1126   with prems show ?case by simp
  1127 next
  1128   case (3 c n p a' b') 
  1129   let ?c' = "(a',b')"
  1130   from prems have "degree (C ?c') = degree (CN c n p)" by simp
  1131   hence nz:"n > 0" by (cases n, auto)
  1132   hence "head (CN c n p) = CN c n p" by (cases n, auto)
  1133   with prems show ?case by simp
  1134 next
  1135   case (4 c n p c' n' p')
  1136   hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
  1137     "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+
  1138   hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all  
  1139   hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" 
  1140     using H(1-2) degree_polyneg by auto
  1141   from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"  by simp+
  1142   from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"  by simp
  1143   from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto
  1144   have "n = n' \<or> n < n' \<or> n > n'" by arith
  1145   moreover
  1146   {assume nn': "n = n'"
  1147     have "n = 0 \<or> n >0" by arith
  1148     moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}
  1149     moreover {assume nz: "n > 0"
  1150       with nn' H(3) have  cc':"c = c'" and pp': "p = p'" by (cases n, auto)+
  1151       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)}
  1152     ultimately have ?case by blast}
  1153   moreover
  1154   {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
  1155     hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
  1156     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)
  1157     hence "n > 0" by (cases n, simp_all)
  1158     hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)
  1159     from H(3) headcnp headcnp' nn' have ?case by auto}
  1160   moreover
  1161   {assume nn': "n > n'"  hence np: "n > 0" by simp 
  1162     hence headcnp:"head (CN c n p) = CN c n p"  by (cases n, simp_all)
  1163     from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp
  1164     from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)
  1165     with degcnpeq have "n' > 0" by (cases n', simp_all)
  1166     hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
  1167     from H(3) headcnp headcnp' nn' have ?case by auto}
  1168   ultimately show ?case  by blast
  1169 qed auto 
  1170  
  1171 lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"
  1172 by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)
  1173 
  1174 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"
  1175 proof(induct k arbitrary: n0 p)
  1176   case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)
  1177   with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"
  1178     and "head (shift1 p) = head p" by (simp_all add: shift1_head) 
  1179   thus ?case by (simp add: funpow_swap1)
  1180 qed auto  
  1181 
  1182 lemma shift1_degree: "degree (shift1 p) = 1 + degree p"
  1183   by (simp add: shift1_def)
  1184 lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "
  1185   by (induct k arbitrary: p, auto simp add: shift1_degree)
  1186 
  1187 lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"
  1188   by (induct n arbitrary: p, simp_all add: funpow_def)
  1189 
  1190 lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"
  1191   by (induct p arbitrary: n rule: degree.induct, auto)
  1192 lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"
  1193   by (induct p arbitrary: n rule: degreen.induct, auto)
  1194 lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"
  1195   by (induct p arbitrary: n rule: degree.induct, auto)
  1196 lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p"
  1197   by (induct p rule: head.induct, auto)
  1198 
  1199 lemma polyadd_eq_const_degree: 
  1200   "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
  1201   using polyadd_eq_const_degreen degree_eq_degreen0 by simp
  1202 
  1203 lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1204   and deg: "degree p \<noteq> degree q"
  1205   shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"
  1206 using np nq deg
  1207 apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)
  1208 apply (case_tac n', simp, simp)
  1209 apply (case_tac n, simp, simp)
  1210 apply (case_tac n, case_tac n', simp add: Let_def)
  1211 apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")
  1212 apply (clarsimp simp add: polyadd_eq_const_degree)
  1213 apply clarsimp
  1214 apply (erule_tac impE,blast)
  1215 apply (erule_tac impE,blast)
  1216 apply clarsimp
  1217 apply simp
  1218 apply (case_tac n', simp_all)
  1219 done
  1220 
  1221 lemma polymul_head_polyeq: 
  1222    assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1223   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"
  1224 proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
  1225   case (2 a b c' n' p' n0 n1)
  1226   hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
  1227   thus ?case using prems by (cases n', auto) 
  1228 next 
  1229   case (3 c n p a' b' n0 n1) 
  1230   hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
  1231   thus ?case using prems by (cases n, auto)
  1232 next
  1233   case (4 c n p c' n' p' n0 n1)
  1234   hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
  1235     "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
  1236     by simp_all
  1237   have "n < n' \<or> n' < n \<or> n = n'" by arith
  1238   moreover 
  1239   {assume nn': "n < n'" hence ?case 
  1240       thm prems
  1241       using norm 
  1242     prems(6)[rule_format, OF nn' norm(1,6)]
  1243     prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}
  1244   moreover {assume nn': "n'< n"
  1245     hence stupid: "n' < n \<and> \<not> n < n'" by simp
  1246     hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]
  1247       prems(5)[rule_format, OF stupid norm(5,4)] 
  1248       by (simp,cases n',simp,cases n,auto)}
  1249   moreover {assume nn': "n' = n"
  1250     hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp
  1251     from nn' polymul_normh[OF norm(5,4)] 
  1252     have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)
  1253     from nn' polymul_normh[OF norm(5,3)] norm 
  1254     have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp
  1255     from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)
  1256     have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
  1257     from polyadd_normh[OF ncnpc' ncnpp0'] 
  1258     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" 
  1259       by (simp add: min_def)
  1260     {assume np: "n > 0"
  1261       with nn' head_isnpolyh_Suc'[OF np nth]
  1262         head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]
  1263       have ?case by simp}
  1264     moreover
  1265     {moreover assume nz: "n = 0"
  1266       from polymul_degreen[OF norm(5,4), where m="0"]
  1267         polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0
  1268       norm(5,6) degree_npolyhCN[OF norm(6)]
  1269     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
  1270     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
  1271     from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth
  1272     have ?case   using norm prems(2)[rule_format, OF stupid norm(5,3)]
  1273         prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }
  1274     ultimately have ?case by (cases n) auto} 
  1275   ultimately show ?case by blast
  1276 qed simp_all
  1277 
  1278 lemma degree_coefficients: "degree p = length (coefficients p) - 1"
  1279   by(induct p rule: degree.induct, auto)
  1280 
  1281 lemma degree_head[simp]: "degree (head p) = 0"
  1282   by (induct p rule: head.induct, auto)
  1283 
  1284 lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"
  1285   by (cases n, simp_all)
  1286 lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge>  degree p"
  1287   by (cases n, simp_all)
  1288 
  1289 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)"
  1290   using polyadd_different_degreen degree_eq_degreen0 by simp
  1291 
  1292 lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"
  1293   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
  1294 
  1295 lemma degree_polymul:
  1296   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1297   and np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1298   shows "degree (p *\<^sub>p q) \<le> degree p + degree q"
  1299   using polymul_degreen[OF np nq, where m="0"]  degree_eq_degreen0 by simp
  1300 
  1301 lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"
  1302   by (induct p arbitrary: n rule: degree.induct, auto)
  1303 
  1304 lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"
  1305   by (induct p arbitrary: n rule: degree.induct, auto)
  1306 
  1307 subsection {* Correctness of polynomial pseudo division *}
  1308 
  1309 lemma polydivide_aux_properties:
  1310   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1311   and np: "isnpolyh p n0" and ns: "isnpolyh s n1"
  1312   and ap: "head p = a" and ndp: "degree p = n" and pnz: "p \<noteq> 0\<^sub>p"
  1313   shows "(polydivide_aux a n p k s = (k',r) \<longrightarrow> (k' \<ge> k) \<and> (degree r = 0 \<or> degree r < degree p) 
  1314           \<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)))"
  1315   using ns
  1316 proof(induct "degree s" arbitrary: s k k' r n1 rule: less_induct)
  1317   case less
  1318   let ?qths = "\<exists>q n1. isnpolyh q n1 \<and> (a ^\<^sub>p (k' - k) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)"
  1319   let ?ths = "polydivide_aux a n p k s = (k', r) \<longrightarrow>  k \<le> k' \<and> (degree r = 0 \<or> degree r < degree p) 
  1320     \<and> (\<exists>nr. isnpolyh r nr) \<and> ?qths"
  1321   let ?b = "head s"
  1322   let ?p' = "funpow (degree s - n) shift1 p"
  1323   let ?xdn = "funpow (degree s - n) shift1 1\<^sub>p"
  1324   let ?akk' = "a ^\<^sub>p (k' - k)"
  1325   note ns = `isnpolyh s n1`
  1326   from np have np0: "isnpolyh p 0" 
  1327     using isnpolyh_mono[where n="n0" and n'="0" and p="p"]  by simp
  1328   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
  1329   have headp': "head ?p' = head p" using funpow_shift1_head[OF np pnz] by simp
  1330   from funpow_shift1_isnpoly[where p="1\<^sub>p"] have nxdn: "isnpolyh ?xdn 0" by (simp add: isnpoly_def)
  1331   from polypow_normh [OF head_isnpolyh[OF np0], where k="k' - k"] ap 
  1332   have nakk':"isnpolyh ?akk' 0" by blast
  1333   {assume sz: "s = 0\<^sub>p"
  1334    hence ?ths using np polydivide_aux.simps apply clarsimp by (rule exI[where x="0\<^sub>p"], simp) }
  1335   moreover
  1336   {assume sz: "s \<noteq> 0\<^sub>p"
  1337     {assume dn: "degree s < n"
  1338       hence "?ths" using ns ndp np polydivide_aux.simps by auto (rule exI[where x="0\<^sub>p"],simp) }
  1339     moreover 
  1340     {assume dn': "\<not> degree s < n" hence dn: "degree s \<ge> n" by arith
  1341       have degsp': "degree s = degree ?p'" 
  1342         using dn ndp funpow_shift1_degree[where k = "degree s - n" and p="p"] by simp
  1343       {assume ba: "?b = a"
  1344         hence headsp': "head s = head ?p'" using ap headp' by simp
  1345         have nr: "isnpolyh (s -\<^sub>p ?p') 0" using polysub_normh[OF ns np'] by simp
  1346         from degree_polysub_samehead[OF ns np' headsp' degsp']
  1347         have "degree (s -\<^sub>p ?p') < degree s \<or> s -\<^sub>p ?p' = 0\<^sub>p" by simp
  1348         moreover 
  1349         {assume deglt:"degree (s -\<^sub>p ?p') < degree s"
  1350           from polydivide_aux.simps sz dn' ba
  1351           have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
  1352             by (simp add: Let_def)
  1353           {assume h1: "polydivide_aux a n p k s = (k', r)"
  1354             from less(1)[OF deglt nr, of k k' r]
  1355               trans[OF eq[symmetric] h1]
  1356             have kk': "k \<le> k'" and nr:"\<exists>nr. isnpolyh r nr" and dr: "degree r = 0 \<or> degree r < degree p"
  1357               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
  1358             from q1 obtain q n1 where nq: "isnpolyh q n1" 
  1359               and asp:"a^\<^sub>p (k' - k) *\<^sub>p (s -\<^sub>p ?p') = p *\<^sub>p q +\<^sub>p r"  by blast
  1360             from nr obtain nr where nr': "isnpolyh r nr" by blast
  1361             from polymul_normh[OF nakk' ns] have nakks': "isnpolyh (a ^\<^sub>p (k' - k) *\<^sub>p s) 0" by simp
  1362             from polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]
  1363             have nq': "isnpolyh (?akk' *\<^sub>p ?xdn +\<^sub>p q) 0" by simp
  1364             from polyadd_normh[OF polymul_normh[OF np 
  1365               polyadd_normh[OF polymul_normh[OF nakk' nxdn] nq]] nr']
  1366             have nqr': "isnpolyh (p *\<^sub>p (?akk' *\<^sub>p ?xdn +\<^sub>p q) +\<^sub>p r) 0" by simp 
  1367             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')) = 
  1368               Ipoly bs (p *\<^sub>p q +\<^sub>p r)" by simp
  1369             hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a^\<^sub>p (k' - k)*\<^sub>p s) = 
  1370               Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs ?p' + Ipoly bs p * Ipoly bs q + Ipoly bs r" 
  1371               by (simp add: field_simps)
  1372             hence " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1373               Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p *\<^sub>p p) 
  1374               + Ipoly bs p * Ipoly bs q + Ipoly bs r"
  1375               by (auto simp only: funpow_shift1_1) 
  1376             hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1377               Ipoly bs p * (Ipoly bs (a^\<^sub>p (k' - k)) * Ipoly bs (funpow (degree s - n) shift1 1\<^sub>p) 
  1378               + Ipoly bs q) + Ipoly bs r" by (simp add: field_simps)
  1379             hence "\<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1380               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
  1381             with isnpolyh_unique[OF nakks' nqr']
  1382             have "a ^\<^sub>p (k' - k) *\<^sub>p s = 
  1383               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
  1384             hence ?qths using nq'
  1385               apply (rule_tac x="(a^\<^sub>p (k' - k)) *\<^sub>p (funpow (degree s - n) shift1 1\<^sub>p) +\<^sub>p q" in exI)
  1386               apply (rule_tac x="0" in exI) by simp
  1387             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"
  1388               by blast } hence ?ths by blast }
  1389         moreover 
  1390         {assume spz:"s -\<^sub>p ?p' = 0\<^sub>p"
  1391           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}"]
  1392           have " \<forall>(bs:: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs s = Ipoly bs ?p'" by simp
  1393           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
  1394             by (simp only: funpow_shift1_1) simp
  1395           hence sp': "s = ?xdn *\<^sub>p p" using isnpolyh_unique[OF ns polymul_normh[OF nxdn np]] by blast
  1396           {assume h1: "polydivide_aux a n p k s = (k',r)"
  1397             from polydivide_aux.simps sz dn' ba
  1398             have eq: "polydivide_aux a n p k s = polydivide_aux a n p k (s -\<^sub>p ?p')"
  1399               by (simp add: Let_def)
  1400             also have "\<dots> = (k,0\<^sub>p)" using polydivide_aux.simps spz by simp
  1401             finally have "(k',r) = (k,0\<^sub>p)" using h1 by simp
  1402             with sp'[symmetric] ns np nxdn polyadd_0(1)[OF polymul_normh[OF np nxdn]]
  1403               polyadd_0(2)[OF polymul_normh[OF np nxdn]] have ?ths
  1404               apply auto
  1405               apply (rule exI[where x="?xdn"])        
  1406               apply (auto simp add: polymul_commute[of p])
  1407               done} }
  1408         ultimately have ?ths by blast }
  1409       moreover
  1410       {assume ba: "?b \<noteq> a"
  1411         from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np0, simplified ap] ns] 
  1412           polymul_normh[OF head_isnpolyh[OF ns] np']]
  1413         have nth: "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by(simp add: min_def)
  1414         have nzths: "a *\<^sub>p s \<noteq> 0\<^sub>p" "?b *\<^sub>p ?p' \<noteq> 0\<^sub>p"
  1415           using polymul_eq0_iff[OF head_isnpolyh[OF np0, simplified ap] ns] 
  1416             polymul_eq0_iff[OF head_isnpolyh[OF ns] np']head_nz[OF np0] ap pnz sz head_nz[OF ns]
  1417             funpow_shift1_nz[OF pnz] by simp_all
  1418         from polymul_head_polyeq[OF head_isnpolyh[OF np] ns] head_nz[OF np] sz ap head_head[OF np] pnz
  1419           polymul_head_polyeq[OF head_isnpolyh[OF ns] np'] head_nz [OF ns] sz funpow_shift1_nz[OF pnz, where n="degree s - n"]
  1420         have hdth: "head (a *\<^sub>p s) = head (?b *\<^sub>p ?p')" 
  1421           using head_head[OF ns] funpow_shift1_head[OF np pnz]
  1422             polymul_commute[OF head_isnpolyh[OF np] head_isnpolyh[OF ns]]
  1423           by (simp add: ap)
  1424         from polymul_degreen[OF head_isnpolyh[OF np] ns, where m="0"]
  1425           head_nz[OF np] pnz sz ap[symmetric]
  1426           funpow_shift1_nz[OF pnz, where n="degree s - n"]
  1427           polymul_degreen[OF head_isnpolyh[OF ns] np', where m="0"]  head_nz[OF ns]
  1428           ndp dn
  1429         have degth: "degree (a *\<^sub>p s) = degree (?b *\<^sub>p ?p') "
  1430           by (simp add: degree_eq_degreen0[symmetric] funpow_shift1_degree)
  1431         {assume dth: "degree ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) < degree s"
  1432           from polysub_normh[OF polymul_normh[OF head_isnpolyh[OF np] ns] polymul_normh[OF head_isnpolyh[OF ns]np']]
  1433           ap have nasbp': "isnpolyh ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) 0" by simp
  1434           {assume h1:"polydivide_aux a n p k s = (k', r)"
  1435             from h1 polydivide_aux.simps sz dn' ba
  1436             have eq:"polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (?b *\<^sub>p ?p')) = (k',r)"
  1437               by (simp add: Let_def)
  1438             with less(1)[OF dth nasbp', of "Suc k" k' r]
  1439             obtain q nq nr where kk': "Suc k \<le> k'" and nr: "isnpolyh r nr" and nq: "isnpolyh q nq" 
  1440               and dr: "degree r = 0 \<or> degree r < degree p"
  1441               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
  1442             from kk' have kk'':"Suc (k' - Suc k) = k' - k" by arith
  1443             {fix bs:: "'a::{field_char_0, field_inverse_zero} list"
  1444               
  1445             from qr isnpolyh_unique[OF polypow_normh[OF head_isnpolyh[OF np], where k="k' - Suc k", simplified ap] nasbp', symmetric]
  1446             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
  1447             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"
  1448               by (simp add: field_simps power_Suc)
  1449             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"
  1450               by (simp add:kk'' funpow_shift1_1[where n="degree s - n" and p="p"])
  1451             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"
  1452               by (simp add: field_simps)}
  1453             hence ieq:"\<forall>(bs :: 'a::{field_char_0, field_inverse_zero} list). Ipoly bs (a ^\<^sub>p (k' - k) *\<^sub>p s) = 
  1454               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 
  1455             let ?q = "q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn)"
  1456             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]]
  1457             have nqw: "isnpolyh ?q 0" by simp
  1458             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]]
  1459             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
  1460             from dr kk' nr h1 asth nqw have ?ths apply simp
  1461               apply (rule conjI)
  1462               apply (rule exI[where x="nr"], simp)
  1463               apply (rule exI[where x="(q +\<^sub>p (a ^\<^sub>p (k' - Suc k) *\<^sub>p ?b *\<^sub>p ?xdn))"], simp)
  1464               apply (rule exI[where x="0"], simp)
  1465               done}
  1466           hence ?ths by blast }
  1467         moreover 
  1468         {assume spz: "a *\<^sub>p s -\<^sub>p (?b *\<^sub>p ?p') = 0\<^sub>p"
  1469           {fix bs :: "'a::{field_char_0, field_inverse_zero} list"
  1470             from isnpolyh_unique[OF nth, where ?'a="'a" and q="0\<^sub>p",simplified,symmetric] spz
  1471           have "Ipoly bs (a*\<^sub>p s) = Ipoly bs ?b * Ipoly bs ?p'" by simp
  1472           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (?b *\<^sub>p ?xdn) * Ipoly bs p" 
  1473             by (simp add: funpow_shift1_1[where n="degree s - n" and p="p"])
  1474           hence "Ipoly bs (a*\<^sub>p s) = Ipoly bs (p *\<^sub>p (?b *\<^sub>p ?xdn))" by simp
  1475         }
  1476         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))" ..
  1477           from hth
  1478           have asq: "a *\<^sub>p s = p *\<^sub>p (?b *\<^sub>p ?xdn)" 
  1479             using isnpolyh_unique[where ?'a = "'a::{field_char_0, field_inverse_zero}", OF polymul_normh[OF head_isnpolyh[OF np] ns] 
  1480                     polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]],
  1481               simplified ap] by simp
  1482           {assume h1: "polydivide_aux a n p k s = (k', r)"
  1483           from h1 sz ba dn' spz polydivide_aux.simps polydivide_aux.simps
  1484           have "(k',r) = (Suc k, 0\<^sub>p)" by (simp add: Let_def)
  1485           with h1 np head_isnpolyh[OF np, simplified ap] ns polymul_normh[OF head_isnpolyh[OF ns] nxdn]
  1486             polymul_normh[OF np polymul_normh[OF head_isnpolyh[OF ns] nxdn]] asq
  1487           have ?ths apply (clarsimp simp add: Let_def)
  1488             apply (rule exI[where x="?b *\<^sub>p ?xdn"]) apply simp
  1489             apply (rule exI[where x="0"], simp)
  1490             done}
  1491         hence ?ths by blast}
  1492         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"]
  1493           head_nz[OF np] pnz sz ap[symmetric]
  1494           by (simp add: degree_eq_degreen0[symmetric]) blast }
  1495       ultimately have ?ths by blast
  1496     }
  1497     ultimately have ?ths by blast}
  1498   ultimately show ?ths by blast
  1499 qed
  1500 
  1501 lemma polydivide_properties: 
  1502   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1503   and np: "isnpolyh p n0" and ns: "isnpolyh s n1" and pnz: "p \<noteq> 0\<^sub>p"
  1504   shows "(\<exists> k r. polydivide s p = (k,r) \<and> (\<exists>nr. isnpolyh r nr) \<and> (degree r = 0 \<or> degree r < degree p) 
  1505   \<and> (\<exists>q n1. isnpolyh q n1 \<and> ((polypow k (head p)) *\<^sub>p s = p *\<^sub>p q +\<^sub>p r)))"
  1506 proof-
  1507   have trv: "head p = head p" "degree p = degree p" by simp_all
  1508   from polydivide_def[where s="s" and p="p"] 
  1509   have ex: "\<exists> k r. polydivide s p = (k,r)" by auto
  1510   then obtain k r where kr: "polydivide s p = (k,r)" by blast
  1511   from trans[OF meta_eq_to_obj_eq[OF polydivide_def[where s="s"and p="p"], symmetric] kr]
  1512     polydivide_aux_properties[OF np ns trv pnz, where k="0" and k'="k" and r="r"]
  1513   have "(degree r = 0 \<or> degree r < degree p) \<and>
  1514    (\<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
  1515   with kr show ?thesis 
  1516     apply -
  1517     apply (rule exI[where x="k"])
  1518     apply (rule exI[where x="r"])
  1519     apply simp
  1520     done
  1521 qed
  1522 
  1523 subsection{* More about polypoly and pnormal etc *}
  1524 
  1525 definition "isnonconstant p = (\<not> isconstant p)"
  1526 
  1527 lemma isnonconstant_pnormal_iff: assumes nc: "isnonconstant p" 
  1528   shows "pnormal (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0" 
  1529 proof
  1530   let ?p = "polypoly bs p"  
  1531   assume H: "pnormal ?p"
  1532   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  1533   
  1534   from coefficients_head[of p] last_map[OF csz, of "Ipoly bs"]  
  1535     pnormal_last_nonzero[OF H]
  1536   show "Ipoly bs (head p) \<noteq> 0" by (simp add: polypoly_def)
  1537 next
  1538   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1539   let ?p = "polypoly bs p"
  1540   have csz: "coefficients p \<noteq> []" using nc by (cases p, auto)
  1541   hence pz: "?p \<noteq> []" by (simp add: polypoly_def) 
  1542   hence lg: "length ?p > 0" by simp
  1543   from h coefficients_head[of p] last_map[OF csz, of "Ipoly bs"] 
  1544   have lz: "last ?p \<noteq> 0" by (simp add: polypoly_def)
  1545   from pnormal_last_length[OF lg lz] show "pnormal ?p" .
  1546 qed
  1547 
  1548 lemma isnonconstant_coefficients_length: "isnonconstant p \<Longrightarrow> length (coefficients p) > 1"
  1549   unfolding isnonconstant_def
  1550   apply (cases p, simp_all)
  1551   apply (case_tac nat, auto)
  1552   done
  1553 lemma isnonconstant_nonconstant: assumes inc: "isnonconstant p"
  1554   shows "nonconstant (polypoly bs p) \<longleftrightarrow> Ipoly bs (head p) \<noteq> 0"
  1555 proof
  1556   let ?p = "polypoly bs p"
  1557   assume nc: "nonconstant ?p"
  1558   from isnonconstant_pnormal_iff[OF inc, of bs] nc
  1559   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" unfolding nonconstant_def by blast
  1560 next
  1561   let ?p = "polypoly bs p"
  1562   assume h: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1563   from isnonconstant_pnormal_iff[OF inc, of bs] h
  1564   have pn: "pnormal ?p" by blast
  1565   {fix x assume H: "?p = [x]" 
  1566     from H have "length (coefficients p) = 1" unfolding polypoly_def by auto
  1567     with isnonconstant_coefficients_length[OF inc] have False by arith}
  1568   thus "nonconstant ?p" using pn unfolding nonconstant_def by blast  
  1569 qed
  1570 
  1571 lemma pnormal_length: "p\<noteq>[] \<Longrightarrow> pnormal p \<longleftrightarrow> length (pnormalize p) = length p"
  1572   unfolding pnormal_def
  1573  apply (induct p)
  1574  apply (simp_all, case_tac "p=[]", simp_all)
  1575  done
  1576 
  1577 lemma degree_degree: assumes inc: "isnonconstant p"
  1578   shows "degree p = Polynomial_List.degree (polypoly bs p) \<longleftrightarrow> \<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1579 proof
  1580   let  ?p = "polypoly bs p"
  1581   assume H: "degree p = Polynomial_List.degree ?p"
  1582   from isnonconstant_coefficients_length[OF inc] have pz: "?p \<noteq> []"
  1583     unfolding polypoly_def by auto
  1584   from H degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
  1585   have lg:"length (pnormalize ?p) = length ?p"
  1586     unfolding Polynomial_List.degree_def polypoly_def by simp
  1587   hence "pnormal ?p" using pnormal_length[OF pz] by blast 
  1588   with isnonconstant_pnormal_iff[OF inc]  
  1589   show "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0" by blast
  1590 next
  1591   let  ?p = "polypoly bs p"  
  1592   assume H: "\<lparr>head p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<noteq> 0"
  1593   with isnonconstant_pnormal_iff[OF inc] have "pnormal ?p" by blast
  1594   with degree_coefficients[of p] isnonconstant_coefficients_length[OF inc]
  1595   show "degree p = Polynomial_List.degree ?p" 
  1596     unfolding polypoly_def pnormal_def Polynomial_List.degree_def by auto
  1597 qed
  1598 
  1599 section{* Swaps ; Division by a certain variable *}
  1600 primrec swap:: "nat \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> poly" where
  1601   "swap n m (C x) = C x"
  1602 | "swap n m (Bound k) = Bound (if k = n then m else if k=m then n else k)"
  1603 | "swap n m (Neg t) = Neg (swap n m t)"
  1604 | "swap n m (Add s t) = Add (swap n m s) (swap n m t)"
  1605 | "swap n m (Sub s t) = Sub (swap n m s) (swap n m t)"
  1606 | "swap n m (Mul s t) = Mul (swap n m s) (swap n m t)"
  1607 | "swap n m (Pw t k) = Pw (swap n m t) k"
  1608 | "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)
  1609   (swap n m p)"
  1610 
  1611 lemma swap: assumes nbs: "n < length bs" and mbs: "m < length bs"
  1612   shows "Ipoly bs (swap n m t) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  1613 proof (induct t)
  1614   case (Bound k) thus ?case using nbs mbs by simp 
  1615 next
  1616   case (CN c k p) thus ?case using nbs mbs by simp 
  1617 qed simp_all
  1618 lemma swap_swap_id[simp]: "swap n m (swap m n t) = t"
  1619   by (induct t,simp_all)
  1620 
  1621 lemma swap_commute: "swap n m p = swap m n p" by (induct p, simp_all)
  1622 
  1623 lemma swap_same_id[simp]: "swap n n t = t"
  1624   by (induct t, simp_all)
  1625 
  1626 definition "swapnorm n m t = polynate (swap n m t)"
  1627 
  1628 lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs"
  1629   shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  1630   using swap[OF prems] swapnorm_def by simp
  1631 
  1632 lemma swapnorm_isnpoly[simp]: 
  1633     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1634   shows "isnpoly (swapnorm n m p)"
  1635   unfolding swapnorm_def by simp
  1636 
  1637 definition "polydivideby n s p = 
  1638     (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
  1639      in (k,swapnorm 0 n h,swapnorm 0 n r))"
  1640 
  1641 lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
  1642 
  1643 consts isweaknpoly :: "poly \<Rightarrow> bool"
  1644 recdef isweaknpoly "measure size"
  1645   "isweaknpoly (C c) = True"
  1646   "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
  1647   "isweaknpoly p = False"       
  1648 
  1649 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
  1650   by (induct p arbitrary: n0, auto)
  1651 
  1652 lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
  1653   by (induct p, auto)
  1654 
  1655 end