33154

1 
(* Title: HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy


2 
Author: Amine Chaieb


3 
*)


4 


5 
header {* Implementation and verification of mutivariate polynomials Library *}


6 


7 


8 
theory Reflected_Multivariate_Polynomial


9 
imports Parity Abstract_Rat Efficient_Nat List Polynomial_List


10 
begin


11 


12 
(* Impelementation *)


13 


14 
subsection{* Datatype of polynomial expressions *}


15 


16 
datatype poly = C Num Bound nat Add poly polySub poly poly


17 
 Mul poly poly Neg poly Pw poly nat CN poly nat poly


18 


19 
ML{* @{term "Add"}*}


20 
syntax "_poly0" :: "poly" ("0\<^sub>p")


21 
translations "0\<^sub>p" \<rightleftharpoons> "C (0\<^sub>N)"


22 
syntax "_poly" :: "int \<Rightarrow> poly" ("_\<^sub>p")


23 
translations "i\<^sub>p" \<rightleftharpoons> "C (i\<^sub>N)"


24 


25 
subsection{* Boundedness, substitution and all that *}


26 
consts polysize:: "poly \<Rightarrow> nat"


27 
primrec


28 
"polysize (C c) = 1"


29 
"polysize (Bound n) = 1"


30 
"polysize (Neg p) = 1 + polysize p"


31 
"polysize (Add p q) = 1 + polysize p + polysize q"


32 
"polysize (Sub p q) = 1 + polysize p + polysize q"


33 
"polysize (Mul p q) = 1 + polysize p + polysize q"


34 
"polysize (Pw p n) = 1 + polysize p"


35 
"polysize (CN c n p) = 4 + polysize c + polysize p"


36 


37 
consts


38 
polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *)


39 
polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly" (* substitute a poly into a poly for Bound 0 *)


40 
primrec


41 
"polybound0 (C c) = True"


42 
"polybound0 (Bound n) = (n>0)"


43 
"polybound0 (Neg a) = polybound0 a"


44 
"polybound0 (Add a b) = (polybound0 a \<and> polybound0 b)"


45 
"polybound0 (Sub a b) = (polybound0 a \<and> polybound0 b)"


46 
"polybound0 (Mul a b) = (polybound0 a \<and> polybound0 b)"


47 
"polybound0 (Pw p n) = (polybound0 p)"


48 
"polybound0 (CN c n p) = (n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p)"


49 
primrec


50 
"polysubst0 t (C c) = (C c)"


51 
"polysubst0 t (Bound n) = (if n=0 then t else Bound n)"


52 
"polysubst0 t (Neg a) = Neg (polysubst0 t a)"


53 
"polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"


54 
"polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"


55 
"polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"


56 
"polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"


57 
"polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))


58 
else CN (polysubst0 t c) n (polysubst0 t p))"


59 


60 
consts


61 
decrpoly:: "poly \<Rightarrow> poly"


62 
recdef decrpoly "measure polysize"


63 
"decrpoly (Bound n) = Bound (n  1)"


64 
"decrpoly (Neg a) = Neg (decrpoly a)"


65 
"decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"


66 
"decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"


67 
"decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"


68 
"decrpoly (Pw p n) = Pw (decrpoly p) n"


69 
"decrpoly (CN c n p) = CN (decrpoly c) (n  1) (decrpoly p)"


70 
"decrpoly a = a"


71 


72 
subsection{* Degrees and heads and coefficients *}


73 


74 
consts degree:: "poly \<Rightarrow> nat"


75 
recdef degree "measure size"


76 
"degree (CN c 0 p) = 1 + degree p"


77 
"degree p = 0"


78 
consts head:: "poly \<Rightarrow> poly"


79 


80 
recdef head "measure size"


81 
"head (CN c 0 p) = head p"


82 
"head p = p"


83 
(* More general notions of degree and head *)


84 
consts degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat"


85 
recdef degreen "measure size"


86 
"degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)"


87 
"degreen p = (\<lambda>m. 0)"


88 


89 
consts headn:: "poly \<Rightarrow> nat \<Rightarrow> poly"


90 
recdef headn "measure size"


91 
"headn (CN c n p) = (\<lambda>m. if n \<le> m then headn p m else CN c n p)"


92 
"headn p = (\<lambda>m. p)"


93 


94 
consts coefficients:: "poly \<Rightarrow> poly list"


95 
recdef coefficients "measure size"


96 
"coefficients (CN c 0 p) = c#(coefficients p)"


97 
"coefficients p = [p]"


98 


99 
consts isconstant:: "poly \<Rightarrow> bool"


100 
recdef isconstant "measure size"


101 
"isconstant (CN c 0 p) = False"


102 
"isconstant p = True"


103 


104 
consts behead:: "poly \<Rightarrow> poly"


105 
recdef behead "measure size"


106 
"behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"


107 
"behead p = 0\<^sub>p"


108 


109 
consts headconst:: "poly \<Rightarrow> Num"


110 
recdef headconst "measure size"


111 
"headconst (CN c n p) = headconst p"


112 
"headconst (C n) = n"


113 


114 
subsection{* Operations for normalization *}


115 
consts


116 
polyadd :: "poly\<times>poly \<Rightarrow> poly"


117 
polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p")


118 
polysub :: "poly\<times>poly \<Rightarrow> poly"


119 
polymul :: "poly\<times>poly \<Rightarrow> poly"


120 
polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"


121 
syntax "_polyadd" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)


122 
translations "a +\<^sub>p b" \<rightleftharpoons> "polyadd (a,b)"


123 
syntax "_polymul" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)


124 
translations "a *\<^sub>p b" \<rightleftharpoons> "polymul (a,b)"


125 
syntax "_polysub" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "\<^sub>p" 60)


126 
translations "a \<^sub>p b" \<rightleftharpoons> "polysub (a,b)"


127 
syntax "_polypow" :: "nat \<Rightarrow> poly \<Rightarrow> poly" (infixl "^\<^sub>p" 60)


128 
translations "a ^\<^sub>p k" \<rightleftharpoons> "polypow k a"


129 


130 
recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"


131 
"polyadd (C c, C c') = C (c+\<^sub>Nc')"


132 
"polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"


133 
"polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"


134 
stupid: "polyadd (CN c n p, CN c' n' p') =


135 
(if n < n' then CN (polyadd(c,CN c' n' p')) n p


136 
else if n'<n then CN (polyadd(CN c n p, c')) n' p'


137 
else (let cc' = polyadd (c,c') ;


138 
pp' = polyadd (p,p')


139 
in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"


140 
"polyadd (a, b) = Add a b"


141 
(hints recdef_simp add: Let_def measure_def split_def inv_image_def)


142 


143 
(*


144 
declare stupid [simp del, code del]


145 


146 
lemma [simp,code]: "polyadd (CN c n p, CN c' n' p') =


147 
(if n < n' then CN (polyadd(c,CN c' n' p')) n p


148 
else if n'<n then CN (polyadd(CN c n p, c')) n' p'


149 
else (let cc' = polyadd (c,c') ;


150 
pp' = polyadd (p,p')


151 
in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))"


152 
by (simp add: Let_def stupid)


153 
*)


154 


155 
recdef polyneg "measure size"


156 
"polyneg (C c) = C (~\<^sub>N c)"


157 
"polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"


158 
"polyneg a = Neg a"


159 


160 
defs polysub_def[code]: "polysub \<equiv> \<lambda> (p,q). polyadd (p,polyneg q)"


161 


162 
recdef polymul "measure (\<lambda>(a,b). size a + size b)"


