author  huffman 
Mon, 18 Sep 2006 07:48:07 +0200  
changeset 20563  44eda2314aab 
parent 20561  6a6d8004322f 
child 20635  e95db20977c5 
permissions  rwrr 
10751  1 
(* Title : Lim.thy 
14477  2 
ID : $Id$ 
10751  3 
Author : Jacques D. Fleuriot 
4 
Copyright : 1998 University of Cambridge 

14477  5 
Conversion to Isar and new proofs by Lawrence C Paulson, 2004 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

6 
GMVT by Benjamin Porter, 2005 
10751  7 
*) 
8 

14477  9 
header{*Limits, Continuity and Differentiation*} 
10751  10 

15131  11 
theory Lim 
15360  12 
imports SEQ 
15131  13 
begin 
14477  14 

15 
text{*Standard and Nonstandard Definitions*} 

10751  16 

19765  17 
definition 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

18 
LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

19 
("((_)/  (_)/ > (_))" [60, 0, 60] 60) 
19765  20 
"f  a > L = 
20563  21 
(\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x  a) < s 
22 
> norm (f x  L) < r)" 

10751  23 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

24 
NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

25 
("((_)/  (_)/ NS> (_))" [60, 0, 60] 60) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

26 
"f  a NS> L = 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

27 
(\<forall>x. (x \<noteq> star_of a & x @= star_of a > ( *f* f) x @= star_of L))" 
10751  28 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

29 
isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
19765  30 
"isCont f a = (f  a > (f a))" 
10751  31 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

32 
isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" 
15228  33 
{*NS definition dispenses with limit notions*} 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

34 
"isNSCont f a = (\<forall>y. y @= star_of a > 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

35 
( *f* f) y @= star_of (f a))" 
10751  36 

14477  37 
deriv:: "[real=>real,real,real] => bool" 
15228  38 
{*Differentiation: D is derivative of function f at x*} 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

39 
("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 
20563  40 
"DERIV f x :> D = ((%h. (f(x + h)  f x)/h)  0 > D)" 
10751  41 

14477  42 
nsderiv :: "[real=>real,real,real] => bool" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

43 
("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60) 
19765  44 
"NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal  {0}. 
20563  45 
(( *f* f)(hypreal_of_real x + h) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

46 
 hypreal_of_real (f x))/h @= hypreal_of_real D)" 
10751  47 

14477  48 
differentiable :: "[real=>real,real] => bool" (infixl "differentiable" 60) 
19765  49 
"f differentiable x = (\<exists>D. DERIV f x :> D)" 
10751  50 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

51 
NSdifferentiable :: "[real=>real,real] => bool" 
14477  52 
(infixl "NSdifferentiable" 60) 
19765  53 
"f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)" 
10751  54 

14477  55 
increment :: "[real=>real,real,hypreal] => hypreal" 
19765  56 
"increment f x h = (@inc. f NSdifferentiable x & 
20563  57 
inc = ( *f* f)(hypreal_of_real x + h)  hypreal_of_real (f x))" 
10751  58 

14477  59 
isUCont :: "(real=>real) => bool" 
20563  60 
"isUCont f = (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x  y\<bar> < s > \<bar>f x  f y\<bar> < r)" 
10751  61 

14477  62 
isNSUCont :: "(real=>real) => bool" 
19765  63 
"isNSUCont f = (\<forall>x y. x @= y > ( *f* f) x @= ( *f* f) y)" 
10751  64 

65 

66 
consts 

67 
Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)" 

68 
primrec 

69 
"Bolzano_bisect P a b 0 = (a,b)" 

70 
"Bolzano_bisect P a b (Suc n) = 

71 
(let (x,y) = Bolzano_bisect P a b n 

11704
3c50a2cd6f00
* sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents:
11701
diff
changeset

72 
in if P(x, (x+y)/2) then ((x+y)/2, y) 
14477  73 
else (x, (x+y)/2))" 
74 

75 

76 

77 
section{*Some Purely Standard Proofs*} 

78 

79 
lemma LIM_eq: 

80 
"f  a > L = 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

81 
(\<forall>r>0.\<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r)" 
14477  82 
by (simp add: LIM_def diff_minus) 
83 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

84 
lemma LIM_I: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

85 
"(!!r. 0<r ==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

86 
==> f  a > L" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

87 
by (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

88 

14477  89 
lemma LIM_D: 
90 
"[ f  a > L; 0<r ] 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

91 
==> \<exists>s>0.\<forall>x. x \<noteq> a & norm (xa) < s > norm (f x  L) < r" 
14477  92 
by (simp add: LIM_eq) 
93 

15228  94 
lemma LIM_const [simp]: "(%x. k)  x > k" 
14477  95 
by (simp add: LIM_def) 
96 

97 
lemma LIM_add: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

98 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector" 
14477  99 
assumes f: "f  a > L" and g: "g  a > M" 
100 
shows "(%x. f x + g(x))  a > (L + M)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

101 
proof (rule LIM_I) 
14477  102 
fix r :: real 
20409  103 
assume r: "0 < r" 
14477  104 
from LIM_D [OF f half_gt_zero [OF r]] 
105 
obtain fs 

106 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

107 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x  L) < r/2" 
14477  108 
by blast 
109 
from LIM_D [OF g half_gt_zero [OF r]] 

110 
obtain gs 

111 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

112 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x  M) < r/2" 
14477  113 
by blast 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

114 
show "\<exists>s>0.\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x + g x  (L + M)) < r" 
14477  115 
proof (intro exI conjI strip) 
116 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

117 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

118 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

119 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  120 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

121 
have "norm (f x  L) < r/2" and "norm (g x  M) < r/2" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

122 
hence "norm (f x  L) + norm (g x  M) < r" by arith 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

123 
thus "norm (f x + g x  (L + M)) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

124 
by (blast intro: norm_diff_triangle_ineq order_le_less_trans) 
14477  125 
qed 
126 
qed 

127 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

128 
lemma minus_diff_minus: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

129 
fixes a b :: "'a::ab_group_add" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

130 
shows "( a)  ( b) =  (a  b)" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

131 
by simp 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

132 

14477  133 
lemma LIM_minus: "f  a > L ==> (%x. f(x))  a > L" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

134 
by (simp only: LIM_eq minus_diff_minus norm_minus_cancel) 
14477  135 

136 
lemma LIM_add_minus: 

137 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

138 
by (intro LIM_add LIM_minus) 
14477  139 

140 
lemma LIM_diff: 

141 
"[ f  x > l; g  x > m ] ==> (%x. f(x)  g(x))  x > lm" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

142 
by (simp only: diff_minus LIM_add LIM_minus) 
14477  143 

144 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

145 
lemma LIM_const_not_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

146 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

147 
shows "k \<noteq> L ==> ~ ((%x. k)  a > L)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

148 
apply (simp add: LIM_eq) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

149 
apply (rule_tac x="norm (k  L)" in exI, simp, safe) 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

150 
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

151 
done 
14477  152 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

153 
lemma LIM_const_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

154 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

155 
shows "(%x. k)  a > L ==> k = L" 
14477  156 
apply (rule ccontr) 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

157 
apply (blast dest: LIM_const_not_eq) 
14477  158 
done 
159 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

160 
lemma LIM_unique: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

161 
fixes a :: "'a::real_normed_div_algebra" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

162 
shows "[ f  a > L; f  a > M ] ==> L = M" 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

163 
apply (drule LIM_diff, assumption) 
14477  164 
apply (auto dest!: LIM_const_eq) 
165 
done 

166 

167 
lemma LIM_mult_zero: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

168 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
14477  169 
assumes f: "f  a > 0" and g: "g  a > 0" 
170 
shows "(%x. f(x) * g(x))  a > 0" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

171 
proof (rule LIM_I, simp) 
14477  172 
fix r :: real 
173 
assume r: "0<r" 

174 
from LIM_D [OF f zero_less_one] 

175 
obtain fs 

176 
where fs: "0 < fs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

177 
and fs_lt: "\<forall>x. x \<noteq> a & norm (xa) < fs > norm (f x) < 1" 
14477  178 
by auto 
179 
from LIM_D [OF g r] 

180 
obtain gs 

181 
where gs: "0 < gs" 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

182 
and gs_lt: "\<forall>x. x \<noteq> a & norm (xa) < gs > norm (g x) < r" 
14477  183 
by auto 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

184 
show "\<exists>s. 0 < s \<and> (\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm (f x * g x) < r)" 
14477  185 
proof (intro exI conjI strip) 
186 
show "0 < min fs gs" by (simp add: fs gs) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

187 
fix x :: 'a 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

188 
assume "x \<noteq> a \<and> norm (xa) < min fs gs" 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

189 
hence "x \<noteq> a \<and> norm (xa) < fs \<and> norm (xa) < gs" by simp 
14477  190 
with fs_lt gs_lt 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

191 
have "norm (f x) < 1" and "norm (g x) < r" by blast+ 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

