10 |
10 |
11 theory SEQ |
11 theory SEQ |
12 imports NatStar |
12 imports NatStar |
13 begin |
13 begin |
14 |
14 |
15 constdefs |
15 definition |
16 |
16 |
17 LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60) |
17 LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60) |
18 --{*Standard definition of convergence of sequence*} |
18 --{*Standard definition of convergence of sequence*} |
19 "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))" |
19 "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))" |
20 |
20 |
21 NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60) |
21 NSLIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----NS> (_))" [60, 60] 60) |
22 --{*Nonstandard definition of convergence of sequence*} |
22 --{*Nonstandard definition of convergence of sequence*} |
23 "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)" |
23 "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)" |
24 |
24 |
25 lim :: "(nat => real) => real" |
25 lim :: "(nat => real) => real" |
26 --{*Standard definition of limit using choice operator*} |
26 --{*Standard definition of limit using choice operator*} |
27 "lim X == (@L. (X ----> L))" |
27 "lim X = (SOME L. (X ----> L))" |
28 |
28 |
29 nslim :: "(nat => real) => real" |
29 nslim :: "(nat => real) => real" |
30 --{*Nonstandard definition of limit using choice operator*} |
30 --{*Nonstandard definition of limit using choice operator*} |
31 "nslim X == (@L. (X ----NS> L))" |
31 "nslim X = (SOME L. (X ----NS> L))" |
32 |
32 |
33 convergent :: "(nat => real) => bool" |
33 convergent :: "(nat => real) => bool" |
34 --{*Standard definition of convergence*} |
34 --{*Standard definition of convergence*} |
35 "convergent X == (\<exists>L. (X ----> L))" |
35 "convergent X = (\<exists>L. (X ----> L))" |
36 |
36 |
37 NSconvergent :: "(nat => real) => bool" |
37 NSconvergent :: "(nat => real) => bool" |
38 --{*Nonstandard definition of convergence*} |
38 --{*Nonstandard definition of convergence*} |
39 "NSconvergent X == (\<exists>L. (X ----NS> L))" |
39 "NSconvergent X = (\<exists>L. (X ----NS> L))" |
40 |
40 |
41 Bseq :: "(nat => real) => bool" |
41 Bseq :: "(nat => real) => bool" |
42 --{*Standard definition for bounded sequence*} |
42 --{*Standard definition for bounded sequence*} |
43 "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K" |
43 "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)" |
44 |
44 |
45 NSBseq :: "(nat=>real) => bool" |
45 NSBseq :: "(nat=>real) => bool" |
46 --{*Nonstandard definition for bounded sequence*} |
46 --{*Nonstandard definition for bounded sequence*} |
47 "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)" |
47 "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)" |
48 |
48 |
49 monoseq :: "(nat=>real)=>bool" |
49 monoseq :: "(nat=>real)=>bool" |
50 --{*Definition for monotonicity*} |
50 --{*Definition for monotonicity*} |
51 "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)" |
51 "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))" |
52 |
52 |
53 subseq :: "(nat => nat) => bool" |
53 subseq :: "(nat => nat) => bool" |
54 --{*Definition of subsequence*} |
54 --{*Definition of subsequence*} |
55 "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)" |
55 "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))" |
56 |
56 |
57 Cauchy :: "(nat => real) => bool" |
57 Cauchy :: "(nat => real) => bool" |
58 --{*Standard definition of the Cauchy condition*} |
58 --{*Standard definition of the Cauchy condition*} |
59 "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e" |
59 "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)" |
60 |
60 |
61 NSCauchy :: "(nat => real) => bool" |
61 NSCauchy :: "(nat => real) => bool" |
62 --{*Nonstandard definition*} |
62 --{*Nonstandard definition*} |
63 "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. |
63 "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)" |
64 ( *f* X) M \<approx> ( *f* X) N)" |
|
65 |
64 |
66 |
65 |
67 |
66 |
68 text{* Example of an hypersequence (i.e. an extended standard sequence) |
67 text{* Example of an hypersequence (i.e. an extended standard sequence) |
69 whose term with an hypernatural suffix is an infinitesimal i.e. |
68 whose term with an hypernatural suffix is an infinitesimal i.e. |
1193 up a sequence |
1192 up a sequence |
1194 Goal "subseq f ==> n \<le> f(n)"; |
1193 Goal "subseq f ==> n \<le> f(n)"; |
1195 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)"; |
1194 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)"; |
1196 ---------------------------------------------------------------***) |
1195 ---------------------------------------------------------------***) |
1197 |
1196 |
1198 |
|
1199 ML |
|
1200 {* |
|
1201 val Cauchy_def = thm"Cauchy_def"; |
|
1202 val SEQ_Infinitesimal = thm "SEQ_Infinitesimal"; |
|
1203 val LIMSEQ_iff = thm "LIMSEQ_iff"; |
|
1204 val NSLIMSEQ_iff = thm "NSLIMSEQ_iff"; |
|
1205 val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ"; |
|
1206 val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set"; |
|
1207 val Compl_less_set = thm "Compl_less_set"; |
|
1208 val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ"; |
|
1209 val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ"; |
|
1210 val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ"; |
|
1211 val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff"; |
|
1212 val NSLIMSEQ_const = thm "NSLIMSEQ_const"; |
|
1213 val LIMSEQ_const = thm "LIMSEQ_const"; |
|
1214 val NSLIMSEQ_add = thm "NSLIMSEQ_add"; |
|
1215 val LIMSEQ_add = thm "LIMSEQ_add"; |
|
1216 val NSLIMSEQ_mult = thm "NSLIMSEQ_mult"; |
|
1217 val LIMSEQ_mult = thm "LIMSEQ_mult"; |
|
1218 val NSLIMSEQ_minus = thm "NSLIMSEQ_minus"; |
|
1219 val LIMSEQ_minus = thm "LIMSEQ_minus"; |
|
1220 val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel"; |
|
1221 val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel"; |
|
1222 val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus"; |
|
1223 val LIMSEQ_add_minus = thm "LIMSEQ_add_minus"; |
|
1224 val LIMSEQ_diff = thm "LIMSEQ_diff"; |
|
1225 val NSLIMSEQ_diff = thm "NSLIMSEQ_diff"; |
|
1226 val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse"; |
|
1227 val LIMSEQ_inverse = thm "LIMSEQ_inverse"; |
|
1228 val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse"; |
|
1229 val LIMSEQ_divide = thm "LIMSEQ_divide"; |
|
1230 val NSLIMSEQ_unique = thm "NSLIMSEQ_unique"; |
|
1231 val LIMSEQ_unique = thm "LIMSEQ_unique"; |
|
1232 val limI = thm "limI"; |
|
1233 val nslimI = thm "nslimI"; |
|
1234 val lim_nslim_iff = thm "lim_nslim_iff"; |
|
1235 val convergentD = thm "convergentD"; |
|
1236 val convergentI = thm "convergentI"; |
|
1237 val NSconvergentD = thm "NSconvergentD"; |
|
1238 val NSconvergentI = thm "NSconvergentI"; |
|
1239 val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff"; |
|
1240 val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff"; |
|
1241 val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff"; |
|
1242 val subseq_Suc_iff = thm "subseq_Suc_iff"; |
|
1243 val monoseq_Suc = thm "monoseq_Suc"; |
|
1244 val monoI1 = thm "monoI1"; |
|
1245 val monoI2 = thm "monoI2"; |
|
1246 val mono_SucI1 = thm "mono_SucI1"; |
|
1247 val mono_SucI2 = thm "mono_SucI2"; |
|
1248 val BseqD = thm "BseqD"; |
|
1249 val BseqI = thm "BseqI"; |
|
1250 val Bseq_iff = thm "Bseq_iff"; |
|
1251 val Bseq_iff1a = thm "Bseq_iff1a"; |
|
1252 val NSBseqD = thm "NSBseqD"; |
|
1253 val NSBseqI = thm "NSBseqI"; |
|
1254 val Bseq_NSBseq = thm "Bseq_NSBseq"; |
|
1255 val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite"; |
|
1256 val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f"; |
|
1257 val NSBseq_Bseq = thm "NSBseq_Bseq"; |
|
1258 val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff"; |
|
1259 val NSconvergent_NSBseq = thm "NSconvergent_NSBseq"; |
|
1260 val convergent_Bseq = thm "convergent_Bseq"; |
|
1261 val Bseq_isUb = thm "Bseq_isUb"; |
|
1262 val Bseq_isLub = thm "Bseq_isLub"; |
|
1263 val NSBseq_isUb = thm "NSBseq_isUb"; |
|
1264 val NSBseq_isLub = thm "NSBseq_isLub"; |
|
1265 val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ"; |
|
1266 val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ"; |
|
1267 val Bseq_mono_convergent = thm "Bseq_mono_convergent"; |
|
1268 val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent"; |
|
1269 val convergent_minus_iff = thm "convergent_minus_iff"; |
|
1270 val Bseq_minus_iff = thm "Bseq_minus_iff"; |
|
1271 val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent"; |
|
1272 val Bseq_iff2 = thm "Bseq_iff2"; |
|
1273 val Bseq_iff3 = thm "Bseq_iff3"; |
|
1274 val BseqI2 = thm "BseqI2"; |
|
1275 val Cauchy_NSCauchy = thm "Cauchy_NSCauchy"; |
|
1276 val NSCauchy_Cauchy = thm "NSCauchy_Cauchy"; |
|
1277 val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff"; |
|
1278 val less_Suc_cancel_iff = thm "less_Suc_cancel_iff"; |
|
1279 val SUP_rabs_subseq = thm "SUP_rabs_subseq"; |
|
1280 val Cauchy_Bseq = thm "Cauchy_Bseq"; |
|
1281 val NSCauchy_NSBseq = thm "NSCauchy_NSBseq"; |
|
1282 val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff"; |
|
1283 val Cauchy_convergent_iff = thm "Cauchy_convergent_iff"; |
|
1284 val NSLIMSEQ_le = thm "NSLIMSEQ_le"; |
|
1285 val LIMSEQ_le = thm "LIMSEQ_le"; |
|
1286 val LIMSEQ_le_const = thm "LIMSEQ_le_const"; |
|
1287 val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const"; |
|
1288 val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2"; |
|
1289 val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2"; |
|
1290 val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc"; |
|
1291 val LIMSEQ_Suc = thm "LIMSEQ_Suc"; |
|
1292 val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc"; |
|
1293 val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc"; |
|
1294 val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff"; |
|
1295 val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff"; |
|
1296 val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero"; |
|
1297 val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero"; |
|
1298 val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs"; |
|
1299 val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs"; |
|
1300 val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero"; |
|
1301 val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero"; |
|
1302 val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat"; |
|
1303 val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat"; |
|
1304 val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add"; |
|
1305 val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add"; |
|
1306 val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus"; |
|
1307 val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus"; |
|
1308 val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult"; |
|
1309 val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult"; |
|
1310 val NSLIMSEQ_pow = thm "NSLIMSEQ_pow"; |
|
1311 val LIMSEQ_pow = thm "LIMSEQ_pow"; |
|
1312 val Bseq_realpow = thm "Bseq_realpow"; |
|
1313 val monoseq_realpow = thm "monoseq_realpow"; |
|
1314 val convergent_realpow = thm "convergent_realpow"; |
|
1315 val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero"; |
|
1316 *} |
|
1317 |
|
1318 |
|
1319 end |
1197 end |