src/HOL/NSA/CLim.thy
author huffman
Thu Jul 03 17:47:22 2008 +0200 (2008-07-03)
changeset 27468 0783dd1dc13d
child 31338 d41a8ba25b67
permissions -rw-r--r--
move nonstandard analysis theories to NSA directory
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 \<noteq> (0::complex) \<Longrightarrow> (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: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>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@27468
    48
lemma LIM_Re: "f -- a --> L ==> (%x. Re(f x)) -- a --> Re(L)"
huffman@27468
    49
by (simp add: LIM_NSLIM_iff NSLIM_Re)
huffman@27468
    50
huffman@27468
    51
lemma LIM_Im: "f -- a --> L ==> (%x. Im(f x)) -- a --> Im(L)"
huffman@27468
    52
by (simp add: LIM_NSLIM_iff NSLIM_Im)
huffman@27468
    53
huffman@27468
    54
lemma LIM_cnj: "f -- a --> L ==> (%x. cnj (f x)) -- a --> cnj L"
huffman@27468
    55
by (simp add: LIM_def complex_cnj_diff [symmetric])
huffman@27468
    56
huffman@27468
    57
lemma LIM_cnj_iff: "((%x. cnj (f x)) -- a --> cnj L) = (f -- a --> L)"
huffman@27468
    58
by (simp add: LIM_def complex_cnj_diff [symmetric])
huffman@27468
    59
huffman@27468
    60
lemma starfun_norm: "( *f* (\<lambda>x. norm (f x))) = (\<lambda>x. hnorm (( *f* f) x))"
huffman@27468
    61
by transfer (rule refl)
huffman@27468
    62
huffman@27468
    63
lemma star_of_Re [simp]: "star_of (Re x) = hRe (star_of x)"
huffman@27468
    64
by transfer (rule refl)
huffman@27468
    65
huffman@27468
    66
lemma star_of_Im [simp]: "star_of (Im x) = hIm (star_of x)"
huffman@27468
    67
by transfer (rule refl)
huffman@27468
    68
huffman@27468
    69
text""
huffman@27468
    70
(** another equivalence result **)
huffman@27468
    71
lemma NSCLIM_NSCRLIM_iff:
huffman@27468
    72
   "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
huffman@27468
    73
by (simp add: NSLIM_def starfun_norm
huffman@27468
    74
    approx_approx_zero_iff [symmetric] approx_minus_iff [symmetric])
huffman@27468
    75
huffman@27468
    76
(** much, much easier standard proof **)
huffman@27468
    77
lemma CLIM_CRLIM_iff: "(f -- x --> L) = ((%y. cmod(f y - L)) -- x --> 0)"
huffman@27468
    78
by (simp add: LIM_def)
huffman@27468
    79
huffman@27468
    80
(* so this is nicer nonstandard proof *)
huffman@27468
    81
lemma NSCLIM_NSCRLIM_iff2:
huffman@27468
    82
     "(f -- x --NS> L) = ((%y. cmod(f y - L)) -- x --NS> 0)"
huffman@27468
    83
by (simp add: LIM_NSLIM_iff [symmetric] CLIM_CRLIM_iff)
huffman@27468
    84
huffman@27468
    85
lemma NSLIM_NSCRLIM_Re_Im_iff:
huffman@27468
    86
     "(f -- a --NS> L) = ((%x. Re(f x)) -- a --NS> Re(L) &
huffman@27468
    87
                            (%x. Im(f x)) -- a --NS> Im(L))"
huffman@27468
    88
apply (auto intro: NSLIM_Re NSLIM_Im)
huffman@27468
    89
apply (auto simp add: NSLIM_def starfun_Re starfun_Im)
huffman@27468
    90
apply (auto dest!: spec)
huffman@27468
    91
apply (simp add: hcomplex_approx_iff)
huffman@27468
    92
done
huffman@27468
    93
huffman@27468
    94
lemma LIM_CRLIM_Re_Im_iff:
huffman@27468
    95
     "(f -- a --> L) = ((%x. Re(f x)) -- a --> Re(L) &
huffman@27468
    96
                         (%x. Im(f x)) -- a --> Im(L))"
huffman@27468
    97
by (simp add: LIM_NSLIM_iff NSLIM_NSCRLIM_Re_Im_iff)
huffman@27468
    98
huffman@27468
    99
huffman@27468
   100
subsection{*Continuity*}
huffman@27468
   101
huffman@27468
   102
lemma NSLIM_isContc_iff:
huffman@27468
   103
     "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
huffman@27468
   104
by (rule NSLIM_h_iff)
huffman@27468
   105
huffman@27468
   106
subsection{*Functions from Complex to Reals*}
huffman@27468
   107