192 
hence "norm (f x) * norm (g x) < 1*r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

193 
by (rule mult_strict_mono' [OF _ _ norm_ge_zero norm_ge_zero]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

194 
thus "norm (f x * g x) < r" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

195 
by (simp add: order_le_less_trans [OF norm_mult_ineq]) 
14477  196 
qed 
197 
qed 

198 

199 
lemma LIM_self: "(%x. x)  a > a" 

200 
by (auto simp add: LIM_def) 

201 

202 
text{*Limits are equal for functions equal except at limit point*} 

203 
lemma LIM_equal: 

204 
"[ \<forall>x. x \<noteq> a > (f x = g x) ] ==> (f  a > l) = (g  a > l)" 

205 
by (simp add: LIM_def) 

206 

207 
text{*Two uses in Hyperreal/Transcendental.ML*} 

208 
lemma LIM_trans: 

209 
"[ (%x. f(x) + g(x))  a > 0; g  a > l ] ==> f  a > l" 

210 
apply (drule LIM_add, assumption) 

211 
apply (auto simp add: add_assoc) 

212 
done 

213 

214 

215 
subsection{*Relationships Between Standard and Nonstandard Concepts*} 

216 

217 
text{*Standard and NS definitions of Limit*} (*NEEDS STRUCTURING*) 

218 
lemma LIM_NSLIM: 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

219 
"f  a > L ==> f  a NS> L" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

220 
apply (simp add: LIM_def NSLIM_def approx_def, safe) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

221 
apply (rule_tac x="x" in star_cases) 
20563  222 
apply (simp add: star_of_def star_n_diff starfun) 
14477  223 
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

224 
apply (simp add: star_n_eq_iff) 
14477  225 
apply (drule_tac x = u in spec, clarify) 
226 
apply (drule_tac x = s in spec, clarify) 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

227 
apply (simp only: FUFNat.Collect_not [symmetric]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

228 
apply (elim ultra, simp) 
14477  229 
done 
230 

15228  231 

232 
subsubsection{*Limit: The NS definition implies the standard definition.*} 

14477  233 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

234 
lemma lemma_LIM: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

235 
fixes L :: "'a::real_normed_vector" 
20563  236 
shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x  a) < s \<and> \<not> norm (f x  L) < r 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

237 
==> \<forall>n::nat. \<exists>x. x \<noteq> a \<and> 
20563  238 
norm (x  a) < inverse(real(Suc n)) \<and> \<not> norm (f x  L) < r" 
14477  239 
apply clarify 
240 
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) 

241 
done 

242 

243 
lemma lemma_skolemize_LIM2: 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

244 
fixes L :: "'a::real_normed_vector" 
20563  245 
shows "\<forall>s>0. \<exists>x. x \<noteq> a \<and> norm (x  a) < s \<and> \<not> norm (f x  L) < r 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

246 
==> \<exists>X. \<forall>n::nat. X n \<noteq> a \<and> 
20563  247 
norm (X n  a) < inverse(real(Suc n)) \<and> \<not> norm(f (X n)  L) < r" 
14477  248 
apply (drule lemma_LIM) 
249 
apply (drule choice, blast) 

250 
done 

251 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

252 
lemma FreeUltrafilterNat_most: "\<exists>N. \<forall>n\<ge>N. P n \<Longrightarrow> {n. P n} \<in> \<U>" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

253 
apply (erule exE) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

254 
apply (rule_tac u="{n. N \<le> n}" in FUFNat.subset) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

255 
apply (rule cofinite_mem_FreeUltrafilterNat) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

256 
apply (simp add: Collect_neg_eq [symmetric]) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

257 
apply (simp add: linorder_not_le finite_nat_segment) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

258 
apply fast 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

259 
done 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

260 

2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

261 
lemma lemma_simp: "\<forall>n. X n \<noteq> a & 
20563  262 
norm (X n  a) < inverse (real(Suc n)) & 
263 
\<not> norm (f (X n)  L) < r ==> 

264 
\<forall>n. norm (X n  a) < inverse (real(Suc n))" 

14477  265 
by auto 
266 

267 

15228  268 
text{*NSLIM => LIM*} 
14477  269 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

270 
lemma NSLIM_LIM: "f  a NS> L ==> f  a > L" 
14477  271 
apply (simp add: LIM_def NSLIM_def approx_def) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

272 
apply (rule ccontr, simp, clarify) 
14477  273 
apply (drule lemma_skolemize_LIM2, safe) 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

274 
apply (drule_tac x = "star_n X" in spec) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

275 
apply (drule mp, rule conjI) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

276 
apply (simp add: star_of_def star_n_eq_iff) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

277 
apply (rule real_seq_to_hypreal_Infinitesimal, simp) 
20563  278 
apply (simp add: starfun star_of_def star_n_diff) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

279 
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

280 
apply (drule spec, drule (1) mp) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

281 
apply simp 
14477  282 
done 
283 

15228  284 
theorem LIM_NSLIM_iff: "(f  x > L) = (f  x NS> L)" 
14477  285 
by (blast intro: LIM_NSLIM NSLIM_LIM) 
286 

15228  287 
text{*Proving properties of limits using nonstandard definition. 
288 
The properties hold for standard limits as well!*} 

14477  289 

290 
lemma NSLIM_mult: 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

291 
fixes l m :: "'a::real_normed_algebra" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

292 
shows "[ f  x NS> l; g  x NS> m ] 
14477  293 
==> (%x. f(x) * g(x))  x NS> (l * m)" 
15228  294 
by (auto simp add: NSLIM_def intro!: approx_mult_HFinite) 
14477  295 

15228  296 
lemma LIM_mult2: 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

297 
fixes l m :: "'a::real_normed_algebra" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

298 
shows "[ f  x > l; g  x > m ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

299 
==> (%x. f(x) * g(x))  x > (l * m)" 
14477  300 
by (simp add: LIM_NSLIM_iff NSLIM_mult) 
301 

302 
lemma NSLIM_add: 

303 
"[ f  x NS> l; g  x NS> m ] 

304 
==> (%x. f(x) + g(x))  x NS> (l + m)" 

15228  305 
by (auto simp add: NSLIM_def intro!: approx_add) 
14477  306 

15228  307 
lemma LIM_add2: 
308 
"[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

14477  309 
by (simp add: LIM_NSLIM_iff NSLIM_add) 
310 

311 

15228  312 
lemma NSLIM_const [simp]: "(%x. k)  x NS> k" 
14477  313 
by (simp add: NSLIM_def) 
314 

315 
lemma LIM_const2: "(%x. k)  x > k" 

316 
by (simp add: LIM_NSLIM_iff) 

317 

318 
lemma NSLIM_minus: "f  a NS> L ==> (%x. f(x))  a NS> L" 

319 
by (simp add: NSLIM_def) 

320 

321 
lemma LIM_minus2: "f  a > L ==> (%x. f(x))  a > L" 

322 
by (simp add: LIM_NSLIM_iff NSLIM_minus) 

323 

324 

325 
lemma NSLIM_add_minus: "[ f  x NS> l; g  x NS> m ] ==> (%x. f(x) + g(x))  x NS> (l + m)" 

326 
by (blast dest: NSLIM_add NSLIM_minus) 

327 

328 
lemma LIM_add_minus2: "[ f  x > l; g  x > m ] ==> (%x. f(x) + g(x))  x > (l + m)" 

329 
by (simp add: LIM_NSLIM_iff NSLIM_add_minus) 

330 

331 

332 
lemma NSLIM_inverse: 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

333 
fixes L :: "'a::{real_normed_div_algebra,division_by_zero}" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

334 
shows "[ f  a NS> L; L \<noteq> 0 ] 
14477  335 
==> (%x. inverse(f(x)))  a NS> (inverse L)" 
336 
apply (simp add: NSLIM_def, clarify) 

337 
apply (drule spec) 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

338 
apply (auto simp add: star_of_approx_inverse) 
14477  339 
done 
340 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

341 
lemma LIM_inverse: 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

342 
fixes L :: "'a::{real_normed_div_algebra,division_by_zero}" 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

343 
shows "[ f  a > L; L \<noteq> 0 ] 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

344 
==> (%x. inverse(f(x)))  a > (inverse L)" 
14477  345 
by (simp add: LIM_NSLIM_iff NSLIM_inverse) 
346 

347 

348 
lemma NSLIM_zero: 

349 
assumes f: "f  a NS> l" shows "(%x. f(x) + l)  a NS> 0" 

15228  350 
proof  
14477  351 
have "(\<lambda>x. f x +  l)  a NS> l + l" 
15228  352 
by (rule NSLIM_add_minus [OF f NSLIM_const]) 
14477  353 
thus ?thesis by simp 
354 
qed 

355 

356 
lemma LIM_zero2: "f  a > l ==> (%x. f(x) + l)  a > 0" 

357 
by (simp add: LIM_NSLIM_iff NSLIM_zero) 

