author  krauss 
Mon, 21 Feb 2011 23:14:36 +0100  
changeset 41813  4eb43410d2fa 
parent 41812  d46c2908a838 
child 41814  3848eb635eab 
permissions  rwrr 
33154  1 
(* Title: HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy 
2 
Author: Amine Chaieb 

3 
*) 

4 

35046  5 
header {* Implementation and verification of multivariate polynomials *} 
33154  6 

7 
theory Reflected_Multivariate_Polynomial 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41404
diff
changeset

8 
imports Complex_Main "~~/src/HOL/Library/Abstract_Rat" Polynomial_List 
33154  9 
begin 
10 

35046  11 
(* Implementation *) 
33154  12 

13 
subsection{* Datatype of polynomial expressions *} 

14 

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

16 
 Mul poly poly Neg poly Pw poly nat CN poly nat poly 

17 

35054  18 
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" 
19 
abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)" 

33154  20 

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

39246  22 
primrec polysize:: "poly \<Rightarrow> nat" where 
33154  23 
"polysize (C c) = 1" 
39246  24 
 "polysize (Bound n) = 1" 
25 
 "polysize (Neg p) = 1 + polysize p" 

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

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

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

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

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

33154  31 

39246  32 
primrec polybound0:: "poly \<Rightarrow> bool" (* a poly is INDEPENDENT of Bound 0 *) where 
33154  33 
"polybound0 (C c) = True" 
39246  34 
 "polybound0 (Bound n) = (n>0)" 
35 
 "polybound0 (Neg a) = polybound0 a" 

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

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

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

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

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

41 

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

33154  43 
"polysubst0 t (C c) = (C c)" 
39246  44 
 "polysubst0 t (Bound n) = (if n=0 then t else Bound n)" 
45 
 "polysubst0 t (Neg a) = Neg (polysubst0 t a)" 

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

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

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

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

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

33154  51 
else CN (polysubst0 t c) n (polysubst0 t p))" 
52 

41808  53 
fun decrpoly:: "poly \<Rightarrow> poly" 
54 
where 

33154  55 
"decrpoly (Bound n) = Bound (n  1)" 
41808  56 
 "decrpoly (Neg a) = Neg (decrpoly a)" 
57 
 "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" 

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

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

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

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

62 
 "decrpoly a = a" 

33154  63 

64 
subsection{* Degrees and heads and coefficients *} 

65 

41808  66 
fun degree:: "poly \<Rightarrow> nat" 
67 
where 

33154  68 
"degree (CN c 0 p) = 1 + degree p" 
41808  69 
 "degree p = 0" 
33154  70 

41808  71 
fun head:: "poly \<Rightarrow> poly" 
72 
where 

33154  73 
"head (CN c 0 p) = head p" 
41808  74 
 "head p = p" 
75 

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

77 
fun degreen:: "poly \<Rightarrow> nat \<Rightarrow> nat" 

78 
where 

33154  79 
"degreen (CN c n p) = (\<lambda>m. if n=m then 1 + degreen p n else 0)" 
41808  80 
"degreen p = (\<lambda>m. 0)" 
33154  81 

41808  82 
fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly" 
83 
where 

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

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

33154  86 

41808  87 
fun coefficients:: "poly \<Rightarrow> poly list" 
88 
where 

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

90 
 "coefficients p = [p]" 

33154  91 

41808  92 
fun isconstant:: "poly \<Rightarrow> bool" 
93 
where 

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

95 
 "isconstant p = True" 

33154  96 

41808  97 
fun behead:: "poly \<Rightarrow> poly" 
98 
where 

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

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

101 

102 
fun headconst:: "poly \<Rightarrow> Num" 

103 
where 

33154  104 
"headconst (CN c n p) = headconst p" 
41808  105 
 "headconst (C n) = n" 
33154  106 

107 
subsection{* Operations for normalization *} 

41812  108 

109 

33154  110 
consts 
111 
polysub :: "poly\<times>poly \<Rightarrow> poly" 

41808  112 

35054  113 
abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "\<^sub>p" 60) 
114 
where "a \<^sub>p b \<equiv> polysub (a,b)" 

33154  115 

41812  116 
declare if_cong[fundef_cong del] 
117 
declare let_cong[fundef_cong del] 

118 

119 
fun polyadd :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60) 

120 
where 

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

122 
 "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" 

123 
 "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" 

124 
 "polyadd (CN c n p) (CN c' n' p') = 

125 
(if n < n' then CN (polyadd c (CN c' n' p')) n p 

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

127 
else (let cc' = polyadd c c' ; 

128 
pp' = polyadd p p' 

33154  129 
in (if pp' = 0\<^sub>p then cc' else CN cc' n pp')))" 
41812  130 
 "polyadd a b = Add a b" 
131 

33154  132 

41808  133 
fun polyneg :: "poly \<Rightarrow> poly" ("~\<^sub>p") 
134 
where 

33154  135 
"polyneg (C c) = C (~\<^sub>N c)" 
41808  136 
 "polyneg (CN c n p) = CN (polyneg c) n (polyneg p)" 
137 
 "polyneg a = Neg a" 

33154  138 

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

41813  141 

142 
fun polymul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60) 

143 
where 

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

145 
 "polymul (C c) (CN c' n' p') = 

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

147 
 "polymul (CN c n p) (C c') = 

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

