13957
|
1 |
(* Title : CSeries.ML
|
|
2 |
Author : Jacques D. Fleuriot
|
|
3 |
Copyright : 2002 University of Edinburgh
|
|
4 |
Description : Finite summation and infinite series for complex numbers
|
|
5 |
*)
|
|
6 |
|
|
7 |
|
|
8 |
Goal "sumc (Suc n) n f = 0";
|
|
9 |
by (induct_tac "n" 1);
|
|
10 |
by (Auto_tac);
|
|
11 |
qed "sumc_Suc_zero";
|
|
12 |
Addsimps [sumc_Suc_zero];
|
|
13 |
|
|
14 |
Goal "sumc m m f = 0";
|
|
15 |
by (induct_tac "m" 1);
|
|
16 |
by (Auto_tac);
|
|
17 |
qed "sumc_eq_bounds";
|
|
18 |
Addsimps [sumc_eq_bounds];
|
|
19 |
|
|
20 |
Goal "sumc m (Suc m) f = f(m)";
|
|
21 |
by (Auto_tac);
|
|
22 |
qed "sumc_Suc_eq";
|
|
23 |
Addsimps [sumc_Suc_eq];
|
|
24 |
|
|
25 |
Goal "sumc (m+k) k f = 0";
|
|
26 |
by (induct_tac "k" 1);
|
|
27 |
by (Auto_tac);
|
|
28 |
qed "sumc_add_lbound_zero";
|
|
29 |
Addsimps [sumc_add_lbound_zero];
|
|
30 |
|
|
31 |
Goal "sumc m n f + sumc m n g = sumc m n (%n. f n + g n)";
|
|
32 |
by (induct_tac "n" 1);
|
|
33 |
by (auto_tac (claset(),simpset() addsimps real_add_ac));
|
|
34 |
qed "sumc_add";
|
|
35 |
|
|
36 |
Goal "r * sumc m n f = sumc m n (%n. r * f n)";
|
|
37 |
by (induct_tac "n" 1);
|
|
38 |
by (Auto_tac);
|
|
39 |
by (auto_tac (claset(),simpset() addsimps
|
|
40 |
[complex_add_mult_distrib2]));
|
|
41 |
qed "sumc_mult";
|
|
42 |
|
|
43 |
Goal "n < p --> sumc 0 n f + sumc n p f = sumc 0 p f";
|
|
44 |
by (induct_tac "p" 1);
|
|
45 |
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na",
|
|
46 |
leI] addDs [le_anti_sym], simpset()));
|
|
47 |
qed_spec_mp "sumc_split_add";
|
|
48 |
|
|
49 |
Goal "n < p ==> sumc 0 p f + \
|
|
50 |
\ - sumc 0 n f = sumc n p f";
|
|
51 |
by (dres_inst_tac [("f1","f")] (sumc_split_add RS sym) 1);
|
|
52 |
by (asm_simp_tac (simpset() addsimps complex_add_ac) 1);
|
|
53 |
qed "sumc_split_add_minus";
|
|
54 |
|
|
55 |
Goal "cmod(sumc m n f) <= sumr m n (%i. cmod(f i))";
|
|
56 |
by (induct_tac "n" 1);
|
|
57 |
by (auto_tac (claset() addIs [complex_mod_triangle_ineq RS order_trans],
|
|
58 |
simpset()));
|
|
59 |
qed "sumc_cmod";
|
|
60 |
|
|
61 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \
|
|
62 |
\ --> sumc m n f = sumc m n g";
|
|
63 |
by (induct_tac "n" 1);
|
|
64 |
by (Auto_tac);
|
|
65 |
qed_spec_mp "sumc_fun_eq";
|
|
66 |
|
|
67 |
Goal "sumc 0 n (%i. r) = complex_of_real (real n) * r";
|
|
68 |
by (induct_tac "n" 1);
|
|
69 |
by (auto_tac (claset(),
|
|
70 |
simpset() addsimps [complex_add_mult_distrib,
|
|
71 |
complex_of_real_add RS sym,
|
|
72 |
real_of_nat_Suc]));
|
|
73 |
qed "sumc_const";
|
|
74 |
Addsimps [sumc_const];
|
|
75 |
|
|
76 |
Goal "sumc 0 n f + -(complex_of_real(real n) * r) = sumc 0 n (%i. f i + -r)";
|
|
77 |
by (full_simp_tac (simpset() addsimps [sumc_add RS sym]) 1);
|
|
78 |
qed "sumc_add_mult_const";
|
|
79 |
|
|
80 |
Goalw [complex_diff_def]
|
|
81 |
"sumc 0 n f - (complex_of_real(real n)*r) = sumc 0 n (%i. f i - r)";
|
|
82 |
by (full_simp_tac (simpset() addsimps [sumc_add_mult_const]) 1);
|
|
83 |
qed "sumc_diff_mult_const";
|
|
84 |
|
|
85 |
Goal "n < m --> sumc m n f = 0";
|
|
86 |
by (induct_tac "n" 1);
|
|
87 |
by Auto_tac;
|
|
88 |
qed_spec_mp "sumc_less_bounds_zero";
|
|
89 |
Addsimps [sumc_less_bounds_zero];
|
|
90 |
|
|
91 |
Goal "sumc m n (%i. - f i) = - sumc m n f";
|
|
92 |
by (induct_tac "n" 1);
|
|
93 |
by Auto_tac;
|
|
94 |
qed "sumc_minus";
|
|
95 |
|
|
96 |
Goal "sumc (m+k) (n+k) f = sumc m n (%i. f(i + k))";
|
|
97 |
by (induct_tac "n" 1);
|
|
98 |
by (Auto_tac);
|
|
99 |
qed "sumc_shift_bounds";
|
|
100 |
|
|
101 |
Goal "sumc 0 (2*n) (%i. (-1) ^ Suc i) = 0";
|
|
102 |
by (induct_tac "n" 1);
|
|
103 |
by (Auto_tac);
|
|
104 |
qed "sumc_minus_one_complexpow_zero";
|
|
105 |
Addsimps [sumc_minus_one_complexpow_zero];
|
|
106 |
|
|
107 |
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \
|
|
108 |
\ --> sumc m na f = (complex_of_real(real (na - m)) * r)";
|
|
109 |
by (induct_tac "na" 1);
|
|
110 |
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib, Suc_diff_n,
|
|
111 |
real_of_nat_Suc,complex_of_real_add RS sym,
|
|
112 |
complex_add_mult_distrib]));
|
|
113 |
qed_spec_mp "sumc_interval_const";
|
|
114 |
|
|
115 |
Goal "(ALL n. m <= n --> f n = r) & m <= na \
|
|
116 |
\ --> sumc m na f = (complex_of_real(real (na - m)) * r)";
|
|
117 |
by (induct_tac "na" 1);
|
|
118 |
by (auto_tac (claset(),simpset() addsimps [real_add_mult_distrib, Suc_diff_n,
|
|
119 |
real_of_nat_Suc,complex_of_real_add RS sym,
|
|
120 |
complex_add_mult_distrib]));
|
|
121 |
qed_spec_mp "sumc_interval_const2";
|
|
122 |
|
|
123 |
(***
|
|
124 |
Goal "(ALL n. m <= n --> 0 <= cmod(f n)) & m < k --> cmod(sumc 0 m f) <= cmod(sumc 0 k f)";
|
|
125 |
by (induct_tac "k" 1);
|
|
126 |
by (Step_tac 1);
|
|
127 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps [less_Suc_eq_le])));
|
|
128 |
by (ALLGOALS(dres_inst_tac [("x","n")] spec));
|
|
129 |
by (Step_tac 1);
|
|
130 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1);
|
|
131 |
by (dtac real_add_le_mono 2);
|
|
132 |
by (dres_inst_tac [("i","sumr 0 m f")] (order_refl RS real_add_le_mono) 1);
|
|
133 |
by (Auto_tac);
|
|
134 |
qed_spec_mp "sumc_le";
|
|
135 |
|
|
136 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \
|
|
137 |
\ --> sumc m n f <= sumc m n g";
|
|
138 |
by (induct_tac "n" 1);
|
|
139 |
by (auto_tac (claset() addIs [real_add_le_mono],
|
|
140 |
simpset() addsimps [le_def]));
|
|
141 |
qed_spec_mp "sumc_le2";
|
|
142 |
|
|
143 |
Goal "(ALL n. 0 <= f n) --> 0 <= sumc m n f";
|
|
144 |
by (induct_tac "n" 1);
|
|
145 |
by Auto_tac;
|
|
146 |
by (dres_inst_tac [("x","n")] spec 1);
|
|
147 |
by (arith_tac 1);
|
|
148 |
qed_spec_mp "sumc_ge_zero";
|
|
149 |
|
|
150 |
Goal "(ALL n. m <= n --> 0 <= f n) --> 0 <= sumc m n f";
|
|
151 |
by (induct_tac "n" 1);
|
|
152 |
by Auto_tac;
|
|
153 |
by (dres_inst_tac [("x","n")] spec 1);
|
|
154 |
by (arith_tac 1);
|
|
155 |
qed_spec_mp "sumc_ge_zero2";
|
|
156 |
***)
|
|
157 |
|
|
158 |
Goal "0 <= sumr m n (%n. cmod (f n))";
|
|
159 |
by (induct_tac "n" 1);
|
|
160 |
by Auto_tac;
|
|
161 |
by (res_inst_tac [("j","0")] real_le_trans 1);
|
|
162 |
by Auto_tac;
|
|
163 |
qed "sumr_cmod_ge_zero";
|
|
164 |
Addsimps [sumr_cmod_ge_zero];
|
|
165 |
AddSIs [sumr_cmod_ge_zero];
|
|
166 |
|
|
167 |
Goal "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))";
|
|
168 |
by (rtac (abs_eqI1 RS ssubst) 1 THEN Auto_tac);
|
|
169 |
qed "rabs_sumc_cmod_cancel";
|
|
170 |
Addsimps [rabs_sumc_cmod_cancel];
|
|
171 |
|
|
172 |
Goal "ALL n. N <= n --> f n = 0 \
|
|
173 |
\ ==> ALL m n. N <= m --> sumc m n f = 0";
|
|
174 |
by (Step_tac 1);
|
|
175 |
by (induct_tac "n" 1);
|
|
176 |
by (Auto_tac);
|
|
177 |
qed "sumc_zero";
|
|
178 |
|
|
179 |
Goal "ALL n. N <= n --> f (Suc n) = 0 \
|
|
180 |
\ ==> ALL m n. Suc N <= m --> sumc m n f = 0";
|
|
181 |
by (rtac sumc_zero 1 THEN Step_tac 1);
|
|
182 |
by (dres_inst_tac [("x","n - 1")] spec 1);
|
|
183 |
by Auto_tac;
|
|
184 |
by (arith_tac 1);
|
|
185 |
qed "fun_zero_sumc_zero";
|
|
186 |
|
|
187 |
Goal "sumc 1 n (%n. f(n) * 0 ^ n) = 0";
|
|
188 |
by (induct_tac "n" 1);
|
|
189 |
by (case_tac "n" 2);
|
|
190 |
by Auto_tac;
|
|
191 |
qed "sumc_one_lb_complexpow_zero";
|
|
192 |
Addsimps [sumc_one_lb_complexpow_zero];
|
|
193 |
|
|
194 |
Goalw [complex_diff_def] "sumc m n f - sumc m n g = sumc m n (%n. f n - g n)";
|
|
195 |
by (simp_tac (simpset() addsimps [sumc_add RS sym,sumc_minus]) 1);
|
|
196 |
qed "sumc_diff";
|
|
197 |
|
|
198 |
Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumc m n f = sumc m n g";
|
|
199 |
by (induct_tac "n" 1);
|
|
200 |
by (Auto_tac);
|
|
201 |
qed_spec_mp "sumc_subst";
|
|
202 |
|
|
203 |
Goal "sumc 0 n (%m. sumc (m * k) (m*k + k) f) = sumc 0 (n * k) f";
|
|
204 |
by (subgoal_tac "k = 0 | 0 < k" 1);
|
|
205 |
by (Auto_tac);
|
|
206 |
by (induct_tac "n" 1);
|
|
207 |
by (auto_tac (claset(),simpset() addsimps [sumc_split_add,add_commute]));
|
|
208 |
qed "sumc_group";
|
|
209 |
Addsimps [sumc_group];
|
|
210 |
|