author  fleuriot 
Thu, 21 Sep 2000 12:17:11 +0200  
changeset 10045  c76b73e16711 
child 10558  09a91221ced1 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

14 
"(*fNat* (%n::nat. rinv(real_of_posnat n))) whn : Infinitesimal"; 
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) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

19 
[real_of_posnat_gt_zero,real_rinv_gt_zero,abs_eqI2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

20 
FreeUltrafilterNat_rinv_real_of_posnat])); 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

29 
"!!X. X > L ==> \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

35 
"!!X. [ X > L; #0 < r] ==> \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

41 
"!!X. ALL r. #0 < r > (EX no. ALL n. \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

47 
"!!X. (X > L) = \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

54 
"!!X. X NS> L ==> ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L"; 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

59 
"!!X. [ X NS> L; N: HNatInfinite ] ==> (*fNat* X) N @= hypreal_of_real L"; 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

64 
"!!X. ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L ==> X NS> L"; 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

69 
"!!X. (X NS> L) = (ALL N: HNatInfinite. (*fNat* X) N @= hypreal_of_real L)"; 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

77 
"!!X. X > L ==> X NS> L"; 
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), 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

123 
finite_nat_le_segment],simpset())); 
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! *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

143 
Goal "!!f. ALL n. n <= f n \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

156 
addIs [real_less_irrefl],simpset())); 
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 

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

159 
Goal "!!f. [ #0 < r; ALL n. r <= abs (X (f n) +  L); \ 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

177 
"!!X. X NS> L ==> X > L"; 
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] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

206 
"!!X. [ X NS> a; Y NS> b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

209 
simpset() addsimps [starfunNat_add RS sym,hypreal_of_real_add])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

211 

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

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

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

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

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

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

217 

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

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

219 
"!!X. [ X NS> a; Y NS> b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

