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