358 

359 
lemma NSLIM_zero_cancel: "(%x. f(x)  l)  x NS> 0 ==> f  x NS> l" 

360 
apply (drule_tac g = "%x. l" and m = l in NSLIM_add) 

361 
apply (auto simp add: diff_minus add_assoc) 

362 
done 

363 

364 
lemma LIM_zero_cancel: "(%x. f(x)  l)  x > 0 ==> f  x > l" 

365 
apply (drule_tac g = "%x. l" and M = l in LIM_add) 

366 
apply (auto simp add: diff_minus add_assoc) 

367 
done 

368 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

369 
lemma NSLIM_const_not_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

370 
fixes a :: real (* TODO: generalize to real_normed_div_algebra *) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

371 
shows "k \<noteq> L ==> ~ ((%x. k)  a NS> L)" 
14477  372 
apply (simp add: NSLIM_def) 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

373 
apply (rule_tac x="star_of a + epsilon" in exI) 
14477  374 
apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym] 
375 
simp add: hypreal_epsilon_not_zero) 

376 
done 

377 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

378 
lemma NSLIM_not_zero: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

379 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

380 
shows "k \<noteq> 0 ==> ~ ((%x. k)  a NS> 0)" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

381 
by (rule NSLIM_const_not_eq) 
14477  382 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

383 
lemma NSLIM_const_eq: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

384 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

385 
shows "(%x. k)  a NS> L ==> k = L" 
14477  386 
apply (rule ccontr) 
15228  387 
apply (blast dest: NSLIM_const_not_eq) 
14477  388 
done 
389 

15228  390 
text{* can actually be proved more easily by unfolding the definition!*} 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

391 
lemma NSLIM_unique: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

392 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

393 
shows "[ f  a NS> L; f  a NS> M ] ==> L = M" 
14477  394 
apply (drule NSLIM_minus) 
395 
apply (drule NSLIM_add, assumption) 

396 
apply (auto dest!: NSLIM_const_eq [symmetric]) 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

397 
apply (simp add: diff_def [symmetric]) 
14477  398 
done 
399 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

400 
lemma LIM_unique2: 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

401 
fixes a :: real 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

402 
shows "[ f  a > L; f  a > M ] ==> L = M" 
14477  403 
by (simp add: LIM_NSLIM_iff NSLIM_unique) 
404 

405 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

406 
lemma NSLIM_mult_zero: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

407 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

408 
shows "[ f  x NS> 0; g  x NS> 0 ] ==> (%x. f(x)*g(x))  x NS> 0" 
14477  409 
by (drule NSLIM_mult, auto) 
410 

411 
(* we can use the corresponding thm LIM_mult2 *) 

412 
(* for standard definition of limit *) 

413 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

414 
lemma LIM_mult_zero2: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

415 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

416 
shows "[ f  x > 0; g  x > 0 ] ==> (%x. f(x)*g(x))  x > 0" 
14477  417 
by (drule LIM_mult2, auto) 
418 

419 

420 
lemma NSLIM_self: "(%x. x)  a NS> a" 

421 
by (simp add: NSLIM_def) 

422 

423 

15228  424 
subsection{* Derivatives and Continuity: NS and Standard properties*} 
425 

426 
subsubsection{*Continuity*} 

14477  427 

428 
lemma isNSContD: "[ isNSCont f a; y \<approx> hypreal_of_real a ] ==> ( *f* f) y \<approx> hypreal_of_real (f a)" 

429 
by (simp add: isNSCont_def) 

430 

431 
lemma isNSCont_NSLIM: "isNSCont f a ==> f  a NS> (f a) " 

432 
by (simp add: isNSCont_def NSLIM_def) 

433 

434 
lemma NSLIM_isNSCont: "f  a NS> (f a) ==> isNSCont f a" 

435 
apply (simp add: isNSCont_def NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

436 
apply (case_tac "y = star_of a", auto) 
14477  437 
done 
438 

15228  439 
text{*NS continuity can be defined using NS Limit in 
440 
similar fashion to standard def of continuity*} 

14477  441 
lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f  a NS> (f a))" 
442 
by (blast intro: isNSCont_NSLIM NSLIM_isNSCont) 

443 

15228  444 
text{*Hence, NS continuity can be given 
445 
in terms of standard limit*} 

14477  446 
lemma isNSCont_LIM_iff: "(isNSCont f a) = (f  a > (f a))" 
447 
by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff) 

448 

15228  449 
text{*Moreover, it's trivial now that NS continuity 
450 
is equivalent to standard continuity*} 

14477  451 
lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)" 
452 
apply (simp add: isCont_def) 

453 
apply (rule isNSCont_LIM_iff) 

454 
done 

455 

15228  456 
text{*Standard continuity ==> NS continuity*} 
14477  457 
lemma isCont_isNSCont: "isCont f a ==> isNSCont f a" 
458 
by (erule isNSCont_isCont_iff [THEN iffD2]) 

459 

15228  460 
text{*NS continuity ==> Standard continuity*} 
14477  461 
lemma isNSCont_isCont: "isNSCont f a ==> isCont f a" 
462 
by (erule isNSCont_isCont_iff [THEN iffD1]) 

463 

464 
text{*Alternative definition of continuity*} 

465 
(* Prove equivalence between NS limits  *) 

466 
(* seems easier than using standard def *) 

467 
lemma NSLIM_h_iff: "(f  a NS> L) = ((%h. f(a + h))  0 NS> L)" 

468 
apply (simp add: NSLIM_def, auto) 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

469 
apply (drule_tac x = "star_of a + x" in spec) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

470 
apply (drule_tac [2] x = " star_of a + x" in spec, safe, simp) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

471 
apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

472 
apply (erule_tac [3] approx_minus_iff2 [THEN iffD1]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

473 
prefer 2 apply (simp add: add_commute diff_def [symmetric]) 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

474 
apply (rule_tac x = x in star_cases) 
17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

475 
apply (rule_tac [2] x = x in star_cases) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

476 
apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num) 
14477  477 
done 
478 

479 
lemma NSLIM_isCont_iff: "(f  a NS> f a) = ((%h. f(a + h))  0 NS> f a)" 

480 
by (rule NSLIM_h_iff) 

481 

482 
lemma LIM_isCont_iff: "(f  a > f a) = ((%h. f(a + h))  0 > f(a))" 

483 
by (simp add: LIM_NSLIM_iff NSLIM_isCont_iff) 

484 

485 
lemma isCont_iff: "(isCont f x) = ((%h. f(x + h))  0 > f(x))" 

486 
by (simp add: isCont_def LIM_isCont_iff) 

487 

15228  488 
text{*Immediate application of nonstandard criterion for continuity can offer 
489 
very simple proofs of some standard property of continuous functions*} 

14477  490 
text{*sum continuous*} 
491 
lemma isCont_add: "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) + g(x)) a" 

492 
by (auto intro: approx_add simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) 

493 

494 
text{*mult continuous*} 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

495 
lemma isCont_mult: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

496 
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

497 
shows "[ isCont f a; isCont g a ] ==> isCont (%x. f(x) * g(x)) a" 
15228  498 
by (auto intro!: starfun_mult_HFinite_approx 
499 
simp del: starfun_mult [symmetric] 

14477  500 
simp add: isNSCont_isCont_iff [symmetric] isNSCont_def) 
501 

15228  502 
text{*composition of continuous functions 
503 
Note very short straightforard proof!*} 

14477  504 
lemma isCont_o: "[ isCont f a; isCont g (f a) ] ==> isCont (g o f) a" 
505 
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_def starfun_o [symmetric]) 

506 

507 
lemma isCont_o2: "[ isCont f a; isCont g (f a) ] ==> isCont (%x. g (f x)) a" 

508 
by (auto dest: isCont_o simp add: o_def) 

509 

510 
lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x.  f x) a" 

511 
by (simp add: isNSCont_def) 

512 

513 
lemma isCont_minus: "isCont f a ==> isCont (%x.  f x) a" 

514 
by (auto simp add: isNSCont_isCont_iff [symmetric] isNSCont_minus) 

515 

516 
lemma isCont_inverse: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

517 
fixes f :: "'a::real_normed_vector \<Rightarrow> 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

518 
'b::{real_normed_div_algebra,division_by_zero}" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

519 
shows "[ isCont f x; f x \<noteq> 0 ] ==> isCont (%x. inverse (f x)) x" 
14477  520 
apply (simp add: isCont_def) 
521 
apply (blast intro: LIM_inverse) 

522 
done 

523 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

524 
lemma isNSCont_inverse: 
20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

525 
fixes f :: "'a::real_normed_vector \<Rightarrow> 
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

526 
'b::{real_normed_div_algebra,division_by_zero}" 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

527 
shows "[ isNSCont f x; f x \<noteq> 0 ] ==> isNSCont (%x. inverse (f x)) x" 
14477  528 
by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff) 
529 