221 
by (auto_tac (claset() addSIs [starfunNat_mult_HFinite_inf_close], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

224 

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

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

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

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

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

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

230 

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

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

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

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

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

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

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

237 

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

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

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

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

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

242 

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

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

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

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

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

247 

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

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

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

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

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

252 

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

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

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

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

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

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

258 

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

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

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

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

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

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

264 

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

265 
goalw SEQ.thy [real_diff_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

266 
"!!X. [ X > a; Y > b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

270 

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

271 
goalw SEQ.thy [real_diff_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

272 
"!!X. [ X NS> a; Y NS> b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

276 

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

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

278 
Proof is exactly same as that of NSLIM_rinv except 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

279 
for starfunNat_hrinv2  would not be the case if we 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

280 
had generalised net theorems for example. Not our 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

281 
real concern though. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

284 
"!!X. [ X NS> a; a ~= #0 ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

288 
addsimps [hypreal_of_real_not_zero_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

290 
by (forward_tac [inf_close_hypreal_of_real_not_zero] 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

291 
THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

292 
by (auto_tac (claset() addSEs [(starfunNat_hrinv2 RS subst), 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

293 
inf_close_hrinv,hypreal_of_real_HFinite_diff_Infinitesimal], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

296 

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

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

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

299 
"!!X. [ X > a; a ~= #0 ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

304 

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

305 
(* trivially proved *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

307 
"!!X. [ X NS> a; Y NS> b; b ~= #0 ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

311 

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

312 
(* let's give a standard proof of theorem *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

314 
"!!X. [ X > a; Y > b; b ~= #0 ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

318 

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

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

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

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

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

323 
"!!X. [ X NS> a; X NS> b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

324 
\ ==> a = b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

325 
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

326 
by (auto_tac (claset() addDs [inf_close_trans3],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

327 
qed "NSLIMSEQ_unique"; 
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 
Goal "!!X. [ X > a; X > b ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

330 
\ ==> a = b"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

334 

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 
theorems about nslim and lim 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

338 
Goalw [lim_def] "!!X. X > L ==> lim X = L"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

341 

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

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

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

344 
qed "nslimI"; 
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 [lim_def,nslim_def] "lim X = nslim X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

349 

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

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

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

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

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

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

357 

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

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

359 
"!!f. (X > L) ==> convergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

362 

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

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

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

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

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

367 

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

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

369 
"!!f. (X NS> L) ==> NSconvergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

372 

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

373 
Goalw [convergent_def,NSconvergent_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

374 
"convergent X = NSconvergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

376 
qed "convergent_NSconvergent_iff"; 
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 
Goalw [NSconvergent_def,nslim_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

379 
"NSconvergent X = (X NS> nslim X)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

380 
by (auto_tac (claset() addIs [someI],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

382 

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

383 
Goalw [convergent_def,lim_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

384 
"convergent X = (X > lim X)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

385 
by (auto_tac (claset() addIs [someI],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

387 

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

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

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

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

391 
Goalw [subseq_def] "subseq f = (ALL n. (f n) < (f (Suc n)))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

392 
by (auto_tac (claset() addSDs [less_eq_Suc_add],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

393 
by (nat_ind_tac "k" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

394 
by (auto_tac (claset() addIs [less_trans],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

396 

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

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

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

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

400 

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

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

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

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

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

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

406 
by (auto_tac (claset() addSIs [lessI RS less_imp_le] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

407 
addSDs [less_eq_Suc_add],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

409 
by (auto_tac (claset() addIs [real_le_trans],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

412 
by (auto_tac (claset() addIs [real_le_trans],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

413 
qed "monoseq_Suc"; 
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 [monoseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

416 
"!!X. ALL m n. m <= n > X m <= X n ==> monoseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

418 
qed "monoI1"; 
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 [monoseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

421 
"!!X. ALL m n. m <= n > X n <= X m ==> monoseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

424 

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

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

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

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

428 

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

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

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

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

432 

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

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

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

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

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

437 
"!!X. Bseq X ==> EX K. #0 < K & (ALL n. abs(X n) <= K)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

440 

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

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

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

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

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

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

446 

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

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

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

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

450 
(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

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

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

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

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

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

456 

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

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

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

459 
"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

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

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

462 

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

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

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

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

466 
(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

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

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

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

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

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

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

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

476 
"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

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

478 
qed "Bseq_iff1a"; 
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 [NSBseq_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

481 
"!!X. [ NSBseq X; N: HNatInfinite ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

485 

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

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

487 
"!!X. ALL N: HNatInfinite. (*fNat* X) N : HFinite \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

491 

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

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

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

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

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

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

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

500 

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

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

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

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

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

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

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

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

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

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

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

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

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

513 

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

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

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

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

517 
(* similar to NSLIM proof in REALTOPOS *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

519 
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

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

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

522 
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

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

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

525 

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

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

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

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

529 
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

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

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

532 

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

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

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

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

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

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

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

539 

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

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

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

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

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

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

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

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

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

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

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

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

551 

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

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

553 
Now prove that we can get out an infinite hypernatural as well 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

556 

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

557 
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

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

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

560 
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

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

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

563 

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

564 
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

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

566 
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

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

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

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

570 
by (rtac (lemma_finite_NSBseq RS finite_subset) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

571 
by (auto_tac (claset() addIs [finite_real_of_posnat_less_real],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

573 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

587 
[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

588 
\ {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

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

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

591 

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

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

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

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

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

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

597 
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

598 
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

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

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

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

602 

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

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

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

605 
for a bounded sequence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

607 
Goal "(Bseq X) = (NSBseq X)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

612 
A convergent sequence is bounded 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

616 
Goalw [NSconvergent_def,NSBseq_def,NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

617 
"!!X. NSconvergent X ==> NSBseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

620 
qed "NSconvergent_NSBseq"; 
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 
(* standard version  easily now proved using *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

623 
(* equivalence of NS and standard definitions *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

624 
Goal "!!X. convergent X ==> Bseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

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

634 
\ 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

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

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

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

638 

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

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

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

641 
to show that any bounded sequence has a lub 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

645 
\ 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

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

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

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

649 

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

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

651 
(* handy when we work in NS universe *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

652 
Goal "!!X. NSBseq X ==> \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

653 
\ 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

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

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

656 
qed "NSBseq_isUb"; 
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 
Goal 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

660 
\ 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

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

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

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

664 

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

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

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

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

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

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

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

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

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

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

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

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

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

677 

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

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

679 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

693 

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

694 
(* Now same theorem in terms of NS limit *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

695 
Goal "!!X. ALL n. m <= n > X n = X m \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

700 

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

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

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

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

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

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

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

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

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

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

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

711 

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

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

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

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

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

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

717 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

733 

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

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

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

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

737 

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

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

739 
"!!X. [ Bseq X; ALL m n. m <= n > X m <= X n ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

753 
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

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

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

756 

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

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

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

759 
"!!X. [ NSBseq X; ALL m n. m <= n > X m <= X n ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

764 
qed "NSBseq_mono_NSconvergent"; 
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 
Goalw [convergent_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

767 
"!!X. (convergent X) = (convergent (%n. (X n)))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

768 
by (auto_tac (claset() addDs [LIMSEQ_minus],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

771 

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

772 
Goalw [Bseq_def] "Bseq (%n. (X n)) = Bseq X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

775 

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

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

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

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

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

780 
"!!X. [ Bseq X; monoseq X ] ==> convergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

783 
by (dtac (Bseq_minus_iff RS ssubst) 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

784 
by (auto_tac (claset() addSIs [Bseq_mono_convergent],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

786 

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

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

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

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

790 

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

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

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

793 
"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

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

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

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

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

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

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

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

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

802 
qed "Bseq_iff2"; 
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 
(*** alternative formulation for boundedness ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

805 
Goal "Bseq X = (EX k N. #0 < k & (ALL n. \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

806 
\ abs(X(n) + X(N)) <= k))"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

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

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

815 
by (res_inst_tac [("j","abs(X n) + abs (X N)")] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

820 

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

821 
val real_not_leE = CLAIM "~ m <= n ==> n < (m::real)"; 
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 [Bseq_def] "(ALL n. k <= f n & f n <= K) ==> Bseq f"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

827 
by (case_tac "#0 <= f n" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

829 
real_not_leE RS abs_minus_eqI2])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

830 
by (res_inst_tac [("j","abs K")] real_le_trans 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

831 
by (res_inst_tac [("j","abs k")] real_le_trans 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

832 
by (auto_tac (claset() addSIs [rename_numerals real_le_add_order] addDs 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

833 
[real_le_trans],simpset() 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

834 
addsimps [abs_ge_zero,rename_numerals real_zero_less_one,abs_eqI1])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

835 
by (subgoal_tac "k < 0" 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

836 
by (rtac (real_not_leE RSN (2,real_le_less_trans)) 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

839 

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

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

841 
Equivalence between NS and standard definitions of Cauchy seqs 
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 
Standard def => NS def 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

846 
Goal "!!x. Abs_hypnat (hypnatrel ^^ {x}) : HNatInfinite \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

853 

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

854 
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

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

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

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

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

859 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

879 

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

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

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

882 
straightforward proof in this case 
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 
Goalw [Cauchy_def,NSCauchy_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

901 
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

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

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

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

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

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

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

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

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

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

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

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

913 

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

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

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

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

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

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

919 

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

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

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

922 
proof mechanization rather than the nonstandard proof 
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 

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

925 
(*** VARIOUS LEMMAS ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

927 
\ ==> ALL n. M <= n > abs(X n) < #1 + abs(X 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 (dtac spec 1 THEN Auto_tac); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

932 

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

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

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

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

936 

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

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

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

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

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

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

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

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

944 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

960 

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

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

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

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

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

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

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

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

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

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

970 

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

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

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

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

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

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

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

977 

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

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

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

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

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

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

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

984 

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

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

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

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

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

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

990 

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

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

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

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

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

995 

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 
Trickier than expected  proof is more involved than 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

998 
outlines sketched by various authors would suggest 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1002 
by (etac (rename_numerals real_zero_less_one RSN (2,impE)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

1007 
by (cut_inst_tac [("M","M"),("X","X")] SUP_rabs_subseq 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1010 
("R2.0","#1 + abs(X M)")] real_linear 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1013 
by (dtac lemma_trans2 3 THEN assume_tac 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1014 
by (dtac lemma_trans3 2 THEN assume_tac 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1015 
by (dtac (abs_add_one_gt_zero RS real_less_trans) 3); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1017 
by (dtac lemma_trans4 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1021 
by (auto_tac (claset() addSEs [lemma_Nat_covered], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1024 

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

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

1026 
Cauchy sequence is bounded  NSformulation 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

1032 

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

1035 
Equivalence of Cauchy criterion and convergence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1036 

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

1037 
We will prove this using our NS formulation which provides a 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1038 
much easier proof than using the standard definition. We do not 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1039 
need to use properties of subsequences such as boundedness, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1040 
monotonicity etc... Compare with Harrison's corresponding proof 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1041 
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

1042 
not have problems which he encountered with guessing the right 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1043 
instantiations for his 'espsilondelta' proof(s) in this case 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1044 
since the NS formulations do not involve existential quantifiers. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1046 
Goalw [NSconvergent_def,NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1047 
"NSCauchy X = NSconvergent X"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

1052 
[NSBseq_def,NSCauchy_def])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1053 
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1054 
by (dtac (HNatInfinite_whn RSN (2,bspec)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

1059 

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

1060 
(* Standard proof for free *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1062 
by (simp_tac (simpset() addsimps [NSCauchy_Cauchy_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1065 

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

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

1067 
We can now try and derive a few properties of sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1068 
starting with the limit comparison property for sequences 
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 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1071 
"!!f. [ f NS> l; g NS> m; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1072 
\ EX N. ALL n. N <= n > f(n) <= g(n) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1073 
\ ] ==> l <= m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1076 
by (REPEAT(dtac (HNatInfinite_whn RSN (2,bspec)) 1)); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

1082 

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

1083 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1084 
Goal "[ f > l; g > m; \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1085 
\ EX N. ALL n. N <= n > f(n) <= g(n) ] \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1086 
\ ==> l <= m"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1090 

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

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

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

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

1094 
Goal "[ X > r; ALL n. a <= X n ] ==> a <= r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

1099 

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

1100 
Goal "[ X NS> r; ALL n. a <= X n ] ==> a <= r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1104 

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

1105 
Goal "[ X > r; ALL n. X n <= a ] ==> r <= a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1107 
by (rtac LIMSEQ_const 2); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1110 

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

1111 
Goal "[ X NS> r; ALL n. X n <= a ] ==> r <= a"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1115 

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 
Shift a convergent series by 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1118 
We use the fact that Cauchyness and convergence 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1119 
are equivalent and also that the successor of an 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1120 
infinite hypernatural is also infinite. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1122 
Goal "f NS> l ==> (%n. f(Suc n)) NS> l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1123 
by (forward_tac [NSconvergentI RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1124 
(NSCauchy_NSconvergent_iff RS iffD2)] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1126 
NSLIMSEQ_def,starfunNat_shift_one])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1129 
by (dtac (SHNat_one RSN (2,HNatInfinite_SHNat_add)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1131 
qed "NSLIMSEQ_Suc"; 
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 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1134 
Goal "f > l ==> (%n. f(Suc n)) > l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1137 
qed "LIMSEQ_Suc"; 
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 
Goal "(%n. f(Suc n)) NS> l ==> f NS> l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1140 
by (forward_tac [NSconvergentI RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1141 
(NSCauchy_NSconvergent_iff RS iffD2)] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1143 
NSLIMSEQ_def,starfunNat_shift_one])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1146 
by (ftac (SHNat_one RSN (2,HNatInfinite_SHNat_diff)) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1148 
by (auto_tac (claset() addSDs [bspec] addIs [inf_close_trans3], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1151 

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

1152 
Goal "(%n. f(Suc n)) > l ==> f > l"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1156 

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

1157 
Goal "(%n. f(Suc n) > l) = (f > l)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1160 

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

1161 
Goal "(%n. f(Suc n) NS> l) = (f NS> l)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1164 

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 
A sequence tends to zero iff its abs does 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1168 
(* we can prove this directly since proof is trivial *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1170 
"((%n. abs(f n)) > #0) = (f > #0)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1173 

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

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

1175 
(* We prove the NS version from the standard one *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1176 
(* Actually pure NS proof seems more complicated *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1177 
(* than the direct standard one above! *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1179 

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

1180 
Goal "((%n. abs(f n)) NS> #0) = (f NS> #0)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1181 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1184 

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 
Also we have for a general limit 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1187 
(NS proof much easier) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1190 
"f NS> l ==> (%n. abs(f n)) NS> abs(l)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1192 
addsimps [starfunNat_rabs,hypreal_of_real_hrabs RS sym])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1194 

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

1195 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1196 
Goal "f > l ==> (%n. abs(f n)) > abs(l)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1200 

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

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

1202 
An unbounded sequence's inverse tends to 0 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1204 
(* standard proof seems easier *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1206 
"ALL y. EX N. ALL n. N <= n > y < f(n) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1207 
\ ==> (%n. rinv(f n)) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

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

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

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

1214 
by (forw_inst_tac [("x","f n")] (rename_numerals real_rinv_gt_zero) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1216 
by (res_inst_tac [("t","r")] (real_rinv_rinv RS subst) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1217 
by (auto_tac (claset() addIs [real_rinv_less_iff RS iffD1],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1219 

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

1220 
Goal "ALL y. EX N. ALL n. N <= n > y < f(n) \ 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1221 
\ ==> (%n. rinv(f n)) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1222 
by (asm_simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1225 

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 
Sequence 1/n > 0 as n > infinity 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1229 
Goal "(%n. rinv(real_of_posnat n)) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

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

1233 
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

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

1235 
by (auto_tac (claset() addEs [real_less_trans],simpset())); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1237 

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

1238 
Goal "(%n. rinv(real_of_posnat n)) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1239 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1242 

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

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

1244 
Sequence r + 1/n > r as n > infinity 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1245 
now easily proved 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1247 
Goal "(%n. r + rinv(real_of_posnat n)) > r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1248 
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1249 
MRS LIMSEQ_add] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1251 
qed "LIMSEQ_rinv_real_of_posnat_add"; 
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 "(%n. r + rinv(real_of_posnat n)) NS> r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1254 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1257 

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

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

1261 

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

1262 
Goal "(%n. r + rinv(real_of_posnat n)) > r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1263 
by (cut_facts_tac [[LIMSEQ_const,LIMSEQ_rinv_real_of_posnat] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1264 
MRS LIMSEQ_add_minus] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1267 

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

1268 
Goal "(%n. r + rinv(real_of_posnat n)) NS> r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1269 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1272 

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

1273 
Goal "(%n. r*( #1 + rinv(real_of_posnat n))) > r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1274 
by (cut_inst_tac [("b","#1")] ([LIMSEQ_const, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1275 
LIMSEQ_rinv_real_of_posnat_add_minus] MRS LIMSEQ_mult) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1278 

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

1279 
Goal "(%n. r*( #1 + rinv(real_of_posnat n))) NS> r"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1280 
by (simp_tac (simpset() addsimps [LIMSEQ_NSLIMSEQ_iff RS sym, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1283 

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

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

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

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

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

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

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

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

1291 
qed_spec_mp "NSLIMSEQ_pow"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1292 

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

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

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

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

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

1297 

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

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

1299 
0 <= x < #1 ==> (x ^ n > 0) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1300 
Proof will use (NS) Cauchy equivalence for convergence and 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1301 
also fact that bounded and monotonic sequence converges. 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1304 
"[ #0 <= x; x < #1 ] ==> Bseq (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1306 
by (auto_tac (claset() addDs [conjI RS realpow_le2] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1307 
addIs [real_less_imp_le],simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1308 
[real_zero_less_one,abs_eqI1,realpow_abs RS sym] )); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1310 

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

1311 
Goal "[ #0 <= x; x < #1 ] ==> monoseq (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

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

1314 

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

1315 
Goal "[ #0 <= x; x < #1 ] ==> convergent (%n. x ^ n)"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1317 
Bseq_realpow,monoseq_realpow]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

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

1319 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1320 
(* We now use NS criterion to bring proof of theorem through *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1321 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1322 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1323 
"[ #0 <= x; x < #1 ] ==> (%n. x ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1324 
by (auto_tac (claset() addSDs [convergent_realpow], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1325 
simpset() addsimps [convergent_NSconvergent_iff])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1326 
by (forward_tac [NSconvergentD] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1327 
by (auto_tac (claset(),simpset() addsimps [NSLIMSEQ_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1328 
NSCauchy_NSconvergent_iff RS sym,NSCauchy_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1329 
starfunNat_pow])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1330 
by (forward_tac [HNatInfinite_add_one] 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1331 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1332 
by (dtac bspec 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1333 
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

1334 
by (asm_full_simp_tac (simpset() addsimps [hyperpow_add]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1335 
by (dtac inf_close_mult_subst_SReal 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1336 
by (dtac inf_close_trans3 1 THEN assume_tac 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1337 
by (auto_tac (claset() addSDs [rename_numerals (real_not_refl2 RS 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1338 
real_mult_eq_self_zero2)],simpset() addsimps 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1339 
[hypreal_of_real_mult RS sym])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1340 
qed "NSLIMSEQ_realpow_zero"; 
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 
(* standard version *) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1343 
Goal "[ #0 <= x; x < #1 ] ==> (%n. x ^ n) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1344 
by (asm_full_simp_tac (simpset() addsimps [NSLIMSEQ_realpow_zero, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1345 
LIMSEQ_NSLIMSEQ_iff]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1346 
qed "LIMSEQ_realpow_zero"; 
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 
(* 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1349 
Limit of c^n for c < 1 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1350 
*) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1351 
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1352 
by (blast_tac (claset() addSIs [LIMSEQ_realpow_zero,abs_ge_zero]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1353 
qed "LIMSEQ_rabs_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1354 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1355 
Goal "abs(c) < #1 ==> (%n. abs(c) ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1356 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1357 
LIMSEQ_NSLIMSEQ_iff RS sym]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1358 
qed "NSLIMSEQ_rabs_realpow_zero"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1359 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1360 
Goal "abs(c) < #1 ==> (%n. c ^ n) > #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1361 
by (rtac (LIMSEQ_rabs_zero RS iffD1) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1362 
by (auto_tac (claset() addIs [LIMSEQ_rabs_realpow_zero], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1363 
simpset() addsimps [realpow_abs RS sym])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1364 
qed "LIMSEQ_rabs_realpow_zero2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1365 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1366 
Goal "abs(c) < #1 ==> (%n. c ^ n) NS> #0"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1367 
by (asm_full_simp_tac (simpset() addsimps [LIMSEQ_rabs_realpow_zero2, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1368 
LIMSEQ_NSLIMSEQ_iff RS sym]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1369 
qed "NSLIMSEQ_rabs_realpow_zero2"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1370 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1371 
(*** 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1372 
Hyperreals and Sequences 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1373 
***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1374 
(*** A bounded sequence is a finite hyperreal ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1375 
Goal "NSBseq X ==> Abs_hypreal(hyprel^^{X}) : HFinite"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1376 
by (auto_tac (claset() addSIs [bexI,lemma_hyprel_refl] addIs 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1377 
[FreeUltrafilterNat_all RS FreeUltrafilterNat_subset], 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1378 
simpset() addsimps [HFinite_FreeUltrafilterNat_iff, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1379 
Bseq_NSBseq_iff RS sym, Bseq_iff1a])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1380 
qed "NSBseq_HFinite_hypreal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1381 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1382 
(*** A sequence converging to zero defines an infinitesimal ***) 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1383 
Goalw [NSLIMSEQ_def] 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1384 
"X NS> #0 ==> Abs_hypreal(hyprel^^{X}) : Infinitesimal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1385 
by (dres_inst_tac [("x","whn")] bspec 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1386 
by (simp_tac (simpset() addsimps [HNatInfinite_whn]) 1); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1387 
by (auto_tac (claset(),simpset() addsimps [hypnat_omega_def, 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1388 
mem_infmal_iff RS sym,starfunNat,hypreal_of_real_zero])); 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1389 
qed "NSLIMSEQ_zero_Infinitesimal_hypreal"; 
c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1390 

c76b73e16711
New theories: construction of hypernaturals, nonstandard extensions,
fleuriot
parents:
diff
changeset

1391 
(*** 