src/HOL/NSA/CLim.thy
 author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 31338 d41a8ba25b67 child 49962 a8cc904a6820 permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
1 (*  Title       : CLim.thy
2     Author      : Jacques D. Fleuriot
3     Copyright   : 2001 University of Edinburgh
4     Conversion to Isar and new proofs by Lawrence C Paulson, 2004
5 *)
7 header{*Limits, Continuity and Differentiation for Complex Functions*}
9 theory CLim
10 imports CStar
11 begin
13 (*not in simpset?*)
14 declare hypreal_epsilon_not_zero [simp]
16 (*??generalize*)
17 lemma lemma_complex_mult_inverse_squared [simp]:
18      "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
21 text{*Changing the quantified variable. Install earlier?*}
22 lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
23 apply auto
24 apply (drule_tac x="x+a" in spec)
26 done
28 lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
29 by (simp add: diff_eq_eq diff_minus [symmetric])
31 lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
32 apply auto
33 apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
34 done
37 subsection{*Limit of Complex to Complex Function*}
39 lemma NSLIM_Re: "f -- a --NS> L ==> (%x. Re(f x)) -- a --NS> Re(L)"
40 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
41               hRe_hcomplex_of_complex)
43 lemma NSLIM_Im: "f -- a --NS> L ==> (%x. Im(f x)) -- a --NS> Im(L)"
44 by (simp add: NSLIM_def starfunC_approx_Re_Im_iff
45               hIm_hcomplex_of_complex)
47 (** get this result easily now **)
48 lemma LIM_Re:
49   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
50   shows "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
51 by (simp add: LIM_NSLIM_iff NSLIM_Re)
53 lemma LIM_Im:
54   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
55   shows "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
56 by (simp add: LIM_NSLIM_iff NSLIM_Im)
58 lemma LIM_cnj:
59   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
60   shows "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
61 by (simp add: LIM_eq complex_cnj_diff [symmetric])
63 lemma LIM_cnj_iff:
64   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
65   shows "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
66 by (simp add: LIM_eq complex_cnj_diff [symmetric])
68 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
69 by transfer (rule refl)
71 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
72 by transfer (rule refl)
74 lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
75 by transfer (rule refl)
77 text""
78 (** another equivalence result **)
79 lemma NSCLIM_NSCRLIM_iff:
80    "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
81 by (simp add: NSLIM_def starfun_norm
82     approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
84 (** much, much easier standard proof **)
85 lemma CLIM_CRLIM_iff:
86   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
87   shows "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
90 (* so this is nicer nonstandard proof *)
91 lemma NSCLIM_NSCRLIM_iff2:
92      "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
93 by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
95 lemma NSLIM_NSCRLIM_Re_Im_iff:
96      "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
97                             (%x. Im(f x)) -- a --NS> Im(L))"
98 apply (auto intro: NSLIM_Re NSLIM_Im)
99 apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
100 apply (auto dest!: spec)
102 done
104 lemma LIM_CRLIM_Re_Im_iff:
105   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
106   shows "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
107                          (%x. Im(f x)) -- a --> Im(L))"
108 by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
111 subsection{*Continuity*}
113 lemma NSLIM_isContc_iff:
114      "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
115 by (rule NSLIM_h_iff)
117 subsection{*Functions from Complex to Reals*}
119 lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
120 by (auto intro: approx_hnorm
121          simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric]
122                     isNSCont_def)
124 lemma isContCR_cmod [simp]: "isCont cmod (a)"
125 by (simp add: isNSCont_isCont_iff [symmetric])
127 lemma isCont_Re:
128   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
129   shows "isCont f a ==> isCont (%x. Re (f x)) a"
130 by (simp add: isCont_def LIM_Re)
132 lemma isCont_Im:
133   fixes f :: "'a::real_normed_vector \<Rightarrow> complex"
134   shows "isCont f a ==> isCont (%x. Im (f x)) a"
135 by (simp add: isCont_def LIM_Im)
137 subsection{* Differentiation of Natural Number Powers*}
139 lemma CDERIV_pow [simp]:
140      "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
141 apply (induct n)
142 apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
143 apply (auto simp add: left_distrib real_of_nat_Suc)
144 apply (case_tac "n")
146 done
148 text{*Nonstandard version*}
149 lemma NSCDERIV_pow:
150      "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
153 text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
154 lemma NSCDERIV_inverse:
155      "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
156 unfolding numeral_2_eq_2
157 by (rule NSDERIV_inverse)
159 lemma CDERIV_inverse:
160      "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
161 unfolding numeral_2_eq_2
162 by (rule DERIV_inverse)
165 subsection{*Derivative of Reciprocals (Function @{term inverse})*}
167 lemma CDERIV_inverse_fun:
168      "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
169       ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
170 unfolding numeral_2_eq_2
171 by (rule DERIV_inverse_fun)
173 lemma NSCDERIV_inverse_fun:
174      "[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
175       ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
176 unfolding numeral_2_eq_2
177 by (rule NSDERIV_inverse_fun)
180 subsection{* Derivative of Quotient*}
182 lemma CDERIV_quotient:
183      "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
184        ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
185 unfolding numeral_2_eq_2
186 by (rule DERIV_quotient)
188 lemma NSCDERIV_quotient:
189      "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
190        ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
191 unfolding numeral_2_eq_2
192 by (rule NSDERIV_quotient)
195 subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
197 lemma CARAT_CDERIVD:
198      "(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
199       ==> NSDERIV f x :> l"
200 by clarify (rule CARAT_DERIVD)
202 end