530 
lemma isCont_diff: 

531 
"[ isCont f a; isCont g a ] ==> isCont (%x. f(x)  g(x)) a" 

532 
apply (simp add: diff_minus) 

533 
apply (auto intro: isCont_add isCont_minus) 

534 
done 

535 

15228  536 
lemma isCont_const [simp]: "isCont (%x. k) a" 
14477  537 
by (simp add: isCont_def) 
538 

15228  539 
lemma isNSCont_const [simp]: "isNSCont (%x. k) a" 
14477  540 
by (simp add: isNSCont_def) 
541 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

542 
lemma isNSCont_abs [simp]: "isNSCont abs (a::real)" 
14477  543 
apply (simp add: isNSCont_def) 
544 
apply (auto intro: approx_hrabs simp add: hypreal_of_real_hrabs [symmetric] starfun_rabs_hrabs) 

545 
done 

546 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

547 
lemma isCont_abs [simp]: "isCont abs (a::real)" 
14477  548 
by (auto simp add: isNSCont_isCont_iff [symmetric]) 
15228  549 

14477  550 

551 
(**************************************************************** 

552 
(%* Leave as commented until I add topology theory or remove? *%) 

553 
(%* 

554 
Elementary topology proof for a characterisation of 

555 
continuity now: a function f is continuous if and only 

556 
if the inverse image, {x. f(x) \<in> A}, of any open set A 

557 
is always an open set 

558 
*%) 

559 
Goal "[ isNSopen A; \<forall>x. isNSCont f x ] 

560 
==> isNSopen {x. f x \<in> A}" 

561 
by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1])); 

562 
by (dtac (mem_monad_approx RS approx_sym); 

563 
by (dres_inst_tac [("x","a")] spec 1); 

564 
by (dtac isNSContD 1 THEN assume_tac 1) 

565 
by (dtac bspec 1 THEN assume_tac 1) 

566 
by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1); 

567 
by (blast_tac (claset() addIs [starfun_mem_starset]); 

568 
qed "isNSCont_isNSopen"; 

569 

570 
Goalw [isNSCont_def] 

571 
"\<forall>A. isNSopen A > isNSopen {x. f x \<in> A} \ 

572 
\ ==> isNSCont f x"; 

573 
by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS 

574 
(approx_minus_iff RS iffD2)],simpset() addsimps 

575 
[Infinitesimal_def,SReal_iff])); 

576 
by (dres_inst_tac [("x","{z. abs(z + f(x)) < ya}")] spec 1); 

577 
by (etac (isNSopen_open_interval RSN (2,impE)); 

578 
by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def])); 

579 
by (dres_inst_tac [("x","x")] spec 1); 

580 
by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad], 

581 
simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus])); 

582 
qed "isNSopen_isNSCont"; 

583 

584 
Goal "(\<forall>x. isNSCont f x) = \ 

585 
\ (\<forall>A. isNSopen A > isNSopen {x. f(x) \<in> A})"; 

586 
by (blast_tac (claset() addIs [isNSCont_isNSopen, 

587 
isNSopen_isNSCont]); 

588 
qed "isNSCont_isNSopen_iff"; 

589 

590 
(%* Standard version of same theorem *%) 

591 
Goal "(\<forall>x. isCont f x) = \ 

592 
\ (\<forall>A. isopen A > isopen {x. f(x) \<in> A})"; 

593 
by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff], 

594 
simpset() addsimps [isNSopen_isopen_iff RS sym, 

595 
isNSCont_isCont_iff RS sym])); 

596 
qed "isCont_isopen_iff"; 

597 
*******************************************************************) 

598 

599 
text{*Uniform continuity*} 

600 
lemma isNSUContD: "[ isNSUCont f; x \<approx> y] ==> ( *f* f) x \<approx> ( *f* f) y" 

601 
by (simp add: isNSUCont_def) 

602 

603 
lemma isUCont_isCont: "isUCont f ==> isCont f x" 

604 
by (simp add: isUCont_def isCont_def LIM_def, meson) 

605 

606 
lemma isUCont_isNSUCont: "isUCont f ==> isNSUCont f" 

607 
apply (simp add: isNSUCont_def isUCont_def approx_def) 

20563  608 
apply (simp add: all_star_eq starfun star_n_diff) 
14477  609 
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff, safe) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

610 
apply (rename_tac Xa Xb u) 
14477  611 
apply (drule_tac x = u in spec, clarify) 
612 
apply (drule_tac x = s in spec, clarify) 

20563  613 
apply (subgoal_tac "\<forall>n::nat. abs ((Xa n)  (Xb n)) < s > abs (f (Xa n)  f (Xb n)) < u") 
14477  614 
prefer 2 apply blast 
20563  615 
apply (erule_tac V = "\<forall>x y. \<bar>x  y\<bar> < s > \<bar>f x  f y\<bar> < u" in thin_rl) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

616 
apply (erule ultra, simp) 
14477  617 
done 
618 

20563  619 
lemma lemma_LIMu: "\<forall>s>0.\<exists>z y. \<bar>z  y\<bar> < s & r \<le> \<bar>f z  f y\<bar> 
620 
==> \<forall>n::nat. \<exists>z y. \<bar>z  y\<bar> < inverse(real(Suc n)) & r \<le> \<bar>f z  f y\<bar>" 

14477  621 
apply clarify 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

622 
apply (cut_tac n1 = n 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

623 
in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto) 
14477  624 
done 
625 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

626 
lemma lemma_skolemize_LIM2u: 
20563  627 
"\<forall>s>0.\<exists>z y. \<bar>z  y\<bar> < s & r \<le> \<bar>f z  f y\<bar> 
14477  628 
==> \<exists>X Y. \<forall>n::nat. 
20563  629 
abs(X n  Y n) < inverse(real(Suc n)) & 
630 
r \<le> abs(f (X n)  f (Y n))" 

14477  631 
apply (drule lemma_LIMu) 
632 
apply (drule choice, safe) 

633 
apply (drule choice, blast) 

634 
done 

635 

20563  636 
lemma lemma_simpu: "\<forall>n. \<bar>X n  Y n\<bar> < inverse (real(Suc n)) & 
637 
r \<le> abs (f (X n)  f(Y n)) ==> 

638 
\<forall>n. \<bar>X n  Y n\<bar> < inverse (real(Suc n))" 

15228  639 
by auto 
14477  640 

641 
lemma isNSUCont_isUCont: 

642 
"isNSUCont f ==> isUCont f" 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

643 
apply (simp add: isNSUCont_def isUCont_def approx_def, safe) 
15228  644 
apply (rule ccontr, simp) 
14477  645 
apply (simp add: linorder_not_less) 
646 
apply (drule lemma_skolemize_LIM2u, safe) 

17318
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

647 
apply (drule_tac x = "star_n X" in spec) 
bc1c75855f3d
starfun, starset, and other functions on NS types are now polymorphic;
huffman
parents:
17298
diff
changeset

648 
apply (drule_tac x = "star_n Y" in spec) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

649 
apply (drule mp) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

650 
apply (rule real_seq_to_hypreal_Infinitesimal2, simp) 
20563  651 
apply (simp add: all_star_eq starfun star_n_diff) 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

652 
apply (simp add: Infinitesimal_FreeUltrafilterNat_iff) 
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

653 
apply (drule spec, drule (1) mp) 
14477  654 
apply (drule FreeUltrafilterNat_all, ultra) 
655 
done 

656 

657 
text{*Derivatives*} 

20563  658 
lemma DERIV_iff: "(DERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 > D)" 
14477  659 
by (simp add: deriv_def) 
660 

661 
lemma DERIV_NS_iff: 

20563  662 
"(DERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 NS> D)" 
14477  663 
by (simp add: deriv_def LIM_NSLIM_iff) 
664 

20563  665 
lemma DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h)  f(x))/h)  0 > D" 
14477  666 
by (simp add: deriv_def) 
667 

20563  668 
lemma NS_DERIV_D: "DERIV f x :> D ==> (%h. (f(x + h)  f(x))/h)  0 NS> D" 
14477  669 
by (simp add: deriv_def LIM_NSLIM_iff) 
670 

15228  671 

14477  672 
subsubsection{*Uniqueness*} 
673 

674 
lemma DERIV_unique: 

675 
"[ DERIV f x :> D; DERIV f x :> E ] ==> D = E" 

676 
apply (simp add: deriv_def) 

677 
apply (blast intro: LIM_unique) 

678 
done 

679 

680 
lemma NSDeriv_unique: 

681 
"[ NSDERIV f x :> D; NSDERIV f x :> E ] ==> D = E" 

682 
apply (simp add: nsderiv_def) 

683 
apply (cut_tac Infinitesimal_epsilon hypreal_epsilon_not_zero) 

15228  684 
apply (auto dest!: bspec [where x=epsilon] 
685 
intro!: inj_hypreal_of_real [THEN injD] 

14477  686 
dest: approx_trans3) 
687 
done 

