equal
deleted
inserted
replaced
9 whose term with an hypernatural suffix is an infinitesimal i.e. |
9 whose term with an hypernatural suffix is an infinitesimal i.e. |
10 the whn'nth term of the hypersequence is a member of Infinitesimal |
10 the whn'nth term of the hypersequence is a member of Infinitesimal |
11 -------------------------------------------------------------------------- *) |
11 -------------------------------------------------------------------------- *) |
12 |
12 |
13 Goalw [hypnat_omega_def] |
13 Goalw [hypnat_omega_def] |
14 "(*fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"; |
14 "( *fNat* (%n::nat. inverse(real(Suc n)))) whn : Infinitesimal"; |
15 by (auto_tac (claset(), |
15 by (auto_tac (claset(), |
16 simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat])); |
16 simpset() addsimps [Infinitesimal_FreeUltrafilterNat_iff,starfunNat])); |
17 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); |
17 by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); |
18 by (auto_tac (claset(), |
18 by (auto_tac (claset(), |
19 simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2, |
19 simpset() addsimps [real_of_nat_Suc_gt_zero, abs_eqI2, |
29 \ (ALL r. 0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))"; |
29 \ (ALL r. 0 <r --> (EX no. ALL n. no <= n --> abs(X n + -L) < r))"; |
30 by (Simp_tac 1); |
30 by (Simp_tac 1); |
31 qed "LIMSEQ_iff"; |
31 qed "LIMSEQ_iff"; |
32 |
32 |
33 Goalw [NSLIMSEQ_def] |
33 Goalw [NSLIMSEQ_def] |
34 "(X ----NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"; |
34 "(X ----NS> L) = (ALL N: HNatInfinite. ( *fNat* X) N @= hypreal_of_real L)"; |
35 by (Simp_tac 1); |
35 by (Simp_tac 1); |
36 qed "NSLIMSEQ_iff"; |
36 qed "NSLIMSEQ_iff"; |
37 |
37 |
38 (*---------------------------------------- |
38 (*---------------------------------------- |
39 LIMSEQ ==> NSLIMSEQ |
39 LIMSEQ ==> NSLIMSEQ |
119 \ = {}"; |
119 \ = {}"; |
120 by Auto_tac; |
120 by Auto_tac; |
121 val lemmaLIM2 = result(); |
121 val lemmaLIM2 = result(); |
122 |
122 |
123 Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \ |
123 Goal "[| 0 < r; ALL n. r <= abs (X (f n) + - L); \ |
124 \ (*fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \ |
124 \ ( *fNat* X) (Abs_hypnat (hypnatrel `` {f})) + \ |
125 \ - hypreal_of_real L @= 0 |] ==> False"; |
125 \ - hypreal_of_real L @= 0 |] ==> False"; |
126 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
126 by (auto_tac (claset(),simpset() addsimps [starfunNat, |
127 mem_infmal_iff RS sym,hypreal_of_real_def, |
127 mem_infmal_iff RS sym,hypreal_of_real_def, |
128 hypreal_minus,hypreal_add, |
128 hypreal_minus,hypreal_add, |
129 Infinitesimal_FreeUltrafilterNat_iff])); |
129 Infinitesimal_FreeUltrafilterNat_iff])); |
417 Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real(Suc N))"; |
417 Goalw [Bseq_def] "Bseq X = (EX N. ALL n. abs(X n) < real(Suc N))"; |
418 by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1); |
418 by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1); |
419 qed "Bseq_iff1a"; |
419 qed "Bseq_iff1a"; |
420 |
420 |
421 Goalw [NSBseq_def] |
421 Goalw [NSBseq_def] |
422 "[| NSBseq X; N: HNatInfinite |] ==> (*fNat* X) N : HFinite"; |
422 "[| NSBseq X; N: HNatInfinite |] ==> ( *fNat* X) N : HFinite"; |
423 by (Blast_tac 1); |
423 by (Blast_tac 1); |
424 qed "NSBseqD"; |
424 qed "NSBseqD"; |
425 |
425 |
426 Goalw [NSBseq_def] |
426 Goalw [NSBseq_def] |
427 "ALL N: HNatInfinite. (*fNat* X) N : HFinite ==> NSBseq X"; |
427 "ALL N: HNatInfinite. ( *fNat* X) N : HFinite ==> NSBseq X"; |
428 by (assume_tac 1); |
428 by (assume_tac 1); |
429 qed "NSBseqI"; |
429 qed "NSBseqI"; |
430 |
430 |
431 (*----------------------------------------------------------- |
431 (*----------------------------------------------------------- |
432 Standard definition ==> NS definition |
432 Standard definition ==> NS definition |