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