688 

689 
subsubsection{*Differentiable*} 

690 

691 
lemma differentiableD: "f differentiable x ==> \<exists>D. DERIV f x :> D" 

692 
by (simp add: differentiable_def) 

693 

694 
lemma differentiableI: "DERIV f x :> D ==> f differentiable x" 

695 
by (force simp add: differentiable_def) 

696 

697 
lemma NSdifferentiableD: "f NSdifferentiable x ==> \<exists>D. NSDERIV f x :> D" 

698 
by (simp add: NSdifferentiable_def) 

699 

700 
lemma NSdifferentiableI: "NSDERIV f x :> D ==> f NSdifferentiable x" 

701 
by (force simp add: NSdifferentiable_def) 

702 

703 
subsubsection{*Alternative definition for differentiability*} 

704 

705 
lemma DERIV_LIM_iff: 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

706 
"((%h::real. (f(a + h)  f(a)) / h)  0 > D) = 
14477  707 
((%x. (f(x)f(a)) / (xa))  a > D)" 
708 
proof (intro iffI LIM_I) 

709 
fix r::real 

710 
assume r: "0<r" 

711 
assume "(\<lambda>h. (f (a + h)  f a) / h)  0 > D" 

712 
from LIM_D [OF this r] 

713 
obtain s 

714 
where s: "0 < s" 

715 
and s_lt: "\<forall>x. x \<noteq> 0 & \<bar>x\<bar> < s > \<bar>(f (a + x)  f a) / x  D\<bar> < r" 

716 
by auto 

717 
show "\<exists>s. 0 < s \<and> 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

718 
(\<forall>x. x \<noteq> a \<and> norm (xa) < s \<longrightarrow> norm ((f x  f a) / (xa)  D) < r)" 
14477  719 
proof (intro exI conjI strip) 
720 
show "0 < s" by (rule s) 

721 
next 

722 
fix x::real 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

723 
assume "x \<noteq> a \<and> norm (xa) < s" 
14477  724 
with s_lt [THEN spec [where x="xa"]] 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

725 
show "norm ((f x  f a) / (xa)  D) < r" by auto 
14477  726 
qed 
727 
next 

728 
fix r::real 

729 
assume r: "0<r" 

730 
assume "(\<lambda>x. (f x  f a) / (xa))  a > D" 

731 
from LIM_D [OF this r] 

732 
obtain s 

733 
where s: "0 < s" 

734 
and s_lt: "\<forall>x. x \<noteq> a & \<bar>xa\<bar> < s > \<bar>(f x  f a)/(xa)  D\<bar> < r" 

735 
by auto 

736 
show "\<exists>s. 0 < s \<and> 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

737 
(\<forall>x. x \<noteq> 0 & norm (x  0) < s > norm ((f (a + x)  f a) / x  D) < r)" 
14477  738 
proof (intro exI conjI strip) 
739 
show "0 < s" by (rule s) 

740 
next 

741 
fix x::real 

20561
6a6d8004322f
generalize type of (NS)LIM to work on functions with vector space domain types
huffman
parents:
20552
diff
changeset

742 
assume "x \<noteq> 0 \<and> norm (x  0) < s" 
14477  743 
with s_lt [THEN spec [where x="x+a"]] 
20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

744 
show "norm ((f (a + x)  f a) / x  D) < r" by (auto simp add: add_ac) 
14477  745 
qed 
746 
qed 

747 

748 
lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z)  f(x)) / (zx))  x > D)" 

749 
by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff) 

750 

751 

752 
subsection{*Equivalence of NS and standard definitions of differentiation*} 

753 

15228  754 
subsubsection{*First NSDERIV in terms of NSLIM*} 
14477  755 

15228  756 
text{*first equivalence *} 
14477  757 
lemma NSDERIV_NSLIM_iff: 
20563  758 
"(NSDERIV f x :> D) = ((%h. (f(x + h)  f(x))/h)  0 NS> D)" 
14477  759 
apply (simp add: nsderiv_def NSLIM_def, auto) 
760 
apply (drule_tac x = xa in bspec) 

761 
apply (rule_tac [3] ccontr) 

762 
apply (drule_tac [3] x = h in spec) 

763 
apply (auto simp add: mem_infmal_iff starfun_lambda_cancel) 

764 
done 

765 

15228  766 
text{*second equivalence *} 
14477  767 
lemma NSDERIV_NSLIM_iff2: 
768 
"(NSDERIV f x :> D) = ((%z. (f(z)  f(x)) / (zx))  x NS> D)" 

15228  769 
by (simp add: NSDERIV_NSLIM_iff DERIV_LIM_iff diff_minus [symmetric] 
14477  770 
LIM_NSLIM_iff [symmetric]) 
771 

772 
(* while we're at it! *) 

773 
lemma NSDERIV_iff2: 

774 
"(NSDERIV f x :> D) = 

775 
(\<forall>w. 

776 
w \<noteq> hypreal_of_real x & w \<approx> hypreal_of_real x > 

777 
( *f* (%z. (f z  f x) / (zx))) w \<approx> hypreal_of_real D)" 

778 
by (simp add: NSDERIV_NSLIM_iff2 NSLIM_def) 

779 

780 
(*FIXME DELETE*) 

20563  781 
lemma hypreal_not_eq_minus_iff: "(x \<noteq> a) = (x  a \<noteq> (0::hypreal))" 
14477  782 
by (auto dest: hypreal_eq_minus_iff [THEN iffD2]) 
783 

784 
lemma NSDERIVD5: 

785 
"(NSDERIV f x :> D) ==> 

786 
(\<forall>u. u \<approx> hypreal_of_real x > 

787 
( *f* (%z. f z  f x)) u \<approx> hypreal_of_real D * (u  hypreal_of_real x))" 

788 
apply (auto simp add: NSDERIV_iff2) 

789 
apply (case_tac "u = hypreal_of_real x", auto) 

790 
apply (drule_tac x = u in spec, auto) 

791 
apply (drule_tac c = "u  hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1) 

792 
apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1]) 

793 
apply (subgoal_tac [2] "( *f* (%z. zx)) u \<noteq> (0::hypreal) ") 

20563  794 
apply (auto simp add: 
19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

795 
approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]] 
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

796 
Infinitesimal_subset_HFinite [THEN subsetD]) 
14477  797 
done 
798 

799 
lemma NSDERIVD4: 

800 
"(NSDERIV f x :> D) ==> 

801 
(\<forall>h \<in> Infinitesimal. 

802 
(( *f* f)(hypreal_of_real x + h)  

803 
hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" 

804 
apply (auto simp add: nsderiv_def) 

805 
apply (case_tac "h = (0::hypreal) ") 

806 
apply (auto simp add: diff_minus) 

807 
apply (drule_tac x = h in bspec) 

808 
apply (drule_tac [2] c = h in approx_mult1) 

809 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 

15539  810 
simp add: diff_minus) 
14477  811 
done 
812 

813 
lemma NSDERIVD3: 

814 
"(NSDERIV f x :> D) ==> 

815 
(\<forall>h \<in> Infinitesimal  {0}. 

816 
(( *f* f)(hypreal_of_real x + h)  

817 
hypreal_of_real (f x))\<approx> (hypreal_of_real D) * h)" 

818 
apply (auto simp add: nsderiv_def) 

819 
apply (rule ccontr, drule_tac x = h in bspec) 

820 
apply (drule_tac [2] c = h in approx_mult1) 

821 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 

15539  822 
simp add: mult_assoc diff_minus) 
14477  823 
done 
824 

825 
text{*Now equivalence between NSDERIV and DERIV*} 

826 
lemma NSDERIV_DERIV_iff: "(NSDERIV f x :> D) = (DERIV f x :> D)" 

827 
by (simp add: deriv_def NSDERIV_NSLIM_iff LIM_NSLIM_iff) 

828 

15228  829 
text{*Differentiability implies continuity 
830 
nice and simple "algebraic" proof*} 

14477  831 
lemma NSDERIV_isNSCont: "NSDERIV f x :> D ==> isNSCont f x" 
832 
apply (auto simp add: nsderiv_def isNSCont_NSLIM_iff NSLIM_def) 

833 
apply (drule approx_minus_iff [THEN iffD1]) 

834 
apply (drule hypreal_not_eq_minus_iff [THEN iffD1]) 

20563  835 
apply (drule_tac x = "xa  hypreal_of_real x" in bspec) 
15228  836 
prefer 2 apply (simp add: add_assoc [symmetric]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

837 
apply (auto simp add: mem_infmal_iff [symmetric] add_commute) 
20563  838 
apply (drule_tac c = "xa  hypreal_of_real x" in approx_mult1) 
14477  839 
apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD] 
840 
simp add: mult_assoc) 

841 
apply (drule_tac x3=D in 

842 
HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult, 

843 
THEN mem_infmal_iff [THEN iffD1]]) 