163 
"polymul(C c, C c') = C (c*\<^sub>Nc')"


164 
"polymul(C c, CN c' n' p') =


165 
(if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))"


166 
"polymul(CN c n p, C c') =


167 
(if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))"


168 
"polymul(CN c n p, CN c' n' p') =


169 
(if n<n' then CN (polymul(c,CN c' n' p')) n (polymul(p,CN c' n' p'))


170 
else if n' < n


171 
then CN (polymul(CN c n p,c')) n' (polymul(CN c n p,p'))


172 
else polyadd(polymul(CN c n p, c'),CN 0\<^sub>p n' (polymul(CN c n p, p'))))"


173 
"polymul (a,b) = Mul a b"


174 
recdef polypow "measure id"


175 
"polypow 0 = (\<lambda>p. 1\<^sub>p)"


176 
"polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul(q,q) in


177 
if even n then d else polymul(p,d))"


178 


179 
consts polynate :: "poly \<Rightarrow> poly"


180 
recdef polynate "measure polysize"


181 
"polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"


182 
"polynate (Add p q) = (polynate p +\<^sub>p polynate q)"


183 
"polynate (Sub p q) = (polynate p \<^sub>p polynate q)"


184 
"polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"


185 
"polynate (Neg p) = (~\<^sub>p (polynate p))"


186 
"polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"


187 
"polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"


188 
"polynate (C c) = C (normNum c)"


189 


190 
fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" where


191 
"poly_cmul y (C x) = C (y *\<^sub>N x)"


192 
 "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"


193 
 "poly_cmul y p = C y *\<^sub>p p"


194 


195 
constdefs monic:: "poly \<Rightarrow> (poly \<times> bool)"


196 
"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))"


197 


198 
subsection{* Pseudodivision *}


199 


200 
constdefs shift1:: "poly \<Rightarrow> poly"


201 
"shift1 p \<equiv> CN 0\<^sub>p 0 p"


202 
consts funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"


203 


204 
primrec


205 
"funpow 0 f x = x"


206 
"funpow (Suc n) f x = funpow n f (f x)"


207 
function (tailrec) polydivide_aux :: "(poly \<times> nat \<times> poly \<times> nat \<times> poly) \<Rightarrow> (nat \<times> poly)"


208 
where


209 
"polydivide_aux (a,n,p,k,s) =


210 
(if s = 0\<^sub>p then (k,s)


211 
else (let b = head s; m = degree s in


212 
(if m < n then (k,s) else


213 
(let p'= funpow (m  n) shift1 p in


214 
(if a = b then polydivide_aux (a,n,p,k,s \<^sub>p p')


215 
else polydivide_aux (a,n,p,Suc k, (a *\<^sub>p s) \<^sub>p (b *\<^sub>p p')))))))"


216 
by pat_completeness auto


217 


218 


219 
constdefs polydivide:: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)"


220 
"polydivide s p \<equiv> polydivide_aux (head p,degree p,p,0, s)"


221 


222 
fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" where


223 
"poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"


224 
 "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"


225 


226 
fun poly_deriv :: "poly \<Rightarrow> poly" where


227 
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"


228 
 "poly_deriv p = 0\<^sub>p"


229 


230 
(* Verification *)


231 
lemma nth_pos2[simp]: "0 < n \<Longrightarrow> (x#xs) ! n = xs ! (n  1)"


232 
using Nat.gr0_conv_Suc


233 
by clarsimp


234 


235 
subsection{* Semantics of the polynomial representation *}


236 


237 
consts Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{ring_char_0,power,division_by_zero,field}"


238 
primrec


239 
"Ipoly bs (C c) = INum c"


240 
"Ipoly bs (Bound n) = bs!n"


241 
"Ipoly bs (Neg a) =  Ipoly bs a"


242 
"Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"


243 
"Ipoly bs (Sub a b) = Ipoly bs a  Ipoly bs b"


244 
"Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"


245 
"Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"


246 
"Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"


247 
syntax "_Ipoly" :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")


248 
translations "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup>" \<rightleftharpoons> "Ipoly bs p"


249 


250 
lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"


251 
by (simp add: INum_def)


252 
lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"


253 
by (simp add: INum_def)


254 


255 
lemmas RIpoly_eqs = Ipoly.simps(27) Ipoly_CInt Ipoly_CRat


256 


257 
subsection {* Normal form and normalization *}


258 


259 
consts isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool"


260 
recdef isnpolyh "measure size"


261 
"isnpolyh (C c) = (\<lambda>k. isnormNum c)"


262 
"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))"


263 
"isnpolyh p = (\<lambda>k. False)"


264 


265 
lemma isnpolyh_mono: "\<lbrakk>n' \<le> n ; isnpolyh p n\<rbrakk> \<Longrightarrow> isnpolyh p n'"


266 
by (induct p rule: isnpolyh.induct, auto)


267 


268 
constdefs isnpoly:: "poly \<Rightarrow> bool"


269 
"isnpoly p \<equiv> isnpolyh p 0"


270 


271 
text{* polyadd preserves normal forms *}


272 


273 
lemma polyadd_normh: "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk>


274 
\<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)"


275 
proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)


276 
case (2 a b c' n' p' n0 n1)


277 
from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp


278 
from prems(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all


279 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp


280 
with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp


281 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp


282 
thus ?case using prems th3 by simp


283 
next


284 
case (3 c' n' p' a b n1 n0)


285 
from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp


286 
from prems(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all


287 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp


288 
with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp


289 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp


290 
thus ?case using prems th3 by simp


291 
next


292 
case (4 c n p c' n' p' n0 n1)


293 
hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all


294 
from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all


295 
from prems have ngen0: "n \<ge> n0" by simp


296 
from prems have n'gen1: "n' \<ge> n1" by simp


297 
have "n < n' \<or> n' < n \<or> n = n'" by auto


298 
moreover {assume eq: "n = n'" hence eq': "\<not> n' < n \<and> \<not> n < n'" by simp


299 
with prems(2)[rule_format, OF eq' nc nc']


300 
have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto


301 
hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"


302 
using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto


303 
from eq prems(1)[rule_format, OF eq' np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp


304 
have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp


305 
from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}


306 
moreover {assume lt: "n < n'"


307 
have "min n0 n1 \<le> n0" 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


310 
from prems have th22: "isnpolyh (CN c' n' p') n'" by simp


311 
from lt have th23: "min (Suc n) n' = Suc n" by arith


312 
from prems(4)[rule_format, OF lt th21 th22]


313 
have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp


314 
with prems th1 have ?case by simp }


315 
moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp


316 
have "min n0 n1 \<le> n1" by simp


317 
with prems have th1:"min n0 n1 \<le> n'" by auto


318 
from prems have th21: "isnpolyh c' (Suc n')" by simp_all


319 
from prems have th22: "isnpolyh (CN c n p) n" by simp


320 
from gt have th23: "min n (Suc n') = Suc n'" by arith


321 
from prems(3)[rule_format, OF gt' th22 th21]


322 
have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp


323 
with prems th1 have ?case by simp}


324 
ultimately show ?case by blast


325 
qed auto


326 


327 
lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"


328 
by (induct p q rule: polyadd.induct, auto simp add: Let_def ring_simps right_distrib[symmetric] simp del: right_distrib)


329 


330 
lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd(p,q))"


331 
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp


332 


333 
text{* The degree of addition and other general lemmas needed for the normal form of polymul*}


334 


335 
lemma polyadd_different_degreen:


336 
"\<lbrakk>isnpolyh p n0 ; isnpolyh q n1; degreen p m \<noteq> degreen q m ; m \<le> min n0 n1\<rbrakk> \<Longrightarrow>


337 
degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"


338 
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)


339 
case (4 c n p c' n' p' m n0 n1)


340 
thus ?case


341 
apply (cases "n' < n", simp_all add: Let_def)


342 
apply (cases "n = n'", simp_all)


343 
apply (cases "n' = m", simp_all add: Let_def)


344 
by (erule allE[where x="m"], erule allE[where x="Suc m"],


345 
erule allE[where x="m"], erule allE[where x="Suc m"],


346 
clarsimp,erule allE[where x="m"],erule allE[where x="Suc m"], simp)


347 
qed simp_all


348 


349 
lemma headnz[simp]: "\<lbrakk>isnpolyh p n ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> headn p m \<noteq> 0\<^sub>p"


350 
by (induct p arbitrary: n rule: headn.induct, auto)


351 
lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0"


352 
by (induct p arbitrary: n rule: degree.induct, auto)


353 
lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0"


354 
by (induct p arbitrary: n rule: degreen.induct, auto)


355 


356 
lemma degree_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> degree p = 0"


357 
by (induct p arbitrary: n rule: degree.induct, auto)


358 


359 
lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degree c = 0"


360 
using degree_isnpolyh_Suc by auto


361 
lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0"


362 
using degreen_0 by auto


363 


364 


365 
lemma degreen_polyadd:


366 
assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> max n0 n1"


367 
shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)"


368 
using np nq m


369 
proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)


370 
case (2 c c' n' p' n0 n1) thus ?case by (cases n', simp_all)


371 
next


372 
case (3 c n p c' n0 n1) thus ?case by (cases n, auto)


373 
next


374 
case (4 c n p c' n' p' n0 n1 m)


375 
thus ?case


376 
apply (cases "n < n'", simp_all add: Let_def)


377 
apply (cases "n' < n", simp_all)


378 
apply (erule allE[where x="n"],erule allE[where x="Suc n"],clarify)


379 
apply (erule allE[where x="n'"],erule allE[where x="Suc n'"],clarify)


380 
by (erule allE[where x="m"],erule allE[where x="m"], auto)


381 
qed auto


382 


383 


384 
lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk>


385 
\<Longrightarrow> degreen p m = degreen q m"


386 
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)


387 
case (4 c n p c' n' p' m n0 n1 x)


388 
hence z: "CN c n p +\<^sub>p CN c' n' p' = C x" by simp


389 
{assume nn': "n' < n" hence ?case using prems by simp}


390 
moreover


391 
{assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith


392 
moreover {assume "n < n'" with prems have ?case by simp }


393 
moreover {assume eq: "n = n'" hence ?case using prems


394 
by (cases "p +\<^sub>p p' = 0\<^sub>p", auto simp add: Let_def) }


395 
ultimately have ?case by blast}


396 
ultimately show ?case by blast


397 
qed simp_all


398 


399 
lemma polymul_properties:


400 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


401 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1"


402 
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"


403 
and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \<or> q = 0\<^sub>p)"


404 
and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \<or> q = 0\<^sub>p) then 0


405 
else degreen p m + degreen q m)"


406 
using np nq m


407 
proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)


408 
case (2 a b c' n' p')


409 
let ?c = "(a,b)"


410 
{ case (1 n0 n1)


411 
hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c"


412 
"isnpolyh (CN c' n' p') n1"


413 
by simp_all


414 
{assume "?c = 0\<^sub>N" hence ?case by auto}


415 
moreover {assume cnz: "?c \<noteq> 0\<^sub>N"


416 
from "2.hyps"(1)[rule_format,where xb="n'", OF cnz n(1) n(3)]


417 
"2.hyps"(2)[rule_format, where x="Suc n'"


418 
and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case


419 
by (auto simp add: min_def)}


420 
ultimately show ?case by blast


421 
next


422 
case (2 n0 n1) thus ?case by auto


423 
next


424 
case (3 n0 n1) thus ?case using "2.hyps" by auto }


425 
next


426 
case (3 c n p a b){


427 
let ?c' = "(a,b)"


428 
case (1 n0 n1)


429 
hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'"


430 
"isnpolyh (CN c n p) n0"


431 
by simp_all


432 
{assume "?c' = 0\<^sub>N" hence ?case by auto}


433 
moreover {assume cnz: "?c' \<noteq> 0\<^sub>N"


434 
from "3.hyps"(1)[rule_format,where xb="n", OF cnz n(3) n(1)]


435 
"3.hyps"(2)[rule_format, where x="Suc n"


436 
and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case


437 
by (auto simp add: min_def)}


438 
ultimately show ?case by blast


439 
next


440 
case (2 n0 n1) thus ?case apply auto done


441 
next


442 
case (3 n0 n1) thus ?case using "3.hyps" by auto }


443 
next


444 
case (4 c n p c' n' p')


445 
let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"


446 
{fix n0 n1


447 
assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"


448 
hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"


449 
and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"


450 
and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"


451 
and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1"


452 
by simp_all


453 
have "n < n' \<or> n' < n \<or> n' = n" by auto


454 
moreover


455 
{assume nn': "n < n'"


456 
with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]


457 
"4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp


458 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"


459 
by (simp add: min_def) }


460 
moreover


461 


462 
{assume nn': "n > n'" hence stupid: "n' < n \<and> \<not> n < n'" by arith


463 
with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]


464 
"4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]


465 
nn' nn0 nn1 cnp'


466 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"


467 
by (cases "Suc n' = n", simp_all add: min_def)}


468 
moreover


469 
{assume nn': "n' = n" hence stupid: "\<not> n' < n \<and> \<not> n < n'" by arith


470 
from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]


471 
"4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1


472 


473 
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"


474 
by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }


475 
ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }


476 
note th = this


477 
{fix n0 n1 m


478 
assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"


479 
and m: "m \<le> min n0 n1"


480 
let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"


481 
let ?d1 = "degreen ?cnp m"


482 
let ?d2 = "degreen ?cnp' m"


483 
let ?eq = "?d = (if ?cnp = 0\<^sub>p \<or> ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)"


484 
have "n'<n \<or> n < n' \<or> n' = n" by auto


485 
moreover


486 
{assume "n' < n \<or> n < n'"


487 
with "4.hyps" np np' m


488 
have ?eq apply (cases "n' < n", simp_all)


489 
apply (erule allE[where x="n"],erule allE[where x="n"],auto)


490 
done }


491 
moreover


492 
{assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith


493 
from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]


494 
"4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]


495 
np np' nn'


496 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"


497 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"


498 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"


499 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def)


500 
{assume mn: "m = n"


501 
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]


502 
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn


503 
have degs: "degreen (?cnp *\<^sub>p c') n =


504 
(if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"


505 
"degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def)


506 
from degs norm


507 
have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp


508 
hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"


509 
by simp


510 
have nmin: "n \<le> min n n" by (simp add: min_def)


511 
from polyadd_different_degreen[OF norm(3,6) neq nmin] th1


512 
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


513 
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]


514 
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]


515 
mn norm m nn' deg


516 
have ?eq by simp}


517 
moreover


518 
{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto


519 
from nn' m np have max1: "m \<le> max n n" by simp


520 
hence min1: "m \<le> min n n" by simp


521 
hence min2: "m \<le> min n (Suc n)" by simp


522 
{assume "c' = 0\<^sub>p"


523 
from `c' = 0\<^sub>p` have ?eq


524 
using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]


525 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'


526 
apply simp


527 
done}


528 
moreover


529 
{assume cnz: "c' \<noteq> 0\<^sub>p"


530 
from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]


531 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2]


532 
degreen_polyadd[OF norm(3,6) max1]


533 


534 
have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m


535 
\<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"


536 
using mn nn' cnz np np' by simp


537 
with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]


538 
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2]


539 
degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}


540 
ultimately have ?eq by blast }


541 
ultimately have ?eq by blast}


542 
ultimately show ?eq by blast}


543 
note degth = this


544 
{ case (2 n0 n1)


545 
hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"


546 
and m: "m \<le> min n0 n1" by simp_all


547 
hence mn: "m \<le> n" by simp


548 
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"


549 
{assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"


550 
hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp


551 
from "4.hyps"(1) [rule_format, OF nn, where x="n" and xa = "n" and xb="n"]


552 
"4.hyps"(2) [rule_format, OF nn, where x="n" and xa = "Suc n" and xb="n"]


553 
np np' C(2) mn


554 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"


555 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"


556 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"


557 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p"


558 
"degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"


559 
"degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"


560 
by (simp_all add: min_def)


561 


562 
from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp


563 
have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"


564 
using norm by simp


565 
from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq


566 
have "False" by simp }


567 
thus ?case using "4.hyps" by clarsimp}


568 
qed auto


569 


570 
lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"


571 
by(induct p q rule: polymul.induct, auto simp add: ring_simps)


572 


573 
lemma polymul_normh:


574 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


575 
shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)"


576 
using polymul_properties(1) by blast


577 
lemma polymul_eq0_iff:


578 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


579 
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) "


580 
using polymul_properties(2) by blast


581 
lemma polymul_degreen:


582 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


583 
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)"


584 
using polymul_properties(3) by blast


585 
lemma polymul_norm:


586 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


587 
shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul (p,q))"


588 
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp


589 


590 
lemma headconst_zero: "isnpolyh p n0 \<Longrightarrow> headconst p = 0\<^sub>N \<longleftrightarrow> p = 0\<^sub>p"


591 
by (induct p arbitrary: n0 rule: headconst.induct, auto)


592 


593 
lemma headconst_isnormNum: "isnpolyh p n0 \<Longrightarrow> isnormNum (headconst p)"


594 
by (induct p arbitrary: n0, auto)


595 


596 
lemma monic_eqI: assumes np: "isnpolyh p n0"


597 
shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{ring_char_0,power,division_by_zero,field})"


598 
unfolding monic_def Let_def


599 
proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])


600 
let ?h = "headconst p"


601 
assume pz: "p \<noteq> 0\<^sub>p"


602 
{assume hz: "INum ?h = (0::'a)"


603 
from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all


604 
from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp


605 
with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}


606 
thus "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by blast


607 
qed


608 


609 


610 


611 


612 
text{* polyneg is a negation and preserves normal form *}


613 
lemma polyneg[simp]: "Ipoly bs (polyneg p) =  Ipoly bs p"


614 
by (induct p rule: polyneg.induct, auto)


615 


616 
lemma polyneg0: "isnpolyh p n \<Longrightarrow> ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"


617 
by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)


