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