1 (* Title: HOL/Library/Polynomial.thy |
1 (* Title: HOL/Library/Polynomial.thy |
2 Author: Brian Huffman |
2 Author: Brian Huffman |
3 Author: Clemens Ballarin |
3 Author: Clemens Ballarin |
|
4 Author: Florian Haftmann |
4 *) |
5 *) |
5 |
6 |
6 header {* Univariate Polynomials *} |
7 header {* Polynomials as type over a ring structure *} |
7 |
8 |
8 theory Polynomial |
9 theory Polynomial |
9 imports Main |
10 imports Main GCD |
10 begin |
11 begin |
11 |
12 |
|
13 subsection {* Auxiliary: operations for lists (later) representing coefficients *} |
|
14 |
|
15 definition strip_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
16 where |
|
17 "strip_while P = rev \<circ> dropWhile P \<circ> rev" |
|
18 |
|
19 lemma strip_while_Nil [simp]: |
|
20 "strip_while P [] = []" |
|
21 by (simp add: strip_while_def) |
|
22 |
|
23 lemma strip_while_append [simp]: |
|
24 "\<not> P x \<Longrightarrow> strip_while P (xs @ [x]) = xs @ [x]" |
|
25 by (simp add: strip_while_def) |
|
26 |
|
27 lemma strip_while_append_rec [simp]: |
|
28 "P x \<Longrightarrow> strip_while P (xs @ [x]) = strip_while P xs" |
|
29 by (simp add: strip_while_def) |
|
30 |
|
31 lemma strip_while_Cons [simp]: |
|
32 "\<not> P x \<Longrightarrow> strip_while P (x # xs) = x # strip_while P xs" |
|
33 by (induct xs rule: rev_induct) (simp_all add: strip_while_def) |
|
34 |
|
35 lemma strip_while_eq_Nil [simp]: |
|
36 "strip_while P xs = [] \<longleftrightarrow> (\<forall>x\<in>set xs. P x)" |
|
37 by (simp add: strip_while_def) |
|
38 |
|
39 lemma strip_while_eq_Cons_rec: |
|
40 "strip_while P (x # xs) = x # strip_while P xs \<longleftrightarrow> \<not> (P x \<and> (\<forall>x\<in>set xs. P x))" |
|
41 by (induct xs rule: rev_induct) (simp_all add: strip_while_def) |
|
42 |
|
43 lemma strip_while_not_last [simp]: |
|
44 "\<not> P (last xs) \<Longrightarrow> strip_while P xs = xs" |
|
45 by (cases xs rule: rev_cases) simp_all |
|
46 |
|
47 lemma split_strip_while_append: |
|
48 fixes xs :: "'a list" |
|
49 obtains ys zs :: "'a list" |
|
50 where "strip_while P xs = ys" and "\<forall>x\<in>set zs. P x" and "xs = ys @ zs" |
|
51 proof (rule that) |
|
52 show "strip_while P xs = strip_while P xs" .. |
|
53 show "\<forall>x\<in>set (rev (takeWhile P (rev xs))). P x" by (simp add: takeWhile_eq_all_conv [symmetric]) |
|
54 have "rev xs = rev (strip_while P xs @ rev (takeWhile P (rev xs)))" |
|
55 by (simp add: strip_while_def) |
|
56 then show "xs = strip_while P xs @ rev (takeWhile P (rev xs))" |
|
57 by (simp only: rev_is_rev_conv) |
|
58 qed |
|
59 |
|
60 |
|
61 definition nth_default :: "'a \<Rightarrow> 'a list \<Rightarrow> nat \<Rightarrow> 'a" |
|
62 where |
|
63 "nth_default x xs n = (if n < length xs then xs ! n else x)" |
|
64 |
|
65 lemma nth_default_Nil [simp]: |
|
66 "nth_default y [] n = y" |
|
67 by (simp add: nth_default_def) |
|
68 |
|
69 lemma nth_default_Cons_0 [simp]: |
|
70 "nth_default y (x # xs) 0 = x" |
|
71 by (simp add: nth_default_def) |
|
72 |
|
73 lemma nth_default_Cons_Suc [simp]: |
|
74 "nth_default y (x # xs) (Suc n) = nth_default y xs n" |
|
75 by (simp add: nth_default_def) |
|
76 |
|
77 lemma nth_default_map_eq: |
|
78 "f y = x \<Longrightarrow> nth_default x (map f xs) n = f (nth_default y xs n)" |
|
79 by (simp add: nth_default_def) |
|
80 |
|
81 lemma nth_default_strip_while_eq [simp]: |
|
82 "nth_default x (strip_while (HOL.eq x) xs) n = nth_default x xs n" |
|
83 proof - |
|
84 from split_strip_while_append obtain ys zs |
|
85 where "strip_while (HOL.eq x) xs = ys" and "\<forall>z\<in>set zs. x = z" and "xs = ys @ zs" by blast |
|
86 then show ?thesis by (simp add: nth_default_def not_less nth_append) |
|
87 qed |
|
88 |
|
89 |
|
90 definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixr "##" 65) |
|
91 where |
|
92 "x ## xs = (if xs = [] \<and> x = 0 then [] else x # xs)" |
|
93 |
|
94 lemma cCons_0_Nil_eq [simp]: |
|
95 "0 ## [] = []" |
|
96 by (simp add: cCons_def) |
|
97 |
|
98 lemma cCons_Cons_eq [simp]: |
|
99 "x ## y # ys = x # y # ys" |
|
100 by (simp add: cCons_def) |
|
101 |
|
102 lemma cCons_append_Cons_eq [simp]: |
|
103 "x ## xs @ y # ys = x # xs @ y # ys" |
|
104 by (simp add: cCons_def) |
|
105 |
|
106 lemma cCons_not_0_eq [simp]: |
|
107 "x \<noteq> 0 \<Longrightarrow> x ## xs = x # xs" |
|
108 by (simp add: cCons_def) |
|
109 |
|
110 lemma strip_while_not_0_Cons_eq [simp]: |
|
111 "strip_while (\<lambda>x. x = 0) (x # xs) = x ## strip_while (\<lambda>x. x = 0) xs" |
|
112 proof (cases "x = 0") |
|
113 case False then show ?thesis by simp |
|
114 next |
|
115 case True show ?thesis |
|
116 proof (induct xs rule: rev_induct) |
|
117 case Nil with True show ?case by simp |
|
118 next |
|
119 case (snoc y ys) then show ?case |
|
120 by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons) |
|
121 qed |
|
122 qed |
|
123 |
|
124 lemma tl_cCons [simp]: |
|
125 "tl (x ## xs) = xs" |
|
126 by (simp add: cCons_def) |
|
127 |
|
128 |
|
129 subsection {* Almost everywhere zero functions *} |
|
130 |
|
131 definition almost_everywhere_zero :: "(nat \<Rightarrow> 'a::zero) \<Rightarrow> bool" |
|
132 where |
|
133 "almost_everywhere_zero f \<longleftrightarrow> (\<exists>n. \<forall>i>n. f i = 0)" |
|
134 |
|
135 lemma almost_everywhere_zeroI: |
|
136 "(\<And>i. i > n \<Longrightarrow> f i = 0) \<Longrightarrow> almost_everywhere_zero f" |
|
137 by (auto simp add: almost_everywhere_zero_def) |
|
138 |
|
139 lemma almost_everywhere_zeroE: |
|
140 assumes "almost_everywhere_zero f" |
|
141 obtains n where "\<And>i. i > n \<Longrightarrow> f i = 0" |
|
142 proof - |
|
143 from assms have "\<exists>n. \<forall>i>n. f i = 0" by (simp add: almost_everywhere_zero_def) |
|
144 then obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by blast |
|
145 with that show thesis . |
|
146 qed |
|
147 |
|
148 lemma almost_everywhere_zero_nat_case: |
|
149 assumes "almost_everywhere_zero f" |
|
150 shows "almost_everywhere_zero (nat_case a f)" |
|
151 using assms |
|
152 by (auto intro!: almost_everywhere_zeroI elim!: almost_everywhere_zeroE split: nat.split) |
|
153 blast |
|
154 |
|
155 lemma almost_everywhere_zero_Suc: |
|
156 assumes "almost_everywhere_zero f" |
|
157 shows "almost_everywhere_zero (\<lambda>n. f (Suc n))" |
|
158 proof - |
|
159 from assms obtain n where "\<And>i. i > n \<Longrightarrow> f i = 0" by (erule almost_everywhere_zeroE) |
|
160 then have "\<And>i. i > n \<Longrightarrow> f (Suc i) = 0" by auto |
|
161 then show ?thesis by (rule almost_everywhere_zeroI) |
|
162 qed |
|
163 |
|
164 |
12 subsection {* Definition of type @{text poly} *} |
165 subsection {* Definition of type @{text poly} *} |
13 |
166 |
14 definition "Poly = {f::nat \<Rightarrow> 'a::zero. \<exists>n. \<forall>i>n. f i = 0}" |
167 typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. almost_everywhere_zero f}" |
15 |
|
16 typedef 'a poly = "Poly :: (nat => 'a::zero) set" |
|
17 morphisms coeff Abs_poly |
168 morphisms coeff Abs_poly |
18 unfolding Poly_def by auto |
169 unfolding almost_everywhere_zero_def by auto |
19 |
170 |
20 (* FIXME should be named poly_eq_iff *) |
171 setup_lifting (no_code) type_definition_poly |
21 lemma expand_poly_eq: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)" |
172 |
|
173 lemma poly_eq_iff: "p = q \<longleftrightarrow> (\<forall>n. coeff p n = coeff q n)" |
22 by (simp add: coeff_inject [symmetric] fun_eq_iff) |
174 by (simp add: coeff_inject [symmetric] fun_eq_iff) |
23 |
175 |
24 (* FIXME should be named poly_eqI *) |
176 lemma poly_eqI: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q" |
25 lemma poly_ext: "(\<And>n. coeff p n = coeff q n) \<Longrightarrow> p = q" |
177 by (simp add: poly_eq_iff) |
26 by (simp add: expand_poly_eq) |
178 |
|
179 lemma coeff_almost_everywhere_zero: |
|
180 "almost_everywhere_zero (coeff p)" |
|
181 using coeff [of p] by simp |
27 |
182 |
28 |
183 |
29 subsection {* Degree of a polynomial *} |
184 subsection {* Degree of a polynomial *} |
30 |
185 |
31 definition |
186 definition degree :: "'a::zero poly \<Rightarrow> nat" |
32 degree :: "'a::zero poly \<Rightarrow> nat" where |
187 where |
33 "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)" |
188 "degree p = (LEAST n. \<forall>i>n. coeff p i = 0)" |
34 |
189 |
35 lemma coeff_eq_0: "degree p < n \<Longrightarrow> coeff p n = 0" |
190 lemma coeff_eq_0: |
|
191 assumes "degree p < n" |
|
192 shows "coeff p n = 0" |
36 proof - |
193 proof - |
37 have "coeff p \<in> Poly" |
194 from coeff_almost_everywhere_zero |
38 by (rule coeff) |
195 have "\<exists>n. \<forall>i>n. coeff p i = 0" by (blast intro: almost_everywhere_zeroE) |
39 hence "\<exists>n. \<forall>i>n. coeff p i = 0" |
196 then have "\<forall>i>degree p. coeff p i = 0" |
40 unfolding Poly_def by simp |
|
41 hence "\<forall>i>degree p. coeff p i = 0" |
|
42 unfolding degree_def by (rule LeastI_ex) |
197 unfolding degree_def by (rule LeastI_ex) |
43 moreover assume "degree p < n" |
198 with assms show ?thesis by simp |
44 ultimately show ?thesis by simp |
|
45 qed |
199 qed |
46 |
200 |
47 lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p" |
201 lemma le_degree: "coeff p n \<noteq> 0 \<Longrightarrow> n \<le> degree p" |
48 by (erule contrapos_np, rule coeff_eq_0, simp) |
202 by (erule contrapos_np, rule coeff_eq_0, simp) |
49 |
203 |
91 also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree) |
248 also from `coeff p i \<noteq> 0` have "i \<le> degree p" by (rule le_degree) |
92 finally have "degree p = i" . |
249 finally have "degree p = i" . |
93 with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp |
250 with `coeff p i \<noteq> 0` show "coeff p (degree p) \<noteq> 0" by simp |
94 qed |
251 qed |
95 |
252 |
96 lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \<longleftrightarrow> p = 0" |
253 lemma leading_coeff_0_iff [simp]: |
|
254 "coeff p (degree p) = 0 \<longleftrightarrow> p = 0" |
97 by (cases "p = 0", simp, simp add: leading_coeff_neq_0) |
255 by (cases "p = 0", simp, simp add: leading_coeff_neq_0) |
98 |
256 |
99 |
257 |
100 subsection {* List-style constructor for polynomials *} |
258 subsection {* List-style constructor for polynomials *} |
101 |
259 |
102 definition |
260 lift_definition pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
103 pCons :: "'a::zero \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
261 is "\<lambda>a p. nat_case a (coeff p)" |
104 where |
262 using coeff_almost_everywhere_zero by (rule almost_everywhere_zero_nat_case) |
105 "pCons a p = Abs_poly (nat_case a (coeff p))" |
263 |
106 |
264 lemmas coeff_pCons = pCons.rep_eq |
107 syntax |
265 |
108 "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]") |
266 lemma coeff_pCons_0 [simp]: |
109 |
267 "coeff (pCons a p) 0 = a" |
110 translations |
268 by transfer simp |
111 "[:x, xs:]" == "CONST pCons x [:xs:]" |
269 |
112 "[:x:]" == "CONST pCons x 0" |
270 lemma coeff_pCons_Suc [simp]: |
113 "[:x:]" <= "CONST pCons x (_constrain 0 t)" |
271 "coeff (pCons a p) (Suc n) = coeff p n" |
114 |
|
115 lemma Poly_nat_case: "f \<in> Poly \<Longrightarrow> nat_case a f \<in> Poly" |
|
116 unfolding Poly_def by (auto split: nat.split) |
|
117 |
|
118 lemma coeff_pCons: |
|
119 "coeff (pCons a p) = nat_case a (coeff p)" |
|
120 unfolding pCons_def |
|
121 by (simp add: Abs_poly_inverse Poly_nat_case coeff) |
|
122 |
|
123 lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a" |
|
124 by (simp add: coeff_pCons) |
272 by (simp add: coeff_pCons) |
125 |
273 |
126 lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n" |
274 lemma degree_pCons_le: |
127 by (simp add: coeff_pCons) |
275 "degree (pCons a p) \<le> Suc (degree p)" |
128 |
276 by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split) |
129 lemma degree_pCons_le: "degree (pCons a p) \<le> Suc (degree p)" |
|
130 by (rule degree_le, simp add: coeff_eq_0 coeff_pCons split: nat.split) |
|
131 |
277 |
132 lemma degree_pCons_eq: |
278 lemma degree_pCons_eq: |
133 "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)" |
279 "p \<noteq> 0 \<Longrightarrow> degree (pCons a p) = Suc (degree p)" |
134 apply (rule order_antisym [OF degree_pCons_le]) |
280 apply (rule order_antisym [OF degree_pCons_le]) |
135 apply (rule le_degree, simp) |
281 apply (rule le_degree, simp) |
136 done |
282 done |
137 |
283 |
138 lemma degree_pCons_0: "degree (pCons a 0) = 0" |
284 lemma degree_pCons_0: |
139 apply (rule order_antisym [OF _ le0]) |
285 "degree (pCons a 0) = 0" |
140 apply (rule degree_le, simp add: coeff_pCons split: nat.split) |
286 apply (rule order_antisym [OF _ le0]) |
141 done |
287 apply (rule degree_le, simp add: coeff_pCons split: nat.split) |
|
288 done |
142 |
289 |
143 lemma degree_pCons_eq_if [simp]: |
290 lemma degree_pCons_eq_if [simp]: |
144 "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" |
291 "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))" |
145 apply (cases "p = 0", simp_all) |
292 apply (cases "p = 0", simp_all) |
146 apply (rule order_antisym [OF _ le0]) |
293 apply (rule order_antisym [OF _ le0]) |
147 apply (rule degree_le, simp add: coeff_pCons split: nat.split) |
294 apply (rule degree_le, simp add: coeff_pCons split: nat.split) |
148 apply (rule order_antisym [OF degree_pCons_le]) |
295 apply (rule order_antisym [OF degree_pCons_le]) |
149 apply (rule le_degree, simp) |
296 apply (rule le_degree, simp) |
150 done |
297 done |
151 |
298 |
152 lemma pCons_0_0 [simp, code_post]: "pCons 0 0 = 0" |
299 lemma pCons_0_0 [simp]: |
153 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
300 "pCons 0 0 = 0" |
|
301 by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) |
154 |
302 |
155 lemma pCons_eq_iff [simp]: |
303 lemma pCons_eq_iff [simp]: |
156 "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q" |
304 "pCons a p = pCons b q \<longleftrightarrow> a = b \<and> p = q" |
157 proof (safe) |
305 proof safe |
158 assume "pCons a p = pCons b q" |
306 assume "pCons a p = pCons b q" |
159 then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp |
307 then have "coeff (pCons a p) 0 = coeff (pCons b q) 0" by simp |
160 then show "a = b" by simp |
308 then show "a = b" by simp |
161 next |
309 next |
162 assume "pCons a p = pCons b q" |
310 assume "pCons a p = pCons b q" |
163 then have "\<forall>n. coeff (pCons a p) (Suc n) = |
311 then have "\<forall>n. coeff (pCons a p) (Suc n) = |
164 coeff (pCons b q) (Suc n)" by simp |
312 coeff (pCons b q) (Suc n)" by simp |
165 then show "p = q" by (simp add: expand_poly_eq) |
313 then show "p = q" by (simp add: poly_eq_iff) |
166 qed |
314 qed |
167 |
315 |
168 lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0" |
316 lemma pCons_eq_0_iff [simp]: |
|
317 "pCons a p = 0 \<longleftrightarrow> a = 0 \<and> p = 0" |
169 using pCons_eq_iff [of a p 0 0] by simp |
318 using pCons_eq_iff [of a p 0 0] by simp |
170 |
|
171 lemma Poly_Suc: "f \<in> Poly \<Longrightarrow> (\<lambda>n. f (Suc n)) \<in> Poly" |
|
172 unfolding Poly_def |
|
173 by (clarify, rule_tac x=n in exI, simp) |
|
174 |
319 |
175 lemma pCons_cases [cases type: poly]: |
320 lemma pCons_cases [cases type: poly]: |
176 obtains (pCons) a q where "p = pCons a q" |
321 obtains (pCons) a q where "p = pCons a q" |
177 proof |
322 proof |
178 show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))" |
323 show "p = pCons (coeff p 0) (Abs_poly (\<lambda>n. coeff p (Suc n)))" |
179 by (rule poly_ext) |
324 by transfer |
180 (simp add: Abs_poly_inverse Poly_Suc coeff coeff_pCons |
325 (simp add: Abs_poly_inverse almost_everywhere_zero_Suc fun_eq_iff split: nat.split) |
181 split: nat.split) |
|
182 qed |
326 qed |
183 |
327 |
184 lemma pCons_induct [case_names 0 pCons, induct type: poly]: |
328 lemma pCons_induct [case_names 0 pCons, induct type: poly]: |
185 assumes zero: "P 0" |
329 assumes zero: "P 0" |
186 assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)" |
330 assumes pCons: "\<And>a p. P p \<Longrightarrow> P (pCons a p)" |
206 then show ?case |
350 then show ?case |
207 using `p = pCons a q` by simp |
351 using `p = pCons a q` by simp |
208 qed |
352 qed |
209 |
353 |
210 |
354 |
211 subsection {* Recursion combinator for polynomials *} |
355 subsection {* List-style syntax for polynomials *} |
212 |
356 |
213 function |
357 syntax |
214 poly_rec :: "'b \<Rightarrow> ('a::zero \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b" |
358 "_poly" :: "args \<Rightarrow> 'a poly" ("[:(_):]") |
|
359 |
|
360 translations |
|
361 "[:x, xs:]" == "CONST pCons x [:xs:]" |
|
362 "[:x:]" == "CONST pCons x 0" |
|
363 "[:x:]" <= "CONST pCons x (_constrain 0 t)" |
|
364 |
|
365 |
|
366 subsection {* Representation of polynomials by lists of coefficients *} |
|
367 |
|
368 primrec Poly :: "'a::zero list \<Rightarrow> 'a poly" |
215 where |
369 where |
216 poly_rec_pCons_eq_if [simp del]: |
370 "Poly [] = 0" |
217 "poly_rec z f (pCons a p) = f a p (if p = 0 then z else poly_rec z f p)" |
371 | "Poly (a # as) = pCons a (Poly as)" |
218 by (case_tac x, rename_tac q, case_tac q, auto) |
372 |
219 |
373 lemma Poly_replicate_0 [simp]: |
220 termination poly_rec |
374 "Poly (replicate n 0) = 0" |
221 by (relation "measure (degree \<circ> snd \<circ> snd)", simp) |
375 by (induct n) simp_all |
222 (simp add: degree_pCons_eq) |
376 |
223 |
377 lemma Poly_eq_0: |
224 lemma poly_rec_0: |
378 "Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)" |
225 "f 0 0 z = z \<Longrightarrow> poly_rec z f 0 = z" |
379 by (induct as) (auto simp add: Cons_replicate_eq) |
226 using poly_rec_pCons_eq_if [of z f 0 0] by simp |
380 |
227 |
381 definition coeffs :: "'a poly \<Rightarrow> 'a::zero list" |
228 lemma poly_rec_pCons: |
382 where |
229 "f 0 0 z = z \<Longrightarrow> poly_rec z f (pCons a p) = f a p (poly_rec z f p)" |
383 "coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])" |
230 by (simp add: poly_rec_pCons_eq_if poly_rec_0) |
384 |
|
385 lemma coeffs_eq_Nil [simp]: |
|
386 "coeffs p = [] \<longleftrightarrow> p = 0" |
|
387 by (simp add: coeffs_def) |
|
388 |
|
389 lemma not_0_coeffs_not_Nil: |
|
390 "p \<noteq> 0 \<Longrightarrow> coeffs p \<noteq> []" |
|
391 by simp |
|
392 |
|
393 lemma coeffs_0_eq_Nil [simp]: |
|
394 "coeffs 0 = []" |
|
395 by simp |
|
396 |
|
397 lemma coeffs_pCons_eq_cCons [simp]: |
|
398 "coeffs (pCons a p) = a ## coeffs p" |
|
399 proof - |
|
400 { fix ms :: "nat list" and f :: "nat \<Rightarrow> 'a" and x :: "'a" |
|
401 assume "\<forall>m\<in>set ms. m > 0" |
|
402 then have "map (nat_case x f) ms = map f (map (\<lambda>n. n - 1) ms)" |
|
403 by (induct ms) (auto, metis Suc_pred' nat_case_Suc) } |
|
404 note * = this |
|
405 show ?thesis |
|
406 by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt One_nat_def del: upt_Suc) |
|
407 qed |
|
408 |
|
409 lemma not_0_cCons_eq [simp]: |
|
410 "p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p" |
|
411 by (simp add: cCons_def) |
|
412 |
|
413 lemma Poly_coeffs [simp, code abstype]: |
|
414 "Poly (coeffs p) = p" |
|
415 by (induct p) (simp_all add: cCons_def) |
|
416 |
|
417 lemma coeffs_Poly [simp]: |
|
418 "coeffs (Poly as) = strip_while (HOL.eq 0) as" |
|
419 proof (induct as) |
|
420 case Nil then show ?case by simp |
|
421 next |
|
422 case (Cons a as) |
|
423 have "(\<forall>n. as \<noteq> replicate n 0) \<longleftrightarrow> (\<exists>a\<in>set as. a \<noteq> 0)" |
|
424 using replicate_length_same [of as 0] by (auto dest: sym [of _ as]) |
|
425 with Cons show ?case by auto |
|
426 qed |
|
427 |
|
428 lemma last_coeffs_not_0: |
|
429 "p \<noteq> 0 \<Longrightarrow> last (coeffs p) \<noteq> 0" |
|
430 by (induct p) (auto simp add: cCons_def) |
|
431 |
|
432 lemma strip_while_coeffs [simp]: |
|
433 "strip_while (HOL.eq 0) (coeffs p) = coeffs p" |
|
434 by (cases "p = 0") (auto dest: last_coeffs_not_0 intro: strip_while_not_last) |
|
435 |
|
436 lemma coeffs_eq_iff: |
|
437 "p = q \<longleftrightarrow> coeffs p = coeffs q" (is "?P \<longleftrightarrow> ?Q") |
|
438 proof |
|
439 assume ?P then show ?Q by simp |
|
440 next |
|
441 assume ?Q |
|
442 then have "Poly (coeffs p) = Poly (coeffs q)" by simp |
|
443 then show ?P by simp |
|
444 qed |
|
445 |
|
446 lemma coeff_Poly_eq: |
|
447 "coeff (Poly xs) n = nth_default 0 xs n" |
|
448 apply (induct xs arbitrary: n) apply simp_all |
|
449 by (metis nat_case_0 nat_case_Suc not0_implies_Suc nth_default_Cons_0 nth_default_Cons_Suc pCons.rep_eq) |
|
450 |
|
451 lemma nth_default_coeffs_eq: |
|
452 "nth_default 0 (coeffs p) = coeff p" |
|
453 by (simp add: fun_eq_iff coeff_Poly_eq [symmetric]) |
|
454 |
|
455 lemma [code]: |
|
456 "coeff p = nth_default 0 (coeffs p)" |
|
457 by (simp add: nth_default_coeffs_eq) |
|
458 |
|
459 lemma coeffs_eqI: |
|
460 assumes coeff: "\<And>n. coeff p n = nth_default 0 xs n" |
|
461 assumes zero: "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" |
|
462 shows "coeffs p = xs" |
|
463 proof - |
|
464 from coeff have "p = Poly xs" by (simp add: poly_eq_iff coeff_Poly_eq) |
|
465 with zero show ?thesis by simp (cases xs, simp_all) |
|
466 qed |
|
467 |
|
468 lemma degree_eq_length_coeffs [code]: |
|
469 "degree p = length (coeffs p) - 1" |
|
470 by (simp add: coeffs_def) |
|
471 |
|
472 lemma length_coeffs_degree: |
|
473 "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = Suc (degree p)" |
|
474 by (induct p) (auto simp add: cCons_def) |
|
475 |
|
476 lemma [code abstract]: |
|
477 "coeffs 0 = []" |
|
478 by (fact coeffs_0_eq_Nil) |
|
479 |
|
480 lemma [code abstract]: |
|
481 "coeffs (pCons a p) = a ## coeffs p" |
|
482 by (fact coeffs_pCons_eq_cCons) |
|
483 |
|
484 instantiation poly :: ("{zero, equal}") equal |
|
485 begin |
|
486 |
|
487 definition |
|
488 [code]: "HOL.equal (p::'a poly) q \<longleftrightarrow> HOL.equal (coeffs p) (coeffs q)" |
|
489 |
|
490 instance proof |
|
491 qed (simp add: equal equal_poly_def coeffs_eq_iff) |
|
492 |
|
493 end |
|
494 |
|
495 lemma [code nbe]: |
|
496 "HOL.equal (p :: _ poly) p \<longleftrightarrow> True" |
|
497 by (fact equal_refl) |
|
498 |
|
499 definition is_zero :: "'a::zero poly \<Rightarrow> bool" |
|
500 where |
|
501 [code]: "is_zero p \<longleftrightarrow> List.null (coeffs p)" |
|
502 |
|
503 lemma is_zero_null [code_abbrev]: |
|
504 "is_zero p \<longleftrightarrow> p = 0" |
|
505 by (simp add: is_zero_def null_def) |
|
506 |
|
507 |
|
508 subsection {* Fold combinator for polynomials *} |
|
509 |
|
510 definition fold_coeffs :: "('a::zero \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a poly \<Rightarrow> 'b \<Rightarrow> 'b" |
|
511 where |
|
512 "fold_coeffs f p = foldr f (coeffs p)" |
|
513 |
|
514 lemma fold_coeffs_0_eq [simp]: |
|
515 "fold_coeffs f 0 = id" |
|
516 by (simp add: fold_coeffs_def) |
|
517 |
|
518 lemma fold_coeffs_pCons_eq [simp]: |
|
519 "f 0 = id \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" |
|
520 by (simp add: fold_coeffs_def cCons_def fun_eq_iff) |
|
521 |
|
522 lemma fold_coeffs_pCons_0_0_eq [simp]: |
|
523 "fold_coeffs f (pCons 0 0) = id" |
|
524 by (simp add: fold_coeffs_def) |
|
525 |
|
526 lemma fold_coeffs_pCons_coeff_not_0_eq [simp]: |
|
527 "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" |
|
528 by (simp add: fold_coeffs_def) |
|
529 |
|
530 lemma fold_coeffs_pCons_not_0_0_eq [simp]: |
|
531 "p \<noteq> 0 \<Longrightarrow> fold_coeffs f (pCons a p) = f a \<circ> fold_coeffs f p" |
|
532 by (simp add: fold_coeffs_def) |
|
533 |
|
534 |
|
535 subsection {* Canonical morphism on polynomials -- evaluation *} |
|
536 |
|
537 definition poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" |
|
538 where |
|
539 "poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)" -- {* The Horner Schema *} |
|
540 |
|
541 lemma poly_0 [simp]: |
|
542 "poly 0 x = 0" |
|
543 by (simp add: poly_def) |
|
544 |
|
545 lemma poly_pCons [simp]: |
|
546 "poly (pCons a p) x = a + x * poly p x" |
|
547 by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def) |
231 |
548 |
232 |
549 |
233 subsection {* Monomials *} |
550 subsection {* Monomials *} |
234 |
551 |
235 definition |
552 lift_definition monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" |
236 monom :: "'a \<Rightarrow> nat \<Rightarrow> 'a::zero poly" where |
553 is "\<lambda>a m n. if m = n then a else 0" |
237 "monom a m = Abs_poly (\<lambda>n. if m = n then a else 0)" |
554 by (auto intro!: almost_everywhere_zeroI) |
238 |
555 |
239 lemma coeff_monom [simp]: "coeff (monom a m) n = (if m=n then a else 0)" |
556 lemma coeff_monom [simp]: |
240 unfolding monom_def |
557 "coeff (monom a m) n = (if m = n then a else 0)" |
241 by (subst Abs_poly_inverse, auto simp add: Poly_def) |
558 by transfer rule |
242 |
559 |
243 lemma monom_0: "monom a 0 = pCons a 0" |
560 lemma monom_0: |
244 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
561 "monom a 0 = pCons a 0" |
245 |
562 by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) |
246 lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)" |
563 |
247 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
564 lemma monom_Suc: |
|
565 "monom a (Suc n) = pCons 0 (monom a n)" |
|
566 by (rule poly_eqI) (simp add: coeff_pCons split: nat.split) |
248 |
567 |
249 lemma monom_eq_0 [simp]: "monom 0 n = 0" |
568 lemma monom_eq_0 [simp]: "monom 0 n = 0" |
250 by (rule poly_ext) simp |
569 by (rule poly_eqI) simp |
251 |
570 |
252 lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0" |
571 lemma monom_eq_0_iff [simp]: "monom a n = 0 \<longleftrightarrow> a = 0" |
253 by (simp add: expand_poly_eq) |
572 by (simp add: poly_eq_iff) |
254 |
573 |
255 lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b" |
574 lemma monom_eq_iff [simp]: "monom a n = monom b n \<longleftrightarrow> a = b" |
256 by (simp add: expand_poly_eq) |
575 by (simp add: poly_eq_iff) |
257 |
576 |
258 lemma degree_monom_le: "degree (monom a n) \<le> n" |
577 lemma degree_monom_le: "degree (monom a n) \<le> n" |
259 by (rule degree_le, simp) |
578 by (rule degree_le, simp) |
260 |
579 |
261 lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n" |
580 lemma degree_monom_eq: "a \<noteq> 0 \<Longrightarrow> degree (monom a n) = n" |
262 apply (rule order_antisym [OF degree_monom_le]) |
581 apply (rule order_antisym [OF degree_monom_le]) |
263 apply (rule le_degree, simp) |
582 apply (rule le_degree, simp) |
264 done |
583 done |
265 |
584 |
|
585 lemma coeffs_monom [code abstract]: |
|
586 "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])" |
|
587 by (induct n) (simp_all add: monom_0 monom_Suc) |
|
588 |
|
589 lemma fold_coeffs_monom [simp]: |
|
590 "a \<noteq> 0 \<Longrightarrow> fold_coeffs f (monom a n) = f 0 ^^ n \<circ> f a" |
|
591 by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff) |
|
592 |
|
593 lemma poly_monom: |
|
594 fixes a x :: "'a::{comm_semiring_1}" |
|
595 shows "poly (monom a n) x = a * x ^ n" |
|
596 by (cases "a = 0", simp_all) |
|
597 (induct n, simp_all add: mult.left_commute poly_def) |
|
598 |
266 |
599 |
267 subsection {* Addition and subtraction *} |
600 subsection {* Addition and subtraction *} |
268 |
601 |
269 instantiation poly :: (comm_monoid_add) comm_monoid_add |
602 instantiation poly :: (comm_monoid_add) comm_monoid_add |
270 begin |
603 begin |
271 |
604 |
272 definition |
605 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
273 plus_poly_def: |
606 is "\<lambda>p q n. coeff p n + coeff q n" |
274 "p + q = Abs_poly (\<lambda>n. coeff p n + coeff q n)" |
607 proof (rule almost_everywhere_zeroI) |
275 |
608 fix q p :: "'a poly" and i |
276 lemma Poly_add: |
609 assume "max (degree q) (degree p) < i" |
277 fixes f g :: "nat \<Rightarrow> 'a" |
610 then show "coeff p i + coeff q i = 0" |
278 shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n + g n) \<in> Poly" |
611 by (simp add: coeff_eq_0) |
279 unfolding Poly_def |
612 qed |
280 apply (clarify, rename_tac m n) |
|
281 apply (rule_tac x="max m n" in exI, simp) |
|
282 done |
|
283 |
613 |
284 lemma coeff_add [simp]: |
614 lemma coeff_add [simp]: |
285 "coeff (p + q) n = coeff p n + coeff q n" |
615 "coeff (p + q) n = coeff p n + coeff q n" |
286 unfolding plus_poly_def |
616 by (simp add: plus_poly.rep_eq) |
287 by (simp add: Abs_poly_inverse coeff Poly_add) |
|
288 |
617 |
289 instance proof |
618 instance proof |
290 fix p q r :: "'a poly" |
619 fix p q r :: "'a poly" |
291 show "(p + q) + r = p + (q + r)" |
620 show "(p + q) + r = p + (q + r)" |
292 by (simp add: expand_poly_eq add_assoc) |
621 by (simp add: poly_eq_iff add_assoc) |
293 show "p + q = q + p" |
622 show "p + q = q + p" |
294 by (simp add: expand_poly_eq add_commute) |
623 by (simp add: poly_eq_iff add_commute) |
295 show "0 + p = p" |
624 show "0 + p = p" |
296 by (simp add: expand_poly_eq) |
625 by (simp add: poly_eq_iff) |
297 qed |
626 qed |
298 |
627 |
299 end |
628 end |
300 |
629 |
301 instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add |
630 instance poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add |
302 proof |
631 proof |
303 fix p q r :: "'a poly" |
632 fix p q r :: "'a poly" |
304 assume "p + q = p + r" thus "q = r" |
633 assume "p + q = p + r" thus "q = r" |
305 by (simp add: expand_poly_eq) |
634 by (simp add: poly_eq_iff) |
306 qed |
635 qed |
307 |
636 |
308 instantiation poly :: (ab_group_add) ab_group_add |
637 instantiation poly :: (ab_group_add) ab_group_add |
309 begin |
638 begin |
310 |
639 |
311 definition |
640 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly" |
312 uminus_poly_def: |
641 is "\<lambda>p n. - coeff p n" |
313 "- p = Abs_poly (\<lambda>n. - coeff p n)" |
642 proof (rule almost_everywhere_zeroI) |
314 |
643 fix p :: "'a poly" and i |
315 definition |
644 assume "degree p < i" |
316 minus_poly_def: |
645 then show "- coeff p i = 0" |
317 "p - q = Abs_poly (\<lambda>n. coeff p n - coeff q n)" |
646 by (simp add: coeff_eq_0) |
318 |
647 qed |
319 lemma Poly_minus: |
648 |
320 fixes f :: "nat \<Rightarrow> 'a" |
649 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
321 shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. - f n) \<in> Poly" |
650 is "\<lambda>p q n. coeff p n - coeff q n" |
322 unfolding Poly_def by simp |
651 proof (rule almost_everywhere_zeroI) |
323 |
652 fix q p :: "'a poly" and i |
324 lemma Poly_diff: |
653 assume "max (degree q) (degree p) < i" |
325 fixes f g :: "nat \<Rightarrow> 'a" |
654 then show "coeff p i - coeff q i = 0" |
326 shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. f n - g n) \<in> Poly" |
655 by (simp add: coeff_eq_0) |
327 unfolding diff_minus by (simp add: Poly_add Poly_minus) |
656 qed |
328 |
657 |
329 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n" |
658 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n" |
330 unfolding uminus_poly_def |
659 by (simp add: uminus_poly.rep_eq) |
331 by (simp add: Abs_poly_inverse coeff Poly_minus) |
|
332 |
660 |
333 lemma coeff_diff [simp]: |
661 lemma coeff_diff [simp]: |
334 "coeff (p - q) n = coeff p n - coeff q n" |
662 "coeff (p - q) n = coeff p n - coeff q n" |
335 unfolding minus_poly_def |
663 by (simp add: minus_poly.rep_eq) |
336 by (simp add: Abs_poly_inverse coeff Poly_diff) |
|
337 |
664 |
338 instance proof |
665 instance proof |
339 fix p q :: "'a poly" |
666 fix p q :: "'a poly" |
340 show "- p + p = 0" |
667 show "- p + p = 0" |
341 by (simp add: expand_poly_eq) |
668 by (simp add: poly_eq_iff) |
342 show "p - q = p + - q" |
669 show "p - q = p + - q" |
343 by (simp add: expand_poly_eq diff_minus) |
670 by (simp add: poly_eq_iff diff_minus) |
344 qed |
671 qed |
345 |
672 |
346 end |
673 end |
347 |
674 |
348 lemma add_pCons [simp]: |
675 lemma add_pCons [simp]: |
349 "pCons a p + pCons b q = pCons (a + b) (p + q)" |
676 "pCons a p + pCons b q = pCons (a + b) (p + q)" |
350 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
677 by (rule poly_eqI, simp add: coeff_pCons split: nat.split) |
351 |
678 |
352 lemma minus_pCons [simp]: |
679 lemma minus_pCons [simp]: |
353 "- pCons a p = pCons (- a) (- p)" |
680 "- pCons a p = pCons (- a) (- p)" |
354 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
681 by (rule poly_eqI, simp add: coeff_pCons split: nat.split) |
355 |
682 |
356 lemma diff_pCons [simp]: |
683 lemma diff_pCons [simp]: |
357 "pCons a p - pCons b q = pCons (a - b) (p - q)" |
684 "pCons a p - pCons b q = pCons (a - b) (p - q)" |
358 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
685 by (rule poly_eqI, simp add: coeff_pCons split: nat.split) |
359 |
686 |
360 lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)" |
687 lemma degree_add_le_max: "degree (p + q) \<le> max (degree p) (degree q)" |
361 by (rule degree_le, auto simp add: coeff_eq_0) |
688 by (rule degree_le, auto simp add: coeff_eq_0) |
362 |
689 |
363 lemma degree_add_le: |
690 lemma degree_add_le: |
396 lemma degree_diff_less: |
723 lemma degree_diff_less: |
397 "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n" |
724 "\<lbrakk>degree p < n; degree q < n\<rbrakk> \<Longrightarrow> degree (p - q) < n" |
398 by (simp add: diff_minus degree_add_less) |
725 by (simp add: diff_minus degree_add_less) |
399 |
726 |
400 lemma add_monom: "monom a n + monom b n = monom (a + b) n" |
727 lemma add_monom: "monom a n + monom b n = monom (a + b) n" |
401 by (rule poly_ext) simp |
728 by (rule poly_eqI) simp |
402 |
729 |
403 lemma diff_monom: "monom a n - monom b n = monom (a - b) n" |
730 lemma diff_monom: "monom a n - monom b n = monom (a - b) n" |
404 by (rule poly_ext) simp |
731 by (rule poly_eqI) simp |
405 |
732 |
406 lemma minus_monom: "- monom a n = monom (-a) n" |
733 lemma minus_monom: "- monom a n = monom (-a) n" |
407 by (rule poly_ext) simp |
734 by (rule poly_eqI) simp |
408 |
735 |
409 lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)" |
736 lemma coeff_setsum: "coeff (\<Sum>x\<in>A. p x) i = (\<Sum>x\<in>A. coeff (p x) i)" |
410 by (cases "finite A", induct set: finite, simp_all) |
737 by (cases "finite A", induct set: finite, simp_all) |
411 |
738 |
412 lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)" |
739 lemma monom_setsum: "monom (\<Sum>x\<in>A. a x) n = (\<Sum>x\<in>A. monom (a x) n)" |
413 by (rule poly_ext) (simp add: coeff_setsum) |
740 by (rule poly_eqI) (simp add: coeff_setsum) |
414 |
741 |
415 |
742 fun plus_coeffs :: "'a::comm_monoid_add list \<Rightarrow> 'a list \<Rightarrow> 'a list" |
416 subsection {* Multiplication by a constant *} |
743 where |
417 |
744 "plus_coeffs xs [] = xs" |
418 definition |
745 | "plus_coeffs [] ys = ys" |
419 smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
746 | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys" |
420 "smult a p = Abs_poly (\<lambda>n. a * coeff p n)" |
747 |
421 |
748 lemma coeffs_plus_eq_plus_coeffs [code abstract]: |
422 lemma Poly_smult: |
749 "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)" |
423 fixes f :: "nat \<Rightarrow> 'a::comm_semiring_0" |
750 proof - |
424 shows "f \<in> Poly \<Longrightarrow> (\<lambda>n. a * f n) \<in> Poly" |
751 { fix xs ys :: "'a list" and n |
425 unfolding Poly_def |
752 have "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n" |
426 by (clarify, rule_tac x=n in exI, simp) |
753 proof (induct xs ys arbitrary: n rule: plus_coeffs.induct) |
427 |
754 case (3 x xs y ys n) then show ?case by (cases n) (auto simp add: cCons_def) |
428 lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n" |
755 qed simp_all } |
429 unfolding smult_def |
756 note * = this |
430 by (simp add: Abs_poly_inverse Poly_smult coeff) |
757 { fix xs ys :: "'a list" |
|
758 assume "xs \<noteq> [] \<Longrightarrow> last xs \<noteq> 0" and "ys \<noteq> [] \<Longrightarrow> last ys \<noteq> 0" |
|
759 moreover assume "plus_coeffs xs ys \<noteq> []" |
|
760 ultimately have "last (plus_coeffs xs ys) \<noteq> 0" |
|
761 proof (induct xs ys rule: plus_coeffs.induct) |
|
762 case (3 x xs y ys) then show ?case by (auto simp add: cCons_def) metis |
|
763 qed simp_all } |
|
764 note ** = this |
|
765 show ?thesis |
|
766 apply (rule coeffs_eqI) |
|
767 apply (simp add: * nth_default_coeffs_eq) |
|
768 apply (rule **) |
|
769 apply (auto dest: last_coeffs_not_0) |
|
770 done |
|
771 qed |
|
772 |
|
773 lemma coeffs_uminus [code abstract]: |
|
774 "coeffs (- p) = map (\<lambda>a. - a) (coeffs p)" |
|
775 by (rule coeffs_eqI) |
|
776 (simp_all add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) |
|
777 |
|
778 lemma [code]: |
|
779 fixes p q :: "'a::ab_group_add poly" |
|
780 shows "p - q = p + - q" |
|
781 by simp |
|
782 |
|
783 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
|
784 apply (induct p arbitrary: q, simp) |
|
785 apply (case_tac q, simp, simp add: algebra_simps) |
|
786 done |
|
787 |
|
788 lemma poly_minus [simp]: |
|
789 fixes x :: "'a::comm_ring" |
|
790 shows "poly (- p) x = - poly p x" |
|
791 by (induct p) simp_all |
|
792 |
|
793 lemma poly_diff [simp]: |
|
794 fixes x :: "'a::comm_ring" |
|
795 shows "poly (p - q) x = poly p x - poly q x" |
|
796 by (simp add: diff_minus) |
|
797 |
|
798 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
|
799 by (induct A rule: infinite_finite_induct) simp_all |
|
800 |
|
801 |
|
802 subsection {* Multiplication by a constant, polynomial multiplication and the unit polynomial *} |
|
803 |
|
804 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
|
805 is "\<lambda>a p n. a * coeff p n" |
|
806 proof (rule almost_everywhere_zeroI) |
|
807 fix a :: 'a and p :: "'a poly" and i |
|
808 assume "degree p < i" |
|
809 then show "a * coeff p i = 0" |
|
810 by (simp add: coeff_eq_0) |
|
811 qed |
|
812 |
|
813 lemma coeff_smult [simp]: |
|
814 "coeff (smult a p) n = a * coeff p n" |
|
815 by (simp add: smult.rep_eq) |
431 |
816 |
432 lemma degree_smult_le: "degree (smult a p) \<le> degree p" |
817 lemma degree_smult_le: "degree (smult a p) \<le> degree p" |
433 by (rule degree_le, simp add: coeff_eq_0) |
818 by (rule degree_le, simp add: coeff_eq_0) |
434 |
819 |
435 lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" |
820 lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p" |
436 by (rule poly_ext, simp add: mult_assoc) |
821 by (rule poly_eqI, simp add: mult_assoc) |
437 |
822 |
438 lemma smult_0_right [simp]: "smult a 0 = 0" |
823 lemma smult_0_right [simp]: "smult a 0 = 0" |
439 by (rule poly_ext, simp) |
824 by (rule poly_eqI, simp) |
440 |
825 |
441 lemma smult_0_left [simp]: "smult 0 p = 0" |
826 lemma smult_0_left [simp]: "smult 0 p = 0" |
442 by (rule poly_ext, simp) |
827 by (rule poly_eqI, simp) |
443 |
828 |
444 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" |
829 lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p" |
445 by (rule poly_ext, simp) |
830 by (rule poly_eqI, simp) |
446 |
831 |
447 lemma smult_add_right: |
832 lemma smult_add_right: |
448 "smult a (p + q) = smult a p + smult a q" |
833 "smult a (p + q) = smult a p + smult a q" |
449 by (rule poly_ext, simp add: algebra_simps) |
834 by (rule poly_eqI, simp add: algebra_simps) |
450 |
835 |
451 lemma smult_add_left: |
836 lemma smult_add_left: |
452 "smult (a + b) p = smult a p + smult b p" |
837 "smult (a + b) p = smult a p + smult b p" |
453 by (rule poly_ext, simp add: algebra_simps) |
838 by (rule poly_eqI, simp add: algebra_simps) |
454 |
839 |
455 lemma smult_minus_right [simp]: |
840 lemma smult_minus_right [simp]: |
456 "smult (a::'a::comm_ring) (- p) = - smult a p" |
841 "smult (a::'a::comm_ring) (- p) = - smult a p" |
457 by (rule poly_ext, simp) |
842 by (rule poly_eqI, simp) |
458 |
843 |
459 lemma smult_minus_left [simp]: |
844 lemma smult_minus_left [simp]: |
460 "smult (- a::'a::comm_ring) p = - smult a p" |
845 "smult (- a::'a::comm_ring) p = - smult a p" |
461 by (rule poly_ext, simp) |
846 by (rule poly_eqI, simp) |
462 |
847 |
463 lemma smult_diff_right: |
848 lemma smult_diff_right: |
464 "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" |
849 "smult (a::'a::comm_ring) (p - q) = smult a p - smult a q" |
465 by (rule poly_ext, simp add: algebra_simps) |
850 by (rule poly_eqI, simp add: algebra_simps) |
466 |
851 |
467 lemma smult_diff_left: |
852 lemma smult_diff_left: |
468 "smult (a - b::'a::comm_ring) p = smult a p - smult b p" |
853 "smult (a - b::'a::comm_ring) p = smult a p - smult b p" |
469 by (rule poly_ext, simp add: algebra_simps) |
854 by (rule poly_eqI, simp add: algebra_simps) |
470 |
855 |
471 lemmas smult_distribs = |
856 lemmas smult_distribs = |
472 smult_add_left smult_add_right |
857 smult_add_left smult_add_right |
473 smult_diff_left smult_diff_right |
858 smult_diff_left smult_diff_right |
474 |
859 |
475 lemma smult_pCons [simp]: |
860 lemma smult_pCons [simp]: |
476 "smult a (pCons b p) = pCons (a * b) (smult a p)" |
861 "smult a (pCons b p) = pCons (a * b) (smult a p)" |
477 by (rule poly_ext, simp add: coeff_pCons split: nat.split) |
862 by (rule poly_eqI, simp add: coeff_pCons split: nat.split) |
478 |
863 |
479 lemma smult_monom: "smult a (monom b n) = monom (a * b) n" |
864 lemma smult_monom: "smult a (monom b n) = monom (a * b) n" |
480 by (induct n, simp add: monom_0, simp add: monom_Suc) |
865 by (induct n, simp add: monom_0, simp add: monom_Suc) |
481 |
866 |
482 lemma degree_smult_eq [simp]: |
867 lemma degree_smult_eq [simp]: |
485 by (cases "a = 0", simp, simp add: degree_def) |
870 by (cases "a = 0", simp, simp add: degree_def) |
486 |
871 |
487 lemma smult_eq_0_iff [simp]: |
872 lemma smult_eq_0_iff [simp]: |
488 fixes a :: "'a::idom" |
873 fixes a :: "'a::idom" |
489 shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0" |
874 shows "smult a p = 0 \<longleftrightarrow> a = 0 \<or> p = 0" |
490 by (simp add: expand_poly_eq) |
875 by (simp add: poly_eq_iff) |
491 |
876 |
492 |
877 lemma coeffs_smult [code abstract]: |
493 subsection {* Multiplication of polynomials *} |
878 fixes p :: "'a::idom poly" |
494 |
879 shows "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))" |
495 (* TODO: move to Set_Interval.thy *) |
880 by (rule coeffs_eqI) |
496 lemma setsum_atMost_Suc_shift: |
881 (auto simp add: not_0_coeffs_not_Nil last_map last_coeffs_not_0 nth_default_map_eq nth_default_coeffs_eq) |
497 fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" |
|
498 shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
|
499 proof (induct n) |
|
500 case 0 show ?case by simp |
|
501 next |
|
502 case (Suc n) note IH = this |
|
503 have "(\<Sum>i\<le>Suc (Suc n). f i) = (\<Sum>i\<le>Suc n. f i) + f (Suc (Suc n))" |
|
504 by (rule setsum_atMost_Suc) |
|
505 also have "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
|
506 by (rule IH) |
|
507 also have "f 0 + (\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = |
|
508 f 0 + ((\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)))" |
|
509 by (rule add_assoc) |
|
510 also have "(\<Sum>i\<le>n. f (Suc i)) + f (Suc (Suc n)) = (\<Sum>i\<le>Suc n. f (Suc i))" |
|
511 by (rule setsum_atMost_Suc [symmetric]) |
|
512 finally show ?case . |
|
513 qed |
|
514 |
882 |
515 instantiation poly :: (comm_semiring_0) comm_semiring_0 |
883 instantiation poly :: (comm_semiring_0) comm_semiring_0 |
516 begin |
884 begin |
517 |
885 |
518 definition |
886 definition |
519 times_poly_def: |
887 "p * q = fold_coeffs (\<lambda>a p. smult a q + pCons 0 p) p 0" |
520 "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p" |
|
521 |
888 |
522 lemma mult_poly_0_left: "(0::'a poly) * q = 0" |
889 lemma mult_poly_0_left: "(0::'a poly) * q = 0" |
523 unfolding times_poly_def by (simp add: poly_rec_0) |
890 by (simp add: times_poly_def) |
524 |
891 |
525 lemma mult_pCons_left [simp]: |
892 lemma mult_pCons_left [simp]: |
526 "pCons a p * q = smult a q + pCons 0 (p * q)" |
893 "pCons a p * q = smult a q + pCons 0 (p * q)" |
527 unfolding times_poly_def by (simp add: poly_rec_pCons) |
894 by (cases "p = 0 \<and> a = 0") (auto simp add: times_poly_def) |
528 |
895 |
529 lemma mult_poly_0_right: "p * (0::'a poly) = 0" |
896 lemma mult_poly_0_right: "p * (0::'a poly) = 0" |
530 by (induct p, simp add: mult_poly_0_left, simp) |
897 by (induct p) (simp add: mult_poly_0_left, simp) |
531 |
898 |
532 lemma mult_pCons_right [simp]: |
899 lemma mult_pCons_right [simp]: |
533 "p * pCons a q = smult a p + pCons 0 (p * q)" |
900 "p * pCons a q = smult a p + pCons 0 (p * q)" |
534 by (induct p, simp add: mult_poly_0_left, simp add: algebra_simps) |
901 by (induct p) (simp add: mult_poly_0_left, simp add: algebra_simps) |
535 |
902 |
536 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right |
903 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right |
537 |
904 |
538 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" |
905 lemma mult_smult_left [simp]: |
539 by (induct p, simp add: mult_poly_0, simp add: smult_add_right) |
906 "smult a p * q = smult a (p * q)" |
540 |
907 by (induct p) (simp add: mult_poly_0, simp add: smult_add_right) |
541 lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" |
908 |
542 by (induct q, simp add: mult_poly_0, simp add: smult_add_right) |
909 lemma mult_smult_right [simp]: |
|
910 "p * smult a q = smult a (p * q)" |
|
911 by (induct q) (simp add: mult_poly_0, simp add: smult_add_right) |
543 |
912 |
544 lemma mult_poly_add_left: |
913 lemma mult_poly_add_left: |
545 fixes p q r :: "'a poly" |
914 fixes p q r :: "'a poly" |
546 shows "(p + q) * r = p * r + q * r" |
915 shows "(p + q) * r = p * r + q * r" |
547 by (induct r, simp add: mult_poly_0, |
916 by (induct r) (simp add: mult_poly_0, simp add: smult_distribs algebra_simps) |
548 simp add: smult_distribs algebra_simps) |
|
549 |
917 |
550 instance proof |
918 instance proof |
551 fix p q r :: "'a poly" |
919 fix p q r :: "'a poly" |
552 show 0: "0 * p = 0" |
920 show 0: "0 * p = 0" |
553 by (rule mult_poly_0_left) |
921 by (rule mult_poly_0_left) |
800 end |
1199 end |
801 |
1200 |
802 text {* TODO: Simplification rules for comparisons *} |
1201 text {* TODO: Simplification rules for comparisons *} |
803 |
1202 |
804 |
1203 |
|
1204 subsection {* Synthetic division and polynomial roots *} |
|
1205 |
|
1206 text {* |
|
1207 Synthetic division is simply division by the linear polynomial @{term "x - c"}. |
|
1208 *} |
|
1209 |
|
1210 definition synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a" |
|
1211 where |
|
1212 "synthetic_divmod p c = fold_coeffs (\<lambda>a (q, r). (pCons r q, a + c * r)) p (0, 0)" |
|
1213 |
|
1214 definition synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly" |
|
1215 where |
|
1216 "synthetic_div p c = fst (synthetic_divmod p c)" |
|
1217 |
|
1218 lemma synthetic_divmod_0 [simp]: |
|
1219 "synthetic_divmod 0 c = (0, 0)" |
|
1220 by (simp add: synthetic_divmod_def) |
|
1221 |
|
1222 lemma synthetic_divmod_pCons [simp]: |
|
1223 "synthetic_divmod (pCons a p) c = (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" |
|
1224 by (cases "p = 0 \<and> a = 0") (auto simp add: synthetic_divmod_def) |
|
1225 |
|
1226 lemma synthetic_div_0 [simp]: |
|
1227 "synthetic_div 0 c = 0" |
|
1228 unfolding synthetic_div_def by simp |
|
1229 |
|
1230 lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0" |
|
1231 by (induct p arbitrary: a) simp_all |
|
1232 |
|
1233 lemma snd_synthetic_divmod: |
|
1234 "snd (synthetic_divmod p c) = poly p c" |
|
1235 by (induct p, simp, simp add: split_def) |
|
1236 |
|
1237 lemma synthetic_div_pCons [simp]: |
|
1238 "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)" |
|
1239 unfolding synthetic_div_def |
|
1240 by (simp add: split_def snd_synthetic_divmod) |
|
1241 |
|
1242 lemma synthetic_div_eq_0_iff: |
|
1243 "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0" |
|
1244 by (induct p, simp, case_tac p, simp) |
|
1245 |
|
1246 lemma degree_synthetic_div: |
|
1247 "degree (synthetic_div p c) = degree p - 1" |
|
1248 by (induct p, simp, simp add: synthetic_div_eq_0_iff) |
|
1249 |
|
1250 lemma synthetic_div_correct: |
|
1251 "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)" |
|
1252 by (induct p) simp_all |
|
1253 |
|
1254 lemma synthetic_div_unique: |
|
1255 "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c" |
|
1256 apply (induct p arbitrary: q r) |
|
1257 apply (simp, frule synthetic_div_unique_lemma, simp) |
|
1258 apply (case_tac q, force) |
|
1259 done |
|
1260 |
|
1261 lemma synthetic_div_correct': |
|
1262 fixes c :: "'a::comm_ring_1" |
|
1263 shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" |
|
1264 using synthetic_div_correct [of p c] |
|
1265 by (simp add: algebra_simps) |
|
1266 |
|
1267 lemma poly_eq_0_iff_dvd: |
|
1268 fixes c :: "'a::idom" |
|
1269 shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p" |
|
1270 proof |
|
1271 assume "poly p c = 0" |
|
1272 with synthetic_div_correct' [of c p] |
|
1273 have "p = [:-c, 1:] * synthetic_div p c" by simp |
|
1274 then show "[:-c, 1:] dvd p" .. |
|
1275 next |
|
1276 assume "[:-c, 1:] dvd p" |
|
1277 then obtain k where "p = [:-c, 1:] * k" by (rule dvdE) |
|
1278 then show "poly p c = 0" by simp |
|
1279 qed |
|
1280 |
|
1281 lemma dvd_iff_poly_eq_0: |
|
1282 fixes c :: "'a::idom" |
|
1283 shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0" |
|
1284 by (simp add: poly_eq_0_iff_dvd) |
|
1285 |
|
1286 lemma poly_roots_finite: |
|
1287 fixes p :: "'a::idom poly" |
|
1288 shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}" |
|
1289 proof (induct n \<equiv> "degree p" arbitrary: p) |
|
1290 case (0 p) |
|
1291 then obtain a where "a \<noteq> 0" and "p = [:a:]" |
|
1292 by (cases p, simp split: if_splits) |
|
1293 then show "finite {x. poly p x = 0}" by simp |
|
1294 next |
|
1295 case (Suc n p) |
|
1296 show "finite {x. poly p x = 0}" |
|
1297 proof (cases "\<exists>x. poly p x = 0") |
|
1298 case False |
|
1299 then show "finite {x. poly p x = 0}" by simp |
|
1300 next |
|
1301 case True |
|
1302 then obtain a where "poly p a = 0" .. |
|
1303 then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) |
|
1304 then obtain k where k: "p = [:-a, 1:] * k" .. |
|
1305 with `p \<noteq> 0` have "k \<noteq> 0" by auto |
|
1306 with k have "degree p = Suc (degree k)" |
|
1307 by (simp add: degree_mult_eq del: mult_pCons_left) |
|
1308 with `Suc n = degree p` have "n = degree k" by simp |
|
1309 then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps) |
|
1310 then have "finite (insert a {x. poly k x = 0})" by simp |
|
1311 then show "finite {x. poly p x = 0}" |
|
1312 by (simp add: k uminus_add_conv_diff Collect_disj_eq |
|
1313 del: mult_pCons_left) |
|
1314 qed |
|
1315 qed |
|
1316 |
|
1317 lemma poly_eq_poly_eq_iff: |
|
1318 fixes p q :: "'a::{idom,ring_char_0} poly" |
|
1319 shows "poly p = poly q \<longleftrightarrow> p = q" (is "?P \<longleftrightarrow> ?Q") |
|
1320 proof |
|
1321 assume ?Q then show ?P by simp |
|
1322 next |
|
1323 { fix p :: "'a::{idom,ring_char_0} poly" |
|
1324 have "poly p = poly 0 \<longleftrightarrow> p = 0" |
|
1325 apply (cases "p = 0", simp_all) |
|
1326 apply (drule poly_roots_finite) |
|
1327 apply (auto simp add: infinite_UNIV_char_0) |
|
1328 done |
|
1329 } note this [of "p - q"] |
|
1330 moreover assume ?P |
|
1331 ultimately show ?Q by auto |
|
1332 qed |
|
1333 |
|
1334 lemma poly_all_0_iff_0: |
|
1335 fixes p :: "'a::{ring_char_0, idom} poly" |
|
1336 shows "(\<forall>x. poly p x = 0) \<longleftrightarrow> p = 0" |
|
1337 by (auto simp add: poly_eq_poly_eq_iff [symmetric]) |
|
1338 |
|
1339 |
805 subsection {* Long division of polynomials *} |
1340 subsection {* Long division of polynomials *} |
806 |
1341 |
807 definition |
1342 definition pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" |
808 pdivmod_rel :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<Rightarrow> bool" |
|
809 where |
1343 where |
810 "pdivmod_rel x y q r \<longleftrightarrow> |
1344 "pdivmod_rel x y q r \<longleftrightarrow> |
811 x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)" |
1345 x = q * y + r \<and> (if y = 0 then q = 0 else r = 0 \<or> degree r < degree y)" |
812 |
1346 |
813 lemma pdivmod_rel_0: |
1347 lemma pdivmod_rel_0: |
1104 unfolding b |
1638 unfolding b |
1105 apply (rule mod_poly_eq) |
1639 apply (rule mod_poly_eq) |
1106 apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl]) |
1640 apply (rule pdivmod_rel_pCons [OF pdivmod_rel y refl]) |
1107 done |
1641 done |
1108 |
1642 |
1109 |
1643 definition pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" |
1110 subsection {* GCD of polynomials *} |
1644 where |
1111 |
1645 "pdivmod p q = (p div q, p mod q)" |
1112 function |
1646 |
1113 poly_gcd :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where |
1647 lemma div_poly_code [code]: |
1114 "poly_gcd x 0 = smult (inverse (coeff x (degree x))) x" |
1648 "p div q = fst (pdivmod p q)" |
1115 | "y \<noteq> 0 \<Longrightarrow> poly_gcd x y = poly_gcd y (x mod y)" |
1649 by (simp add: pdivmod_def) |
1116 by auto |
1650 |
1117 |
1651 lemma mod_poly_code [code]: |
1118 termination poly_gcd |
1652 "p mod q = snd (pdivmod p q)" |
1119 by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))") |
1653 by (simp add: pdivmod_def) |
1120 (auto dest: degree_mod_less) |
1654 |
1121 |
1655 lemma pdivmod_0: |
1122 declare poly_gcd.simps [simp del] |
1656 "pdivmod 0 q = (0, 0)" |
1123 |
1657 by (simp add: pdivmod_def) |
1124 lemma poly_gcd_dvd1 [iff]: "poly_gcd x y dvd x" |
1658 |
1125 and poly_gcd_dvd2 [iff]: "poly_gcd x y dvd y" |
1659 lemma pdivmod_pCons: |
1126 apply (induct x y rule: poly_gcd.induct) |
1660 "pdivmod (pCons a p) q = |
1127 apply (simp_all add: poly_gcd.simps) |
1661 (if q = 0 then (0, pCons a p) else |
1128 apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero) |
1662 (let (s, r) = pdivmod p q; |
1129 apply (blast dest: dvd_mod_imp_dvd) |
1663 b = coeff (pCons a r) (degree q) / coeff q (degree q) |
|
1664 in (pCons b s, pCons a r - smult b q)))" |
|
1665 apply (simp add: pdivmod_def Let_def, safe) |
|
1666 apply (rule div_poly_eq) |
|
1667 apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) |
|
1668 apply (rule mod_poly_eq) |
|
1669 apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) |
1130 done |
1670 done |
1131 |
1671 |
1132 lemma poly_gcd_greatest: "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd poly_gcd x y" |
1672 lemma pdivmod_fold_coeffs [code]: |
1133 by (induct x y rule: poly_gcd.induct) |
1673 "pdivmod p q = (if q = 0 then (0, p) |
1134 (simp_all add: poly_gcd.simps dvd_mod dvd_smult) |
1674 else fold_coeffs (\<lambda>a (s, r). |
1135 |
1675 let b = coeff (pCons a r) (degree q) / coeff q (degree q) |
1136 lemma dvd_poly_gcd_iff [iff]: |
1676 in (pCons b s, pCons a r - smult b q) |
1137 "k dvd poly_gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y" |
1677 ) p (0, 0))" |
1138 by (blast intro!: poly_gcd_greatest intro: dvd_trans) |
1678 apply (cases "q = 0") |
1139 |
1679 apply (simp add: pdivmod_def) |
1140 lemma poly_gcd_monic: |
1680 apply (rule sym) |
1141 "coeff (poly_gcd x y) (degree (poly_gcd x y)) = |
1681 apply (induct p) |
1142 (if x = 0 \<and> y = 0 then 0 else 1)" |
1682 apply (simp_all add: pdivmod_0 pdivmod_pCons) |
1143 by (induct x y rule: poly_gcd.induct) |
1683 apply (case_tac "a = 0 \<and> p = 0") |
1144 (simp_all add: poly_gcd.simps nonzero_imp_inverse_nonzero) |
1684 apply (auto simp add: pdivmod_def) |
1145 |
|
1146 lemma poly_gcd_zero_iff [simp]: |
|
1147 "poly_gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
|
1148 by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff) |
|
1149 |
|
1150 lemma poly_gcd_0_0 [simp]: "poly_gcd 0 0 = 0" |
|
1151 by simp |
|
1152 |
|
1153 lemma poly_dvd_antisym: |
|
1154 fixes p q :: "'a::idom poly" |
|
1155 assumes coeff: "coeff p (degree p) = coeff q (degree q)" |
|
1156 assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" |
|
1157 proof (cases "p = 0") |
|
1158 case True with coeff show "p = q" by simp |
|
1159 next |
|
1160 case False with coeff have "q \<noteq> 0" by auto |
|
1161 have degree: "degree p = degree q" |
|
1162 using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0` |
|
1163 by (intro order_antisym dvd_imp_degree_le) |
|
1164 |
|
1165 from `p dvd q` obtain a where a: "q = p * a" .. |
|
1166 with `q \<noteq> 0` have "a \<noteq> 0" by auto |
|
1167 with degree a `p \<noteq> 0` have "degree a = 0" |
|
1168 by (simp add: degree_mult_eq) |
|
1169 with coeff a show "p = q" |
|
1170 by (cases a, auto split: if_splits) |
|
1171 qed |
|
1172 |
|
1173 lemma poly_gcd_unique: |
|
1174 assumes dvd1: "d dvd x" and dvd2: "d dvd y" |
|
1175 and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d" |
|
1176 and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
1177 shows "poly_gcd x y = d" |
|
1178 proof - |
|
1179 have "coeff (poly_gcd x y) (degree (poly_gcd x y)) = coeff d (degree d)" |
|
1180 by (simp_all add: poly_gcd_monic monic) |
|
1181 moreover have "poly_gcd x y dvd d" |
|
1182 using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest) |
|
1183 moreover have "d dvd poly_gcd x y" |
|
1184 using dvd1 dvd2 by (rule poly_gcd_greatest) |
|
1185 ultimately show ?thesis |
|
1186 by (rule poly_dvd_antisym) |
|
1187 qed |
|
1188 |
|
1189 interpretation poly_gcd: abel_semigroup poly_gcd |
|
1190 proof |
|
1191 fix x y z :: "'a poly" |
|
1192 show "poly_gcd (poly_gcd x y) z = poly_gcd x (poly_gcd y z)" |
|
1193 by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic) |
|
1194 show "poly_gcd x y = poly_gcd y x" |
|
1195 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1196 qed |
|
1197 |
|
1198 lemmas poly_gcd_assoc = poly_gcd.assoc |
|
1199 lemmas poly_gcd_commute = poly_gcd.commute |
|
1200 lemmas poly_gcd_left_commute = poly_gcd.left_commute |
|
1201 |
|
1202 lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute |
|
1203 |
|
1204 lemma poly_gcd_1_left [simp]: "poly_gcd 1 y = 1" |
|
1205 by (rule poly_gcd_unique) simp_all |
|
1206 |
|
1207 lemma poly_gcd_1_right [simp]: "poly_gcd x 1 = 1" |
|
1208 by (rule poly_gcd_unique) simp_all |
|
1209 |
|
1210 lemma poly_gcd_minus_left [simp]: "poly_gcd (- x) y = poly_gcd x y" |
|
1211 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1212 |
|
1213 lemma poly_gcd_minus_right [simp]: "poly_gcd x (- y) = poly_gcd x y" |
|
1214 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1215 |
|
1216 |
|
1217 subsection {* Evaluation of polynomials *} |
|
1218 |
|
1219 definition |
|
1220 poly :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a" where |
|
1221 "poly = poly_rec (\<lambda>x. 0) (\<lambda>a p f x. a + x * f x)" |
|
1222 |
|
1223 lemma poly_0 [simp]: "poly 0 x = 0" |
|
1224 unfolding poly_def by (simp add: poly_rec_0) |
|
1225 |
|
1226 lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x" |
|
1227 unfolding poly_def by (simp add: poly_rec_pCons) |
|
1228 |
|
1229 lemma poly_1 [simp]: "poly 1 x = 1" |
|
1230 unfolding one_poly_def by simp |
|
1231 |
|
1232 lemma poly_monom: |
|
1233 fixes a x :: "'a::{comm_semiring_1}" |
|
1234 shows "poly (monom a n) x = a * x ^ n" |
|
1235 by (induct n, simp add: monom_0, simp add: monom_Suc power_Suc mult_ac) |
|
1236 |
|
1237 lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x" |
|
1238 apply (induct p arbitrary: q, simp) |
|
1239 apply (case_tac q, simp, simp add: algebra_simps) |
|
1240 done |
1685 done |
1241 |
1686 |
1242 lemma poly_minus [simp]: |
|
1243 fixes x :: "'a::comm_ring" |
|
1244 shows "poly (- p) x = - poly p x" |
|
1245 by (induct p, simp_all) |
|
1246 |
|
1247 lemma poly_diff [simp]: |
|
1248 fixes x :: "'a::comm_ring" |
|
1249 shows "poly (p - q) x = poly p x - poly q x" |
|
1250 by (simp add: diff_minus) |
|
1251 |
|
1252 lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)" |
|
1253 by (cases "finite A", induct set: finite, simp_all) |
|
1254 |
|
1255 lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x" |
|
1256 by (induct p, simp, simp add: algebra_simps) |
|
1257 |
|
1258 lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x" |
|
1259 by (induct p, simp_all, simp add: algebra_simps) |
|
1260 |
|
1261 lemma poly_power [simp]: |
|
1262 fixes p :: "'a::{comm_semiring_1} poly" |
|
1263 shows "poly (p ^ n) x = poly p x ^ n" |
|
1264 by (induct n, simp, simp add: power_Suc) |
|
1265 |
|
1266 |
|
1267 subsection {* Synthetic division *} |
|
1268 |
|
1269 text {* |
|
1270 Synthetic division is simply division by the |
|
1271 linear polynomial @{term "x - c"}. |
|
1272 *} |
|
1273 |
|
1274 definition |
|
1275 synthetic_divmod :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly \<times> 'a" |
|
1276 where |
|
1277 "synthetic_divmod p c = |
|
1278 poly_rec (0, 0) (\<lambda>a p (q, r). (pCons r q, a + c * r)) p" |
|
1279 |
|
1280 definition |
|
1281 synthetic_div :: "'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a poly" |
|
1282 where |
|
1283 "synthetic_div p c = fst (synthetic_divmod p c)" |
|
1284 |
|
1285 lemma synthetic_divmod_0 [simp]: |
|
1286 "synthetic_divmod 0 c = (0, 0)" |
|
1287 unfolding synthetic_divmod_def |
|
1288 by (simp add: poly_rec_0) |
|
1289 |
|
1290 lemma synthetic_divmod_pCons [simp]: |
|
1291 "synthetic_divmod (pCons a p) c = |
|
1292 (\<lambda>(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)" |
|
1293 unfolding synthetic_divmod_def |
|
1294 by (simp add: poly_rec_pCons) |
|
1295 |
|
1296 lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c" |
|
1297 by (induct p, simp, simp add: split_def) |
|
1298 |
|
1299 lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0" |
|
1300 unfolding synthetic_div_def by simp |
|
1301 |
|
1302 lemma synthetic_div_pCons [simp]: |
|
1303 "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)" |
|
1304 unfolding synthetic_div_def |
|
1305 by (simp add: split_def snd_synthetic_divmod) |
|
1306 |
|
1307 lemma synthetic_div_eq_0_iff: |
|
1308 "synthetic_div p c = 0 \<longleftrightarrow> degree p = 0" |
|
1309 by (induct p, simp, case_tac p, simp) |
|
1310 |
|
1311 lemma degree_synthetic_div: |
|
1312 "degree (synthetic_div p c) = degree p - 1" |
|
1313 by (induct p, simp, simp add: synthetic_div_eq_0_iff) |
|
1314 |
|
1315 lemma synthetic_div_correct: |
|
1316 "p + smult c (synthetic_div p c) = pCons (poly p c) (synthetic_div p c)" |
|
1317 by (induct p) simp_all |
|
1318 |
|
1319 lemma synthetic_div_unique_lemma: "smult c p = pCons a p \<Longrightarrow> p = 0" |
|
1320 by (induct p arbitrary: a) simp_all |
|
1321 |
|
1322 lemma synthetic_div_unique: |
|
1323 "p + smult c q = pCons r q \<Longrightarrow> r = poly p c \<and> q = synthetic_div p c" |
|
1324 apply (induct p arbitrary: q r) |
|
1325 apply (simp, frule synthetic_div_unique_lemma, simp) |
|
1326 apply (case_tac q, force) |
|
1327 done |
|
1328 |
|
1329 lemma synthetic_div_correct': |
|
1330 fixes c :: "'a::comm_ring_1" |
|
1331 shows "[:-c, 1:] * synthetic_div p c + [:poly p c:] = p" |
|
1332 using synthetic_div_correct [of p c] |
|
1333 by (simp add: algebra_simps) |
|
1334 |
|
1335 lemma poly_eq_0_iff_dvd: |
|
1336 fixes c :: "'a::idom" |
|
1337 shows "poly p c = 0 \<longleftrightarrow> [:-c, 1:] dvd p" |
|
1338 proof |
|
1339 assume "poly p c = 0" |
|
1340 with synthetic_div_correct' [of c p] |
|
1341 have "p = [:-c, 1:] * synthetic_div p c" by simp |
|
1342 then show "[:-c, 1:] dvd p" .. |
|
1343 next |
|
1344 assume "[:-c, 1:] dvd p" |
|
1345 then obtain k where "p = [:-c, 1:] * k" by (rule dvdE) |
|
1346 then show "poly p c = 0" by simp |
|
1347 qed |
|
1348 |
|
1349 lemma dvd_iff_poly_eq_0: |
|
1350 fixes c :: "'a::idom" |
|
1351 shows "[:c, 1:] dvd p \<longleftrightarrow> poly p (-c) = 0" |
|
1352 by (simp add: poly_eq_0_iff_dvd) |
|
1353 |
|
1354 lemma poly_roots_finite: |
|
1355 fixes p :: "'a::idom poly" |
|
1356 shows "p \<noteq> 0 \<Longrightarrow> finite {x. poly p x = 0}" |
|
1357 proof (induct n \<equiv> "degree p" arbitrary: p) |
|
1358 case (0 p) |
|
1359 then obtain a where "a \<noteq> 0" and "p = [:a:]" |
|
1360 by (cases p, simp split: if_splits) |
|
1361 then show "finite {x. poly p x = 0}" by simp |
|
1362 next |
|
1363 case (Suc n p) |
|
1364 show "finite {x. poly p x = 0}" |
|
1365 proof (cases "\<exists>x. poly p x = 0") |
|
1366 case False |
|
1367 then show "finite {x. poly p x = 0}" by simp |
|
1368 next |
|
1369 case True |
|
1370 then obtain a where "poly p a = 0" .. |
|
1371 then have "[:-a, 1:] dvd p" by (simp only: poly_eq_0_iff_dvd) |
|
1372 then obtain k where k: "p = [:-a, 1:] * k" .. |
|
1373 with `p \<noteq> 0` have "k \<noteq> 0" by auto |
|
1374 with k have "degree p = Suc (degree k)" |
|
1375 by (simp add: degree_mult_eq del: mult_pCons_left) |
|
1376 with `Suc n = degree p` have "n = degree k" by simp |
|
1377 then have "finite {x. poly k x = 0}" using `k \<noteq> 0` by (rule Suc.hyps) |
|
1378 then have "finite (insert a {x. poly k x = 0})" by simp |
|
1379 then show "finite {x. poly p x = 0}" |
|
1380 by (simp add: k uminus_add_conv_diff Collect_disj_eq |
|
1381 del: mult_pCons_left) |
|
1382 qed |
|
1383 qed |
|
1384 |
|
1385 lemma poly_zero: |
|
1386 fixes p :: "'a::{idom,ring_char_0} poly" |
|
1387 shows "poly p = poly 0 \<longleftrightarrow> p = 0" |
|
1388 apply (cases "p = 0", simp_all) |
|
1389 apply (drule poly_roots_finite) |
|
1390 apply (auto simp add: infinite_UNIV_char_0) |
|
1391 done |
|
1392 |
|
1393 lemma poly_eq_iff: |
|
1394 fixes p q :: "'a::{idom,ring_char_0} poly" |
|
1395 shows "poly p = poly q \<longleftrightarrow> p = q" |
|
1396 using poly_zero [of "p - q"] |
|
1397 by (simp add: fun_eq_iff) |
|
1398 |
|
1399 |
|
1400 subsection {* Composition of polynomials *} |
|
1401 |
|
1402 definition |
|
1403 pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
|
1404 where |
|
1405 "pcompose p q = poly_rec 0 (\<lambda>a _ c. [:a:] + q * c) p" |
|
1406 |
|
1407 lemma pcompose_0 [simp]: "pcompose 0 q = 0" |
|
1408 unfolding pcompose_def by (simp add: poly_rec_0) |
|
1409 |
|
1410 lemma pcompose_pCons: |
|
1411 "pcompose (pCons a p) q = [:a:] + q * pcompose p q" |
|
1412 unfolding pcompose_def by (simp add: poly_rec_pCons) |
|
1413 |
|
1414 lemma poly_pcompose: "poly (pcompose p q) x = poly p (poly q x)" |
|
1415 by (induct p) (simp_all add: pcompose_pCons) |
|
1416 |
|
1417 lemma degree_pcompose_le: |
|
1418 "degree (pcompose p q) \<le> degree p * degree q" |
|
1419 apply (induct p, simp) |
|
1420 apply (simp add: pcompose_pCons, clarify) |
|
1421 apply (rule degree_add_le, simp) |
|
1422 apply (rule order_trans [OF degree_mult_le], simp) |
|
1423 done |
|
1424 |
|
1425 |
1687 |
1426 subsection {* Order of polynomial roots *} |
1688 subsection {* Order of polynomial roots *} |
1427 |
1689 |
1428 definition |
1690 definition order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat" |
1429 order :: "'a::idom \<Rightarrow> 'a poly \<Rightarrow> nat" |
|
1430 where |
1691 where |
1431 "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)" |
1692 "order a p = (LEAST n. \<not> [:-a, 1:] ^ Suc n dvd p)" |
1432 |
1693 |
1433 lemma coeff_linear_power: |
1694 lemma coeff_linear_power: |
1434 fixes a :: "'a::comm_semiring_1" |
1695 fixes a :: "'a::comm_semiring_1" |
1488 apply (simp only: order_def) |
1749 apply (simp only: order_def) |
1489 apply (drule not_less_Least, simp) |
1750 apply (drule not_less_Least, simp) |
1490 done |
1751 done |
1491 |
1752 |
1492 |
1753 |
1493 subsection {* Configuration of the code generator *} |
1754 subsection {* GCD of polynomials *} |
1494 |
1755 |
1495 code_datatype "0::'a::zero poly" pCons |
1756 instantiation poly :: (field) gcd |
1496 |
|
1497 quickcheck_generator poly constructors: "0::'a::zero poly", pCons |
|
1498 |
|
1499 instantiation poly :: ("{zero, equal}") equal |
|
1500 begin |
1757 begin |
1501 |
1758 |
1502 definition |
1759 function gcd_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
1503 "HOL.equal (p::'a poly) q \<longleftrightarrow> p = q" |
1760 where |
1504 |
1761 "gcd (x::'a poly) 0 = smult (inverse (coeff x (degree x))) x" |
1505 instance proof |
1762 | "y \<noteq> 0 \<Longrightarrow> gcd (x::'a poly) y = gcd y (x mod y)" |
1506 qed (rule equal_poly_def) |
1763 by auto |
|
1764 |
|
1765 termination "gcd :: _ poly \<Rightarrow> _" |
|
1766 by (relation "measure (\<lambda>(x, y). if y = 0 then 0 else Suc (degree y))") |
|
1767 (auto dest: degree_mod_less) |
|
1768 |
|
1769 declare gcd_poly.simps [simp del] |
|
1770 |
|
1771 instance .. |
1507 |
1772 |
1508 end |
1773 end |
1509 |
1774 |
1510 lemma eq_poly_code [code]: |
1775 lemma |
1511 "HOL.equal (0::_ poly) (0::_ poly) \<longleftrightarrow> True" |
1776 fixes x y :: "_ poly" |
1512 "HOL.equal (0::_ poly) (pCons b q) \<longleftrightarrow> HOL.equal 0 b \<and> HOL.equal 0 q" |
1777 shows poly_gcd_dvd1 [iff]: "gcd x y dvd x" |
1513 "HOL.equal (pCons a p) (0::_ poly) \<longleftrightarrow> HOL.equal a 0 \<and> HOL.equal p 0" |
1778 and poly_gcd_dvd2 [iff]: "gcd x y dvd y" |
1514 "HOL.equal (pCons a p) (pCons b q) \<longleftrightarrow> HOL.equal a b \<and> HOL.equal p q" |
1779 apply (induct x y rule: gcd_poly.induct) |
1515 by (simp_all add: equal) |
1780 apply (simp_all add: gcd_poly.simps) |
1516 |
1781 apply (fastforce simp add: smult_dvd_iff dest: inverse_zero_imp_zero) |
1517 lemma [code nbe]: |
1782 apply (blast dest: dvd_mod_imp_dvd) |
1518 "HOL.equal (p :: _ poly) p \<longleftrightarrow> True" |
1783 done |
1519 by (fact equal_refl) |
1784 |
1520 |
1785 lemma poly_gcd_greatest: |
1521 lemmas coeff_code [code] = |
1786 fixes k x y :: "_ poly" |
1522 coeff_0 coeff_pCons_0 coeff_pCons_Suc |
1787 shows "k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd gcd x y" |
1523 |
1788 by (induct x y rule: gcd_poly.induct) |
1524 lemmas degree_code [code] = |
1789 (simp_all add: gcd_poly.simps dvd_mod dvd_smult) |
1525 degree_0 degree_pCons_eq_if |
1790 |
1526 |
1791 lemma dvd_poly_gcd_iff [iff]: |
1527 lemmas monom_poly_code [code] = |
1792 fixes k x y :: "_ poly" |
1528 monom_0 monom_Suc |
1793 shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y" |
1529 |
1794 by (blast intro!: poly_gcd_greatest intro: dvd_trans) |
1530 lemma add_poly_code [code]: |
1795 |
1531 "0 + q = (q :: _ poly)" |
1796 lemma poly_gcd_monic: |
1532 "p + 0 = (p :: _ poly)" |
1797 fixes x y :: "_ poly" |
1533 "pCons a p + pCons b q = pCons (a + b) (p + q)" |
1798 shows "coeff (gcd x y) (degree (gcd x y)) = |
1534 by simp_all |
1799 (if x = 0 \<and> y = 0 then 0 else 1)" |
1535 |
1800 by (induct x y rule: gcd_poly.induct) |
1536 lemma minus_poly_code [code]: |
1801 (simp_all add: gcd_poly.simps nonzero_imp_inverse_nonzero) |
1537 "- 0 = (0 :: _ poly)" |
1802 |
1538 "- pCons a p = pCons (- a) (- p)" |
1803 lemma poly_gcd_zero_iff [simp]: |
1539 by simp_all |
1804 fixes x y :: "_ poly" |
1540 |
1805 shows "gcd x y = 0 \<longleftrightarrow> x = 0 \<and> y = 0" |
1541 lemma diff_poly_code [code]: |
1806 by (simp only: dvd_0_left_iff [symmetric] dvd_poly_gcd_iff) |
1542 "0 - q = (- q :: _ poly)" |
1807 |
1543 "p - 0 = (p :: _ poly)" |
1808 lemma poly_gcd_0_0 [simp]: |
1544 "pCons a p - pCons b q = pCons (a - b) (p - q)" |
1809 "gcd (0::_ poly) 0 = 0" |
1545 by simp_all |
1810 by simp |
1546 |
1811 |
1547 lemmas smult_poly_code [code] = |
1812 lemma poly_dvd_antisym: |
1548 smult_0_right smult_pCons |
1813 fixes p q :: "'a::idom poly" |
1549 |
1814 assumes coeff: "coeff p (degree p) = coeff q (degree q)" |
1550 lemma mult_poly_code [code]: |
1815 assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q" |
1551 "0 * q = (0 :: _ poly)" |
1816 proof (cases "p = 0") |
1552 "pCons a p * q = smult a q + pCons 0 (p * q)" |
1817 case True with coeff show "p = q" by simp |
1553 by simp_all |
1818 next |
1554 |
1819 case False with coeff have "q \<noteq> 0" by auto |
1555 lemmas poly_code [code] = |
1820 have degree: "degree p = degree q" |
1556 poly_0 poly_pCons |
1821 using `p dvd q` `q dvd p` `p \<noteq> 0` `q \<noteq> 0` |
1557 |
1822 by (intro order_antisym dvd_imp_degree_le) |
1558 lemmas synthetic_divmod_code [code] = |
1823 |
1559 synthetic_divmod_0 synthetic_divmod_pCons |
1824 from `p dvd q` obtain a where a: "q = p * a" .. |
1560 |
1825 with `q \<noteq> 0` have "a \<noteq> 0" by auto |
1561 text {* code generator setup for div and mod *} |
1826 with degree a `p \<noteq> 0` have "degree a = 0" |
1562 |
1827 by (simp add: degree_mult_eq) |
1563 definition |
1828 with coeff a show "p = q" |
1564 pdivmod :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly" |
1829 by (cases a, auto split: if_splits) |
|
1830 qed |
|
1831 |
|
1832 lemma poly_gcd_unique: |
|
1833 fixes d x y :: "_ poly" |
|
1834 assumes dvd1: "d dvd x" and dvd2: "d dvd y" |
|
1835 and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d" |
|
1836 and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)" |
|
1837 shows "gcd x y = d" |
|
1838 proof - |
|
1839 have "coeff (gcd x y) (degree (gcd x y)) = coeff d (degree d)" |
|
1840 by (simp_all add: poly_gcd_monic monic) |
|
1841 moreover have "gcd x y dvd d" |
|
1842 using poly_gcd_dvd1 poly_gcd_dvd2 by (rule greatest) |
|
1843 moreover have "d dvd gcd x y" |
|
1844 using dvd1 dvd2 by (rule poly_gcd_greatest) |
|
1845 ultimately show ?thesis |
|
1846 by (rule poly_dvd_antisym) |
|
1847 qed |
|
1848 |
|
1849 interpretation gcd_poly!: abel_semigroup "gcd :: _ poly \<Rightarrow> _" |
|
1850 proof |
|
1851 fix x y z :: "'a poly" |
|
1852 show "gcd (gcd x y) z = gcd x (gcd y z)" |
|
1853 by (rule poly_gcd_unique) (auto intro: dvd_trans simp add: poly_gcd_monic) |
|
1854 show "gcd x y = gcd y x" |
|
1855 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1856 qed |
|
1857 |
|
1858 lemmas poly_gcd_assoc = gcd_poly.assoc |
|
1859 lemmas poly_gcd_commute = gcd_poly.commute |
|
1860 lemmas poly_gcd_left_commute = gcd_poly.left_commute |
|
1861 |
|
1862 lemmas poly_gcd_ac = poly_gcd_assoc poly_gcd_commute poly_gcd_left_commute |
|
1863 |
|
1864 lemma poly_gcd_1_left [simp]: "gcd 1 y = (1 :: _ poly)" |
|
1865 by (rule poly_gcd_unique) simp_all |
|
1866 |
|
1867 lemma poly_gcd_1_right [simp]: "gcd x 1 = (1 :: _ poly)" |
|
1868 by (rule poly_gcd_unique) simp_all |
|
1869 |
|
1870 lemma poly_gcd_minus_left [simp]: "gcd (- x) y = gcd x (y :: _ poly)" |
|
1871 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1872 |
|
1873 lemma poly_gcd_minus_right [simp]: "gcd x (- y) = gcd x (y :: _ poly)" |
|
1874 by (rule poly_gcd_unique) (simp_all add: poly_gcd_monic) |
|
1875 |
|
1876 lemma poly_gcd_code [code]: |
|
1877 "gcd x y = (if y = 0 then smult (inverse (coeff x (degree x))) x else gcd y (x mod (y :: _ poly)))" |
|
1878 by (simp add: gcd_poly.simps) |
|
1879 |
|
1880 |
|
1881 subsection {* Composition of polynomials *} |
|
1882 |
|
1883 definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" |
1565 where |
1884 where |
1566 "pdivmod x y = (x div y, x mod y)" |
1885 "pcompose p q = fold_coeffs (\<lambda>a c. [:a:] + q * c) p 0" |
1567 |
1886 |
1568 lemma div_poly_code [code]: "x div y = fst (pdivmod x y)" |
1887 lemma pcompose_0 [simp]: |
1569 unfolding pdivmod_def by simp |
1888 "pcompose 0 q = 0" |
1570 |
1889 by (simp add: pcompose_def) |
1571 lemma mod_poly_code [code]: "x mod y = snd (pdivmod x y)" |
1890 |
1572 unfolding pdivmod_def by simp |
1891 lemma pcompose_pCons: |
1573 |
1892 "pcompose (pCons a p) q = [:a:] + q * pcompose p q" |
1574 lemma pdivmod_0 [code]: "pdivmod 0 y = (0, 0)" |
1893 by (cases "p = 0 \<and> a = 0") (auto simp add: pcompose_def) |
1575 unfolding pdivmod_def by simp |
1894 |
1576 |
1895 lemma poly_pcompose: |
1577 lemma pdivmod_pCons [code]: |
1896 "poly (pcompose p q) x = poly p (poly q x)" |
1578 "pdivmod (pCons a x) y = |
1897 by (induct p) (simp_all add: pcompose_pCons) |
1579 (if y = 0 then (0, pCons a x) else |
1898 |
1580 (let (q, r) = pdivmod x y; |
1899 lemma degree_pcompose_le: |
1581 b = coeff (pCons a r) (degree y) / coeff y (degree y) |
1900 "degree (pcompose p q) \<le> degree p * degree q" |
1582 in (pCons b q, pCons a r - smult b y)))" |
1901 apply (induct p, simp) |
1583 apply (simp add: pdivmod_def Let_def, safe) |
1902 apply (simp add: pcompose_pCons, clarify) |
1584 apply (rule div_poly_eq) |
1903 apply (rule degree_add_le, simp) |
1585 apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) |
1904 apply (rule order_trans [OF degree_mult_le], simp) |
1586 apply (rule mod_poly_eq) |
|
1587 apply (erule pdivmod_rel_pCons [OF pdivmod_rel _ refl]) |
|
1588 done |
1905 done |
1589 |
1906 |
1590 lemma poly_gcd_code [code]: |
1907 |
1591 "poly_gcd x y = |
1908 no_notation cCons (infixr "##" 65) |
1592 (if y = 0 then smult (inverse (coeff x (degree x))) x |
|
1593 else poly_gcd y (x mod y))" |
|
1594 by (simp add: poly_gcd.simps) |
|
1595 |
1909 |
1596 end |
1910 end |
|
1911 |