618 
lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p"


619 
by (induct p arbitrary: n0 rule: polyneg.induct, auto)


620 
lemma polyneg_normh: "\<And>n. isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n "


621 
by (induct p rule: polyneg.induct, auto simp add: polyneg0)


622 


623 
lemma polyneg_norm: "isnpoly p \<Longrightarrow> isnpoly (polyneg p)"


624 
using isnpoly_def polyneg_normh by simp


625 


626 


627 
text{* polysub is a substraction and preserves normalform *}


628 
lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p)  (Ipoly bs q)"


629 
by (simp add: polysub_def polyneg polyadd)


630 
lemma polysub_normh: "\<And> n0 n1. \<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (polysub(p,q)) (min n0 n1)"


631 
by (simp add: polysub_def polyneg_normh polyadd_normh)


632 


633 
lemma polysub_norm: "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polysub(p,q))"


634 
using polyadd_norm polyneg_norm by (simp add: polysub_def)


635 
lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


636 
shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p"


637 
unfolding polysub_def split_def fst_conv snd_conv


638 
by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])


639 


640 
lemma polysub_0:


641 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


642 
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p \<^sub>p q = 0\<^sub>p) = (p = q)"


643 
unfolding polysub_def split_def fst_conv snd_conv


644 
apply (induct p q arbitrary: n0 n1 rule:polyadd.induct, simp_all add: Nsub0[simplified Nsub_def])


