author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64861  9e8de30fd859 
child 65346  673a7b3379ec 
permissions  rwrr 
41959  1 
(* Title: HOL/Library/Polynomial.thy 
29451  2 
Author: Brian Huffman 
41959  3 
Author: Clemens Ballarin 
62352
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62351
diff
changeset

4 
Author: Amine Chaieb 
52380  5 
Author: Florian Haftmann 
29451  6 
*) 
7 

60500  8 
section \<open>Polynomials as type over a ring structure\<close> 
29451  9 

10 
theory Polynomial 

62352
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62351
diff
changeset

11 
imports Main "~~/src/HOL/Deriv" "~~/src/HOL/Library/More_List" 
35a9e1cbb5b3
separated potentially conflicting type class instance into separate theory
haftmann
parents:
62351
diff
changeset

12 
"~~/src/HOL/Library/Infinite_Set" 
29451  13 
begin 
14 

60500  15 
subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close> 
52380  16 

17 
definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65) 

18 
where 

19 
"x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)" 

20 

21 
lemma cCons_0_Nil_eq [simp]: 

22 
"0 ## [] = []" 

23 
by (simp add: cCons_def) 

24 

25 
lemma cCons_Cons_eq [simp]: 

26 
"x ## y # ys = x # y # ys" 

27 
by (simp add: cCons_def) 

28 

29 
lemma cCons_append_Cons_eq [simp]: 

30 
"x ## xs @ y # ys = x # xs @ y # ys" 

31 
by (simp add: cCons_def) 

32 

33 
lemma cCons_not_0_eq [simp]: 

34 
"x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs" 

35 
by (simp add: cCons_def) 

36 

37 
lemma strip_while_not_0_Cons_eq [simp]: 

38 
"strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs" 

39 
proof (cases "x = 0") 

40 
case False then show ?thesis by simp 

41 
next 

42 
case True show ?thesis 

43 
proof (induct xs rule: rev_induct) 

44 
case Nil with True show ?case by simp 

45 
next 

46 
case (snoc y ys) then show ?case 

47 
by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons) 

48 
qed 

49 
qed 

50 

51 
lemma tl_cCons [simp]: 

52 
"tl (x ## xs) = xs" 

53 
by (simp add: cCons_def) 

54 

61585  55 
subsection \<open>Definition of type \<open>poly\<close>\<close> 
29451  56 

61260  57 
typedef (overloaded) 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}" 
63433  58 
morphisms coeff Abs_poly 
59 
by (auto intro!: ALL_MOST) 

29451  60 

59487
adaa430fc0f7
default abstypes and default abstract equations make technical (no_code) annotation superfluous
haftmann
parents:
58881
diff
changeset

61 
setup_lifting type_definition_poly 
52380  62 

63 
lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)" 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
45605
diff
changeset

64 
by (simp add: coeff_inject [symmetric] fun_eq_iff) 
29451  65 

52380  66 
lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q" 
67 
by (simp add: poly_eq_iff) 

68 

59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

69 
lemma MOST_coeff_eq_0: "\<forall>\<^sub>\<infinity> n. coeff p n = 0" 
52380  70 
using coeff [of p] by simp 
29451  71 

72 

60500  73 
subsection \<open>Degree of a polynomial\<close> 
29451  74 

52380  75 
definition degree :: "'a::zero poly \<Rightarrow> nat" 
76 
where 

29451  77 
"degree p = (LEAST n. \<forall>i>n. coeff p i = 0)" 
78 

52380  79 
lemma coeff_eq_0: 
80 
assumes "degree p < n" 

81 
shows "coeff p n = 0" 

29451  82 
proof  
59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

83 
have "\<exists>n. \<forall>i>n. coeff p i = 0" 
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

84 
using MOST_coeff_eq_0 by (simp add: MOST_nat) 
52380  85 
then have "\<forall>i>degree p. coeff p i = 0" 
29451  86 
unfolding degree_def by (rule LeastI_ex) 
52380  87 
with assms show ?thesis by simp 
29451  88 
qed 
89 

90 
lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p" 

91 
by (erule contrapos_np, rule coeff_eq_0, simp) 

92 

93 
lemma degree_le: "\<forall>i>n. coeff p i = 0 \<Longrightarrow> degree p \<le> n" 

94 
unfolding degree_def by (erule Least_le) 

95 

96 
lemma less_degree_imp: "n < degree p \<Longrightarrow> \<exists>i>n. coeff p i \<noteq> 0" 

97 
unfolding degree_def by (drule not_less_Least, simp) 

98 

99 

60500  100 
subsection \<open>The zero polynomial\<close> 
29451  101 

102 
instantiation poly :: (zero) zero 

103 
begin 

104 

52380  105 
lift_definition zero_poly :: "'a poly" 
59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

106 
is "\<lambda>_. 0" by (rule MOST_I) simp 
29451  107 

108 
instance .. 

52380  109 

29451  110 
end 
111 

52380  112 
lemma coeff_0 [simp]: 
113 
"coeff 0 n = 0" 

114 
by transfer rule 

29451  115 

52380  116 
lemma degree_0 [simp]: 
117 
"degree 0 = 0" 

29451  118 
by (rule order_antisym [OF degree_le le0]) simp 
119 

120 
lemma leading_coeff_neq_0: 

52380  121 
assumes "p \<noteq> 0" 
122 
shows "coeff p (degree p) \<noteq> 0" 

29451  123 
proof (cases "degree p") 
124 
case 0 

60500  125 
from \<open>p \<noteq> 0\<close> have "\<exists>n. coeff p n \<noteq> 0" 
52380  126 
by (simp add: poly_eq_iff) 
29451  127 
then obtain n where "coeff p n \<noteq> 0" .. 
128 
hence "n \<le> degree p" by (rule le_degree) 

60500  129 
with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close> 
29451  130 
show "coeff p (degree p) \<noteq> 0" by simp 
131 
next 

132 
case (Suc n) 

60500  133 
from \<open>degree p = Suc n\<close> have "n < degree p" by simp 
29451  134 
hence "\<exists>i>n. coeff p i \<noteq> 0" by (rule less_degree_imp) 
135 
then obtain i where "n < i" and "coeff p i \<noteq> 0" by fast 

60500  136 
from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i" by simp 
137 
also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p" by (rule le_degree) 

29451  138 
finally have "degree p = i" . 
60500  139 
with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp 
29451  140 
qed 
141 

52380  142 
lemma leading_coeff_0_iff [simp]: 
143 
"coeff p (degree p) = 0 \<longleftrightarrow> p = 0" 

29451  144 
by (cases "p = 0", simp, simp add: leading_coeff_neq_0) 
145 

64795  146 
lemma eq_zero_or_degree_less: 
147 
assumes "degree p \<le> n" and "coeff p n = 0" 

148 
shows "p = 0 \<or> degree p < n" 

149 
proof (cases n) 

150 
case 0 

151 
with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close> 

152 
have "coeff p (degree p) = 0" by simp 

153 
then have "p = 0" by simp 

154 
then show ?thesis .. 

155 
next 

156 
case (Suc m) 

157 
have "\<forall>i>n. coeff p i = 0" 

158 
using \<open>degree p \<le> n\<close> by (simp add: coeff_eq_0) 

159 
then have "\<forall>i\<ge>n. coeff p i = 0" 

160 
using \<open>coeff p n = 0\<close> by (simp add: le_less) 

161 
then have "\<forall>i>m. coeff p i = 0" 

