(* 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))"
fun decrpoly:: "poly \ poly"
where
"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 *}
fun degree:: "poly \ nat"
where
"degree (CN c 0 p) = 1 + degree p"
| "degree p = 0"
fun head:: "poly \ poly"
where
"head (CN c 0 p) = head p"
| "head p = p"
(* More general notions of degree and head *)
fun degreen:: "poly \ nat \ nat"
where
"degreen (CN c n p) = (\m. if n=m then 1 + degreen p n else 0)"
|"degreen p = (\m. 0)"
fun headn:: "poly \ nat \ poly"
where
"headn (CN c n p) = (\m. if n \ m then headn p m else CN c n p)"
| "headn p = (\m. p)"
fun coefficients:: "poly \ poly list"
where
"coefficients (CN c 0 p) = c#(coefficients p)"
| "coefficients p = [p]"
fun isconstant:: "poly \ bool"
where
"isconstant (CN c 0 p) = False"
| "isconstant p = True"
fun behead:: "poly \ poly"
where
"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"
fun headconst:: "poly \ Num"
where
"headconst (CN c n p) = headconst p"
| "headconst (C n) = n"
subsection{* Operations for normalization *}
declare if_cong[fundef_cong del]
declare let_cong[fundef_cong del]
fun polyadd :: "poly \ poly \ poly" (infixl "+\<^sub>p" 60)
where
"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"
| "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"
fun polyneg :: "poly \ poly" ("~\<^sub>p")
where
"polyneg (C c) = C (~\<^sub>N c)"
| "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)"
| "polyneg a = Neg a"
definition polysub :: "poly \ poly \ poly" (infixl "-\<^sub>p" 60)
where
"p -\<^sub>p q = polyadd p (polyneg q)"
fun polymul :: "poly \ poly \ poly" (infixl "*\<^sub>p" 60)
where
"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"
declare if_cong[fundef_cong]
declare let_cong[fundef_cong]
fun polypow :: "nat \ poly \ poly"
where
"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)"
abbreviation poly_pow :: "poly \ nat \ poly" (infixl "^\<^sub>p" 60)
where "a ^\<^sub>p k \ polypow k a"
function polynate :: "poly \ poly"
where
"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)"
by pat_completeness auto
termination by (relation "measure polysize") auto
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 *}
fun isnpolyh:: "poly \ nat \ bool"
where
"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 ab c' n' p' n0 n1)
from 2 have th1: "isnpolyh (C ab) (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 ab +\<^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' ab n1 n0)
from 3 have th1: "isnpolyh (C ab) (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 ab) (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.hyps"(3)[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.hyps"(4)[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 4 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 lt 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.hyps"(1)[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 gt 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.hyps"(2)[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(4)[of n n m] 4(3)[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(4)[of n n m] 4(3)[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)
by blast
}
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 c c' n' p')
{ case (1 n0 n1)
with "2.hyps"(4-6)[of n' n' n']
and "2.hyps"(1-3)[of "Suc n'" "Suc n'" n']
show ?case by (auto simp add: min_def)
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 c')
{ case (1 n0 n1)
with "3.hyps"(4-6)[of n n n]
"3.hyps"(1-3)[of "Suc n" "Suc n" n]
show ?case by (auto simp add: min_def)
next
case (2 n0 n1) thus ?case by auto
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'"
{
case (1 n0 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
{ assume "n < n'"
with "4.hyps"(4-5)[OF np cnp', of n]
"4.hyps"(1)[OF nc cnp', of n] nn0 cnp
have ?case by (simp add: min_def)
} moreover {
assume "n' < n"
with "4.hyps"(16-17)[OF cnp np', of "n'"]
"4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp'
have ?case
by (cases "Suc n' = n", simp_all add: min_def)
} moreover {
assume "n' = n"
with "4.hyps"(16-17)[OF cnp np', of n]
"4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0
have ?case
apply (auto intro!: polyadd_normh)
apply (simp_all add: min_def isnpolyh_mono[OF nn0])
done
}
ultimately show ?case by arith
next
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"(3,6,18) np np' m
have ?eq by auto }
moreover
{assume nn': "n' = n" hence nn:"\ n' < n \ \ n < n'" by arith
from "4.hyps"(16,18)[of n n' n]
"4.hyps"(13,14)[of n "Suc n'" 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"(17,18)[OF norm(1,4), of n]
"4.hyps"(13,15)[OF norm(1,2), of 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"(16-18)[OF norm(1,4), of n]
"4.hyps"(13-15)[OF norm(1,2), of 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
from "4.hyps"(16-18)[OF norm(1,4) min1]
"4.hyps"(13-15)[OF 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' np np' by simp
with "4.hyps"(16-18)[OF norm(1,4) min1]
"4.hyps"(13-15)[OF norm(1,2) min2]
degreen_0[OF norm(3) mn']
have ?eq using nn' mn np np' by clarsimp}
ultimately have ?eq by blast}
ultimately show ?eq by blast}
{ 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 polymul)
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 \ isnpolyh (f p) n "and np: "isnpolyh p n"
shows "isnpolyh (funpow k f p) n"
using f np by (induct k arbitrary: p, auto)
lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)"
by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc )
lemma shift1_isnpolyh: "isnpolyh p n0 \ p\ 0\<^sub>p \ isnpolyh (shift1 p) 0"
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def)
lemma funpow_shift1_1:
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)"
by (simp add: funpow_shift1)
lemma poly_cmul[simp]: "Ipoly bs (poly_cmul c p) = Ipoly bs (Mul (C c) p)"
by (induct p arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps)
lemma behead:
assumes np: "isnpolyh p n"
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})"
using np
proof (induct p arbitrary: n rule: behead.induct)
case (1 c p n) hence pn: "isnpolyh p n" by simp
from 1(1)[OF pn]
have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" .
then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p")
by (simp_all add: th[symmetric] field_simps power_Suc)
qed (auto simp add: Let_def)
lemma behead_isnpolyh:
assumes np: "isnpolyh p n" shows "isnpolyh (behead p) n"
using np by (induct p rule: behead.induct, auto simp add: Let_def isnpolyh_mono)
subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *}
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \ polybound0 p"
proof(induct p arbitrary: n rule: poly.induct, auto)
case (goal1 c n p n')
hence "n = Suc (n - 1)" by simp
hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp
with goal1(2) show ?case by simp
qed
lemma isconstant_polybound0: "isnpolyh p n0 \ isconstant p \ polybound0 p"
by (induct p arbitrary: n0 rule: isconstant.induct, auto simp add: isnpolyh_polybound0)
lemma decrpoly_zero[simp]: "decrpoly p = 0\<^sub>p \ p = 0\<^sub>p" by (induct p, auto)
lemma decrpoly_normh: "isnpolyh p n0 \ polybound0 p \ isnpolyh (decrpoly p) (n0 - 1)"
apply (induct p arbitrary: n0, auto)
apply (atomize)
apply (erule_tac x = "Suc nat" in allE)
apply auto
done
lemma head_polybound0: "isnpolyh p n0 \ polybound0 (head p)"
by (induct p arbitrary: n0 rule: head.induct, auto intro: isnpolyh_polybound0)
lemma polybound0_I:
assumes nb: "polybound0 a"
shows "Ipoly (b#bs) a = Ipoly (b'#bs) a"
using nb
by (induct a rule: poly.induct) auto
lemma polysubst0_I:
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t"
by (induct t) simp_all
lemma polysubst0_I':
assumes nb: "polybound0 a"
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b'#bs) a)#bs) t"
by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"])
lemma decrpoly: assumes nb: "polybound0 t"
shows "Ipoly (x#bs) t = Ipoly bs (decrpoly t)"
using nb by (induct t rule: decrpoly.induct, simp_all)
lemma polysubst0_polybound0: assumes nb: "polybound0 t"
shows "polybound0 (polysubst0 t a)"
using nb by (induct a rule: poly.induct, auto)
lemma degree0_polybound0: "isnpolyh p n \ degree p = 0 \ polybound0 p"
by (induct p arbitrary: n rule: degree.induct, auto simp add: isnpolyh_polybound0)
primrec maxindex :: "poly \ nat" where
"maxindex (Bound n) = n + 1"
| "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))"
| "maxindex (Add p q) = max (maxindex p) (maxindex q)"
| "maxindex (Sub p q) = max (maxindex p) (maxindex q)"
| "maxindex (Mul p q) = max (maxindex p) (maxindex q)"
| "maxindex (Neg p) = maxindex p"
| "maxindex (Pw p n) = maxindex p"
| "maxindex (C x) = 0"
definition wf_bs :: "'a list \ poly \ bool" where
"wf_bs bs p = (length bs \ maxindex p)"
lemma wf_bs_coefficients: "wf_bs bs p \ \ c \ set (coefficients p). wf_bs bs c"
proof(induct p rule: coefficients.induct)
case (1 c p)
show ?case
proof
fix x assume xc: "x \ set (coefficients (CN c 0 p))"
hence "x = c \ x \ set (coefficients p)" by simp
moreover
{assume "x = c" hence "wf_bs bs x" using "1.prems" unfolding wf_bs_def by simp}
moreover
{assume H: "x \