23 by (simp add: expand_fps_eq) |
24 by (simp add: expand_fps_eq) |
24 |
25 |
25 lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n" |
26 lemma fps_nth_Abs_fps [simp]: "Abs_fps f $ n = f n" |
26 by (simp add: Abs_fps_inverse) |
27 by (simp add: Abs_fps_inverse) |
27 |
28 |
28 text\<open>Definition of the basic elements 0 and 1 and the basic operations of addition, |
29 text \<open>Definition of the basic elements 0 and 1 and the basic operations of addition, |
29 negation and multiplication\<close> |
30 negation and multiplication.\<close> |
30 |
31 |
31 instantiation fps :: (zero) zero |
32 instantiation fps :: (zero) zero |
32 begin |
33 begin |
33 |
34 definition fps_zero_def: "0 = Abs_fps (\<lambda>n. 0)" |
34 definition fps_zero_def: |
35 instance .. |
35 "0 = Abs_fps (\<lambda>n. 0)" |
|
36 |
|
37 instance .. |
|
38 end |
36 end |
39 |
37 |
40 lemma fps_zero_nth [simp]: "0 $ n = 0" |
38 lemma fps_zero_nth [simp]: "0 $ n = 0" |
41 unfolding fps_zero_def by simp |
39 unfolding fps_zero_def by simp |
42 |
40 |
43 instantiation fps :: ("{one, zero}") one |
41 instantiation fps :: ("{one, zero}") one |
44 begin |
42 begin |
45 |
43 definition fps_one_def: "1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)" |
46 definition fps_one_def: |
44 instance .. |
47 "1 = Abs_fps (\<lambda>n. if n = 0 then 1 else 0)" |
|
48 |
|
49 instance .. |
|
50 end |
45 end |
51 |
46 |
52 lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)" |
47 lemma fps_one_nth [simp]: "1 $ n = (if n = 0 then 1 else 0)" |
53 unfolding fps_one_def by simp |
48 unfolding fps_one_def by simp |
54 |
49 |
55 instantiation fps :: (plus) plus |
50 instantiation fps :: (plus) plus |
56 begin |
51 begin |
57 |
52 definition fps_plus_def: "op + = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n + g $ n))" |
58 definition fps_plus_def: |
53 instance .. |
59 "op + = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n + g $ n))" |
|
60 |
|
61 instance .. |
|
62 end |
54 end |
63 |
55 |
64 lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n" |
56 lemma fps_add_nth [simp]: "(f + g) $ n = f $ n + g $ n" |
65 unfolding fps_plus_def by simp |
57 unfolding fps_plus_def by simp |
66 |
58 |
67 instantiation fps :: (minus) minus |
59 instantiation fps :: (minus) minus |
68 begin |
60 begin |
69 |
61 definition fps_minus_def: "op - = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n - g $ n))" |
70 definition fps_minus_def: |
62 instance .. |
71 "op - = (\<lambda>f g. Abs_fps (\<lambda>n. f $ n - g $ n))" |
|
72 |
|
73 instance .. |
|
74 end |
63 end |
75 |
64 |
76 lemma fps_sub_nth [simp]: "(f - g) $ n = f $ n - g $ n" |
65 lemma fps_sub_nth [simp]: "(f - g) $ n = f $ n - g $ n" |
77 unfolding fps_minus_def by simp |
66 unfolding fps_minus_def by simp |
78 |
67 |
79 instantiation fps :: (uminus) uminus |
68 instantiation fps :: (uminus) uminus |
80 begin |
69 begin |
81 |
70 definition fps_uminus_def: "uminus = (\<lambda>f. Abs_fps (\<lambda>n. - (f $ n)))" |
82 definition fps_uminus_def: |
71 instance .. |
83 "uminus = (\<lambda>f. Abs_fps (\<lambda>n. - (f $ n)))" |
|
84 |
|
85 instance .. |
|
86 end |
72 end |
87 |
73 |
88 lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)" |
74 lemma fps_neg_nth [simp]: "(- f) $ n = - (f $ n)" |
89 unfolding fps_uminus_def by simp |
75 unfolding fps_uminus_def by simp |
90 |
76 |
91 instantiation fps :: ("{comm_monoid_add, times}") times |
77 instantiation fps :: ("{comm_monoid_add, times}") times |
92 begin |
78 begin |
93 |
79 definition fps_times_def: "op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))" |
94 definition fps_times_def: |
80 instance .. |
95 "op * = (\<lambda>f g. Abs_fps (\<lambda>n. \<Sum>i=0..n. f $ i * g $ (n - i)))" |
|
96 |
|
97 instance .. |
|
98 end |
81 end |
99 |
82 |
100 lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n - i))" |
83 lemma fps_mult_nth: "(f * g) $ n = (\<Sum>i=0..n. f$i * g$(n - i))" |
101 unfolding fps_times_def by simp |
84 unfolding fps_times_def by simp |
102 |
85 |
191 qed |
175 qed |
192 |
176 |
193 instance fps :: (semiring_1) monoid_mult |
177 instance fps :: (semiring_1) monoid_mult |
194 proof |
178 proof |
195 fix a :: "'a fps" |
179 fix a :: "'a fps" |
196 show "1 * a = a" by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) |
180 show "1 * a = a" |
197 show "a * 1 = a" by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') |
181 by (simp add: fps_ext fps_mult_nth mult_delta_left setsum.delta) |
|
182 show "a * 1 = a" |
|
183 by (simp add: fps_ext fps_mult_nth mult_delta_right setsum.delta') |
198 qed |
184 qed |
199 |
185 |
200 instance fps :: (cancel_semigroup_add) cancel_semigroup_add |
186 instance fps :: (cancel_semigroup_add) cancel_semigroup_add |
201 proof |
187 proof |
202 fix a b c :: "'a fps" |
188 fix a b c :: "'a fps" |
203 { assume "a + b = a + c" then show "b = c" by (simp add: expand_fps_eq) } |
189 show "b = c" if "a + b = a + c" |
204 { assume "b + a = c + a" then show "b = c" by (simp add: expand_fps_eq) } |
190 using that by (simp add: expand_fps_eq) |
|
191 show "b = c" if "b + a = c + a" |
|
192 using that by (simp add: expand_fps_eq) |
205 qed |
193 qed |
206 |
194 |
207 instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add |
195 instance fps :: (cancel_ab_semigroup_add) cancel_ab_semigroup_add |
208 proof |
196 proof |
209 fix a b c :: "'a fps" |
197 fix a b c :: "'a fps" |
210 show "a + b - a = b" by (simp add: expand_fps_eq) |
198 show "a + b - a = b" |
211 show "a - b - c = a - (b + c)" by (simp add: expand_fps_eq diff_diff_eq) |
199 by (simp add: expand_fps_eq) |
|
200 show "a - b - c = a - (b + c)" |
|
201 by (simp add: expand_fps_eq diff_diff_eq) |
212 qed |
202 qed |
213 |
203 |
214 instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. |
204 instance fps :: (cancel_comm_monoid_add) cancel_comm_monoid_add .. |
215 |
205 |
216 instance fps :: (group_add) group_add |
206 instance fps :: (group_add) group_add |
240 qed |
230 qed |
241 |
231 |
242 instance fps :: (semiring_0) semiring_0 |
232 instance fps :: (semiring_0) semiring_0 |
243 proof |
233 proof |
244 fix a :: "'a fps" |
234 fix a :: "'a fps" |
245 show "0 * a = 0" by (simp add: fps_ext fps_mult_nth) |
235 show "0 * a = 0" |
246 show "a * 0 = 0" by (simp add: fps_ext fps_mult_nth) |
236 by (simp add: fps_ext fps_mult_nth) |
|
237 show "a * 0 = 0" |
|
238 by (simp add: fps_ext fps_mult_nth) |
247 qed |
239 qed |
248 |
240 |
249 instance fps :: (semiring_0_cancel) semiring_0_cancel .. |
241 instance fps :: (semiring_0_cancel) semiring_0_cancel .. |
|
242 |
250 |
243 |
251 subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close> |
244 subsection \<open>Selection of the nth power of the implicit variable in the infinite sum\<close> |
252 |
245 |
253 lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)" |
246 lemma fps_nonzero_nth: "f \<noteq> 0 \<longleftrightarrow> (\<exists> n. f $n \<noteq> 0)" |
254 by (simp add: expand_fps_eq) |
247 by (simp add: expand_fps_eq) |
255 |
248 |
256 lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m < n. f $ m = 0))" |
249 lemma fps_nonzero_nth_minimal: "f \<noteq> 0 \<longleftrightarrow> (\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m < n. f $ m = 0))" |
|
250 (is "?lhs \<longleftrightarrow> ?rhs") |
257 proof |
251 proof |
258 let ?n = "LEAST n. f $ n \<noteq> 0" |
252 let ?n = "LEAST n. f $ n \<noteq> 0" |
259 assume "f \<noteq> 0" |
253 show ?rhs if ?lhs |
260 then have "\<exists>n. f $ n \<noteq> 0" |
254 proof - |
261 by (simp add: fps_nonzero_nth) |
255 from that have "\<exists>n. f $ n \<noteq> 0" |
262 then have "f $ ?n \<noteq> 0" |
256 by (simp add: fps_nonzero_nth) |
263 by (rule LeastI_ex) |
257 then have "f $ ?n \<noteq> 0" |
264 moreover have "\<forall>m<?n. f $ m = 0" |
258 by (rule LeastI_ex) |
265 by (auto dest: not_less_Least) |
259 moreover have "\<forall>m<?n. f $ m = 0" |
266 ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" .. |
260 by (auto dest: not_less_Least) |
267 then show "\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m<n. f $ m = 0)" .. |
261 ultimately have "f $ ?n \<noteq> 0 \<and> (\<forall>m<?n. f $ m = 0)" .. |
268 next |
262 then show ?thesis .. |
269 assume "\<exists>n. f $ n \<noteq> 0 \<and> (\<forall>m<n. f $ m = 0)" |
263 qed |
270 then show "f \<noteq> 0" by (auto simp add: expand_fps_eq) |
264 show ?lhs if ?rhs |
|
265 using that by (auto simp add: expand_fps_eq) |
271 qed |
266 qed |
272 |
267 |
273 lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $ n = g $n)" |
268 lemma fps_eq_iff: "f = g \<longleftrightarrow> (\<forall>n. f $ n = g $n)" |
274 by (rule expand_fps_eq) |
269 by (rule expand_fps_eq) |
275 |
270 |
340 by (intro_classes, auto simp add: distrib_right) |
337 by (intro_classes, auto simp add: distrib_right) |
341 |
338 |
342 instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors |
339 instance fps :: (ring_no_zero_divisors) ring_no_zero_divisors |
343 proof |
340 proof |
344 fix a b :: "'a fps" |
341 fix a b :: "'a fps" |
345 assume a0: "a \<noteq> 0" and b0: "b \<noteq> 0" |
342 assume "a \<noteq> 0" and "b \<noteq> 0" |
346 then obtain i j where i: "a$i\<noteq>0" "\<forall>k<i. a$k=0" and j: "b$j \<noteq>0" "\<forall>k<j. b$k =0" |
343 then obtain i j where i: "a $ i \<noteq> 0" "\<forall>k<i. a $ k = 0" and j: "b $ j \<noteq> 0" "\<forall>k<j. b $ k =0" |
347 unfolding fps_nonzero_nth_minimal |
344 unfolding fps_nonzero_nth_minimal |
348 by blast+ |
345 by blast+ |
349 have "(a * b) $ (i+j) = (\<Sum>k=0..i+j. a$k * b$(i+j-k))" |
346 have "(a * b) $ (i + j) = (\<Sum>k=0..i+j. a $ k * b $ (i + j - k))" |
350 by (rule fps_mult_nth) |
347 by (rule fps_mult_nth) |
351 also have "\<dots> = (a$i * b$(i+j-i)) + (\<Sum>k\<in>{0..i+j}-{i}. a$k * b$(i+j-k))" |
348 also have "\<dots> = (a $ i * b $ (i + j - i)) + (\<Sum>k\<in>{0..i+j} - {i}. a $ k * b $ (i + j - k))" |
352 by (rule setsum.remove) simp_all |
349 by (rule setsum.remove) simp_all |
353 also have "(\<Sum>k\<in>{0..i+j}-{i}. a$k * b$(i+j-k)) = 0" |
350 also have "(\<Sum>k\<in>{0..i+j}-{i}. a $ k * b $ (i + j - k)) = 0" |
354 proof (rule setsum.neutral [rule_format]) |
351 proof (rule setsum.neutral [rule_format]) |
355 fix k assume "k \<in> {0..i+j} - {i}" |
352 fix k assume "k \<in> {0..i+j} - {i}" |
356 then have "k < i \<or> i+j-k < j" by auto |
353 then have "k < i \<or> i+j-k < j" |
357 then show "a$k * b$(i+j-k) = 0" using i j by auto |
354 by auto |
358 qed |
355 then show "a $ k * b $ (i + j - k) = 0" |
359 also have "a$i * b$(i+j-i) + 0 = a$i * b$j" by simp |
356 using i j by auto |
360 also have "a$i * b$j \<noteq> 0" using i j by simp |
357 qed |
|
358 also have "a $ i * b $ (i + j - i) + 0 = a $ i * b $ j" |
|
359 by simp |
|
360 also have "a $ i * b $ j \<noteq> 0" |
|
361 using i j by simp |
361 finally have "(a*b) $ (i+j) \<noteq> 0" . |
362 finally have "(a*b) $ (i+j) \<noteq> 0" . |
362 then show "a*b \<noteq> 0" unfolding fps_nonzero_nth by blast |
363 then show "a * b \<noteq> 0" |
|
364 unfolding fps_nonzero_nth by blast |
363 qed |
365 qed |
364 |
366 |
365 instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. |
367 instance fps :: (ring_1_no_zero_divisors) ring_1_no_zero_divisors .. |
366 |
368 |
367 instance fps :: (idom) idom .. |
369 instance fps :: (idom) idom .. |
458 |
463 |
459 definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" |
464 definition open_fps_def: "open (S :: 'a fps set) = (\<forall>a \<in> S. \<exists>r. r >0 \<and> ball a r \<subseteq> S)" |
460 |
465 |
461 instance |
466 instance |
462 proof |
467 proof |
463 fix S :: "'a fps set" |
468 show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" for S :: "'a fps set" |
464 show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)" |
|
465 by (auto simp add: open_fps_def ball_def subset_eq) |
469 by (auto simp add: open_fps_def ball_def subset_eq) |
466 next |
470 show th: "dist a b = 0 \<longleftrightarrow> a = b" for a b :: "'a fps" |
467 { |
471 proof |
468 fix a b :: "'a fps" |
472 assume "a = b" |
469 { |
473 then have "\<not> (\<exists>n. a $ n \<noteq> b $ n)" by simp |
470 assume "a = b" |
474 then show "dist a b = 0" by (simp add: dist_fps_def) |
471 then have "\<not> (\<exists>n. a $ n \<noteq> b $ n)" by simp |
475 next |
472 then have "dist a b = 0" by (simp add: dist_fps_def) |
476 assume d: "dist a b = 0" |
473 } |
477 then have "\<forall>n. a$n = b$n" |
474 moreover |
478 by - (rule ccontr, simp add: dist_fps_def) |
475 { |
479 then show "a = b" by (simp add: fps_eq_iff) |
476 assume d: "dist a b = 0" |
480 qed |
477 then have "\<forall>n. a$n = b$n" |
481 then have th'[simp]: "dist a a = 0" for a :: "'a fps" |
478 by - (rule ccontr, simp add: dist_fps_def) |
482 by simp |
479 then have "a = b" by (simp add: fps_eq_iff) |
483 |
480 } |
|
481 ultimately show "dist a b =0 \<longleftrightarrow> a = b" by blast |
|
482 } |
|
483 note th = this |
|
484 from th have th'[simp]: "\<And>a::'a fps. dist a a = 0" by simp |
|
485 fix a b c :: "'a fps" |
484 fix a b c :: "'a fps" |
486 { |
485 consider "a = b" | "c = a \<or> c = b" | "a \<noteq> b" "a \<noteq> c" "b \<noteq> c" by blast |
487 assume "a = b" |
486 then show "dist a b \<le> dist a c + dist b c" |
|
487 proof cases |
|
488 case 1 |
488 then have "dist a b = 0" unfolding th . |
489 then have "dist a b = 0" unfolding th . |
489 then have "dist a b \<le> dist a c + dist b c" |
490 then show ?thesis |
490 using dist_fps_ge0 [of a c] dist_fps_ge0 [of b c] by simp |
491 using dist_fps_ge0 [of a c] dist_fps_ge0 [of b c] by simp |
491 } |
492 next |
492 moreover |
493 case 2 |
493 { |
494 then show ?thesis |
494 assume "c = a \<or> c = b" |
|
495 then have "dist a b \<le> dist a c + dist b c" |
|
496 by (cases "c = a") (simp_all add: th dist_fps_sym) |
495 by (cases "c = a") (simp_all add: th dist_fps_sym) |
497 } |
496 next |
498 moreover |
497 case 3 |
499 { |
|
500 assume ab: "a \<noteq> b" and ac: "a \<noteq> c" and bc: "b \<noteq> c" |
|
501 def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n" |
498 def n \<equiv> "\<lambda>a b::'a fps. LEAST n. a$n \<noteq> b$n" |
502 then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m" |
499 then have n': "\<And>m a b. m < n a b \<Longrightarrow> a$m = b$m" |
503 by (auto dest: not_less_Least) |
500 by (auto dest: not_less_Least) |
504 |
501 from 3 have dab: "dist a b = inverse (2 ^ n a b)" |
505 from ab ac bc |
|
506 have dab: "dist a b = inverse (2 ^ n a b)" |
|
507 and dac: "dist a c = inverse (2 ^ n a c)" |
502 and dac: "dist a c = inverse (2 ^ n a c)" |
508 and dbc: "dist b c = inverse (2 ^ n b c)" |
503 and dbc: "dist b c = inverse (2 ^ n b c)" |
509 by (simp_all add: dist_fps_def n_def fps_eq_iff) |
504 by (simp_all add: dist_fps_def n_def fps_eq_iff) |
510 from ab ac bc have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0" |
505 from 3 have nz: "dist a b \<noteq> 0" "dist a c \<noteq> 0" "dist b c \<noteq> 0" |
511 unfolding th by simp_all |
506 unfolding th by simp_all |
512 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" |
507 from nz have pos: "dist a b > 0" "dist a c > 0" "dist b c > 0" |
513 using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] |
508 using dist_fps_ge0[of a b] dist_fps_ge0[of a c] dist_fps_ge0[of b c] |
514 by auto |
509 by auto |
515 have th1: "\<And>n. (2::real)^n >0" by auto |
510 have th1: "\<And>n. (2::real)^n > 0" by auto |
516 { |
511 { |
517 assume h: "dist a b > dist a c + dist b c" |
512 assume h: "dist a b > dist a c + dist b c" |
518 then have gt: "dist a b > dist a c" "dist a b > dist b c" |
513 then have gt: "dist a b > dist a c" "dist a b > dist b c" |
519 using pos by auto |
514 using pos by auto |
520 from gt have gtn: "n a b < n b c" "n a b < n a c" |
515 from gt have gtn: "n a b < n b c" "n a b < n a c" |
521 unfolding dab dbc dac by (auto simp add: th1) |
516 unfolding dab dbc dac by (auto simp add: th1) |
522 from n'[OF gtn(2)] n'(1)[OF gtn(1)] |
517 from n'[OF gtn(2)] n'(1)[OF gtn(1)] |
523 have "a $ n a b = b $ n a b" by simp |
518 have "a $ n a b = b $ n a b" by simp |
524 moreover have "a $ n a b \<noteq> b $ n a b" |
519 moreover have "a $ n a b \<noteq> b $ n a b" |
525 unfolding n_def by (rule LeastI_ex) (insert ab, simp add: fps_eq_iff) |
520 unfolding n_def by (rule LeastI_ex) (insert \<open>a \<noteq> b\<close>, simp add: fps_eq_iff) |
526 ultimately have False by contradiction |
521 ultimately have False by contradiction |
527 } |
522 } |
528 then have "dist a b \<le> dist a c + dist b c" |
523 then show ?thesis |
529 by (auto simp add: not_le[symmetric]) |
524 by (auto simp add: not_le[symmetric]) |
530 } |
525 qed |
531 ultimately show "dist a b \<le> dist a c + dist b c" by blast |
|
532 qed |
526 qed |
533 |
527 |
534 end |
528 end |
535 |
529 |
536 text\<open>The infinite sums and justification of the notation in textbooks\<close> |
530 text \<open>The infinite sums and justification of the notation in textbooks\<close> |
537 |
531 |
538 lemma reals_power_lt_ex: |
532 lemma reals_power_lt_ex: |
539 fixes x y :: real |
533 fixes x y :: real |
540 assumes xp: "x > 0" |
534 assumes xp: "x > 0" |
541 and y1: "y > 1" |
535 and y1: "y > 1" |
582 lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) ----> a" |
576 lemma fps_notation: "(\<lambda>n. setsum (\<lambda>i. fps_const(a$i) * X^i) {0..n}) ----> a" |
583 (is "?s ----> a") |
577 (is "?s ----> a") |
584 proof - |
578 proof - |
585 { |
579 { |
586 fix r :: real |
580 fix r :: real |
587 assume rp: "r > 0" |
581 assume "r > 0" |
588 have th0: "(2::real) > 1" by simp |
582 obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" |
589 from reals_power_lt_ex[OF rp th0] |
583 using reals_power_lt_ex[OF \<open>r > 0\<close>, of 2] by auto |
590 obtain n0 where n0: "(1/2)^n0 < r" "n0 > 0" by blast |
584 have "\<exists>n0. \<forall>n \<ge> n0. dist (?s n) a < r" |
591 { |
585 proof - |
592 fix n :: nat |
|
593 assume nn0: "n \<ge> n0" |
|
594 then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0" |
|
595 by (simp add: divide_simps) |
|
596 { |
586 { |
597 assume "?s n = a" |
587 fix n :: nat |
598 then have "dist (?s n) a < r" |
588 assume nn0: "n \<ge> n0" |
599 unfolding dist_eq_0_iff[of "?s n" a, symmetric] |
589 then have thnn0: "(1/2)^n \<le> (1/2 :: real)^n0" |
600 using rp by (simp del: dist_eq_0_iff) |
590 by (simp add: divide_simps) |
|
591 have "dist (?s n) a < r" |
|
592 proof (cases "?s n = a") |
|
593 case True |
|
594 then show ?thesis |
|
595 unfolding dist_eq_0_iff[of "?s n" a, symmetric] |
|
596 using \<open>r > 0\<close> by (simp del: dist_eq_0_iff) |
|
597 next |
|
598 case False |
|
599 def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i" |
|
600 from False have dth: "dist (?s n) a = (1/2)^k" |
|
601 by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) |
|
602 from False have kn: "k > n" |
|
603 by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff |
|
604 split: split_if_asm intro: LeastI2_ex) |
|
605 then have "dist (?s n) a < (1/2)^n" |
|
606 unfolding dth by (simp add: divide_simps) |
|
607 also have "\<dots> \<le> (1/2)^n0" |
|
608 using nn0 by (simp add: divide_simps) |
|
609 also have "\<dots> < r" |
|
610 using n0 by simp |
|
611 finally show ?thesis . |
|
612 qed |
601 } |
613 } |
602 moreover |
614 then show ?thesis by blast |
603 { |
615 qed |
604 assume neq: "?s n \<noteq> a" |
|
605 def k \<equiv> "LEAST i. ?s n $ i \<noteq> a $ i" |
|
606 from neq have dth: "dist (?s n) a = (1/2)^k" |
|
607 by (auto simp add: dist_fps_def inverse_eq_divide power_divide k_def fps_eq_iff) |
|
608 |
|
609 from neq have kn: "k > n" |
|
610 by (auto simp: fps_sum_rep_nth not_le k_def fps_eq_iff |
|
611 split: split_if_asm intro: LeastI2_ex) |
|
612 then have "dist (?s n) a < (1/2)^n" |
|
613 unfolding dth by (simp add: divide_simps) |
|
614 also have "\<dots> \<le> (1/2)^n0" |
|
615 using nn0 by (simp add: divide_simps) |
|
616 also have "\<dots> < r" |
|
617 using n0 by simp |
|
618 finally have "dist (?s n) a < r" . |
|
619 } |
|
620 ultimately have "dist (?s n) a < r" |
|
621 by blast |
|
622 } |
|
623 then have "\<exists>n0. \<forall> n \<ge> n0. dist (?s n) a < r" |
|
624 by blast |
|
625 } |
616 } |
626 then show ?thesis |
617 then show ?thesis |
627 unfolding lim_sequentially by blast |
618 unfolding lim_sequentially by blast |
628 qed |
619 qed |
629 |
620 |
630 |
621 |
631 subsection\<open>Inverses of formal power series\<close> |
622 subsection \<open>Inverses of formal power series\<close> |
632 |
623 |
633 declare setsum.cong[fundef_cong] |
624 declare setsum.cong[fundef_cong] |
634 |
625 |
635 instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse |
626 instantiation fps :: ("{comm_monoid_add, inverse, times, uminus}") inverse |
636 begin |
627 begin |
687 unfolding fps_mult_nth ifn .. |
675 unfolding fps_mult_nth ifn .. |
688 also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))" |
676 also have "\<dots> = f$0 * natfun_inverse f n + (\<Sum>i = 1..n. f$i * natfun_inverse f (n-i))" |
689 by (simp add: eq) |
677 by (simp add: eq) |
690 also have "\<dots> = 0" |
678 also have "\<dots> = 0" |
691 unfolding th1 ifn by simp |
679 unfolding th1 ifn by simp |
692 finally have "(inverse f * f)$n = 0" |
680 finally show ?thesis unfolding c . |
693 unfolding c . |
681 qed |
694 } |
|
695 with th0 show ?thesis |
682 with th0 show ?thesis |
696 by (simp add: fps_eq_iff) |
683 by (simp add: fps_eq_iff) |
697 qed |
684 qed |
698 |
685 |
699 lemma fps_inverse_0_iff[simp]: "(inverse f)$0 = (0::'a::division_ring) \<longleftrightarrow> f$0 = 0" |
686 lemma fps_inverse_0_iff[simp]: "(inverse f) $ 0 = (0::'a::division_ring) \<longleftrightarrow> f $ 0 = 0" |
700 by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) |
687 by (simp add: fps_inverse_def nonzero_imp_inverse_nonzero) |
701 |
688 |
702 lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f $0 = 0" |
689 lemma fps_inverse_eq_0_iff[simp]: "inverse f = (0:: ('a::field) fps) \<longleftrightarrow> f $ 0 = 0" |
703 proof - |
690 (is "?lhs \<longleftrightarrow> ?rhs") |
704 { |
691 proof |
705 assume "f $ 0 = 0" |
692 show ?lhs if ?rhs |
706 then have "inverse f = 0" |
693 using that by (simp add: fps_inverse_def) |
707 by (simp add: fps_inverse_def) |
694 show ?rhs if h: ?lhs |
708 } |
695 proof (rule ccontr) |
709 moreover |
|
710 { |
|
711 assume h: "inverse f = 0" |
|
712 assume c: "f $0 \<noteq> 0" |
696 assume c: "f $0 \<noteq> 0" |
713 from inverse_mult_eq_1[OF c] h have False |
697 from inverse_mult_eq_1[OF c] h show False |
714 by simp |
698 by simp |
715 } |
699 qed |
716 ultimately show ?thesis by blast |
|
717 qed |
700 qed |
718 |
701 |
719 lemma fps_inverse_idempotent[intro]: |
702 lemma fps_inverse_idempotent[intro]: |
720 assumes f0: "f$0 \<noteq> (0::'a::field)" |
703 assumes f0: "f$0 \<noteq> (0::'a::field)" |
721 shows "inverse (inverse f) = f" |
704 shows "inverse (inverse f) = f" |
870 show ?thesis by (induct rule: finite_induct [OF True]) simp_all |
853 show ?thesis by (induct rule: finite_induct [OF True]) simp_all |
871 qed |
854 qed |
872 |
855 |
873 lemma fps_deriv_eq_0_iff [simp]: |
856 lemma fps_deriv_eq_0_iff [simp]: |
874 "fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})" |
857 "fps_deriv f = 0 \<longleftrightarrow> f = fps_const (f$0 :: 'a::{idom,semiring_char_0})" |
875 proof - |
858 (is "?lhs \<longleftrightarrow> ?rhs") |
876 { |
859 proof |
877 assume "f = fps_const (f$0)" |
860 show ?lhs if ?rhs |
878 then have "fps_deriv f = fps_deriv (fps_const (f$0))" by simp |
861 proof - |
879 then have "fps_deriv f = 0" by simp |
862 from that have "fps_deriv f = fps_deriv (fps_const (f$0))" |
880 } |
863 by simp |
881 moreover |
864 then show ?thesis |
882 { |
865 by simp |
883 assume z: "fps_deriv f = 0" |
866 qed |
884 then have "\<forall>n. (fps_deriv f)$n = 0" by simp |
867 show ?rhs if ?lhs |
885 then have "\<forall>n. f$(n+1) = 0" by (simp del: of_nat_Suc of_nat_add One_nat_def) |
868 proof - |
886 then have "f = fps_const (f$0)" |
869 from that have "\<forall>n. (fps_deriv f)$n = 0" |
|
870 by simp |
|
871 then have "\<forall>n. f$(n+1) = 0" |
|
872 by (simp del: of_nat_Suc of_nat_add One_nat_def) |
|
873 then show ?thesis |
887 apply (clarsimp simp add: fps_eq_iff fps_const_def) |
874 apply (clarsimp simp add: fps_eq_iff fps_const_def) |
888 apply (erule_tac x="n - 1" in allE) |
875 apply (erule_tac x="n - 1" in allE) |
889 apply simp |
876 apply simp |
890 done |
877 done |
891 } |
878 qed |
892 ultimately show ?thesis by blast |
|
893 qed |
879 qed |
894 |
880 |
895 lemma fps_deriv_eq_iff: |
881 lemma fps_deriv_eq_iff: |
896 fixes f :: "'a::{idom,semiring_char_0} fps" |
882 fixes f :: "'a::{idom,semiring_char_0} fps" |
897 shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)" |
883 shows "fps_deriv f = fps_deriv g \<longleftrightarrow> (f = fps_const(f$0 - g$0) + g)" |
898 proof - |
884 proof - |
899 have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0" |
885 have "fps_deriv f = fps_deriv g \<longleftrightarrow> fps_deriv (f - g) = 0" |
900 by simp |
886 by simp |
901 also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f - g) $ 0)" |
887 also have "\<dots> \<longleftrightarrow> f - g = fps_const ((f - g) $ 0)" |
902 unfolding fps_deriv_eq_0_iff .. |
888 unfolding fps_deriv_eq_0_iff .. |
903 finally show ?thesis by (simp add: field_simps) |
889 finally show ?thesis |
|
890 by (simp add: field_simps) |
904 qed |
891 qed |
905 |
892 |
906 lemma fps_deriv_eq_iff_ex: |
893 lemma fps_deriv_eq_iff_ex: |
907 "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)" |
894 "(fps_deriv f = fps_deriv g) \<longleftrightarrow> (\<exists>c::'a::{idom,semiring_char_0}. f = fps_const c + g)" |
908 by (auto simp: fps_deriv_eq_iff) |
895 by (auto simp: fps_deriv_eq_iff) |
998 apply (auto simp add: fps_mult_nth) |
984 apply (auto simp add: fps_mult_nth) |
999 apply (rule startsby_zero_power, simp_all) |
985 apply (rule startsby_zero_power, simp_all) |
1000 done |
986 done |
1001 |
987 |
1002 lemma startsby_zero_power_prefix: |
988 lemma startsby_zero_power_prefix: |
1003 assumes a0: "a $0 = (0::'a::idom)" |
989 assumes a0: "a $ 0 = (0::'a::idom)" |
1004 shows "\<forall>n < k. a ^ k $ n = 0" |
990 shows "\<forall>n < k. a ^ k $ n = 0" |
1005 using a0 |
991 using a0 |
1006 proof (induct k rule: nat_less_induct) |
992 proof (induct k rule: nat_less_induct) |
1007 fix k |
993 fix k |
1008 assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0" |
994 assume H: "\<forall>m<k. a $0 = 0 \<longrightarrow> (\<forall>n<m. a ^ m $ n = 0)" and a0: "a $ 0 = 0" |
1009 let ?ths = "\<forall>m<k. a ^ k $ m = 0" |
995 show "\<forall>m<k. a ^ k $ m = 0" |
1010 { |
996 proof (cases k) |
1011 assume "k = 0" |
997 case 0 |
1012 then have ?ths by simp |
998 then show ?thesis by simp |
1013 } |
999 next |
1014 moreover |
1000 case (Suc l) |
1015 { |
1001 have "a^k $ m = 0" if mk: "m < k" for m |
1016 fix l |
1002 proof (cases "m = 0") |
1017 assume k: "k = Suc l" |
1003 case True |
1018 { |
1004 then show ?thesis |
1019 fix m |
1005 using startsby_zero_power[of a k] Suc a0 by simp |
1020 assume mk: "m < k" |
1006 next |
1021 { |
1007 case False |
1022 assume "m = 0" |
1008 have "a ^k $ m = (a^l * a) $m" |
1023 then have "a^k $ m = 0" |
1009 by (simp add: Suc mult.commute) |
1024 using startsby_zero_power[of a k] k a0 by simp |
1010 also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))" |
1025 } |
1011 by (simp add: fps_mult_nth) |
1026 moreover |
1012 also have "\<dots> = 0" |
1027 { |
1013 apply (rule setsum.neutral) |
1028 assume m0: "m \<noteq> 0" |
1014 apply auto |
1029 have "a ^k $ m = (a^l * a) $m" |
1015 apply (case_tac "x = m") |
1030 by (simp add: k mult.commute) |
1016 using a0 apply simp |
1031 also have "\<dots> = (\<Sum>i = 0..m. a ^ l $ i * a $ (m - i))" |
1017 apply (rule H[rule_format]) |
1032 by (simp add: fps_mult_nth) |
1018 using a0 Suc mk apply auto |
1033 also have "\<dots> = 0" |
1019 done |
1034 apply (rule setsum.neutral) |
1020 finally show ?thesis . |
1035 apply auto |
1021 qed |
1036 apply (case_tac "x = m") |
1022 then show ?thesis by blast |
1037 using a0 apply simp |
1023 qed |
1038 apply (rule H[rule_format]) |
|
1039 using a0 k mk apply auto |
|
1040 done |
|
1041 finally have "a^k $ m = 0" . |
|
1042 } |
|
1043 ultimately have "a^k $ m = 0" |
|
1044 by blast |
|
1045 } |
|
1046 then have ?ths by blast |
|
1047 } |
|
1048 ultimately show ?ths |
|
1049 by (cases k) auto |
|
1050 qed |
1024 qed |
1051 |
1025 |
1052 lemma startsby_zero_setsum_depends: |
1026 lemma startsby_zero_setsum_depends: |
1053 assumes a0: "a $0 = (0::'a::idom)" |
1027 assumes a0: "a $0 = (0::'a::idom)" |
1054 and kn: "n \<ge> k" |
1028 and kn: "n \<ge> k" |
1087 qed |
1061 qed |
1088 |
1062 |
1089 lemma fps_inverse_power: |
1063 lemma fps_inverse_power: |
1090 fixes a :: "'a::field fps" |
1064 fixes a :: "'a::field fps" |
1091 shows "inverse (a^n) = inverse a ^ n" |
1065 shows "inverse (a^n) = inverse a ^ n" |
1092 proof - |
1066 proof (cases "a$0 = 0") |
1093 { |
1067 case True |
1094 assume a0: "a$0 = 0" |
1068 then have eq: "inverse a = 0" |
1095 then have eq: "inverse a = 0" |
1069 by (simp add: fps_inverse_def) |
|
1070 consider "n = 0" | "n > 0" by blast |
|
1071 then show ?thesis |
|
1072 proof cases |
|
1073 case 1 |
|
1074 then show ?thesis by simp |
|
1075 next |
|
1076 case 2 |
|
1077 from startsby_zero_power[OF True 2] eq show ?thesis |
1096 by (simp add: fps_inverse_def) |
1078 by (simp add: fps_inverse_def) |
1097 { |
1079 qed |
1098 assume "n = 0" |
1080 next |
1099 then have ?thesis by simp |
1081 case False |
1100 } |
1082 show ?thesis |
1101 moreover |
1083 apply (rule fps_inverse_unique) |
1102 { |
1084 apply (simp add: False) |
1103 assume n: "n > 0" |
1085 unfolding power_mult_distrib[symmetric] |
1104 from startsby_zero_power[OF a0 n] eq a0 n have ?thesis |
1086 apply (rule ssubst[where t = "a * inverse a" and s= 1]) |
1105 by (simp add: fps_inverse_def) |
1087 apply simp_all |
1106 } |
1088 apply (subst mult.commute) |
1107 ultimately have ?thesis by blast |
1089 apply (rule inverse_mult_eq_1[OF False]) |
1108 } |
1090 done |
1109 moreover |
|
1110 { |
|
1111 assume a0: "a$0 \<noteq> 0" |
|
1112 have ?thesis |
|
1113 apply (rule fps_inverse_unique) |
|
1114 apply (simp add: a0) |
|
1115 unfolding power_mult_distrib[symmetric] |
|
1116 apply (rule ssubst[where t = "a * inverse a" and s= 1]) |
|
1117 apply simp_all |
|
1118 apply (subst mult.commute) |
|
1119 apply (rule inverse_mult_eq_1[OF a0]) |
|
1120 done |
|
1121 } |
|
1122 ultimately show ?thesis by blast |
|
1123 qed |
1091 qed |
1124 |
1092 |
1125 lemma fps_deriv_power: |
1093 lemma fps_deriv_power: |
1126 "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)" |
1094 "fps_deriv (a ^ n) = fps_const (of_nat n :: 'a::comm_ring_1) * fps_deriv a * a ^ (n - 1)" |
1127 apply (induct n) |
1095 apply (induct n) |
1156 |
1124 |
1157 lemma fps_inverse_mult: |
1125 lemma fps_inverse_mult: |
1158 fixes a :: "'a::field fps" |
1126 fixes a :: "'a::field fps" |
1159 shows "inverse (a * b) = inverse a * inverse b" |
1127 shows "inverse (a * b) = inverse a * inverse b" |
1160 proof - |
1128 proof - |
1161 { |
1129 consider "a $ 0 = 0" | "b $ 0 = 0" | "a $ 0 \<noteq> 0" "b $ 0 \<noteq> 0" |
1162 assume a0: "a$0 = 0" |
1130 by blast |
1163 then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) |
1131 then show ?thesis |
1164 from a0 ab0 have th: "inverse a = 0" "inverse (a*b) = 0" by simp_all |
1132 proof cases |
1165 have ?thesis unfolding th by simp |
1133 case 1 |
1166 } |
1134 then have "(a * b) $ 0 = 0" |
1167 moreover |
1135 by (simp add: fps_mult_nth) |
1168 { |
1136 with 1 have th: "inverse a = 0" "inverse (a * b) = 0" |
1169 assume b0: "b$0 = 0" |
1137 by simp_all |
1170 then have ab0: "(a*b)$0 = 0" by (simp add: fps_mult_nth) |
1138 show ?thesis |
1171 from b0 ab0 have th: "inverse b = 0" "inverse (a*b) = 0" by simp_all |
1139 unfolding th by simp |
1172 have ?thesis unfolding th by simp |
1140 next |
1173 } |
1141 case 2 |
1174 moreover |
1142 then have "(a * b) $ 0 = 0" |
1175 { |
1143 by (simp add: fps_mult_nth) |
1176 assume a0: "a$0 \<noteq> 0" and b0: "b$0 \<noteq> 0" |
1144 with 2 have th: "inverse b = 0" "inverse (a * b) = 0" |
1177 from a0 b0 have ab0:"(a*b) $ 0 \<noteq> 0" by (simp add: fps_mult_nth) |
1145 by simp_all |
|
1146 show ?thesis |
|
1147 unfolding th by simp |
|
1148 next |
|
1149 case 3 |
|
1150 then have ab0:"(a * b) $ 0 \<noteq> 0" |
|
1151 by (simp add: fps_mult_nth) |
1178 from inverse_mult_eq_1[OF ab0] |
1152 from inverse_mult_eq_1[OF ab0] |
1179 have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" by simp |
1153 have "inverse (a*b) * (a*b) * inverse a * inverse b = 1 * inverse a * inverse b" |
|
1154 by simp |
1180 then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" |
1155 then have "inverse (a*b) * (inverse a * a) * (inverse b * b) = inverse a * inverse b" |
1181 by (simp add: field_simps) |
1156 by (simp add: field_simps) |
1182 then have ?thesis using inverse_mult_eq_1[OF a0] inverse_mult_eq_1[OF b0] by simp |
1157 then show ?thesis |
1183 } |
1158 using inverse_mult_eq_1[OF \<open>a $ 0 \<noteq> 0\<close>] inverse_mult_eq_1[OF \<open>b $ 0 \<noteq> 0\<close>] by simp |
1184 ultimately show ?thesis by blast |
1159 qed |
1185 qed |
1160 qed |
1186 |
1161 |
1187 lemma fps_inverse_deriv': |
1162 lemma fps_inverse_deriv': |
1188 fixes a :: "'a::field fps" |
1163 fixes a :: "'a::field fps" |
1189 assumes a0: "a$0 \<noteq> 0" |
1164 assumes a0: "a $ 0 \<noteq> 0" |
1190 shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2" |
1165 shows "fps_deriv (inverse a) = - fps_deriv a / a\<^sup>2" |
1191 using fps_inverse_deriv[OF a0] |
1166 using fps_inverse_deriv[OF a0] |
1192 unfolding power2_eq_square fps_divide_def fps_inverse_mult |
1167 unfolding power2_eq_square fps_divide_def fps_inverse_mult |
1193 by simp |
1168 by simp |
1194 |
1169 |
1280 lemma fps_power_mult_eq_shift: |
1253 lemma fps_power_mult_eq_shift: |
1281 "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = |
1254 "X^Suc k * Abs_fps (\<lambda>n. a (n + Suc k)) = |
1282 Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}" |
1255 Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a::comm_ring_1) * X^i) {0 .. k}" |
1283 (is "?lhs = ?rhs") |
1256 (is "?lhs = ?rhs") |
1284 proof - |
1257 proof - |
1285 { fix n :: nat |
1258 have "?lhs $ n = ?rhs $ n" for n :: nat |
|
1259 proof - |
1286 have "?lhs $ n = (if n < Suc k then 0 else a n)" |
1260 have "?lhs $ n = (if n < Suc k then 0 else a n)" |
1287 unfolding X_power_mult_nth by auto |
1261 unfolding X_power_mult_nth by auto |
1288 also have "\<dots> = ?rhs $ n" |
1262 also have "\<dots> = ?rhs $ n" |
1289 proof (induct k) |
1263 proof (induct k) |
1290 case 0 |
1264 case 0 |
1291 then show ?case by (simp add: fps_setsum_nth) |
1265 then show ?case |
|
1266 by (simp add: fps_setsum_nth) |
1292 next |
1267 next |
1293 case (Suc k) |
1268 case (Suc k) |
1294 note th = Suc.hyps[symmetric] |
|
1295 have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = |
1269 have "(Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. Suc k})$n = |
1296 (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - |
1270 (Abs_fps a - setsum (\<lambda>i. fps_const (a i :: 'a) * X^i) {0 .. k} - |
1297 fps_const (a (Suc k)) * X^ Suc k) $ n" |
1271 fps_const (a (Suc k)) * X^ Suc k) $ n" |
1298 by (simp add: field_simps) |
1272 by (simp add: field_simps) |
1299 also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n" |
1273 also have "\<dots> = (if n < Suc k then 0 else a n) - (fps_const (a (Suc k)) * X^ Suc k)$n" |
1300 using th unfolding fps_sub_nth by simp |
1274 using Suc.hyps[symmetric] unfolding fps_sub_nth by simp |
1301 also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)" |
1275 also have "\<dots> = (if n < Suc (Suc k) then 0 else a n)" |
1302 unfolding X_power_mult_right_nth |
1276 unfolding X_power_mult_right_nth |
1303 apply (auto simp add: not_less fps_const_def) |
1277 apply (auto simp add: not_less fps_const_def) |
1304 apply (rule cong[of a a, OF refl]) |
1278 apply (rule cong[of a a, OF refl]) |
1305 apply arith |
1279 apply arith |
1306 done |
1280 done |
1307 finally show ?case by simp |
1281 finally show ?case |
|
1282 by simp |
1308 qed |
1283 qed |
1309 finally have "?lhs $ n = ?rhs $ n" . |
1284 finally show ?thesis . |
1310 } |
1285 qed |
1311 then show ?thesis by (simp add: fps_eq_iff) |
1286 then show ?thesis |
|
1287 by (simp add: fps_eq_iff) |
1312 qed |
1288 qed |
1313 |
1289 |
1314 |
1290 |
1315 subsubsection \<open>Rule 2\<close> |
1291 subsubsection \<open>Rule 2\<close> |
1316 |
1292 |
1336 by (induct n) simp_all |
1312 by (induct n) simp_all |
1337 |
1313 |
1338 lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" |
1314 lemma fps_mult_X_deriv_shift: "X* fps_deriv a = Abs_fps (\<lambda>n. of_nat n* a$n)" |
1339 by (simp add: fps_eq_iff) |
1315 by (simp add: fps_eq_iff) |
1340 |
1316 |
1341 |
|
1342 lemma fps_mult_XD_shift: |
1317 lemma fps_mult_XD_shift: |
1343 "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)" |
1318 "(XD ^^ k) (a :: 'a::comm_ring_1 fps) = Abs_fps (\<lambda>n. (of_nat n ^ k) * a$n)" |
1344 by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def) |
1319 by (induct k arbitrary: a) (simp_all add: XD_def fps_eq_iff field_simps del: One_nat_def) |
1345 |
1320 |
1346 |
1321 |
1347 subsubsection \<open>Rule 3 is trivial and is given by @{text fps_times_def}\<close> |
1322 subsubsection \<open>Rule 3\<close> |
|
1323 |
|
1324 text \<open>Rule 3 is trivial and is given by @{text fps_times_def}.\<close> |
|
1325 |
1348 |
1326 |
1349 subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close> |
1327 subsubsection \<open>Rule 5 --- summation and "division" by (1 - X)\<close> |
1350 |
1328 |
1351 lemma fps_divide_X_minus1_setsum_lemma: |
1329 lemma fps_divide_X_minus1_setsum_lemma: |
1352 "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1330 "a = ((1::'a::comm_ring_1 fps) - X) * Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1353 proof - |
1331 proof - |
1354 let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1332 let ?sa = "Abs_fps (\<lambda>n. setsum (\<lambda>i. a $ i) {0..n})" |
1355 have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" |
1333 have th0: "\<And>i. (1 - (X::'a fps)) $ i = (if i = 0 then 1 else if i = 1 then - 1 else 0)" |
1356 by simp |
1334 by simp |
1357 { |
1335 have "a$n = ((1 - X) * ?sa) $ n" for n |
1358 fix n :: nat |
1336 proof (cases "n = 0") |
1359 { |
1337 case True |
1360 assume "n = 0" |
1338 then show ?thesis |
1361 then have "a $ n = ((1 - X) * ?sa) $ n" |
1339 by (simp add: fps_mult_nth) |
1362 by (simp add: fps_mult_nth) |
1340 next |
1363 } |
1341 case False |
1364 moreover |
1342 then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1} \<union> {2..n} = {1..n}" |
1365 { |
1343 "{0..n - 1} \<union> {n} = {0..n}" |
1366 assume n0: "n \<noteq> 0" |
1344 by (auto simp: set_eq_iff) |
1367 then have u: "{0} \<union> ({1} \<union> {2..n}) = {0..n}" "{1} \<union> {2..n} = {1..n}" |
1345 have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" "{0..n - 1} \<inter> {n} = {}" |
1368 "{0..n - 1} \<union> {n} = {0..n}" |
1346 using False by simp_all |
1369 by (auto simp: set_eq_iff) |
1347 have f: "finite {0}" "finite {1}" "finite {2 .. n}" |
1370 have d: "{0} \<inter> ({1} \<union> {2..n}) = {}" "{1} \<inter> {2..n} = {}" "{0..n - 1} \<inter> {n} = {}" |
1348 "finite {0 .. n - 1}" "finite {n}" by simp_all |
1371 using n0 by simp_all |
1349 have "((1 - X) * ?sa) $ n = setsum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}" |
1372 have f: "finite {0}" "finite {1}" "finite {2 .. n}" |
1350 by (simp add: fps_mult_nth) |
1373 "finite {0 .. n - 1}" "finite {n}" by simp_all |
1351 also have "\<dots> = a$n" |
1374 have "((1 - X) * ?sa) $ n = setsum (\<lambda>i. (1 - X)$ i * ?sa $ (n - i)) {0 .. n}" |
1352 unfolding th0 |
1375 by (simp add: fps_mult_nth) |
1353 unfolding setsum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] |
1376 also have "\<dots> = a$n" |
1354 unfolding setsum.union_disjoint[OF f(2) f(3) d(2)] |
1377 unfolding th0 |
1355 apply (simp) |
1378 unfolding setsum.union_disjoint[OF f(1) finite_UnI[OF f(2,3)] d(1), unfolded u(1)] |
1356 unfolding setsum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] |
1379 unfolding setsum.union_disjoint[OF f(2) f(3) d(2)] |
1357 apply simp |
1380 apply (simp) |
1358 done |
1381 unfolding setsum.union_disjoint[OF f(4,5) d(3), unfolded u(3)] |
1359 finally show ?thesis |
1382 apply simp |
1360 by simp |
1383 done |
1361 qed |
1384 finally have "a$n = ((1 - X) * ?sa) $ n" |
|
1385 by simp |
|
1386 } |
|
1387 ultimately have "a$n = ((1 - X) * ?sa) $ n" |
|
1388 by blast |
|
1389 } |
|
1390 then show ?thesis |
1362 then show ?thesis |
1391 unfolding fps_eq_iff by blast |
1363 unfolding fps_eq_iff by blast |
1392 qed |
1364 qed |
1393 |
1365 |
1394 lemma fps_divide_X_minus1_setsum: |
1366 lemma fps_divide_X_minus1_setsum: |
1670 assumes a0: "a$0 = (0::'a::idom)" |
1642 assumes a0: "a$0 = (0::'a::idom)" |
1671 and a1: "a$1 \<noteq> 0" |
1643 and a1: "a$1 \<noteq> 0" |
1672 shows "(b oo a = c oo a) \<longleftrightarrow> b = c" |
1644 shows "(b oo a = c oo a) \<longleftrightarrow> b = c" |
1673 (is "?lhs \<longleftrightarrow>?rhs") |
1645 (is "?lhs \<longleftrightarrow>?rhs") |
1674 proof |
1646 proof |
1675 assume ?rhs |
1647 show ?lhs if ?rhs using that by simp |
1676 then show "?lhs" by simp |
1648 show ?rhs if ?lhs |
1677 next |
1649 proof - |
1678 assume h: ?lhs |
1650 have "b$n = c$n" for n |
1679 { |
|
1680 fix n |
|
1681 have "b$n = c$n" |
|
1682 proof (induct n rule: nat_less_induct) |
1651 proof (induct n rule: nat_less_induct) |
1683 fix n |
1652 fix n |
1684 assume H: "\<forall>m<n. b$m = c$m" |
1653 assume H: "\<forall>m<n. b$m = c$m" |
1685 { |
1654 show "b$n = c$n" |
1686 assume n0: "n=0" |
1655 proof (cases n) |
1687 from h have "(b oo a)$n = (c oo a)$n" by simp |
1656 case 0 |
1688 then have "b$n = c$n" using n0 by (simp add: fps_compose_nth) |
1657 from \<open>?lhs\<close> have "(b oo a)$n = (c oo a)$n" |
1689 } |
1658 by simp |
1690 moreover |
1659 then show ?thesis |
1691 { |
1660 using 0 by (simp add: fps_compose_nth) |
1692 fix n1 assume n1: "n = Suc n1" |
1661 next |
|
1662 case (Suc n1) |
1693 have f: "finite {0 .. n1}" "finite {n}" by simp_all |
1663 have f: "finite {0 .. n1}" "finite {n}" by simp_all |
1694 have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using n1 by auto |
1664 have eq: "{0 .. n1} \<union> {n} = {0 .. n}" using Suc by auto |
1695 have d: "{0 .. n1} \<inter> {n} = {}" using n1 by auto |
1665 have d: "{0 .. n1} \<inter> {n} = {}" using Suc by auto |
1696 have seq: "(\<Sum>i = 0..n1. b $ i * a ^ i $ n) = (\<Sum>i = 0..n1. c $ i * a ^ i $ n)" |
1666 have seq: "(\<Sum>i = 0..n1. b $ i * a ^ i $ n) = (\<Sum>i = 0..n1. c $ i * a ^ i $ n)" |
1697 apply (rule setsum.cong) |
1667 apply (rule setsum.cong) |
1698 using H n1 |
1668 using H Suc |
1699 apply auto |
1669 apply auto |
1700 done |
1670 done |
1701 have th0: "(b oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" |
1671 have th0: "(b oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + b$n * (a$1)^n" |
1702 unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] seq |
1672 unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] seq |
1703 using startsby_zero_power_nth_same[OF a0] |
1673 using startsby_zero_power_nth_same[OF a0] |
1704 by simp |
1674 by simp |
1705 have th1: "(c oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + c$n * (a$1)^n" |
1675 have th1: "(c oo a) $n = (\<Sum>i = 0..n1. c $ i * a ^ i $ n) + c$n * (a$1)^n" |
1706 unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] |
1676 unfolding fps_compose_nth setsum.union_disjoint[OF f d, unfolded eq] |
1707 using startsby_zero_power_nth_same[OF a0] |
1677 using startsby_zero_power_nth_same[OF a0] |
1708 by simp |
1678 by simp |
1709 from h[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 |
1679 from \<open>?lhs\<close>[unfolded fps_eq_iff, rule_format, of n] th0 th1 a1 |
1710 have "b$n = c$n" by auto |
1680 show ?thesis by auto |
1711 } |
1681 qed |
1712 ultimately show "b$n = c$n" by (cases n) auto |
1682 qed |
1713 qed} |
1683 then show ?rhs by (simp add: fps_eq_iff) |
1714 then show ?rhs by (simp add: fps_eq_iff) |
1684 qed |
1715 qed |
1685 qed |
1716 |
1686 |
1717 |
1687 |
1718 subsection \<open>Radicals\<close> |
1688 subsection \<open>Radicals\<close> |
1719 |
1689 |
1795 apply simp |
1765 apply simp |
1796 using Suc |
1766 using Suc |
1797 apply (subgoal_tac "replicate k 0 ! x = 0") |
1767 apply (subgoal_tac "replicate k 0 ! x = 0") |
1798 apply (auto intro: nth_replicate simp del: replicate.simps) |
1768 apply (auto intro: nth_replicate simp del: replicate.simps) |
1799 done |
1769 done |
1800 also have "\<dots> = a$0" using r Suc by (simp add: setprod_constant) |
1770 also have "\<dots> = a$0" |
1801 finally show ?thesis using Suc by simp |
1771 using r Suc by (simp add: setprod_constant) |
|
1772 finally show ?thesis |
|
1773 using Suc by simp |
1802 qed |
1774 qed |
1803 |
1775 |
1804 lemma natpermute_max_card: |
1776 lemma natpermute_max_card: |
1805 assumes n0: "n \<noteq> 0" |
1777 assumes n0: "n \<noteq> 0" |
1806 shows "card {xs \<in> natpermute n (k+1). n \<in> set xs} = k + 1" |
1778 shows "card {xs \<in> natpermute n (k+1). n \<in> set xs} = k + 1" |
1807 unfolding natpermute_contain_maximal |
1779 unfolding natpermute_contain_maximal |
1808 proof - |
1780 proof - |
1809 let ?A= "\<lambda>i. {replicate (k + 1) 0[i := n]}" |
1781 let ?A = "\<lambda>i. {replicate (k + 1) 0[i := n]}" |
1810 let ?K = "{0 ..k}" |
1782 let ?K = "{0 ..k}" |
1811 have fK: "finite ?K" by simp |
1783 have fK: "finite ?K" |
1812 have fAK: "\<forall>i\<in>?K. finite (?A i)" by auto |
1784 by simp |
|
1785 have fAK: "\<forall>i\<in>?K. finite (?A i)" |
|
1786 by auto |
1813 have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow> |
1787 have d: "\<forall>i\<in> ?K. \<forall>j\<in> ?K. i \<noteq> j \<longrightarrow> |
1814 {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}" |
1788 {replicate (k + 1) 0[i := n]} \<inter> {replicate (k + 1) 0[j := n]} = {}" |
1815 proof clarify |
1789 proof clarify |
1816 fix i j |
1790 fix i j |
1817 assume i: "i \<in> ?K" and j: "j\<in> ?K" and ij: "i\<noteq>j" |
1791 assume i: "i \<in> ?K" and j: "j \<in> ?K" and ij: "i \<noteq> j" |
1818 { |
1792 { |
1819 assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" |
1793 assume eq: "replicate (k+1) 0 [i:=n] = replicate (k+1) 0 [j:= n]" |
1820 have "(replicate (k+1) 0 [i:=n] ! i) = n" |
1794 have "(replicate (k+1) 0 [i:=n] ! i) = n" |
1821 using i by (simp del: replicate.simps) |
1795 using i by (simp del: replicate.simps) |
1822 moreover |
1796 moreover |
1840 proof - |
1814 proof - |
1841 let ?r = "fps_radical r (Suc k) a" |
1815 let ?r = "fps_radical r (Suc k) a" |
1842 { |
1816 { |
1843 assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" |
1817 assume r0: "(r (Suc k) (a$0)) ^ Suc k = a$0" |
1844 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1818 from a0 r0 have r00: "r (Suc k) (a$0) \<noteq> 0" by auto |
1845 { |
1819 have "?r ^ Suc k $ z = a$z" for z |
1846 fix z |
1820 proof (induct z rule: nat_less_induct) |
1847 have "?r ^ Suc k $ z = a$z" |
1821 fix n |
1848 proof (induct z rule: nat_less_induct) |
1822 assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1849 fix n |
1823 show "?r ^ Suc k $ n = a $n" |
1850 assume H: "\<forall>m<n. ?r ^ Suc k $ m = a$m" |
1824 proof (cases n) |
1851 { |
1825 case 0 |
1852 assume "n = 0" |
1826 then show ?thesis |
1853 then have "?r ^ Suc k $ n = a $n" |
1827 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp |
1854 using fps_radical_power_nth[of r "Suc k" a, OF r0] by simp |
1828 next |
1855 } |
1829 case (Suc n1) |
1856 moreover |
1830 then have "n \<noteq> 0" by simp |
1857 { |
1831 let ?Pnk = "natpermute n (k + 1)" |
1858 fix n1 assume n1: "n = Suc n1" |
1832 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1859 have nz: "n \<noteq> 0" using n1 by arith |
1833 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1860 let ?Pnk = "natpermute n (k + 1)" |
1834 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1861 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1835 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1862 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1836 have f: "finite ?Pnkn" "finite ?Pnknn" |
1863 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1837 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1864 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1838 by (metis natpermute_finite)+ |
1865 have f: "finite ?Pnkn" "finite ?Pnknn" |
1839 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1866 using finite_Un[of ?Pnkn ?Pnknn, unfolded eq] |
1840 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1867 by (metis natpermute_finite)+ |
1841 proof (rule setsum.cong) |
1868 let ?f = "\<lambda>v. \<Prod>j\<in>{0..k}. ?r $ v ! j" |
1842 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1869 have "setsum ?f ?Pnkn = setsum (\<lambda>v. ?r $ n * r (Suc k) (a $ 0) ^ k) ?Pnkn" |
1843 let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = |
1870 proof (rule setsum.cong) |
1844 fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" |
1871 fix v assume v: "v \<in> {xs \<in> natpermute n (k + 1). n \<in> set xs}" |
1845 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1872 let ?ths = "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = |
1846 unfolding natpermute_contain_maximal by auto |
1873 fps_radical r (Suc k) a $ n * r (Suc k) (a $ 0) ^ k" |
1847 have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = |
1874 from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]" |
1848 (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" |
1875 unfolding natpermute_contain_maximal by auto |
1849 apply (rule setprod.cong, simp) |
1876 have "(\<Prod>j\<in>{0..k}. fps_radical r (Suc k) a $ v ! j) = |
1850 using i r0 |
1877 (\<Prod>j\<in>{0..k}. if j = i then fps_radical r (Suc k) a $ n else r (Suc k) (a$0))" |
1851 apply (simp del: replicate.simps) |
1878 apply (rule setprod.cong, simp) |
1852 done |
1879 using i r0 |
1853 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1880 apply (simp del: replicate.simps) |
1854 using i r0 by (simp add: setprod_gen_delta) |
1881 done |
1855 finally show ?ths . |
1882 also have "\<dots> = (fps_radical r (Suc k) a $ n) * r (Suc k) (a$0) ^ k" |
1856 qed rule |
1883 using i r0 by (simp add: setprod_gen_delta) |
1857 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1884 finally show ?ths . |
1858 by (simp add: natpermute_max_card[OF \<open>n \<noteq> 0\<close>, simplified]) |
1885 qed rule |
1859 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1886 then have "setsum ?f ?Pnkn = of_nat (k+1) * ?r $ n * r (Suc k) (a $ 0) ^ k" |
1860 unfolding Suc using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc) |
1887 by (simp add: natpermute_max_card[OF nz, simplified]) |
1861 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1888 also have "\<dots> = a$n - setsum ?f ?Pnknn" |
1862 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1889 unfolding n1 using r00 a0 by (simp add: field_simps fps_radical_def del: of_nat_Suc) |
1863 unfolding fps_power_nth_Suc setsum.union_disjoint[OF f d, unfolded eq] .. |
1890 finally have fn: "setsum ?f ?Pnkn = a$n - setsum ?f ?Pnknn" . |
1864 also have "\<dots> = a$n" unfolding fn by simp |
1891 have "(?r ^ Suc k)$n = setsum ?f ?Pnkn + setsum ?f ?Pnknn" |
1865 finally show ?thesis . |
1892 unfolding fps_power_nth_Suc setsum.union_disjoint[OF f d, unfolded eq] .. |
|
1893 also have "\<dots> = a$n" unfolding fn by simp |
|
1894 finally have "?r ^ Suc k $ n = a $n" . |
|
1895 } |
|
1896 ultimately show "?r ^ Suc k $ n = a $n" by (cases n) auto |
|
1897 qed |
1866 qed |
1898 } |
1867 qed |
1899 then have ?thesis using r0 by (simp add: fps_eq_iff) |
1868 then have ?thesis using r0 by (simp add: fps_eq_iff) |
1900 } |
1869 } |
1901 moreover |
1870 moreover |
1902 { |
1871 { |
1903 assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" |
1872 assume h: "(fps_radical r (Suc k) a) ^ (Suc k) = a" |
1962 then show ?thesis by (simp add: fps_eq_iff) |
1931 then show ?thesis by (simp add: fps_eq_iff) |
1963 qed |
1932 qed |
1964 |
1933 |
1965 *) |
1934 *) |
1966 lemma eq_divide_imp': |
1935 lemma eq_divide_imp': |
1967 fixes c :: "'a::field" shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" |
1936 fixes c :: "'a::field" |
|
1937 shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c" |
1968 by (simp add: field_simps) |
1938 by (simp add: field_simps) |
1969 |
1939 |
1970 lemma radical_unique: |
1940 lemma radical_unique: |
1971 assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0" |
1941 assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0" |
1972 and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0" |
1942 and a0: "r (Suc k) (b$0 ::'a::field_char_0) = a$0" |
1973 and b0: "b$0 \<noteq> 0" |
1943 and b0: "b$0 \<noteq> 0" |
1974 shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b" |
1944 shows "a^(Suc k) = b \<longleftrightarrow> a = fps_radical r (Suc k) b" |
1975 proof - |
1945 (is "?lhs \<longleftrightarrow> ?rhs" is "_ \<longleftrightarrow> a = ?r") |
1976 let ?r = "fps_radical r (Suc k) b" |
1946 proof |
1977 have r00: "r (Suc k) (b$0) \<noteq> 0" using b0 r0 by auto |
1947 show ?lhs if ?rhs |
1978 { |
1948 using that using power_radical[OF b0, of r k, unfolded r0] by simp |
1979 assume H: "a = ?r" |
1949 show ?rhs if ?lhs |
1980 from H have "a^Suc k = b" |
1950 proof - |
1981 using power_radical[OF b0, of r k, unfolded r0] by simp |
1951 have r00: "r (Suc k) (b$0) \<noteq> 0" using b0 r0 by auto |
1982 } |
|
1983 moreover |
|
1984 { |
|
1985 assume H: "a^Suc k = b" |
|
1986 have ceq: "card {0..k} = Suc k" by simp |
1952 have ceq: "card {0..k} = Suc k" by simp |
1987 from a0 have a0r0: "a$0 = ?r$0" by simp |
1953 from a0 have a0r0: "a$0 = ?r$0" by simp |
1988 { |
1954 have "a $ n = ?r $ n" for n |
|
1955 proof (induct n rule: nat_less_induct) |
1989 fix n |
1956 fix n |
1990 have "a $ n = ?r $ n" |
1957 assume h: "\<forall>m<n. a$m = ?r $m" |
1991 proof (induct n rule: nat_less_induct) |
1958 show "a$n = ?r $ n" |
1992 fix n |
1959 proof (cases n) |
1993 assume h: "\<forall>m<n. a$m = ?r $m" |
1960 case 0 |
1994 { |
1961 then show ?thesis using a0 by simp |
1995 assume "n = 0" |
1962 next |
1996 then have "a$n = ?r $n" using a0 by simp |
1963 case (Suc n1) |
1997 } |
1964 have fK: "finite {0..k}" by simp |
1998 moreover |
1965 have nz: "n \<noteq> 0" using Suc by simp |
1999 { |
|
2000 fix n1 |
|
2001 assume n1: "n = Suc n1" |
|
2002 have fK: "finite {0..k}" by simp |
|
2003 have nz: "n \<noteq> 0" using n1 by arith |
|
2004 let ?Pnk = "natpermute n (Suc k)" |
1966 let ?Pnk = "natpermute n (Suc k)" |
2005 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
1967 let ?Pnkn = "{xs \<in> ?Pnk. n \<in> set xs}" |
2006 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
1968 let ?Pnknn = "{xs \<in> ?Pnk. n \<notin> set xs}" |
2007 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
1969 have eq: "?Pnkn \<union> ?Pnknn = ?Pnk" by blast |
2008 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
1970 have d: "?Pnkn \<inter> ?Pnknn = {}" by blast |
2051 using xs by (simp add: natpermute_def listsum_setsum_nth) |
2013 using xs by (simp add: natpermute_def listsum_setsum_nth) |
2052 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
2014 also have "\<dots> = xs!i + setsum (nth xs) {0..<i} + setsum (nth xs) {i+1..<Suc k}" |
2053 unfolding eqs setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
2015 unfolding eqs setsum.union_disjoint[OF fths(1) finite_UnI[OF fths(2,3)] d(1)] |
2054 unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)] |
2016 unfolding setsum.union_disjoint[OF fths(2) fths(3) d(2)] |
2055 by simp |
2017 by simp |
2056 finally have False using c' by simp |
2018 finally show ?thesis using c' by simp |
2057 } |
2019 qed |
2058 then have thn: "xs!i < n" by presburger |
2020 then have thn: "xs!i < n" by presburger |
2059 from h[rule_format, OF thn] show "a$(xs !i) = ?r$(xs!i)" . |
2021 from h[rule_format, OF thn] show "a$(xs !i) = ?r$(xs!i)" . |
2060 qed |
2022 qed |
2061 have th00: "\<And>x::'a. of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" |
2023 have th00: "\<And>x::'a. of_nat (Suc k) * (x * inverse (of_nat (Suc k))) = x" |
2062 by (simp add: field_simps del: of_nat_Suc) |
2024 by (simp add: field_simps del: of_nat_Suc) |
2063 from H have "b$n = a^Suc k $ n" |
2025 from \<open>?lhs\<close> have "b$n = a^Suc k $ n" |
2064 by (simp add: fps_eq_iff) |
2026 by (simp add: fps_eq_iff) |
2065 also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" |
2027 also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn" |
2066 unfolding fps_power_nth_Suc |
2028 unfolding fps_power_nth_Suc |
2067 using setsum.union_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
2029 using setsum.union_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric], |
2068 unfolded eq, of ?g] by simp |
2030 unfolded eq, of ?g] by simp |
2146 and b0: "b$0 \<noteq> 0" |
2105 and b0: "b$0 \<noteq> 0" |
2147 shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow> |
2106 shows "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0) \<longleftrightarrow> |
2148 fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" |
2107 fps_radical r (k) (a*b) = fps_radical r (k) a * fps_radical r (k) (b)" |
2149 proof - |
2108 proof - |
2150 { |
2109 { |
2151 assume r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)" |
2110 assume r0': "r k ((a * b) $ 0) = r k (a $ 0) * r k (b $ 0)" |
2152 from r0' have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0" |
2111 then have r0: "(r (k) ((a*b)$0)) ^ k = (a*b)$0" |
2153 by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) |
2112 by (simp add: fps_mult_nth ra0 rb0 power_mult_distrib) |
2154 { |
2113 have ?thesis |
2155 assume "k = 0" |
2114 proof (cases k) |
2156 then have ?thesis using r0' by simp |
2115 case 0 |
2157 } |
2116 then show ?thesis using r0' by simp |
2158 moreover |
2117 next |
2159 { |
2118 case (Suc h) |
2160 fix h assume k: "k = Suc h" |
|
2161 let ?ra = "fps_radical r (Suc h) a" |
2119 let ?ra = "fps_radical r (Suc h) a" |
2162 let ?rb = "fps_radical r (Suc h) b" |
2120 let ?rb = "fps_radical r (Suc h) b" |
2163 have th0: "r (Suc h) ((a * b) $ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) $ 0" |
2121 have th0: "r (Suc h) ((a * b) $ 0) = (fps_radical r (Suc h) a * fps_radical r (Suc h) b) $ 0" |
2164 using r0' k by (simp add: fps_mult_nth) |
2122 using r0' Suc by (simp add: fps_mult_nth) |
2165 have ab0: "(a*b) $ 0 \<noteq> 0" |
2123 have ab0: "(a*b) $ 0 \<noteq> 0" |
2166 using a0 b0 by (simp add: fps_mult_nth) |
2124 using a0 b0 by (simp add: fps_mult_nth) |
2167 from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded k] th0 ab0, symmetric] |
2125 from radical_unique[of r h "a*b" "fps_radical r (Suc h) a * fps_radical r (Suc h) b", OF r0[unfolded Suc] th0 ab0, symmetric] |
2168 iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded k]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded k]] k r0' |
2126 iffD1[OF power_radical[of _ r], OF a0 ra0[unfolded Suc]] iffD1[OF power_radical[of _ r], OF b0 rb0[unfolded Suc]] Suc r0' |
2169 have ?thesis by (auto simp add: power_mult_distrib simp del: power_Suc) |
2127 show ?thesis |
2170 } |
2128 by (auto simp add: power_mult_distrib simp del: power_Suc) |
2171 ultimately have ?thesis by (cases k) auto |
2129 qed |
2172 } |
2130 } |
2173 moreover |
2131 moreover |
2174 { |
2132 { |
2175 assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b" |
2133 assume h: "fps_radical r k (a*b) = fps_radical r k a * fps_radical r k b" |
2176 then have "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0" |
2134 then have "(fps_radical r k (a*b))$0 = (fps_radical r k a * fps_radical r k b)$0" |
2220 and a0: "a$0 \<noteq> 0" |
2178 and a0: "a$0 \<noteq> 0" |
2221 and b0: "b$0 \<noteq> 0" |
2179 and b0: "b$0 \<noteq> 0" |
2222 shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \<longleftrightarrow> |
2180 shows "r k ((a $ 0) / (b$0)) = r k (a$0) / r k (b $ 0) \<longleftrightarrow> |
2223 fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" |
2181 fps_radical r k (a/b) = fps_radical r k a / fps_radical r k b" |
2224 (is "?lhs = ?rhs") |
2182 (is "?lhs = ?rhs") |
2225 proof - |
2183 proof |
2226 let ?r = "fps_radical r k" |
2184 let ?r = "fps_radical r k" |
2227 from kp obtain h where k: "k = Suc h" by (cases k) auto |
2185 from kp obtain h where k: "k = Suc h" by (cases k) auto |
2228 have ra0': "r k (a$0) \<noteq> 0" using a0 ra0 k by auto |
2186 have ra0': "r k (a$0) \<noteq> 0" using a0 ra0 k by auto |
2229 have rb0': "r k (b$0) \<noteq> 0" using b0 rb0 k by auto |
2187 have rb0': "r k (b$0) \<noteq> 0" using b0 rb0 k by auto |
2230 |
2188 |
2231 { |
2189 show ?lhs if ?rhs |
2232 assume ?rhs |
2190 proof - |
2233 then have "?r (a/b) $ 0 = (?r a / ?r b)$0" by simp |
2191 from that have "?r (a/b) $ 0 = (?r a / ?r b)$0" |
2234 then have ?lhs using k a0 b0 rb0' |
2192 by simp |
2235 by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) |
2193 then show ?thesis |
2236 } |
2194 using k a0 b0 rb0' by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) |
2237 moreover |
2195 qed |
2238 { |
2196 show ?rhs if ?lhs |
2239 assume h: ?lhs |
2197 proof - |
2240 from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0" |
2198 from a0 b0 have ab0[simp]: "(a/b)$0 = a$0 / b$0" |
2241 by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def) |
2199 by (simp add: fps_divide_def fps_mult_nth divide_inverse fps_inverse_def) |
2242 have th0: "r k ((a/b)$0) ^ k = (a/b)$0" |
2200 have th0: "r k ((a/b)$0) ^ k = (a/b)$0" |
2243 by (simp add: h nonzero_power_divide[OF rb0'] ra0 rb0) |
2201 by (simp add: \<open>?lhs\<close> nonzero_power_divide[OF rb0'] ra0 rb0) |
2244 from a0 b0 ra0' rb0' kp h |
2202 from a0 b0 ra0' rb0' kp \<open>?lhs\<close> |
2245 have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0" |
2203 have th1: "r k ((a / b) $ 0) = (fps_radical r k a / fps_radical r k b) $ 0" |
2246 by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) |
2204 by (simp add: fps_divide_def fps_mult_nth fps_inverse_def divide_inverse) |
2247 from a0 b0 ra0' rb0' kp have ab0': "(a / b) $ 0 \<noteq> 0" |
2205 from a0 b0 ra0' rb0' kp have ab0': "(a / b) $ 0 \<noteq> 0" |
2248 by (simp add: fps_divide_def fps_mult_nth fps_inverse_def nonzero_imp_inverse_nonzero) |
2206 by (simp add: fps_divide_def fps_mult_nth fps_inverse_def nonzero_imp_inverse_nonzero) |
2249 note tha[simp] = iffD1[OF power_radical[where r=r and k=h], OF a0 ra0[unfolded k], unfolded k[symmetric]] |
2207 note tha[simp] = iffD1[OF power_radical[where r=r and k=h], OF a0 ra0[unfolded k], unfolded k[symmetric]] |
2250 note thb[simp] = iffD1[OF power_radical[where r=r and k=h], OF b0 rb0[unfolded k], unfolded k[symmetric]] |
2208 note thb[simp] = iffD1[OF power_radical[where r=r and k=h], OF b0 rb0[unfolded k], unfolded k[symmetric]] |
2251 have th2: "(?r a / ?r b)^k = a/b" |
2209 have th2: "(?r a / ?r b)^k = a/b" |
2252 by (simp add: fps_divide_def power_mult_distrib fps_inverse_power[symmetric]) |
2210 by (simp add: fps_divide_def power_mult_distrib fps_inverse_power[symmetric]) |
2253 from iffD1[OF radical_unique[where r=r and a="?r a / ?r b" and b="a/b" and k=h], symmetric, unfolded k[symmetric], OF th0 th1 ab0' th2] |
2211 from iffD1[OF radical_unique[where r=r and a="?r a / ?r b" and b="a/b" and k=h], symmetric, unfolded k[symmetric], OF th0 th1 ab0' th2] |
2254 have ?rhs . |
2212 show ?thesis . |
2255 } |
2213 qed |
2256 ultimately show ?thesis by blast |
|
2257 qed |
2214 qed |
2258 |
2215 |
2259 lemma radical_inverse: |
2216 lemma radical_inverse: |
2260 fixes a :: "'a::field_char_0 fps" |
2217 fixes a :: "'a::field_char_0 fps" |
2261 assumes k: "k > 0" |
2218 assumes k: "k > 0" |
2265 shows "r k (inverse (a $ 0)) = r k 1 / (r k (a $ 0)) \<longleftrightarrow> |
2222 shows "r k (inverse (a $ 0)) = r k 1 / (r k (a $ 0)) \<longleftrightarrow> |
2266 fps_radical r k (inverse a) = fps_radical r k 1 / fps_radical r k a" |
2223 fps_radical r k (inverse a) = fps_radical r k 1 / fps_radical r k a" |
2267 using radical_divide[where k=k and r=r and a=1 and b=a, OF k ] ra0 r1 a0 |
2224 using radical_divide[where k=k and r=r and a=1 and b=a, OF k ] ra0 r1 a0 |
2268 by (simp add: divide_inverse fps_divide_def) |
2225 by (simp add: divide_inverse fps_divide_def) |
2269 |
2226 |
2270 subsection\<open>Derivative of composition\<close> |
2227 |
|
2228 subsection \<open>Derivative of composition\<close> |
2271 |
2229 |
2272 lemma fps_compose_deriv: |
2230 lemma fps_compose_deriv: |
2273 fixes a :: "'a::idom fps" |
2231 fixes a :: "'a::idom fps" |
2274 assumes b0: "b$0 = 0" |
2232 assumes b0: "b$0 = 0" |
2275 shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * fps_deriv b" |
2233 shows "fps_deriv (a oo b) = ((fps_deriv a) oo b) * fps_deriv b" |
2276 proof - |
2234 proof - |
2277 { |
2235 have "(fps_deriv (a oo b))$n = (((fps_deriv a) oo b) * (fps_deriv b)) $n" for n |
2278 fix n |
2236 proof - |
2279 have "(fps_deriv (a oo b))$n = setsum (\<lambda>i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}" |
2237 have "(fps_deriv (a oo b))$n = setsum (\<lambda>i. a $ i * (fps_deriv (b^i))$n) {0.. Suc n}" |
2280 by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc) |
2238 by (simp add: fps_compose_def field_simps setsum_right_distrib del: of_nat_Suc) |
2281 also have "\<dots> = setsum (\<lambda>i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}" |
2239 also have "\<dots> = setsum (\<lambda>i. a$i * ((fps_const (of_nat i)) * (fps_deriv b * (b^(i - 1))))$n) {0.. Suc n}" |
2282 by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) |
2240 by (simp add: field_simps fps_deriv_power del: fps_mult_left_const_nth of_nat_Suc) |
2283 also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}" |
2241 also have "\<dots> = setsum (\<lambda>i. of_nat i * a$i * (((b^(i - 1)) * fps_deriv b))$n) {0.. Suc n}" |
2368 assumes a0: "a$0 = 0" |
2324 assumes a0: "a$0 = 0" |
2369 and a1: "a$1 \<noteq> 0" |
2325 and a1: "a$1 \<noteq> 0" |
2370 shows "fps_inv a oo a = X" |
2326 shows "fps_inv a oo a = X" |
2371 proof - |
2327 proof - |
2372 let ?i = "fps_inv a oo a" |
2328 let ?i = "fps_inv a oo a" |
2373 { |
2329 have "?i $n = X$n" for n |
|
2330 proof (induct n rule: nat_less_induct) |
2374 fix n |
2331 fix n |
2375 have "?i $n = X$n" |
2332 assume h: "\<forall>m<n. ?i$m = X$m" |
2376 proof (induct n rule: nat_less_induct) |
2333 show "?i $ n = X$n" |
2377 fix n |
2334 proof (cases n) |
2378 assume h: "\<forall>m<n. ?i$m = X$m" |
2335 case 0 |
2379 show "?i $ n = X$n" |
2336 then show ?thesis using a0 |
2380 proof (cases n) |
2337 by (simp add: fps_compose_nth fps_inv_def) |
2381 case 0 |
2338 next |
2382 then show ?thesis using a0 |
2339 case (Suc n1) |
2383 by (simp add: fps_compose_nth fps_inv_def) |
2340 have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1" |
2384 next |
2341 by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc) |
2385 case (Suc n1) |
2342 also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + |
2386 have "?i $ n = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + fps_inv a $ Suc n1 * (a $ 1)^ Suc n1" |
2343 (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})" |
2387 by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc) |
2344 using a0 a1 Suc by (simp add: fps_inv_def) |
2388 also have "\<dots> = setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1} + |
2345 also have "\<dots> = X$n" using Suc by simp |
2389 (X$ Suc n1 - setsum (\<lambda>i. (fps_inv a $ i) * (a^i)$n) {0 .. n1})" |
2346 finally show ?thesis . |
2390 using a0 a1 Suc by (simp add: fps_inv_def) |
|
2391 also have "\<dots> = X$n" using Suc by simp |
|
2392 finally show ?thesis . |
|
2393 qed |
|
2394 qed |
2347 qed |
2395 } |
2348 qed |
2396 then show ?thesis by (simp add: fps_eq_iff) |
2349 then show ?thesis |
|
2350 by (simp add: fps_eq_iff) |
2397 qed |
2351 qed |
2398 |
2352 |
2399 |
2353 |
2400 fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::field" |
2354 fun gcompinv :: "'a fps \<Rightarrow> 'a fps \<Rightarrow> nat \<Rightarrow> 'a::field" |
2401 where |
2355 where |
2409 assumes a0: "a$0 = 0" |
2363 assumes a0: "a$0 = 0" |
2410 and a1: "a$1 \<noteq> 0" |
2364 and a1: "a$1 \<noteq> 0" |
2411 shows "fps_ginv b a oo a = b" |
2365 shows "fps_ginv b a oo a = b" |
2412 proof - |
2366 proof - |
2413 let ?i = "fps_ginv b a oo a" |
2367 let ?i = "fps_ginv b a oo a" |
2414 { |
2368 have "?i $n = b$n" for n |
|
2369 proof (induct n rule: nat_less_induct) |
2415 fix n |
2370 fix n |
2416 have "?i $n = b$n" |
2371 assume h: "\<forall>m<n. ?i$m = b$m" |
2417 proof (induct n rule: nat_less_induct) |
2372 show "?i $ n = b$n" |
2418 fix n |
2373 proof (cases n) |
2419 assume h: "\<forall>m<n. ?i$m = b$m" |
2374 case 0 |
2420 show "?i $ n = b$n" |
2375 then show ?thesis using a0 |
2421 proof (cases n) |
2376 by (simp add: fps_compose_nth fps_ginv_def) |
2422 case 0 |
2377 next |
2423 then show ?thesis using a0 |
2378 case (Suc n1) |
2424 by (simp add: fps_compose_nth fps_ginv_def) |
2379 have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1" |
2425 next |
2380 by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc) |
2426 case (Suc n1) |
2381 also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + |
2427 have "?i $ n = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + fps_ginv b a $ Suc n1 * (a $ 1)^ Suc n1" |
2382 (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})" |
2428 by (simp only: fps_compose_nth) (simp add: Suc startsby_zero_power_nth_same [OF a0] del: power_Suc) |
2383 using a0 a1 Suc by (simp add: fps_ginv_def) |
2429 also have "\<dots> = setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1} + |
2384 also have "\<dots> = b$n" using Suc by simp |
2430 (b$ Suc n1 - setsum (\<lambda>i. (fps_ginv b a $ i) * (a^i)$n) {0 .. n1})" |
2385 finally show ?thesis . |
2431 using a0 a1 Suc by (simp add: fps_ginv_def) |
|
2432 also have "\<dots> = b$n" using Suc by simp |
|
2433 finally show ?thesis . |
|
2434 qed |
|
2435 qed |
2386 qed |
2436 } |
2387 qed |
2437 then show ?thesis by (simp add: fps_eq_iff) |
2388 then show ?thesis |
|
2389 by (simp add: fps_eq_iff) |
2438 qed |
2390 qed |
2439 |
2391 |
2440 lemma fps_inv_ginv: "fps_inv = fps_ginv X" |
2392 lemma fps_inv_ginv: "fps_inv = fps_ginv X" |
2441 apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def) |
2393 apply (auto simp add: fun_eq_iff fps_eq_iff fps_inv_def fps_ginv_def) |
2442 apply (induct_tac n rule: nat_less_induct) |
2394 apply (induct_tac n rule: nat_less_induct) |
2727 proof (cases k) |
2677 proof (cases k) |
2728 case 0 |
2678 case 0 |
2729 then show ?thesis by simp |
2679 then show ?thesis by simp |
2730 next |
2680 next |
2731 case (Suc h) |
2681 case (Suc h) |
2732 { |
2682 have "?l $ n = ?r $n" for n |
2733 fix n |
2683 proof - |
2734 { |
2684 consider "k > n" | "k \<le> n" by arith |
2735 assume kn: "k>n" |
2685 then show ?thesis |
2736 then have "?l $ n = ?r $n" using a0 startsby_zero_power_prefix[OF a0] Suc |
2686 proof cases |
|
2687 case 1 |
|
2688 then show ?thesis |
|
2689 using a0 startsby_zero_power_prefix[OF a0] Suc |
2737 by (simp add: fps_compose_nth del: power_Suc) |
2690 by (simp add: fps_compose_nth del: power_Suc) |
2738 } |
2691 next |
2739 moreover |
2692 case 2 |
2740 { |
2693 then show ?thesis |
2741 assume kn: "k \<le> n" |
|
2742 then have "?l$n = ?r$n" |
|
2743 by (simp add: fps_compose_nth mult_delta_left setsum.delta) |
2694 by (simp add: fps_compose_nth mult_delta_left setsum.delta) |
2744 } |
2695 qed |
2745 moreover have "k >n \<or> k\<le> n" by arith |
2696 qed |
2746 ultimately have "?l$n = ?r$n" by blast |
2697 then show ?thesis |
2747 } |
2698 unfolding fps_eq_iff by blast |
2748 then show ?thesis unfolding fps_eq_iff by blast |
|
2749 qed |
2699 qed |
2750 |
2700 |
2751 lemma fps_inv_right: |
2701 lemma fps_inv_right: |
2752 assumes a0: "a$0 = 0" |
2702 assumes a0: "a$0 = 0" |
2753 and a1: "a$1 \<noteq> 0" |
2703 and a1: "a$1 \<noteq> 0" |
2754 shows "a oo fps_inv a = X" |
2704 shows "a oo fps_inv a = X" |
2755 proof - |
2705 proof - |
2756 let ?ia = "fps_inv a" |
2706 let ?ia = "fps_inv a" |
2757 let ?iaa = "a oo fps_inv a" |
2707 let ?iaa = "a oo fps_inv a" |
2758 have th0: "?ia $ 0 = 0" by (simp add: fps_inv_def) |
2708 have th0: "?ia $ 0 = 0" |
2759 have th1: "?iaa $ 0 = 0" using a0 a1 |
2709 by (simp add: fps_inv_def) |
2760 by (simp add: fps_inv_def fps_compose_nth) |
2710 have th1: "?iaa $ 0 = 0" |
2761 have th2: "X$0 = 0" by simp |
2711 using a0 a1 by (simp add: fps_inv_def fps_compose_nth) |
2762 from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X" by simp |
2712 have th2: "X$0 = 0" |
|
2713 by simp |
|
2714 from fps_inv[OF a0 a1] have "a oo (fps_inv a oo a) = a oo X" |
|
2715 by simp |
2763 then have "(a oo fps_inv a) oo a = X oo a" |
2716 then have "(a oo fps_inv a) oo a = X oo a" |
2764 by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0]) |
2717 by (simp add: fps_compose_assoc[OF a0 th0] X_fps_compose_startby0[OF a0]) |
2765 with fps_compose_inj_right[OF a0 a1] |
2718 with fps_compose_inj_right[OF a0 a1] show ?thesis |
2766 show ?thesis by simp |
2719 by simp |
2767 qed |
2720 qed |
2768 |
2721 |
2769 lemma fps_inv_deriv: |
2722 lemma fps_inv_deriv: |
2770 assumes a0:"a$0 = (0::'a::field)" |
2723 assumes a0: "a$0 = (0::'a::field)" |
2771 and a1: "a$1 \<noteq> 0" |
2724 and a1: "a$1 \<noteq> 0" |
2772 shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)" |
2725 shows "fps_deriv (fps_inv a) = inverse (fps_deriv a oo fps_inv a)" |
2773 proof - |
2726 proof - |
2774 let ?ia = "fps_inv a" |
2727 let ?ia = "fps_inv a" |
2775 let ?d = "fps_deriv a oo ?ia" |
2728 let ?d = "fps_deriv a oo ?ia" |
2776 let ?dia = "fps_deriv ?ia" |
2729 let ?dia = "fps_deriv ?ia" |
2777 have ia0: "?ia$0 = 0" by (simp add: fps_inv_def) |
2730 have ia0: "?ia$0 = 0" |
2778 have th0: "?d$0 \<noteq> 0" using a1 by (simp add: fps_compose_nth) |
2731 by (simp add: fps_inv_def) |
|
2732 have th0: "?d$0 \<noteq> 0" |
|
2733 using a1 by (simp add: fps_compose_nth) |
2779 from fps_inv_right[OF a0 a1] have "?d * ?dia = 1" |
2734 from fps_inv_right[OF a0 a1] have "?d * ?dia = 1" |
2780 by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] ) |
2735 by (simp add: fps_compose_deriv[OF ia0, of a, symmetric] ) |
2781 then have "inverse ?d * ?d * ?dia = inverse ?d * 1" by simp |
2736 then have "inverse ?d * ?d * ?dia = inverse ?d * 1" |
2782 with inverse_mult_eq_1 [OF th0] |
2737 by simp |
2783 show "?dia = inverse ?d" by simp |
2738 with inverse_mult_eq_1 [OF th0] show "?dia = inverse ?d" |
|
2739 by simp |
2784 qed |
2740 qed |
2785 |
2741 |
2786 lemma fps_inv_idempotent: |
2742 lemma fps_inv_idempotent: |
2787 assumes a0: "a$0 = 0" |
2743 assumes a0: "a$0 = 0" |
2788 and a1: "a$1 \<noteq> 0" |
2744 and a1: "a$1 \<noteq> 0" |
2789 shows "fps_inv (fps_inv a) = a" |
2745 shows "fps_inv (fps_inv a) = a" |
2790 proof - |
2746 proof - |
2791 let ?r = "fps_inv" |
2747 let ?r = "fps_inv" |
2792 have ra0: "?r a $ 0 = 0" by (simp add: fps_inv_def) |
2748 have ra0: "?r a $ 0 = 0" |
2793 from a1 have ra1: "?r a $ 1 \<noteq> 0" by (simp add: fps_inv_def field_simps) |
2749 by (simp add: fps_inv_def) |
2794 have X0: "X$0 = 0" by simp |
2750 from a1 have ra1: "?r a $ 1 \<noteq> 0" |
|
2751 by (simp add: fps_inv_def field_simps) |
|
2752 have X0: "X$0 = 0" |
|
2753 by simp |
2795 from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" . |
2754 from fps_inv[OF ra0 ra1] have "?r (?r a) oo ?r a = X" . |
2796 then have "?r (?r a) oo ?r a oo a = X oo a" by simp |
2755 then have "?r (?r a) oo ?r a oo a = X oo a" |
|
2756 by simp |
2797 then have "?r (?r a) oo (?r a oo a) = a" |
2757 then have "?r (?r a) oo (?r a oo a) = a" |
2798 unfolding X_fps_compose_startby0[OF a0] |
2758 unfolding X_fps_compose_startby0[OF a0] |
2799 unfolding fps_compose_assoc[OF a0 ra0, symmetric] . |
2759 unfolding fps_compose_assoc[OF a0 ra0, symmetric] . |
2800 then show ?thesis unfolding fps_inv[OF a0 a1] by simp |
2760 then show ?thesis |
|
2761 unfolding fps_inv[OF a0 a1] by simp |
2801 qed |
2762 qed |
2802 |
2763 |
2803 lemma fps_ginv_ginv: |
2764 lemma fps_ginv_ginv: |
2804 assumes a0: "a$0 = 0" |
2765 assumes a0: "a$0 = 0" |
2805 and a1: "a$1 \<noteq> 0" |
2766 and a1: "a$1 \<noteq> 0" |
2806 and c0: "c$0 = 0" |
2767 and c0: "c$0 = 0" |
2807 and c1: "c$1 \<noteq> 0" |
2768 and c1: "c$1 \<noteq> 0" |
2808 shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c" |
2769 shows "fps_ginv b (fps_ginv c a) = b oo a oo fps_inv c" |
2809 proof - |
2770 proof - |
2810 let ?r = "fps_ginv" |
2771 let ?r = "fps_ginv" |
2811 from c0 have rca0: "?r c a $0 = 0" by (simp add: fps_ginv_def) |
2772 from c0 have rca0: "?r c a $0 = 0" |
2812 from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" by (simp add: fps_ginv_def field_simps) |
2773 by (simp add: fps_ginv_def) |
|
2774 from a1 c1 have rca1: "?r c a $ 1 \<noteq> 0" |
|
2775 by (simp add: fps_ginv_def field_simps) |
2813 from fps_ginv[OF rca0 rca1] |
2776 from fps_ginv[OF rca0 rca1] |
2814 have "?r b (?r c a) oo ?r c a = b" . |
2777 have "?r b (?r c a) oo ?r c a = b" . |
2815 then have "?r b (?r c a) oo ?r c a oo a = b oo a" by simp |
2778 then have "?r b (?r c a) oo ?r c a oo a = b oo a" |
|
2779 by simp |
2816 then have "?r b (?r c a) oo (?r c a oo a) = b oo a" |
2780 then have "?r b (?r c a) oo (?r c a oo a) = b oo a" |
2817 apply (subst fps_compose_assoc) |
2781 apply (subst fps_compose_assoc) |
2818 using a0 c0 |
2782 using a0 c0 |
2819 apply (auto simp add: fps_ginv_def) |
2783 apply (auto simp add: fps_ginv_def) |
2820 done |
2784 done |
2821 then have "?r b (?r c a) oo c = b oo a" |
2785 then have "?r b (?r c a) oo c = b oo a" |
2822 unfolding fps_ginv[OF a0 a1] . |
2786 unfolding fps_ginv[OF a0 a1] . |
2823 then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" by simp |
2787 then have "?r b (?r c a) oo c oo fps_inv c= b oo a oo fps_inv c" |
|
2788 by simp |
2824 then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" |
2789 then have "?r b (?r c a) oo (c oo fps_inv c) = b oo a oo fps_inv c" |
2825 apply (subst fps_compose_assoc) |
2790 apply (subst fps_compose_assoc) |
2826 using a0 c0 |
2791 using a0 c0 |
2827 apply (auto simp add: fps_inv_def) |
2792 apply (auto simp add: fps_inv_def) |
2828 done |
2793 done |
2829 then show ?thesis unfolding fps_inv_right[OF c0 c1] by simp |
2794 then show ?thesis |
|
2795 unfolding fps_inv_right[OF c0 c1] by simp |
2830 qed |
2796 qed |
2831 |
2797 |
2832 lemma fps_ginv_deriv: |
2798 lemma fps_ginv_deriv: |
2833 assumes a0:"a$0 = (0::'a::field)" |
2799 assumes a0:"a$0 = (0::'a::field)" |
2834 and a1: "a$1 \<noteq> 0" |
2800 and a1: "a$1 \<noteq> 0" |
2836 proof - |
2802 proof - |
2837 let ?ia = "fps_ginv b a" |
2803 let ?ia = "fps_ginv b a" |
2838 let ?iXa = "fps_ginv X a" |
2804 let ?iXa = "fps_ginv X a" |
2839 let ?d = "fps_deriv" |
2805 let ?d = "fps_deriv" |
2840 let ?dia = "?d ?ia" |
2806 let ?dia = "?d ?ia" |
2841 have iXa0: "?iXa $ 0 = 0" by (simp add: fps_ginv_def) |
2807 have iXa0: "?iXa $ 0 = 0" |
2842 have da0: "?d a $ 0 \<noteq> 0" using a1 by simp |
2808 by (simp add: fps_ginv_def) |
2843 from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" by simp |
2809 have da0: "?d a $ 0 \<noteq> 0" |
2844 then have "(?d ?ia oo a) * ?d a = ?d b" unfolding fps_compose_deriv[OF a0] . |
2810 using a1 by simp |
2845 then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" by simp |
2811 from fps_ginv[OF a0 a1, of b] have "?d (?ia oo a) = fps_deriv b" |
|
2812 by simp |
|
2813 then have "(?d ?ia oo a) * ?d a = ?d b" |
|
2814 unfolding fps_compose_deriv[OF a0] . |
|
2815 then have "(?d ?ia oo a) * ?d a * inverse (?d a) = ?d b * inverse (?d a)" |
|
2816 by simp |
2846 then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" |
2817 then have "(?d ?ia oo a) * (inverse (?d a) * ?d a) = ?d b / ?d a" |
2847 by (simp add: fps_divide_def) |
2818 by (simp add: fps_divide_def) |
2848 then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa " |
2819 then have "(?d ?ia oo a) oo ?iXa = (?d b / ?d a) oo ?iXa" |
2849 unfolding inverse_mult_eq_1[OF da0] by simp |
2820 unfolding inverse_mult_eq_1[OF da0] by simp |
2850 then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" |
2821 then have "?d ?ia oo (a oo ?iXa) = (?d b / ?d a) oo ?iXa" |
2851 unfolding fps_compose_assoc[OF iXa0 a0] . |
2822 unfolding fps_compose_assoc[OF iXa0 a0] . |
2852 then show ?thesis unfolding fps_inv_ginv[symmetric] |
2823 then show ?thesis unfolding fps_inv_ginv[symmetric] |
2853 unfolding fps_inv_right[OF a0 a1] by simp |
2824 unfolding fps_inv_right[OF a0 a1] by simp |
2854 qed |
2825 qed |
2855 |
2826 |
2856 subsection\<open>Elementary series\<close> |
2827 |
2857 |
2828 subsection \<open>Elementary series\<close> |
2858 subsubsection\<open>Exponential series\<close> |
2829 |
|
2830 subsubsection \<open>Exponential series\<close> |
2859 |
2831 |
2860 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))" |
2832 definition "E x = Abs_fps (\<lambda>n. x^n / of_nat (fact n))" |
2861 |
2833 |
2862 lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r") |
2834 lemma E_deriv[simp]: "fps_deriv (E a) = fps_const (a::'a::field_char_0) * E a" (is "?l = ?r") |
2863 proof - |
2835 proof - |
2864 { |
2836 have "?l$n = ?r $ n" for n |
2865 fix n |
2837 apply (auto simp add: E_def field_simps power_Suc[symmetric] |
2866 have "?l$n = ?r $ n" |
2838 simp del: fact.simps of_nat_Suc power_Suc) |
2867 apply (auto simp add: E_def field_simps power_Suc[symmetric] |
2839 apply (simp add: of_nat_mult field_simps) |
2868 simp del: fact.simps of_nat_Suc power_Suc) |
2840 done |
2869 apply (simp add: of_nat_mult field_simps) |
2841 then show ?thesis |
2870 done |
2842 by (simp add: fps_eq_iff) |
2871 } |
|
2872 then show ?thesis by (simp add: fps_eq_iff) |
|
2873 qed |
2843 qed |
2874 |
2844 |
2875 lemma E_unique_ODE: |
2845 lemma E_unique_ODE: |
2876 "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)" |
2846 "fps_deriv a = fps_const c * a \<longleftrightarrow> a = fps_const (a$0) * E (c::'a::field_char_0)" |
2877 (is "?lhs \<longleftrightarrow> ?rhs") |
2847 (is "?lhs \<longleftrightarrow> ?rhs") |
2878 proof |
2848 proof |
2879 assume d: ?lhs |
2849 show ?rhs if ?lhs |
2880 from d have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)" |
2850 proof - |
2881 by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) |
2851 from that have th: "\<And>n. a $ Suc n = c * a$n / of_nat (Suc n)" |
2882 { |
2852 by (simp add: fps_deriv_def fps_eq_iff field_simps del: of_nat_Suc) |
2883 fix n |
2853 have th': "a$n = a$0 * c ^ n/ (fact n)" for n |
2884 have "a$n = a$0 * c ^ n/ (fact n)" |
2854 proof (induct n) |
2885 apply (induct n) |
2855 case 0 |
2886 apply simp |
2856 then show ?case by simp |
2887 unfolding th |
2857 next |
2888 using fact_gt_zero |
2858 case Suc |
2889 apply (simp add: field_simps del: of_nat_Suc fact_Suc) |
2859 then show ?case |
2890 apply simp |
2860 unfolding th |
2891 done |
2861 using fact_gt_zero |
2892 } |
2862 apply (simp add: field_simps del: of_nat_Suc fact_Suc) |
2893 note th' = this |
2863 apply simp |
2894 show ?rhs by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th') |
2864 done |
2895 next |
2865 qed |
2896 assume h: ?rhs |
2866 show ?thesis |
2897 show ?lhs |
2867 by (auto simp add: fps_eq_iff fps_const_mult_left E_def intro: th') |
2898 by (metis E_deriv fps_deriv_mult_const_left h mult.left_commute) |
2868 qed |
|
2869 show ?lhs if ?rhs |
|
2870 using that by (metis E_deriv fps_deriv_mult_const_left mult.left_commute) |
2899 qed |
2871 qed |
2900 |
2872 |
2901 lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") |
2873 lemma E_add_mult: "E (a + b) = E (a::'a::field_char_0) * E b" (is "?l = ?r") |
2902 proof - |
2874 proof - |
2903 have "fps_deriv (?r) = fps_const (a+b) * ?r" |
2875 have "fps_deriv ?r = fps_const (a + b) * ?r" |
2904 by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add) |
2876 by (simp add: fps_const_add[symmetric] field_simps del: fps_const_add) |
2905 then have "?r = ?l" apply (simp only: E_unique_ODE) |
2877 then have "?r = ?l" |
2906 by (simp add: fps_mult_nth E_def) |
2878 by (simp only: E_unique_ODE) (simp add: fps_mult_nth E_def) |
2907 then show ?thesis .. |
2879 then show ?thesis .. |
2908 qed |
2880 qed |
2909 |
2881 |
2910 lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)" |
2882 lemma E_nth[simp]: "E a $ n = a^n / of_nat (fact n)" |
2911 by (simp add: E_def) |
2883 by (simp add: E_def) |
2958 have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c" |
2931 have eq0[simp]: "?ck * of_nat (Suc k) = c" "of_nat (Suc k) * ?ck = c" |
2959 by (simp_all del: of_nat_Suc) |
2932 by (simp_all del: of_nat_Suc) |
2960 have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 .. |
2933 have th0: "E ?ck ^ (Suc k) = E c" unfolding E_power_mult eq0 .. |
2961 have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0" |
2934 have th: "r (Suc k) (E c $0) ^ Suc k = E c $ 0" |
2962 "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all |
2935 "r (Suc k) (E c $ 0) = E ?ck $ 0" "E c $ 0 \<noteq> 0" using r by simp_all |
2963 from th0 radical_unique[where r=r and k=k, OF th] |
2936 from th0 radical_unique[where r=r and k=k, OF th] show ?thesis |
2964 show ?thesis by auto |
2937 by auto |
2965 qed |
2938 qed |
2966 |
2939 |
2967 lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c" |
2940 lemma Ec_E1_eq: "E (1::'a::field_char_0) oo (fps_const c * X) = E c" |
2968 apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib) |
2941 apply (auto simp add: fps_eq_iff E_def fps_compose_def power_mult_distrib) |
2969 apply (simp add: cond_value_iff cond_application_beta setsum.delta' cong del: if_weak_cong) |
2942 apply (simp add: cond_value_iff cond_application_beta setsum.delta' cong del: if_weak_cong) |
2970 done |
2943 done |
2971 |
2944 |
2972 |
2945 |
2973 subsubsection\<open>Logarithmic series\<close> |
2946 subsubsection \<open>Logarithmic series\<close> |
2974 |
2947 |
2975 lemma Abs_fps_if_0: |
2948 lemma Abs_fps_if_0: |
2976 "Abs_fps(\<lambda>n. if n=0 then (v::'a::ring_1) else f n) = fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))" |
2949 "Abs_fps (\<lambda>n. if n = 0 then (v::'a::ring_1) else f n) = |
|
2950 fps_const v + X * Abs_fps (\<lambda>n. f (Suc n))" |
2977 by (auto simp add: fps_eq_iff) |
2951 by (auto simp add: fps_eq_iff) |
2978 |
2952 |
2979 definition L :: "'a::field_char_0 \<Rightarrow> 'a fps" |
2953 definition L :: "'a::field_char_0 \<Rightarrow> 'a fps" |
2980 where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" |
2954 where "L c = fps_const (1/c) * Abs_fps (\<lambda>n. if n = 0 then 0 else (- 1) ^ (n - 1) / of_nat n)" |
2981 |
2955 |
2982 lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)" |
2956 lemma fps_deriv_L: "fps_deriv (L c) = fps_const (1/c) * inverse (1 + X)" |
2983 unfolding fps_inverse_X_plus1 |
2957 unfolding fps_inverse_X_plus1 |
2984 by (simp add: L_def fps_eq_iff del: of_nat_Suc) |
2958 by (simp add: L_def fps_eq_iff del: of_nat_Suc) |
2985 |
2959 |
2986 lemma L_nth: "L c $ n = (if n=0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" |
2960 lemma L_nth: "L c $ n = (if n = 0 then 0 else 1/c * ((- 1) ^ (n - 1) / of_nat n))" |
2987 by (simp add: L_def field_simps) |
2961 by (simp add: L_def field_simps) |
2988 |
2962 |
2989 lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def) |
2963 lemma L_0[simp]: "L c $ 0 = 0" by (simp add: L_def) |
2990 |
2964 |
2991 lemma L_E_inv: |
2965 lemma L_E_inv: |
3030 finally show ?thesis |
3004 finally show ?thesis |
3031 unfolding fps_deriv_eq_iff by simp |
3005 unfolding fps_deriv_eq_iff by simp |
3032 qed |
3006 qed |
3033 |
3007 |
3034 |
3008 |
3035 subsubsection\<open>Binomial series\<close> |
3009 subsubsection \<open>Binomial series\<close> |
3036 |
3010 |
3037 definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)" |
3011 definition "fps_binomial a = Abs_fps (\<lambda>n. a gchoose n)" |
3038 |
3012 |
3039 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" |
3013 lemma fps_binomial_nth[simp]: "fps_binomial a $ n = a gchoose n" |
3040 by (simp add: fps_binomial_def) |
3014 by (simp add: fps_binomial_def) |
3041 |
3015 |
3042 lemma fps_binomial_ODE_unique: |
3016 lemma fps_binomial_ODE_unique: |
3043 fixes c :: "'a::field_char_0" |
3017 fixes c :: "'a::field_char_0" |
3044 shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" |
3018 shows "fps_deriv a = (fps_const c * a) / (1 + X) \<longleftrightarrow> a = fps_const (a$0) * fps_binomial c" |
3045 (is "?lhs \<longleftrightarrow> ?rhs") |
3019 (is "?lhs \<longleftrightarrow> ?rhs") |
3046 proof - |
3020 proof |
3047 let ?da = "fps_deriv a" |
3021 let ?da = "fps_deriv a" |
3048 let ?x1 = "(1 + X):: 'a fps" |
3022 let ?x1 = "(1 + X):: 'a fps" |
3049 let ?l = "?x1 * ?da" |
3023 let ?l = "?x1 * ?da" |
3050 let ?r = "fps_const c * a" |
3024 let ?r = "fps_const c * a" |
3051 have x10: "?x1 $ 0 \<noteq> 0" by simp |
3025 |
3052 have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp |
3026 have eq: "?l = ?r \<longleftrightarrow> ?lhs" |
3053 also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1" |
3027 proof - |
3054 apply (simp only: fps_divide_def mult.assoc[symmetric] inverse_mult_eq_1[OF x10]) |
3028 have x10: "?x1 $ 0 \<noteq> 0" by simp |
3055 apply (simp add: field_simps) |
3029 have "?l = ?r \<longleftrightarrow> inverse ?x1 * ?l = inverse ?x1 * ?r" by simp |
3056 done |
3030 also have "\<dots> \<longleftrightarrow> ?da = (fps_const c * a) / ?x1" |
3057 finally have eq: "?l = ?r \<longleftrightarrow> ?lhs" by simp |
3031 apply (simp only: fps_divide_def mult.assoc[symmetric] inverse_mult_eq_1[OF x10]) |
3058 moreover |
3032 apply (simp add: field_simps) |
3059 {assume h: "?l = ?r" |
3033 done |
3060 {fix n |
3034 finally show ?thesis . |
3061 from h have lrn: "?l $ n = ?r$n" by simp |
3035 qed |
3062 |
3036 |
3063 from lrn |
3037 show ?rhs if ?lhs |
3064 have "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" |
3038 proof - |
|
3039 from eq that have h: "?l = ?r" .. |
|
3040 have th0: "a$ Suc n = ((c - of_nat n) / of_nat (Suc n)) * a $n" for n |
|
3041 proof - |
|
3042 from h have "?l $ n = ?r $ n" by simp |
|
3043 then show ?thesis |
3065 apply (simp add: field_simps del: of_nat_Suc) |
3044 apply (simp add: field_simps del: of_nat_Suc) |
3066 by (cases n, simp_all add: field_simps del: of_nat_Suc) |
3045 apply (cases n) |
3067 } |
3046 apply (simp_all add: field_simps del: of_nat_Suc) |
3068 note th0 = this |
3047 done |
3069 { |
3048 qed |
3070 fix n |
3049 have th1: "a $ n = (c gchoose n) * a $ 0" for n |
3071 have "a$n = (c gchoose n) * a$0" |
3050 proof (induct n) |
3072 proof (induct n) |
3051 case 0 |
3073 case 0 |
3052 then show ?case by simp |
3074 then show ?case by simp |
3053 next |
3075 next |
3054 case (Suc m) |
3076 case (Suc m) |
3055 then show ?case |
3077 then show ?case unfolding th0 |
3056 unfolding th0 |
3078 apply (simp add: field_simps del: of_nat_Suc) |
3057 apply (simp add: field_simps del: of_nat_Suc) |
3079 unfolding mult.assoc[symmetric] gbinomial_mult_1 |
3058 unfolding mult.assoc[symmetric] gbinomial_mult_1 |
3080 apply (simp add: field_simps) |
3059 apply (simp add: field_simps) |
3081 done |
3060 done |
3082 qed |
3061 qed |
3083 } |
3062 show ?thesis |
3084 note th1 = this |
|
3085 have ?rhs |
|
3086 apply (simp add: fps_eq_iff) |
3063 apply (simp add: fps_eq_iff) |
3087 apply (subst th1) |
3064 apply (subst th1) |
3088 apply (simp add: field_simps) |
3065 apply (simp add: field_simps) |
3089 done |
3066 done |
3090 } |
3067 qed |
3091 moreover |
3068 |
3092 { |
3069 show ?lhs if ?rhs |
3093 assume h: ?rhs |
3070 proof - |
3094 have th00: "\<And>x y. x * (a$0 * y) = a$0 * (x*y)" |
3071 have th00: "x * (a $ 0 * y) = a $ 0 * (x * y)" for x y |
3095 by (simp add: mult.commute) |
3072 by (simp add: mult.commute) |
3096 have "?l = ?r" |
3073 have "?l = ?r" |
3097 apply (subst h) |
3074 apply (subst \<open>?rhs\<close>) |
3098 apply (subst (2) h) |
3075 apply (subst (2) \<open>?rhs\<close>) |
3099 apply (clarsimp simp add: fps_eq_iff field_simps) |
3076 apply (clarsimp simp add: fps_eq_iff field_simps) |
3100 unfolding mult.assoc[symmetric] th00 gbinomial_mult_1 |
3077 unfolding mult.assoc[symmetric] th00 gbinomial_mult_1 |
3101 apply (simp add: field_simps gbinomial_mult_1) |
3078 apply (simp add: field_simps gbinomial_mult_1) |
3102 done |
3079 done |
3103 } |
3080 with eq show ?thesis .. |
3104 ultimately show ?thesis by blast |
3081 qed |
3105 qed |
3082 qed |
3106 |
3083 |
3107 lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" |
3084 lemma fps_binomial_deriv: "fps_deriv (fps_binomial c) = fps_const c * fps_binomial c / (1 + X)" |
3108 proof - |
3085 proof - |
3109 let ?a = "fps_binomial c" |
3086 let ?a = "fps_binomial c" |
3181 (is "?l = ?r") |
3158 (is "?l = ?r") |
3182 proof - |
3159 proof - |
3183 let ?m1 = "\<lambda>m. (- 1 :: 'a) ^ m" |
3160 let ?m1 = "\<lambda>m. (- 1 :: 'a) ^ m" |
3184 let ?f = "\<lambda>m. of_nat (fact m)" |
3161 let ?f = "\<lambda>m. of_nat (fact m)" |
3185 let ?p = "\<lambda>(x::'a). pochhammer (- x)" |
3162 let ?p = "\<lambda>(x::'a). pochhammer (- x)" |
3186 from b have bn0: "?p b n \<noteq> 0" unfolding pochhammer_eq_0_iff by simp |
3163 from b have bn0: "?p b n \<noteq> 0" |
|
3164 unfolding pochhammer_eq_0_iff by simp |
3187 { |
3165 { |
3188 fix k |
3166 fix k |
3189 assume kn: "k \<in> {0..n}" |
3167 assume kn: "k \<in> {0..n}" |
3190 { |
3168 have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" |
3191 assume c:"pochhammer (b - of_nat n + 1) n = 0" |
3169 proof |
|
3170 assume "pochhammer (1 + b - of_nat n) n = 0" |
|
3171 then have c: "pochhammer (b - of_nat n + 1) n = 0" |
|
3172 by (simp add: algebra_simps) |
3192 then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j" |
3173 then obtain j where j: "j < n" "b - of_nat n + 1 = - of_nat j" |
3193 unfolding pochhammer_eq_0_iff by blast |
3174 unfolding pochhammer_eq_0_iff by blast |
3194 from j have "b = of_nat n - of_nat j - of_nat 1" |
3175 from j have "b = of_nat n - of_nat j - of_nat 1" |
3195 by (simp add: algebra_simps) |
3176 by (simp add: algebra_simps) |
3196 then have "b = of_nat (n - j - 1)" |
3177 then have "b = of_nat (n - j - 1)" |
3197 using j kn by (simp add: of_nat_diff) |
3178 using j kn by (simp add: of_nat_diff) |
3198 with b have False using j by auto |
3179 with b show False using j by auto |
3199 } |
3180 qed |
3200 then have nz: "pochhammer (1 + b - of_nat n) n \<noteq> 0" |
|
3201 by (auto simp add: algebra_simps) |
|
3202 |
3181 |
3203 from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" |
3182 from nz kn [simplified] have nz': "pochhammer (1 + b - of_nat n) k \<noteq> 0" |
3204 by (rule pochhammer_neq_0_mono) |
3183 by (rule pochhammer_neq_0_mono) |
3205 { |
3184 { |
3206 assume k0: "k = 0 \<or> n =0" |
3185 assume k0: "k = 0 \<or> n =0" |
3210 by (cases "k = 0") (simp_all add: gbinomial_pochhammer) |
3189 by (cases "k = 0") (simp_all add: gbinomial_pochhammer) |
3211 } |
3190 } |
3212 moreover |
3191 moreover |
3213 { |
3192 { |
3214 assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" |
3193 assume n0: "n \<noteq> 0" and k0: "k \<noteq> 0" |
3215 then obtain m where m: "n = Suc m" by (cases n) auto |
3194 then obtain m where m: "n = Suc m" |
3216 from k0 obtain h where h: "k = Suc h" by (cases k) auto |
3195 by (cases n) auto |
3217 { |
3196 from k0 obtain h where h: "k = Suc h" |
3218 assume "k = n" |
3197 by (cases k) auto |
3219 then have "b gchoose (n - k) = |
3198 have "b gchoose (n - k) = |
3220 (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" |
3199 (?m1 n * ?p b n * ?m1 k * ?p (of_nat n) k) / (?f n * pochhammer (b - of_nat n + 1) k)" |
|
3200 proof (cases "k = n") |
|
3201 case True |
|
3202 then show ?thesis |
3221 using pochhammer_minus'[where k=k and b=b] |
3203 using pochhammer_minus'[where k=k and b=b] |
3222 apply (simp add: pochhammer_same) |
3204 apply (simp add: pochhammer_same) |
3223 using bn0 |
3205 using bn0 |
3224 apply (simp add: field_simps power_add[symmetric]) |
3206 apply (simp add: field_simps power_add[symmetric]) |
3225 done |
3207 done |
3226 } |
3208 next |
3227 moreover |
3209 case False |
3228 { |
3210 with kn have kn': "k < n" |
3229 assume nk: "k \<noteq> n" |
3211 by simp |
3230 have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {0..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}" |
3212 have m1nk: "?m1 n = setprod (\<lambda>i. - 1) {0..m}" "?m1 k = setprod (\<lambda>i. - 1) {0..h}" |
3231 by (simp_all add: setprod_constant m h) |
3213 by (simp_all add: setprod_constant m h) |
3232 from kn nk have kn': "k < n" by simp |
|
3233 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
3214 have bnz0: "pochhammer (b - of_nat n + 1) k \<noteq> 0" |
3234 using bn0 kn |
3215 using bn0 kn |
3235 unfolding pochhammer_eq_0_iff |
3216 unfolding pochhammer_eq_0_iff |
3236 apply auto |
3217 apply auto |
3237 apply (erule_tac x= "n - ka - 1" in allE) |
3218 apply (erule_tac x= "n - ka - 1" in allE) |
3365 lemma fps_sin_deriv: |
3341 lemma fps_sin_deriv: |
3366 "fps_deriv (fps_sin c) = fps_const c * fps_cos c" |
3342 "fps_deriv (fps_sin c) = fps_const c * fps_cos c" |
3367 (is "?lhs = ?rhs") |
3343 (is "?lhs = ?rhs") |
3368 proof (rule fps_ext) |
3344 proof (rule fps_ext) |
3369 fix n :: nat |
3345 fix n :: nat |
3370 { |
3346 show "?lhs $ n = ?rhs $ n" |
3371 assume en: "even n" |
3347 proof (cases "even n") |
|
3348 case True |
3372 have "?lhs$n = of_nat (n+1) * (fps_sin c $ (n+1))" by simp |
3349 have "?lhs$n = of_nat (n+1) * (fps_sin c $ (n+1))" by simp |
3373 also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3350 also have "\<dots> = of_nat (n+1) * ((- 1)^(n div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3374 using en by (simp add: fps_sin_def) |
3351 using True by (simp add: fps_sin_def) |
3375 also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3352 also have "\<dots> = (- 1)^(n div 2) * c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3376 unfolding fact_Suc of_nat_mult |
3353 unfolding fact_Suc of_nat_mult |
3377 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3354 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3378 also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)" |
3355 also have "\<dots> = (- 1)^(n div 2) *c^Suc n / of_nat (fact n)" |
3379 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3356 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3380 finally have "?lhs $n = ?rhs$n" using en |
3357 finally show ?thesis |
3381 by (simp add: fps_cos_def field_simps) |
3358 using True by (simp add: fps_cos_def field_simps) |
3382 } |
3359 next |
3383 then show "?lhs $ n = ?rhs $ n" |
3360 case False |
3384 by (cases "even n") (simp_all add: fps_deriv_def fps_sin_def fps_cos_def) |
3361 then show ?thesis |
|
3362 by (simp_all add: fps_deriv_def fps_sin_def fps_cos_def) |
|
3363 qed |
3385 qed |
3364 qed |
3386 |
3365 |
3387 lemma fps_cos_deriv: "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)" |
3366 lemma fps_cos_deriv: "fps_deriv (fps_cos c) = fps_const (- c)* (fps_sin c)" |
3388 (is "?lhs = ?rhs") |
3367 (is "?lhs = ?rhs") |
3389 proof (rule fps_ext) |
3368 proof (rule fps_ext) |
3390 have th0: "\<And>n. - ((- 1::'a) ^ n) = (- 1)^Suc n" by simp |
3369 have th0: "- ((- 1::'a) ^ n) = (- 1)^Suc n" for n |
3391 have th1: "\<And>n. odd n \<Longrightarrow> Suc ((n - 1) div 2) = Suc n div 2" |
3370 by simp |
3392 by (case_tac n, simp_all) |
3371 show "?lhs $ n = ?rhs $ n" for n |
3393 fix n::nat |
3372 proof (cases "even n") |
3394 { |
3373 case False |
3395 assume en: "odd n" |
3374 then have n0: "n \<noteq> 0" by presburger |
3396 from en have n0: "n \<noteq>0 " by presburger |
3375 from False have th1: "Suc ((n - 1) div 2) = Suc n div 2" |
|
3376 by (cases n) simp_all |
3397 have "?lhs$n = of_nat (n+1) * (fps_cos c $ (n+1))" by simp |
3377 have "?lhs$n = of_nat (n+1) * (fps_cos c $ (n+1))" by simp |
3398 also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3378 also have "\<dots> = of_nat (n+1) * ((- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact (Suc n)))" |
3399 using en by (simp add: fps_cos_def) |
3379 using False by (simp add: fps_cos_def) |
3400 also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3380 also have "\<dots> = (- 1)^((n + 1) div 2)*c^Suc n * (of_nat (n+1) / (of_nat (Suc n) * of_nat (fact n)))" |
3401 unfolding fact_Suc of_nat_mult |
3381 unfolding fact_Suc of_nat_mult |
3402 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3382 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3403 also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" |
3383 also have "\<dots> = (- 1)^((n + 1) div 2) * c^Suc n / of_nat (fact n)" |
3404 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3384 by (simp add: field_simps del: of_nat_add of_nat_Suc) |
3405 also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" |
3385 also have "\<dots> = (- ((- 1)^((n - 1) div 2))) * c^Suc n / of_nat (fact n)" |
3406 unfolding th0 unfolding th1[OF en] by simp |
3386 unfolding th0 unfolding th1 by simp |
3407 finally have "?lhs $n = ?rhs$n" using en |
3387 finally show ?thesis |
3408 by (simp add: fps_sin_def field_simps) |
3388 using False by (simp add: fps_sin_def field_simps) |
3409 } |
3389 next |
3410 then show "?lhs $ n = ?rhs $ n" |
3390 case True |
3411 by (cases "even n") (simp_all add: fps_deriv_def fps_sin_def fps_cos_def) |
3391 then show ?thesis |
3412 qed |
3392 by (simp_all add: fps_deriv_def fps_sin_def fps_cos_def) |
3413 |
3393 qed |
3414 lemma fps_sin_cos_sum_of_squares: |
3394 qed |
3415 "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" (is "?lhs = 1") |
3395 |
|
3396 lemma fps_sin_cos_sum_of_squares: "(fps_cos c)\<^sup>2 + (fps_sin c)\<^sup>2 = 1" |
|
3397 (is "?lhs = _") |
3416 proof - |
3398 proof - |
3417 have "fps_deriv ?lhs = 0" |
3399 have "fps_deriv ?lhs = 0" |
3418 apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv) |
3400 apply (simp add: fps_deriv_power fps_sin_deriv fps_cos_deriv) |
3419 apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg) |
3401 apply (simp add: field_simps fps_const_neg[symmetric] del: fps_const_neg) |
3420 done |
3402 done |
3737 |
3722 |
3738 lemma nth_equal_imp_dist_less: |
3723 lemma nth_equal_imp_dist_less: |
3739 assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j" |
3724 assumes "\<And>j. j \<le> i \<Longrightarrow> f $ j = g $ j" |
3740 shows "dist f g < inverse (2 ^ i)" |
3725 shows "dist f g < inverse (2 ^ i)" |
3741 proof (cases "f = g") |
3726 proof (cases "f = g") |
|
3727 case True |
|
3728 then show ?thesis by simp |
|
3729 next |
3742 case False |
3730 case False |
3743 then have "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff) |
3731 then have "\<exists>n. f $ n \<noteq> g $ n" by (simp add: fps_eq_iff) |
3744 with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))" |
3732 with assms have "dist f g = inverse (2 ^ (LEAST n. f $ n \<noteq> g $ n))" |
3745 by (simp add: split_if_asm dist_fps_def) |
3733 by (simp add: split_if_asm dist_fps_def) |
3746 moreover |
3734 moreover |
3747 from assms \<open>\<exists>n. f $ n \<noteq> g $ n\<close> have "i < (LEAST n. f $ n \<noteq> g $ n)" |
3735 from assms \<open>\<exists>n. f $ n \<noteq> g $ n\<close> have "i < (LEAST n. f $ n \<noteq> g $ n)" |
3748 by (metis (mono_tags) LeastI not_less) |
3736 by (metis (mono_tags) LeastI not_less) |
3749 ultimately show ?thesis by simp |
3737 ultimately show ?thesis by simp |
3750 qed simp |
3738 qed |
3751 |
3739 |
3752 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)" |
3740 lemma dist_less_eq_nth_equal: "dist f g < inverse (2 ^ i) \<longleftrightarrow> (\<forall>j \<le> i. f $ j = g $ j)" |
3753 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast |
3741 using dist_less_imp_nth_equal nth_equal_imp_dist_less by blast |
3754 |
3742 |
3755 instance fps :: (comm_ring_1) complete_space |
3743 instance fps :: (comm_ring_1) complete_space |
3756 proof |
3744 proof |
3757 fix X :: "nat \<Rightarrow> 'a fps" |
3745 fix X :: "nat \<Rightarrow> 'a fps" |
3758 assume "Cauchy X" |
3746 assume "Cauchy X" |
3759 { |
3747 obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" |
3760 fix i |
3748 proof - |
3761 have "0 < inverse ((2::real)^i)" by simp |
3749 have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" for i |
3762 from metric_CauchyD[OF \<open>Cauchy X\<close> this] dist_less_imp_nth_equal |
3750 proof - |
3763 have "\<exists>M. \<forall>m \<ge> M. \<forall>j\<le>i. X M $ j = X m $ j" by blast |
3751 have "0 < inverse ((2::real)^i)" by simp |
3764 } |
3752 from metric_CauchyD[OF \<open>Cauchy X\<close> this] dist_less_imp_nth_equal |
3765 then obtain M where M: "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis |
3753 show ?thesis by blast |
3766 then have "\<forall>i. \<forall>m \<ge> M i. \<forall>j \<le> i. X (M i) $ j = X m $ j" by metis |
3754 qed |
|
3755 then show ?thesis using that by metis |
|
3756 qed |
|
3757 |
3767 show "convergent X" |
3758 show "convergent X" |
3768 proof (rule convergentI) |
3759 proof (rule convergentI) |
3769 show "X ----> Abs_fps (\<lambda>i. X (M i) $ i)" |
3760 show "X ----> Abs_fps (\<lambda>i. X (M i) $ i)" |
3770 unfolding tendsto_iff |
3761 unfolding tendsto_iff |
3771 proof safe |
3762 proof safe |
3774 THEN spec, of "\<lambda>x. x < e"] |
3765 THEN spec, of "\<lambda>x. x < e"] |
3775 have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially" |
3766 have "eventually (\<lambda>i. inverse (2 ^ i) < e) sequentially" |
3776 unfolding eventually_nhds |
3767 unfolding eventually_nhds |
3777 apply clarsimp |
3768 apply clarsimp |
3778 apply (rule FalseE) |
3769 apply (rule FalseE) |
3779 apply auto --\<open>slow\<close> |
3770 apply auto -- \<open>slow\<close> |
3780 done |
3771 done |
3781 then obtain i where "inverse (2 ^ i) < e" by (auto simp: eventually_sequentially) |
3772 then obtain i where "inverse (2 ^ i) < e" |
3782 have "eventually (\<lambda>x. M i \<le> x) sequentially" by (auto simp: eventually_sequentially) |
3773 by (auto simp: eventually_sequentially) |
|
3774 have "eventually (\<lambda>x. M i \<le> x) sequentially" |
|
3775 by (auto simp: eventually_sequentially) |
3783 then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially" |
3776 then show "eventually (\<lambda>x. dist (X x) (Abs_fps (\<lambda>i. X (M i) $ i)) < e) sequentially" |
3784 proof eventually_elim |
3777 proof eventually_elim |
3785 fix x |
3778 fix x |
3786 assume "M i \<le> x" |
3779 assume x: "M i \<le> x" |
3787 moreover |
3780 have "X (M i) $ j = X (M j) $ j" if "j \<le> i" for j |
3788 have "\<And>j. j \<le> i \<Longrightarrow> X (M i) $ j = X (M j) $ j" |
3781 using M that by (metis nat_le_linear) |
3789 using M by (metis nat_le_linear) |
3782 with x have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)" |
3790 ultimately have "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < inverse (2 ^ i)" |
|
3791 using M by (force simp: dist_less_eq_nth_equal) |
3783 using M by (force simp: dist_less_eq_nth_equal) |
3792 also note \<open>inverse (2 ^ i) < e\<close> |
3784 also note \<open>inverse (2 ^ i) < e\<close> |
3793 finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" . |
3785 finally show "dist (X x) (Abs_fps (\<lambda>j. X (M j) $ j)) < e" . |
3794 qed |
3786 qed |
3795 qed |
3787 qed |