162 
using \<open>n = Suc m\<close> by (simp add: less_eq_Suc_le) 

163 
then have "degree p \<le> m" 

164 
by (rule degree_le) 

165 
then have "degree p < n" 

166 
using \<open>n = Suc m\<close> by (simp add: less_Suc_eq_le) 

167 
then show ?thesis .. 

168 
qed 

169 

170 
lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \<Longrightarrow> degree rrr \<le> dr \<Longrightarrow> degree rrr \<le> dr  1" 

171 
using eq_zero_or_degree_less by fastforce 

172 

29451  173 

60500  174 
subsection \<open>Liststyle constructor for polynomials\<close> 
29451  175 

52380  176 
lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
55415  177 
is "\<lambda>a p. case_nat a (coeff p)" 
59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

178 
by (rule MOST_SucD) (simp add: MOST_coeff_eq_0) 
29451  179 

52380  180 
lemmas coeff_pCons = pCons.rep_eq 
29455  181 

52380  182 
lemma coeff_pCons_0 [simp]: 
183 
"coeff (pCons a p) 0 = a" 

184 
by transfer simp 

29455  185 

52380  186 
lemma coeff_pCons_Suc [simp]: 
187 
"coeff (pCons a p) (Suc n) = coeff p n" 

29451  188 
by (simp add: coeff_pCons) 
189 

52380  190 
lemma degree_pCons_le: 
191 
"degree (pCons a p) \<le> Suc (degree p)" 

192 
by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split) 

29451  193 

194 
lemma degree_pCons_eq: 

195 
"p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)" 

52380  196 
apply (rule order_antisym [OF degree_pCons_le]) 
197 
apply (rule le_degree, simp) 

198 
done 

29451  199 

52380  200 
lemma degree_pCons_0: 
201 
"degree (pCons a 0) = 0" 

202 
apply (rule order_antisym [OF _ le0]) 

203 
apply (rule degree_le, simp add: coeff_pCons split: nat.split) 

204 
done 

29451  205 

29460
ad87e5d1488b
new lemmas about synthetic_div; declare degree_pCons_eq_if [simp]
huffman
parents:
29457
diff
changeset

206 
lemma degree_pCons_eq_if [simp]: 
29451  207 
"degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" 
52380  208 
apply (cases "p = 0", simp_all) 
209 
apply (rule order_antisym [OF _ le0]) 

210 
apply (rule degree_le, simp add: coeff_pCons split: nat.split) 

211 
apply (rule order_antisym [OF degree_pCons_le]) 

212 
apply (rule le_degree, simp) 

213 
done 

29451  214 

52380  215 
lemma pCons_0_0 [simp]: 
216 
"pCons 0 0 = 0" 

217 
by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) 

29451  218 

219 
lemma pCons_eq_iff [simp]: 

220 
"pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q" 

52380  221 
proof safe 
29451  222 
assume "pCons a p = pCons b q" 
223 
then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp 

224 
then show "a = b" by simp 

225 
next 

226 
assume "pCons a p = pCons b q" 

227 
then have "\<forall>n. coeff (pCons a p) (Suc n) = 

228 
coeff (pCons b q) (Suc n)" by simp 

52380  229 
then show "p = q" by (simp add: poly_eq_iff) 
29451  230 
qed 
231 

52380  232 
lemma pCons_eq_0_iff [simp]: 
233 
"pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0" 

29451  234 
using pCons_eq_iff [of a p 0 0] by simp 
235 

236 
lemma pCons_cases [cases type: poly]: 

237 
obtains (pCons) a q where "p = pCons a q" 

238 
proof 

239 
show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))" 

52380  240 
by transfer 
59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

241 
(simp_all add: MOST_inj[where f=Suc and P="\<lambda>n. p n = 0" for p] fun_eq_iff Abs_poly_inverse 
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

242 
split: nat.split) 
29451  243 
qed 
244 

245 
lemma pCons_induct [case_names 0 pCons, induct type: poly]: 

246 
assumes zero: "P 0" 

54856  247 
assumes pCons: "\<And>a p. a \<noteq> 0 \<or> p \<noteq> 0 \<Longrightarrow> P p \<Longrightarrow> P (pCons a p)" 
29451  248 
shows "P p" 
249 
proof (induct p rule: measure_induct_rule [where f=degree]) 

250 
case (less p) 

251 
obtain a q where "p = pCons a q" by (rule pCons_cases) 

252 
have "P q" 

253 
proof (cases "q = 0") 

254 
case True 

255 
then show "P q" by (simp add: zero) 

256 
next 

257 
case False 

258 
then have "degree (pCons a q) = Suc (degree q)" 

259 
by (rule degree_pCons_eq) 

260 
then have "degree q < degree p" 

60500  261 
using \<open>p = pCons a q\<close> by simp 
29451  262 
then show "P q" 
263 
by (rule less.hyps) 

264 
qed 

54856  265 
have "P (pCons a q)" 
266 
proof (cases "a \<noteq> 0 \<or> q \<noteq> 0") 

267 
case True 

60500  268 
with \<open>P q\<close> show ?thesis by (auto intro: pCons) 
54856  269 
next 
270 
case False 

271 
with zero show ?thesis by simp 

272 
qed 

29451  273 
then show ?case 
60500  274 
using \<open>p = pCons a q\<close> by simp 
29451  275 
qed 
276 

60570  277 
lemma degree_eq_zeroE: 
278 
fixes p :: "'a::zero poly" 

279 
assumes "degree p = 0" 

280 
obtains a where "p = pCons a 0" 

281 
proof  

282 
obtain a q where p: "p = pCons a q" by (cases p) 

283 
with assms have "q = 0" by (cases "q = 0") simp_all 

284 
with p have "p = pCons a 0" by simp 

285 
with that show thesis . 

286 
qed 

287 

29451  288 

62422  289 
subsection \<open>Quickcheck generator for polynomials\<close> 
290 

291 
quickcheck_generator poly constructors: "0 :: _ poly", pCons 

292 

293 

60500  294 
subsection \<open>Liststyle syntax for polynomials\<close> 
52380  295 

296 
syntax 

297 
"_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]") 

298 

299 
translations 

300 
"[:x, xs:]" == "CONST pCons x [:xs:]" 

301 
"[:x:]" == "CONST pCons x 0" 

302 
"[:x:]" <= "CONST pCons x (_constrain 0 t)" 

303 

304 

60500  305 
subsection \<open>Representation of polynomials by lists of coefficients\<close> 
52380  306 

307 
primrec Poly :: "'a::zero list \<Rightarrow> 'a poly" 

308 
where 

54855  309 
[code_post]: "Poly [] = 0" 
310 
 [code_post]: "Poly (a # as) = pCons a (Poly as)" 

52380  311 

312 
lemma Poly_replicate_0 [simp]: 

313 
"Poly (replicate n 0) = 0" 

314 
by (induct n) simp_all 

315 

316 
lemma Poly_eq_0: 

317 
"Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)" 

318 
by (induct as) (auto simp add: Cons_replicate_eq) 

63027
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

319 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

320 
lemma Poly_append_replicate_zero [simp]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

321 
"Poly (as @ replicate n 0) = Poly as" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

322 
by (induct as) simp_all 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

323 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

324 
lemma Poly_snoc_zero [simp]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

325 
"Poly (as @ [0]) = Poly as" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

326 
using Poly_append_replicate_zero [of as 1] by simp 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

327 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

328 
lemma Poly_cCons_eq_pCons_Poly [simp]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