645 
apply (clarsimp simp add: Let_def)


646 
apply (case_tac "n < n'", simp_all)


647 
apply (case_tac "n' < n", simp_all)


648 
apply (erule impE)+


649 
apply (rule_tac x="Suc n" in exI, simp)


650 
apply (rule_tac x="n" in exI, simp)


651 
apply (erule impE)+


652 
apply (rule_tac x="n" in exI, simp)


653 
apply (rule_tac x="Suc n" in exI, simp)


654 
apply (erule impE)+


655 
apply (rule_tac x="Suc n" in exI, simp)


656 
apply (rule_tac x="n" in exI, simp)


657 
apply (erule impE)+


658 
apply (rule_tac x="Suc n" in exI, simp)


659 
apply clarsimp


660 
done


661 


662 
text{* polypow is a power function and preserves normal forms *}


663 
lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{ring_char_0,division_by_zero,field})) ^ n"


664 
proof(induct n rule: polypow.induct)


665 
case 1 thus ?case by simp


666 
next


667 
case (2 n)


668 
let ?q = "polypow ((Suc n) div 2) p"


669 
let ?d = "polymul(?q,?q)"


670 
have "odd (Suc n) \<or> even (Suc n)" by simp


671 
moreover


672 
{assume odd: "odd (Suc n)"


673 
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


674 
from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def)


675 
also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"


676 
using "2.hyps" by simp


677 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"


678 
apply (simp only: power_add power_one_right) by simp


679 
also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc (0\<Colon>nat)) * (Suc n div Suc (Suc (0\<Colon>nat)))))"


680 
by (simp only: th)


681 
finally have ?case


682 
using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp }


683 
moreover


684 
{assume even: "even (Suc n)"


685 
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


686 
from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)


687 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"


688 
using "2.hyps" apply (simp only: power_add) by simp


689 
finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)}


690 
ultimately show ?case by blast


691 
qed


692 


693 
lemma polypow_normh:


694 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


695 
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n"


696 
proof (induct k arbitrary: n rule: polypow.induct)


697 
case (2 k n)


698 
let ?q = "polypow (Suc k div 2) p"


699 
let ?d = "polymul (?q,?q)"


700 
from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+


701 
from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp


702 
from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp


703 
from dn on show ?case by (simp add: Let_def)


704 
qed auto


705 


706 
lemma polypow_norm:


707 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


708 
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)"


709 
by (simp add: polypow_normh isnpoly_def)


710 


711 
text{* Finally the whole normalization*}


712 


713 
lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{ring_char_0,division_by_zero,field})"


714 
by (induct p rule:polynate.induct, auto)


715 


716 
lemma polynate_norm[simp]:


717 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


718 
shows "isnpoly (polynate p)"


719 
by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)


720 


721 
text{* shift1 *}


722 


723 


724 
lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"


725 
by (simp add: shift1_def polymul)


726 


727 
lemma shift1_isnpoly:


728 
assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) "


729 
using pn pnz by (simp add: shift1_def isnpoly_def )


730 


731 
lemma shift1_nz[simp]:"shift1 p \<noteq> 0\<^sub>p"


732 
by (simp add: shift1_def)


