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