329 
"Poly (a ## p) = pCons a (Poly p)" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

330 
by (simp add: cCons_def) 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

331 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

332 
lemma Poly_on_rev_starting_with_0 [simp]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

333 
assumes "hd as = 0" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

334 
shows "Poly (rev (tl as)) = Poly (rev as)" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

335 
using assms by (cases as) simp_all 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

336 

62065  337 
lemma degree_Poly: "degree (Poly xs) \<le> length xs" 
338 
by (induction xs) simp_all 

63027
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

339 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

340 
lemma coeff_Poly_eq [simp]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

341 
"coeff (Poly xs) = nth_default 0 xs" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

342 
by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits) 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

343 

52380  344 
definition coeffs :: "'a poly \<Rightarrow> 'a::zero list" 
345 
where 

346 
"coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])" 

347 

348 
lemma coeffs_eq_Nil [simp]: 

349 
"coeffs p = [] \<longleftrightarrow> p = 0" 

350 
by (simp add: coeffs_def) 

351 

352 
lemma not_0_coeffs_not_Nil: 

353 
"p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []" 

354 
by simp 

355 

356 
lemma coeffs_0_eq_Nil [simp]: 

357 
"coeffs 0 = []" 

358 
by simp 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

359 

52380  360 
lemma coeffs_pCons_eq_cCons [simp]: 
361 
"coeffs (pCons a p) = a ## coeffs p" 

362 
proof  

363 
{ fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a" 

364 
assume "\<forall>m\<in>set ms. m > 0" 

55415  365 
then have "map (case_nat x f) ms = map f (map (\<lambda>n. n  1) ms)" 
58199
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
57862
diff
changeset

366 
by (induct ms) (auto split: nat.split) 
5fbe474b5da8
explicit theory with additional, less commonly used list operations
haftmann
parents:
57862
diff
changeset

367 
} 
52380  368 
note * = this 
369 
show ?thesis 

60570  370 
by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc) 
52380  371 
qed 
372 

62065  373 
lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1" 
374 
by (simp add: coeffs_def) 

64860  375 

62065  376 
lemma coeffs_nth: 
377 
assumes "p \<noteq> 0" "n \<le> degree p" 

378 
shows "coeffs p ! n = coeff p n" 

379 
using assms unfolding coeffs_def by (auto simp del: upt_Suc) 

380 

64860  381 
lemma coeff_in_coeffs: 
382 
"p \<noteq> 0 \<Longrightarrow> n \<le> degree p \<Longrightarrow> coeff p n \<in> set (coeffs p)" 

383 
using coeffs_nth [of p n, symmetric] 

384 
by (simp add: length_coeffs) 

385 

52380  386 
lemma not_0_cCons_eq [simp]: 
387 
"p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p" 

388 
by (simp add: cCons_def) 

389 

390 
lemma Poly_coeffs [simp, code abstype]: 

391 
"Poly (coeffs p) = p" 

54856  392 
by (induct p) auto 
52380  393 

394 
lemma coeffs_Poly [simp]: 

395 
"coeffs (Poly as) = strip_while (HOL.eq 0) as" 

396 
proof (induct as) 

397 
case Nil then show ?case by simp 

398 
next 

399 
case (Cons a as) 

400 
have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)" 

401 
using replicate_length_same [of as 0] by (auto dest: sym [of _ as]) 

402 
with Cons show ?case by auto 

403 
qed 

404 

405 
lemma last_coeffs_not_0: 

406 
"p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0" 

407 
by (induct p) (auto simp add: cCons_def) 

408 

409 
lemma strip_while_coeffs [simp]: 

410 
"strip_while (HOL.eq 0) (coeffs p) = coeffs p" 

411 
by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last) 

412 

413 
lemma coeffs_eq_iff: 

414 
"p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q") 

415 
proof 

416 
assume ?P then show ?Q by simp 

417 
next 

418 
assume ?Q 

419 
then have "Poly (coeffs p) = Poly (coeffs q)" by simp 

420 
then show ?P by simp 

421 
qed 

422 

423 
lemma nth_default_coeffs_eq: 

424 
"nth_default 0 (coeffs p) = coeff p" 

425 
by (simp add: fun_eq_iff coeff_Poly_eq [symmetric]) 

426 

427 
lemma [code]: 

428 
"coeff p = nth_default 0 (coeffs p)" 

429 
by (simp add: nth_default_coeffs_eq) 

430 

431 
lemma coeffs_eqI: 

432 
assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n" 

433 
assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" 

434 
shows "coeffs p = xs" 

435 
proof  

63027
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

436 
from coeff have "p = Poly xs" by (simp add: poly_eq_iff) 
52380  437 
with zero show ?thesis by simp (cases xs, simp_all) 
438 
qed 

439 

440 
lemma degree_eq_length_coeffs [code]: 

441 
"degree p = length (coeffs p)  1" 

442 
by (simp add: coeffs_def) 

443 

444 
lemma length_coeffs_degree: 

445 
"p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)" 

446 
by (induct p) (auto simp add: cCons_def) 

447 

448 
lemma [code abstract]: 

449 
"coeffs 0 = []" 

450 
by (fact coeffs_0_eq_Nil) 

451 

452 
lemma [code abstract]: 

453 
"coeffs (pCons a p) = a ## coeffs p" 

454 
by (fact coeffs_pCons_eq_cCons) 

455 

456 
instantiation poly :: ("{zero, equal}") equal 

457 
begin 

458 

459 
definition 

460 
[code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)" 

461 

60679  462 
instance 
463 
by standard (simp add: equal equal_poly_def coeffs_eq_iff) 

52380  464 

465 
end 

466 

60679  467 
lemma [code nbe]: "HOL.equal (p :: _ poly) p \<longleftrightarrow> True" 
52380  468 
by (fact equal_refl) 
29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

469 

52380  470 
definition is_zero :: "'a::zero poly \<Rightarrow> bool" 
471 
where 

472 
[code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)" 

473 

474 
lemma is_zero_null [code_abbrev]: 

475 
"is_zero p \<longleftrightarrow> p = 0" 

476 
by (simp add: is_zero_def null_def) 

477 

63027
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

478 
subsubsection \<open>Reconstructing the polynomial from the list\<close> 
63145  479 
\<comment> \<open>contributed by Sebastiaan J.C. Joosten and RenÃ© Thiemann\<close> 
63027
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

480 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

481 
definition poly_of_list :: "'a::comm_monoid_add list \<Rightarrow> 'a poly" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

482 
where 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

483 
[simp]: "poly_of_list = Poly" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

484 

8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

485 
lemma poly_of_list_impl [code abstract]: 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

486 
"coeffs (poly_of_list as) = strip_while (HOL.eq 0) as" 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

487 
by simp 
8de0ebee3f1c
several updates on polynomial long division and pseudo division
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
62422
diff
changeset

488 

52380  489 

60500  490 
subsection \<open>Fold combinator for polynomials\<close> 
52380  491 

492 
definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b" 

493 
where 

494 
"fold_coeffs f p = foldr f (coeffs p)" 

495 

496 
lemma fold_coeffs_0_eq [simp]: 

497 
"fold_coeffs f 0 = id" 

498 
by (simp add: fold_coeffs_def) 

499 

500 
lemma fold_coeffs_pCons_eq [simp]: 

501 
"f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" 

502 
by (simp add: fold_coeffs_def cCons_def fun_eq_iff) 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

503 

