src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
author wenzelm
Mon Feb 21 23:47:19 2011 +0100 (2011-02-21)
changeset 41807 ab5d2d81f9fb
parent 41763 8ce56536fda7
child 41816 7a55699805dc
permissions -rw-r--r--
tuned proofs -- eliminated prems;
     1 (*  Title:      HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
     2     Author:     Amine Chaieb
     3 *)
     4 
     5 header {* Implementation and verification of multivariate polynomials *}
     6 
     7 theory Reflected_Multivariate_Polynomial
     8 imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
     9 begin
    10 
    11   (* Implementation *)
    12 
    13 subsection{* Datatype of polynomial expressions *} 
    14 
    15 datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
    16   | Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
    17 
    18 abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
    19 abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
    20 
    21 subsection{* Boundedness, substitution and all that *}
    22 primrec polysize:: "poly \<Rightarrow> nat" where
    23   "polysize (C c) = 1"
    24 | "polysize (Bound n) = 1"
    25 | "polysize (Neg p) = 1 + polysize p"
    26 | "polysize (Add p q) = 1 + polysize p + polysize q"
    27 | "polysize (Sub p q) = 1 + polysize p + polysize q"
    28 | "polysize (Mul p q) = 1 + polysize p + polysize q"
    29 | "polysize (Pw p n) = 1 + polysize p"
    30 | "polysize (CN c n p) = 4 + polysize c + polysize p"
    31 
    32 primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where
    33   "polybound0 (C c) = True"
    34 | "polybound0 (Bound n) = (n>0)"
    35 | "polybound0 (Neg a) = polybound0 a"
    36 | "polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"
    37 | "polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)" 
    38 | "polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"
    39 | "polybound0 (Pw p n) = (polybound0 p)"
    40 | "polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"
    41 
    42 primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *) where
    43   "polysubst0 t (C c) = (C c)"
    44 | "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
    45 | "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
    46 | "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
    47 | "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
    48 | "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
    49 | "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
    50 | "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
    51                              else CN (polysubst0 t c) n (polysubst0 t p))"
    52 
    53 consts 
    54   decrpoly:: "poly \<Rightarrow> poly" 
    55 recdef decrpoly "measure polysize"
    56   "decrpoly (Bound n) = Bound (n - 1)"
    57   "decrpoly (Neg a) = Neg (decrpoly a)"
    58   "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
    59   "decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
    60   "decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
    61   "decrpoly (Pw p n) = Pw (decrpoly p) n"
    62   "decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
    63   "decrpoly a = a"
    64 
    65 subsection{* Degrees and heads and coefficients *}
    66 
    67 consts degree:: "poly \<Rightarrow> nat"
    68 recdef degree "measure size"
    69   "degree (CN c 0 p) = 1 + degree p"
    70   "degree p = 0"
    71 consts head:: "poly \<Rightarrow> poly"
    72 
    73 recdef head "measure size"
    74   "head (CN c 0 p) = head p"
    75   "head p = p"
    76   (* More general notions of degree and head *)
    77 consts degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"
    78 recdef degreen "measure size"
    79   "degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)"
    80   "degreen p = (\<lambda>m. 0)"
    81 
    82 consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"
    83 recdef headn "measure size"
    84   "headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"
    85   "headn p = (\<lambda>m. p)"
    86 
    87 consts coefficients:: "poly \<Rightarrow> poly list"
    88 recdef coefficients "measure size"
    89   "coefficients (CN c 0 p) = c#(coefficients p)"
    90   "coefficients p = [p]"
    91 
    92 consts isconstant:: "poly \<Rightarrow> bool"
    93 recdef isconstant "measure size"
    94   "isconstant (CN c 0 p) = False"
    95   "isconstant p = True"
    96 
    97 consts behead:: "poly \<Rightarrow> poly"
    98 recdef behead "measure size"
    99   "behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
   100   "behead p = 0\<^sub>p"
   101 
   102 consts headconst:: "poly \<Rightarrow> Num"
   103 recdef headconst "measure size"
   104   "headconst (CN c n p) = headconst p"
   105   "headconst (C n) = n"
   106 
   107 subsection{* Operations for normalization *}
   108 consts 
   109   polyadd :: "poly\<times>poly \<Rightarrow> poly"
   110   polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")
   111   polysub :: "poly\<times>poly \<Rightarrow> poly"
   112   polymul :: "poly\<times>poly \<Rightarrow> poly"
   113   polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
   114 abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
   115   where "a +\<^sub>p b \<equiv> polyadd (a,b)"
   116 abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
   117   where "a *\<^sub>p b \<equiv> polymul (a,b)"
   118 abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
   119   where "a -\<^sub>p b \<equiv> polysub (a,b)"
   120 abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
   121   where "a ^\<^sub>p k \<equiv> polypow k a"
   122 
   123 recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
   124   "polyadd (C c, C c') = C (c+\<^sub>Nc')"
   125   "polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
   126   "polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
   127 stupid:  "polyadd (CN c n p, CN c' n' p') = 
   128     (if n < n' then CN (polyadd(c,CN c' n' p')) n p
   129      else if n'<n then CN (polyadd(CN c n p, c')) n' p'
   130      else (let cc' = polyadd (c,c') ; 
   131                pp' = polyadd (p,p')
   132            in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"
   133   "polyadd (a, b) = Add a b"
   134 (hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
   135 
   136 recdef polyneg "measure size"
   137   "polyneg (C c) = C (~\<^sub>N c)"
   138   "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
   139   "polyneg a = Neg a"
   140 
   141 defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"
   142 
   143 recdef polymul "measure (\<lambda>(a,b). size a + size b)"
   144   "polymul(C c, C c') = C (c*\<^sub>Nc')"
   145   "polymul(C c, CN c' n' p') = 
   146       (if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))"
   147   "polymul(CN c n p, C c') = 
   148       (if c' = 0\<^sub>N  then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))"
   149   "polymul(CN c n p, CN c' n' p') = 
   150   (if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))
   151   else if n' < n 
   152   then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))
   153   else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"
   154   "polymul (a,b) = Mul a b"
   155 recdef polypow "measure id"
   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 consts polynate :: "poly \<Rightarrow> poly"
   161 recdef polynate "measure polysize"
   162   "polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
   163   "polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
   164   "polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
   165   "polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
   166   "polynate (Neg p) = (~\<^sub>p (polynate p))"
   167   "polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
   168   "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
   169   "polynate (C c) = C (normNum c)"
   170 
   171 fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where
   172   "poly_cmul y (C x) = C (y *\<^sub>N x)"
   173 | "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
   174 | "poly_cmul y p = C y *\<^sub>p p"
   175 
   176 definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where
   177   "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))"
   178 
   179 subsection{* Pseudo-division *}
   180 
   181 definition shift1 :: "poly \<Rightarrow> poly" where
   182   "shift1 p \<equiv> CN 0\<^sub>p 0 p"
   183 
   184 abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where
   185   "funpow \<equiv> compow"
   186 
   187 partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly"
   188   where
   189   "polydivide_aux a n p k s = 
   190   (if s = 0\<^sub>p then (k,s)
   191   else (let b = head s; m = degree s in
   192   (if m < n then (k,s) else 
   193   (let p'= funpow (m - n) shift1 p in 
   194   (if a = b then polydivide_aux a n p k (s -\<^sub>p p') 
   195   else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
   196 
   197 definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where
   198   "polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s"
   199 
   200 fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where
   201   "poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
   202 | "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
   203 
   204 fun poly_deriv :: "poly \<Rightarrow> poly" where
   205   "poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
   206 | "poly_deriv p = 0\<^sub>p"
   207 
   208   (* Verification *)
   209 lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n - 1)"
   210 using Nat.gr0_conv_Suc
   211 by clarsimp
   212 
   213 subsection{* Semantics of the polynomial representation *}
   214 
   215 primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where
   216   "Ipoly bs (C c) = INum c"
   217 | "Ipoly bs (Bound n) = bs!n"
   218 | "Ipoly bs (Neg a) = - Ipoly bs a"
   219 | "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
   220 | "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
   221 | "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
   222 | "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
   223 | "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
   224 
   225 abbreviation
   226   Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
   227   where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
   228 
   229 lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i" 
   230   by (simp add: INum_def)
   231 lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" 
   232   by (simp  add: INum_def)
   233 
   234 lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
   235 
   236 subsection {* Normal form and normalization *}
   237 
   238 consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"
   239 recdef isnpolyh "measure size"
   240   "isnpolyh (C c) = (\<lambda>k. isnormNum c)"
   241   "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))"
   242   "isnpolyh p = (\<lambda>k. False)"
   243 
   244 lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"
   245 by (induct p rule: isnpolyh.induct, auto)
   246 
   247 definition isnpoly :: "poly \<Rightarrow> bool" where
   248   "isnpoly p \<equiv> isnpolyh p 0"
   249 
   250 text{* polyadd preserves normal forms *}
   251 
   252 lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> 
   253       \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"
   254 proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
   255   case (2 a b c' n' p' n0 n1)
   256   from 2 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
   257   from 2(3) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   258   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
   259   with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
   260   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   261   thus ?case using 2 th3 by simp
   262 next
   263   case (3 c' n' p' a b n1 n0)
   264   from 3 have  th1: "isnpolyh (C (a,b)) (Suc n')" by simp 
   265   from 3(2) have th2: "isnpolyh c' (Suc n')"  and nplen1: "n' \<ge> n1" by simp_all
   266   with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
   267   with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
   268   from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
   269   thus ?case using 3 th3 by simp
   270 next
   271   case (4 c n p c' n' p' n0 n1)
   272   hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
   273   from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 
   274   from 4 have ngen0: "n \<ge> n0" by simp
   275   from 4 have n'gen1: "n' \<ge> n1" by simp 
   276   have "n < n' \<or> n' < n \<or> n = n'" by auto
   277   moreover {assume eq: "n = n'"
   278     with 4(2)[OF nc nc'] 
   279     have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
   280     hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
   281       using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
   282     from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
   283     have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp
   284     from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
   285   moreover {assume lt: "n < n'"
   286     have "min n0 n1 \<le> n0" by simp
   287     with 4 have th1:"min n0 n1 \<le> n" by auto 
   288     from 4 have th21: "isnpolyh c (Suc n)" by simp
   289     from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
   290     from lt have th23: "min (Suc n) n' = Suc n" by arith
   291     from 4(4)[OF th21 th22]
   292     have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
   293     with 4 lt th1 have ?case by simp }
   294   moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp
   295     have "min n0 n1 \<le> n1"  by simp
   296     with 4 have th1:"min n0 n1 \<le> n'" by auto
   297     from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
   298     from 4 have th22: "isnpolyh (CN c n p) n" by simp
   299     from gt have th23: "min n (Suc n') = Suc n'" by arith
   300     from 4(3)[OF th22 th21]
   301     have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
   302     with 4 gt th1 have ?case by simp}
   303       ultimately show ?case by blast
   304 qed auto
   305 
   306 lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
   307 by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
   308 
   309 lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"
   310   using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   311 
   312 text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
   313 
   314 lemma polyadd_different_degreen: 
   315   "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow> 
   316   degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
   317 proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
   318   case (4 c n p c' n' p' m n0 n1)
   319   have "n' = n \<or> n < n' \<or> n' < n" by arith
   320   thus ?case
   321   proof (elim disjE)
   322     assume [simp]: "n' = n"
   323     from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
   324     show ?thesis by (auto simp: Let_def)
   325   next
   326     assume "n < n'"
   327     with 4 show ?thesis by auto
   328   next
   329     assume "n' < n"
   330     with 4 show ?thesis by auto
   331   qed
   332 qed auto
   333 
   334 lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"
   335   by (induct p arbitrary: n rule: headn.induct, auto)
   336 lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"
   337   by (induct p arbitrary: n rule: degree.induct, auto)
   338 lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"
   339   by (induct p arbitrary: n rule: degreen.induct, auto)
   340 
   341 lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"
   342   by (induct p arbitrary: n rule: degree.induct, auto)
   343 
   344 lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"
   345   using degree_isnpolyh_Suc by auto
   346 lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"
   347   using degreen_0 by auto
   348 
   349 
   350 lemma degreen_polyadd:
   351   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1"
   352   shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"
   353   using np nq m
   354 proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
   355   case (2 c c' n' p' n0 n1) thus ?case  by (cases n', simp_all)
   356 next
   357   case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
   358 next
   359   case (4 c n p c' n' p' n0 n1 m) 
   360   have "n' = n \<or> n < n' \<or> n' < n" by arith
   361   thus ?case
   362   proof (elim disjE)
   363     assume [simp]: "n' = n"
   364     from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
   365     show ?thesis by (auto simp: Let_def)
   366   qed simp_all
   367 qed auto
   368 
   369 lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> 
   370   \<Longrightarrow> degreen p m = degreen q m"
   371 proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
   372   case (4 c n p c' n' p' m n0 n1 x) 
   373   {assume nn': "n' < n" hence ?case using 4 by simp}
   374   moreover 
   375   {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith
   376     moreover {assume "n < n'" with 4 have ?case by simp }
   377     moreover {assume eq: "n = n'" hence ?case using 4 
   378         apply (cases "p +\<^sub>p p' = 0\<^sub>p")
   379         apply (auto simp add: Let_def)
   380         apply blast
   381         done
   382       }
   383     ultimately have ?case by blast}
   384   ultimately show ?case by blast
   385 qed simp_all
   386 
   387 lemma polymul_properties:
   388   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   389   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"
   390   shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
   391   and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)" 
   392   and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0 
   393                              else degreen p m + degreen q m)"
   394   using np nq m
   395 proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
   396   case (2 a b c' n' p') 
   397   let ?c = "(a,b)"
   398   { case (1 n0 n1) 
   399     hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c" 
   400       "isnpolyh (CN c' n' p') n1"
   401       by simp_all
   402     {assume "?c = 0\<^sub>N" hence ?case by auto}
   403       moreover {assume cnz: "?c \<noteq> 0\<^sub>N" 
   404         from "2.hyps"(1)[rule_format,where xb="n'",  OF cnz n(1) n(3)] 
   405           "2.hyps"(2)[rule_format, where x="Suc n'" 
   406           and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
   407           by (auto simp add: min_def)}
   408       ultimately show ?case by blast
   409   next
   410     case (2 n0 n1) thus ?case by auto 
   411   next
   412     case (3 n0 n1) thus ?case  using "2.hyps" by auto } 
   413 next
   414   case (3 c n p a b){
   415     let ?c' = "(a,b)"
   416     case (1 n0 n1) 
   417     hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'" 
   418       "isnpolyh (CN c n p) n0"
   419       by simp_all
   420     {assume "?c' = 0\<^sub>N" hence ?case by auto}
   421       moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"
   422         from "3.hyps"(1)[rule_format,where xb="n",  OF cnz n(3) n(1)] 
   423           "3.hyps"(2)[rule_format, where x="Suc n" 
   424           and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
   425           by (auto simp add: min_def)}
   426       ultimately show ?case by blast
   427   next
   428     case (2 n0 n1) thus ?case apply auto done
   429   next
   430     case (3 n0 n1) thus ?case  using "3.hyps" by auto } 
   431 next
   432   case (4 c n p c' n' p')
   433   let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
   434     {fix n0 n1
   435       assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
   436       hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
   437         and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
   438         and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
   439         and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"
   440         by simp_all
   441       have "n < n' \<or> n' < n \<or> n' = n" by auto
   442       moreover
   443       {assume nn': "n < n'"
   444         with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"] 
   445           "4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
   446         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   447           by (simp add: min_def) }
   448       moreover
   449 
   450       {assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith
   451         with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
   452           "4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"] 
   453           nn' nn0 nn1 cnp'
   454         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   455           by (cases "Suc n' = n", simp_all add: min_def)}
   456       moreover
   457       {assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith
   458         from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
   459           "4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
   460         
   461         have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
   462           by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
   463       ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
   464     note th = this
   465     {fix n0 n1 m
   466       assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
   467       and m: "m \<le> min n0 n1"
   468       let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
   469       let ?d1 = "degreen ?cnp m"
   470       let ?d2 = "degreen ?cnp' m"
   471       let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0  else ?d1 + ?d2)"
   472       have "n'<n \<or> n < n' \<or> n' = n" by auto
   473       moreover 
   474       {assume "n' < n \<or> n < n'"
   475         with "4.hyps" np np' m 
   476         have ?eq apply (cases "n' < n", simp_all)
   477         apply (erule allE[where x="n"],erule allE[where x="n"],auto) 
   478         done }
   479       moreover
   480       {assume nn': "n' = n"  hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith
   481         from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
   482           "4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"] 
   483           np np' nn'
   484         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   485           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   486           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   487           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)
   488         {assume mn: "m = n" 
   489           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   490             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
   491           have degs:  "degreen (?cnp *\<^sub>p c') n = 
   492             (if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
   493             "degreen (?cnp *\<^sub>p p') n = ?d1  + degreen p' n" by (simp_all add: min_def)
   494           from degs norm
   495           have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
   496           hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
   497             by simp
   498           have nmin: "n \<le> min n n" by (simp add: min_def)
   499           from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
   500           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 
   501           from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
   502             "4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
   503             mn norm m nn' deg
   504           have ?eq by simp}
   505         moreover
   506         {assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto
   507           from nn' m np have max1: "m \<le> max n n"  by simp 
   508           hence min1: "m \<le> min n n" by simp     
   509           hence min2: "m \<le> min n (Suc n)" by simp
   510           {assume "c' = 0\<^sub>p"
   511             from `c' = 0\<^sub>p` have ?eq
   512               using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   513             "4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
   514               apply simp
   515               done}
   516           moreover
   517           {assume cnz: "c' \<noteq> 0\<^sub>p"
   518             from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   519               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   520               degreen_polyadd[OF norm(3,6) max1]
   521 
   522             have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
   523               \<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
   524               using mn nn' cnz np np' by simp
   525             with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
   526               "4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
   527               degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
   528           ultimately have ?eq by blast }
   529         ultimately have ?eq by blast}
   530       ultimately show ?eq by blast}
   531     note degth = this
   532     { case (2 n0 n1)
   533       hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1" 
   534         and m: "m \<le> min n0 n1" by simp_all
   535       hence mn: "m \<le> n" by simp
   536       let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
   537       {assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
   538         hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp
   539         from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"] 
   540           "4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"] 
   541           np np' C(2) mn
   542         have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
   543           "isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
   544           "(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
   545           "?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
   546           "degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
   547             "degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
   548           by (simp_all add: min_def)
   549             
   550           from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
   551           have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
   552             using norm by simp
   553         from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"]  degneq
   554         have "False" by simp }
   555       thus ?case using "4.hyps" by clarsimp}
   556 qed auto
   557 
   558 lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
   559 by(induct p q rule: polymul.induct, auto simp add: field_simps)
   560 
   561 lemma polymul_normh: 
   562     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   563   shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"
   564   using polymul_properties(1)  by blast
   565 lemma polymul_eq0_iff: 
   566   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   567   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) "
   568   using polymul_properties(2)  by blast
   569 lemma polymul_degreen:  
   570   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   571   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)"
   572   using polymul_properties(3) by blast
   573 lemma polymul_norm:   
   574   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   575   shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"
   576   using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
   577 
   578 lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"
   579   by (induct p arbitrary: n0 rule: headconst.induct, auto)
   580 
   581 lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"
   582   by (induct p arbitrary: n0, auto)
   583 
   584 lemma monic_eqI: assumes np: "isnpolyh p n0" 
   585   shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
   586   unfolding monic_def Let_def
   587 proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
   588   let ?h = "headconst p"
   589   assume pz: "p \<noteq> 0\<^sub>p"
   590   {assume hz: "INum ?h = (0::'a)"
   591     from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
   592     from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
   593     with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
   594   thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
   595 qed
   596 
   597 
   598 text{* polyneg is a negation and preserves normal forms *}
   599 
   600 lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
   601 by (induct p rule: polyneg.induct, auto)
   602 
   603 lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
   604   by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
   605 lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"
   606   by (induct p arbitrary: n0 rule: polyneg.induct, auto)
   607 lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "
   608 by (induct p rule: polyneg.induct, auto simp add: polyneg0)
   609 
   610 lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"
   611   using isnpoly_def polyneg_normh by simp
   612 
   613 
   614 text{* polysub is a substraction and preserves normal forms *}
   615 
   616 lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
   617 by (simp add: polysub_def polyneg polyadd)
   618 lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"
   619 by (simp add: polysub_def polyneg_normh polyadd_normh)
   620 
   621 lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"
   622   using polyadd_norm polyneg_norm by (simp add: polysub_def) 
   623 lemma polysub_same_0[simp]:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   624   shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"
   625 unfolding polysub_def split_def fst_conv snd_conv
   626 by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
   627 
   628 lemma polysub_0: 
   629   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   630   shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
   631   unfolding polysub_def split_def fst_conv snd_conv
   632   by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
   633   (auto simp: Nsub0[simplified Nsub_def] Let_def)
   634 
   635 text{* polypow is a power function and preserves normal forms *}
   636 
   637 lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
   638 proof(induct n rule: polypow.induct)
   639   case 1 thus ?case by simp
   640 next
   641   case (2 n)
   642   let ?q = "polypow ((Suc n) div 2) p"
   643   let ?d = "polymul(?q,?q)"
   644   have "odd (Suc n) \<or> even (Suc n)" by simp
   645   moreover 
   646   {assume odd: "odd (Suc n)"
   647     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
   648     from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def)
   649     also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
   650       using "2.hyps" by simp
   651     also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
   652       apply (simp only: power_add power_one_right) by simp
   653     also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"
   654       by (simp only: th)
   655     finally have ?case 
   656     using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp  }
   657   moreover 
   658   {assume even: "even (Suc n)"
   659     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
   660     from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
   661     also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
   662       using "2.hyps" apply (simp only: power_add) by simp
   663     finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)}
   664   ultimately show ?case by blast
   665 qed
   666 
   667 lemma polypow_normh: 
   668   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   669   shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"
   670 proof (induct k arbitrary: n rule: polypow.induct)
   671   case (2 k n)
   672   let ?q = "polypow (Suc k div 2) p"
   673   let ?d = "polymul (?q,?q)"
   674   from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
   675   from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
   676   from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
   677   from dn on show ?case by (simp add: Let_def)
   678 qed auto 
   679 
   680 lemma polypow_norm:   
   681   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   682   shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"
   683   by (simp add: polypow_normh isnpoly_def)
   684 
   685 text{* Finally the whole normalization *}
   686 
   687 lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
   688 by (induct p rule:polynate.induct, auto)
   689 
   690 lemma polynate_norm[simp]: 
   691   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
   692   shows "isnpoly (polynate p)"
   693   by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
   694 
   695 text{* shift1 *}
   696 
   697 
   698 lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
   699   by (simp add: shift1_def)
   700 
   701 lemma shift1_isnpoly: 
   702   assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "
   703   using pn pnz by (simp add: shift1_def isnpoly_def )
   704 
   705 lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"
   706   by (simp add: shift1_def)
   707 lemma funpow_shift1_isnpoly: 
   708   "\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"
   709   by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
   710 
   711 lemma funpow_isnpolyh: 
   712   assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"
   713   shows "isnpolyh (funpow k f p) n"
   714   using f np by (induct k arbitrary: p, auto)
   715 
   716 lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
   717   by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1)
   718 
   719 lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"
   720   using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
   721 
   722 lemma funpow_shift1_1: 
   723   "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
   724   by (simp add: funpow_shift1)
   725 
   726 lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
   727 by (induct p  arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
   728 
   729 lemma behead:
   730   assumes np: "isnpolyh p n"
   731   shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
   732   using np
   733 proof (induct p arbitrary: n rule: behead.induct)
   734   case (1 c p n) hence pn: "isnpolyh p n" by simp
   735   from 1(1)[OF pn] 
   736   have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 
   737   then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
   738     by (simp_all add: th[symmetric] field_simps)
   739 qed (auto simp add: Let_def)
   740 
   741 lemma behead_isnpolyh:
   742   assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
   743   using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
   744 
   745 subsection{* Miscellaneous lemmas about indexes, decrementation, substitution  etc ... *}
   746 lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"
   747 proof(induct p arbitrary: n rule: poly.induct, auto)
   748   case (goal1 c n p n')
   749   hence "n = Suc (n - 1)" by simp
   750   hence "isnpolyh p (Suc (n - 1))"  using `isnpolyh p n` by simp
   751   with goal1(2) show ?case by simp
   752 qed
   753 
   754 lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"
   755 by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)
   756 
   757 lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto)
   758 
   759 lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0 - 1)"
   760   apply (induct p arbitrary: n0, auto)
   761   apply (atomize)
   762   apply (erule_tac x = "Suc nat" in allE)
   763   apply auto
   764   done
   765 
   766 lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)"
   767  by (induct p  arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)
   768 
   769 lemma polybound0_I:
   770   assumes nb: "polybound0 a"
   771   shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
   772 using nb
   773 by (induct a rule: poly.induct) auto 
   774 lemma polysubst0_I:
   775   shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
   776   by (induct t) simp_all
   777 
   778 lemma polysubst0_I':
   779   assumes nb: "polybound0 a"
   780   shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
   781   by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
   782 
   783 lemma decrpoly: assumes nb: "polybound0 t"
   784   shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
   785   using nb by (induct t rule: decrpoly.induct, simp_all)
   786 
   787 lemma polysubst0_polybound0: assumes nb: "polybound0 t"
   788   shows "polybound0 (polysubst0 t a)"
   789 using nb by (induct a rule: poly.induct, auto)
   790 
   791 lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"
   792   by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
   793 
   794 primrec maxindex :: "poly \<Rightarrow> nat" where
   795   "maxindex (Bound n) = n + 1"
   796 | "maxindex (CN c n p) = max  (n + 1) (max (maxindex c) (maxindex p))"
   797 | "maxindex (Add p q) = max (maxindex p) (maxindex q)"
   798 | "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
   799 | "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
   800 | "maxindex (Neg p) = maxindex p"
   801 | "maxindex (Pw p n) = maxindex p"
   802 | "maxindex (C x) = 0"
   803 
   804 definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where
   805   "wf_bs bs p = (length bs \<ge> maxindex p)"
   806 
   807 lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"
   808 proof(induct p rule: coefficients.induct)
   809   case (1 c p) 
   810   show ?case 
   811   proof
   812     fix x assume xc: "x \<in> set (coefficients (CN c 0 p))"
   813     hence "x = c \<or> x \<in> set (coefficients p)" by simp
   814     moreover 
   815     {assume "x = c" hence "wf_bs bs x" using "1.prems"  unfolding wf_bs_def by simp}
   816     moreover 
   817     {assume H: "x \<in> set (coefficients p)" 
   818       from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp
   819       with "1.hyps" H have "wf_bs bs x" by blast }
   820     ultimately  show "wf_bs bs x" by blast
   821   qed
   822 qed simp_all
   823 
   824 lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"
   825 by (induct p rule: coefficients.induct, auto)
   826 
   827 lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"
   828   unfolding wf_bs_def by (induct p, auto simp add: nth_append)
   829 
   830 lemma take_maxindex_wf: assumes wf: "wf_bs bs p" 
   831   shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"
   832 proof-
   833   let ?ip = "maxindex p"
   834   let ?tbs = "take ?ip bs"
   835   from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp
   836   hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by  simp
   837   have eq: "bs = ?tbs @ (drop ?ip bs)" by simp
   838   from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp
   839 qed
   840 
   841 lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1"
   842   by (induct p) auto
   843 
   844 lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"
   845   unfolding wf_bs_def by simp
   846 
   847 lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"
   848   unfolding wf_bs_def by simp
   849 
   850 
   851 
   852 lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"
   853 by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)
   854 lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"
   855   by (induct p rule: coefficients.induct, simp_all)
   856 
   857 
   858 lemma coefficients_head: "last (coefficients p) = head p"
   859   by (induct p rule: coefficients.induct, auto)
   860 
   861 lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"
   862   unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)
   863 
   864 lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"
   865   apply (rule exI[where x="replicate (n - length xs) z"])
   866   by simp
   867 lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"
   868 by (cases p, auto) (case_tac "nat", simp_all)
   869 
   870 lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"
   871   unfolding wf_bs_def 
   872   apply (induct p q rule: polyadd.induct)
   873   apply (auto simp add: Let_def)
   874   done
   875 
   876 lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"
   877 
   878  unfolding wf_bs_def 
   879   apply (induct p q arbitrary: bs rule: polymul.induct) 
   880   apply (simp_all add: wf_bs_polyadd)
   881   apply clarsimp
   882   apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])
   883   apply auto
   884   done
   885 
   886 lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"
   887   unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)
   888 
   889 lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p -\<^sub>p q)"
   890   unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast
   891 
   892 subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}
   893 
   894 definition "polypoly bs p = map (Ipoly bs) (coefficients p)"
   895 definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)"
   896 definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))"
   897 
   898 lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"
   899 proof (induct p arbitrary: n0 rule: coefficients.induct)
   900   case (1 c p n0)
   901   have cp: "isnpolyh (CN c 0 p) n0" by fact
   902   hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"
   903     by (auto simp add: isnpolyh_mono[where n'=0])
   904   from "1.hyps"[OF norm(2)] norm(1) norm(4)  show ?case by simp 
   905 qed auto
   906 
   907 lemma coefficients_isconst:
   908   "isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"
   909   by (induct p arbitrary: n rule: coefficients.induct, 
   910     auto simp add: isnpolyh_Suc_const)
   911 
   912 lemma polypoly_polypoly':
   913   assumes np: "isnpolyh p n0"
   914   shows "polypoly (x#bs) p = polypoly' bs p"
   915 proof-
   916   let ?cf = "set (coefficients p)"
   917   from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .
   918   {fix q assume q: "q \<in> ?cf"
   919     from q cn_norm have th: "isnpolyh q n0" by blast
   920     from coefficients_isconst[OF np] q have "isconstant q" by blast
   921     with isconstant_polybound0[OF th] have "polybound0 q" by blast}
   922   hence "\<forall>q \<in> ?cf. polybound0 q" ..
   923   hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"
   924     using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]
   925     by auto
   926   
   927   thus ?thesis unfolding polypoly_def polypoly'_def by simp 
   928 qed
   929 
   930 lemma polypoly_poly:
   931   assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"
   932   using np 
   933 by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)
   934 
   935 lemma polypoly'_poly: 
   936   assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"
   937   using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .
   938 
   939 
   940 lemma polypoly_poly_polybound0:
   941   assumes np: "isnpolyh p n0" and nb: "polybound0 p"
   942   shows "polypoly bs p = [Ipoly bs p]"
   943   using np nb unfolding polypoly_def 
   944   by (cases p, auto, case_tac nat, auto)
   945 
   946 lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 
   947   by (induct p rule: head.induct, auto)
   948 
   949 lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"
   950   by (cases p,auto)
   951 
   952 lemma head_eq_headn0: "head p = headn p 0"
   953   by (induct p rule: head.induct, simp_all)
   954 
   955 lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"
   956   by (simp add: head_eq_headn0)
   957 
   958 lemma isnpolyh_zero_iff: 
   959   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})"
   960   shows "p = 0\<^sub>p"
   961 using nq eq
   962 proof (induct "maxindex p" arbitrary: p n0 rule: less_induct)
   963   case less
   964   note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)`
   965   {assume nz: "maxindex p = 0"
   966     then obtain c where "p = C c" using np by (cases p, auto)
   967     with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}
   968   moreover
   969   {assume nz: "maxindex p \<noteq> 0"
   970     let ?h = "head p"
   971     let ?hd = "decrpoly ?h"
   972     let ?ihd = "maxindex ?hd"
   973     from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h" 
   974       by simp_all
   975     hence nhd: "isnpolyh ?hd (n0 - 1)" using decrpoly_normh by blast
   976     
   977     from maxindex_coefficients[of p] coefficients_head[of p, symmetric]
   978     have mihn: "maxindex ?h \<le> maxindex p" by auto
   979     with decr_maxindex[OF h(2)] nz  have ihd_lt_n: "?ihd < maxindex p" by auto
   980     {fix bs:: "'a list"  assume bs: "wf_bs bs ?hd"
   981       let ?ts = "take ?ihd bs"
   982       let ?rs = "drop ?ihd bs"
   983       have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp
   984       have bs_ts_eq: "?ts@ ?rs = bs" by simp
   985       from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp
   986       from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp
   987       with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast
   988       hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" unfolding wf_bs_def by simp
   989       with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast
   990       hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp
   991       with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]
   992       have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x"  by simp
   993       hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext) 
   994       hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"
   995         using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)
   996       with coefficients_head[of p, symmetric]
   997       have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp
   998       from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp
   999       with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp
  1000       with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }
  1001     then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast
  1002     
  1003     from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast
  1004     hence "?h = 0\<^sub>p" by simp
  1005     with head_nz[OF np] have "p = 0\<^sub>p" by simp}
  1006   ultimately show "p = 0\<^sub>p" by blast
  1007 qed
  1008 
  1009 lemma isnpolyh_unique:  
  1010   assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1011   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"
  1012 proof(auto)
  1013   assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"
  1014   hence "\<forall>bs.\<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp
  1015   hence "\<forall>bs. wf_bs bs (p -\<^sub>p q) \<longrightarrow> \<lparr>p -\<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" 
  1016     using wf_bs_polysub[where p=p and q=q] by auto
  1017   with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]
  1018   show "p = q" by blast
  1019 qed
  1020 
  1021 
  1022 text{* consequences of unicity on the algorithms for polynomial normalization *}
  1023 
  1024 lemma polyadd_commute:   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1025   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"
  1026   using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp
  1027 
  1028 lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp
  1029 lemma one_normh: "isnpolyh 1\<^sub>p n" by simp
  1030 lemma polyadd_0[simp]: 
  1031   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1032   and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"
  1033   using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 
  1034     isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all
  1035 
  1036 lemma polymul_1[simp]: 
  1037   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1038   and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"
  1039   using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 
  1040     isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all
  1041 lemma polymul_0[simp]: 
  1042   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1043   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"
  1044   using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 
  1045     isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all
  1046 
  1047 lemma polymul_commute: 
  1048     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1049   and np:"isnpolyh p n0" and nq: "isnpolyh q n1"
  1050   shows "p *\<^sub>p q = q *\<^sub>p p"
  1051 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
  1052 
  1053 declare polyneg_polyneg[simp]
  1054   
  1055 lemma isnpolyh_polynate_id[simp]: 
  1056   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1057   and np:"isnpolyh p n0" shows "polynate p = p"
  1058   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
  1059 
  1060 lemma polynate_idempotent[simp]: 
  1061     assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1062   shows "polynate (polynate p) = polynate p"
  1063   using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .
  1064 
  1065 lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"
  1066   unfolding poly_nate_def polypoly'_def ..
  1067 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>)"
  1068   using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]
  1069   unfolding poly_nate_polypoly' by (auto intro: ext)
  1070 
  1071 subsection{* heads, degrees and all that *}
  1072 lemma degree_eq_degreen0: "degree p = degreen p 0"
  1073   by (induct p rule: degree.induct, simp_all)
  1074 
  1075 lemma degree_polyneg: assumes n: "isnpolyh p n"
  1076   shows "degree (polyneg p) = degree p"
  1077   using n
  1078   by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)
  1079 
  1080 lemma degree_polyadd:
  1081   assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1082   shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"
  1083 using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp
  1084 
  1085 
  1086 lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"
  1087   shows "degree (p -\<^sub>p q) \<le> max (degree p) (degree q)"
  1088 proof-
  1089   from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp
  1090   from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])
  1091 qed
  1092 
  1093 lemma degree_polysub_samehead: 
  1094   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1095   and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
  1096   and d: "degree p = degree q"
  1097   shows "degree (p -\<^sub>p q) < degree p \<or> (p -\<^sub>p q = 0\<^sub>p)"
  1098 unfolding polysub_def split_def fst_conv snd_conv
  1099 using np nq h d
  1100 proof(induct p q rule:polyadd.induct)
  1101   case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
  1102 next
  1103   case (2 a b c' n' p') 
  1104   let ?c = "(a,b)"
  1105   from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp
  1106   hence nz:"n' > 0" by (cases n', auto)
  1107   hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)
  1108   with 2 show ?case by simp
  1109 next
  1110   case (3 c n p a' b') 
  1111   let ?c' = "(a',b')"
  1112   from 3 have "degree (C ?c') = degree (CN c n p)" by simp
  1113   hence nz:"n > 0" by (cases n, auto)
  1114   hence "head (CN c n p) = CN c n p" by (cases n, auto)
  1115   with 3 show ?case by simp
  1116 next
  1117   case (4 c n p c' n' p')
  1118   hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 
  1119     "head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+
  1120   hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all  
  1121   hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0" 
  1122     using H(1-2) degree_polyneg by auto
  1123   from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')"  by simp+
  1124   from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p  ~\<^sub>pc') = 0"  by simp
  1125   from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto
  1126   have "n = n' \<or> n < n' \<or> n > n'" by arith
  1127   moreover
  1128   {assume nn': "n = n'"
  1129     have "n = 0 \<or> n >0" by arith
  1130     moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')}
  1131     moreover {assume nz: "n > 0"
  1132       with nn' H(3) have  cc': "c = c'" and pp': "p = p'" by (cases n, auto)+
  1133       hence ?case
  1134         using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv]
  1135           polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv]
  1136         using 4 nn' by (simp add: Let_def) }
  1137     ultimately have ?case by blast}
  1138   moreover
  1139   {assume nn': "n < n'" hence n'p: "n' > 0" by simp 
  1140     hence headcnp':"head (CN c' n' p') = CN c' n' p'"  by (cases n', simp_all)
  1141     have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')"
  1142       using 4 nn' 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 4 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 Suc 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 apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans)
  1203 done
  1204 
  1205 lemma polymul_head_polyeq: 
  1206   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1207   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"
  1208 proof (induct p q arbitrary: n0 n1 rule: polymul.induct)
  1209   case (2 a b c' n' p' n0 n1)
  1210   hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)"  by (simp_all add: head_isnpolyh)
  1211   thus ?case using 2 by (cases n') auto
  1212 next 
  1213   case (3 c n p a' b' n0 n1) 
  1214   hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')"  by (simp_all add: head_isnpolyh)
  1215   thus ?case using 3 by (cases n) auto
  1216 next
  1217   case (4 c n p c' n' p' n0 n1)
  1218   hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"
  1219     "isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"
  1220     by simp_all
  1221   have "n < n' \<or> n' < n \<or> n = n'" by arith
  1222   moreover 
  1223   {assume nn': "n < n'" hence ?case 
  1224     using norm 
  1225     4(5)[rule_format, OF nn' norm(1,6)]
  1226     4(6)[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 4(3) [rule_format, OF stupid norm(5,3)]
  1230       4(4)[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 4(1)[rule_format, OF stupid norm(5,3)]
  1256         4(2)[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:
  1612   assumes nbs: "n < length bs" and mbs: "m < length bs"
  1613   shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t"
  1614   using swap[OF assms] swapnorm_def by simp
  1615 
  1616 lemma swapnorm_isnpoly[simp]: 
  1617   assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
  1618   shows "isnpoly (swapnorm n m p)"
  1619   unfolding swapnorm_def by simp
  1620 
  1621 definition "polydivideby n s p = 
  1622     (let ss = swapnorm 0 n s ; sp = swapnorm 0 n p ; h = head sp; (k,r) = polydivide ss sp
  1623      in (k,swapnorm 0 n h,swapnorm 0 n r))"
  1624 
  1625 lemma swap_nz [simp]: " (swap n m p = 0\<^sub>p) = (p = 0\<^sub>p)" by (induct p, simp_all)
  1626 
  1627 consts isweaknpoly :: "poly \<Rightarrow> bool"
  1628 recdef isweaknpoly "measure size"
  1629   "isweaknpoly (C c) = True"
  1630   "isweaknpoly (CN c n p) \<longleftrightarrow> isweaknpoly c \<and> isweaknpoly p"
  1631   "isweaknpoly p = False"       
  1632 
  1633 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 
  1634   by (induct p arbitrary: n0) auto
  1635 
  1636 lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 
  1637   by (induct p) auto
  1638 
  1639 end