15539  844 
apply (auto simp add: mult_commute 
14477  845 
intro: approx_trans approx_minus_iff [THEN iffD2]) 
846 
done 

847 

848 
text{*Now Sandard proof*} 

849 
lemma DERIV_isCont: "DERIV f x :> D ==> isCont f x" 

15228  850 
by (simp add: NSDERIV_DERIV_iff [symmetric] isNSCont_isCont_iff [symmetric] 
14477  851 
NSDERIV_isNSCont) 
852 

853 

15228  854 
text{*Differentiation rules for combinations of functions 
14477  855 
follow from clear, straightforard, algebraic 
15228  856 
manipulations*} 
14477  857 
text{*Constant function*} 
858 

859 
(* use simple constant nslimit theorem *) 

15228  860 
lemma NSDERIV_const [simp]: "(NSDERIV (%x. k) x :> 0)" 
14477  861 
by (simp add: NSDERIV_NSLIM_iff) 
862 

15228  863 
lemma DERIV_const [simp]: "(DERIV (%x. k) x :> 0)" 
14477  864 
by (simp add: NSDERIV_DERIV_iff [symmetric]) 
865 

15228  866 
text{*Sum of functions proved easily*} 
14477  867 

868 

869 
lemma NSDERIV_add: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

870 
==> NSDERIV (%x. f x + g x) x :> Da + Db" 

871 
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) 

20563  872 
apply (auto simp add: add_divide_distrib diff_divide_distrib dest!: spec) 
14477  873 
apply (drule_tac b = "hypreal_of_real Da" and d = "hypreal_of_real Db" in approx_add) 
20563  874 
apply (auto simp add: diff_def add_ac) 
14477  875 
done 
876 

877 
(* Standard theorem *) 

878 
lemma DERIV_add: "[ DERIV f x :> Da; DERIV g x :> Db ] 

879 
==> DERIV (%x. f x + g x) x :> Da + Db" 

880 
apply (simp add: NSDERIV_add NSDERIV_DERIV_iff [symmetric]) 

881 
done 

882 

15228  883 
text{*Product of functions  Proof is trivial but tedious 
884 
and long due to rearrangement of terms*} 

14477  885 

20563  886 
lemma lemma_nsderiv1: "((a::hypreal)*b)  (c*d) = (b*(a  c)) + (c*(b  d))" 
887 
by (simp add: right_diff_distrib) 

14477  888 

20563  889 
lemma lemma_nsderiv2: "[ (x  y) / z = hypreal_of_real D + yb; z \<noteq> 0; 
14477  890 
z \<in> Infinitesimal; yb \<in> Infinitesimal ] 
20563  891 
==> x  y \<approx> 0" 
14477  892 
apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption) 
20563  893 
apply (erule_tac V = "(x  y) / z = hypreal_of_real D + yb" in thin_rl) 
14477  894 
apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add 
15539  895 
simp add: mult_assoc mem_infmal_iff [symmetric]) 
14477  896 
apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) 
897 
done 

898 

899 

900 
lemma NSDERIV_mult: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

901 
==> NSDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" 

902 
apply (auto simp add: NSDERIV_NSLIM_iff NSLIM_def) 

903 
apply (auto dest!: spec 

19023
5652a536b7e8
* include generalised MVT in HyperReal (contributed by Benjamin Porter)
kleing
parents:
17318
diff
changeset

904 
simp add: starfun_lambda_cancel lemma_nsderiv1) 
20563  905 
apply (simp (no_asm) add: add_divide_distrib diff_divide_distrib) 
14477  906 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2])+ 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

907 
apply (auto simp add: times_divide_eq_right [symmetric] 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

908 
simp del: times_divide_eq) 
20563  909 
apply (drule_tac D = Db in lemma_nsderiv2, assumption+) 
910 
apply (drule_tac 

15228  911 
approx_minus_iff [THEN iffD2, THEN bex_Infinitesimal_iff2 [THEN iffD2]]) 
912 
apply (auto intro!: approx_add_mono1 

14477  913 
simp add: left_distrib right_distrib mult_commute add_assoc) 
15228  914 
apply (rule_tac b1 = "hypreal_of_real Db * hypreal_of_real (f x)" 
14477  915 
in add_commute [THEN subst]) 
15228  916 
apply (auto intro!: Infinitesimal_add_approx_self2 [THEN approx_sym] 
917 
Infinitesimal_add Infinitesimal_mult 

918 
Infinitesimal_hypreal_of_real_mult 

14477  919 
Infinitesimal_hypreal_of_real_mult2 
920 
simp add: add_assoc [symmetric]) 

921 
done 

922 

923 
lemma DERIV_mult: 

15228  924 
"[ DERIV f x :> Da; DERIV g x :> Db ] 
14477  925 
==> DERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))" 
926 
by (simp add: NSDERIV_mult NSDERIV_DERIV_iff [symmetric]) 

927 

928 
text{*Multiplying by a constant*} 

929 
lemma NSDERIV_cmult: "NSDERIV f x :> D 

930 
==> NSDERIV (%x. c * f x) x :> c*D" 

15228  931 
apply (simp only: times_divide_eq_right [symmetric] NSDERIV_NSLIM_iff 
20563  932 
minus_mult_right right_diff_distrib [symmetric]) 
14477  933 
apply (erule NSLIM_const [THEN NSLIM_mult]) 
934 
done 

935 

936 
(* let's do the standard proof though theorem *) 

937 
(* LIM_mult2 follows from a NS proof *) 

938 

939 
lemma DERIV_cmult: 

940 
"DERIV f x :> D ==> DERIV (%x. c * f x) x :> c*D" 

15228  941 
apply (simp only: deriv_def times_divide_eq_right [symmetric] 
20563  942 
NSDERIV_NSLIM_iff minus_mult_right right_diff_distrib [symmetric]) 
14477  943 
apply (erule LIM_const [THEN LIM_mult2]) 
944 
done 

945 

946 
text{*Negation of function*} 

947 
lemma NSDERIV_minus: "NSDERIV f x :> D ==> NSDERIV (%x. (f x)) x :> D" 

948 
proof (simp add: NSDERIV_NSLIM_iff) 

20563  949 
assume "(\<lambda>h. (f (x + h)  f x) / h)  0 NS> D" 
950 
hence deriv: "(\<lambda>h.  ((f(x+h)  f x) / h))  0 NS>  D" 

14477  951 
by (rule NSLIM_minus) 
20563  952 
have "\<forall>h.  ((f (x + h)  f x) / h) = ( f (x + h) + f x) / h" 
15228  953 
by (simp add: minus_divide_left) 
14477  954 
with deriv 
955 
show "(\<lambda>h. ( f (x + h) + f x) / h)  0 NS>  D" by simp 

956 
qed 

957 

958 

959 
lemma DERIV_minus: "DERIV f x :> D ==> DERIV (%x. (f x)) x :> D" 

960 
by (simp add: NSDERIV_minus NSDERIV_DERIV_iff [symmetric]) 

961 

962 
text{*Subtraction*} 

963 
lemma NSDERIV_add_minus: "[ NSDERIV f x :> Da; NSDERIV g x :> Db ] ==> NSDERIV (%x. f x + g x) x :> Da + Db" 

964 
by (blast dest: NSDERIV_add NSDERIV_minus) 

965 

966 
lemma DERIV_add_minus: "[ DERIV f x :> Da; DERIV g x :> Db ] ==> DERIV (%x. f x + g x) x :> Da + Db" 

967 
by (blast dest: DERIV_add DERIV_minus) 

968 

969 
lemma NSDERIV_diff: 

970 
"[ NSDERIV f x :> Da; NSDERIV g x :> Db ] 

971 
==> NSDERIV (%x. f x  g x) x :> DaDb" 

972 
apply (simp add: diff_minus) 

973 
apply (blast intro: NSDERIV_add_minus) 

974 
done 

975 

976 
lemma DERIV_diff: 

977 
"[ DERIV f x :> Da; DERIV g x :> Db ] 

978 
==> DERIV (%x. f x  g x) x :> DaDb" 

979 
apply (simp add: diff_minus) 

980 
apply (blast intro: DERIV_add_minus) 

981 
done 

982 

15228  983 
text{*(NS) Increment*} 
14477  984 
lemma incrementI: 
985 
"f NSdifferentiable x ==> 

20563  986 
increment f x h = ( *f* f) (hypreal_of_real(x) + h)  
987 
hypreal_of_real (f x)" 

14477  988 
by (simp add: increment_def) 
989 

990 
lemma incrementI2: "NSDERIV f x :> D ==> 

20563  991 
increment f x h = ( *f* f) (hypreal_of_real(x) + h)  
992 
hypreal_of_real (f x)" 

14477  993 
apply (erule NSdifferentiableI [THEN incrementI]) 
994 
done 

995 

996 
(* The Increment theorem  Keisler p. 65 *) 

997 
lemma increment_thm: "[ NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 ] 

998 
==> \<exists>e \<in> Infinitesimal. increment f x h = hypreal_of_real(D)*h + e*h" 

999 
apply (frule_tac h = h in incrementI2, simp add: nsderiv_def) 

1000 
apply (drule bspec, auto) 

15228  1001 
apply (drule bex_Infinitesimal_iff2 [THEN iffD2], clarify) 
1002 
apply (frule_tac b1 = "hypreal_of_real (D) + y" 

14477  1003 
in hypreal_mult_right_cancel [THEN iffD2]) 
20563  1004 
apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h)  hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl) 
14477  1005 
apply assumption 
15539  1006 
apply (simp add: times_divide_eq_right [symmetric]) 
14477  1007 
apply (auto simp add: left_distrib) 
1008 
done 