52380  504 
lemma fold_coeffs_pCons_0_0_eq [simp]: 
505 
"fold_coeffs f (pCons 0 0) = id" 

506 
by (simp add: fold_coeffs_def) 

507 

508 
lemma fold_coeffs_pCons_coeff_not_0_eq [simp]: 

509 
"a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" 

510 
by (simp add: fold_coeffs_def) 

511 

512 
lemma fold_coeffs_pCons_not_0_0_eq [simp]: 

513 
"p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" 

514 
by (simp add: fold_coeffs_def) 

515 

64795  516 

60500  517 
subsection \<open>Canonical morphism on polynomials  evaluation\<close> 
52380  518 

519 
definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" 

520 
where 

61585  521 
"poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" \<comment> \<open>The Horner Schema\<close> 
52380  522 

523 
lemma poly_0 [simp]: 

524 
"poly 0 x = 0" 

525 
by (simp add: poly_def) 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

526 

52380  527 
lemma poly_pCons [simp]: 
528 
"poly (pCons a p) x = a + x * poly p x" 

529 
by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def) 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

530 

62065  531 
lemma poly_altdef: 
532 
"poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)" 

533 
proof (induction p rule: pCons_induct) 

534 
case (pCons a p) 

535 
show ?case 

536 
proof (cases "p = 0") 

537 
case False 

538 
let ?p' = "pCons a p" 

539 
note poly_pCons[of a p x] 

540 
also note pCons.IH 

541 
also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) = 

542 
coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)" 

64267  543 
by (simp add: field_simps sum_distrib_left coeff_pCons) 
544 
also note sum_atMost_Suc_shift[symmetric] 

62072  545 
also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric] 
62065  546 
finally show ?thesis . 
547 
qed simp 

548 
qed simp 

549 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

550 
lemma poly_0_coeff_0: "poly p 0 = coeff p 0" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

551 
by (cases p) (auto simp: poly_altdef) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

552 

29454
b0f586f38dd7
add recursion combinator poly_rec; define poly function using poly_rec
huffman
parents:
29453
diff
changeset

553 

60500  554 
subsection \<open>Monomials\<close> 
29451  555 

52380  556 
lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" 
557 
is "\<lambda>a m n. if m = n then a else 0" 

59983
cd2efd7d06bd
replace almost_everywhere_zero by Infinite_Set.MOST
hoelzl
parents:
59815
diff
changeset

558 
by (simp add: MOST_iff_cofinite) 
52380  559 

560 
lemma coeff_monom [simp]: 

561 
"coeff (monom a m) n = (if m = n then a else 0)" 

562 
by transfer rule 

29451  563 

52380  564 
lemma monom_0: 
565 
"monom a 0 = pCons a 0" 

566 
by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) 

29451  567 

52380  568 
lemma monom_Suc: 
569 
"monom a (Suc n) = pCons 0 (monom a n)" 

570 
by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) 

29451  571 

572 
lemma monom_eq_0 [simp]: "monom 0 n = 0" 

52380  573 
by (rule poly_eqI) simp 
29451  574 

575 
lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0" 

52380  576 
by (simp add: poly_eq_iff) 
29451  577 

578 
lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b" 

52380  579 
by (simp add: poly_eq_iff) 
29451  580 

581 
lemma degree_monom_le: "degree (monom a n) \<le> n" 

582 
by (rule degree_le, simp) 

583 

584 
lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n" 

585 
apply (rule order_antisym [OF degree_monom_le]) 

586 
apply (rule le_degree, simp) 

587 
done 

588 

52380  589 
lemma coeffs_monom [code abstract]: 
590 
"coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])" 

591 
by (induct n) (simp_all add: monom_0 monom_Suc) 

592 

593 
lemma fold_coeffs_monom [simp]: 

594 
"a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a" 

595 
by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff) 

596 

597 
lemma poly_monom: 

598 
fixes a x :: "'a::{comm_semiring_1}" 

599 
shows "poly (monom a n) x = a * x ^ n" 

600 
by (cases "a = 0", simp_all) 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

601 
(induct n, simp_all add: mult.left_commute poly_def) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

602 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

603 
lemma monom_eq_iff': "monom c n = monom d m \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = m)" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

604 
by (auto simp: poly_eq_iff) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

605 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

606 
lemma monom_eq_const_iff: "monom c n = [:d:] \<longleftrightarrow> c = d \<and> (c = 0 \<or> n = 0)" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

607 
using monom_eq_iff'[of c n d 0] by (simp add: monom_0) 
64795  608 

609 

610 
subsection \<open>Leading coefficient\<close> 

611 

612 
abbreviation lead_coeff:: "'a::zero poly \<Rightarrow> 'a" 

613 
where "lead_coeff p \<equiv> coeff p (degree p)" 

614 

615 
lemma lead_coeff_pCons[simp]: 

616 
"p \<noteq> 0 \<Longrightarrow> lead_coeff (pCons a p) = lead_coeff p" 

617 
"p = 0 \<Longrightarrow> lead_coeff (pCons a p) = a" 

618 
by auto 

619 

620 
lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c" 

621 
by (cases "c = 0") (simp_all add: degree_monom_eq) 

622 

623 

60500  624 
subsection \<open>Addition and subtraction\<close> 
29451  625 

626 
instantiation poly :: (comm_monoid_add) comm_monoid_add 

627 
begin 

628 

52380  629 
lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
630 
is "\<lambda>p q n. coeff p n + coeff q n" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

631 
proof  
60679  632 
fix q p :: "'a poly" 
633 
show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

634 
using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp 
52380  635 
qed 
29451  636 

60679  637 
lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n" 
52380  638 
by (simp add: plus_poly.rep_eq) 
29451  639 

60679  640 
instance 
641 
proof 

29451  642 
fix p q r :: "'a poly" 
643 
show "(p + q) + r = p + (q + r)" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57482
diff
changeset

644 
by (simp add: poly_eq_iff add.assoc) 
29451  645 
show "p + q = q + p" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57482
diff
changeset

646 
by (simp add: poly_eq_iff add.commute) 
29451  647 
show "0 + p = p" 
52380  648 
by (simp add: poly_eq_iff) 
29451  649 
qed 
650 

651 
end 

652 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

653 
instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

654 
begin 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

655 

cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

656 
lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

657 
is "\<lambda>p q n. coeff p n  coeff q n" 
60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

658 
proof  
60679  659 
fix q p :: "'a poly" 
660 
show "\<forall>\<^sub>\<infinity>n. coeff p n  coeff q n = 0" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

661 
using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

662 
qed 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

663 

60679  664 
lemma coeff_diff [simp]: "coeff (p  q) n = coeff p n  coeff q n" 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

665 
by (simp add: minus_poly.rep_eq) 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

666 

60679  667 
instance 
668 
proof 

29540  669 
fix p q r :: "'a poly" 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

670 
show "p + q  p = q" 
52380  671 
by (simp add: poly_eq_iff) 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

672 
show "p  q  r = p  (q + r)" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

673 
by (simp add: poly_eq_iff diff_diff_eq) 
29540  674 
qed 
675 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

676 
end 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

677 

29451  678 
instantiation poly :: (ab_group_add) ab_group_add 
679 
begin 

680 

52380  681 
lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly" 
682 
is "\<lambda>p n.  coeff p n" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

683 
proof  
60679  684 
fix p :: "'a poly" 
685 
show "\<forall>\<^sub>\<infinity>n.  coeff p n = 0" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

