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