15228  1009 

14477  1010 
lemma increment_thm2: 
1011 
"[ NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 ] 

1012 
==> \<exists>e \<in> Infinitesimal. increment f x h = 

1013 
hypreal_of_real(D)*h + e*h" 

1014 
by (blast dest!: mem_infmal_iff [THEN iffD2] intro!: increment_thm) 

1015 

1016 

1017 
lemma increment_approx_zero: "[ NSDERIV f x :> D; h \<approx> 0; h \<noteq> 0 ] 

1018 
==> increment f x h \<approx> 0" 

15228  1019 
apply (drule increment_thm2, 
14477  1020 
auto intro!: Infinitesimal_HFinite_mult2 HFinite_add simp add: left_distrib [symmetric] mem_infmal_iff [symmetric]) 
1021 
apply (erule Infinitesimal_subset_HFinite [THEN subsetD]) 

1022 
done 

1023 

1024 
text{* Similarly to the above, the chain rule admits an entirely 

1025 
straightforward derivation. Compare this with Harrison's 

1026 
HOL proof of the chain rule, which proved to be trickier and 

1027 
required an alternative characterisation of differentiability 

1028 
the socalled Carathedory derivative. Our main problem is 

1029 
manipulation of terms.*} 

1030 

1031 

1032 
(* lemmas *) 

1033 
lemma NSDERIV_zero: 

1034 
"[ NSDERIV g x :> D; 

1035 
( *f* g) (hypreal_of_real(x) + xa) = hypreal_of_real(g x); 

1036 
xa \<in> Infinitesimal; 

1037 
xa \<noteq> 0 

1038 
] ==> D = 0" 

1039 
apply (simp add: nsderiv_def) 

1040 
apply (drule bspec, auto) 

1041 
done 

1042 

1043 
(* can be proved differently using NSLIM_isCont_iff *) 

1044 
lemma NSDERIV_approx: 

1045 
"[ NSDERIV f x :> D; h \<in> Infinitesimal; h \<noteq> 0 ] 

20563  1046 
==> ( *f* f) (hypreal_of_real(x) + h)  hypreal_of_real(f x) \<approx> 0" 
14477  1047 
apply (simp add: nsderiv_def) 
1048 
apply (simp add: mem_infmal_iff [symmetric]) 

1049 
apply (rule Infinitesimal_ratio) 

1050 
apply (rule_tac [3] approx_hypreal_of_real_HFinite, auto) 

1051 
done 

1052 

1053 
(* 

1054 
from one version of differentiability 

1055 

1056 
f(x)  f(a) 

1057 
 \<approx> Db 

1058 
x  a 

1059 
*) 

1060 
lemma NSDERIVD1: "[ NSDERIV f (g x) :> Da; 

1061 
( *f* g) (hypreal_of_real(x) + xa) \<noteq> hypreal_of_real (g x); 

1062 
( *f* g) (hypreal_of_real(x) + xa) \<approx> hypreal_of_real (g x) 

1063 
] ==> (( *f* f) (( *f* g) (hypreal_of_real(x) + xa)) 

20563  1064 
 hypreal_of_real (f (g x))) 
1065 
/ (( *f* g) (hypreal_of_real(x) + xa)  hypreal_of_real (g x)) 

14477  1066 
\<approx> hypreal_of_real(Da)" 
1067 
by (auto simp add: NSDERIV_NSLIM_iff2 NSLIM_def diff_minus [symmetric]) 

1068 

1069 
(* 

1070 
from other version of differentiability 

1071 

1072 
f(x + h)  f(x) 

1073 
 \<approx> Db 

1074 
h 

1075 
*) 

1076 
lemma NSDERIVD2: "[ NSDERIV g x :> Db; xa \<in> Infinitesimal; xa \<noteq> 0 ] 

20563  1077 
==> (( *f* g) (hypreal_of_real(x) + xa)  hypreal_of_real(g x)) / xa 
14477  1078 
\<approx> hypreal_of_real(Db)" 
1079 
by (auto simp add: NSDERIV_NSLIM_iff NSLIM_def mem_infmal_iff starfun_lambda_cancel) 

1080 

1081 
lemma lemma_chain: "(z::hypreal) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)" 

1082 
by auto 

1083 

15228  1084 
text{*This proof uses both definitions of differentiability.*} 
14477  1085 
lemma NSDERIV_chain: "[ NSDERIV f (g x) :> Da; NSDERIV g x :> Db ] 
1086 
==> NSDERIV (f o g) x :> Da * Db" 

1087 
apply (simp (no_asm_simp) add: NSDERIV_NSLIM_iff NSLIM_def 

1088 
mem_infmal_iff [symmetric]) 

1089 
apply clarify 

1090 
apply (frule_tac f = g in NSDERIV_approx) 

1091 
apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric]) 

1092 
apply (case_tac "( *f* g) (hypreal_of_real (x) + xa) = hypreal_of_real (g x) ") 

1093 
apply (drule_tac g = g in NSDERIV_zero) 

1094 
apply (auto simp add: divide_inverse) 

20563  1095 
apply (rule_tac z1 = "( *f* g) (hypreal_of_real (x) + xa)  hypreal_of_real (g x) " and y1 = "inverse xa" in lemma_chain [THEN ssubst]) 
14477  1096 
apply (erule hypreal_not_eq_minus_iff [THEN iffD1]) 
1097 
apply (rule approx_mult_hypreal_of_real) 

1098 
apply (simp_all add: divide_inverse [symmetric]) 

1099 
apply (blast intro: NSDERIVD1 approx_minus_iff [THEN iffD2]) 

1100 
apply (blast intro: NSDERIVD2) 

1101 
done 

1102 

1103 
(* standard version *) 

1104 
lemma DERIV_chain: "[ DERIV f (g x) :> Da; DERIV g x :> Db ] ==> DERIV (f o g) x :> Da * Db" 

1105 
by (simp add: NSDERIV_DERIV_iff [symmetric] NSDERIV_chain) 

1106 

1107 
lemma DERIV_chain2: "[ DERIV f (g x) :> Da; DERIV g x :> Db ] ==> DERIV (%x. f (g x)) x :> Da * Db" 

1108 
by (auto dest: DERIV_chain simp add: o_def) 

1109 

1110 
text{*Differentiation of natural number powers*} 

15228  1111 
lemma NSDERIV_Id [simp]: "NSDERIV (%x. x) x :> 1" 
1112 
by (simp add: NSDERIV_NSLIM_iff NSLIM_def divide_self del: divide_self_if) 

14477  1113 

1114 
(*derivative of the identity function*) 

15228  1115 
lemma DERIV_Id [simp]: "DERIV (%x. x) x :> 1" 
14477  1116 
by (simp add: NSDERIV_DERIV_iff [symmetric]) 
1117 

1118 
lemmas isCont_Id = DERIV_Id [THEN DERIV_isCont, standard] 

1119 

1120 
(*derivative of linear multiplication*) 

15228  1121 
lemma DERIV_cmult_Id [simp]: "DERIV (op * c) x :> c" 
14477  1122 
by (cut_tac c = c and x = x in DERIV_Id [THEN DERIV_cmult], simp) 
1123 

15228  1124 
lemma NSDERIV_cmult_Id [simp]: "NSDERIV (op * c) x :> c" 
14477  1125 
by (simp add: NSDERIV_DERIV_iff) 
1126 

1127 
lemma DERIV_pow: "DERIV (%x. x ^ n) x :> real n * (x ^ (n  Suc 0))" 

15251  1128 
apply (induct "n") 
14477  1129 
apply (drule_tac [2] DERIV_Id [THEN DERIV_mult]) 
1130 
apply (auto simp add: real_of_nat_Suc left_distrib) 

1131 
apply (case_tac "0 < n") 

1132 
apply (drule_tac x = x in realpow_minus_mult) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1133 
apply (auto simp add: mult_assoc add_commute) 
14477  1134 
done 
1135 

1136 
(* NS version *) 

1137 
lemma NSDERIV_pow: "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n  Suc 0))" 

1138 
by (simp add: NSDERIV_DERIV_iff DERIV_pow) 