huffman@27468
   108
lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)"
huffman@27468
   109
by (auto intro: approx_hnorm
huffman@27468
   110
         simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] 
huffman@27468
   111
                    isNSCont_def)
huffman@27468
   112
huffman@27468
   113
lemma isContCR_cmod [simp]: "isCont cmod (a)"
huffman@27468
   114
by (simp add: isNSCont_isCont_iff [symmetric])
huffman@27468
   115
huffman@27468
   116
lemma isCont_Re: "isCont f a ==> isCont (%x. Re (f x)) a"
huffman@27468
   117
by (simp add: isCont_def LIM_Re)
huffman@27468
   118
huffman@27468
   119
lemma isCont_Im: "isCont f a ==> isCont (%x. Im (f x)) a"
huffman@27468
   120
by (simp add: isCont_def LIM_Im)
huffman@27468
   121
huffman@27468
   122
subsection{* Differentiation of Natural Number Powers*}
huffman@27468
   123
huffman@27468
   124
lemma CDERIV_pow [simp]:
huffman@27468
   125
     "DERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
huffman@27468
   126
apply (induct n)
huffman@27468
   127
apply (drule_tac [2] DERIV_ident [THEN DERIV_mult])
huffman@27468
   128
apply (auto simp add: left_distrib real_of_nat_Suc)
huffman@27468
   129
apply (case_tac "n")
huffman@27468
   130
apply (auto simp add: mult_ac add_commute)
huffman@27468
   131
done
huffman@27468
   132
huffman@27468
   133
text{*Nonstandard version*}
huffman@27468
   134
lemma NSCDERIV_pow:
huffman@27468
   135
     "NSDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
huffman@27468
   136
by (simp add: NSDERIV_DERIV_iff)
huffman@27468
   137
huffman@27468
   138
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
huffman@27468
   139
lemma NSCDERIV_inverse:
huffman@27468
   140
     "(x::complex) \<noteq> 0 ==> NSDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
huffman@27468
   141
unfolding numeral_2_eq_2
huffman@27468
   142
by (rule NSDERIV_inverse)
huffman@27468
   143
huffman@27468
   144
lemma CDERIV_inverse:
huffman@27468
   145
     "(x::complex) \<noteq> 0 ==> DERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
huffman@27468
   146
unfolding numeral_2_eq_2
huffman@27468
   147
by (rule DERIV_inverse)
huffman@27468
   148
huffman@27468
   149
huffman@27468
   150
subsection{*Derivative of Reciprocals (Function @{term inverse})*}
huffman@27468
   151
huffman@27468
   152
lemma CDERIV_inverse_fun:
huffman@27468
   153
     "[| DERIV f x :> d; f(x) \<noteq> (0::complex) |]
huffman@27468
   154
      ==> DERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
huffman@27468
   155
unfolding numeral_2_eq_2
huffman@27468
   156
by (rule DERIV_inverse_fun)
huffman@27468
   157
huffman@27468
   158
lemma NSCDERIV_inverse_fun:
huffman@27468
   159
     "[| NSDERIV f x :> d; f(x) \<noteq> (0::complex) |]
huffman@27468
   160
      ==> NSDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
huffman@27468
   161
unfolding numeral_2_eq_2
huffman@27468
   162
by (rule NSDERIV_inverse_fun)
huffman@27468
   163
huffman@27468
   164
huffman@27468
   165
subsection{* Derivative of Quotient*}
huffman@27468
   166
huffman@27468
   167
lemma CDERIV_quotient:
huffman@27468
   168
     "[| DERIV f x :> d; DERIV g x :> e; g(x) \<noteq> (0::complex) |]
huffman@27468
   169
       ==> DERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
huffman@27468
   170
unfolding numeral_2_eq_2
huffman@27468
   171
by (rule DERIV_quotient)
huffman@27468
   172
huffman@27468
   173
lemma NSCDERIV_quotient:
huffman@27468
   174
     "[| NSDERIV f x :> d; NSDERIV g x :> e; g(x) \<noteq> (0::complex) |]
huffman@27468
   175
       ==> NSDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
huffman@27468
   176
unfolding numeral_2_eq_2
huffman@27468
   177
by (rule NSDERIV_quotient)
huffman@27468
   178
huffman@27468
   179
huffman@27468
   180
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
huffman@27468
   181
huffman@27468
   182
lemma CARAT_CDERIVD:
huffman@27468
   183
     "(\<forall>z. f z - f x = g z * (z - x)) & isNSCont g x & g x = l
huffman@27468
   184
      ==> NSDERIV f x :> l"
huffman@27468
   185
by clarify (rule CARAT_DERIVD)
huffman@27468
   186
huffman@27468
   187
end