author  wenzelm 
Mon, 10 Mar 2014 23:03:15 +0100  
changeset 56043  0b25c3d34b77 
parent 56009  dda076a32aea 
child 56066  cce36efe32eb 
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 

54220
0e6645622f22
more convenient place for a theory in solitariness
haftmann
parents:
53374
diff
changeset

8 
imports Complex_Main Rat_Pair Polynomial_List 
33154  9 
begin 
10 

52803  11 
subsection{* Datatype of polynomial expressions *} 
33154  12 

56043  13 
datatype poly = C Num  Bound nat  Add poly poly  Sub poly poly 
33154  14 
 Mul poly poly Neg poly Pw poly nat CN poly nat poly 
15 

35054  16 
abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)" 
50282
fe4d4bb9f4c2
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents:
49962
diff
changeset

17 
abbreviation poly_p :: "int \<Rightarrow> poly" ("'((_)')\<^sub>p") where "(i)\<^sub>p \<equiv> C (i)\<^sub>N" 
33154  18 

52658  19 

33154  20 
subsection{* Boundedness, substitution and all that *} 
52658  21 

22 
primrec polysize:: "poly \<Rightarrow> nat" 

23 
where 

33154  24 
"polysize (C c) = 1" 
39246  25 
 "polysize (Bound n) = 1" 
26 
 "polysize (Neg p) = 1 + polysize p" 

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

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

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

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

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

33154  32 

52658  33 
primrec polybound0:: "poly \<Rightarrow> bool"  {* a poly is INDEPENDENT of Bound 0 *} 
34 
where 

56000  35 
"polybound0 (C c) \<longleftrightarrow> True" 
36 
 "polybound0 (Bound n) \<longleftrightarrow> n > 0" 

37 
 "polybound0 (Neg a) \<longleftrightarrow> polybound0 a" 

38 
 "polybound0 (Add a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" 

39 
 "polybound0 (Sub a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" 

40 
 "polybound0 (Mul a b) \<longleftrightarrow> polybound0 a \<and> polybound0 b" 

41 
 "polybound0 (Pw p n) \<longleftrightarrow> polybound0 p" 

42 
 "polybound0 (CN c n p) \<longleftrightarrow> n \<noteq> 0 \<and> polybound0 c \<and> polybound0 p" 

39246  43 

52658  44 
primrec polysubst0:: "poly \<Rightarrow> poly \<Rightarrow> poly"  {* substitute a poly into a poly for Bound 0 *} 
45 
where 

56000  46 
"polysubst0 t (C c) = C c" 
47 
 "polysubst0 t (Bound n) = (if n = 0 then t else Bound n)" 

39246  48 
 "polysubst0 t (Neg a) = Neg (polysubst0 t a)" 
49 
 "polysubst0 t (Add a b) = Add (polysubst0 t a) (polysubst0 t b)" 

52803  50 
 "polysubst0 t (Sub a b) = Sub (polysubst0 t a) (polysubst0 t b)" 
39246  51 
 "polysubst0 t (Mul a b) = Mul (polysubst0 t a) (polysubst0 t b)" 
52 
 "polysubst0 t (Pw p n) = Pw (polysubst0 t p) n" 

56000  53 
 "polysubst0 t (CN c n p) = 
54 
(if n = 0 then Add (polysubst0 t c) (Mul t (polysubst0 t p)) 

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

33154  56 

52803  57 
fun decrpoly:: "poly \<Rightarrow> poly" 
41808  58 
where 
33154  59 
"decrpoly (Bound n) = Bound (n  1)" 
41808  60 
 "decrpoly (Neg a) = Neg (decrpoly a)" 
61 
 "decrpoly (Add a b) = Add (decrpoly a) (decrpoly b)" 

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

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

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

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

66 
 "decrpoly a = a" 

33154  67 

52658  68 

33154  69 
subsection{* Degrees and heads and coefficients *} 
70 

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

33154  73 
"degree (CN c 0 p) = 1 + degree p" 
41808  74 
 "degree p = 0" 
33154  75 

41808  76 
fun head:: "poly \<Rightarrow> poly" 
77 
where 

33154  78 
"head (CN c 0 p) = head p" 
41808  79 
 "head p = p" 
80 

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

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

83 
where 

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

33154  86 

41808  87 
fun headn:: "poly \<Rightarrow> nat \<Rightarrow> poly" 
88 
where 

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

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

33154  91 

41808  92 
fun coefficients:: "poly \<Rightarrow> poly list" 
93 
where 

56000  94 
"coefficients (CN c 0 p) = c # coefficients p" 
41808  95 
 "coefficients p = [p]" 
33154  96 

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

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

100 
 "isconstant p = True" 

33154  101 

41808  102 
fun behead:: "poly \<Rightarrow> poly" 
103 
where 

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

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

106 

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

108 
where 

33154  109 
"headconst (CN c n p) = headconst p" 
41808  110 
 "headconst (C n) = n" 
33154  111 

52658  112 

33154  113 
subsection{* Operations for normalization *} 
41812  114 

115 
declare if_cong[fundef_cong del] 

116 
declare let_cong[fundef_cong del] 

117 

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

119 
where 

56000  120 
"polyadd (C c) (C c') = C (c +\<^sub>N c')" 
52803  121 
 "polyadd (C c) (CN c' n' p') = CN (polyadd (C c) c') n' p'" 
41812  122 
 "polyadd (CN c n p) (C c') = CN (polyadd c (C c')) n p" 
123 
 "polyadd (CN c n p) (CN c' n' p') = 

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

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

127 
let 

128 
cc' = polyadd c c'; 

129 
pp' = polyadd p p' 

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

41812  131 
 "polyadd a b = Add a b" 
132 

33154  133 

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

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

33154  139 

41814  140 
definition polysub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "\<^sub>p" 60) 
52658  141 
where "p \<^sub>p q = polyadd p (polyneg q)" 
41813  142 

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

144 
where 

56043  145 
"polymul (C c) (C c') = C (c *\<^sub>N c')" 
52803  146 
 "polymul (C c) (CN c' n' p') = 