1139 

15228  1140 
text{*Power of 1*} 
14477  1141 

1142 
(*Can't get rid of x \<noteq> 0 because it isn't continuous at zero*) 

1143 
lemma NSDERIV_inverse: 

1144 
"x \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> ( (inverse x ^ Suc (Suc 0)))" 

1145 
apply (simp add: nsderiv_def) 

15228  1146 
apply (rule ballI, simp, clarify) 
20563  1147 
apply (frule (1) Infinitesimal_add_not_zero) 
1148 
apply (simp add: add_commute) 

1149 
(*apply (auto simp add: starfun_inverse_inverse realpow_two 

1150 
simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])*) 

14477  1151 
apply (simp add: inverse_add inverse_mult_distrib [symmetric] 
20563  1152 
inverse_minus_eq [symmetric] add_ac mult_ac diff_def 
15228  1153 
del: inverse_mult_distrib inverse_minus_eq 
14477  1154 
minus_mult_left [symmetric] minus_mult_right [symmetric]) 
1155 
apply (simp (no_asm_simp) add: mult_assoc [symmetric] right_distrib 

1156 
del: minus_mult_left [symmetric] minus_mult_right [symmetric]) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1157 
apply (rule_tac y = "inverse ( hypreal_of_real x * hypreal_of_real x)" in approx_trans) 
14477  1158 
apply (rule inverse_add_Infinitesimal_approx2) 
15228  1159 
apply (auto dest!: hypreal_of_real_HFinite_diff_Infinitesimal 
14477  1160 
simp add: inverse_minus_eq [symmetric] HFinite_minus_iff) 
1161 
apply (rule Infinitesimal_HFinite_mult2, auto) 

1162 
done 

1163 

1164 

1165 

1166 

1167 
lemma DERIV_inverse: "x \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> ((inverse x ^ Suc (Suc 0)))" 

1168 
by (simp add: NSDERIV_inverse NSDERIV_DERIV_iff [symmetric] del: realpow_Suc) 

1169 

1170 
text{*Derivative of inverse*} 

1171 
lemma DERIV_inverse_fun: "[ DERIV f x :> d; f(x) \<noteq> 0 ] 

1172 
==> DERIV (%x. inverse(f x)) x :> ( (d * inverse(f(x) ^ Suc (Suc 0))))" 

1173 
apply (simp only: mult_commute [of d] minus_mult_left power_inverse) 

1174 
apply (fold o_def) 

1175 
apply (blast intro!: DERIV_chain DERIV_inverse) 

1176 
done 

1177 

1178 
lemma NSDERIV_inverse_fun: "[ NSDERIV f x :> d; f(x) \<noteq> 0 ] 

1179 
==> NSDERIV (%x. inverse(f x)) x :> ( (d * inverse(f(x) ^ Suc (Suc 0))))" 

1180 
by (simp add: NSDERIV_DERIV_iff DERIV_inverse_fun del: realpow_Suc) 

1181 

1182 
text{*Derivative of quotient*} 

1183 
lemma DERIV_quotient: "[ DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 ] 

20563  1184 
==> DERIV (%y. f(y) / (g y)) x :> (d*g(x)  (e*f(x))) / (g(x) ^ Suc (Suc 0))" 
14477  1185 
apply (drule_tac f = g in DERIV_inverse_fun) 
1186 
apply (drule_tac [2] DERIV_mult) 

1187 
apply (assumption+) 

1188 
apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 

20563  1189 
mult_ac diff_def 
14477  1190 
del: realpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric]) 
1191 
done 

1192 

1193 
lemma NSDERIV_quotient: "[ NSDERIV f x :> d; DERIV g x :> e; g(x) \<noteq> 0 ] 

1194 
==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) 

20563  1195 
 (e*f(x))) / (g(x) ^ Suc (Suc 0))" 
14477  1196 
by (simp add: NSDERIV_DERIV_iff DERIV_quotient del: realpow_Suc) 
1197 

1198 
(*  *) 

1199 
(* Caratheodory formulation of derivative at a point: standard proof *) 

1200 
(*  *) 

1201 

1202 
lemma CARAT_DERIV: 

1203 
"(DERIV f x :> l) = 

1204 
(\<exists>g. (\<forall>z. f z  f x = g z * (zx)) & isCont g x & g x = l)" 

1205 
(is "?lhs = ?rhs") 

1206 
proof 

1207 
assume der: "DERIV f x :> l" 

1208 
show "\<exists>g. (\<forall>z. f z  f x = g z * (zx)) \<and> isCont g x \<and> g x = l" 

1209 
proof (intro exI conjI) 

1210 
let ?g = "(%z. if z = x then l else (f z  f x) / (zx))" 

15539  1211 
show "\<forall>z. f z  f x = ?g z * (zx)" by (simp) 
15228  1212 
show "isCont ?g x" using der 
1213 
by (simp add: isCont_iff DERIV_iff diff_minus 

14477  1214 
cong: LIM_equal [rule_format]) 
1215 
show "?g x = l" by simp 

1216 
qed 

1217 
next 

1218 
assume "?rhs" 

15228  1219 
then obtain g where 
14477  1220 
"(\<forall>z. f z  f x = g z * (zx))" and "isCont g x" and "g x = l" by blast 
15228  1221 
thus "(DERIV f x :> l)" 
1222 
by (auto simp add: isCont_iff DERIV_iff diff_minus 

14477  1223 
cong: LIM_equal [rule_format]) 
1224 
qed 

1225 

1226 

1227 
lemma CARAT_NSDERIV: "NSDERIV f x :> l ==> 

1228 
\<exists>g. (\<forall>z. f z  f x = g z * (zx)) & isNSCont g x & g x = l" 

1229 
by (auto simp add: NSDERIV_DERIV_iff isNSCont_isCont_iff CARAT_DERIV) 

1230 

1231 
lemma hypreal_eq_minus_iff3: "(x = y + z) = (x + z = (y::hypreal))" 

1232 
by auto 

1233 

1234 
lemma CARAT_DERIVD: 

1235 
assumes all: "\<forall>z. f z  f x = g z * (zx)" 

1236 
and nsc: "isNSCont g x" 

1237 
shows "NSDERIV f x :> g x" 

1238 
proof  

1239 
from nsc 

1240 
have "\<forall>w. w \<noteq> hypreal_of_real x \<and> w \<approx> hypreal_of_real x \<longrightarrow> 

1241 
( *f* g) w * (w  hypreal_of_real x) / (w  hypreal_of_real x) \<approx> 

15228  1242 
hypreal_of_real (g x)" 
14477  1243 
by (simp add: diff_minus isNSCont_def) 
1244 
thus ?thesis using all 

15228  1245 
by (simp add: NSDERIV_iff2 starfun_if_eq cong: if_cong) 
14477  1246 
qed 
1247 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1248 
text{*Lemmas about nested intervals and proof by bisection (cf.Harrison). 
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1249 
All considerably tidied by lcp.*} 
14477  1250 

1251 
lemma lemma_f_mono_add [rule_format (no_asm)]: "(\<forall>n. (f::nat=>real) n \<le> f (Suc n)) > f m \<le> f(m + no)" 

15251  1252 
apply (induct "no") 
14477  1253 
apply (auto intro: order_trans) 
1254 
done 

1255 

1256 
lemma f_inc_g_dec_Beq_f: "[ \<forall>n. f(n) \<le> f(Suc n); 

1257 
\<forall>n. g(Suc n) \<le> g(n); 

1258 
\<forall>n. f(n) \<le> g(n) ] 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

1259 
==> Bseq (f :: nat \<Rightarrow> real)" 
14477  1260 
apply (rule_tac k = "f 0" and K = "g 0" in BseqI2, rule allI) 
1261 
apply (induct_tac "n") 

1262 
apply (auto intro: order_trans) 

15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1263 
apply (rule_tac y = "g (Suc na)" in order_trans) 
14477  1264 
apply (induct_tac [2] "na") 
1265 
apply (auto intro: order_trans) 

1266 
done 

1267 

1268 
lemma f_inc_g_dec_Beq_g: "[ \<forall>n. f(n) \<le> f(Suc n); 

1269 
\<forall>n. g(Suc n) \<le> g(n); 

1270 
\<forall>n. f(n) \<le> g(n) ] 

20552
2c31dd358c21
generalized types of many constants to work over arbitrary vector spaces;
huffman
parents:
20432
diff
changeset

1271 
==> Bseq (g :: nat \<Rightarrow> real)" 
14477  1272 
apply (subst Bseq_minus_iff [symmetric]) 
15234
ec91a90c604e
simplification tweaks for better arithmetic reasoning
paulson
parents:
15228
diff
changeset

1273 
apply (rule_tac g = "%x.  (f x)" in f_inc_g_dec_Beq_f) 
14477  1274 
apply auto 
1275 
done 

cc61fd03e589
conversion of Hyperreal/Lim to newstyle
pa 