733 
lemma funpow_shift1_isnpoly:


734 
"\<lbrakk> isnpoly p ; p \<noteq> 0\<^sub>p\<rbrakk> \<Longrightarrow> isnpoly (funpow n shift1 p)"


735 
by (induct n arbitrary: p, auto simp add: shift1_isnpoly)


736 


737 
lemma funpow_isnpolyh:


738 
assumes f: "\<And> p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n "and np: "isnpolyh p n"


739 
shows "isnpolyh (funpow k f p) n"


740 
using f np by (induct k arbitrary: p, auto)


741 


742 
lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {ring_char_0,division_by_zero,field}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"


743 
by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )


744 


745 
lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0"


746 
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)


747 


748 
lemma funpow_shift1_1:


749 
"(Ipoly bs (funpow n shift1 p) :: 'a :: {ring_char_0,division_by_zero,field}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"


750 
by (simp add: funpow_shift1)


751 


752 
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"


753 
by (induct p arbitrary: n0 rule: poly_cmul.induct, auto simp add: ring_simps)


754 


755 
lemma behead:


756 
assumes np: "isnpolyh p n"


757 
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {ring_char_0,division_by_zero,field})"


758 
using np


759 
proof (induct p arbitrary: n rule: behead.induct)


760 
case (1 c p n) hence pn: "isnpolyh p n" by simp


761 
from prems(2)[OF pn]


762 
have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .


763 
then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")


764 
by (simp_all add: th[symmetric] ring_simps power_Suc)


765 
qed (auto simp add: Let_def)


766 


767 
lemma behead_isnpolyh:


768 
assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"


769 
using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)


770 


771 
subsection{* Miscilanious lemmas about indexes, decrementation, substitution etc ... *}


772 
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p"


773 
proof(induct p arbitrary: n rule: polybound0.induct, auto)


774 
case (goal1 c n p n')


775 
hence "n = Suc (n  1)" by simp


776 
hence "isnpolyh p (Suc (n  1))" using `isnpolyh p n` by simp


777 
with prems(2) show ?case by simp


778 
qed


779 


780 
lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p"


781 
by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)


782 


783 
lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" by (induct p, auto)


784 


785 
lemma decrpoly_normh: "isnpolyh p n0 \<Longrightarrow> polybound0 p \<Longrightarrow> isnpolyh (decrpoly p) (n0  1)"


786 
apply (induct p arbitrary: n0, auto)


787 
apply (atomize)


788 
apply (erule_tac x = "Suc nat" in allE)


789 
apply auto


790 
done


791 


792 
lemma head_polybound0: "isnpolyh p n0 \<Longrightarrow> polybound0 (head p)"


793 
by (induct p arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)


794 


795 
lemma polybound0_I:


796 
assumes nb: "polybound0 a"


797 
shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"


798 
using nb


799 
by (induct a rule: polybound0.induct) auto


800 
lemma polysubst0_I:


801 
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"


802 
by (induct t) simp_all


803 


804 
lemma polysubst0_I':


805 
assumes nb: "polybound0 a"


806 
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"


807 
by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])


808 


809 
lemma decrpoly: assumes nb: "polybound0 t"


810 
shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"


811 
using nb by (induct t rule: decrpoly.induct, simp_all)


812 


813 
lemma polysubst0_polybound0: assumes nb: "polybound0 t"


814 
shows "polybound0 (polysubst0 t a)"


815 
using nb by (induct a rule: polysubst0.induct, auto)


816 


817 
lemma degree0_polybound0: "isnpolyh p n \<Longrightarrow> degree p = 0 \<Longrightarrow> polybound0 p"


818 
by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)


819 


820 
fun maxindex :: "poly \<Rightarrow> nat" where


821 
"maxindex (Bound n) = n + 1"


822 
 "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))"


823 
 "maxindex (Add p q) = max (maxindex p) (maxindex q)"


824 
 "maxindex (Sub p q) = max (maxindex p) (maxindex q)"


825 
 "maxindex (Mul p q) = max (maxindex p) (maxindex q)"


826 
 "maxindex (Neg p) = maxindex p"


827 
 "maxindex (Pw p n) = maxindex p"


828 
 "maxindex (C x) = 0"


829 


830 
definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" where


831 
"wf_bs bs p = (length bs \<ge> maxindex p)"


832 


833 
lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall> c \<in> set (coefficients p). wf_bs bs c"


834 
proof(induct p rule: coefficients.induct)


835 
case (1 c p)


836 
show ?case


837 
proof


838 
fix x assume xc: "x \<in> set (coefficients (CN c 0 p))"


839 
hence "x = c \<or> x \<in> set (coefficients p)" by simp


840 
moreover


841 
{assume "x = c" hence "wf_bs bs x" using "1.prems" unfolding wf_bs_def by simp}


842 
moreover


843 
{assume H: "x \<in> set (coefficients p)"


844 
from "1.prems" have "wf_bs bs p" unfolding wf_bs_def by simp


845 
with "1.hyps" H have "wf_bs bs x" by blast }


846 
ultimately show "wf_bs bs x" by blast


847 
qed


848 
qed simp_all


849 


850 
lemma maxindex_coefficients: " \<forall>c\<in> set (coefficients p). maxindex c \<le> maxindex p"


851 
by (induct p rule: coefficients.induct, auto)


852 


853 
lemma length_exists: "\<exists>xs. length xs = n" by (rule exI[where x="replicate n x"], simp)


854 


855 
lemma wf_bs_I: "wf_bs bs p ==> Ipoly (bs@bs') p = Ipoly bs p"


856 
unfolding wf_bs_def by (induct p, auto simp add: nth_append)


857 


858 
lemma take_maxindex_wf: assumes wf: "wf_bs bs p"


859 
shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p"


860 
proof


861 
let ?ip = "maxindex p"


862 
let ?tbs = "take ?ip bs"


863 
from wf have "length ?tbs = ?ip" unfolding wf_bs_def by simp


864 
hence wf': "wf_bs ?tbs p" unfolding wf_bs_def by simp


865 
have eq: "bs = ?tbs @ (drop ?ip bs)" by simp


866 
from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis using eq by simp


867 
qed


868 


869 
lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p  1"


870 
by (induct p, auto)


871 


872 
lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p"


873 
unfolding wf_bs_def by simp


874 


875 
lemma wf_bs_insensitive': "wf_bs (x#bs) p = wf_bs (y#bs) p"


876 
unfolding wf_bs_def by simp


877 


878 


879 


880 
lemma wf_bs_coefficients': "\<forall>c \<in> set (coefficients p). wf_bs bs c \<Longrightarrow> wf_bs (x#bs) p"


881 
by(induct p rule: coefficients.induct, auto simp add: wf_bs_def)


882 
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []"


883 
by (induct p rule: coefficients.induct, simp_all)


884 


885 


886 
lemma coefficients_head: "last (coefficients p) = head p"


887 
by (induct p rule: coefficients.induct, auto)


888 


889 
lemma wf_bs_decrpoly: "wf_bs bs (decrpoly p) \<Longrightarrow> wf_bs (x#bs) p"


890 
unfolding wf_bs_def by (induct p rule: decrpoly.induct, auto)


891 


892 
lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists> ys. length (xs @ ys) = n"


893 
apply (rule exI[where x="replicate (n  length xs) z"])


894 
by simp


895 
lemma isnpolyh_Suc_const:"isnpolyh p (Suc n) \<Longrightarrow> isconstant p"


896 
by (cases p, auto) (case_tac "nat", simp_all)


897 


