(* Title: HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy
Author: Amine Chaieb
*)
header {* Implementation and verification of multivariate polynomials *}
theory Reflected_Multivariate_Polynomial
imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List
begin
(* Implementation *)
subsection{* Datatype of polynomial expressions *}
datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
| Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \ C (0\<^sub>N)"
abbreviation poly_p :: "int \ poly" ("_\<^sub>p") where "i\<^sub>p \ C (i\<^sub>N)"
subsection{* Boundedness, substitution and all that *}
primrec polysize:: "poly \ nat" where
"polysize (C c) = 1"
| "polysize (Bound n) = 1"
| "polysize (Neg p) = 1 + polysize p"
| "polysize (Add p q) = 1 + polysize p + polysize q"
| "polysize (Sub p q) = 1 + polysize p + polysize q"
| "polysize (Mul p q) = 1 + polysize p + polysize q"
| "polysize (Pw p n) = 1 + polysize p"
| "polysize (CN c n p) = 4 + polysize c + polysize p"
primrec polybound0:: "poly \ bool" (* a poly is INDEPENDENT of Bound 0 *) where
"polybound0 (C c) = True"
| "polybound0 (Bound n) = (n>0)"
| "polybound0 (Neg a) = polybound0 a"
| "polybound0 (Add a b) = (polybound0 a \ polybound0 b)"
| "polybound0 (Sub a b) = (polybound0 a \ polybound0 b)"
| "polybound0 (Mul a b) = (polybound0 a \ polybound0 b)"
| "polybound0 (Pw p n) = (polybound0 p)"
| "polybound0 (CN c n p) = (n \ 0 \ polybound0 c \ polybound0 p)"
primrec polysubst0:: "poly \ poly \ poly" (* substitute a poly into a poly for Bound 0 *) where
"polysubst0 t (C c) = (C c)"
| "polysubst0 t (Bound n) = (if n=0 then t else Bound n)"
| "polysubst0 t (Neg a) = Neg (polysubst0 t a)"
| "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)"
| "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)"
| "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)"
| "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n"
| "polysubst0 t (CN c n p) = (if n=0 then Add (polysubst0 t c) (Mul t (polysubst0 t p))
else CN (polysubst0 t c) n (polysubst0 t p))"
consts
decrpoly:: "poly \ poly"
recdef decrpoly "measure polysize"
"decrpoly (Bound n) = Bound (n - 1)"
"decrpoly (Neg a) = Neg (decrpoly a)"
"decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)"
"decrpoly (Sub a b) = Sub (decrpoly a) (decrpoly b)"
"decrpoly (Mul a b) = Mul (decrpoly a) (decrpoly b)"
"decrpoly (Pw p n) = Pw (decrpoly p) n"
"decrpoly (CN c n p) = CN (decrpoly c) (n - 1) (decrpoly p)"
"decrpoly a = a"
subsection{* Degrees and heads and coefficients *}
consts degree:: "poly \ nat"
recdef degree "measure size"
"degree (CN c 0 p) = 1 + degree p"
"degree p = 0"
consts head:: "poly \ poly"
recdef head "measure size"
"head (CN c 0 p) = head p"
"head p = p"
(* More general notions of degree and head *)
consts degreen:: "poly \ nat \ nat"
recdef degreen "measure size"
"degreen (CN c n p) = (\m. if n=m then 1 + degreen p n else 0)"
"degreen p = (\m. 0)"
consts headn:: "poly \ nat \ poly"
recdef headn "measure size"
"headn (CN c n p) = (\m. if n \ m then headn p m else CN c n p)"
"headn p = (\m. p)"
consts coefficients:: "poly \ poly list"
recdef coefficients "measure size"
"coefficients (CN c 0 p) = c#(coefficients p)"
"coefficients p = [p]"
consts isconstant:: "poly \ bool"
recdef isconstant "measure size"
"isconstant (CN c 0 p) = False"
"isconstant p = True"
consts behead:: "poly \ poly"
recdef behead "measure size"
"behead (CN c 0 p) = (let p' = behead p in if p' = 0\<^sub>p then c else CN c 0 p')"
"behead p = 0\<^sub>p"
consts headconst:: "poly \ Num"
recdef headconst "measure size"
"headconst (CN c n p) = headconst p"
"headconst (C n) = n"
subsection{* Operations for normalization *}
consts
polyadd :: "poly\poly \ poly"
polyneg :: "poly \ poly" ("~\<^sub>p")
polysub :: "poly\poly \ poly"
polymul :: "poly\poly \ poly"
polypow :: "nat \ poly \ poly"
abbreviation poly_add :: "poly \ poly \ poly" (infixl "+\<^sub>p" 60)
where "a +\<^sub>p b \ polyadd (a,b)"
abbreviation poly_mul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60)
where "a *\<^sub>p b \ polymul (a,b)"
abbreviation poly_sub :: "poly \ poly \ poly" (infixl "-\<^sub>p" 60)
where "a -\<^sub>p b \ polysub (a,b)"
abbreviation poly_pow :: "poly \ nat \ poly" (infixl "^\<^sub>p" 60)
where "a ^\<^sub>p k \ polypow k a"
recdef polyadd "measure (\ (a,b). polysize a + polysize b)"
"polyadd (C c, C c') = C (c+\<^sub>Nc')"
"polyadd (C c, CN c' n' p') = CN (polyadd (C c, c')) n' p'"
"polyadd (CN c n p, C c') = CN (polyadd (c, C c')) n p"
stupid: "polyadd (CN c n p, CN c' n' p') =
(if n < n' then CN (polyadd(c,CN c' n' p')) n p
else if n'p then cc' else CN cc' n pp')))"
"polyadd (a, b) = Add a b"
(hints recdef_simp add: Let_def measure_def split_def inv_image_def recdef_cong del: if_cong)
recdef polyneg "measure size"
"polyneg (C c) = C (~\<^sub>N c)"
"polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
"polyneg a = Neg a"
defs polysub_def[code]: "polysub \ \ (p,q). polyadd (p,polyneg q)"
recdef polymul "measure (\(a,b). size a + size b)"
"polymul(C c, C c') = C (c*\<^sub>Nc')"
"polymul(C c, CN c' n' p') =
(if c = 0\<^sub>N then 0\<^sub>p else CN (polymul(C c,c')) n' (polymul(C c, p')))"
"polymul(CN c n p, C c') =
(if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul(c,C c')) n (polymul(p, C c')))"
"polymul(CN c n p, CN c' n' p') =
(if np n' (polymul(CN c n p, p'))))"
"polymul (a,b) = Mul a b"
recdef polypow "measure id"
"polypow 0 = (\p. 1\<^sub>p)"
"polypow n = (\p. let q = polypow (n div 2) p ; d = polymul(q,q) in
if even n then d else polymul(p,d))"
consts polynate :: "poly \ poly"
recdef polynate "measure polysize"
"polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p"
"polynate (Add p q) = (polynate p +\<^sub>p polynate q)"
"polynate (Sub p q) = (polynate p -\<^sub>p polynate q)"
"polynate (Mul p q) = (polynate p *\<^sub>p polynate q)"
"polynate (Neg p) = (~\<^sub>p (polynate p))"
"polynate (Pw p n) = ((polynate p) ^\<^sub>p n)"
"polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))"
"polynate (C c) = C (normNum c)"
fun poly_cmul :: "Num \ poly \ poly" where
"poly_cmul y (C x) = C (y *\<^sub>N x)"
| "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)"
| "poly_cmul y p = C y *\<^sub>p p"
definition monic :: "poly \ (poly \ bool)" where
"monic p \ (let h = headconst p in if h = 0\<^sub>N then (p,False) else ((C (Ninv h)) *\<^sub>p p, 0>\<^sub>N h))"
subsection{* Pseudo-division *}
definition shift1 :: "poly \ poly" where
"shift1 p \ CN 0\<^sub>p 0 p"
abbreviation funpow :: "nat \ ('a \ 'a) \ ('a \ 'a)" where
"funpow \ compow"
partial_function (tailrec) polydivide_aux :: "poly \ nat \ poly \ nat \ poly \ nat \ poly"
where
"polydivide_aux a n p k s =
(if s = 0\<^sub>p then (k,s)
else (let b = head s; m = degree s in
(if m < n then (k,s) else
(let p'= funpow (m - n) shift1 p in
(if a = b then polydivide_aux a n p k (s -\<^sub>p p')
else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) -\<^sub>p (b *\<^sub>p p')))))))"
definition polydivide :: "poly \ poly \ (nat \ poly)" where
"polydivide s p \ polydivide_aux (head p) (degree p) p 0 s"
fun poly_deriv_aux :: "nat \ poly \ poly" where
"poly_deriv_aux n (CN c 0 p) = CN (poly_cmul ((int n)\<^sub>N) c) 0 (poly_deriv_aux (n + 1) p)"
| "poly_deriv_aux n p = poly_cmul ((int n)\<^sub>N) p"
fun poly_deriv :: "poly \ poly" where
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p"
| "poly_deriv p = 0\<^sub>p"
(* Verification *)
lemma nth_pos2[simp]: "0 < n \ (x#xs) ! n = xs ! (n - 1)"
using Nat.gr0_conv_Suc
by clarsimp
subsection{* Semantics of the polynomial representation *}
primrec Ipoly :: "'a list \ poly \ 'a::{field_char_0, field_inverse_zero, power}" where
"Ipoly bs (C c) = INum c"
| "Ipoly bs (Bound n) = bs!n"
| "Ipoly bs (Neg a) = - Ipoly bs a"
| "Ipoly bs (Add a b) = Ipoly bs a + Ipoly bs b"
| "Ipoly bs (Sub a b) = Ipoly bs a - Ipoly bs b"
| "Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
| "Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
| "Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
abbreviation
Ipoly_syntax :: "poly \ 'a list \'a::{field_char_0, field_inverse_zero, power}" ("\_\\<^sub>p\<^bsup>_\<^esup>")
where "\p\\<^sub>p\<^bsup>bs\<^esup> \ Ipoly bs p"
lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
by (simp add: INum_def)
lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j"
by (simp add: INum_def)
lemmas RIpoly_eqs = Ipoly.simps(2-7) Ipoly_CInt Ipoly_CRat
subsection {* Normal form and normalization *}
consts isnpolyh:: "poly \ nat \ bool"
recdef isnpolyh "measure size"
"isnpolyh (C c) = (\k. isnormNum c)"
"isnpolyh (CN c n p) = (\k. n\ k \ (isnpolyh c (Suc n)) \ (isnpolyh p n) \ (p \ 0\<^sub>p))"
"isnpolyh p = (\k. False)"
lemma isnpolyh_mono: "\n' \ n ; isnpolyh p n\ \ isnpolyh p n'"
by (induct p rule: isnpolyh.induct, auto)
definition isnpoly :: "poly \ bool" where
"isnpoly p \ isnpolyh p 0"
text{* polyadd preserves normal forms *}
lemma polyadd_normh: "\isnpolyh p n0 ; isnpolyh q n1\
\ isnpolyh (polyadd(p,q)) (min n0 n1)"
proof(induct p q arbitrary: n0 n1 rule: polyadd.induct)
case (2 a b c' n' p' n0 n1)
from 2 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp
from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" by simp_all
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp
from nplen1 have n01len1: "min n0 n1 \ n'" by simp
thus ?case using 2 th3 by simp
next
case (3 c' n' p' a b n1 n0)
from 3 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp
from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \ n1" by simp_all
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp
with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp
from nplen1 have n01len1: "min n0 n1 \ n'" by simp
thus ?case using 3 th3 by simp
next
case (4 c n p c' n' p' n0 n1)
hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all
from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all
from 4 have ngen0: "n \ n0" by simp
from 4 have n'gen1: "n' \ n1" by simp
have "n < n' \ n' < n \ n = n'" by auto
moreover {assume eq: "n = n'"
with 4(2)[OF nc nc']
have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto
hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)"
using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto
from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp
have minle: "min n0 n1 \ n'" using ngen0 n'gen1 eq by simp
from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)}
moreover {assume lt: "n < n'"
have "min n0 n1 \ n0" by simp
with 4 have th1:"min n0 n1 \ n" by auto
from 4 have th21: "isnpolyh c (Suc n)" by simp
from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp
from lt have th23: "min (Suc n) n' = Suc n" by arith
from 4(4)[OF th21 th22]
have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp
with 4 lt th1 have ?case by simp }
moreover {assume gt: "n' < n" hence gt': "n' < n \ \ n < n'" by simp
have "min n0 n1 \ n1" by simp
with 4 have th1:"min n0 n1 \ n'" by auto
from 4 have th21: "isnpolyh c' (Suc n')" by simp_all
from 4 have th22: "isnpolyh (CN c n p) n" by simp
from gt have th23: "min n (Suc n') = Suc n'" by arith
from 4(3)[OF th22 th21]
have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp
with 4 gt th1 have ?case by simp}
ultimately show ?case by blast
qed auto
lemma polyadd[simp]: "Ipoly bs (polyadd (p,q)) = (Ipoly bs p) + (Ipoly bs q)"
by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib)
lemma polyadd_norm: "\ isnpoly p ; isnpoly q\ \ isnpoly (polyadd(p,q))"
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp
text{* The degree of addition and other general lemmas needed for the normal form of polymul *}
lemma polyadd_different_degreen:
"\isnpolyh p n0 ; isnpolyh q n1; degreen p m \ degreen q m ; m \ min n0 n1\ \
degreen (polyadd(p,q)) m = max (degreen p m) (degreen q m)"
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct)
case (4 c n p c' n' p' m n0 n1)
have "n' = n \ n < n' \ n' < n" by arith
thus ?case
proof (elim disjE)
assume [simp]: "n' = n"
from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
show ?thesis by (auto simp: Let_def)
next
assume "n < n'"
with 4 show ?thesis by auto
next
assume "n' < n"
with 4 show ?thesis by auto
qed
qed auto
lemma headnz[simp]: "\isnpolyh p n ; p \ 0\<^sub>p\ \ headn p m \ 0\<^sub>p"
by (induct p arbitrary: n rule: headn.induct, auto)
lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \ degree p = 0"
by (induct p arbitrary: n rule: degree.induct, auto)
lemma degreen_0[simp]: "isnpolyh p n \ m < n \ degreen p m = 0"
by (induct p arbitrary: n rule: degreen.induct, auto)
lemma degree_isnpolyh_Suc': "n > 0 \ isnpolyh p n \ degree p = 0"
by (induct p arbitrary: n rule: degree.induct, auto)
lemma degree_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degree c = 0"
using degree_isnpolyh_Suc by auto
lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \ degreen c n = 0"
using degreen_0 by auto
lemma degreen_polyadd:
assumes np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ max n0 n1"
shows "degreen (p +\<^sub>p q) m \ max (degreen p m) (degreen q m)"
using np nq m
proof (induct p q arbitrary: n0 n1 m rule: polyadd.induct)
case (2 c c' n' p' n0 n1) thus ?case by (cases n', simp_all)
next
case (3 c n p c' n0 n1) thus ?case by (cases n, auto)
next
case (4 c n p c' n' p' n0 n1 m)
have "n' = n \ n < n' \ n' < n" by arith
thus ?case
proof (elim disjE)
assume [simp]: "n' = n"
from 4(1)[of n n m] 4(2)[of "Suc n" "Suc n" m] 4(5-7)
show ?thesis by (auto simp: Let_def)
qed simp_all
qed auto
lemma polyadd_eq_const_degreen: "\ isnpolyh p n0 ; isnpolyh q n1 ; polyadd (p,q) = C c\
\ degreen p m = degreen q m"
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct)
case (4 c n p c' n' p' m n0 n1 x)
{assume nn': "n' < n" hence ?case using 4 by simp}
moreover
{assume nn':"\ n' < n" hence "n < n' \ n = n'" by arith
moreover {assume "n < n'" with 4 have ?case by simp }
moreover {assume eq: "n = n'" hence ?case using 4
apply (cases "p +\<^sub>p p' = 0\<^sub>p")
apply (auto simp add: Let_def)
apply blast
done
}
ultimately have ?case by blast}
ultimately show ?case by blast
qed simp_all
lemma polymul_properties:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \ min n0 n1"
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)"
and "(p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p)"
and "degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0
else degreen p m + degreen q m)"
using np nq m
proof(induct p q arbitrary: n0 n1 m rule: polymul.induct)
case (2 a b c' n' p')
let ?c = "(a,b)"
{ case (1 n0 n1)
hence n: "isnpolyh (C ?c) n'" "isnpolyh c' (Suc n')" "isnpolyh p' n'" "isnormNum ?c"
"isnpolyh (CN c' n' p') n1"
by simp_all
{assume "?c = 0\<^sub>N" hence ?case by auto}
moreover {assume cnz: "?c \ 0\<^sub>N"
from "2.hyps"(1)[rule_format,where xb="n'", OF cnz n(1) n(3)]
"2.hyps"(2)[rule_format, where x="Suc n'"
and xa="Suc n'" and xb = "n'", OF cnz ] cnz n have ?case
by (auto simp add: min_def)}
ultimately show ?case by blast
next
case (2 n0 n1) thus ?case by auto
next
case (3 n0 n1) thus ?case using "2.hyps" by auto }
next
case (3 c n p a b){
let ?c' = "(a,b)"
case (1 n0 n1)
hence n: "isnpolyh (C ?c') n" "isnpolyh c (Suc n)" "isnpolyh p n" "isnormNum ?c'"
"isnpolyh (CN c n p) n0"
by simp_all
{assume "?c' = 0\<^sub>N" hence ?case by auto}
moreover {assume cnz: "?c' \ 0\<^sub>N"
from "3.hyps"(1)[rule_format,where xb="n", OF cnz n(3) n(1)]
"3.hyps"(2)[rule_format, where x="Suc n"
and xa="Suc n" and xb = "n", OF cnz ] cnz n have ?case
by (auto simp add: min_def)}
ultimately show ?case by blast
next
case (2 n0 n1) thus ?case apply auto done
next
case (3 n0 n1) thus ?case using "3.hyps" by auto }
next
case (4 c n p c' n' p')
let ?cnp = "CN c n p" let ?cnp' = "CN c' n' p'"
{fix n0 n1
assume "isnpolyh ?cnp n0" and "isnpolyh ?cnp' n1"
hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'"
and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)"
and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')"
and nn0: "n \ n0" and nn1:"n' \ n1"
by simp_all
have "n < n' \ n' < n \ n' = n" by auto
moreover
{assume nn': "n < n'"
with "4.hyps"(5)[rule_format, OF nn' np cnp', where xb ="n"]
"4.hyps"(6)[rule_format, OF nn' nc cnp', where xb="n"] nn' nn0 nn1 cnp
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
by (simp add: min_def) }
moreover
{assume nn': "n > n'" hence stupid: "n' < n \ \ n < n'" by arith
with "4.hyps"(3)[rule_format, OF stupid cnp np', where xb="n'"]
"4.hyps"(4)[rule_format, OF stupid cnp nc', where xb="Suc n'"]
nn' nn0 nn1 cnp'
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
by (cases "Suc n' = n", simp_all add: min_def)}
moreover
{assume nn': "n' = n" hence stupid: "\ n' < n \ \ n < n'" by arith
from "4.hyps"(1)[rule_format, OF stupid cnp np', where xb="n"]
"4.hyps"(2)[rule_format, OF stupid cnp nc', where xb="n"] nn' cnp cnp' nn1
have "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)"
by simp (rule polyadd_normh,simp_all add: min_def isnpolyh_mono[OF nn0]) }
ultimately show "isnpolyh (?cnp *\<^sub>p ?cnp') (min n0 n1)" by blast }
note th = this
{fix n0 n1 m
assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1"
and m: "m \ min n0 n1"
let ?d = "degreen (?cnp *\<^sub>p ?cnp') m"
let ?d1 = "degreen ?cnp m"
let ?d2 = "degreen ?cnp' m"
let ?eq = "?d = (if ?cnp = 0\<^sub>p \ ?cnp' = 0\<^sub>p then 0 else ?d1 + ?d2)"
have "n' n < n' \ n' = n" by auto
moreover
{assume "n' < n \ n < n'"
with "4.hyps" np np' m
have ?eq apply (cases "n' < n", simp_all)
apply (erule allE[where x="n"],erule allE[where x="n"],auto)
done }
moreover
{assume nn': "n' = n" hence nn:"\ n' < n \ \ n < n'" by arith
from "4.hyps"(1)[rule_format, OF nn, where x="n" and xa ="n'" and xb="n"]
"4.hyps"(2)[rule_format, OF nn, where x="n" and xa ="Suc n'" and xb="n"]
np np' nn'
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n"
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
"?cnp *\<^sub>p p' \ 0\<^sub>p" by (auto simp add: min_def)
{assume mn: "m = n"
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"] norm nn' mn
have degs: "degreen (?cnp *\<^sub>p c') n =
(if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)"
"degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def)
from degs norm
have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp
hence neq: "degreen (?cnp *\<^sub>p c') n \ degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
by simp
have nmin: "n \ min n n" by (simp add: min_def)
from polyadd_different_degreen[OF norm(3,6) neq nmin] th1
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
from "4.hyps"(1)[rule_format, OF nn norm(1,4), where xb="n"]
"4.hyps"(2)[rule_format, OF nn norm(1,2), where xb="n"]
mn norm m nn' deg
have ?eq by simp}
moreover
{assume mn: "m \ n" hence mn': "m < n" using m np by auto
from nn' m np have max1: "m \ max n n" by simp
hence min1: "m \ min n n" by simp
hence min2: "m \ min n (Suc n)" by simp
{assume "c' = 0\<^sub>p"
from `c' = 0\<^sub>p` have ?eq
using "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2] mn nn'
apply simp
done}
moreover
{assume cnz: "c' \ 0\<^sub>p"
from "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
degreen_polyadd[OF norm(3,6) max1]
have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m
\ max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)"
using mn nn' cnz np np' by simp
with "4.hyps"(1)[rule_format, OF nn norm(1,4) min1]
"4.hyps"(2)[rule_format, OF nn norm(1,2) min2]
degreen_0[OF norm(3) mn'] have ?eq using nn' mn cnz np np' by clarsimp}
ultimately have ?eq by blast }
ultimately have ?eq by blast}
ultimately show ?eq by blast}
note degth = this
{ case (2 n0 n1)
hence np: "isnpolyh ?cnp n0" and np': "isnpolyh ?cnp' n1"
and m: "m \ min n0 n1" by simp_all
hence mn: "m \ n" by simp
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')"
{assume C: "?cnp *\<^sub>p c' +\<^sub>p ?c0p = 0\<^sub>p" "n' = n"
hence nn: "\n' < n \ \ np c') n"
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n"
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)"
"?cnp *\<^sub>p p' \ 0\<^sub>p"
"degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)"
"degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n"
by (simp_all add: min_def)
from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp
have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n"
using norm by simp
from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq
have "False" by simp }
thus ?case using "4.hyps" by clarsimp}
qed auto
lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = (Ipoly bs p) * (Ipoly bs q)"
by(induct p q rule: polymul.induct, auto simp add: field_simps)
lemma polymul_normh:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (p *\<^sub>p q) (min n0 n1)"
using polymul_properties(1) by blast
lemma polymul_eq0_iff:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p *\<^sub>p q = 0\<^sub>p) = (p = 0\<^sub>p \ q = 0\<^sub>p) "
using polymul_properties(2) by blast
lemma polymul_degreen:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\ isnpolyh p n0 ; isnpolyh q n1 ; m \ min n0 n1\ \ degreen (p *\<^sub>p q) m = (if (p = 0\<^sub>p \ q = 0\<^sub>p) then 0 else degreen p m + degreen q m)"
using polymul_properties(3) by blast
lemma polymul_norm:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\ isnpoly p; isnpoly q\ \ isnpoly (polymul (p,q))"
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp
lemma headconst_zero: "isnpolyh p n0 \ headconst p = 0\<^sub>N \ p = 0\<^sub>p"
by (induct p arbitrary: n0 rule: headconst.induct, auto)
lemma headconst_isnormNum: "isnpolyh p n0 \ isnormNum (headconst p)"
by (induct p arbitrary: n0, auto)
lemma monic_eqI: assumes np: "isnpolyh p n0"
shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})"
unfolding monic_def Let_def
proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np])
let ?h = "headconst p"
assume pz: "p \ 0\<^sub>p"
{assume hz: "INum ?h = (0::'a)"
from headconst_isnormNum[OF np] have norm: "isnormNum ?h" "isnormNum 0\<^sub>N" by simp_all
from isnormNum_unique[where ?'a = 'a, OF norm] hz have "?h = 0\<^sub>N" by simp
with headconst_zero[OF np] have "p =0\<^sub>p" by blast with pz have "False" by blast}
thus "INum (headconst p) = (0::'a) \ \p\\<^sub>p\<^bsup>bs\<^esup> = 0" by blast
qed
text{* polyneg is a negation and preserves normal forms *}
lemma polyneg[simp]: "Ipoly bs (polyneg p) = - Ipoly bs p"
by (induct p rule: polyneg.induct, auto)
lemma polyneg0: "isnpolyh p n \ ((~\<^sub>p p) = 0\<^sub>p) = (p = 0\<^sub>p)"
by (induct p arbitrary: n rule: polyneg.induct, auto simp add: Nneg_def)
lemma polyneg_polyneg: "isnpolyh p n0 \ ~\<^sub>p (~\<^sub>p p) = p"
by (induct p arbitrary: n0 rule: polyneg.induct, auto)
lemma polyneg_normh: "\n. isnpolyh p n \ isnpolyh (polyneg p) n "
by (induct p rule: polyneg.induct, auto simp add: polyneg0)
lemma polyneg_norm: "isnpoly p \ isnpoly (polyneg p)"
using isnpoly_def polyneg_normh by simp
text{* polysub is a substraction and preserves normal forms *}
lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p) - (Ipoly bs q)"
by (simp add: polysub_def polyneg polyadd)
lemma polysub_normh: "\ n0 n1. \ isnpolyh p n0 ; isnpolyh q n1\ \ isnpolyh (polysub(p,q)) (min n0 n1)"
by (simp add: polysub_def polyneg_normh polyadd_normh)
lemma polysub_norm: "\ isnpoly p; isnpoly q\ \ isnpoly (polysub(p,q))"
using polyadd_norm polyneg_norm by (simp add: polysub_def)
lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpolyh p n0 \ polysub (p, p) = 0\<^sub>p"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p arbitrary: n0,auto simp add: Let_def Nsub0[simplified Nsub_def])
lemma polysub_0:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "\ isnpolyh p n0 ; isnpolyh q n1\ \ (p -\<^sub>p q = 0\<^sub>p) = (p = q)"
unfolding polysub_def split_def fst_conv snd_conv
by (induct p q arbitrary: n0 n1 rule:polyadd.induct)
(auto simp: Nsub0[simplified Nsub_def] Let_def)
text{* polypow is a power function and preserves normal forms *}
lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n"
proof(induct n rule: polypow.induct)
case 1 thus ?case by simp
next
case (2 n)
let ?q = "polypow ((Suc n) div 2) p"
let ?d = "polymul(?q,?q)"
have "odd (Suc n) \ even (Suc n)" by simp
moreover
{assume odd: "odd (Suc n)"
have th: "(Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat))))) = Suc n div 2 + Suc n div 2 + 1" by arith
from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul(p, ?d))" by (simp add: Let_def)
also have "\ = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)"
using "2.hyps" by simp
also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)"
apply (simp only: power_add power_one_right) by simp
also have "\ = (Ipoly bs p) ^ (Suc (Suc (Suc (0\nat)) * (Suc n div Suc (Suc (0\nat)))))"
by (simp only: th)
finally have ?case
using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp }
moreover
{assume even: "even (Suc n)"
have th: "(Suc (Suc (0\nat))) * (Suc n div Suc (Suc (0\nat))) = Suc n div 2 + Suc n div 2" by arith
from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" by (simp add: Let_def)
also have "\ = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)"
using "2.hyps" apply (simp only: power_add) by simp
finally have ?case using even_nat_div_two_times_two[OF even] by (simp only: th)}
ultimately show ?case by blast
qed
lemma polypow_normh:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpolyh p n \ isnpolyh (polypow k p) n"
proof (induct k arbitrary: n rule: polypow.induct)
case (2 k n)
let ?q = "polypow (Suc k div 2) p"
let ?d = "polymul (?q,?q)"
from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+
from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp
from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp
from dn on show ?case by (simp add: Let_def)
qed auto
lemma polypow_norm:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpoly p \ isnpoly (polypow k p)"
by (simp add: polypow_normh isnpoly_def)
text{* Finally the whole normalization *}
lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})"
by (induct p rule:polynate.induct, auto)
lemma polynate_norm[simp]:
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})"
shows "isnpoly (polynate p)"
by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def)
text{* shift1 *}
lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)"
by (simp add: shift1_def)
lemma shift1_isnpoly:
assumes pn: "isnpoly p" and pnz: "p \ 0\<^sub>p" shows "isnpoly (shift1 p) "
using pn pnz by (simp add: shift1_def isnpoly_def )
lemma shift1_nz[simp]:"shift1 p \ 0\<^sub>p"
by (simp add: shift1_def)
lemma funpow_shift1_isnpoly:
"\ isnpoly p ; p \ 0\<^sub>p\ \ isnpoly (funpow n shift1 p)"
by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1)
lemma funpow_isnpolyh:
assumes f: "\ p. isnpolyh p n \