author | nipkow |
Thu, 12 Oct 2000 18:38:23 +0200 | |
changeset 10212 | 33fe2d701ddd |
parent 10045 | c76b73e16711 |
child 10214 | 77349ed89f45 |
permissions | -rw-r--r-- |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
1 |
(* Title : Series.ML |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
2 |
Author : Jacques D. Fleuriot |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
3 |
Copyright : 1998 University of Cambridge |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
4 |
: 1999 University of Edinburgh |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
5 |
Description : Finite summation and infinite series |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
6 |
*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
7 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
8 |
Goal "sumr (Suc n) n f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
9 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
10 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
11 |
qed "sumr_Suc_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
12 |
Addsimps [sumr_Suc_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
13 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
14 |
Goal "sumr m m f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
15 |
by (induct_tac "m" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
16 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
17 |
qed "sumr_eq_bounds"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
18 |
Addsimps [sumr_eq_bounds]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
19 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
20 |
Goal "sumr m (Suc m) f = f(m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
21 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
22 |
qed "sumr_Suc_eq"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
23 |
Addsimps [sumr_Suc_eq]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
24 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
25 |
Goal "sumr (m+k) k f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
26 |
by (induct_tac "k" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
27 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
28 |
qed "sumr_add_lbound_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
29 |
Addsimps [sumr_add_lbound_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
30 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
31 |
Goal "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
32 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
33 |
by (auto_tac (claset(),simpset() addsimps real_add_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
34 |
qed "sumr_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
35 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
36 |
Goal "r * sumr m n f = sumr m n (%n. r * f n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
37 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
38 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
39 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
40 |
[real_add_mult_distrib2])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
41 |
qed "sumr_mult"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
42 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
43 |
Goal "n < p --> sumr 0 n f + sumr n p f = sumr 0 p f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
44 |
by (induct_tac "p" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
45 |
by (auto_tac (claset() addSDs [CLAIM "n < Suc na ==> n <= na", |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
46 |
leI] addDs [le_anti_sym],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
47 |
qed_spec_mp "sumr_split_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
48 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
49 |
Goal "!!n. n < p ==> sumr 0 p f + \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
50 |
\ - sumr 0 n f = sumr n p f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
51 |
by (dres_inst_tac [("f1","f")] (sumr_split_add RS sym) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
52 |
by (asm_simp_tac (simpset() addsimps real_add_ac) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
53 |
qed "sumr_split_add_minus"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
54 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
55 |
Goal "abs(sumr m n f) <= sumr m n (%i. abs(f i))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
56 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
57 |
by (auto_tac (claset() addIs [(abs_triangle_ineq |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
58 |
RS real_le_trans),real_add_le_mono1],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
59 |
qed "sumr_rabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
60 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
61 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r = g r) \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
62 |
\ --> sumr m n f = sumr m n g"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
63 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
64 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
65 |
qed_spec_mp "sumr_fun_eq"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
66 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
67 |
Goal "sumr 0 n (%i. r) = real_of_nat n*r"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
68 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
69 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
70 |
[real_add_mult_distrib,real_of_nat_zero])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
71 |
qed "sumr_const"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
72 |
Addsimps [sumr_const]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
73 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
74 |
Goal "sumr 0 n f + -(real_of_nat n*r) = sumr 0 n (%i. f i + -r)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
75 |
by (full_simp_tac (simpset() addsimps [sumr_add RS sym, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
76 |
real_minus_mult_eq2] delsimps [real_minus_mult_eq2 RS sym]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
77 |
qed "sumr_add_mult_const"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
78 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
79 |
goalw Series.thy [real_diff_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
80 |
"sumr 0 n f - (real_of_nat n*r) = sumr 0 n (%i. f i - r)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
81 |
by (full_simp_tac (simpset() addsimps [sumr_add_mult_const]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
82 |
qed "sumr_diff_mult_const"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
83 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
84 |
Goal "n < m --> sumr m n f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
85 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
86 |
by (auto_tac (claset() addDs [less_imp_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
87 |
qed_spec_mp "sumr_less_bounds_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
88 |
Addsimps [sumr_less_bounds_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
89 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
90 |
Goal "sumr m n (%i. - f i) = - sumr m n f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
91 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
92 |
by (case_tac "Suc n <= m" 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
93 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
94 |
[real_minus_add_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
95 |
qed "sumr_minus"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
96 |
|
10212 | 97 |
context Arithmetic.thy; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
98 |
|
10212 | 99 |
Goal "!!n. ~ Suc n <= m + k ==> ~ Suc n <= m"; |
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
100 |
by (auto_tac (claset() addSDs [not_leE],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
101 |
qed "lemma_not_Suc_add"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
102 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
103 |
context thy; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
104 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
105 |
Goal "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
106 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
107 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
108 |
qed "sumr_shift_bounds"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
109 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
110 |
Goal "sumr 0 (n + n) (%i. (- #1) ^ Suc i) = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
111 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
112 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
113 |
qed "sumr_minus_one_realpow_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
114 |
Addsimps [sumr_minus_one_realpow_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
115 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
116 |
Goal "sumr 0 (n + n) (%i. (#-1) ^ Suc i) = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
117 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
118 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
119 |
qed "sumr_minus_one_realpow_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
120 |
Addsimps [sumr_minus_one_realpow_zero2]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
121 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
122 |
Goal "m < Suc n ==> Suc n - m = Suc (n - m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
123 |
by (dtac less_eq_Suc_add 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
124 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
125 |
val Suc_diff_n = result(); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
126 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
127 |
Goal "(ALL n. m <= Suc n --> f n = r) & m <= na \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
128 |
\ --> sumr m na f = (real_of_nat (na - m) * r)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
129 |
by (induct_tac "na" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
130 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
131 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
132 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
133 |
by (dres_inst_tac [("x","n")] spec 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
134 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
135 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
136 |
by (asm_simp_tac (simpset() addsimps [real_add_mult_distrib, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
137 |
Suc_diff_n]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
138 |
qed_spec_mp "sumr_interval_const"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
139 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
140 |
Goal "(ALL n. m <= n --> f n = r) & m <= na \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
141 |
\ --> sumr m na f = (real_of_nat (na - m) * r)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
142 |
by (induct_tac "na" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
143 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
144 |
by (asm_full_simp_tac (simpset() addsimps [le_Suc_eq]) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
145 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
146 |
by (dres_inst_tac [("x","n")] spec 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
147 |
by (auto_tac (claset() addSDs [le_imp_less_or_eq], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
148 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
149 |
by (asm_simp_tac (simpset() addsimps [Suc_diff_n, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
150 |
real_add_mult_distrib]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
151 |
qed_spec_mp "sumr_interval_const2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
152 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
153 |
Goal "(m <= n)= (m < Suc n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
154 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
155 |
qed "le_eq_less_Suc"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
156 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
157 |
Goal "(ALL n. m <= n --> #0 <= f n) & m < na \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
158 |
\ --> sumr 0 m f <= sumr 0 na f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
159 |
by (induct_tac "na" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
160 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
161 |
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
162 |
[le_eq_less_Suc RS sym]))); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
163 |
by (ALLGOALS(dres_inst_tac [("x","n")] spec)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
164 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
165 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
166 |
by (dtac real_add_le_mono 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
167 |
by (dres_inst_tac [("i","sumr 0 m f")] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
168 |
(real_le_refl RS real_add_le_mono) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
169 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
170 |
qed_spec_mp "sumr_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
171 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
172 |
Goal "!!f g. (ALL r. m <= r & r < n --> f r <= g r) \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
173 |
\ --> sumr m n f <= sumr m n g"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
174 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
175 |
by (auto_tac (claset() addIs [real_add_le_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
176 |
simpset() addsimps [le_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
177 |
qed_spec_mp "sumr_le2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
178 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
179 |
Goal "(ALL n. #0 <= f n) --> #0 <= sumr m n f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
180 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
181 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
182 |
[rename_numerals real_le_add_order])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
183 |
qed_spec_mp "sumr_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
184 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
185 |
Goal "(ALL n. m <= n --> #0 <= f n) --> #0 <= sumr m n f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
186 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
187 |
by (auto_tac (claset() addIs [rename_numerals real_le_add_order] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
188 |
addDs [leI],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
189 |
qed_spec_mp "sumr_ge_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
190 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
191 |
Goal "#0 <= sumr m n (%n. abs (f n))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
192 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
193 |
by (auto_tac (claset() addSIs [rename_numerals real_le_add_order, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
194 |
abs_ge_zero],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
195 |
qed "sumr_rabs_ge_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
196 |
Addsimps [sumr_rabs_ge_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
197 |
AddSIs [sumr_rabs_ge_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
198 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
199 |
Goal "abs (sumr m n (%n. abs (f n))) = (sumr m n (%n. abs (f n)))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
200 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
201 |
by (Auto_tac THEN arith_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
202 |
qed "rabs_sumr_rabs_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
203 |
Addsimps [rabs_sumr_rabs_cancel]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
204 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
205 |
Goal "ALL n. N <= n --> f n = #0 \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
206 |
\ ==> ALL m n. N <= m --> sumr m n f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
207 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
208 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
209 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
210 |
qed "sumr_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
211 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
212 |
Goal "Suc N <= n --> N <= n - 1"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
213 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
214 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
215 |
qed_spec_mp "Suc_le_imp_diff_ge"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
216 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
217 |
Goal "ALL n. N <= n --> f (Suc n) = #0 \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
218 |
\ ==> ALL m n. Suc N <= m --> sumr m n f = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
219 |
by (rtac sumr_zero 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
220 |
by (subgoal_tac "0 < n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
221 |
by (dtac Suc_le_imp_diff_ge 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
222 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
223 |
qed "Suc_le_imp_diff_ge2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
224 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
225 |
(* proved elsewhere? *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
226 |
Goal "(0 < n) = (EX m. n = Suc m)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
227 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
228 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
229 |
qed "gt_zero_eq_Ex"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
230 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
231 |
Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
232 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
233 |
by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
234 |
qed "sumr_one_lb_realpow_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
235 |
Addsimps [sumr_one_lb_realpow_zero]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
236 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
237 |
Goalw [real_diff_def] "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
238 |
by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
239 |
qed "sumr_diff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
240 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
241 |
Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
242 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
243 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
244 |
qed_spec_mp "sumr_subst"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
245 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
246 |
Goal "(ALL p. m <= p & p < m + n --> (f(p) <= K)) \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
247 |
\ --> (sumr m (m + n) f <= (real_of_nat n * K))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
248 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
249 |
by (auto_tac (claset() addIs [real_add_le_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
250 |
simpset() addsimps [real_add_mult_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
251 |
qed_spec_mp "sumr_bound"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
252 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
253 |
Goal "(ALL p. 0 <= p & p < n --> (f(p) <= K)) \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
254 |
\ --> (sumr 0 n f <= (real_of_nat n * K))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
255 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
256 |
by (auto_tac (claset() addIs [real_add_le_mono], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
257 |
simpset() addsimps [real_add_mult_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
258 |
qed_spec_mp "sumr_bound2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
259 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
260 |
Goal "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
261 |
by (subgoal_tac "k = 0 | 0 < k" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
262 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
263 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
264 |
by (auto_tac (claset(),simpset() addsimps [sumr_split_add,add_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
265 |
qed "sumr_group"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
266 |
Addsimps [sumr_group]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
267 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
268 |
Goal "0 < (k::nat) --> ~(n*k < n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
269 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
270 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
271 |
qed_spec_mp "lemma_summable_group"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
272 |
Addsimps [lemma_summable_group]; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
273 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
274 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
275 |
Infinite sums |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
276 |
Theorems follow from properties of limits and sums |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
277 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
278 |
(*---------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
279 |
suminf is the sum |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
280 |
---------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
281 |
Goalw [sums_def,summable_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
282 |
"!!f. f sums l ==> summable f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
283 |
by (Blast_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
284 |
qed "sums_summable"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
285 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
286 |
Goalw [summable_def,suminf_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
287 |
"!!f. summable f ==> f sums (suminf f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
288 |
by (blast_tac (claset() addIs [someI2]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
289 |
qed "summable_sums"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
290 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
291 |
Goalw [summable_def,suminf_def,sums_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
292 |
"!!f. summable f ==> (%n. sumr 0 n f) ----> (suminf f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
293 |
by (blast_tac (claset() addIs [someI2]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
294 |
qed "summable_sumr_LIMSEQ_suminf"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
295 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
296 |
(*------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
297 |
sum is unique |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
298 |
------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
299 |
Goal "!!f. f sums s ==> (s = suminf f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
300 |
by (forward_tac [sums_summable RS summable_sums] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
301 |
by (auto_tac (claset() addSIs [LIMSEQ_unique], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
302 |
simpset() addsimps [sums_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
303 |
qed "sums_unique"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
304 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
305 |
Goalw [sums_def,LIMSEQ_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
306 |
"!!f. ALL m. n <= Suc m --> f(m) = #0 \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
307 |
\ ==> f sums (sumr 0 n f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
308 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
309 |
by (res_inst_tac [("x","n")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
310 |
by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
311 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
312 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
313 |
by (ALLGOALS (Asm_simp_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
314 |
by (dtac (conjI RS sumr_interval_const) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
315 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
316 |
qed "series_zero"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
317 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
318 |
goalw Series.thy [sums_def,LIMSEQ_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
319 |
"!!f. ALL m. n <= m --> f(m) = #0 \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
320 |
\ ==> f sums (sumr 0 n f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
321 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
322 |
by (res_inst_tac [("x","n")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
323 |
by (Step_tac 1 THEN forward_tac [le_imp_less_or_eq] 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
324 |
by (Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
325 |
by (dres_inst_tac [("f","f")] sumr_split_add_minus 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
326 |
by (ALLGOALS (Asm_simp_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
327 |
by (dtac (conjI RS sumr_interval_const2) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
328 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
329 |
qed "series_zero2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
330 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
331 |
Goalw [sums_def] "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
332 |
by (auto_tac (claset() addSIs [LIMSEQ_mult] addIs [LIMSEQ_const], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
333 |
simpset() addsimps [sumr_mult RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
334 |
qed "sums_mult"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
335 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
336 |
Goalw [sums_def] "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0 - y0)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
337 |
by (auto_tac (claset() addIs [LIMSEQ_diff], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
338 |
simpset() addsimps [sumr_diff RS sym])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
339 |
qed "sums_diff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
340 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
341 |
goal Series.thy "!!f. summable f ==> suminf f * c = suminf(%n. f n * c)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
342 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
343 |
simpset() addsimps [real_mult_commute])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
344 |
qed "suminf_mult"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
345 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
346 |
goal Series.thy "!!f. summable f ==> c * suminf f = suminf(%n. c * f n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
347 |
by (auto_tac (claset() addSIs [sums_unique,sums_mult,summable_sums], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
348 |
simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
349 |
qed "suminf_mult2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
350 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
351 |
Goal "[| summable f; summable g |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
352 |
\ ==> suminf f - suminf g = suminf(%n. f n - g n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
353 |
by (auto_tac (claset() addSIs [sums_diff,sums_unique,summable_sums],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
354 |
qed "suminf_diff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
355 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
356 |
goalw Series.thy [sums_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
357 |
"!!x. x sums x0 ==> (%n. - x n) sums - x0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
358 |
by (auto_tac (claset() addSIs [LIMSEQ_minus],simpset() addsimps [sumr_minus])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
359 |
qed "sums_minus"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
360 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
361 |
Goal "[|summable f; 0 < k |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
362 |
\ ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
363 |
by (dtac summable_sums 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
364 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
365 |
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
366 |
by (res_inst_tac [("x","no")] exI 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
367 |
by (dres_inst_tac [("x","n*k")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
368 |
by (auto_tac (claset() addSDs [not_leE],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
369 |
by (dres_inst_tac [("j","no")] less_le_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
370 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
371 |
qed "sums_group"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
372 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
373 |
Goal "[|summable f; ALL d. #0 < (f(n + (2 * d))) + f(n + ((2 * d) + 1))|] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
374 |
\ ==> sumr 0 n f < suminf f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
375 |
by (dtac summable_sums 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
376 |
by (auto_tac (claset(),simpset() addsimps [sums_def,LIMSEQ_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
377 |
by (dres_inst_tac [("x","f(n) + f(n + 1)")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
378 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
379 |
by (rtac ccontr 2 THEN dtac real_leI 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
380 |
by (subgoal_tac "sumr 0 (n + 2) f <= sumr 0 (2 * (Suc no) + n) f" 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
381 |
by (induct_tac "no" 3 THEN Simp_tac 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
382 |
by (res_inst_tac [("j","sumr 0 (2*(Suc na)+n) f")] real_le_trans 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
383 |
by (assume_tac 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
384 |
by (dres_inst_tac [("x","Suc na")] spec 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
385 |
by (dres_inst_tac [("x","0")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
386 |
by (Asm_full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
387 |
by (asm_full_simp_tac (simpset() addsimps add_ac) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
388 |
by (rotate_tac 1 1 THEN dres_inst_tac [("x","2 * (Suc no) + n")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
389 |
by (Step_tac 1 THEN Asm_full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
390 |
by (subgoal_tac "suminf f + (f(n) + f(n + 1)) <= \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
391 |
\ sumr 0 (2 * (Suc no) + n) f" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
392 |
by (res_inst_tac [("j","sumr 0 (n+2) f")] real_le_trans 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
393 |
by (assume_tac 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
394 |
by (res_inst_tac [("j","sumr 0 n f + (f(n) + f(n + 1))")] real_le_trans 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
395 |
by (REPEAT(Asm_simp_tac 2)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
396 |
by (subgoal_tac "suminf f <= sumr 0 (2 * (Suc no) + n) f" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
397 |
by (res_inst_tac [("j","suminf f + (f(n) + f(n + 1))")] real_le_trans 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
398 |
by (assume_tac 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
399 |
by (dres_inst_tac [("x","0")] spec 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
400 |
by (Asm_full_simp_tac 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
401 |
by (subgoal_tac "#0 <= sumr 0 (2 * Suc no + n) f + - suminf f" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
402 |
by (dtac (rename_numerals abs_eqI1) 1 ); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
403 |
by (Asm_full_simp_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
404 |
by (auto_tac (claset(),simpset() addsimps [real_le_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
405 |
qed "sumr_pos_lt_pair"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
406 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
407 |
(*----------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
408 |
Summable series of positive terms has limit >= any partial sum |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
409 |
----------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
410 |
Goal |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
411 |
"!!f. [| summable f; ALL m. n <= m --> #0 <= f(m) |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
412 |
\ ==> sumr 0 n f <= suminf f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
413 |
by (dtac summable_sums 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
414 |
by (rewtac sums_def); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
415 |
by (cut_inst_tac [("k","sumr 0 n f")] LIMSEQ_const 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
416 |
by (etac LIMSEQ_le 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
417 |
by (res_inst_tac [("x","n")] exI 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
418 |
by (dtac le_imp_less_or_eq 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
419 |
by (auto_tac (claset() addIs [sumr_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
420 |
qed "series_pos_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
421 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
422 |
Goal "!!f. [| summable f; ALL m. n <= m --> #0 < f(m) |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
423 |
\ ==> sumr 0 n f < suminf f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
424 |
by (res_inst_tac [("j","sumr 0 (Suc n) f")] real_less_le_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
425 |
by (rtac series_pos_le 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
426 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
427 |
by (dres_inst_tac [("x","m")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
428 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
429 |
qed "series_pos_less"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
430 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
431 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
432 |
sum of geometric progression |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
433 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
434 |
(* lemma *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
435 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
436 |
Goalw [real_diff_def] "x ~= y ==> x - y ~= (#0::real)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
437 |
by (asm_full_simp_tac (simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
438 |
[rename_numerals (real_eq_minus_iff2 RS sym)]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
439 |
qed "real_not_eq_diff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
440 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
441 |
Goal "x ~= #1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - #1) * rinv(x - #1)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
442 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
443 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
444 |
by (res_inst_tac [("c1","x - #1")] (real_mult_right_cancel RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
445 |
by (auto_tac (claset(),simpset() addsimps [real_not_eq_diff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
446 |
real_eq_minus_iff2 RS sym,real_mult_assoc,real_add_mult_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
447 |
by (asm_full_simp_tac (simpset() addsimps [real_add_mult_distrib2, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
448 |
real_diff_def,real_mult_commute]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
449 |
qed "sumr_geometric"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
450 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
451 |
Goal "abs(x) < #1 ==> (%n. x ^ n) sums rinv(#1 - x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
452 |
by (case_tac "x = #1" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
453 |
by (auto_tac (claset() addSDs [LIMSEQ_rabs_realpow_zero2], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
454 |
simpset() addsimps [sumr_geometric,abs_one,sums_def, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
455 |
real_diff_def,real_add_mult_distrib])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
456 |
by (rtac (real_add_zero_left RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
457 |
by (rtac (real_mult_0 RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
458 |
by (rtac LIMSEQ_add 1 THEN rtac LIMSEQ_mult 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
459 |
by (dtac real_not_eq_diff 3); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
460 |
by (auto_tac (claset() addIs [LIMSEQ_const], simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
461 |
[real_minus_rinv RS sym,real_diff_def,real_add_commute, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
462 |
rename_numerals LIMSEQ_rabs_realpow_zero2])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
463 |
qed "geometric_sums"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
464 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
465 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
466 |
Cauchy-type criterion for convergence of series (c.f. Harrison) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
467 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
468 |
Goalw [summable_def,sums_def,convergent_def] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
469 |
"summable f = convergent (%n. sumr 0 n f)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
470 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
471 |
qed "summable_convergent_sumr_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
472 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
473 |
Goal "summable f = \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
474 |
\ (ALL e. #0 < e --> (EX N. ALL m n. N <= m --> abs(sumr m n f) < e))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
475 |
by (auto_tac (claset(),simpset() addsimps [summable_convergent_sumr_iff, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
476 |
Cauchy_convergent_iff RS sym,Cauchy_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
477 |
by (ALLGOALS(dtac spec) THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
478 |
by (res_inst_tac [("x","M")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
479 |
by (res_inst_tac [("x","N")] exI 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
480 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
481 |
by (ALLGOALS(cut_inst_tac [("m","m"),("n","n")] less_linear)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
482 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
483 |
by (ftac (le_less_trans RS less_imp_le) 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
484 |
by (dres_inst_tac [("x","n")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
485 |
by (dres_inst_tac [("x","m")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
486 |
by (auto_tac (claset() addIs [(abs_minus_add_cancel RS subst)], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
487 |
simpset() addsimps [sumr_split_add_minus,abs_minus_add_cancel])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
488 |
qed "summable_Cauchy"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
489 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
490 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
491 |
Terms of a convergent series tend to zero |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
492 |
> Goalw [LIMSEQ_def] "summable f ==> f ----> #0"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
493 |
Proved easily in HSeries after proving nonstandard case. |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
494 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
495 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
496 |
Comparison test |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
497 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
498 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
499 |
\ summable g \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
500 |
\ |] ==> summable f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
501 |
by (auto_tac (claset(),simpset() addsimps [summable_Cauchy])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
502 |
by (dtac spec 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
503 |
by (res_inst_tac [("x","N + Na")] exI 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
504 |
by (rotate_tac 2 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
505 |
by (dres_inst_tac [("x","m")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
506 |
by (Auto_tac THEN rotate_tac 2 1 THEN dres_inst_tac [("x","n")] spec 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
507 |
by (res_inst_tac [("j","sumr m n (%k. abs(f k))")] real_le_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
508 |
by (rtac sumr_rabs 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
509 |
by (res_inst_tac [("j","sumr m n g")] real_le_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
510 |
by (auto_tac (claset() addIs [sumr_le2], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
511 |
simpset() addsimps [abs_interval_iff])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
512 |
qed "summable_comparison_test"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
513 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
514 |
Goal "[| EX N. ALL n. N <= n --> abs(f n) <= g n; \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
515 |
\ summable g \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
516 |
\ |] ==> summable (%k. abs (f k))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
517 |
by (rtac summable_comparison_test 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
518 |
by (auto_tac (claset(),simpset() addsimps [abs_idempotent])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
519 |
qed "summable_rabs_comparison_test"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
520 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
521 |
(*------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
522 |
(* Limit comparison property for series (c.f. jrh) *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
523 |
(*------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
524 |
Goal "[|ALL n. f n <= g n; summable f; summable g |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
525 |
\ ==> suminf f <= suminf g"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
526 |
by (REPEAT(dtac summable_sums 1)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
527 |
by (auto_tac (claset() addSIs [LIMSEQ_le],simpset() addsimps [sums_def])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
528 |
by (rtac exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
529 |
by (auto_tac (claset() addSIs [sumr_le2],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
530 |
qed "summable_le"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
531 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
532 |
Goal "[|ALL n. abs(f n) <= g n; summable g |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
533 |
\ ==> summable f & suminf f <= suminf g"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
534 |
by (auto_tac (claset() addIs [summable_comparison_test] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
535 |
addSIs [summable_le],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
536 |
by (auto_tac (claset(),simpset() addsimps [abs_le_interval_iff])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
537 |
qed "summable_le2"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
538 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
539 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
540 |
Absolute convergence imples normal convergence |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
541 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
542 |
Goal "summable (%n. abs (f n)) ==> summable f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
543 |
by (auto_tac (claset(),simpset() addsimps [sumr_rabs,summable_Cauchy])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
544 |
by (dtac spec 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
545 |
by (res_inst_tac [("x","N")] exI 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
546 |
by (dtac spec 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
547 |
by (res_inst_tac [("j","sumr m n (%n. abs(f n))")] real_le_less_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
548 |
by (auto_tac (claset() addIs [sumr_rabs],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
549 |
qed "summable_rabs_cancel"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
550 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
551 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
552 |
Absolute convergence of series |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
553 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
554 |
Goal "summable (%n. abs (f n)) ==> abs(suminf f) <= suminf (%n. abs(f n))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
555 |
by (auto_tac (claset() addIs [LIMSEQ_le,LIMSEQ_imp_rabs,summable_rabs_cancel, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
556 |
summable_sumr_LIMSEQ_suminf,sumr_rabs],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
557 |
qed "summable_rabs"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
558 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
559 |
(*------------------------------------------------------------------- |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
560 |
The ratio test |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
561 |
-------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
562 |
Goal "[| c <= #0; abs x <= c * abs y |] ==> x = (#0::real)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
563 |
by (dtac real_le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
564 |
by (Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
565 |
by (dres_inst_tac [("x1","y")] (abs_ge_zero RS |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
566 |
rename_numerals real_mult_le_zero) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
567 |
by (asm_full_simp_tac (simpset() addsimps [real_mult_commute]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
568 |
by (dtac real_le_trans 1 THEN assume_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
569 |
by (TRYALL(arith_tac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
570 |
qed "rabs_ratiotest_lemma"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
571 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
572 |
(* lemmas *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
573 |
Goal "#0 < r ==> (x * r ^ n) * rinv (r ^ n) = x"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
574 |
by (auto_tac (claset(),simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
575 |
[real_mult_assoc,rename_numerals realpow_not_zero])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
576 |
val lemma_rinv_realpow = result(); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
577 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
578 |
Goal "[| c ~= #0; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
579 |
\ ==> ALL n. N <= n --> abs(f(Suc n)) <= (c * c ^ n)* (rinv(c ^ n)*abs(f n))"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
580 |
by (auto_tac (claset(),simpset() addsimps real_mult_ac)); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
581 |
by (res_inst_tac [("z2.1","c ^ n")] (real_mult_left_commute RS subst) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
582 |
by (auto_tac (claset(),simpset() addsimps [rename_numerals |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
583 |
realpow_not_zero])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
584 |
val lemma_rinv_realpow2 = result(); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
585 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
586 |
Goal "(k::nat) <= l ==> (EX n. l = k + n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
587 |
by (dtac le_imp_less_or_eq 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
588 |
by (auto_tac (claset() addDs [less_eq_Suc_add],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
589 |
qed "le_Suc_ex"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
590 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
591 |
Goal "((k::nat) <= l) = (EX n. l = k + n)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
592 |
by (auto_tac (claset(),simpset() addsimps [le_Suc_ex])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
593 |
qed "le_Suc_ex_iff"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
594 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
595 |
Goal "!!c. [| c < #1; ALL n. N <= n --> abs(f(Suc n)) <= c*abs(f n) |] \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
596 |
\ ==> summable f"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
597 |
by (subgoal_tac "c <= #0 | #0 < c" 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
598 |
by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
599 |
by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
600 |
by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
601 |
by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
602 |
by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
603 |
by (res_inst_tac [("g","%n. (abs (f N)* rinv(c ^ N))*c ^ n")] |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
604 |
summable_comparison_test 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
605 |
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
606 |
by (dtac (le_Suc_ex_iff RS iffD1) 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
607 |
by (auto_tac (claset(),simpset() addsimps [realpow_add, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
608 |
CLAIM_SIMP "(a * b) * (c * d) = (a * d) * (b * (c::real))" real_mult_ac, |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
609 |
rename_numerals realpow_not_zero])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
610 |
by (induct_tac "na" 1 THEN Auto_tac); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
611 |
by (res_inst_tac [("j","c*abs(f(N + n))")] real_le_trans 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
612 |
by (auto_tac (claset() addIs [real_mult_le_le_mono1], |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
613 |
simpset() addsimps [summable_def, CLAIM_SIMP |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
614 |
"a * (b * c) = b * (a * (c::real))" real_mult_ac])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
615 |
by (res_inst_tac [("x","(abs(f N)*rinv(c ^ N))*rinv(#1 - c)")] exI 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
616 |
by (auto_tac (claset() addSIs [sums_mult,geometric_sums],simpset() addsimps |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
617 |
[abs_eqI2])); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
618 |
qed "ratio_test"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
619 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
620 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
621 |
(*----------------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
622 |
(* Differentiation of finite sum *) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
623 |
(*----------------------------------------------------------------------------*) |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
624 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
625 |
Goal "(ALL r. m <= r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x)) \ |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
626 |
\ --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
627 |
by (induct_tac "n" 1); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
628 |
by (auto_tac (claset() addIs [DERIV_add],simpset())); |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
629 |
qed "DERIV_sumr"; |
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
630 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
631 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
632 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
633 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
634 |
|
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset
|
635 |