898 
lemma wf_bs_polyadd: "wf_bs bs p \<and> wf_bs bs q \<longrightarrow> wf_bs bs (p +\<^sub>p q)"


899 
unfolding wf_bs_def


900 
apply (induct p q rule: polyadd.induct)


901 
apply (auto simp add: Let_def)


902 
done


903 


904 
lemma wf_bs_polyul: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p *\<^sub>p q)"


905 


906 
unfolding wf_bs_def


907 
apply (induct p q arbitrary: bs rule: polymul.induct)


908 
apply (simp_all add: wf_bs_polyadd)


909 
apply clarsimp


910 
apply (rule wf_bs_polyadd[unfolded wf_bs_def, rule_format])


911 
apply auto


912 
done


913 


914 
lemma wf_bs_polyneg: "wf_bs bs p \<Longrightarrow> wf_bs bs (~\<^sub>p p)"


915 
unfolding wf_bs_def by (induct p rule: polyneg.induct, auto)


916 


917 
lemma wf_bs_polysub: "wf_bs bs p \<Longrightarrow> wf_bs bs q \<Longrightarrow> wf_bs bs (p \<^sub>p q)"


918 
unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast


919 


920 
subsection{* Canonicity of polynomial representation, see lemma isnpolyh_unique*}


921 


922 
definition "polypoly bs p = map (Ipoly bs) (coefficients p)"


923 
definition "polypoly' bs p = map ((Ipoly bs o decrpoly)) (coefficients p)"


924 
definition "poly_nate bs p = map ((Ipoly bs o decrpoly)) (coefficients (polynate p))"


925 


926 
lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall> q \<in> set (coefficients p). isnpolyh q n0"


927 
proof (induct p arbitrary: n0 rule: coefficients.induct)


928 
case (1 c p n0)


929 
have cp: "isnpolyh (CN c 0 p) n0" by fact


930 
hence norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0"


931 
by (auto simp add: isnpolyh_mono[where n'=0])


932 
from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case by simp


933 
qed auto


934 


935 
lemma coefficients_isconst:


936 
"isnpolyh p n \<Longrightarrow> \<forall>q\<in>set (coefficients p). isconstant q"


937 
by (induct p arbitrary: n rule: coefficients.induct,


938 
auto simp add: isnpolyh_Suc_const)


939 


940 
lemma polypoly_polypoly':


941 
assumes np: "isnpolyh p n0"


942 
shows "polypoly (x#bs) p = polypoly' bs p"


943 
proof


944 
let ?cf = "set (coefficients p)"


945 
from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" .


946 
{fix q assume q: "q \<in> ?cf"


947 
from q cn_norm have th: "isnpolyh q n0" by blast


948 
from coefficients_isconst[OF np] q have "isconstant q" by blast


949 
with isconstant_polybound0[OF th] have "polybound0 q" by blast}


950 
hence "\<forall>q \<in> ?cf. polybound0 q" ..


951 
hence "\<forall>q \<in> ?cf. Ipoly (x#bs) q = Ipoly bs (decrpoly q)"


952 
using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs]


953 
by auto


954 


955 
thus ?thesis unfolding polypoly_def polypoly'_def by simp


956 
qed


957 


958 
lemma polypoly_poly:


959 
assumes np: "isnpolyh p n0" shows "Ipoly (x#bs) p = poly (polypoly (x#bs) p) x"


960 
using np


961 
by (induct p arbitrary: n0 bs rule: coefficients.induct, auto simp add: polypoly_def)


962 


963 
lemma polypoly'_poly:


964 
assumes np: "isnpolyh p n0" shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x"


965 
using polypoly_poly[OF np, simplified polypoly_polypoly'[OF np]] .


966 


967 


968 
lemma polypoly_poly_polybound0:


969 
assumes np: "isnpolyh p n0" and nb: "polybound0 p"


970 
shows "polypoly bs p = [Ipoly bs p]"


971 
using np nb unfolding polypoly_def


972 
by (cases p, auto, case_tac nat, auto)


973 


974 
lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0"


975 
by (induct p rule: head.induct, auto)


976 


977 
lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (headn p m = 0\<^sub>p) = (p = 0\<^sub>p)"


978 
by (cases p,auto)


979 


980 
lemma head_eq_headn0: "head p = headn p 0"


981 
by (induct p rule: head.induct, simp_all)


982 


983 
lemma head_nz[simp]: "isnpolyh p n0 \<Longrightarrow> (head p = 0\<^sub>p) = (p = 0\<^sub>p)"


984 
by (simp add: head_eq_headn0)


985 


986 
lemma isnpolyh_zero_iff:


987 
assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{ring_char_0,power,division_by_zero,field})"


988 
shows "p = 0\<^sub>p"


989 
using nq eq


990 
proof (induct n\<equiv>"maxindex p" arbitrary: p n0 rule: nat_less_induct)


991 
fix n p n0


992 
assume H: "\<forall>m<n. \<forall>p n0. isnpolyh p n0 \<longrightarrow>


993 
(\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)) \<longrightarrow> m = maxindex p \<longrightarrow> p = 0\<^sub>p"


994 
and np: "isnpolyh p n0" and zp: "\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" and n: "n = maxindex p"


995 
{assume nz: "n = 0"


996 
then obtain c where "p = C c" using n np by (cases p, auto)


997 
with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp}


998 
moreover


999 
{assume nz: "n \<noteq> 0"


1000 
let ?h = "head p"


1001 
let ?hd = "decrpoly ?h"


1002 
let ?ihd = "maxindex ?hd"


1003 
from head_isnpolyh[OF np] head_polybound0[OF np] have h:"isnpolyh ?h n0" "polybound0 ?h"


1004 
by simp_all


1005 
hence nhd: "isnpolyh ?hd (n0  1)" using decrpoly_normh by blast


1006 


1007 
from maxindex_coefficients[of p] coefficients_head[of p, symmetric]


1008 
have mihn: "maxindex ?h \<le> n" unfolding n by auto


1009 
with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < n" by auto


1010 
{fix bs:: "'a list" assume bs: "wf_bs bs ?hd"


1011 
let ?ts = "take ?ihd bs"


1012 
let ?rs = "drop ?ihd bs"


1013 
have ts: "wf_bs ?ts ?hd" using bs unfolding wf_bs_def by simp


1014 
have bs_ts_eq: "?ts@ ?rs = bs" by simp


1015 
from wf_bs_decrpoly[OF ts] have tsh: " \<forall>x. wf_bs (x#?ts) ?h" by simp


1016 
from ihd_lt_n have "ALL x. length (x#?ts) \<le> n" by simp


1017 
with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = n" by blast


1018 
hence "\<forall> x. wf_bs ((x#?ts) @ xs) p" using n unfolding wf_bs_def by simp


1019 
with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast


1020 
hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp


1021 
with polypoly_poly[OF np, where ?'a = 'a] polypoly_polypoly'[OF np, where ?'a = 'a]


1022 
have "\<forall>x. poly (polypoly' (?ts @ xs) p) x = poly [] x" by simp


1023 
hence "poly (polypoly' (?ts @ xs) p) = poly []" by (auto intro: ext)


1024 
hence "\<forall> c \<in> set (coefficients p). Ipoly (?ts @ xs) (decrpoly c) = 0"


1025 
thm poly_zero


1026 
using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff)


1027 
with coefficients_head[of p, symmetric]


1028 
have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp


1029 
from bs have wf'': "wf_bs ?ts ?hd" unfolding wf_bs_def by simp


1030 
with th0 wf_bs_I[of ?ts ?hd xs] have "Ipoly ?ts ?hd = 0" by simp


1031 
with wf'' wf_bs_I[of ?ts ?hd ?rs] bs_ts_eq have "\<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" by simp }