686 
using MOST_coeff_eq_0 by simp 
52380  687 
qed 
29451  688 

689 
lemma coeff_minus [simp]: "coeff ( p) n =  coeff p n" 

52380  690 
by (simp add: uminus_poly.rep_eq) 
29451  691 

60679  692 
instance 
693 
proof 

29451  694 
fix p q :: "'a poly" 
695 
show " p + p = 0" 

52380  696 
by (simp add: poly_eq_iff) 
29451  697 
show "p  q = p +  q" 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
52380
diff
changeset

698 
by (simp add: poly_eq_iff) 
29451  699 
qed 
700 

701 
end 

702 

703 
lemma add_pCons [simp]: 

704 
"pCons a p + pCons b q = pCons (a + b) (p + q)" 

52380  705 
by (rule poly_eqI, simp add: coeff_pCons split: nat.split) 
29451  706 

707 
lemma minus_pCons [simp]: 

708 
" pCons a p = pCons ( a) ( p)" 

52380  709 
by (rule poly_eqI, simp add: coeff_pCons split: nat.split) 
29451  710 

711 
lemma diff_pCons [simp]: 

712 
"pCons a p  pCons b q = pCons (a  b) (p  q)" 

52380  713 
by (rule poly_eqI, simp add: coeff_pCons split: nat.split) 
29451  714 

29539  715 
lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)" 
29451  716 
by (rule degree_le, auto simp add: coeff_eq_0) 
717 

29539  718 
lemma degree_add_le: 
719 
"\<lbrakk>degree p \<le> n; degree q \<le> n\<rbrakk> \<Longrightarrow> degree (p + q) \<le> n" 

720 
by (auto intro: order_trans degree_add_le_max) 

721 

29453  722 
lemma degree_add_less: 
723 
"\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p + q) < n" 

29539  724 
by (auto intro: le_less_trans degree_add_le_max) 
29453  725 

29451  726 
lemma degree_add_eq_right: 
727 
"degree p < degree q \<Longrightarrow> degree (p + q) = degree q" 

728 
apply (cases "q = 0", simp) 

729 
apply (rule order_antisym) 

29539  730 
apply (simp add: degree_add_le) 
29451  731 
apply (rule le_degree) 
732 
apply (simp add: coeff_eq_0) 

733 
done 

734 

735 
lemma degree_add_eq_left: 

736 
"degree q < degree p \<Longrightarrow> degree (p + q) = degree p" 

737 
using degree_add_eq_right [of q p] 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57482
diff
changeset

738 
by (simp add: add.commute) 
29451  739 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

740 
lemma degree_minus [simp]: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

741 
"degree ( p) = degree p" 
29451  742 
unfolding degree_def by simp 
743 

64795  744 
lemma lead_coeff_add_le: 
745 
assumes "degree p < degree q" 

746 
shows "lead_coeff (p + q) = lead_coeff q" 

747 
using assms 

748 
by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right) 

749 

750 
lemma lead_coeff_minus: 

751 
"lead_coeff ( p) =  lead_coeff p" 

752 
by (metis coeff_minus degree_minus) 

753 

59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

754 
lemma degree_diff_le_max: 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

755 
fixes p q :: "'a :: ab_group_add poly" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

756 
shows "degree (p  q) \<le> max (degree p) (degree q)" 
29451  757 
using degree_add_le [where p=p and q="q"] 
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
52380
diff
changeset

758 
by simp 
29451  759 

29539  760 
lemma degree_diff_le: 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

761 
fixes p q :: "'a :: ab_group_add poly" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

762 
assumes "degree p \<le> n" and "degree q \<le> n" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

763 
shows "degree (p  q) \<le> n" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

764 
using assms degree_add_le [of p n " q"] by simp 
29539  765 

29453  766 
lemma degree_diff_less: 
59815
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

767 
fixes p q :: "'a :: ab_group_add poly" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

768 
assumes "degree p < n" and "degree q < n" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

769 
shows "degree (p  q) < n" 
cce82e360c2f
explicit commutative additive inverse operation;
haftmann
parents:
59557
diff
changeset

770 
using assms degree_add_less [of p n " q"] by simp 
29453  771 

29451  772 
lemma add_monom: "monom a n + monom b n = monom (a + b) n" 
52380  773 
by (rule poly_eqI) simp 
29451  774 

775 
lemma diff_monom: "monom a n  monom b n = monom (a  b) n" 

52380  776 
by (rule poly_eqI) simp 
29451  777 

778 
lemma minus_monom: " monom a n = monom (a) n" 

52380  779 
by (rule poly_eqI) simp 
29451  780 

64267  781 
lemma coeff_sum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)" 
29451  782 
by (cases "finite A", induct set: finite, simp_all) 
783 

64267  784 
lemma monom_sum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)" 
785 
by (rule poly_eqI) (simp add: coeff_sum) 

52380  786 

787 
fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list" 

788 
where 

789 
"plus_coeffs xs [] = xs" 

790 
 "plus_coeffs [] ys = ys" 

791 
 "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys" 

792 

793 
lemma coeffs_plus_eq_plus_coeffs [code abstract]: 

794 
"coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)" 

795 
proof  

796 
{ fix xs ys :: "'a list" and n 

797 
have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" 

798 
proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) 

60679  799 
case (3 x xs y ys n) 
800 
then show ?case by (cases n) (auto simp add: cCons_def) 

52380  801 
qed simp_all } 
802 
note * = this 

803 
{ fix xs ys :: "'a list" 

804 
assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0" 

805 
moreover assume "plus_coeffs xs ys \<noteq> []" 

806 
ultimately have "last (plus_coeffs xs ys) \<noteq> 0" 

807 
proof (induct xs ys rule: plus_coeffs.induct) 

808 
case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis 

809 
qed simp_all } 

810 
note ** = this 

811 
show ?thesis 

812 
apply (rule coeffs_eqI) 

813 
apply (simp add: * nth_default_coeffs_eq) 

814 
apply (rule **) 

815 
apply (auto dest: last_coeffs_not_0) 

816 
done 

817 
qed 

818 

819 
lemma coeffs_uminus [code abstract]: 

820 
"coeffs ( p) = map (\<lambda>a.  a) (coeffs p)" 

821 
by (rule coeffs_eqI) 

822 
(simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) 

823 

824 
lemma [code]: 

825 
fixes p q :: "'a::ab_group_add poly" 

826 
shows "p  q = p +  q" 

59557  827 
by (fact diff_conv_add_uminus) 
52380  828 

829 
lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" 

830 
apply (induct p arbitrary: q, simp) 

831 
apply (case_tac q, simp, simp add: algebra_simps) 

832 
done 

833 

834 
lemma poly_minus [simp]: 

835 
fixes x :: "'a::comm_ring" 

836 
shows "poly ( p) x =  poly p x" 

837 
by (induct p) simp_all 

838 

839 
lemma poly_diff [simp]: 

840 
fixes x :: "'a::comm_ring" 

841 
shows "poly (p  q) x = poly p x  poly q x" 

54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
52380
diff
changeset

842 
using poly_add [of p " q" x] by simp 
52380  843 

64267  844 
lemma poly_sum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" 
52380  845 
by (induct A rule: infinite_finite_induct) simp_all 
29451  846 

64267  847 
lemma degree_sum_le: "finite S \<Longrightarrow> (\<And> p . p \<in> S \<Longrightarrow> degree (f p) \<le> n) 
848 
\<Longrightarrow> degree (sum f S) \<le> n" 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