149 
 "polymul (CN c n p) (CN c' n' p') = 

150 
(if n<n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p')) 

33154  151 
else if n' < n 
41813  152 
then CN (polymul (CN c n p) c') n' (polymul (CN c n p) p') 
153 
else polyadd (polymul (CN c n p) c') (CN 0\<^sub>p n' (polymul (CN c n p) p')))" 

154 
 "polymul a b = Mul a b" 

41808  155 

41812  156 
declare if_cong[fundef_cong] 
157 
declare let_cong[fundef_cong] 

158 

41808  159 
fun polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly" 
160 
where 

33154  161 
"polypow 0 = (\<lambda>p. 1\<^sub>p)" 
41813  162 
 "polypow n = (\<lambda>p. let q = polypow (n div 2) p ; d = polymul q q in 
163 
if even n then d else polymul p d)" 

33154  164 

41808  165 
abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60) 
166 
where "a ^\<^sub>p k \<equiv> polypow k a" 

167 

168 
function polynate :: "poly \<Rightarrow> poly" 

169 
where 

33154  170 
"polynate (Bound n) = CN 0\<^sub>p n 1\<^sub>p" 
41808  171 
 "polynate (Add p q) = (polynate p +\<^sub>p polynate q)" 
172 
 "polynate (Sub p q) = (polynate p \<^sub>p polynate q)" 

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

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

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

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

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

178 
by pat_completeness auto 

179 
termination by (relation "measure polysize") auto 

33154  180 

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

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

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

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

185 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

186 
definition monic :: "poly \<Rightarrow> (poly \<times> bool)" where 
33154  187 
"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))" 
188 

189 
subsection{* Pseudodivision *} 

190 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

191 
definition shift1 :: "poly \<Rightarrow> poly" where 
33154  192 
"shift1 p \<equiv> CN 0\<^sub>p 0 p" 
193 

39246  194 
abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> 'a)" where 
195 
"funpow \<equiv> compow" 

196 

41403
7eba049f7310
partial_function (tailrec) replaces function (tailrec);
krauss
parents:
39246
diff
changeset

197 
partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly" 
33154  198 
where 
41403
7eba049f7310
partial_function (tailrec) replaces function (tailrec);
krauss
parents:
39246
diff
changeset

199 
"polydivide_aux a n p k s = 
33154  200 
(if s = 0\<^sub>p then (k,s) 
201 
else (let b = head s; m = degree s in 

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

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

41403
7eba049f7310
partial_function (tailrec) replaces function (tailrec);
krauss
parents:
39246
diff
changeset

204 
(if a = b then polydivide_aux a n p k (s \<^sub>p p') 
7eba049f7310
partial_function (tailrec) replaces function (tailrec);
krauss
parents:
39246
diff
changeset

205 
else polydivide_aux a n p (Suc k) ((a *\<^sub>p s) \<^sub>p (b *\<^sub>p p')))))))" 
33154  206 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

207 
definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> (nat \<times> poly)" where 
41403
7eba049f7310
partial_function (tailrec) replaces function (tailrec);
krauss
parents:
39246
diff
changeset

208 
"polydivide s p \<equiv> polydivide_aux (head p) (degree p) p 0 s" 
33154  209 

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

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

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

213 

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

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

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

217 

218 
(* Verification *) 

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

220 
using Nat.gr0_conv_Suc 

221 
by clarsimp 

222 

223 
subsection{* Semantics of the polynomial representation *} 

224 

39246  225 
primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0, field_inverse_zero, power}" where 
33154  226 
"Ipoly bs (C c) = INum c" 
39246  227 
 "Ipoly bs (Bound n) = bs!n" 
228 
 "Ipoly bs (Neg a) =  Ipoly bs a" 

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

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

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

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

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

234 

35054  235 
abbreviation 
36409  236 
Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0, field_inverse_zero, power}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") 
35054  237 
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" 
33154  238 

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

240 
by (simp add: INum_def) 

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

242 
by (simp add: INum_def) 

243 

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

245 

246 
subsection {* Normal form and normalization *} 

247 

41808  248 
fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool" 
249 
where 

33154  250 
"isnpolyh (C c) = (\<lambda>k. isnormNum c)" 
41808  251 
 "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))" 
252 
 "isnpolyh p = (\<lambda>k. False)" 

33154  253 

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

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

256 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
35054
diff
changeset

257 
definition isnpoly :: "poly \<Rightarrow> bool" where 
33154  258 
"isnpoly p \<equiv> isnpolyh p 0" 
259 

260 
text{* polyadd preserves normal forms *} 

261 

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

41812  263 
\<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)" 
33154  264 
proof(induct p q arbitrary: n0 n1 rule: polyadd.induct) 
41812  265 
case (2 ab c' n' p' n0 n1) 
266 
from prems have th1: "isnpolyh (C ab) (Suc n')" by simp 

33154  267 
from prems(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 
268 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 

41812  269 
with prems(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" by simp 
33154  270 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
271 
thus ?case using prems th3 by simp 

272 
next 

41812  273 
case (3 c' n' p' ab n1 n0) 
274 
from prems have th1: "isnpolyh (C ab) (Suc n')" by simp 

33154  275 
from prems(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 
276 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 

41812  277 
with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" by simp 
33154  278 
from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 
279 
thus ?case using prems th3 by simp 

280 
next 

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

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

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

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

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

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

41763  287 
moreover {assume eq: "n = n'" 
41812  288 
with "4.hyps"(3)[OF nc nc'] 
33154  289 
have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto 
290 
hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" 

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

41812  292 
from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp 
33154  293 
have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp 
294 
from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} 

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

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

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

298 
from prems have th21: "isnpolyh c (Suc n)" by simp 

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

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

41812  301 
from "4.hyps"(1)[OF th21 th22] 
302 
have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" using th23 by simp 

33154  303 
with prems th1 have ?case by simp } 
304 
moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp 

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

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

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

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

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

41812  310 
from "4.hyps"(2)[OF th22 th21] 
311 
have "isnpolyh (polyadd (CN c n p) c') (Suc n')" using th23 by simp 

33154  312 
with prems th1 have ?case by simp} 
313 
ultimately show ?case by blast 

314 
qed auto 

315 

41812  316 
lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" 
36349  317 
by (induct p q rule: polyadd.induct, auto simp add: Let_def field_simps right_distrib[symmetric] simp del: right_distrib) 
33154  318 

41812  319 
lemma polyadd_norm: "\<lbrakk> isnpoly p ; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polyadd p q)" 
33154  320 
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp 
321 

41404  322 
text{* The degree of addition and other general lemmas needed for the normal form of polymul *} 
33154  323 

324 
lemma polyadd_different_degreen: 

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

41812  326 
degreen (polyadd p q) m = max (degreen p m) (degreen q m)" 
33154  327 
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) 
328 
case (4 c n p c' n' p' m n0 n1) 

41763  329 
have "n' = n \<or> n < n' \<or> n' < n" by arith 
330 
thus ?case 

331 
proof (elim disjE) 

332 
assume [simp]: "n' = n" 

41812  333 
from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(57) 
41763  334 
show ?thesis by (auto simp: Let_def) 
335 
next 

336 
assume "n < n'" 

337 
with 4 show ?thesis by auto 

338 
next 

339 
assume "n' < n" 

340 
with 4 show ?thesis by auto 

341 
qed 

342 
qed auto 

33154  343 

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

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

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

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

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

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

350 

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

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

353 

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

355 
using degree_isnpolyh_Suc by auto 

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

357 
using degreen_0 by auto 

358 

359 

360 
lemma degreen_polyadd: 

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

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

363 
using np nq m 

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

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

366 
next 

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

368 
next 

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

41763  370 
have "n' = n \<or> n < n' \<or> n' < n" by arith 
371 
thus ?case 

372 
proof (elim disjE) 

373 
assume [simp]: "n' = n" 

41812  374 
from 4(4)[of n n m] 4(3)[of "Suc n" "Suc n" m] 4(57) 
41763  375 
show ?thesis by (auto simp: Let_def) 
376 
qed simp_all 

33154  377 
qed auto 
378 

41812  379 
lemma polyadd_eq_const_degreen: "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> 
33154  380 
\<Longrightarrow> degreen p m = degreen q m" 
381 
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) 

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

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

384 
moreover 

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

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

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

41763  388 
apply (cases "p +\<^sub>p p' = 0\<^sub>p") 
389 
apply (auto simp add: Let_def) 

390 
by blast 

391 
} 

33154  392 
ultimately have ?case by blast} 
393 
ultimately show ?case by blast 

394 
qed simp_all 

395 

396 
lemma polymul_properties: 

36409  397 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  398 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and m: "m \<le> min n0 n1" 
399 
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 

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

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

402 
else degreen p m + degreen q m)" 

403 
using np nq m 

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

41813  405 
case (2 c c' n' p') 
33154  406 
{ case (1 n0 n1) 
41813  407 
with "2.hyps"(46)[of n' n' n'] 
408 
and "2.hyps"(13)[of "Suc n'" "Suc n'" n'] 

41811  409 
show ?case by (auto simp add: min_def) 
33154  410 
next 
411 
case (2 n0 n1) thus ?case by auto 

412 
next 

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

414 
next 

41813  415 
case (3 c n p c') 
41811  416 
{ case (1 n0 n1) 
41813  417 
with "3.hyps"(46)[of n n n] 
418 
"3.hyps"(13)[of "Suc n" "Suc n" n] 

41811  419 
show ?case by (auto simp add: min_def) 
33154  420 
next 
41811  421 
case (2 n0 n1) thus ?case by auto 
33154  422 
next 
423 
case (3 n0 n1) thus ?case using "3.hyps" by auto } 

424 
next 

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

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

41811  427 
{ 
428 
case (1 n0 n1) 

33154  429 
hence cnp: "isnpolyh ?cnp n" and cnp': "isnpolyh ?cnp' n'" 
33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

430 
and np: "isnpolyh p n" and nc: "isnpolyh c (Suc n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

431 
and np': "isnpolyh p' n'" and nc': "isnpolyh c' (Suc n')" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

432 
and nn0: "n \<ge> n0" and nn1:"n' \<ge> n1" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

433 
by simp_all 
41811  434 
{ assume "n < n'" 
41813  435 
with "4.hyps"(45)[OF np cnp', of n] 
436 
"4.hyps"(1)[OF nc cnp', of n] nn0 cnp 

41811  437 
have ?case by (simp add: min_def) 
438 
} moreover { 

439 
assume "n' < n" 

41813  440 
with "4.hyps"(1617)[OF cnp np', of "n'"] 
441 
"4.hyps"(13)[OF cnp nc', of "Suc n'"] nn1 cnp' 

41811  442 
have ?case 
443 
by (cases "Suc n' = n", simp_all add: min_def) 

444 
} moreover { 

445 
assume "n' = n" 

41813  446 
with "4.hyps"(1617)[OF cnp np', of n] 
447 
"4.hyps"(13)[OF cnp nc', of n] cnp cnp' nn1 nn0 

41811  448 
have ?case 
449 
apply (auto intro!: polyadd_normh) 

450 
apply (simp_all add: min_def isnpolyh_mono[OF nn0]) 

451 
done 

452 
} 

453 
ultimately show ?case by arith 

454 
next 

455 
fix n0 n1 m 

33154  456 
assume np: "isnpolyh ?cnp n0" and np':"isnpolyh ?cnp' n1" 
457 
and m: "m \<le> min n0 n1" 

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

459 
let ?d1 = "degreen ?cnp m" 

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

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

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

463 
moreover 

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

41813  465 
with "4.hyps"(3,6,18) np np' m 
41811  466 
have ?eq by auto } 
33154  467 
moreover 
41811  468 
{assume nn': "n' = n" hence nn:"\<not> n' < n \<and> \<not> n < n'" by arith 
41813  469 
from "4.hyps"(16,18)[of n n' n] 
470 
"4.hyps"(13,14)[of n "Suc n'" n] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

471 
np np' nn' 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

472 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

473 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

474 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

475 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" by (auto simp add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

476 
{assume mn: "m = n" 
41813  477 
from "4.hyps"(17,18)[OF norm(1,4), of n] 
478 
"4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

479 
have degs: "degreen (?cnp *\<^sub>p c') n = 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

480 
(if c'=0\<^sub>p then 0 else ?d1 + degreen c' n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

481 
"degreen (?cnp *\<^sub>p p') n = ?d1 + degreen p' n" by (simp_all add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

482 
from degs norm 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

483 
have th1: "degreen(?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

484 
hence neq: "degreen (?cnp *\<^sub>p c') n \<noteq> degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

485 
by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

486 
have nmin: "n \<le> min n n" by (simp add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

487 
from polyadd_different_degreen[OF norm(3,6) neq nmin] th1 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

488 
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 
41813  489 
from "4.hyps"(1618)[OF norm(1,4), of n] 
490 
"4.hyps"(1315)[OF norm(1,2), of n] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

491 
mn norm m nn' deg 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

492 
have ?eq by simp} 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

493 
moreover 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

494 
{assume mn: "m \<noteq> n" hence mn': "m < n" using m np by auto 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

495 
from nn' m np have max1: "m \<le> max n n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

496 
hence min1: "m \<le> min n n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

497 
hence min2: "m \<le> min n (Suc n)" by simp 
41813  498 
from "4.hyps"(1618)[OF norm(1,4) min1] 
499 
"4.hyps"(1315)[OF norm(1,2) min2] 

41811  500 
degreen_polyadd[OF norm(3,6) max1] 
33154  501 

41811  502 
have "degreen (?cnp *\<^sub>p c' +\<^sub>p CN 0\<^sub>p n (?cnp *\<^sub>p p')) m 
503 
\<le> max (degreen (?cnp *\<^sub>p c') m) (degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) m)" 

504 
using mn nn' np np' by simp 

41813  505 
with "4.hyps"(1618)[OF norm(1,4) min1] 
506 
"4.hyps"(1315)[OF norm(1,2) min2] 

41811  507 
degreen_0[OF norm(3) mn'] 
508 
have ?eq using nn' mn np np' by clarsimp} 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

509 
ultimately have ?eq by blast} 
33154  510 
ultimately show ?eq by blast} 
511 
{ case (2 n0 n1) 

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

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

513 
and m: "m \<le> min n0 n1" by simp_all 
33154  514 
hence mn: "m \<le> n" by simp 
515 
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" 

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

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

517 
hence nn: "\<not>n' < n \<and> \<not> n<n'" by simp 
41813  518 
from "4.hyps"(1618) [of n n n] 
519 
"4.hyps"(1315)[of n "Suc n" n] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

520 
np np' C(2) mn 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

521 
have norm: "isnpolyh ?cnp n" "isnpolyh c' (Suc n)" "isnpolyh (?cnp *\<^sub>p c') n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

522 
"isnpolyh p' n" "isnpolyh (?cnp *\<^sub>p p') n" "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

523 
"(?cnp *\<^sub>p c' = 0\<^sub>p) = (c' = 0\<^sub>p)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

524 
"?cnp *\<^sub>p p' \<noteq> 0\<^sub>p" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

525 
"degreen (?cnp *\<^sub>p c') n = (if c'=0\<^sub>p then 0 else degreen ?cnp n + degreen c' n)" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

526 
"degreen (?cnp *\<^sub>p p') n = degreen ?cnp n + degreen p' n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

527 
by (simp_all add: min_def) 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

528 

02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

529 
from norm have cn: "isnpolyh (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

530 
have degneq: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

531 
using norm by simp 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

532 
from polyadd_eq_const_degreen[OF norm(3) cn C(1), where m="n"] degneq 
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

533 
have "False" by simp } 
33154  534 
thus ?case using "4.hyps" by clarsimp} 
535 
qed auto 

536 

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

36349  538 
by(induct p q rule: polymul.induct, auto simp add: field_simps) 
33154  539 

540 
lemma polymul_normh: 

36409  541 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  542 
shows "\<lbrakk>isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)" 
543 
using polymul_properties(1) by blast 

544 
lemma polymul_eq0_iff: 

36409  545 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  546 
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) " 
547 
using polymul_properties(2) by blast 

548 
lemma polymul_degreen: 

36409  549 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  550 
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)" 
551 
using polymul_properties(3) by blast 

552 
lemma polymul_norm: 

36409  553 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
41813  554 
shows "\<lbrakk> isnpoly p; isnpoly q\<rbrakk> \<Longrightarrow> isnpoly (polymul p q)" 
33154  555 
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp 
556 

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

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

559 

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

561 
by (induct p arbitrary: n0, auto) 

562 

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

36409  564 
shows "INum (headconst p) * Ipoly bs (fst (monic p)) = (Ipoly bs p ::'a::{field_char_0, field_inverse_zero, power})" 
33154  565 
unfolding monic_def Let_def 
566 
proof(cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) 

567 
let ?h = "headconst p" 

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

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

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

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

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

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

574 
qed 

575 

576 

41404  577 
text{* polyneg is a negation and preserves normal forms *} 
33154  578 

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

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

581 

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

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

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

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

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

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

588 

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

590 
using isnpoly_def polyneg_normh by simp 

591 

592 

41404  593 
text{* polysub is a substraction and preserves normal forms *} 
594 

33154  595 
lemma polysub[simp]: "Ipoly bs (polysub (p,q)) = (Ipoly bs p)  (Ipoly bs q)" 
596 
by (simp add: polysub_def polyneg polyadd) 

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

598 
by (simp add: polysub_def polyneg_normh polyadd_normh) 

599 

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

601 
using polyadd_norm polyneg_norm by (simp add: polysub_def) 

36409  602 
lemma polysub_same_0[simp]: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  603 
shows "isnpolyh p n0 \<Longrightarrow> polysub (p, p) = 0\<^sub>p" 
604 
unfolding polysub_def split_def fst_conv snd_conv 

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

606 

607 
lemma polysub_0: 

36409  608 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  609 
shows "\<lbrakk> isnpolyh p n0 ; isnpolyh q n1\<rbrakk> \<Longrightarrow> (p \<^sub>p q = 0\<^sub>p) = (p = q)" 
610 
unfolding polysub_def split_def fst_conv snd_conv 

41763  611 
by (induct p q arbitrary: n0 n1 rule:polyadd.induct) 
612 
(auto simp: Nsub0[simplified Nsub_def] Let_def) 

33154  613 

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

41404  615 

36409  616 
lemma polypow[simp]: "Ipoly bs (polypow n p) = ((Ipoly bs p :: 'a::{field_char_0, field_inverse_zero})) ^ n" 
33154  617 
proof(induct n rule: polypow.induct) 
618 
case 1 thus ?case by simp 

619 
next 

620 
case (2 n) 

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

41813  622 
let ?d = "polymul ?q ?q" 
33154  623 
have "odd (Suc n) \<or> even (Suc n)" by simp 
624 
moreover 

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

626 
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 

41813  627 
from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" by (simp add: Let_def) 
33154  628 
also have "\<dots> = (Ipoly bs p) * (Ipoly bs p)^(Suc n div 2)*(Ipoly bs p)^(Suc n div 2)" 
629 
using "2.hyps" by simp 

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

631 
apply (simp only: power_add power_one_right) by simp 

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

633 
by (simp only: th) 

634 
finally have ?case 

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

636 
moreover 

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

638 
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 

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

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

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

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

643 
ultimately show ?case by blast 

644 
qed 

645 

646 
lemma polypow_normh: 

36409  647 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  648 
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" 
649 
proof (induct k arbitrary: n rule: polypow.induct) 

650 
case (2 k n) 

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

41813  652 
let ?d = "polymul ?q ?q" 
33154  653 
from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ 
654 
from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp 

41813  655 
from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" by simp 
33154  656 
from dn on show ?case by (simp add: Let_def) 
657 
qed auto 

658 

659 
lemma polypow_norm: 

36409  660 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  661 
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" 
662 
by (simp add: polypow_normh isnpoly_def) 

663 

41404  664 
text{* Finally the whole normalization *} 
33154  665 

36409  666 
lemma polynate[simp]: "Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0, field_inverse_zero})" 
33154  667 
by (induct p rule:polynate.induct, auto) 
668 

669 
lemma polynate_norm[simp]: 

36409  670 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  671 
shows "isnpoly (polynate p)" 
672 
by (induct p rule: polynate.induct, simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm) (simp_all add: isnpoly_def) 

673 

674 
text{* shift1 *} 

675 

676 

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

678 
by (simp add: shift1_def polymul) 

679 

680 
lemma shift1_isnpoly: 

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

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

683 

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

685 
by (simp add: shift1_def) 

686 
lemma funpow_shift1_isnpoly: 

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

39246  688 
by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) 
33154  689 

690 
lemma funpow_isnpolyh: 

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

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

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

694 

36409  695 
lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" 
33154  696 
by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) 
697 

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

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

700 

701 
lemma funpow_shift1_1: 

36409  702 
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (funpow n shift1 1\<^sub>p *\<^sub>p p)" 
33154  703 
by (simp add: funpow_shift1) 
704 

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

36349  706 
by (induct p arbitrary: n0 rule: poly_cmul.induct, auto simp add: field_simps) 
33154  707 

708 
lemma behead: 

709 
assumes np: "isnpolyh p n" 

36409  710 
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = (Ipoly bs p :: 'a :: {field_char_0, field_inverse_zero})" 
33154  711 
using np 
712 
proof (induct p arbitrary: n rule: behead.induct) 

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

714 
from prems(2)[OF pn] 

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

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

36349  717 
by (simp_all add: th[symmetric] field_simps power_Suc) 
33154  718 
qed (auto simp add: Let_def) 
719 

720 
lemma behead_isnpolyh: 

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

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

723 

41404  724 
subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *} 
33154  725 
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" 
39246  726 
proof(induct p arbitrary: n rule: poly.induct, auto) 
33154  727 
case (goal1 c n p n') 
728 
hence "n = Suc (n  1)" by simp 

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

730 
with prems(2) show ?case by simp 

731 
qed 

732 

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

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

735 

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

737 

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

739 
apply (induct p arbitrary: n0, auto) 

740 
apply (atomize) 

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

742 
apply auto 

743 
done 

744 

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

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

747 

748 
lemma polybound0_I: 

749 
assumes nb: "polybound0 a" 

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

751 
using nb 

39246  752 
by (induct a rule: poly.induct) auto 
33154  753 
lemma polysubst0_I: 
754 
shows "Ipoly (b#bs) (polysubst0 a t) = Ipoly ((Ipoly (b#bs) a)#bs) t" 

755 
by (induct t) simp_all 

756 

757 
lemma polysubst0_I': 

758 
assumes nb: "polybound0 a" 

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

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

761 

762 
lemma decrpoly: assumes nb: "polybound0 t" 

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

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

765 

766 
lemma polysubst0_polybound0: assumes nb: "polybound0 t" 

767 
shows "polybound0 (polysubst0 t a)" 

39246  768 
using nb by (induct a rule: poly.induct, auto) 
33154  769 

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

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

772 

39246  773 
primrec maxindex :: "poly \<Rightarrow> nat" where 
33154  774 
"maxindex (Bound n) = n + 1" 
775 
 "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" 

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

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

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

779 
 "maxindex (Neg p) = maxindex p" 

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

781 
 "maxindex (C x) = 0" 

782 

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

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

785 

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

787 
proof(induct p rule: coefficients.induct) 

788 
case (1 c p) 

789 
show ?case 

790 
proof 

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

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

793 
moreover 

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

795 
moreover 

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

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

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

799 
ultimately show "wf_bs bs x" by blast 

800 
qed 

801 
qed simp_all 

802 

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

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

805 

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

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

808 

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

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

811 
proof 

812 
let ?ip = "maxindex p" 

813 
let ?tbs = "take ?ip bs" 

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

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

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

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

818 
qed 

819 

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

821 
by (induct p, auto) 

822 

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

824 
unfolding wf_bs_def by simp 

825 

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

827 
unfolding wf_bs_def by simp 

828 

829 

830 

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

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

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

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

835 

836 

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

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

839 

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

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

842 

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

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

845 
by simp 

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

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

848 

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

850 
unfolding wf_bs_def 

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

852 
apply (auto simp add: Let_def) 

853 
done 

854 

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

41811  856 
unfolding wf_bs_def 
33154  857 
apply (induct p q arbitrary: bs rule: polymul.induct) 
858 
apply (simp_all add: wf_bs_polyadd) 

859 
apply clarsimp 

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

861 
apply auto 

862 
done 

863 

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

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

866 

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

868 
unfolding polysub_def split_def fst_conv snd_conv using wf_bs_polyadd wf_bs_polyneg by blast 

869 

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

871 

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

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

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

875 

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

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

878 
case (1 c p n0) 

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

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

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

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

883 
qed auto 

884 

885 
lemma coefficients_isconst: 

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

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

888 
auto simp add: isnpolyh_Suc_const) 

889 

890 
lemma polypoly_polypoly': 

891 
assumes np: "isnpolyh p n0" 

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

893 
proof 

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

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

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

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

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

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

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

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

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

903 
by auto 

904 

905 
thus ?thesis unfolding polypoly_def polypoly'_def by simp 

906 
qed 

907 

908 
lemma polypoly_poly: 

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

910 
using np 

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

912 

913 
lemma polypoly'_poly: 

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

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

916 

917 

918 
lemma polypoly_poly_polybound0: 

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

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

921 
using np nb unfolding polypoly_def 

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

923 

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

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

926 

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

928 
by (cases p,auto) 

929 

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

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

932 

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

934 
by (simp add: head_eq_headn0) 

935 

936 
lemma isnpolyh_zero_iff: 

36409  937 
assumes nq: "isnpolyh p n0" and eq :"\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a::{field_char_0, field_inverse_zero, power})" 
33154  938 
shows "p = 0\<^sub>p" 
939 
using nq eq 

34915  940 
proof (induct "maxindex p" arbitrary: p n0 rule: less_induct) 
941 
case less 

942 
note np = `isnpolyh p n0` and zp = `\<forall>bs. wf_bs bs p \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (0::'a)` 

943 
{assume nz: "maxindex p = 0" 

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

33154  945 
with zp np have "p = 0\<^sub>p" unfolding wf_bs_def by simp} 
946 
moreover 

34915  947 
{assume nz: "maxindex p \<noteq> 0" 
33154  948 
let ?h = "head p" 
949 
let ?hd = "decrpoly ?h" 

950 
let ?ihd = "maxindex ?hd" 

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

952 
by simp_all 

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

954 

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

34915  956 
have mihn: "maxindex ?h \<le> maxindex p" by auto 
957 
with decr_maxindex[OF h(2)] nz have ihd_lt_n: "?ihd < maxindex p" by auto 

33154  958 
{fix bs:: "'a list" assume bs: "wf_bs bs ?hd" 
959 
let ?ts = "take ?ihd bs" 

960 
let ?rs = "drop ?ihd bs" 

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

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

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

34915  964 
from ihd_lt_n have "ALL x. length (x#?ts) \<le> maxindex p" by simp 
965 
with length_le_list_ex obtain xs where xs:"length ((x#?ts) @ xs) = maxindex p" by blast 

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

33154  967 
with zp have "\<forall> x. Ipoly ((x#?ts) @ xs) p = 0" by blast 
968 
hence "\<forall> x. Ipoly (x#(?ts @ xs)) p = 0" by simp 

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

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

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

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

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

973 
using poly_zero[where ?'a='a] by (simp add: polypoly'_def list_all_iff) 
33154  974 
with coefficients_head[of p, symmetric] 
975 
have th0: "Ipoly (?ts @ xs) ?hd = 0" by simp 

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

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

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

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

980 

34915  981 
from less(1)[OF ihd_lt_n nhd] hdz have "?hd = 0\<^sub>p" by blast 
33154  982 
hence "?h = 0\<^sub>p" by simp 
983 
with head_nz[OF np] have "p = 0\<^sub>p" by simp} 

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

985 
qed 

986 

987 
lemma isnpolyh_unique: 

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

36409  989 
shows "(\<forall>bs. \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = (\<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup> :: 'a::{field_char_0, field_inverse_zero, power})) \<longleftrightarrow> p = q" 
33154  990 
proof(auto) 
991 
assume H: "\<forall>bs. (\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> ::'a)= \<lparr>q\<rparr>\<^sub>p\<^bsup>bs\<^esup>" 

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

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

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

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

996 
show "p = q" by blast 

997 
qed 

998 

999 

41404  1000 
text{* consequences of unicity on the algorithms for polynomial normalization *} 
33154  1001 

36409  1002 
lemma polyadd_commute: assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1003 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" shows "p +\<^sub>p q = q +\<^sub>p p" 
1004 
using isnpolyh_unique[OF polyadd_normh[OF np nq] polyadd_normh[OF nq np]] by simp 

1005 

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

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

1008 
lemma polyadd_0[simp]: 

36409  1009 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1010 
and np: "isnpolyh p n0" shows "p +\<^sub>p 0\<^sub>p = p" and "0\<^sub>p +\<^sub>p p = p" 
1011 
using isnpolyh_unique[OF polyadd_normh[OF np zero_normh] np] 

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

1013 

1014 
lemma polymul_1[simp]: 

36409  1015 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1016 
and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" 
1017 
using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 

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

1019 
lemma polymul_0[simp]: 

36409  1020 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1021 
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" 
1022 
using isnpolyh_unique[OF polymul_normh[OF np zero_normh] zero_normh] 

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

1024 

1025 
lemma polymul_commute: 

36409  1026 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1027 
and np:"isnpolyh p n0" and nq: "isnpolyh q n1" 
1028 
shows "p *\<^sub>p q = q *\<^sub>p p" 

36409  1029 
using isnpolyh_unique[OF polymul_normh[OF np nq] polymul_normh[OF nq np], where ?'a = "'a\<Colon>{field_char_0, field_inverse_zero, power}"] by simp 
33154  1030 

1031 
declare polyneg_polyneg[simp] 

1032 

1033 
lemma isnpolyh_polynate_id[simp]: 

36409  1034 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1035 
and np:"isnpolyh p n0" shows "polynate p = p" 
36409  1036 
using isnpolyh_unique[where ?'a= "'a::{field_char_0, field_inverse_zero}", OF polynate_norm[of p, unfolded isnpoly_def] np] polynate[where ?'a = "'a::{field_char_0, field_inverse_zero}"] by simp 
33154  1037 

1038 
lemma polynate_idempotent[simp]: 

36409  1039 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1040 
shows "polynate (polynate p) = polynate p" 
1041 
using isnpolyh_polynate_id[OF polynate_norm[of p, unfolded isnpoly_def]] . 

1042 

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

1044 
unfolding poly_nate_def polypoly'_def .. 

36409  1045 
lemma poly_nate_poly: shows "poly (poly_nate bs p) = (\<lambda>x:: 'a ::{field_char_0, field_inverse_zero}. \<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup>)" 
33154  1046 
using polypoly'_poly[OF polynate_norm[unfolded isnpoly_def], symmetric, of bs p] 
1047 
unfolding poly_nate_polypoly' by (auto intro: ext) 

1048 

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

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

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

1052 

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

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

1055 
using n 

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

1057 

1058 
lemma degree_polyadd: 

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

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

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

1062 

1063 

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

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

1066 
proof 

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

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

1069 
qed 

1070 

1071 
lemma degree_polysub_samehead: 

36409  1072 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1073 
and np: "isnpolyh p n0" and nq: "isnpolyh q n1" and h: "head p = head q" 
1074 
and d: "degree p = degree q" 

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

1076 
unfolding polysub_def split_def fst_conv snd_conv 

1077 
using np nq h d 

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

41812  1079 
case (1 c c') thus ?case by (simp add: Nsub_def Nsub0[simplified Nsub_def]) 
33154  1080 
next 
41812  1081 
case (2 c c' n' p') 
1082 
from prems have "degree (C c) = degree (CN c' n' p')" by simp 

33154  1083 
hence nz:"n' > 0" by (cases n', auto) 
1084 
hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) 

1085 
with prems show ?case by simp 

1086 
next 

41812  1087 
case (3 c n p c') 
1088 
from prems have "degree (C c') = degree (CN c n p)" by simp 

33154  1089 
hence nz:"n > 0" by (cases n, auto) 
1090 
hence "head (CN c n p) = CN c n p" by (cases n, auto) 

1091 
with prems show ?case by simp 

1092 
next 

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

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

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

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

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

1098 
using H(12) degree_polyneg by auto 

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

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

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

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

1103 
moreover 

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

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

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

1107 
moreover {assume nz: "n > 0" 

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

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

1110 
ultimately have ?case by blast} 

1111 
moreover 

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

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

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

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

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

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

1118 
moreover 

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

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

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

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

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

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

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

1126 
ultimately show ?case by blast 

41812  1127 
qed auto 
33154  1128 

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

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

1131 

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

1133 
proof(induct k arbitrary: n0 p) 

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

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

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

39246  1137 
thus ?case by (simp add: funpow_swap1) 
33154  1138 
qed auto 
1139 

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

1141 
by (simp add: shift1_def) 

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

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

1144 

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

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

1147 

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

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

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

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

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

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

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

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

1156 

1157 
lemma polyadd_eq_const_degree: 

41812  1158 
"\<lbrakk> isnpolyh p n0 ; isnpolyh q n1 ; polyadd p q = C c\<rbrakk> \<Longrightarrow> degree p = degree q" 
33154  1159 
using polyadd_eq_const_degreen degree_eq_degreen0 by simp 
1160 

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

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

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

1164 
using np nq deg 

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

1166 
apply (case_tac n', simp, simp) 

1167 
apply (case_tac n, simp, simp) 

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

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

41763  1170 
apply (auto simp add: polyadd_eq_const_degree) 
1171 
apply (metis head_nz) 

1172 
apply (metis head_nz) 

1173 
apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) 

1174 
by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) 

33154  1175 

1176 
lemma polymul_head_polyeq: 

36409  1177 
assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 
33154  1178 
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" 
1179 
proof (induct p q arbitrary: n0 n1 rule: polymul.induct) 

41813  1180 
case (2 c c' n' p' n0 n1) 
1181 
hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum c" by (simp_all add: head_isnpolyh) 

33154  1182 
thus ?case using prems by (cases n', auto) 
1183 
next 

41813  1184 
case (3 c n p c' n0 n1) 
1185 
hence "isnpolyh (head (CN c n p)) n0" "isnormNum c'" by (simp_all add: head_isnpolyh) 

33154  1186 
thus ?case using prems by (cases n, auto) 
1187 
next 

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

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

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

1191 
by simp_all 

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

1193 
moreover 

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

1195 
using norm 

41813  1196 
"4.hyps"(2)[OF norm(1,6)] 
1197 
"4.hyps"(1)[OF norm(2,6)] by (simp, cases n, simp,cases n', simp_all)} 

33154  1198 
moreover {assume nn': "n'< n" 
41813  1199 
hence ?case using norm "4.hyps"(6) [OF norm(5,3)] 
1200 
"4.hyps"(5)[OF norm(5,4)] 

33154  1201 
by (simp,cases n',simp,cases n,auto)} 
1202 
moreover {assume nn': "n' = n" 

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

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

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

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

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

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

1209 
from polyadd_normh[OF ncnpc' ncnpp0'] 

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

1211 
by (simp add: min_def) 

1212 
{assume np: "n > 0" 

1213 
with nn' head_isnpolyh_Suc'[OF np nth] 

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1214 
head_isnpolyh_Suc'[OF np norm(5)] head_isnpolyh_Suc'[OF np norm(6)[simplified nn']] 
33154  1215 
have ?case by simp} 
1216 
moreover 

1217 
{moreover assume nz: "n = 0" 

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

33268
02de0317f66f
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
33154
diff
changeset

1219 
polymul_degreen[OF norm(5,3), where m="0"] nn' nz degree_eq_degreen0 
33154  1220 
norm(5,6) degree_npolyhCN[OF norm(6)] 
1221 
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 

1222 
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 

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

41813  1224 
have ?case using norm "4.hyps"(6)[OF norm(5,3)] 
1225 
"4.hyps"(5)[OF norm(5,4)] nn' nz by simp } 

33154  1226 
ultimately have ?case by (cases n) auto} 
1227 
ultimately show ?case by blast 

1228 
qed simp_all 

1229 

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

1231 
< 