1032 
then have hdz: "\<forall>bs. wf_bs bs ?hd \<longrightarrow> \<lparr>?hd\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)" by blast


1033 


1034 
from H[rule_format, OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast


1035 
hence "?h = 0\<^sub>p" by simp


1036 
with head_nz[OF np] have "p = 0\<^sub>p" by simp}


1037 
ultimately show "p = 0\<^sub>p" by blast


1038 
qed


1039 


1040 
lemma isnpolyh_unique:


1041 
assumes np:"isnpolyh p n0" and nq: "isnpolyh q n1"


1042 
shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{ring_char_0,power,division_by_zero,field})) \<longleftrightarrow> p = q"


1043 
proof(auto)


1044 
assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>"


1045 
hence "\<forall>bs.\<lparr>p \<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup>= (0::'a)" by simp


1046 
hence "\<forall>bs. wf_bs bs (p \<^sub>p q) \<longrightarrow> \<lparr>p \<^sub>p q\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)"


1047 
using wf_bs_polysub[where p=p and q=q] by auto


1048 
with isnpolyh_zero_iff[OF polysub_normh[OF np nq]] polysub_0[OF np nq]


1049 
show "p = q" by blast


1050 
qed


1051 


1052 


1053 
text{* consequenses of unicity on the algorithms for polynomial normalization *}


1054 


1055 
lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1056 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p"


1057 
using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp


1058 


1059 
lemma zero_normh: "isnpolyh 0\<^sub>p n" by simp


1060 
lemma one_normh: "isnpolyh 1\<^sub>p n" by simp


1061 
lemma polyadd_0[simp]:


1062 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1063 
and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p"


1064 
using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np]


1065 
isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all


1066 


1067 
lemma polymul_1[simp]:


1068 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1069 
and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p"


1070 
using isnpolyh_unique[OF polymul_normh[OF np one_normh] np]


1071 
isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all


1072 
lemma polymul_0[simp]:


1073 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1074 
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"


1075 
using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh]


1076 
isnpolyh_unique[OF polymul_normh[OF zero_normh np] zero_normh] by simp_all


1077 


1078 
lemma polymul_commute:


1079 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1080 
and np:"isnpolyh p n0" and nq: "isnpolyh q n1"


1081 
shows "p *\<^sub>p q = q *\<^sub>p p"


1082 
using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{ring_char_0,power,division_by_zero,field}"] by simp


1083 


1084 
declare polyneg_polyneg[simp]


1085 


1086 
lemma isnpolyh_polynate_id[simp]:


1087 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1088 
and np:"isnpolyh p n0" shows "polynate p = p"


1089 
using isnpolyh_unique[where ?'a= "'a::{ring_char_0,division_by_zero,field}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{ring_char_0,division_by_zero,field}"] by simp


1090 


1091 
lemma polynate_idempotent[simp]:


1092 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1093 
shows "polynate (polynate p) = polynate p"


1094 
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] .


1095 


1096 
lemma poly_nate_polypoly': "poly_nate bs p = polypoly' bs (polynate p)"


1097 
unfolding poly_nate_def polypoly'_def ..


1098 
lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{ring_char_0,division_by_zero,field}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)"


1099 
using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p]


1100 
unfolding poly_nate_polypoly' by (auto intro: ext)


1101 


1102 
subsection{* heads, degrees and all that *}


1103 
lemma degree_eq_degreen0: "degree p = degreen p 0"


1104 
by (induct p rule: degree.induct, simp_all)


1105 


1106 
lemma degree_polyneg: assumes n: "isnpolyh p n"


1107 
shows "degree (polyneg p) = degree p"


1108 
using n


1109 
by (induct p arbitrary: n rule: polyneg.induct, simp_all) (case_tac na, auto)


1110 


1111 
lemma degree_polyadd:


1112 
assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"


1113 
shows "degree (p +\<^sub>p q) \<le> max (degree p) (degree q)"


1114 
using degreen_polyadd[OF np nq, where m= "0"] degree_eq_degreen0 by simp


1115 


1116 


1117 
lemma degree_polysub: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"


1118 
shows "degree (p \<^sub>p q) \<le> max (degree p) (degree q)"


1119 
proof


1120 
from nq have nq': "isnpolyh (~\<^sub>p q) n1" using polyneg_normh by simp


1121 
from degree_polyadd[OF np nq'] show ?thesis by (simp add: polysub_def degree_polyneg[OF nq])


1122 
qed


1123 


1124 
lemma degree_polysub_samehead:


1125 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1126 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q"


1127 
and d: "degree p = degree q"


1128 
shows "degree (p \<^sub>p q) < degree p \<or> (p \<^sub>p q = 0\<^sub>p)"


1129 
unfolding polysub_def split_def fst_conv snd_conv


1130 
using np nq h d


1131 
proof(induct p q rule:polyadd.induct)


1132 
case (1 a b a' b') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def])


1133 
next


1134 
case (2 a b c' n' p')


1135 
let ?c = "(a,b)"


1136 
from prems have "degree (C ?c) = degree (CN c' n' p')" by simp


1137 
hence nz:"n' > 0" by (cases n', auto)


1138 
hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)


1139 
with prems show ?case by simp


1140 
next


1141 
case (3 c n p a' b')


1142 
let ?c' = "(a',b')"


1143 
from prems have "degree (C ?c') = degree (CN c n p)" by simp


1144 
hence nz:"n > 0" by (cases n, auto)


1145 
hence "head (CN c n p) = CN c n p" by (cases n, auto)


1146 
with prems show ?case by simp


1147 
next


1148 
case (4 c n p c' n' p')


1149 
hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1"


1150 
"head (CN c n p) = head (CN c' n' p')" "degree (CN c n p) = degree (CN c' n' p')" by simp+


1151 
hence degc: "degree c = 0" and degc': "degree c' = 0" by simp_all


1152 
hence degnc: "degree (~\<^sub>p c) = 0" and degnc': "degree (~\<^sub>p c') = 0"


1153 
using H(12) degree_polyneg by auto


1154 
from H have cnh: "isnpolyh c (Suc n)" and c'nh: "isnpolyh c' (Suc n')" by simp+


1155 
from degree_polysub[OF cnh c'nh, simplified polysub_def] degc degc' have degcmc': "degree (c +\<^sub>p ~\<^sub>pc') = 0" by simp


1156 
from H have pnh: "isnpolyh p n" and p'nh: "isnpolyh p' n'" by auto


1157 
have "n = n' \<or> n < n' \<or> n > n'" by arith


1158 
moreover


1159 
{assume nn': "n = n'"


1160 
have "n = 0 \<or> n >0" by arith


1161 
moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')}


1162 
moreover {assume nz: "n > 0"


1163 
with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+


1164 
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)}


1165 
ultimately have ?case by blast}


1166 
moreover


1167 
{assume nn': "n < n'" hence n'p: "n' > 0" by simp


1168 
hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n', simp_all)


1169 
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)


1170 
hence "n > 0" by (cases n, simp_all)


1171 
hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto)


1172 
from H(3) headcnp headcnp' nn' have ?case by auto}


1173 
moreover


1174 
{assume nn': "n > n'" hence np: "n > 0" by simp


1175 
hence headcnp:"head (CN c n p) = CN c n p" by (cases n, simp_all)


1176 
from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp


1177 
from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all)


1178 
with degcnpeq have "n' > 0" by (cases n', simp_all)


1179 
hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto)


1180 
from H(3) headcnp headcnp' nn' have ?case by auto}