56000  147 
(if c = 0\<^sub>N then 0\<^sub>p else CN (polymul (C c) c') n' (polymul (C c) p'))" 
52803  148 
 "polymul (CN c n p) (C c') = 
56000  149 
(if c' = 0\<^sub>N then 0\<^sub>p else CN (polymul c (C c')) n (polymul p (C c')))" 
52803  150 
 "polymul (CN c n p) (CN c' n' p') = 
56000  151 
(if n < n' then CN (polymul c (CN c' n' p')) n (polymul p (CN c' n' p')) 
152 
else if n' < n 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')))" 

41813  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 

50282
fe4d4bb9f4c2
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents:
49962
diff
changeset

161 
"polypow 0 = (\<lambda>p. (1)\<^sub>p)" 
56000  162 
 "polypow n = 
163 
(\<lambda>p. 

164 
let 

165 
q = polypow (n div 2) p; 

166 
d = polymul q q 

167 
in if even n then d else polymul p d)" 

33154  168 

35054  169 
abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60) 
170 
where "a ^\<^sub>p k \<equiv> polypow k a" 

33154  171 

41808  172 
function polynate :: "poly \<Rightarrow> poly" 
173 
where 

50282
fe4d4bb9f4c2
more robust syntax that survives collapse of \<^isub> and \<^sub>;
wenzelm
parents:
49962
diff
changeset

174 
"polynate (Bound n) = CN 0\<^sub>p n (1)\<^sub>p" 
56000  175 
 "polynate (Add p q) = polynate p +\<^sub>p polynate q" 
176 
 "polynate (Sub p q) = polynate p \<^sub>p polynate q" 

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

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

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

41808  180 
 "polynate (CN c n p) = polynate (Add c (Mul (Bound n) p))" 
181 
 "polynate (C c) = C (normNum c)" 

182 
by pat_completeness auto 

183 
termination by (relation "measure polysize") auto 

33154  184 

52658  185 
fun poly_cmul :: "Num \<Rightarrow> poly \<Rightarrow> poly" 
186 
where 

33154  187 
"poly_cmul y (C x) = C (y *\<^sub>N x)" 
188 
 "poly_cmul y (CN c n p) = CN (poly_cmul y c) n (poly_cmul y p)" 

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

190 

56009  191 
definition monic :: "poly \<Rightarrow> poly \<times> bool" 
56000  192 
where 
193 
"monic p = 

194 
(let h = headconst p 

195 
in if h = 0\<^sub>N then (p, False) else (C (Ninv h) *\<^sub>p p, 0>\<^sub>N h))" 

33154  196 

52658  197 

56000  198 
subsection {* Pseudodivision *} 
33154  199 

52658  200 
definition shift1 :: "poly \<Rightarrow> poly" 
56000  201 
where "shift1 p = CN 0\<^sub>p 0 p" 
33154  202 

56009  203 
abbreviation funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" 
52658  204 
where "funpow \<equiv> compow" 
39246  205 

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

206 
partial_function (tailrec) polydivide_aux :: "poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<Rightarrow> poly \<Rightarrow> nat \<times> poly" 
52658  207 
where 
52803  208 
"polydivide_aux a n p k s = 
56000  209 
(if s = 0\<^sub>p then (k, s) 
52803  210 
else 
56000  211 
let 
212 
b = head s; 

213 
m = degree s 

214 
in 

215 
if m < n then (k,s) 

216 
else 

217 
let p' = funpow (m  n) shift1 p 

218 
in 

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

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

33154  221 

56000  222 
definition polydivide :: "poly \<Rightarrow> poly \<Rightarrow> nat \<times> poly" 
223 
where "polydivide s p = polydivide_aux (head p) (degree p) p 0 s" 

33154  224 

52658  225 
fun poly_deriv_aux :: "nat \<Rightarrow> poly \<Rightarrow> poly" 
226 
where 

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

229 

52658  230 
fun poly_deriv :: "poly \<Rightarrow> poly" 
231 
where 

33154  232 
"poly_deriv (CN c 0 p) = poly_deriv_aux 1 p" 
233 
 "poly_deriv p = 0\<^sub>p" 

234 

52658  235 

33154  236 
subsection{* Semantics of the polynomial representation *} 
237 

56000  238 
primrec Ipoly :: "'a list \<Rightarrow> poly \<Rightarrow> 'a::{field_char_0,field_inverse_zero,power}" 
239 
where 

33154  240 
"Ipoly bs (C c) = INum c" 
39246  241 
 "Ipoly bs (Bound n) = bs!n" 
242 
 "Ipoly bs (Neg a) =  Ipoly bs a" 

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

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

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

56000  246 
 "Ipoly bs (Pw t n) = Ipoly bs t ^ n" 
247 
 "Ipoly bs (CN c n p) = Ipoly bs c + (bs!n) * Ipoly bs p" 

39246  248 

56000  249 
abbreviation Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{field_char_0,field_inverse_zero,power}" 
250 
("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>") 

35054  251 
where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p" 
33154  252 

56009  253 
lemma Ipoly_CInt: "Ipoly bs (C (i, 1)) = of_int i" 
33154  254 
by (simp add: INum_def) 
56000  255 

52803  256 
lemma Ipoly_CRat: "Ipoly bs (C (i, j)) = of_int i / of_int j" 
33154  257 
by (simp add: INum_def) 
258 

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

260 

52658  261 

33154  262 
subsection {* Normal form and normalization *} 
263 

41808  264 
fun isnpolyh:: "poly \<Rightarrow> nat \<Rightarrow> bool" 
265 
where 

33154  266 
"isnpolyh (C c) = (\<lambda>k. isnormNum c)" 
56000  267 
 "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)" 
41808  268 
 "isnpolyh p = (\<lambda>k. False)" 
33154  269 

56000  270 
lemma isnpolyh_mono: "n' \<le> n \<Longrightarrow> isnpolyh p n \<Longrightarrow> isnpolyh p n'" 
52658  271 
by (induct p rule: isnpolyh.induct) auto 
33154  272 

52658  273 
definition isnpoly :: "poly \<Rightarrow> bool" 
56000  274 
where "isnpoly p = isnpolyh p 0" 
33154  275 

276 
text{* polyadd preserves normal forms *} 

277 

56000  278 
lemma polyadd_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polyadd p q) (min n0 n1)" 
52803  279 
proof (induct p q arbitrary: n0 n1 rule: polyadd.induct) 
41812  280 
case (2 ab c' n' p' n0 n1) 
56009  281 
from 2 have th1: "isnpolyh (C ab) (Suc n')" 
282 
by simp 

283 
from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" 

284 
by simp_all 

285 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" 

286 
by simp 

287 
with 2(1)[OF th1 th2] have th3:"isnpolyh (C ab +\<^sub>p c') (Suc n')" 

288 
by simp 

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

290 
by simp 

291 
then show ?case using 2 th3 

292 
by simp 

33154  293 
next 
41812  294 
case (3 c' n' p' ab n1 n0) 
56009  295 
from 3 have th1: "isnpolyh (C ab) (Suc n')" 
296 
by simp 

297 
from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" 

298 
by simp_all 

299 
with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" 

300 
by simp 

301 
with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C ab) (Suc n')" 

302 
by simp 

303 
from nplen1 have n01len1: "min n0 n1 \<le> n'" 

304 
by simp 

305 
then show ?case using 3 th3 

306 
by simp 

33154  307 
next 
308 
case (4 c n p c' n' p' n0 n1) 

56009  309 
then have nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" 
310 
by simp_all 

311 
from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" 

312 
by simp_all 

313 
from 4 have ngen0: "n \<ge> n0" 

314 
by simp 

315 
from 4 have n'gen1: "n' \<ge> n1" 

316 
by simp 

317 
have "n < n' \<or> n' < n \<or> n = n'" 

318 
by auto 

319 
moreover 

320 
{ 

52803  321 
assume eq: "n = n'" 
322 
with "4.hyps"(3)[OF nc nc'] 

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

325 
then have ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" 

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

327 
by auto 

328 
from eq "4.hyps"(4)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" 

329 
by simp 

330 
have minle: "min n0 n1 \<le> n'" 

331 
using ngen0 n'gen1 eq by simp 

332 
from minle npp' ncc'n01 4 eq ngen0 n'gen1 ncc' have ?case 

333 
by (simp add: Let_def) 

334 
} 

335 
moreover 

336 
{ 

52803  337 
assume lt: "n < n'" 
56009  338 
have "min n0 n1 \<le> n0" 
339 
by simp 

340 
with 4 lt have th1:"min n0 n1 \<le> n" 

341 
by auto 

342 
from 4 have th21: "isnpolyh c (Suc n)" 

343 
by simp 

344 
from 4 have th22: "isnpolyh (CN c' n' p') n'" 

345 
by simp 

346 
from lt have th23: "min (Suc n) n' = Suc n" 

347 
by arith 

348 
from "4.hyps"(1)[OF th21 th22] have "isnpolyh (polyadd c (CN c' n' p')) (Suc n)" 

349 
using th23 by simp 

350 
with 4 lt th1 have ?case 

351 
by simp 

352 
} 

353 
moreover 

354 
{ 

355 
assume gt: "n' < n" 

356 
then have gt': "n' < n \<and> \<not> n < n'" 

357 
by simp 

358 
have "min n0 n1 \<le> n1" 

359 
by simp 

360 
with 4 gt have th1: "min n0 n1 \<le> n'" 

361 
by auto 

362 
from 4 have th21: "isnpolyh c' (Suc n')" 

363 
by simp_all 

364 
from 4 have th22: "isnpolyh (CN c n p) n" 

365 
by simp 

366 
from gt have th23: "min n (Suc n') = Suc n'" 

367 
by arith 

368 
from "4.hyps"(2)[OF th22 th21] have "isnpolyh (polyadd (CN c n p) c') (Suc n')" 

369 
using th23 by simp 

370 
with 4 gt th1 have ?case 

371 
by simp 

372 
} 

52803  373 
ultimately show ?case by blast 
33154  374 
qed auto 
375 

41812  376 
lemma polyadd[simp]: "Ipoly bs (polyadd p q) = Ipoly bs p + Ipoly bs q" 
52658  377 
by (induct p q rule: polyadd.induct) 
378 
(auto simp add: Let_def field_simps distrib_left[symmetric] simp del: distrib_left) 

33154  379 

56009  380 
lemma polyadd_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polyadd p q)" 
33154  381 
using polyadd_normh[of "p" "0" "q" "0"] isnpoly_def by simp 
382 

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

52803  385 
lemma polyadd_different_degreen: 
56009  386 
assumes "isnpolyh p n0" 
387 
and "isnpolyh q n1" 

388 
and "degreen p m \<noteq> degreen q m" 

389 
and "m \<le> min n0 n1" 

390 
shows "degreen (polyadd p q) m = max (degreen p m) (degreen q m)" 

391 
using assms 

33154  392 
proof (induct p q arbitrary: m n0 n1 rule: polyadd.induct) 
393 
case (4 c n p c' n' p' m n0 n1) 

41763  394 
have "n' = n \<or> n < n' \<or> n' < n" by arith 
56009  395 
then show ?case 
41763  396 
proof (elim disjE) 
397 
assume [simp]: "n' = n" 

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

401 
assume "n < n'" 

402 
with 4 show ?thesis by auto 

403 
next 

404 
assume "n' < n" 

405 
with 4 show ?thesis by auto 

406 
qed 

407 
qed auto 

33154  408 

56009  409 
lemma headnz[simp]: "isnpolyh p n \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> headn p m \<noteq> 0\<^sub>p" 
52658  410 
by (induct p arbitrary: n rule: headn.induct) auto 
56009  411 

33154  412 
lemma degree_isnpolyh_Suc[simp]: "isnpolyh p (Suc n) \<Longrightarrow> degree p = 0" 
52658  413 
by (induct p arbitrary: n rule: degree.induct) auto 
56009  414 

33154  415 
lemma degreen_0[simp]: "isnpolyh p n \<Longrightarrow> m < n \<Longrightarrow> degreen p m = 0" 
52658  416 
by (induct p arbitrary: n rule: degreen.induct) auto 
33154  417 

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

52658  419 
by (induct p arbitrary: n rule: degree.induct) auto 
33154  420 

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

422 
using degree_isnpolyh_Suc by auto 

56009  423 

33154  424 
lemma degreen_npolyhCN[simp]: "isnpolyh (CN c n p) n0 \<Longrightarrow> degreen c n = 0" 
425 
using degreen_0 by auto 

426 

427 

428 
lemma degreen_polyadd: 

56009  429 
assumes np: "isnpolyh p n0" 
430 
and nq: "isnpolyh q n1" 

431 
and m: "m \<le> max n0 n1" 

33154  432 
shows "degreen (p +\<^sub>p q) m \<le> max (degreen p m) (degreen q m)" 
433 
using np nq m 

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

52803  435 
case (2 c c' n' p' n0 n1) 
56009  436 
then show ?case 
437 
by (cases n') simp_all 

33154  438 
next 
52803  439 
case (3 c n p c' n0 n1) 
56009  440 
then show ?case 
441 
by (cases n) auto 

33154  442 
next 
52803  443 
case (4 c n p c' n' p' n0 n1 m) 
41763  444 
have "n' = n \<or> n < n' \<or> n' < n" by arith 
56009  445 
then show ?case 
41763  446 
proof (elim disjE) 
447 
assume [simp]: "n' = n" 

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

33154  451 
qed auto 
452 

56009  453 
lemma polyadd_eq_const_degreen: 
454 
assumes "isnpolyh p n0" 

455 
and "isnpolyh q n1" 

456 
and "polyadd p q = C c" 

457 
shows "degreen p m = degreen q m" 

458 
using assms 

33154  459 
proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) 
52803  460 
case (4 c n p c' n' p' m n0 n1 x) 
56009  461 
{ 
462 
assume nn': "n' < n" 

463 
then have ?case using 4 by simp 

464 
} 

52803  465 
moreover 
56009  466 
{ 
467 
assume nn': "\<not> n' < n" 

468 
then have "n < n' \<or> n = n'" by arith 

52803  469 
moreover { assume "n < n'" with 4 have ?case by simp } 
56009  470 
moreover 
471 
{ 

472 
assume eq: "n = n'" 

473 
then have ?case using 4 

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

52658  476 
apply blast 
477 
done 

52803  478 
} 
56009  479 
ultimately have ?case by blast 
480 
} 

33154  481 
ultimately show ?case by blast 
482 
qed simp_all 

483 

484 
lemma polymul_properties: 

56000  485 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
52658  486 
and np: "isnpolyh p n0" 
487 
and nq: "isnpolyh q n1" 

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

52803  489 
shows "isnpolyh (p *\<^sub>p q) (min n0 n1)" 
56009  490 
and "p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p" 
491 
and "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)" 

33154  492 
using np nq m 
52658  493 
proof (induct p q arbitrary: n0 n1 m rule: polymul.induct) 
52803  494 
case (2 c c' n' p') 
56009  495 
{ 
496 
case (1 n0 n1) 

497 
with "2.hyps"(46)[of n' n' n'] and "2.hyps"(13)[of "Suc n'" "Suc n'" n'] 

41811  498 
show ?case by (auto simp add: min_def) 
33154  499 
next 
56009  500 
case (2 n0 n1) 
501 
then show ?case by auto 

33154  502 
next 
56009  503 
case (3 n0 n1) 
504 
then show ?case using "2.hyps" by auto 

505 
} 

33154  506 
next 
41813  507 
case (3 c n p c') 
56009  508 
{ 
509 
case (1 n0 n1) 

510 
with "3.hyps"(46)[of n n n] and "3.hyps"(13)[of "Suc n" "Suc n" n] 

41811  511 
show ?case by (auto simp add: min_def) 
33154  512 
next 
56009  513 
case (2 n0 n1) 
514 
then show ?case by auto 

33154  515 
next 
56009  516 
case (3 n0 n1) 
517 
then show ?case using "3.hyps" by auto 

518 
} 

33154  519 
next 
520 
case (4 c n p c' n' p') 

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

56009  522 
{ 
523 
case (1 n0 n1) 

524 
then have cnp: "isnpolyh ?cnp n" 

525 
and cnp': "isnpolyh ?cnp' n'" 

526 
and np: "isnpolyh p n" 

527 
and nc: "isnpolyh c (Suc n)" 

528 
and np': "isnpolyh p' n'" 

529 
and nc': "isnpolyh c' (Suc n')" 

530 
and nn0: "n \<ge> n0" 

531 
and nn1: "n' \<ge> n1" 

532 
by simp_all 

41811  533 
{ 
56009  534 
assume "n < n'" 
535 
with "4.hyps"(45)[OF np cnp', of n] and "4.hyps"(1)[OF nc cnp', of n] nn0 cnp 

536 
have ?case by (simp add: min_def) 

537 
} moreover { 

538 
assume "n' < n" 

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

540 
have ?case by (cases "Suc n' = n") (simp_all add: min_def) 

541 
} moreover { 

542 
assume "n' = n" 

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

544 
have ?case 

545 
apply (auto intro!: polyadd_normh) 

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

547 
done 

548 
} 

549 
ultimately show ?case by arith 

550 
next 

551 
fix n0 n1 m 

552 
assume np: "isnpolyh ?cnp n0" 

553 
assume np':"isnpolyh ?cnp' n1" 

554 
assume m: "m \<le> min n0 n1" 

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

556 
let ?d1 = "degreen ?cnp m" 

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

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

56043  559 
have "n' < n \<or> n < n' \<or> n' = n" by auto 
56009  560 
moreover 
561 
{ 

562 
assume "n' < n \<or> n < n'" 

563 
with "4.hyps"(3,6,18) np np' m have ?eq 

564 
by auto 

565 
} 

566 
moreover 

567 
{ 

568 
assume nn': "n' = n" 

569 
then have nn: "\<not> n' < n \<and> \<not> n < n'" by arith 

570 
from "4.hyps"(16,18)[of n n' n] 

571 
"4.hyps"(13,14)[of n "Suc n'" n] 

572 
np np' nn' 

56043  573 
have norm: 
574 
"isnpolyh ?cnp n" 

575 
"isnpolyh c' (Suc n)" 

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

577 
"isnpolyh p' n" 

578 
"isnpolyh (?cnp *\<^sub>p p') n" 

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

580 
"?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p" 

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

582 
by (auto simp add: min_def) 

56009  583 
{ 
584 
assume mn: "m = n" 

585 
from "4.hyps"(17,18)[OF norm(1,4), of n] 

586 
"4.hyps"(13,15)[OF norm(1,2), of n] norm nn' mn 

587 
have degs: 

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

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

590 
by (simp_all add: min_def) 

591 
from degs norm have th1: "degreen (?cnp *\<^sub>p c') n < degreen (CN 0\<^sub>p n (?cnp *\<^sub>p p')) n" 

592 
by simp 

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

594 
by simp 

595 
have nmin: "n \<le> min n n" 

596 
by (simp add: min_def) 

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

598 
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 = 

599 
degreen (CN 0\<^sub>p n (CN c n p *\<^sub>p p')) n" 

600 
by simp 

601 
from "4.hyps"(1618)[OF norm(1,4), of n] 

602 
"4.hyps"(1315)[OF norm(1,2), of n] 

603 
mn norm m nn' deg 

604 
have ?eq by simp 

41811  605 
} 
33154  606 
moreover 
56009  607 
{ 
608 
assume mn: "m \<noteq> n" 

609 
then have mn': "m < n" 

610 
using m np by auto 

611 
from nn' m np have max1: "m \<le> max n n" 

612 
by simp 

613 
then have min1: "m \<le> min n n" 

614 
by simp 

615 
then have min2: "m \<le> min n (Suc n)" 

616 
by simp 

617 
from "4.hyps"(1618)[OF norm(1,4) min1] 

618 
"4.hyps"(1315)[OF norm(1,2) min2] 

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

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

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

622 
using mn nn' np np' by simp 

623 
with "4.hyps"(1618)[OF norm(1,4) min1] 

624 
"4.hyps"(1315)[OF norm(1,2) min2] 

625 
degreen_0[OF norm(3) mn'] 

626 
have ?eq using nn' mn np np' by clarsimp 

627 
} 

628 
ultimately have ?eq by blast 

629 
} 

630 
ultimately show ?eq by blast 

631 
} 

632 
{ 

633 
case (2 n0 n1) 

634 
then have np: "isnpolyh ?cnp n0" 

635 
and np': "isnpolyh ?cnp' n1" 

56043  636 
and m: "m \<le> min n0 n1" 
637 
by simp_all 

56009  638 
then have mn: "m \<le> n" by simp 
639 
let ?c0p = "CN 0\<^sub>p n (?cnp *\<^sub>p p')" 

640 
{ 

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

642 
then have nn: "\<not> n' < n \<and> \<not> n < n'" 

643 
by simp 

644 
from "4.hyps"(1618) [of n n n] 

645 
"4.hyps"(1315)[of n "Suc n" n] 

646 
np np' C(2) mn 

647 
have norm: 

648 
"isnpolyh ?cnp n" 

649 
"isnpolyh c' (Suc n)" 

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

651 
"isnpolyh p' n" 

652 
"isnpolyh (?cnp *\<^sub>p p') n" 

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

654 
"?cnp *\<^sub>p c' = 0\<^sub>p \<longleftrightarrow> c' = 0\<^sub>p" 

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

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

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

658 
by (simp_all add: min_def) 

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

660 
by simp 

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

662 
using norm by simp 

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

664 
have False by simp 

665 
} 

666 
then show ?case using "4.hyps" by clarsimp 

667 
} 

33154  668 
qed auto 
669 

56009  670 
lemma polymul[simp]: "Ipoly bs (p *\<^sub>p q) = Ipoly bs p * Ipoly bs q" 
52658  671 
by (induct p q rule: polymul.induct) (auto simp add: field_simps) 
33154  672 

52803  673 
lemma polymul_normh: 
56000  674 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
56009  675 
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (p *\<^sub>p q) (min n0 n1)" 
52803  676 
using polymul_properties(1) by blast 
52658  677 

52803  678 
lemma polymul_eq0_iff: 
56000  679 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
56009  680 
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p *\<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p \<or> q = 0\<^sub>p" 
52803  681 
using polymul_properties(2) by blast 
52658  682 

683 
lemma polymul_degreen: (* FIXME duplicate? *) 

56000  684 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
56009  685 
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> m \<le> min n0 n1 \<Longrightarrow> 
686 
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)" 

33154  687 
using polymul_properties(3) by blast 
52658  688 

52803  689 
lemma polymul_norm: 
56000  690 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
56009  691 
shows "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polymul p q)" 
33154  692 
using polymul_normh[of "p" "0" "q" "0"] isnpoly_def by simp 
693 

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

52658  695 
by (induct p arbitrary: n0 rule: headconst.induct) auto 
33154  696 

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

52658  698 
by (induct p arbitrary: n0) auto 
33154  699 

52658  700 
lemma monic_eqI: 
52803  701 
assumes np: "isnpolyh p n0" 
52658  702 
shows "INum (headconst p) * Ipoly bs (fst (monic p)) = 
56000  703 
(Ipoly bs p ::'a::{field_char_0,field_inverse_zero, power})" 
33154  704 
unfolding monic_def Let_def 
52658  705 
proof (cases "headconst p = 0\<^sub>N", simp_all add: headconst_zero[OF np]) 
33154  706 
let ?h = "headconst p" 
707 
assume pz: "p \<noteq> 0\<^sub>p" 

56000  708 
{ 
709 
assume hz: "INum ?h = (0::'a)" 

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

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

713 
by simp 

714 
with headconst_zero[OF np] have "p = 0\<^sub>p" 

715 
by blast 

716 
with pz have False 

717 
by blast 

718 
} 

719 
then show "INum (headconst p) = (0::'a) \<longrightarrow> \<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> = 0" 

720 
by blast 

33154  721 
qed 
722 

723 

41404  724 
text{* polyneg is a negation and preserves normal forms *} 
33154  725 

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

52658  727 
by (induct p rule: polyneg.induct) auto 
33154  728 

56009  729 
lemma polyneg0: "isnpolyh p n \<Longrightarrow> (~\<^sub>p p) = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" 
52658  730 
by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: Nneg_def) 
56009  731 

33154  732 
lemma polyneg_polyneg: "isnpolyh p n0 \<Longrightarrow> ~\<^sub>p (~\<^sub>p p) = p" 
52658  733 
by (induct p arbitrary: n0 rule: polyneg.induct) auto 
56009  734 

735 
lemma polyneg_normh: "isnpolyh p n \<Longrightarrow> isnpolyh (polyneg p) n" 

736 
by (induct p arbitrary: n rule: polyneg.induct) (auto simp add: polyneg0) 

33154  737 

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

739 
using isnpoly_def polyneg_normh by simp 

740 

741 

41404  742 
text{* polysub is a substraction and preserves normal forms *} 
743 

56009  744 
lemma polysub[simp]: "Ipoly bs (polysub p q) = Ipoly bs p  Ipoly bs q" 
52658  745 
by (simp add: polysub_def) 
56009  746 

747 
lemma polysub_normh: "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> isnpolyh (polysub p q) (min n0 n1)" 

52658  748 
by (simp add: polysub_def polyneg_normh polyadd_normh) 
33154  749 

56009  750 
lemma polysub_norm: "isnpoly p \<Longrightarrow> isnpoly q \<Longrightarrow> isnpoly (polysub p q)" 
52803  751 
using polyadd_norm polyneg_norm by (simp add: polysub_def) 
56009  752 

52658  753 
lemma polysub_same_0[simp]: 
56000  754 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
41814  755 
shows "isnpolyh p n0 \<Longrightarrow> polysub p p = 0\<^sub>p" 
52658  756 
unfolding polysub_def split_def fst_conv snd_conv 
757 
by (induct p arbitrary: n0) (auto simp add: Let_def Nsub0[simplified Nsub_def]) 

33154  758 

52803  759 
lemma polysub_0: 
56000  760 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
56009  761 
shows "isnpolyh p n0 \<Longrightarrow> isnpolyh q n1 \<Longrightarrow> p \<^sub>p q = 0\<^sub>p \<longleftrightarrow> p = q" 
33154  762 
unfolding polysub_def split_def fst_conv snd_conv 
41763  763 
by (induct p q arbitrary: n0 n1 rule:polyadd.induct) 
52658  764 
(auto simp: Nsub0[simplified Nsub_def] Let_def) 
33154  765 

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

41404  767 

56009  768 
lemma polypow[simp]: 
769 
"Ipoly bs (polypow n p) = (Ipoly bs p :: 'a::{field_char_0,field_inverse_zero}) ^ n" 

52658  770 
proof (induct n rule: polypow.induct) 
771 
case 1 

56043  772 
then show ?case 
773 
by simp 

33154  774 
next 
775 
case (2 n) 

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

41813  777 
let ?d = "polymul ?q ?q" 
56043  778 
have "odd (Suc n) \<or> even (Suc n)" 
779 
by simp 

52803  780 
moreover 
56043  781 
{ 
782 
assume odd: "odd (Suc n)" 

56000  783 
have th: "(Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0)))) = Suc n div 2 + Suc n div 2 + 1" 
52658  784 
by arith 
56043  785 
from odd have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs (polymul p ?d)" 
786 
by (simp add: Let_def) 

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

33154  788 
using "2.hyps" by simp 
789 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2 + 1)" 

52658  790 
by (simp only: power_add power_one_right) simp 
56000  791 
also have "\<dots> = (Ipoly bs p) ^ (Suc (Suc (Suc 0) * (Suc n div Suc (Suc 0))))" 
33154  792 
by (simp only: th) 
52803  793 
finally have ?case 
56043  794 
using odd_nat_div_two_times_two_plus_one[OF odd, symmetric] by simp 
795 
} 

52803  796 
moreover 
56043  797 
{ 
798 
assume even: "even (Suc n)" 

56000  799 
have th: "(Suc (Suc 0)) * (Suc n div Suc (Suc 0)) = Suc n div 2 + Suc n div 2" 
52658  800 
by arith 
56043  801 
from even have "Ipoly bs (p ^\<^sub>p Suc n) = Ipoly bs ?d" 
802 
by (simp add: Let_def) 

33154  803 
also have "\<dots> = (Ipoly bs p) ^ (Suc n div 2 + Suc n div 2)" 
56043  804 
using "2.hyps" by (simp only: power_add) simp 
805 
finally have ?case using even_nat_div_two_times_two[OF even] 

806 
by (simp only: th) 

807 
} 

33154  808 
ultimately show ?case by blast 
809 
qed 

810 

52803  811 
lemma polypow_normh: 
56000  812 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
33154  813 
shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" 
814 
proof (induct k arbitrary: n rule: polypow.induct) 

56043  815 
case 1 
816 
then show ?case by auto 

817 
next 

33154  818 
case (2 k n) 
819 
let ?q = "polypow (Suc k div 2) p" 

41813  820 
let ?d = "polymul ?q ?q" 
56043  821 
from 2 have th1: "isnpolyh ?q n" and th2: "isnpolyh p n" 
822 
by blast+ 

823 
from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" 

824 
by simp 

825 
from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul p ?d) n" 

826 
by simp 

827 
from dn on show ?case 

828 
by (simp add: Let_def) 

829 
qed 

33154  830 

52803  831 
lemma polypow_norm: 
56000  832 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
33154  833 
shows "isnpoly p \<Longrightarrow> isnpoly (polypow k p)" 
834 
by (simp add: polypow_normh isnpoly_def) 

835 

41404  836 
text{* Finally the whole normalization *} 
33154  837 

52658  838 
lemma polynate [simp]: 
56000  839 
"Ipoly bs (polynate p) = (Ipoly bs p :: 'a ::{field_char_0,field_inverse_zero})" 
52658  840 
by (induct p rule:polynate.induct) auto 
33154  841 

52803  842 
lemma polynate_norm[simp]: 
56000  843 
assumes "SORT_CONSTRAINT('a::{field_char_0,field_inverse_zero})" 
33154  844 
shows "isnpoly (polynate p)" 
52658  845 
by (induct p rule: polynate.induct) 
846 
(simp_all add: polyadd_norm polymul_norm polysub_norm polyneg_norm polypow_norm, 

847 
simp_all add: isnpoly_def) 

33154  848 

849 
text{* shift1 *} 

850 

851 

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

52658  853 
by (simp add: shift1_def) 
33154  854 

52803  855 
lemma shift1_isnpoly: 
52658  856 
assumes pn: "isnpoly p" 
857 
and pnz: "p \<noteq> 0\<^sub>p" 

858 
shows "isnpoly (shift1 p) " 

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

33154  860 

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

862 
by (simp add: shift1_def) 

56043  863 

864 
lemma funpow_shift1_isnpoly: "isnpoly p \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpoly (funpow n shift1 p)" 

39246  865 
by (induct n arbitrary: p) (auto simp add: shift1_isnpoly funpow_swap1) 
33154  866 

52803  867 
lemma funpow_isnpolyh: 
56043  868 
assumes f: "\<And>p. isnpolyh p n \<Longrightarrow> isnpolyh (f p) n" 
52658  869 
and np: "isnpolyh p n" 
33154  870 
shows "isnpolyh (funpow k f p) n" 
52658  871 
using f np by (induct k arbitrary: p) auto 
33154  872 

52658  873 
lemma funpow_shift1: 
56000  874 
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) = 
52658  875 
Ipoly bs (Mul (Pw (Bound 0) n) p)" 
876 
by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) 

33154  877 

56043  878 
lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p \<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0" 
33154  879 
using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) 
880 

52803  881 
lemma funpow_shift1_1: 
56000  882 
"(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0,field_inverse_zero}) = 
52658  883 
Ipoly bs (funpow n shift1 (1)\<^sub>p *\<^sub>p p)" 
33154  884 
by (simp add: funpow_shift1) 
885 

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

45129
1fce03e3e8ad
tuned proofs  eliminated vacuous "induct arbitrary: ..." situations;
wenzelm
parents:
41842
diff
changeset

887 
by (induct p rule: poly_cmul.induct) (auto simp add: field_simps) 
33154  888 

889 
lemma behead: 

890 
assumes np: "isnpolyh p n" 

52658  891 
shows "Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = 
56000  892 
(Ipoly bs p :: 'a :: {field_char_0,field_inverse_zero})" 
33154  893 
using np 
894 
proof (induct p arbitrary: n rule: behead.induct) 

56009  895 
case (1 c p n) 
896 
then have pn: "isnpolyh p n" by simp 

52803  897 
from 1(1)[OF pn] 
898 
have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 

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

901 
apply (simp_all add: th[symmetric] field_simps) 

902 
done 

33154  903 
qed (auto simp add: Let_def) 
904 

905 
lemma behead_isnpolyh: 

52658  906 
assumes np: "isnpolyh p n" 
907 
shows "isnpolyh (behead p) n" 

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

909 

33154  910 

41404  911 
subsection{* Miscellaneous lemmas about indexes, decrementation, substitution etc ... *} 
52658  912 

33154  913 
lemma isnpolyh_polybound0: "isnpolyh p (Suc n) \<Longrightarrow> polybound0 p" 
52658  914 
proof (induct p arbitrary: n rule: poly.induct, auto) 
33154  915 
case (goal1 c n p n') 
56009  916 
then have "n = Suc (n  1)" 
917 
by simp 

918 
then have "isnpolyh p (Suc (n  1))" 

919 
using `isnpolyh p n` by simp 

920 
with goal1(2) show ?case 

921 
by simp 

33154  922 
qed 
923 

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

52658  925 
by (induct p arbitrary: n0 rule: isconstant.induct) (auto simp add: isnpolyh_polybound0) 
33154  926 

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

33154  929 

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

52658  931 
apply (induct p arbitrary: n0) 
932 
apply auto 

56043  933 
apply atomize 
33154  934 
apply (erule_tac x = "Suc nat" in allE) 
935 
apply auto 

936 
done 

937 

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

52658  939 
by (induct p arbitrary: n0 rule: head.induct) (auto intro: isnpolyh_polybound0) 
33154  940 

941 
lemma polybound0_I: 

942 
assumes nb: "polybound0 a" 

56009  943 
shows "Ipoly (b # bs) a = Ipoly (b' # bs) a" 
52658  944 
using nb 
52803  945 
by (induct a rule: poly.induct) auto 
52658  946 

56009  947 
lemma polysubst0_I: "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b # bs) a) # bs) t" 
33154  948 
by (induct t) simp_all 
949 

950 
lemma polysubst0_I': 

951 
assumes nb: "polybound0 a" 

56009  952 
shows "Ipoly (b # bs) (polysubst0 a t) = Ipoly ((Ipoly (b' # bs) a) # bs) t" 
33154  953 
by (induct t) (simp_all add: polybound0_I[OF nb, where b="b" and b'="b'"]) 
954 

52658  955 
lemma decrpoly: 
956 
assumes nb: "polybound0 t" 

56043  957 
shows "Ipoly (x # bs) t = Ipoly bs (decrpoly t)" 
52658  958 
using nb by (induct t rule: decrpoly.induct) simp_all 
33154  959 

52658  960 
lemma polysubst0_polybound0: 
961 
assumes nb: "polybound0 t" 

33154  962 
shows "polybound0 (polysubst0 t a)" 
52658  963 
using nb by (induct a rule: poly.induct) auto 
33154  964 

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

52658  966 
by (induct p arbitrary: n rule: degree.induct) (auto simp add: isnpolyh_polybound0) 
33154  967 

56043  968 
primrec maxindex :: "poly \<Rightarrow> nat" 
969 
where 

33154  970 
"maxindex (Bound n) = n + 1" 
971 
 "maxindex (CN c n p) = max (n + 1) (max (maxindex c) (maxindex p))" 

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

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

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

975 
 "maxindex (Neg p) = maxindex p" 

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

977 
 "maxindex (C x) = 0" 

978 

52658  979 
definition wf_bs :: "'a list \<Rightarrow> poly \<Rightarrow> bool" 
56000  980 
where "wf_bs bs p \<longleftrightarrow> length bs \<ge> maxindex p" 
33154  981 

56043  982 
lemma wf_bs_coefficients: "wf_bs bs p \<Longrightarrow> \<forall>c \<in> set (coefficients p). wf_bs bs c" 
52658  983 
proof (induct p rule: coefficients.induct) 
52803  984 
case (1 c p) 
985 
show ?case 

33154  986 
proof 
56009  987 
fix x 
988 
assume xc: "x \<in> set (coefficients (CN c 0 p))" 

989 
then have "x = c \<or> x \<in> set (coefficients p)" 

990 
by simp 

52803  991 
moreover 
56009  992 
{ 
993 
assume "x = c" 

994 
then have "wf_bs bs x" 

56043  995 
using "1.prems" unfolding wf_bs_def by simp 
56009  996 
} 
997 
moreover 

998 
{ 

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

1000 
from "1.prems" have "wf_bs bs p" 

1001 
unfolding wf_bs_def by simp 

1002 
with "1.hyps" H have "wf_bs bs x" 

1003 
by blast 

1004 
} 

1005 
ultimately show "wf_bs bs x" 

1006 
by blast 

33154  1007 
qed 
1008 
qed simp_all 

1009 

56043  1010 
lemma maxindex_coefficients: "\<forall>c \<in> set (coefficients p). maxindex c \<le> maxindex p" 
52658  1011 
by (induct p rule: coefficients.induct) auto 
33154  1012 

56000  1013 
lemma wf_bs_I: "wf_bs bs p \<Longrightarrow> Ipoly (bs @ bs') p = Ipoly bs p" 
52658  1014 
unfolding wf_bs_def by (induct p) (auto simp add: nth_append) 
33154  1015 

52658  1016 
lemma take_maxindex_wf: 
52803  1017 
assumes wf: "wf_bs bs p" 
33154  1018 
shows "Ipoly (take (maxindex p) bs) p = Ipoly bs p" 
56009  1019 
proof  
33154  1020 
let ?ip = "maxindex p" 
1021 
let ?tbs = "take ?ip bs" 

56009  1022 
from wf have "length ?tbs = ?ip" 
1023 
unfolding wf_bs_def by simp 

1024 
then have wf': "wf_bs ?tbs p" 

1025 
unfolding wf_bs_def by simp 

56043  1026 
have eq: "bs = ?tbs @ drop ?ip bs" 
56009  1027 
by simp 
1028 
from wf_bs_I[OF wf', of "drop ?ip bs"] show ?thesis 

1029 
using eq by simp 

33154  1030 
qed 
1031 

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

52658  1033 
by (induct p) auto 
33154  1034 

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

1036 
unfolding wf_bs_def by simp 

1037 

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

1039 
unfolding wf_bs_def by simp 

1040 

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

52658  1042 
by (induct p rule: coefficients.induct) (auto simp add: wf_bs_def) 
56043  1043 

33154  1044 
lemma coefficients_Nil[simp]: "coefficients p \<noteq> []" 
52658  1045 
by (induct p rule: coefficients.induct) simp_all 
33154  1046 

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

52658  1048 
by (induct p rule: coefficients.induct) auto 
33154  1049 

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

52658  1051 
unfolding wf_bs_def by (induct p rule: decrpoly.induct) auto 
33154  1052 

56043  1053 
lemma length_le_list_ex: "length xs \<le> n \<Longrightarrow> \<exists>ys. length (xs @ ys) = n" 
33154  1054 
apply (rule exI[where x="replicate (n  length xs) z"]) 
52658  1055 
apply simp 
1056 
done 

1057 

56043  1058 
lemma isnpolyh_Suc_const: "isnpolyh p (Suc n) \<Longrightarrow> isconstant p" 
52658  1059 
apply (cases p) 
1060 
apply auto 

1061 
apply (case_tac "nat") 

1062 
apply simp_all 

1063 
done 

33154  1064 

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

52803  1066 
unfolding wf_bs_def 
33154  1067 
apply (induct p q rule: polyadd.induct) 
1068 
apply (auto simp add: Let_def) 

1069 
done 

1070 

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

52803  1072 
unfolding wf_bs_def 
1073 
apply (induct p q arbitrary: bs rule: polymul.induct) 

33154  1074 
apply (simp_all add: wf_bs_polyadd) 
1075 
apply clarsimp 

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

1077 
apply auto 

1078 
done 

1079 

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

52658  1081 
unfolding wf_bs_def by (induct p rule: polyneg.induct) auto 
33154  1082 

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

56043  1084 
unfolding polysub_def split_def fst_conv snd_conv 
1085 
using wf_bs_polyadd wf_bs_polyneg by blast 

33154  1086 

52658  1087 

56043  1088 
subsection {* Canonicity of polynomial representation, see lemma isnpolyh_unique *} 
33154  1089 

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

56043  1091 
definition "polypoly' bs p = map (Ipoly bs \<circ> decrpoly) (coefficients p)" 
1092 
definition "poly_nate bs p = map (Ipoly bs \<circ> decrpoly) (coefficients (polynate p))" 

33154  1093 

56043  1094 
lemma coefficients_normh: "isnpolyh p n0 \<Longrightarrow> \<forall>q \<in> set (coefficients p). isnpolyh q n0" 
33154  1095 
proof (induct p arbitrary: n0 rule: coefficients.induct) 
1096 
case (1 c p n0) 

56009  1097 
have cp: "isnpolyh (CN c 0 p) n0" 
1098 
by fact 

1099 
then have norm: "isnpolyh c 0" "isnpolyh p 0" "p \<noteq> 0\<^sub>p" "n0 = 0" 

33154  1100 
by (auto simp add: isnpolyh_mono[where n'=0]) 
56009  1101 
from "1.hyps"[OF norm(2)] norm(1) norm(4) show ?case 
1102 
by simp 

33154  1103 
qed auto 
1104 

56043  1105 
lemma coefficients_isconst: "isnpolyh p n \<Longrightarrow> \<forall>q \<in> set (coefficients p). isconstant q" 
1106 
by (induct p arbitrary: n rule: coefficients.induct) (auto simp add: isnpolyh_Suc_const) 

33154  1107 

1108 
lemma polypoly_polypoly': 

1109 
assumes np: "isnpolyh p n0" 

56043  1110 
shows "polypoly (x # bs) p = polypoly' bs p" 
1111 
proof  

33154  1112 
let ?cf = "set (coefficients p)" 
1113 
from coefficients_normh[OF np] have cn_norm: "\<forall> q\<in> ?cf. isnpolyh q n0" . 

56043  1114 
{ 
1115 
fix q 

1116 
assume q: "q \<in> ?cf" 

1117 
from q cn_norm have th: "isnpolyh q n0" 

1118 
by blast 

1119 
from coefficients_isconst[OF np] q have "isconstant q" 

1120 
by blast 

1121 
with isconstant_polybound0[OF th] have "polybound0 q" 

1122 
by blast 

1123 
} 

56009  1124 
then have "\<forall>q \<in> ?cf. polybound0 q" .. 
56043  1125 
then have "\<forall>q \<in> ?cf. Ipoly (x # bs) q = Ipoly bs (decrpoly q)" 
33154  1126 
using polybound0_I[where b=x and bs=bs and b'=y] decrpoly[where x=x and bs=bs] 
1127 
by auto 

56043  1128 
then show ?thesis 
1129 
unfolding polypoly_def polypoly'_def by simp 

33154  1130 
qed 
1131 

1132 
lemma polypoly_poly: 

56043  1133 
assumes "isnpolyh p n0" 
1134 
shows "Ipoly (x # bs) p = poly (polypoly (x # bs) p) x" 

1135 
using assms 

52658  1136 
by (induct p arbitrary: n0 bs rule: coefficients.induct) (auto simp add: polypoly_def) 
33154  1137 

52803  1138 
lemma polypoly'_poly: 
56043  1139 
assumes "isnpolyh p n0" 
52658  1140 
shows "\<lparr>p\<rparr>\<^sub>p\<^bsup>x # bs\<^esup> = poly (polypoly' bs p) x" 
56043  1141 
using polypoly_poly[OF assms, simplified polypoly_polypoly'[OF assms]] . 
33154  1142 

1143 

1144 
lemma polypoly_poly_polybound0: 

56043  1145 
assumes "isnpolyh p n0" 
1146 
and "polybound0 p" 

33154  1147 
shows "polypoly bs p = [Ipoly bs p]" 
56043  1148 
using assms 
1149 
unfolding polypoly_def 

52658  1150 
apply (cases p) 
1151 
apply auto 

1152 
apply (case_tac nat) 

1153 
apply auto 

1154 
done 

33154  1155 

52803  1156 
lemma head_isnpolyh: "isnpolyh p n0 \<Longrightarrow> isnpolyh (head p) n0" 
52658  1157 
by (induct p rule: head.induct) auto 
33154  1158 

56043  1159 
lemma headn_nz[simp]: "isnpolyh p n0 \<Longrightarrow> headn p m = 0\<^sub>p \<longleftrightarrow> p = 0\<^sub>p" 
52658  1160 
by (cases p) auto 
33154  1161 

daa6ddece9f0
Multivariate polynomials library over fields
cha