849 
proof (induct S rule: finite_induct) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

850 
case (insert p S) 
64267  851 
hence "degree (sum f S) \<le> n" "degree (f p) \<le> n" by auto 
852 
thus ?case unfolding sum.insert[OF insert(12)] by (metis degree_add_le) 

62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

853 
qed simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

854 

3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

855 
lemma poly_as_sum_of_monoms': 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

856 
assumes n: "degree p \<le> n" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

857 
shows "(\<Sum>i\<le>n. monom (coeff p i) i) = p" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

858 
proof  
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

859 
have eq: "\<And>i. {..n} \<inter> {i} = (if i \<le> n then {i} else {})" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

860 
by auto 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

861 
show ?thesis 
64267  862 
using n by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq 
62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

863 
if_distrib[where f="\<lambda>x. x * a" for a]) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

864 
qed 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

865 

3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

866 
lemma poly_as_sum_of_monoms: "(\<Sum>i\<le>degree p. monom (coeff p i) i) = p" 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

867 
by (intro poly_as_sum_of_monoms' order_refl) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

868 

62065  869 
lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)" 
870 
by (induction xs) (simp_all add: monom_0 monom_Suc) 

871 

29451  872 

60500  873 
subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close> 
29451  874 

52380  875 
lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" 
876 
is "\<lambda>a p n. a * coeff p n" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

877 
proof  
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

878 
fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59983
diff
changeset

879 
using MOST_coeff_eq_0[of p] by eventually_elim simp 
52380  880 
qed 
29451  881 

52380  882 
lemma coeff_smult [simp]: 
883 
"coeff (smult a p) n = a * coeff p n" 

884 
by (simp add: smult.rep_eq) 

29451  885 

886 
lemma degree_smult_le: "degree (smult a p) \<le> degree p" 

887 
by (rule degree_le, simp add: coeff_eq_0) 

888 

29472  889 
lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57482
diff
changeset

890 
by (rule poly_eqI, simp add: mult.assoc) 
29451  891 

892 
lemma smult_0_right [simp]: "smult a 0 = 0" 

52380  893 
by (rule poly_eqI, simp) 
29451  894 

895 
lemma smult_0_left [simp]: "smult 0 p = 0" 

52380  896 
by (rule poly_eqI, simp) 
29451  897 

898 
lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" 

52380  899 
by (rule poly_eqI, simp) 
29451  900 

901 
lemma smult_add_right: 

902 
"smult a (p + q) = smult a p + smult a q" 

52380  903 
by (rule poly_eqI, simp add: algebra_simps) 
29451  904 

905 
lemma smult_add_left: 

906 
"smult (a + b) p = smult a p + smult b p" 

52380  907 
by (rule poly_eqI, simp add: algebra_simps) 
29451  908 

29457  909 
lemma smult_minus_right [simp]: 
29451  910 
"smult (a::'a::comm_ring) ( p) =  smult a p" 
52380  911 
by (rule poly_eqI, simp) 
29451  912 

29457  913 
lemma smult_minus_left [simp]: 
29451  914 
"smult ( a::'a::comm_ring) p =  smult a p" 
52380  915 
by (rule poly_eqI, simp) 
29451  916 

917 
lemma smult_diff_right: 

918 
"smult (a::'a::comm_ring) (p  q) = smult a p  smult a q" 

52380  919 
by (rule poly_eqI, simp add: algebra_simps) 
29451  920 

921 
lemma smult_diff_left: 

922 
"smult (a  b::'a::comm_ring) p = smult a p  smult b p" 

52380  923 
by (rule poly_eqI, simp add: algebra_simps) 
29451  924 

29472  925 
lemmas smult_distribs = 
926 
smult_add_left smult_add_right 

927 
smult_diff_left smult_diff_right 

928 

29451  929 
lemma smult_pCons [simp]: 
930 
"smult a (pCons b p) = pCons (a * b) (smult a p)" 

52380  931 
by (rule poly_eqI, simp add: coeff_pCons split: nat.split) 
29451  932 

933 
lemma smult_monom: "smult a (monom b n) = monom (a * b) n" 

934 
by (induct n, simp add: monom_0, simp add: monom_Suc) 

935 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

936 
lemma smult_Poly: "smult c (Poly xs) = Poly (map (op * c) xs)" 
64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

937 
by (auto simp add: poly_eq_iff nth_default_def) 
63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

938 

29659  939 
lemma degree_smult_eq [simp]: 
63498  940 
fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" 
29659  941 
shows "degree (smult a p) = (if a = 0 then 0 else degree p)" 
942 
by (cases "a = 0", simp, simp add: degree_def) 

943 

944 
lemma smult_eq_0_iff [simp]: 

63498  945 
fixes a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}" 
29659  946 
shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0" 
52380  947 
by (simp add: poly_eq_iff) 
63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

948 

52380  949 
lemma coeffs_smult [code abstract]: 
63498  950 
fixes p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly" 
52380  951 
shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" 
952 
by (rule coeffs_eqI) 

953 
(auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) 

64795  954 

955 
lemma smult_eq_iff: 

956 
assumes "(b :: 'a :: field) \<noteq> 0" 

957 
shows "smult a p = smult b q \<longleftrightarrow> smult (a / b) p = q" 

958 
proof 

959 
assume "smult a p = smult b q" 

960 
also from assms have "smult (inverse b) \<dots> = q" by simp 

961 
finally show "smult (a / b) p = q" by (simp add: field_simps) 

962 
qed (insert assms, auto) 

963 

29451  964 
instantiation poly :: (comm_semiring_0) comm_semiring_0 
965 
begin 

966 

967 
definition 

52380  968 
"p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0" 
29474  969 

970 
lemma mult_poly_0_left: "(0::'a poly) * q = 0" 

52380  971 
by (simp add: times_poly_def) 
29474  972 

973 
lemma mult_pCons_left [simp]: 

974 
"pCons a p * q = smult a q + pCons 0 (p * q)" 

52380  975 
by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def) 
29474  976 

977 
lemma mult_poly_0_right: "p * (0::'a poly) = 0" 

52380  978 
by (induct p) (simp add: mult_poly_0_left, simp) 
29451  979 

29474  980 
lemma mult_pCons_right [simp]: 
981 
"p * pCons a q = smult a p + pCons 0 (p * q)" 

52380  982 
by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps) 
29474  983 

984 
lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right 

985 

52380  986 
lemma mult_smult_left [simp]: 
987 
"smult a p * q = smult a (p * q)" 

988 
by (induct p) (simp add: mult_poly_0, simp add: smult_add_right) 

29474  989 

52380  990 
lemma mult_smult_right [simp]: 
991 
"p * smult a q = smult a (p * q)" 

992 
by (induct q) (simp add: mult_poly_0, simp add: smult_add_right) 

29474  993 

994 
lemma mult_poly_add_left: 

995 
fixes p q r :: "'a poly" 

996 
shows "(p + q) * r = p * r + q * r" 

52380  997 
by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps) 
29451  998 

60679  999 
instance 
1000 
proof 

29451  1001 
fix p q r :: "'a poly" 
1002 
show 0: "0 * p = 0" 

29474  1003 
by (rule mult_poly_0_left) 
29451  1004 
show "p * 0 = 0" 
29474  1005 
by (rule mult_poly_0_right) 
29451  1006 
show "(p + q) * r = p * r + q * r" 
29474  1007 
by (rule mult_poly_add_left) 
29451  1008 
show "(p * q) * r = p * (q * r)" 
29474  1009 
by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left) 
29451  1010 
show "p * q = q * p" 
29474  1011 
by (induct p, simp add: mult_poly_0, simp) 
29451  1012 
qed 
1013 

