author  paulson 
Thu, 21 Dec 2000 18:53:32 +0100  
changeset 10721  12b166418455 
parent 10720  1ce5a189f672 
permissions  rwrr 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1 
(* Title : SEQ.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 
Description : Theory of sequence and series of real numbers 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

5 
*) 
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 
Example of an hypersequence (i.e. an extended standard sequence) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

9 
whose term with an hypernatural suffix is an infinitesimal i.e. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

10 
the whn'nth term of the hypersequence is a member of Infinitesimal 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

11 
 *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

12 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

13 
Goalw [hypnat_omega_def] 
10607  14 
"(*fNat* (%n::nat. inverse(real_of_posnat n))) whn : Infinitesimal"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

15 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

16 
[Infinitesimal_FreeUltrafilterNat_iff,starfunNat])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

17 
by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

18 
by (auto_tac (claset(),simpset() addsimps (map rename_numerals) 
10607  19 
[real_of_posnat_gt_zero,real_inverse_gt_zero,abs_eqI2, 
20 
FreeUltrafilterNat_inverse_real_of_posnat])); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

21 
qed "SEQ_Infinitesimal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

22 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

23 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

24 
Rules for LIMSEQ and NSLIMSEQ etc. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

25 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

26 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

27 
(*** LIMSEQ ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

28 
Goalw [LIMSEQ_def] 
10677  29 
"X > L ==> \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

30 
\ ALL r. #0 < r > (EX no. ALL n. no <= n > abs(X n + L) < r)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

31 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

32 
qed "LIMSEQD1"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

33 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

34 
Goalw [LIMSEQ_def] 
10677  35 
"[ X > L; #0 < r] ==> \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

36 
\ EX no. ALL n. no <= n > abs(X n + L) < r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

37 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

38 
qed "LIMSEQD2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

39 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

40 
Goalw [LIMSEQ_def] 
10677  41 
"ALL r. #0 < r > (EX no. ALL n. \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

42 
\ no <= n > abs(X n + L) < r) ==> X > L"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

43 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

44 
qed "LIMSEQI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

45 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

46 
Goalw [LIMSEQ_def] 
10677  47 
"(X > L) = \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