1181 
ultimately show ?case by blast


1182 
qed auto


1183 


1184 
lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p"


1185 
by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def)


1186 


1187 
lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p"


1188 
proof(induct k arbitrary: n0 p)


1189 
case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh)


1190 
with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)"


1191 
and "head (shift1 p) = head p" by (simp_all add: shift1_head)


1192 
thus ?case by simp


1193 
qed auto


1194 


1195 
lemma shift1_degree: "degree (shift1 p) = 1 + degree p"


1196 
by (simp add: shift1_def)


1197 
lemma funpow_shift1_degree: "degree (funpow k shift1 p) = k + degree p "


1198 
by (induct k arbitrary: p, auto simp add: shift1_degree)


1199 


1200 
lemma funpow_shift1_nz: "p \<noteq> 0\<^sub>p \<Longrightarrow> funpow n shift1 p \<noteq> 0\<^sub>p"


1201 
by (induct n arbitrary: p, simp_all add: funpow_def)


1202 


1203 
lemma head_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> head p = p"


1204 
by (induct p arbitrary: n rule: degree.induct, auto)


1205 
lemma headn_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> headn p m = p"


1206 
by (induct p arbitrary: n rule: degreen.induct, auto)


1207 
lemma head_isnpolyh_Suc': "n > 0 \<Longrightarrow> isnpolyh p n \<Longrightarrow> head p = p"


1208 
by (induct p arbitrary: n rule: degree.induct, auto)


1209 
lemma head_head[simp]: "isnpolyh p n0 \<Longrightarrow> head (head p) = head p"


1210 
by (induct p rule: head.induct, auto)


1211 


1212 
lemma polyadd_eq_const_degree:


1213 
"\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\<rbrakk> \<Longrightarrow> degree p = degree q"


1214 
using polyadd_eq_const_degreen degree_eq_degreen0 by simp


1215 


1216 
lemma polyadd_head: assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1"


1217 
and deg: "degree p \<noteq> degree q"


1218 
shows "head (p +\<^sub>p q) = (if degree p < degree q then head q else head p)"


1219 
using np nq deg


1220 
apply(induct p q arbitrary: n0 n1 rule: polyadd.induct,simp_all)


1221 
apply (case_tac n', simp, simp)


1222 
apply (case_tac n, simp, simp)


1223 
apply (case_tac n, case_tac n', simp add: Let_def)


1224 
apply (case_tac "pa +\<^sub>p p' = 0\<^sub>p")


1225 
apply (clarsimp simp add: polyadd_eq_const_degree)


1226 
apply clarsimp


1227 
apply (erule_tac impE,blast)


1228 
apply (erule_tac impE,blast)


1229 
apply clarsimp


1230 
apply simp


1231 
apply (case_tac n', simp_all)


1232 
done


1233 


1234 
lemma polymul_head_polyeq:


1235 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1236 
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"


1237 
proof (induct p q arbitrary: n0 n1 rule: polymul.induct)


1238 
case (2 a b c' n' p' n0 n1)


1239 
hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)" by (simp_all add: head_isnpolyh)


1240 
thus ?case using prems by (cases n', auto)


1241 
next


1242 
case (3 c n p a' b' n0 n1)


1243 
hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')" by (simp_all add: head_isnpolyh)


1244 
thus ?case using prems by (cases n, auto)


1245 
next


1246 
case (4 c n p c' n' p' n0 n1)


1247 
hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')"


1248 
"isnpolyh (CN c n p) n" "isnpolyh (CN c' n' p') n'"


1249 
by simp_all


1250 
have "n < n' \<or> n' < n \<or> n = n'" by arith


1251 
moreover


1252 
{assume nn': "n < n'" hence ?case


1253 
thm prems


1254 
using norm


1255 
prems(6)[rule_format, OF nn' norm(1,6)]


1256 
prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)}


1257 
moreover {assume nn': "n'< n"


1258 
hence stupid: "n' < n \<and> \<not> n < n'" by simp


1259 
hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)]


1260 
prems(5)[rule_format, OF stupid norm(5,4)]


1261 
by (simp,cases n',simp,cases n,auto)}


1262 
moreover {assume nn': "n' = n"


1263 
hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp


1264 
from nn' polymul_normh[OF norm(5,4)]


1265 
have ncnpc':"isnpolyh (CN c n p *\<^sub>p c') n" by (simp add: min_def)


1266 
from nn' polymul_normh[OF norm(5,3)] norm


1267 
have ncnpp':"isnpolyh (CN c n p *\<^sub>p p') n" by simp


1268 
from nn' ncnpp' polymul_eq0_iff[OF norm(5,3)] norm(6)


1269 
have ncnpp0':"isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp


1270 
from polyadd_normh[OF ncnpc' ncnpp0']


1271 
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"


1272 
by (simp add: min_def)


1273 
{assume np: "n > 0"


1274 
with nn' head_isnpolyh_Suc'[OF np nth]


1275 
head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']]


1276 
have ?case by simp}


1277 
moreover


1278 
{moreover assume nz: "n = 0"


1279 
from polymul_degreen[OF norm(5,4), where m="0"]


1280 
polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0


1281 
norm(5,6) degree_npolyhCN[OF norm(6)]


1282 
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


1283 
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


1284 
from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth


1285 
have ?case using norm prems(2)[rule_format, OF stupid norm(5,3)]


1286 
prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp }


1287 
ultimately have ?case by (cases n) auto}


1288 
ultimately show ?case by blast


1289 
qed simp_all


1290 


1291 
lemma degree_coefficients: "degree p = length (coefficients p)  1"


1292 
by(induct p rule: degree.induct, auto)


1293 


1294 
lemma degree_head[simp]: "degree (head p) = 0"


1295 
by (induct p rule: head.induct, auto)


1296 


1297 
lemma degree_CN: "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<le> 1+ degree p"


1298 
by (cases n, simp_all)


1299 
lemma degree_CN': "isnpolyh p n \<Longrightarrow> degree (CN c n p) \<ge> degree p"


1300 
by (cases n, simp_all)


1301 


1302 
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)"


1303 
using polyadd_different_degreen degree_eq_degreen0 by simp


1304 


1305 
lemma degreen_polyneg: "isnpolyh p n0 \<Longrightarrow> degreen (~\<^sub>p p) m = degreen p m"


1306 
by (induct p arbitrary: n0 rule: polyneg.induct, auto)


1307 


1308 
lemma degree_polymul:


1309 
assumes "SORT_CONSTRAINT('a::{ring_char_0,division_by_zero,field})"


1310 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1"


1311 
shows "degree (p *\<^sub>p q) \<le> degree p + degree q"


1312 
using polymul_degreen[OF np nq, where m="0"] degree_eq_degreen0 by simp


1313 


1314 
lemma polyneg_degree: "isnpolyh p n \<Longrightarrow> degree (polyneg p) = degree p"


1315 
by (induct p arbitrary: n rule: degree.induct, auto)


1316 


1317 
lemma polyneg_head: "isnpolyh p n \<Longrightarrow> head(polyneg p) = polyneg (head p)"


1318 
by (induct p arbitrary: n rule: degree.induct, auto)


1319 


1320 
subsection {* Correctness of polynomial pseudo division *}


1321 


1322 
lemma polydivide_aux_real_domintros:


1323 
assumes call1: "\<lbrakk>s \<noteq> 0\<^sub>p; \<not> degree s < n; a = head s\<rbrakk>


1324 
\<Longrightarrow> polydivide_aux_dom (a, n, p, k, s \<^sub>p funpow (degree s  n) shift1 p)"


1325 
and call2 