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 *)
     6 
     7 header{*Limits, Continuity and Differentiation for Complex Functions*}
     8 
     9 theory CLim
    10 imports CStar
    11 begin
    12 
    13 (*not in simpset?*)
    14 declare hypreal_epsilon_not_zero [simp]
    15 
    16 (*??generalize*)
    17 lemma lemma_complex_mult_inverse_squared [simp]:
    18      "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
    19 by (simp add: numeral_2_eq_2)
    20 
    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) 
    25 apply (simp add: diff_minus add_assoc) 
    26 done
    27 
    28 lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
    29 by (simp add: diff_eq_eq diff_minus [symmetric])
    30 
    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
    35 
    36 
    37 subsection{*Limit of Complex to Complex Function*}
    38 
    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)
    42 
    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)
    46 
    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)
    52 
    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)
    57 
    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])
    62 
    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])
    67 
    68 lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
    69 by transfer (rule refl)
    70 
    71 lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
    72 by transfer (rule refl)
    73 
    74 lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
    75 by transfer (rule refl)
    76 
    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])
    83 
    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)"
    88 by (simp add: LIM_eq)
    89 
    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)
    94 
    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)
   101 apply (simp add: hcomplex_approx_iff)
   102 done
   103 
   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)
   109 
   110 
   111 subsection{*Continuity*}
   112 
   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)
   116 
   117 subsection{*Functions from Complex to Reals*}
   118 
   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)
   123 
   124 lemma isContCR_cmod [simp]: "isCont cmod (a)"
   125 by (simp add: isNSCont_isCont_iff [symmetric])
   126 
   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)
   131 
   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)
   136 
   137 subsection{* Differentiation of Natural Number Powers*}
   138 
   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")
   145 apply (auto simp add: mult_ac add_commute)
   146 done
   147 
   148 text{*Nonstandard version*}
   149 lemma NSCDERIV_pow:
   150      "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
   151 by (simp add: NSDERIV_DERIV_iff)
   152 
   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)
   158 
   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)
   163 
   164 
   165 subsection{*Derivative of Reciprocals (Function @{term inverse})*}
   166 
   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)
   172 
   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)
   178 
   179 
   180 subsection{* Derivative of Quotient*}
   181 
   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)
   187 
   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)
   193 
   194 
   195 subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
   196 
   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)
   201 
   202 end