48 
\ (ALL r. #0 <r > (EX no. ALL n. no <= n > abs(X n + L) < r))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

49 
by (Simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

50 
qed "LIMSEQ_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

51 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

52 
(*** NSLIMSEQ ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

53 
Goalw [NSLIMSEQ_def] 
10677  54 
"X NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

55 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

56 
qed "NSLIMSEQD1"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

57 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

58 
Goalw [NSLIMSEQ_def] 
10677  59 
"[ X NS> L; N: HNatInfinite ] ==> (*fNat* X) N @= hypreal_of_real L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

60 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

61 
qed "NSLIMSEQD2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

62 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

63 
Goalw [NSLIMSEQ_def] 
10677  64 
"ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X NS> L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

65 
by (Asm_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

66 
qed "NSLIMSEQI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

67 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

68 
Goalw [NSLIMSEQ_def] 
10677  69 
"(X NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

70 
by (Simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

71 
qed "NSLIMSEQ_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

72 

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 
LIMSEQ ==> NSLIMSEQ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

75 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

76 
Goalw [LIMSEQ_def,NSLIMSEQ_def] 
10677  77 
"X > L ==> X NS> L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

78 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

79 
[HNatInfinite_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

80 
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

81 
by (rtac (inf_close_minus_iff RS iffD2) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

82 
by (auto_tac (claset(),simpset() addsimps [starfunNat, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

83 
mem_infmal_iff RS sym,hypreal_of_real_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

84 
hypreal_minus,hypreal_add, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

85 
Infinitesimal_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

86 
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, Step_tac 1]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

87 
by (dres_inst_tac [("x","u")] spec 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

88 
by (dres_inst_tac [("x","no")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

89 
by (Fuf_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

90 
by (blast_tac (claset() addDs [less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

91 
qed "LIMSEQ_NSLIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

92 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

93 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

94 
NSLIMSEQ ==> LIMSEQ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

95 
proving NS def ==> Standard def is trickier as usual 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

96 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

97 
(* the following sequence f(n) defines a hypernatural *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

98 
(* lemmas etc. first *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

99 
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

100 
\ ==> {n. f n = 0} = {0}  {n. f n = 0} = {}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

101 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

102 
by (dres_inst_tac [("x","xa")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

103 
by (dres_inst_tac [("x","x")] spec 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

104 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

105 
val lemma_NSLIMSEQ1 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

106 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

107 
Goal "{n. f n <= Suc u} = {n. f n <= u} Un {n. f n = Suc u}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

108 
by (auto_tac (claset(),simpset() addsimps [le_Suc_eq])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

109 
val lemma_NSLIMSEQ2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

110 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

111 
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

112 
\ ==> {n. f n = Suc u} <= {n. n <= Suc u}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

113 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

114 
by (dres_inst_tac [("x","x")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

115 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

116 
val lemma_NSLIMSEQ3 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

117 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

118 
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

119 
\ ==> finite {n. f n <= u}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

120 
by (induct_tac "u" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

121 
by (auto_tac (claset(),simpset() addsimps [lemma_NSLIMSEQ2])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

122 
by (auto_tac (claset() addIs [(lemma_NSLIMSEQ3 RS finite_subset), 
10558  123 
finite_nat_le_segment], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

124 
by (dtac lemma_NSLIMSEQ1 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

125 
by (ALLGOALS(Asm_simp_tac)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

126 
qed "NSLIMSEQ_finite_set"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

127 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

128 
Goal " {n. u < (f::nat=>nat) n} = {n. f n <= u}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

129 
by (auto_tac (claset() addDs [less_le_trans], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

130 
simpset() addsimps [le_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

131 
qed "Compl_less_set"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

132 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

133 
(* the index set is in the free ultrafilter *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

134 
Goal "!!(f::nat=>nat). ALL n. n <= f n \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

135 
\ ==> {n. u < f n} : FreeUltrafilterNat"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

136 
by (rtac (FreeUltrafilterNat_Compl_iff2 RS iffD2) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

137 
by (rtac FreeUltrafilterNat_finite 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

138 
by (auto_tac (claset() addDs [NSLIMSEQ_finite_set], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

139 
simpset() addsimps [Compl_less_set])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

140 
qed "FreeUltrafilterNat_NSLIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

141 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

142 
(* thus, the sequence defines an infinite hypernatural! *) 
10677  143 
Goal "ALL n. n <= f n \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

144 
\ ==> Abs_hypnat (hypnatrel ^^ {f}) : HNatInfinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

145 
by (auto_tac (claset(),simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

146 
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, Step_tac 1]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

147 
by (etac FreeUltrafilterNat_NSLIMSEQ 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

148 
qed "HNatInfinite_NSLIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

149 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

150 
val lemmaLIM = CLAIM "{n. X (f n) +  L = Y n} Int {n. abs (Y n) < r} <= \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

151 
\ {n. abs (X (f n) +  L) < r}"; 
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 "{n. abs (X (f n) +  L) < r} Int \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

154 
\ {n. r <= abs (X (f n) +  (L::real))} = {}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

155 
by (auto_tac (claset() addDs [real_less_le_trans] 
10558  156 
addIs [real_less_irrefl], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

157 
val lemmaLIM2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

158 

10677  159 
Goal "[ #0 < r; ALL n. r <= abs (X (f n) +  L); \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

160 
\ (*fNat* X) (Abs_hypnat (hypnatrel ^^ {f})) + \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

161 
\  hypreal_of_real L @= 0 ] ==> False"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

162 
by (auto_tac (claset(),simpset() addsimps [starfunNat, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

163 
mem_infmal_iff RS sym,hypreal_of_real_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

164 
hypreal_minus,hypreal_add, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

165 
Infinitesimal_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

166 
by (dres_inst_tac [("x","r")] spec 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

167 
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

168 
by (dtac (lemmaLIM RSN (2,FreeUltrafilterNat_subset)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

169 
by (dtac FreeUltrafilterNat_all 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

170 
by (thin_tac "{n. abs (Y n) < r} : FreeUltrafilterNat" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

171 
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

172 
by (asm_full_simp_tac (simpset() addsimps [lemmaLIM2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

173 
FreeUltrafilterNat_empty]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

174 
val lemmaLIM3 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

175 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

176 
Goalw [LIMSEQ_def,NSLIMSEQ_def] 
10677  177 
"X NS> L ==> X > L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

178 
by (rtac ccontr 1 THEN Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

179 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

180 
(* skolemization step *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

181 
by (dtac choice 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

182 
by (dres_inst_tac [("x","Abs_hypnat(hypnatrel^^{f})")] bspec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

183 
by (dtac (inf_close_minus_iff RS iffD1) 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

184 
by (fold_tac [real_le_def]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

185 
by (blast_tac (claset() addIs [HNatInfinite_NSLIMSEQ]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

186 
by (blast_tac (claset() addIs [rename_numerals lemmaLIM3]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

187 
qed "NSLIMSEQ_LIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

188 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

189 
(* Now the all important result is trivially proved! *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

190 
Goal "(f > L) = (f NS> L)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

191 
by (blast_tac (claset() addIs [LIMSEQ_NSLIMSEQ,NSLIMSEQ_LIMSEQ]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

192 
qed "LIMSEQ_NSLIMSEQ_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

193 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

194 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

195 
Theorems about sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

196 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

197 
Goalw [NSLIMSEQ_def] "(%n. k) NS> k"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

198 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

199 
qed "NSLIMSEQ_const"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

200 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

201 
Goalw [LIMSEQ_def] "(%n. k) > k"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

202 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

203 
qed "LIMSEQ_const"; 
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 
Goalw [NSLIMSEQ_def] 
10699  206 
"[ X NS> a; Y NS> b ] ==> (%n. X n + Y n) NS> a + b"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

207 
by (auto_tac (claset() addIs [inf_close_add], 
10720  208 
simpset() addsimps [starfunNat_add RS sym])); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

209 
qed "NSLIMSEQ_add"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

210 

10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

211 
Goal "[ X > a; Y > b ] ==> (%n. X n + Y n) > a + b"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

212 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
10720  213 
NSLIMSEQ_add]) 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

214 
qed "LIMSEQ_add"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

215 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

216 
Goalw [NSLIMSEQ_def] 
10699  217 
"[ X NS> a; Y NS> b ] ==> (%n. X n * Y n) NS> a * b"; 
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

218 
by (auto_tac (claset() addSIs [inf_close_mult_HFinite], 
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

219 
simpset() addsimps [hypreal_of_real_mult, starfunNat_mult RS sym])); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

220 
qed "NSLIMSEQ_mult"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

221 

10699  222 
Goal "[ X > a; Y > b ] ==> (%n. X n * Y n) > a * b"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

223 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
10699  224 
NSLIMSEQ_mult]) 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

225 
qed "LIMSEQ_mult"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

226 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

227 
Goalw [NSLIMSEQ_def] 
10699  228 
"X NS> a ==> (%n. (X n)) NS> a"; 
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

229 
by (auto_tac (claset(), simpset() addsimps [starfunNat_minus RS sym])); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

230 
qed "NSLIMSEQ_minus"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

231 

10677  232 
Goal "X > a ==> (%n. (X n)) > a"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

233 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
10699  234 
NSLIMSEQ_minus]) 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

235 
qed "LIMSEQ_minus"; 
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 
Goal "(%n. (X n)) > a ==> X > a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

238 
by (dtac LIMSEQ_minus 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

239 
by (Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

240 
qed "LIMSEQ_minus_cancel"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

241 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

242 
Goal "(%n. (X n)) NS> a ==> X NS> a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

243 
by (dtac NSLIMSEQ_minus 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

244 
by (Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

245 
qed "NSLIMSEQ_minus_cancel"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

246 

10677  247 
Goal "[ X NS> a; Y NS> b ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

248 
\ ==> (%n. X n + Y n) NS> a + b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

249 
by (dres_inst_tac [("X","Y")] NSLIMSEQ_minus 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

250 
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_add])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

251 
qed "NSLIMSEQ_add_minus"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

252 

10677  253 
Goal "[ X > a; Y > b ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

254 
\ ==> (%n. X n + Y n) > a + b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

255 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

256 
NSLIMSEQ_add_minus]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

257 
qed "LIMSEQ_add_minus"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

258 

10677  259 
Goalw [real_diff_def] 
260 
"[ X > a; Y > b ] ==> (%n. X n  Y n) > a  b"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

261 
by (blast_tac (claset() addIs [LIMSEQ_add_minus]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

262 
qed "LIMSEQ_diff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

263 

10677  264 
Goalw [real_diff_def] 
265 
"[ X NS> a; Y NS> b ] ==> (%n. X n  Y n) NS> a  b"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

266 
by (blast_tac (claset() addIs [NSLIMSEQ_add_minus]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

267 
qed "NSLIMSEQ_diff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

268 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

269 
(* 
10677  270 
Proof is like that of NSLIM_inverse. 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

271 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

272 
Goalw [NSLIMSEQ_def] 
10677  273 
"[ X NS> a; a ~= #0 ] ==> (%n. inverse(X n)) NS> inverse(a)"; 
274 
by (Clarify_tac 1); 

275 
by (dtac bspec 1); 

10720  276 
by (auto_tac (claset(), 
277 
simpset() addsimps [starfunNat_inverse RS sym, 

278 
hypreal_of_real_inf_close_inverse])); 

10607  279 
qed "NSLIMSEQ_inverse"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

280 

10677  281 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

282 
(* Standard version of theorem *) 
10677  283 
Goal "[ X > a; a ~= #0 ] ==> (%n. inverse(X n)) > inverse(a)"; 
10607  284 
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_inverse, 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

285 
LIMSEQ_NSLIMSEQ_iff]) 1); 
10607  286 
qed "LIMSEQ_inverse"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

287 

10712  288 
Goal "[ X NS> a; Y NS> b; b ~= #0 ] \ 
289 
\ ==> (%n. X n / Y n) NS> a/b"; 

290 
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_mult, NSLIMSEQ_inverse, 

291 
real_divide_def]) 1); 

10607  292 
qed "NSLIMSEQ_mult_inverse"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

293 

10712  294 
Goal "[ X > a; Y > b; b ~= #0 ] ==> (%n. X n / Y n) > a/b"; 
295 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_mult, LIMSEQ_inverse, 

296 
real_divide_def]) 1); 

297 
qed "LIMSEQ_divide"; 

10045
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 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

300 
Uniqueness of limit 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

301 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

302 
Goalw [NSLIMSEQ_def] 
10677  303 
"[ X NS> a; X NS> b ] ==> a = b"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

304 
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1)); 
10558  305 
by (auto_tac (claset() addDs [inf_close_trans3], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

306 
qed "NSLIMSEQ_unique"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

307 

10677  308 
Goal "[ X > a; X > b ] ==> a = b"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

309 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

310 
NSLIMSEQ_unique]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

311 
qed "LIMSEQ_unique"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

312 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

313 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

314 
theorems about nslim and lim 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

315 
*) 
10677  316 
Goalw [lim_def] "X > L ==> lim X = L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

317 
by (blast_tac (claset() addIs [LIMSEQ_unique]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

318 
qed "limI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

319 

10677  320 
Goalw [nslim_def] "X NS> L ==> nslim X = L"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

321 
by (blast_tac (claset() addIs [NSLIMSEQ_unique]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

322 
qed "nslimI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

323 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

324 
Goalw [lim_def,nslim_def] "lim X = nslim X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

325 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

326 
qed "lim_nslim_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

327 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

328 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

329 
Convergence 
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 [convergent_def] 
10677  332 
"convergent X ==> EX L. (X > L)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

333 
by (assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

334 
qed "convergentD"; 
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 [convergent_def] 
10677  337 
"(X > L) ==> convergent X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

338 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

339 
qed "convergentI"; 
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 
Goalw [NSconvergent_def] 
10677  342 
"NSconvergent X ==> EX L. (X NS> L)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

343 
by (assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

344 
qed "NSconvergentD"; 
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 
Goalw [NSconvergent_def] 
10677  347 
"(X NS> L) ==> NSconvergent X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

348 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

349 
qed "NSconvergentI"; 
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 
Goalw [convergent_def,NSconvergent_def] 
10677  352 
"convergent X = NSconvergent X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

353 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

354 
qed "convergent_NSconvergent_iff"; 
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 [NSconvergent_def,nslim_def] 
10677  357 
"NSconvergent X = (X NS> nslim X)"; 
10558  358 
by (auto_tac (claset() addIs [someI], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

359 
qed "NSconvergent_NSLIMSEQ_iff"; 
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 
Goalw [convergent_def,lim_def] 
10677  362 
"convergent X = (X > lim X)"; 
10558  363 
by (auto_tac (claset() addIs [someI], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

364 
qed "convergent_LIMSEQ_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

365 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

366 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

367 
Subsequence (alternative definition) (e.g. Hoskins) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

368 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

369 
Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))"; 
10558  370 
by (auto_tac (claset() addSDs [less_imp_Suc_add], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

371 
by (nat_ind_tac "k" 1); 
10558  372 
by (auto_tac (claset() addIs [less_trans], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

373 
qed "subseq_Suc_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

374 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

375 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

376 
Monotonicity 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

377 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

378 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

379 
Goalw [monoseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

380 
"monoseq X = ((ALL n. X n <= X (Suc n)) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

381 
\  (ALL n. X (Suc n) <= X n))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

382 
by (auto_tac (claset () addSDs [le_imp_less_or_eq], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

383 
simpset() addsimps [real_le_refl])); 
10558  384 
by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
385 
addSDs [less_imp_Suc_add], 

386 
simpset())); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

387 
by (induct_tac "ka" 1); 
10558  388 
by (auto_tac (claset() addIs [real_le_trans], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

389 
by (EVERY1[rtac ccontr, rtac swap, Simp_tac]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

390 
by (induct_tac "k" 1); 
10558  391 
by (auto_tac (claset() addIs [real_le_trans], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

392 
qed "monoseq_Suc"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

393 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

394 
Goalw [monoseq_def] 
10677  395 
"ALL m n. m <= n > X m <= X n ==> monoseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

396 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

397 
qed "monoI1"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

398 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

399 
Goalw [monoseq_def] 
10677  400 
"ALL m n. m <= n > X n <= X m ==> monoseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

401 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

402 
qed "monoI2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

403 

10677  404 
Goal "ALL n. X n <= X (Suc n) ==> monoseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

405 
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

406 
qed "mono_SucI1"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

407 

10677  408 
Goal "ALL n. X (Suc n) <= X n ==> monoseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

409 
by (asm_simp_tac (simpset() addsimps [monoseq_Suc]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

410 
qed "mono_SucI2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

411 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

412 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

413 
Bounded Sequence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

414 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

415 
Goalw [Bseq_def] 
10677  416 
"Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

417 
by (assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

418 
qed "BseqD"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

419 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

420 
Goalw [Bseq_def] 
10677  421 
"[ #0 < K; ALL n. abs(X n) <= K ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

422 
\ ==> Bseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

423 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

424 
qed "BseqI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

425 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

426 
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

427 
\ (EX N. ALL n. abs(X n) <= real_of_posnat N)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

428 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

429 
(map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

430 
by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

431 
by (blast_tac (claset() addIs [real_le_less_trans, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

432 
real_less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

433 
by (auto_tac (claset(),simpset() addsimps [real_of_posnat_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

434 
qed "lemma_NBseq_def"; 
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 
(* alternative definition for Bseq *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

437 
Goalw [Bseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

438 
"Bseq X = (EX N. ALL n. abs(X n) <= real_of_posnat N)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

439 
by (simp_tac (simpset() addsimps [lemma_NBseq_def]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

440 
qed "Bseq_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

441 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

442 
Goal "(EX K. #0 < K & (ALL n. abs(X n) <= K)) = \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

443 
\ (EX N. ALL n. abs(X n) < real_of_posnat N)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

444 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

445 
(map rename_numerals) [real_gt_zero_preal_Ex,real_of_posnat_gt_zero])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

446 
by (cut_inst_tac [("x","real_of_preal y")] reals_Archimedean2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

447 
by (blast_tac (claset() addIs [real_less_trans, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

448 
real_le_less_trans]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

449 
by (auto_tac (claset() addIs [real_less_imp_le], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

450 
simpset() addsimps [real_of_posnat_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

451 
qed "lemma_NBseq_def2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

452 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

453 
(* yet another definition for Bseq *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

454 
Goalw [Bseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

455 
"Bseq X = (EX N. ALL n. abs(X n) < real_of_posnat N)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

456 
by (simp_tac (simpset() addsimps [lemma_NBseq_def2]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

457 
qed "Bseq_iff1a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

458 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

459 
Goalw [NSBseq_def] 
10677  460 
"[ NSBseq X; N: HNatInfinite ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

461 
\ ==> (*fNat* X) N : HFinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

462 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

463 
qed "NSBseqD"; 
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 
Goalw [NSBseq_def] 
10677  466 
"ALL N: HNatInfinite. (*fNat* X) N : HFinite \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

467 
\ ==> NSBseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

468 
by (assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

469 
qed "NSBseqI"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

470 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

471 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

472 
Standard definition ==> NS definition 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

473 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

474 
(* a few lemmas *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

475 
Goal "ALL n. abs(X n) <= K ==> \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

476 
\ ALL n. abs(X((f::nat=>nat) n)) <= K"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

477 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

478 
val lemma_Bseq = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

479 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

480 
Goalw [Bseq_def,NSBseq_def] "Bseq X ==> NSBseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

481 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

482 
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

483 
by (auto_tac (claset(),simpset() addsimps [starfunNat, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

484 
HFinite_FreeUltrafilterNat_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

485 
HNatInfinite_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

486 
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

487 
by (dres_inst_tac [("f","Xa")] lemma_Bseq 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

488 
by (res_inst_tac [("x","K+#1")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

489 
by (rotate_tac 2 1 THEN dtac FreeUltrafilterNat_all 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

490 
by (Ultra_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

491 
qed "Bseq_NSBseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

492 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

493 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

494 
NS definition ==> Standard definition 
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 
(* similar to NSLIM proof in REALTOPOS *) 
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 
We need to get rid of the real variable and do so by proving the 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

499 
following which relies on the Archimedean property of the reals 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

500 
When we skolemize we then get the required function f::nat=>nat 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

501 
o/w we would be stuck with a skolem function f :: real=>nat which 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

502 
is not what we want (read useless!) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

503 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

504 

10677  505 
Goal "ALL K. #0 < K > (EX n. K < abs (X n)) \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

506 
\ ==> ALL N. EX n. real_of_posnat N < abs (X n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

507 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

508 
by (cut_inst_tac [("n","N")] (rename_numerals real_of_posnat_gt_zero) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

509 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

510 
val lemmaNSBseq = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

511 

10677  512 
Goal "ALL K. #0 < K > (EX n. K < abs (X n)) \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

513 
\ ==> EX f. ALL N. real_of_posnat N < abs (X (f N))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

514 
by (dtac lemmaNSBseq 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

515 
by (dtac choice 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

516 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

517 
val lemmaNSBseq2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

518 

10677  519 
Goal "ALL N. real_of_posnat N < abs (X (f N)) \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

520 
\ ==> Abs_hypreal(hyprel^^{X o f}) : HInfinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

521 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

522 
[HInfinite_FreeUltrafilterNat_iff,o_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

523 
by (EVERY[rtac bexI 1, rtac lemma_hyprel_refl 2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

524 
Step_tac 1]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

525 
by (cut_inst_tac [("u","u")] FreeUltrafilterNat_nat_gt_real 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

526 
by (blast_tac (claset() addDs [FreeUltrafilterNat_all, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

527 
FreeUltrafilterNat_Int] addIs [real_less_trans, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

528 
FreeUltrafilterNat_subset]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

529 
qed "real_seq_to_hypreal_HInfinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

530 

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 
Now prove that we can get out an infinite hypernatural as well 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

533 
defined using the skolem function f::nat=>nat above 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

534 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

535 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

536 
Goal "{n. f n <= Suc u & real_of_posnat n < abs (X (f n))} <= \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

537 
\ {n. f n <= u & real_of_posnat n < abs (X (f n))} \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

538 
\ Un {n. real_of_posnat n < abs (X (Suc u))}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

539 
by (auto_tac (claset() addSDs [le_imp_less_or_eq] addIs [less_imp_le], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

540 
simpset() addsimps [less_Suc_eq])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

541 
val lemma_finite_NSBseq = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

542 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

543 
Goal "finite {n. f n <= (u::nat) & real_of_posnat n < abs(X(f n))}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

544 
by (induct_tac "u" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

545 
by (rtac (CLAIM "{n. f n <= (0::nat) & real_of_posnat n < abs (X (f n))} <= \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

546 
\ {n. real_of_posnat n < abs (X 0)}" 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

547 
RS finite_subset) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

548 
by (rtac finite_real_of_posnat_less_real 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

549 
by (rtac (lemma_finite_NSBseq RS finite_subset) 1); 
10558  550 
by (auto_tac (claset() addIs [finite_real_of_posnat_less_real], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

551 
val lemma_finite_NSBseq2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

552 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

553 
Goal "ALL N. real_of_posnat N < abs (X (f N)) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

554 
\ ==> Abs_hypnat(hypnatrel^^{f}) : HNatInfinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

555 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

556 
[HNatInfinite_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

557 
by (EVERY[rtac bexI 1, rtac lemma_hypnatrel_refl 2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

558 
Step_tac 1]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

559 
by (rtac ccontr 1 THEN dtac FreeUltrafilterNat_Compl_mem 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

560 
by (asm_full_simp_tac (simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

561 
[CLAIM_SIMP " {n. u < (f::nat=>nat) n} \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

562 
\ = {n. f n <= u}" [le_def]]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

563 
by (dtac FreeUltrafilterNat_all 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

564 
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

565 
by (auto_tac (claset(),simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

566 
[CLAIM "({n. f n <= u} Int {n. real_of_posnat n < abs(X(f n))}) = \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

567 
\ {n. f n <= (u::nat) & real_of_posnat n < abs(X(f n))}", 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

568 
lemma_finite_NSBseq2 RS FreeUltrafilterNat_finite])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

569 
qed "HNatInfinite_skolem_f"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

570 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

571 
Goalw [Bseq_def,NSBseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

572 
"NSBseq X ==> Bseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

573 
by (rtac ccontr 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

574 
by (auto_tac (claset(),simpset() addsimps [real_le_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

575 
by (dtac lemmaNSBseq2 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

576 
by (forw_inst_tac [("X","X"),("f","f")] real_seq_to_hypreal_HInfinite 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

577 
by (dtac (HNatInfinite_skolem_f RSN (2,bspec)) 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

578 
by (auto_tac (claset(),simpset() addsimps [starfunNat, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

579 
o_def,HFinite_HInfinite_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

580 
qed "NSBseq_Bseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

581 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

582 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

583 
Equivalence of nonstandard and standard definitions 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

584 
for a bounded sequence 
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 "(Bseq X) = (NSBseq X)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

587 
by (blast_tac (claset() addSIs [NSBseq_Bseq,Bseq_NSBseq]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

588 
qed "Bseq_NSBseq_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

589 

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 
A convergent sequence is bounded 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

592 
(Boundedness as a necessary condition for convergence) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

593 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

594 
(* easier  nonstandard version  no existential as usual *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

595 
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
10677  596 
"NSconvergent X ==> NSBseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

597 
by (blast_tac (claset() addDs [HFinite_hypreal_of_real RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

598 
(inf_close_sym RSN (2,inf_close_HFinite))]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

599 
qed "NSconvergent_NSBseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

600 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

601 
(* standard version  easily now proved using *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

602 
(* equivalence of NS and standard definitions *) 
10677  603 
Goal "convergent X ==> Bseq X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

604 
by (asm_full_simp_tac (simpset() addsimps [NSconvergent_NSBseq, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

605 
convergent_NSconvergent_iff,Bseq_NSBseq_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

606 
qed "convergent_Bseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

607 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

608 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

609 
Results about Ubs and Lubs of bounded sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

610 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

611 
Goalw [Bseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

612 
"!!(X::nat=>real). Bseq X ==> \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

613 
\ EX U. isUb (UNIV::real set) {x. EX n. X n = x} U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

614 
by (auto_tac (claset() addIs [isUbI,setleI], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

615 
simpset() addsimps [abs_le_interval_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

616 
qed "Bseq_isUb"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

617 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

618 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

619 
Use completeness of reals (supremum property) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

620 
to show that any bounded sequence has a lub 
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 
Goal 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

623 
"!!(X::nat=>real). Bseq X ==> \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

624 
\ EX U. isLub (UNIV::real set) {x. EX n. X n = x} U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

625 
by (blast_tac (claset() addIs [reals_complete, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

626 
Bseq_isUb]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

627 
qed "Bseq_isLub"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

628 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

629 
(* nonstandard version of premise will be *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

630 
(* handy when we work in NS universe *) 
10677  631 
Goal "NSBseq X ==> \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

632 
\ EX U. isUb (UNIV::real set) {x. EX n. X n = x} U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

633 
by (asm_full_simp_tac (simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

634 
[Bseq_NSBseq_iff RS sym,Bseq_isUb]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

635 
qed "NSBseq_isUb"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

636 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

637 
Goal 
10677  638 
"NSBseq X ==> \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

639 
\ EX U. isLub (UNIV::real set) {x. EX n. X n = x} U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

640 
by (asm_full_simp_tac (simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

641 
[Bseq_NSBseq_iff RS sym,Bseq_isLub]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

642 
qed "NSBseq_isLub"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

643 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

644 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

645 
Bounded and monotonic sequence converges 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

646 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

647 
(* lemmas *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

648 
Goal 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

649 
"!!(X::nat=>real). [ ALL m n. m <= n > X m <= X n; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

650 
\ isLub (UNIV::real set) {x. EX n. X n = x} (X ma) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

651 
\ ] ==> ALL n. ma <= n > X n = X ma"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

652 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

653 
by (dres_inst_tac [("y","X n")] isLubD2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

654 
by (ALLGOALS(blast_tac (claset() addDs [real_le_anti_sym]))); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

655 
val lemma_converg1 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

656 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

657 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

658 
The best of both world: Easier to prove this result as a standard 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

659 
theorem and then use equivalence to "transfer" it into the 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

660 
equivalent nonstandard form if needed! 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

661 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

662 
Goalw [LIMSEQ_def] 
10677  663 
"ALL n. m <= n > X n = X m \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

664 
\ ==> EX L. (X > L)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

665 
by (res_inst_tac [("x","X m")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

666 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

667 
by (res_inst_tac [("x","m")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

668 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

669 
by (dtac spec 1 THEN etac impE 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

670 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

671 
qed "Bmonoseq_LIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

672 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

673 
(* Now same theorem in terms of NS limit *) 
10677  674 
Goal "ALL n. m <= n > X n = X m \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

675 
\ ==> EX L. (X NS> L)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

676 
by (auto_tac (claset() addSDs [Bmonoseq_LIMSEQ], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

677 
simpset() addsimps [LIMSEQ_NSLIMSEQ_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

678 
qed "Bmonoseq_NSLIMSEQ"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

679 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

680 
(* a few more lemmas *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

681 
Goal "!!(X::nat=>real). \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

682 
\ [ ALL m. X m ~= U; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

683 
\ isLub UNIV {x. EX n. X n = x} U \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

684 
\ ] ==> ALL m. X m < U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

685 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

686 
by (dres_inst_tac [("y","X m")] isLubD2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

687 
by (auto_tac (claset() addSDs [real_le_imp_less_or_eq], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

688 
simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

689 
val lemma_converg2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

690 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

691 
Goal "!!(X ::nat=>real). ALL m. X m <= U ==> \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

692 
\ isUb UNIV {x. EX n. X n = x} U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

693 
by (rtac (setleI RS isUbI) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

694 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

695 
val lemma_converg3 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

696 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

697 
(* FIXME: U  T < U redundant *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

698 
Goal "!!(X::nat=> real). \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

699 
\ [ ALL m. X m ~= U; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

700 
\ isLub UNIV {x. EX n. X n = x} U; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

701 
\ #0 < T; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

702 
\ U +  T < U \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

703 
\ ] ==> EX m. U + T < X m & X m < U"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

704 
by (dtac lemma_converg2 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

705 
by (rtac ccontr 1 THEN Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

706 
by (fold_tac [real_le_def]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

707 
by (dtac lemma_converg3 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

708 
by (dtac isLub_le_isUb 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

709 
by (auto_tac (claset() addDs [real_less_le_trans], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

710 
simpset() addsimps [real_minus_zero_le_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

711 
val lemma_converg4 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

712 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

713 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

714 
A standard proof of the theorem for monotone increasing sequence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

715 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

716 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

717 
Goalw [convergent_def] 
10677  718 
"[ Bseq X; ALL m n. m <= n > X m <= X n ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

719 
\ ==> convergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

720 
by (forward_tac [Bseq_isLub] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

721 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

722 
by (case_tac "EX m. X m = U" 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

723 
by (blast_tac (claset() addDs [lemma_converg1, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

724 
Bmonoseq_LIMSEQ]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

725 
(* second case *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

726 
by (res_inst_tac [("x","U")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

727 
by (rtac LIMSEQI 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

728 
by (forward_tac [lemma_converg2] 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

729 
by (dtac lemma_converg4 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

730 
by (res_inst_tac [("x","m")] exI 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

731 
by (subgoal_tac "X m <= X n" 1 THEN Fast_tac 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

732 
by (rotate_tac 3 1 THEN dres_inst_tac [("x","n")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

733 
by (arith_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

734 
qed "Bseq_mono_convergent"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

735 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

736 
(* NS version of theorem *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

737 
Goalw [convergent_def] 
10677  738 
"[ NSBseq X; ALL m n. m <= n > X m <= X n ] \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

739 
\ ==> NSconvergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

740 
by (auto_tac (claset() addIs [Bseq_mono_convergent], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

741 
simpset() addsimps [convergent_NSconvergent_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

742 
Bseq_NSBseq_iff RS sym])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

743 
qed "NSBseq_mono_NSconvergent"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

744 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

745 
Goalw [convergent_def] 
10677  746 
"(convergent X) = (convergent (%n. (X n)))"; 
10558  747 
by (auto_tac (claset() addDs [LIMSEQ_minus], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

748 
by (dtac LIMSEQ_minus 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

749 
qed "convergent_minus_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

750 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

751 
Goalw [Bseq_def] "Bseq (%n. (X n)) = Bseq X"; 
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

752 
by (Asm_full_simp_tac 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

753 
qed "Bseq_minus_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

754 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

755 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

756 
**** main mono theorem **** 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

757 
*) 
10715
c838477b5c18
more tidying, especially to rationalize the simprules
paulson
parents:
10712
diff
changeset

758 
Goalw [monoseq_def] "[ Bseq X; monoseq X ] ==> convergent X"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

759 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

760 
by (rtac (convergent_minus_iff RS ssubst) 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

761 
by (dtac (Bseq_minus_iff RS ssubst) 2); 
10558  762 
by (auto_tac (claset() addSIs [Bseq_mono_convergent], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

763 
qed "Bseq_monoseq_convergent"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

764 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

765 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

766 
A few more equivalence theorems for boundedness 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

767 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

768 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

769 
(*** alternative formulation for boundedness***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

770 
Goalw [Bseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

771 
"Bseq X = (EX k x. #0 < k & (ALL n. abs(X(n) + x) <= k))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

772 
by (Step_tac 1); 
10677  773 
by (res_inst_tac [("x","k + abs(x)")] exI 2); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

774 
by (res_inst_tac [("x","K")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

775 
by (res_inst_tac [("x","0")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

776 
by (Auto_tac); 
10677  777 
by (ALLGOALS (dres_inst_tac [("x","n")] spec)); 
778 
by (ALLGOALS arith_tac); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

779 
qed "Bseq_iff2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

780 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

781 
(*** alternative formulation for boundedness ***) 
10677  782 
Goal "Bseq X = (EX k N. #0 < k & (ALL n. abs(X(n) + X(N)) <= k))"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

783 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

784 
by (asm_full_simp_tac (simpset() addsimps [Bseq_def]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

785 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

786 
by (res_inst_tac [("x","K + abs(X N)")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

787 
by (Auto_tac); 
10677  788 
by (arith_tac 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

789 
by (res_inst_tac [("x","N")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

790 
by (Step_tac 1); 
10677  791 
by (dres_inst_tac [("x","n")] spec 1); 
792 
by (arith_tac 1); 

793 
by (auto_tac (claset(), simpset() addsimps [Bseq_iff2])); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

794 
qed "Bseq_iff3"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

795 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

796 
Goalw [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

797 
by (res_inst_tac [("x","(abs(k) + abs(K)) + #1")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

798 
by (Auto_tac); 
10677  799 
by (dres_inst_tac [("x","n")] spec 2); 
800 
by (ALLGOALS arith_tac); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

801 
qed "BseqI2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

802 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

803 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

804 
Equivalence between NS and standard definitions of Cauchy seqs 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

805 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

806 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

807 
Standard def => NS def 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

808 
*) 
10677  809 
Goal "Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

810 
\ ==> {n. M <= x n} : FreeUltrafilterNat"; 
10677  811 
by (auto_tac (claset(), 
812 
simpset() addsimps [HNatInfinite_FreeUltrafilterNat_iff])); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

813 
by (dres_inst_tac [("x","M")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

814 
by (ultra_tac (claset(),simpset() addsimps [less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

815 
val lemmaCauchy1 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

816 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

817 
Goal "{n. ALL m n. M <= m & M <= (n::nat) > abs (X m +  X n) < u} Int \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

818 
\ {n. M <= xa n} Int {n. M <= x n} <= \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

819 
\ {n. abs (X (xa n) +  X (x n)) < u}"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

820 
by (Blast_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

821 
val lemmaCauchy2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

822 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

823 
Goalw [Cauchy_def,NSCauchy_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

824 
"Cauchy X ==> NSCauchy X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

825 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

826 
by (res_inst_tac [("z","M")] eq_Abs_hypnat 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

827 
by (res_inst_tac [("z","N")] eq_Abs_hypnat 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

828 
by (rtac (inf_close_minus_iff RS iffD2) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

829 
by (rtac (mem_infmal_iff RS iffD1) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

830 
by (auto_tac (claset(),simpset() addsimps [starfunNat, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

831 
hypreal_minus,hypreal_add,Infinitesimal_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

832 
by (EVERY[rtac bexI 1, Auto_tac]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

833 
by (dtac spec 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

834 
by (dres_inst_tac [("M","M")] lemmaCauchy1 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

835 
by (dres_inst_tac [("M","M")] lemmaCauchy1 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

836 
by (res_inst_tac [("x1","xa")] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

837 
(lemmaCauchy2 RSN (2,FreeUltrafilterNat_subset)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

838 
by (rtac FreeUltrafilterNat_Int 1 THEN assume_tac 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

839 
by (auto_tac (claset() addIs [FreeUltrafilterNat_Int, 
10558  840 
FreeUltrafilterNat_Nat_set], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

841 
qed "Cauchy_NSCauchy"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

842 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

843 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

844 
NS def => Standard def  rather long but 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

845 
straightforward proof in this case 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

846 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

847 
Goalw [Cauchy_def,NSCauchy_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

848 
"NSCauchy X ==> Cauchy X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

849 
by (EVERY1[Step_tac, rtac ccontr,Asm_full_simp_tac]); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

850 
by (dtac choice 1 THEN auto_tac (claset(),simpset() 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

851 
addsimps [all_conj_distrib])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

852 
by (dtac choice 1 THEN step_tac (claset() addSDs 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

853 
[all_conj_distrib RS iffD1]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

854 
by (REPEAT(dtac HNatInfinite_NSLIMSEQ 1)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

855 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

856 
by (dres_inst_tac [("x","Abs_hypnat (hypnatrel ^^ {fa})")] bspec 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

857 
THEN auto_tac (claset(),simpset() addsimps [starfunNat])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

858 
by (dtac (inf_close_minus_iff RS iffD1) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

859 
by (dtac (mem_infmal_iff RS iffD2) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

860 
by (auto_tac (claset(),simpset() addsimps [hypreal_minus, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

861 
hypreal_add,Infinitesimal_FreeUltrafilterNat_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

862 
by (dres_inst_tac [("x","e")] spec 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

863 
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

864 
by (dtac (CLAIM "{n. X (f n) +  X (fa n) = Y n} Int \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

865 
\ {n. abs (Y n) < e} <= \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

866 
\ {n. abs (X (f n) +  X (fa n)) < e}" RSN 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

867 
(2,FreeUltrafilterNat_subset)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

868 
by (thin_tac "{n. abs (Y n) < e} : FreeUltrafilterNat" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

869 
by (dtac FreeUltrafilterNat_all 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

870 
by (dtac FreeUltrafilterNat_Int 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

871 
by (asm_full_simp_tac (simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

872 
[CLAIM "{n. abs (X (f n) +  X (fa n)) < e} Int \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

873 
\ {M. ~ abs (X (f M) +  X (fa M)) < e} = {}", 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

874 
FreeUltrafilterNat_empty]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

875 
qed "NSCauchy_Cauchy"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

876 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

877 
(* Equivalence *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

878 
Goal "NSCauchy X = Cauchy X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

879 
by (blast_tac (claset() addSIs[NSCauchy_Cauchy, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

880 
Cauchy_NSCauchy]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

881 
qed "NSCauchy_Cauchy_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

882 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

883 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

884 
Cauchy sequence is bounded  this is the standard 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

885 
proof mechanization rather than the nonstandard proof 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

886 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

887 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

888 
(*** VARIOUS LEMMAS ***) 
10677  889 
Goal "ALL n. M <= n > abs (X M +  X n) < (#1::real) \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

890 
\ ==> ALL n. M <= n > abs(X n) < #1 + abs(X M)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

891 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

892 
by (dtac spec 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

893 
by (arith_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

894 
val lemmaCauchy = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

895 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

896 
Goal "(n < Suc M) = (n <= M)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

897 
by Auto_tac; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

898 
qed "less_Suc_cancel_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

899 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

900 
(* FIXME: Long. Maximal element in subsequence *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

901 
Goal "EX m. m <= M & (ALL n. n <= M > \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

902 
\ abs ((X::nat=> real) n) <= abs (X m))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

903 
by (induct_tac "M" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

904 
by (res_inst_tac [("x","0")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

905 
by (Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

906 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

907 
by (cut_inst_tac [("R1.0","abs (X (Suc n))"),("R2.0","abs(X m)")] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

908 
real_linear 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

909 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

910 
by (res_inst_tac [("x","m")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

911 
by (res_inst_tac [("x","m")] exI 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

912 
by (res_inst_tac [("x","Suc n")] exI 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

913 
by (ALLGOALS(Asm_full_simp_tac)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

914 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

915 
by (ALLGOALS(eres_inst_tac [("m1","na")] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

916 
(le_imp_less_or_eq RS disjE))); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

917 
by (ALLGOALS(asm_full_simp_tac (simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

918 
[real_le_refl,less_Suc_cancel_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

919 
real_less_imp_le]))); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

920 
by (blast_tac (claset() addIs [real_le_less_trans RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

921 
real_less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

922 
qed "SUP_rabs_subseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

923 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

924 
(* lemmas to help proof  mostly trivial *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

925 
Goal "[ ALL m::nat. m <= M > P M m; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

926 
\ ALL m. M <= m > P M m ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

927 
\ ==> ALL m. P M m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

928 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

929 
by (REPEAT(dres_inst_tac [("x","m")] spec 1)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

930 
by (auto_tac (claset() addEs [less_asym], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

931 
simpset() addsimps [le_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

932 
val lemma_Nat_covered = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

933 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

934 
Goal "[ ALL n. n <= M > abs ((X::nat=>real) n) <= a; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

935 
\ a < b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

936 
\ ==> ALL n. n <= M > abs(X n) <= b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

937 
by (blast_tac (claset() addIs [real_le_less_trans RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

938 
real_less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

939 
val lemma_trans1 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

940 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

941 
Goal "[ ALL n. M <= n > abs ((X::nat=>real) n) < a; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

942 
\ a < b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

943 
\ ==> ALL n. M <= n > abs(X n)<= b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

944 
by (blast_tac (claset() addIs [real_less_trans RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

945 
real_less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

946 
val lemma_trans2 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

947 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

948 
Goal "[ ALL n. n <= M > abs (X n) <= a; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

949 
\ a = b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

950 
\ ==> ALL n. n <= M > abs(X n) <= b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

951 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

952 
val lemma_trans3 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

953 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

954 
Goal "ALL n. M <= n > abs ((X::nat=>real) n) < a \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

955 
\ ==> ALL n. M <= n > abs (X n) <= a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

956 
by (blast_tac (claset() addIs [real_less_imp_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

957 
val lemma_trans4 = result(); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

958 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

959 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

960 
Trickier than expected  proof is more involved than 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

961 
outlines sketched by various authors would suggest 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

962 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

963 
Goalw [Cauchy_def,Bseq_def] "Cauchy X ==> Bseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

964 
by (dres_inst_tac [("x","#1")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

965 
by (etac (rename_numerals real_zero_less_one RSN (2,impE)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

966 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

967 
by (dres_inst_tac [("x","M")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

968 
by (Asm_full_simp_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

969 
by (dtac lemmaCauchy 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

970 
by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

971 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

972 
by (cut_inst_tac [("R1.0","abs(X m)"), 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

973 
("R2.0","#1 + abs(X M)")] real_linear 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

974 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

975 
by (dtac lemma_trans1 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

976 
by (dtac lemma_trans2 3 THEN assume_tac 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

977 
by (dtac lemma_trans3 2 THEN assume_tac 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

978 
by (dtac (abs_add_one_gt_zero RS real_less_trans) 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

979 
by (dtac lemma_trans4 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

980 
by (dtac lemma_trans4 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

981 
by (res_inst_tac [("x","#1 + abs(X M)")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

982 
by (res_inst_tac [("x","#1 + abs(X M)")] exI 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

983 
by (res_inst_tac [("x","abs(X m)")] exI 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

984 
by (auto_tac (claset() addSEs [lemma_Nat_covered], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

985 
simpset())); 
10677  986 
by (ALLGOALS arith_tac); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

987 
qed "Cauchy_Bseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

988 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

989 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

990 
Cauchy sequence is bounded  NSformulation 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

991 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

992 
Goal "NSCauchy X ==> NSBseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

993 
by (asm_full_simp_tac (simpset() addsimps [Cauchy_Bseq, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

994 
Bseq_NSBseq_iff RS sym,NSCauchy_Cauchy_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

995 
qed "NSCauchy_NSBseq"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

996 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

997 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

998 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

999 
Equivalence of Cauchy criterion and convergence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1000 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1001 
We will prove this using our NS formulation which provides a 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1002 
much easier proof than using the standard definition. We do not 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1003 
need to use properties of subsequences such as boundedness, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1004 
monotonicity etc... Compare with Harrison's corresponding proof 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1005 
in HOL which is much longer and more complicated. Of course, we do 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1006 
not have problems which he encountered with guessing the right 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1007 
instantiations for his 'espsilondelta' proof(s) in this case 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1008 
since the NS formulations do not involve existential quantifiers. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1009 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1010 
Goalw [NSconvergent_def,NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1011 
"NSCauchy X = NSconvergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1012 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1013 
by (forward_tac [NSCauchy_NSBseq] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1014 
by (auto_tac (claset() addIs [inf_close_trans2], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1015 
simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1016 
[NSBseq_def,NSCauchy_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1017 
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1018 
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1); 
10558  1019 
by (auto_tac (claset() addSDs [st_part_Ex], simpset() 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1020 
addsimps [SReal_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1021 
by (blast_tac (claset() addIs [inf_close_trans3]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1022 
qed "NSCauchy_NSconvergent_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1023 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1024 
(* Standard proof for free *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1025 
Goal "Cauchy X = convergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1026 
by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1027 
convergent_NSconvergent_iff, NSCauchy_NSconvergent_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1028 
qed "Cauchy_convergent_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1029 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1030 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1031 
We can now try and derive a few properties of sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1032 
starting with the limit comparison property for sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1033 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1034 
Goalw [NSLIMSEQ_def] 
10677  1035 
"[ f NS> l; g NS> m; \ 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1036 
\ EX N. ALL n. N <= n > f(n) <= g(n) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1037 
\ ] ==> l <= m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1038 
by (Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1039 
by (dtac starfun_le_mono 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1040 
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1041 
by (dres_inst_tac [("x","whn")] spec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1042 
by (REPEAT(dtac (bex_Infinitesimal_iff2 RS iffD2) 1)); 
10721  1043 
by Auto_tac; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1044 
by (auto_tac (claset() addIs 
10558  1045 
[hypreal_of_real_le_add_Infininitesimal_cancel2], simpset())); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1046 
qed "NSLIMSEQ_le"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1047 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1048 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1049 
Goal "[ f > l; g > m; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1050 
\ EX N. ALL n. N <= n > f(n) <= g(n) ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1051 
\ ==> l <= m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1052 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1053 
NSLIMSEQ_le]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1054 
qed "LIMSEQ_le"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1055 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1056 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1057 
Also... 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1058 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1059 
Goal "[ X > r; ALL n. a <= X n ] ==> a <= r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1060 
by (rtac LIMSEQ_le 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1061 
by (rtac LIMSEQ_const 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1062 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1063 
qed "LIMSEQ_le_const"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1064 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1065 
Goal "[ X NS> r; ALL n. a <= X n ] ==> a <= r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1066 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1067 
LIMSEQ_le_const]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1068 
qed "NSLIMSEQ_le_const"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1069 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1070 
Goal "[ X > r; ALL n. X n <= a ] ==> r <= a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1071 
by (rtac LIMSEQ_le 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1072 
by (rtac LIMSEQ_const 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1073 
by (Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1074 
qed "LIMSEQ_le_const2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1075 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1076 
Goal "[ X NS> r; ALL n. X n <= a ] ==> r <= a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1077 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1078 
LIMSEQ_le_const2]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1079 
qed "NSLIMSEQ_le_const2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1080 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1081 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1082 
Shift a convergent series by 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1083 
We use the fact that Cauchyness and convergence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1084 
are equivalent and also that the successor of an 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1085 
infinite hypernatural is also infinite. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1086 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1087 
Goal "f NS> l ==> (%n. f(Suc n)) NS> l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1088 
by (forward_tac [NSconvergentI RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1089 
(NSCauchy_NSconvergent_iff RS iffD2)] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1090 
by (auto_tac (claset(),simpset() addsimps [NSCauchy_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1091 
NSLIMSEQ_def,starfunNat_shift_one])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1092 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1093 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1094 
by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1095 
by (blast_tac (claset() addIs [inf_close_trans3]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1096 
qed "NSLIMSEQ_Suc"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1097 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1098 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1099 
Goal "f > l ==> (%n. f(Suc n)) > l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1100 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1101 
NSLIMSEQ_Suc]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1102 
qed "LIMSEQ_Suc"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1103 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1104 
Goal "(%n. f(Suc n)) NS> l ==> f NS> l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1105 
by (forward_tac [NSconvergentI RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1106 
(NSCauchy_NSconvergent_iff RS iffD2)] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1107 
by (auto_tac (claset(),simpset() addsimps [NSCauchy_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1108 
NSLIMSEQ_def,starfunNat_shift_one])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1109 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1110 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1111 
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1112 
by (rotate_tac 2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1113 
by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1114 
simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1115 
qed "NSLIMSEQ_imp_Suc"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1116 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1117 
Goal "(%n. f(Suc n)) > l ==> f > l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1118 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1119 
by (etac NSLIMSEQ_imp_Suc 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1120 
qed "LIMSEQ_imp_Suc"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1121 

10648  1122 
Goal "((%n. f(Suc n)) > l) = (f > l)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1123 
by (blast_tac (claset() addIs [LIMSEQ_imp_Suc,LIMSEQ_Suc]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1124 
qed "LIMSEQ_Suc_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1125 

10648  1126 
Goal "((%n. f(Suc n)) NS> l) = (f NS> l)"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1127 
by (blast_tac (claset() addIs [NSLIMSEQ_imp_Suc,NSLIMSEQ_Suc]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1128 
qed "NSLIMSEQ_Suc_iff"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1129 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1130 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1131 
A sequence tends to zero iff its abs does 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1132 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1133 
(* we can prove this directly since proof is trivial *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1134 
Goalw [LIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1135 
"((%n. abs(f n)) > #0) = (f > #0)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1136 
by (simp_tac (simpset() addsimps [abs_idempotent]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1137 
qed "LIMSEQ_rabs_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1138 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1139 
(**) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1140 
(* We prove the NS version from the standard one *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1141 
(* Actually pure NS proof seems more complicated *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1142 
(* than the direct standard one above! *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1143 
(**) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1144 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1145 
Goal "((%n. abs(f n)) NS> #0) = (f NS> #0)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1146 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1147 
LIMSEQ_rabs_zero]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1148 
qed "NSLIMSEQ_rabs_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1149 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1150 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1151 
Also we have for a general limit 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1152 
(NS proof much easier) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1153 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1154 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1155 
"f NS> l ==> (%n. abs(f n)) NS> abs(l)"; 
10558  1156 
by (auto_tac (claset() addIs [inf_close_hrabs], simpset() 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1157 
addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1158 
qed "NSLIMSEQ_imp_rabs"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1159 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1160 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1161 
Goal "f > l ==> (%n. abs(f n)) > abs(l)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1162 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1163 
NSLIMSEQ_imp_rabs]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1164 
qed "LIMSEQ_imp_rabs"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1165 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1166 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1167 
An unbounded sequence's inverse tends to 0 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1168 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1169 
(* standard proof seems easier *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1170 
Goalw [LIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1171 
"ALL y. EX N. ALL n. N <= n > y < f(n) \ 
10607  1172 
\ ==> (%n. inverse(f n)) > #0"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1173 
by (Step_tac 1 THEN Asm_full_simp_tac 1); 
10607  1174 
by (dres_inst_tac [("x","inverse r")] spec 1 THEN Step_tac 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1175 
by (res_inst_tac [("x","N")] exI 1 THEN Step_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1176 
by (dtac spec 1 THEN Auto_tac); 
10607  1177 
by (forward_tac [rename_numerals real_inverse_gt_zero] 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1178 
by (forward_tac [real_less_trans] 1 THEN assume_tac 1); 
10607  1179 
by (forw_inst_tac [("x","f n")] (rename_numerals real_inverse_gt_zero) 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1180 
by (asm_simp_tac (simpset() addsimps [abs_eqI2]) 1); 
10607  1181 
by (res_inst_tac [("t","r")] (real_inverse_inverse RS subst) 1); 
10648  1182 
by (auto_tac (claset() addIs [real_inverse_less_iff RS iffD2], 
1183 
simpset() delsimps [real_inverse_inverse])); 

10607  1184 
qed "LIMSEQ_inverse_zero"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1185 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1186 
Goal "ALL y. EX N. ALL n. N <= n > y < f(n) \ 
10607  1187 
\ ==> (%n. inverse(f n)) NS> #0"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1188 
by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
10607  1189 
LIMSEQ_inverse_zero]) 1); 
1190 
qed "NSLIMSEQ_inverse_zero"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1191 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1192 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1193 
Sequence 1/n > 0 as n > infinity 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1194 
*) 
10607  1195 
Goal "(%n. inverse(real_of_posnat n)) > #0"; 
1196 
by (rtac LIMSEQ_inverse_zero 1 THEN Step_tac 1); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1197 
by (cut_inst_tac [("x","y")] reals_Archimedean2 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1198 
by (Step_tac 1 THEN res_inst_tac [("x","n")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1199 
by (Step_tac 1 THEN etac (le_imp_less_or_eq RS disjE) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1200 
by (dtac (real_of_posnat_less_iff RS iffD2) 1); 
10558  1201 
by (auto_tac (claset() addEs [real_less_trans], simpset())); 
10607  1202 
qed "LIMSEQ_inverse_real_of_posnat"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1203 

10607  1204 
Goal "(%n. inverse(real_of_posnat n)) NS> #0"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1205 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
10607  1206 
LIMSEQ_inverse_real_of_posnat]) 1); 
1207 
qed "NSLIMSEQ_inverse_real_of_posnat"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1208 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1209 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1210 
Sequence r + 1/n > r as n > infinity 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1211 
now easily proved 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1212 
*) 
10607  1213 
Goal "(%n. r + inverse(real_of_posnat n)) > r"; 
1214 
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat] 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1215 
MRS LIMSEQ_add] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1216 
by (Auto_tac); 
10607  1217 
qed "LIMSEQ_inverse_real_of_posnat_add"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1218 

10607  1219 
Goal "(%n. r + inverse(real_of_posnat n)) NS> r"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1220 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
10607  1221 
LIMSEQ_inverse_real_of_posnat_add]) 1); 
1222 
qed "NSLIMSEQ_inverse_real_of_posnat_add"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1223 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1224 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1225 
Also... 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1226 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1227 

10607  1228 
Goal "(%n. r + inverse(real_of_posnat n)) > r"; 
1229 
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_inverse_real_of_posnat] 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1230 
MRS LIMSEQ_add_minus] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1231 
by (Auto_tac); 
10607  1232 
qed "LIMSEQ_inverse_real_of_posnat_add_minus"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1233 

10607  1234 
Goal "(%n. r + inverse(real_of_posnat n)) NS> r"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1235 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
10607  1236 
LIMSEQ_inverse_real_of_posnat_add_minus]) 1); 
1237 
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1238 

10607  1239 
Goal "(%n. r*( #1 + inverse(real_of_posnat n))) > r"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1240 
by (cut_inst_tac [("b","#1")] ([LIMSEQ_const, 
10607  1241 
LIMSEQ_inverse_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1242 
by (Auto_tac); 
10607  1243 
qed "LIMSEQ_inverse_real_of_posnat_add_minus_mult"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1244 

10607  1245 
Goal "(%n. r*( #1 + inverse(real_of_posnat n))) NS> r"; 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1246 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
10607  1247 
LIMSEQ_inverse_real_of_posnat_add_minus_mult]) 1); 
1248 
qed "NSLIMSEQ_inverse_real_of_posnat_add_minus_mult"; 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1249 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1250 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1251 
Real Powers 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1252 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1253 
Goal "(X NS> a) > ((%n. (X n) ^ m) NS> a ^ m)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1254 
by (induct_tac "m" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1255 
by (auto_tac (claset() addIs [NSLIMSEQ_mult,NSLIMSEQ_const], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1256 
simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1257 
qed_spec_mp "NSLIMSEQ_pow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1258 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1259 
Goal "X > a ==> (%n. (X n) ^ m) > a ^ m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1260 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1261 
NSLIMSEQ_pow]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1262 
qed "LIMSEQ_pow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1263 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1264 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1265 
0 <= x < #1 ==> (x ^ n > 0) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1266 
Proof will use (NS) Cauchy equivalence for convergence and 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1267 
also fact that bounded and monotonic sequence converges. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1268 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1269 
Goalw [Bseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1270 
"[ #0 <= x; x < #1 ] ==> Bseq (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1271 
by (res_inst_tac [("x","#1")] exI 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1272 
by (auto_tac (claset() addDs [conjI RS realpow_le2] 
10558  1273 
addIs [real_less_imp_le], simpset() addsimps 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1274 
[real_zero_less_one,abs_eqI1,realpow_abs RS sym] )); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1275 
qed "Bseq_realpow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1276 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1277 
Goal "[ #0 <= x; x < #1 ] ==> monoseq (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1278 
by (blast_tac (claset() addSIs [mono_SucI2,realpow_Suc_le3]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1279 
qed "monoseq_realpow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1280 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1281 
Goal "[ #0 <= x; x < #1 ] ==> convergent (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1282 
by (blast_tac (claset() addSIs [Bseq_monoseq_convergent, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1283 
Bseq_realpow,monoseq_realpow]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1284 
qed "convergent_realpow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1285 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1286 
(* We now use NS criterion to bring proof of theorem through *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1287 

10720  1288 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1289 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1290 
"[ #0 <= x; x < #1 ] ==> (%n. x ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1291 
by (auto_tac (claset() addSDs [convergent_realpow], 
10712  1292 
simpset() addsimps [convergent_NSconvergent_iff])); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1293 
by (forward_tac [NSconvergentD] 1); 
10712  1294 
by (auto_tac (claset(), 
1295 
simpset() addsimps [NSLIMSEQ_def, NSCauchy_NSconvergent_iff RS sym, 

1296 
NSCauchy_def, starfunNat_pow])); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1297 
by (forward_tac [HNatInfinite_add_one] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1298 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1299 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1300 
by (dres_inst_tac [("x","N + 1hn")] bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1301 
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1302 
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1303 
by (dtac inf_close_trans3 1 THEN assume_tac 1); 
10712  1304 
by (auto_tac (claset(), 
10720  1305 
simpset() delsimps [hypreal_of_real_mult] 
1306 
addsimps [hypreal_of_real_mult RS sym])); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1307 
qed "NSLIMSEQ_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1308 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1309 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1310 
Goal "[ #0 <= x; x < #1 ] ==> (%n. x ^ n) > #0"; 
10712  1311 
by (asm_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero, 
1312 
LIMSEQ_NSLIMSEQ_iff]) 1); 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1313 
qed "LIMSEQ_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1314 

10712  1315 
Goal "#1 < x ==> (%n. a / (x ^ n)) > #0"; 
1316 
by (cut_inst_tac [("a","a"),("x1","inverse x")] 

1317 
([LIMSEQ_const, LIMSEQ_realpow_zero] MRS LIMSEQ_mult) 1); 

1318 
by (auto_tac (claset(), 

1319 
simpset() addsimps [real_divide_def, realpow_inverse])); 

1320 
by (asm_simp_tac (simpset() addsimps [real_inverse_eq_divide, 

1321 
pos_real_divide_less_eq]) 1); 

1322 
qed "LIMSEQ_divide_realpow_zero"; 

1323 

10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1324 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1325 
Limit of c^n for c < 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1326 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1327 
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1328 
by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1329 
qed "LIMSEQ_rabs_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1330 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1331 
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1332 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1333 
LIMSEQ_NSLIMSEQ_iff RS sym]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1334 
qed "NSLIMSEQ_rabs_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1335 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1336 
Goal "abs(c) < #1 ==> (%n. c ^ n) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1337 
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1338 
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero], 
10712  1339 
simpset() addsimps [realpow_abs RS sym])); 
10045
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1340 
qed "LIMSEQ_rabs_realpow_zero2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1341 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1342 
Goal "abs(c) < #1 ==> (%n. c ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1343 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1344 
LIMSEQ_NSLIMSEQ_iff RS sym]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1345 
qed "NSLIMSEQ_rabs_realpow_zero2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1346 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1347 
(*** 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1348 
Hyperreals and Sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1349 
***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1350 
(*** A bounded sequence is a finite hyperreal ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1351 
Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1352 
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1353 
[FreeUltrafilterNat_all RS FreeUltrafilterNat_subset], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1354 
simpset() addsimps [HFinite_FreeUltrafilterNat_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1355 
Bseq_NSBseq_iff RS sym, Bseq_iff1a])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1356 
qed "NSBseq_HFinite_hypreal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1357 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1358 
(*** A sequence converging to zero defines an infinitesimal ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1359 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1360 
"X NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1361 
by (dres_inst_tac [("x","whn")] bspec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1362 
by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1); 