1014 
end 

1015 

63498  1016 
lemma coeff_mult_degree_sum: 
1017 
"coeff (p * q) (degree p + degree q) = 

1018 
coeff p (degree p) * coeff q (degree q)" 

1019 
by (induct p, simp, simp add: coeff_eq_0) 

1020 

1021 
instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors 

1022 
proof 

1023 
fix p q :: "'a poly" 

1024 
assume "p \<noteq> 0" and "q \<noteq> 0" 

1025 
have "coeff (p * q) (degree p + degree q) = 

1026 
coeff p (degree p) * coeff q (degree q)" 

1027 
by (rule coeff_mult_degree_sum) 

1028 
also have "coeff p (degree p) * coeff q (degree q) \<noteq> 0" 

1029 
using \<open>p \<noteq> 0\<close> and \<open>q \<noteq> 0\<close> by simp 

1030 
finally have "\<exists>n. coeff (p * q) n \<noteq> 0" .. 

1031 
thus "p * q \<noteq> 0" by (simp add: poly_eq_iff) 

1032 
qed 

1033 

29540  1034 
instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel .. 
1035 

29474  1036 
lemma coeff_mult: 
1037 
"coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (ni))" 

1038 
proof (induct p arbitrary: n) 

1039 
case 0 show ?case by simp 

1040 
next 

1041 
case (pCons a p n) thus ?case 

64267  1042 
by (cases n, simp, simp add: sum_atMost_Suc_shift 
1043 
del: sum_atMost_Suc) 

29474  1044 
qed 
29451  1045 

29474  1046 
lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q" 
1047 
apply (rule degree_le) 

1048 
apply (induct p) 

1049 
apply simp 

1050 
apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) 

29451  1051 
done 
1052 

1053 
lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)" 

60679  1054 
by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc) 
29451  1055 

1056 
instantiation poly :: (comm_semiring_1) comm_semiring_1 

1057 
begin 

1058 

60679  1059 
definition one_poly_def: "1 = pCons 1 0" 
29451  1060 

60679  1061 
instance 
1062 
proof 

1063 
show "1 * p = p" for p :: "'a poly" 

52380  1064 
unfolding one_poly_def by simp 
29451  1065 
show "0 \<noteq> (1::'a poly)" 
1066 
unfolding one_poly_def by simp 

1067 
qed 

1068 

1069 
end 

1070 

63498  1071 
instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors .. 
1072 

52380  1073 
instance poly :: (comm_ring) comm_ring .. 
1074 

1075 
instance poly :: (comm_ring_1) comm_ring_1 .. 

1076 

63498  1077 
instance poly :: (comm_ring_1) comm_semiring_1_cancel .. 
1078 

29451  1079 
lemma coeff_1 [simp]: "coeff 1 n = (if n = 0 then 1 else 0)" 
1080 
unfolding one_poly_def 

1081 
by (simp add: coeff_pCons split: nat.split) 

1082 

60570  1083 
lemma monom_eq_1 [simp]: 
1084 
"monom 1 0 = 1" 

1085 
by (simp add: monom_0 one_poly_def) 

63317
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1086 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1087 
lemma monom_eq_1_iff: "monom c n = 1 \<longleftrightarrow> c = 1 \<and> n = 0" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1088 
using monom_eq_const_iff[of c n 1] by (auto simp: one_poly_def) 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1089 

ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1090 
lemma monom_altdef: 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1091 
"monom c n = smult c ([:0, 1:]^n)" 
ca187a9f66da
Various additions to polynomials, FPSs, Gamma function
eberlm
parents:
63145
diff
changeset

1092 
by (induction n) (simp_all add: monom_0 monom_Suc one_poly_def) 
60570  1093 

29451  1094 
lemma degree_1 [simp]: "degree 1 = 0" 
1095 
unfolding one_poly_def 

1096 
by (rule degree_pCons_0) 

1097 

52380  1098 
lemma coeffs_1_eq [simp, code abstract]: 
1099 
"coeffs 1 = [1]" 

1100 
by (simp add: one_poly_def) 

1101 

1102 
lemma degree_power_le: 

1103 
"degree (p ^ n) \<le> degree p * n" 

1104 
by (induct n) (auto intro: order_trans degree_mult_le) 

1105 

64795  1106 
lemma coeff_0_power: 
1107 
"coeff (p ^ n) 0 = coeff p 0 ^ n" 

1108 
by (induction n) (simp_all add: coeff_mult) 

1109 

52380  1110 
lemma poly_smult [simp]: 
1111 
"poly (smult a p) x = a * poly p x" 

1112 
by (induct p, simp, simp add: algebra_simps) 

1113 

1114 
lemma poly_mult [simp]: 

1115 
"poly (p * q) x = poly p x * poly q x" 

1116 
by (induct p, simp_all, simp add: algebra_simps) 

1117 

1118 
lemma poly_1 [simp]: 

1119 
"poly 1 x = 1" 

1120 
by (simp add: one_poly_def) 

1121 

1122 
lemma poly_power [simp]: 

1123 
fixes p :: "'a::{comm_semiring_1} poly" 

1124 
shows "poly (p ^ n) x = poly p x ^ n" 

1125 
by (induct n) simp_all 

1126 

64272  1127 
lemma poly_prod: "poly (\<Prod>k\<in>A. p k) x = (\<Prod>k\<in>A. poly (p k) x)" 
62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1128 
by (induct A rule: infinite_finite_induct) simp_all 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1129 

64272  1130 
lemma degree_prod_sum_le: "finite S \<Longrightarrow> degree (prod f S) \<le> sum (degree o f) S" 
62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1131 
proof (induct S rule: finite_induct) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1132 
case (insert a S) 
64272  1133 
show ?case unfolding prod.insert[OF insert(12)] sum.insert[OF insert(12)] 
62128
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1134 
by (rule le_trans[OF degree_mult_le], insert insert, auto) 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1135 
qed simp 
3201ddb00097
Integrated some material from Algebraic_Numbers AFP entry to Polynomials; generalised some polynomial stuff.
eberlm
parents:
62072
diff
changeset

1136 

64795  1137 
lemma coeff_0_prod_list: 
1138 
"coeff (prod_list xs) 0 = prod_list (map (\<lambda>p. coeff p 0) xs)" 

1139 
by (induction xs) (simp_all add: coeff_mult) 

1140 

1141 
lemma coeff_monom_mult: 

1142 
"coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k  n))" 

1143 
proof  

1144 
have "coeff (monom c n * p) k = (\<Sum>i\<le>k. (if n = i then c else 0) * coeff p (k  i))" 

1145 
by (simp add: coeff_mult) 

1146 
also have "\<dots> = (\<Sum>i\<le>k. (if n = i then c * coeff p (k  i) else 0))" 

1147 
by (intro sum.cong) simp_all 

1148 
also have "\<dots> = (if k < n then 0 else c * coeff p (k  n))" by (simp add: sum.delta') 

1149 
finally show ?thesis . 

1150 
qed 

1151 

1152 
lemma monom_1_dvd_iff': 

1153 
"monom 1 n dvd p \<longleftrightarrow> (\<forall>k<n. coeff p k = 0)" 

1154 
proof 

1155 
assume "monom 1 n dvd p" 

1156 
then obtain r where r: "p = monom 1 n * r" by (elim dvdE) 

1157 
thus "\<forall>k<n. coeff p k = 0" by (simp add: coeff_mult) 

1158 
next 

1159 
assume zero: "(\<forall>k<n. coeff p k = 0)" 

1160 
define r where "r = Abs_poly (\<lambda>k. coeff p (k + n))" 

1161 
have "\<forall>\<^sub>\<infinity>k. coeff p (k + n) = 0" 

1162 
by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg, 

1163 
subst cofinite_eq_sequentially [symmetric]) transfer 

1164 
hence coeff_r [simp]: "coeff r k = coeff p (k + n)" for k unfolding r_def 

1165 
by (subst poly.Abs_poly_inverse) simp_all 

1166 
have "p = monom 1 n * r" 

1167 
by (intro poly_eqI, subst coeff_monom_mult) (insert zero, simp_all) 

1168 
thus "monom 1 n dvd p" by simp 

1169 
qed 

1170 

64591
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1171 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1172 
subsection \<open>Mapping polynomials\<close> 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1173 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1174 
definition map_poly 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1175 
:: "('a :: zero \<Rightarrow> 'b :: zero) \<Rightarrow> 'a poly \<Rightarrow> 'b poly" where 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1176 
"map_poly f p = Poly (map f (coeffs p))" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1177 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1178 
lemma map_poly_0 [simp]: "map_poly f 0 = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1179 
by (simp add: map_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1180 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1181 
lemma map_poly_1: "map_poly f 1 = [:f 1:]" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1182 
by (simp add: map_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1183 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1184 
lemma map_poly_1' [simp]: "f 1 = 1 \<Longrightarrow> map_poly f 1 = 1" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1185 
by (simp add: map_poly_def one_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1186 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1187 
lemma coeff_map_poly: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1188 
assumes "f 0 = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1189 
shows "coeff (map_poly f p) n = f (coeff p n)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1190 
by (auto simp: map_poly_def nth_default_def coeffs_def assms 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1191 
not_less Suc_le_eq coeff_eq_0 simp del: upt_Suc) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1192 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1193 
lemma coeffs_map_poly [code abstract]: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1194 
"coeffs (map_poly f p) = strip_while (op = 0) (map f (coeffs p))" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1195 
by (simp add: map_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1196 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1197 
lemma set_coeffs_map_poly: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1198 
"(\<And>x. f x = 0 \<longleftrightarrow> x = 0) \<Longrightarrow> set (coeffs (map_poly f p)) = f ` set (coeffs p)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1199 
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1200 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1201 
lemma coeffs_map_poly': 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1202 
assumes "(\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1203 
shows "coeffs (map_poly f p) = map f (coeffs p)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1204 
by (cases "p = 0") (auto simp: coeffs_map_poly last_map last_coeffs_not_0 assms 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1205 
intro!: strip_while_not_last split: if_splits) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1206 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1207 
lemma degree_map_poly: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1208 
assumes "\<And>x. x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1209 
shows "degree (map_poly f p) = degree p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1210 
by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1211 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1212 
lemma map_poly_eq_0_iff: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1213 
assumes "f 0 = 0" "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> f x \<noteq> 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1214 
shows "map_poly f p = 0 \<longleftrightarrow> p = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1215 
proof  
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1216 
{ 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1217 
fix n :: nat 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1218 
have "coeff (map_poly f p) n = f (coeff p n)" by (simp add: coeff_map_poly assms) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1219 
also have "\<dots> = 0 \<longleftrightarrow> coeff p n = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1220 
proof (cases "n < length (coeffs p)") 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1221 
case True 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1222 
hence "coeff p n \<in> set (coeffs p)" by (auto simp: coeffs_def simp del: upt_Suc) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1223 
with assms show "f (coeff p n) = 0 \<longleftrightarrow> coeff p n = 0" by auto 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1224 
qed (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1225 
finally have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" . 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1226 
} 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1227 
thus ?thesis by (auto simp: poly_eq_iff) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1228 
qed 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1229 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1230 
lemma map_poly_smult: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1231 
assumes "f 0 = 0""\<And>c x. f (c * x) = f c * f x" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1232 
shows "map_poly f (smult c p) = smult (f c) (map_poly f p)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1233 
by (intro poly_eqI) (simp_all add: assms coeff_map_poly) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1234 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1235 
lemma map_poly_pCons: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1236 
assumes "f 0 = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1237 
shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1238 
by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1239 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1240 
lemma map_poly_map_poly: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1241 
assumes "f 0 = 0" "g 0 = 0" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1242 
shows "map_poly f (map_poly g p) = map_poly (f \<circ> g) p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1243 
by (intro poly_eqI) (simp add: coeff_map_poly assms) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1244 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1245 
lemma map_poly_id [simp]: "map_poly id p = p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1246 
by (simp add: map_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1247 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1248 
lemma map_poly_id' [simp]: "map_poly (\<lambda>x. x) p = p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1249 
by (simp add: map_poly_def) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1250 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1251 
lemma map_poly_cong: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1252 
assumes "(\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = g x)" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1253 
shows "map_poly f p = map_poly g p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1254 
proof  
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1255 
from assms have "map f (coeffs p) = map g (coeffs p)" by (intro map_cong) simp_all 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1256 
thus ?thesis by (simp only: coeffs_eq_iff coeffs_map_poly) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1257 
qed 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1258 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1259 
lemma map_poly_monom: "f 0 = 0 \<Longrightarrow> map_poly f (monom c n) = monom (f c) n" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1260 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1261 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1262 
lemma map_poly_idI: 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1263 
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1264 
shows "map_poly f p = p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1265 
using map_poly_cong[OF assms, of _ id] by simp 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1266 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1267 
lemma map_poly_idI': 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1268 
assumes "\<And>x. x \<in> set (coeffs p) \<Longrightarrow> f x = x" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1269 
shows "p = map_poly f p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1270 
using map_poly_cong[OF assms, of _ id] by simp 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1271 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1272 
lemma smult_conv_map_poly: "smult c p = map_poly (\<lambda>x. c * x) p" 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1273 
by (intro poly_eqI) (simp_all add: coeff_map_poly) 
240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1274 

240a39af9ec4
restructured matter on polynomials and normalized fractions
haftmann
parents:
64272
diff
changeset

1275 

64793  1276 
subsection \<open>Conversions from @{typ nat} and @{typ int} numbers\<close> 
62065  1277 

1278 
lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]" 

1279 
proof (induction n) 

1280 
case (Suc n) 

1281 
hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)" 

1282 
by simp 

1283 
also have "(of_nat n :: 'a poly) = [: of_nat n :]" 

1284 
by (subst Suc) (rule refl) 

1285 
also have "1 = [:1:]" by (simp add: one_poly_def) 

1286 
finally show ?case by (subst (asm) add_pCons) simp 

1287 
qed simp 

1288 

1289 
lemma degree_of_nat [simp]: "degree (of_nat n) = 0" 

1290 
by (simp add: of_nat_poly) 

1291 

64795  1292 
lemma lead_coeff_of_nat [simp]: 
1293 
"lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})" 

1294 
by (simp add: of_nat_poly) 

1295 

1296 
lemma of_int_poly: "of_int k = [:of_int k :: 'a :: comm_ring_1:]" 

64793  1297 
by (simp only: of_int_of_nat of_nat_poly) simp 
1298 

64795
8e7db8df16a0
tuned structure
haftman 