src/HOL/Complex/CLim.thy
author nipkow
Wed Aug 18 11:09:40 2004 +0200 (2004-08-18)
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15228 4d332d10fa3d
permissions -rw-r--r--
import -> imports
paulson@13957
     1
(*  Title       : CLim.thy
paulson@13957
     2
    Author      : Jacques D. Fleuriot
paulson@13957
     3
    Copyright   : 2001 University of Edinburgh
paulson@14469
     4
    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
paulson@13957
     5
*)
paulson@13957
     6
paulson@14469
     7
header{*Limits, Continuity and Differentiation for Complex Functions*}
paulson@14469
     8
nipkow@15131
     9
theory CLim
nipkow@15140
    10
imports CSeries
nipkow@15131
    11
begin
paulson@14405
    12
paulson@14405
    13
(*not in simpset?*)
paulson@14405
    14
declare hypreal_epsilon_not_zero [simp]
paulson@14405
    15
paulson@14405
    16
(*??generalize*)
paulson@14405
    17
lemma lemma_complex_mult_inverse_squared [simp]:
paulson@14405
    18
     "x \<noteq> (0::complex) \<Longrightarrow> (x * inverse(x) ^ 2) = inverse x"
paulson@14469
    19
by (simp add: numeral_2_eq_2)
paulson@14405
    20
paulson@14405
    21
text{*Changing the quantified variable. Install earlier?*}
obua@14738
    22
lemma all_shift: "(\<forall>x::'a::comm_ring_1. P x) = (\<forall>x. P (x-a))";
paulson@14405
    23
apply auto 
paulson@14405
    24
apply (drule_tac x="x+a" in spec) 
paulson@14405
    25
apply (simp add: diff_minus add_assoc) 
paulson@14405
    26
done
paulson@14405
    27
paulson@14405
    28
lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
paulson@14405
    29
by (simp add: diff_eq_eq diff_minus [symmetric])
paulson@14405
    30
paulson@14405
    31
lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
paulson@14405
    32
apply auto
paulson@14405
    33
apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
paulson@14405
    34
done
paulson@13957
    35
paulson@13957
    36
constdefs
paulson@13957
    37
paulson@14405
    38
  CLIM :: "[complex=>complex,complex,complex] => bool"
paulson@13957
    39
				("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
paulson@13957
    40
  "f -- a --C> L ==
paulson@14405
    41
     \<forall>r. 0 < r -->
paulson@14405
    42
	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
paulson@13957
    43
			  --> cmod(f x - L) < r)))"
paulson@13957
    44
paulson@14405
    45
  NSCLIM :: "[complex=>complex,complex,complex] => bool"
paulson@13957
    46
			      ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
paulson@14405
    47
  "f -- a --NSC> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
paulson@14405
    48
           		         x @c= hcomplex_of_complex a
paulson@14405
    49
                                   --> ( *fc* f) x @c= hcomplex_of_complex L))"
paulson@13957
    50
paulson@13957
    51
  (* f: C --> R *)
paulson@14405
    52
  CRLIM :: "[complex=>real,complex,real] => bool"
paulson@13957
    53
				("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
paulson@13957
    54
  "f -- a --CR> L ==
paulson@14405
    55
     \<forall>r. 0 < r -->
paulson@14405
    56
	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
paulson@13957
    57
			  --> abs(f x - L) < r)))"
paulson@13957
    58
paulson@14405
    59
  NSCRLIM :: "[complex=>real,complex,real] => bool"
paulson@13957
    60
			      ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
paulson@14405
    61
  "f -- a --NSCR> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
paulson@14405
    62
           		         x @c= hcomplex_of_complex a
paulson@14405
    63
                                   --> ( *fcR* f) x @= hypreal_of_real L))"
paulson@13957
    64
paulson@13957
    65
paulson@14405
    66
  isContc :: "[complex=>complex,complex] => bool"
paulson@14405
    67
  "isContc f a == (f -- a --C> (f a))"
paulson@13957
    68
paulson@13957
    69
  (* NS definition dispenses with limit notions *)
paulson@14405
    70
  isNSContc :: "[complex=>complex,complex] => bool"
paulson@14405
    71
  "isNSContc f a == (\<forall>y. y @c= hcomplex_of_complex a -->
paulson@13957
    72
			   ( *fc* f) y @c= hcomplex_of_complex (f a))"
paulson@13957
    73
paulson@14405
    74
  isContCR :: "[complex=>real,complex] => bool"
paulson@14405
    75
  "isContCR f a == (f -- a --CR> (f a))"
paulson@13957
    76
paulson@13957
    77
  (* NS definition dispenses with limit notions *)
paulson@14405
    78
  isNSContCR :: "[complex=>real,complex] => bool"
paulson@14405
    79
  "isNSContCR f a == (\<forall>y. y @c= hcomplex_of_complex a -->
paulson@13957
    80
			   ( *fcR* f) y @= hypreal_of_real (f a))"
paulson@13957
    81
paulson@13957
    82
  (* differentiation: D is derivative of function f at x *)
paulson@14405
    83
  cderiv:: "[complex=>complex,complex,complex] => bool"
paulson@13957
    84
			    ("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
paulson@13957
    85
  "CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
paulson@13957
    86
paulson@14405
    87
  nscderiv :: "[complex=>complex,complex,complex] => bool"
paulson@13957
    88
			    ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
paulson@14405
    89
  "NSCDERIV f x :> D == (\<forall>h \<in> CInfinitesimal - {0}.
paulson@13957
    90
			      (( *fc* f)(hcomplex_of_complex x + h)
paulson@13957
    91
        			 - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)"
paulson@13957
    92
paulson@14405
    93
  cdifferentiable :: "[complex=>complex,complex] => bool"
paulson@14405
    94
                     (infixl "cdifferentiable" 60)
paulson@14405
    95
  "f cdifferentiable x == (\<exists>D. CDERIV f x :> D)"
paulson@14405
    96
paulson@14405
    97
  NSCdifferentiable :: "[complex=>complex,complex] => bool"
paulson@14405
    98
                        (infixl "NSCdifferentiable" 60)
paulson@14405
    99
  "f NSCdifferentiable x == (\<exists>D. NSCDERIV f x :> D)"
paulson@14405
   100
paulson@14405
   101
paulson@14405
   102
  isUContc :: "(complex=>complex) => bool"
paulson@14405
   103
  "isUContc f ==  (\<forall>r. 0 < r -->
paulson@14405
   104
		      (\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
paulson@14405
   105
			    --> cmod(f x - f y) < r)))"
paulson@14405
   106
paulson@14405
   107
  isNSUContc :: "(complex=>complex) => bool"
paulson@14405
   108
  "isNSUContc f == (\<forall>x y. x @c= y --> ( *fc* f) x @c= ( *fc* f) y)"
paulson@14405
   109
paulson@14405
   110
paulson@14405
   111
paulson@14405
   112
subsection{*Limit of Complex to Complex Function*}
paulson@14405
   113
paulson@14405
   114
lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
paulson@14469
   115
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
paulson@14469
   116
              hRe_hcomplex_of_complex)
paulson@14469
   117
paulson@14405
   118
paulson@14469
   119
lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
paulson@14469
   120
by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff 
paulson@14469
   121
              hIm_hcomplex_of_complex)
paulson@14405
   122
paulson@14405
   123
lemma CLIM_NSCLIM:
paulson@14405
   124
      "f -- x --C> L ==> f -- x --NSC> L"
paulson@14469
   125
apply (simp add: CLIM_def NSCLIM_def capprox_def, auto)
paulson@14405
   126
apply (rule_tac z = xa in eq_Abs_hcomplex)
paulson@14405
   127
apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff 
paulson@14405
   128
         CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
paulson@14405
   129
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
paulson@14405
   130
apply (drule_tac x = u in spec, auto)
paulson@14405
   131
apply (drule_tac x = s in spec, auto, ultra)
paulson@14405
   132
apply (drule sym, auto)
paulson@14405
   133
done
paulson@14405
   134
paulson@14405
   135
lemma eq_Abs_hcomplex_ALL:
paulson@14405
   136
     "(\<forall>t. P t) = (\<forall>X. P (Abs_hcomplex(hcomplexrel `` {X})))"
paulson@14405
   137
apply auto
paulson@14405
   138
apply (rule_tac z = t in eq_Abs_hcomplex, auto)
paulson@14405
   139
done
paulson@14405
   140
paulson@14405
   141
lemma lemma_CLIM:
paulson@14405
   142
     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
paulson@14405
   143
         cmod (xa - x) < s  & r \<le> cmod (f xa - L))
paulson@14405
   144
      ==> \<forall>(n::nat). \<exists>xa.  xa \<noteq> x &
paulson@14405
   145
              cmod(xa - x) < inverse(real(Suc n)) & r \<le> cmod(f xa - L)"
paulson@14405
   146
apply clarify
paulson@14405
   147
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
paulson@14405
   148
done
paulson@14405
   149
paulson@14405
   150
paulson@14405
   151
lemma lemma_skolemize_CLIM2:
paulson@14405
   152
     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
paulson@14405
   153
         cmod (xa - x) < s  & r \<le> cmod (f xa - L))
paulson@14405
   154
      ==> \<exists>X. \<forall>(n::nat). X n \<noteq> x &
paulson@14405
   155
                cmod(X n - x) < inverse(real(Suc n)) & r \<le> cmod(f (X n) - L)"
paulson@14405
   156
apply (drule lemma_CLIM)
paulson@14405
   157
apply (drule choice, blast)
paulson@14405
   158
done
paulson@14405
   159
paulson@14405
   160
lemma lemma_csimp:
paulson@14405
   161
     "\<forall>n. X n \<noteq> x &
paulson@14405
   162
          cmod (X n - x) < inverse (real(Suc n)) &
paulson@14405
   163
          r \<le> cmod (f (X n) - L) ==>
paulson@14405
   164
          \<forall>n. cmod (X n - x) < inverse (real(Suc n))"
paulson@14405
   165
by auto
paulson@14405
   166
paulson@14405
   167
lemma NSCLIM_CLIM:
paulson@14405
   168
     "f -- x --NSC> L ==> f -- x --C> L"
paulson@14469
   169
apply (simp add: CLIM_def NSCLIM_def)
paulson@14405
   170
apply (rule ccontr) 
paulson@14469
   171
apply (auto simp add: eq_Abs_hcomplex_ALL starfunC 
paulson@14469
   172
            CInfinitesimal_capprox_minus [symmetric] hcomplex_diff
paulson@14469
   173
            CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
paulson@14469
   174
            Infinitesimal_FreeUltrafilterNat_iff hcmod)
paulson@14405
   175
apply (simp add: linorder_not_less)
paulson@14405
   176
apply (drule lemma_skolemize_CLIM2, safe)
paulson@14405
   177
apply (drule_tac x = X in spec, auto)
paulson@14405
   178
apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
paulson@14469
   179
apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
paulson@14469
   180
            Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod,  blast)
paulson@14405
   181
apply (drule_tac x = r in spec, clarify)
paulson@14405
   182
apply (drule FreeUltrafilterNat_all, ultra, arith)
paulson@14405
   183
done
paulson@14405
   184
paulson@14405
   185
paulson@14405
   186
text{*First key result*}
paulson@14405
   187
theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)"
paulson@14405
   188
by (blast intro: CLIM_NSCLIM NSCLIM_CLIM)
paulson@14405
   189
paulson@14405
   190
paulson@14405
   191
subsection{*Limit of Complex to Real Function*}
paulson@14405
   192
paulson@14405
   193
lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
paulson@14469
   194
apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto)
paulson@14405
   195
apply (rule_tac z = xa in eq_Abs_hcomplex)
paulson@14469
   196
apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff
paulson@14469
   197
              CInfinitesimal_hcmod_iff hcmod hypreal_diff
paulson@14469
   198
              Infinitesimal_FreeUltrafilterNat_iff
paulson@14469
   199
              Infinitesimal_approx_minus [symmetric] hypreal_of_real_def)
paulson@14405
   200
apply (rule bexI, rule_tac [2] lemma_hyprel_refl, safe)
paulson@14405
   201
apply (drule_tac x = u in spec, auto)
paulson@14405
   202
apply (drule_tac x = s in spec, auto, ultra)
paulson@14405
   203
apply (drule sym, auto)
paulson@14405
   204
done
paulson@14405
   205
paulson@14405
   206
lemma lemma_CRLIM:
paulson@14405
   207
     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
paulson@14405
   208
         cmod (xa - x) < s  & r \<le> abs (f xa - L))
paulson@14405
   209
      ==> \<forall>(n::nat). \<exists>xa.  xa \<noteq> x &
paulson@14405
   210
              cmod(xa - x) < inverse(real(Suc n)) & r \<le> abs (f xa - L)"
paulson@14405
   211
apply clarify
paulson@14405
   212
apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
paulson@14405
   213
done
paulson@14405
   214
paulson@14405
   215
lemma lemma_skolemize_CRLIM2:
paulson@14405
   216
     "\<forall>s. 0 < s --> (\<exists>xa.  xa \<noteq> x &
paulson@14405
   217
         cmod (xa - x) < s  & r \<le> abs (f xa - L))
paulson@14405
   218
      ==> \<exists>X. \<forall>(n::nat). X n \<noteq> x &
paulson@14405
   219
                cmod(X n - x) < inverse(real(Suc n)) & r \<le> abs (f (X n) - L)"
paulson@14405
   220
apply (drule lemma_CRLIM)
paulson@14405
   221
apply (drule choice, blast)
paulson@14405
   222
done
paulson@14405
   223
paulson@14405
   224
lemma lemma_crsimp:
paulson@14405
   225
     "\<forall>n. X n \<noteq> x &
paulson@14405
   226
          cmod (X n - x) < inverse (real(Suc n)) &
paulson@14405
   227
          r \<le> abs (f (X n) - L) ==>
paulson@14405
   228
      \<forall>n. cmod (X n - x) < inverse (real(Suc n))"
paulson@14405
   229
by auto
paulson@14405
   230
paulson@14405
   231
lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
paulson@14469
   232
apply (simp add: CRLIM_def NSCRLIM_def capprox_def)
paulson@14405
   233
apply (rule ccontr) 
paulson@14405
   234
apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff 
paulson@14405
   235
             hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff 
paulson@14405
   236
             hcmod Infinitesimal_approx_minus [symmetric] 
paulson@14405
   237
             Infinitesimal_FreeUltrafilterNat_iff)
paulson@14405
   238
apply (simp add: linorder_not_less)
paulson@14405
   239
apply (drule lemma_skolemize_CRLIM2, safe)
paulson@14405
   240
apply (drule_tac x = X in spec, auto)
paulson@14405
   241
apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
paulson@14405
   242
apply (simp add: CInfinitesimal_hcmod_iff hcomplex_of_complex_def 
paulson@14405
   243
             Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod)
paulson@14405
   244
apply (auto simp add: hypreal_of_real_def hypreal_diff)
paulson@14405
   245
apply (drule_tac x = r in spec, clarify)
paulson@14405
   246
apply (drule FreeUltrafilterNat_all, ultra)
paulson@14405
   247
done
paulson@14405
   248
paulson@14405
   249
text{*Second key result*}
paulson@14405
   250
theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)"
paulson@14405
   251
by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM)
paulson@14405
   252
paulson@14405
   253
(** get this result easily now **)
paulson@14405
   254
lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"
paulson@14405
   255
by (auto dest: NSCLIM_NSCRLIM_Re simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
paulson@14405
   256
paulson@14405
   257
lemma CLIM_CRLIM_Im: "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)"
paulson@14405
   258
by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])
paulson@14405
   259
paulson@14405
   260
lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"
paulson@14469
   261
by (simp add: CLIM_def complex_cnj_diff [symmetric])
paulson@14405
   262
paulson@14405
   263
lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"
paulson@14469
   264
by (simp add: CLIM_def complex_cnj_diff [symmetric])
paulson@14405
   265
paulson@14405
   266
(*** NSLIM_add hence CLIM_add *)
paulson@14405
   267
paulson@14405
   268
lemma NSCLIM_add:
paulson@14405
   269
     "[| f -- x --NSC> l; g -- x --NSC> m |]
paulson@14405
   270
      ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"
paulson@14405
   271
by (auto simp: NSCLIM_def intro!: capprox_add)
paulson@14405
   272
paulson@14405
   273
lemma CLIM_add:
paulson@14405
   274
     "[| f -- x --C> l; g -- x --C> m |]
paulson@14405
   275
      ==> (%x. f(x) + g(x)) -- x --C> (l + m)"
paulson@14405
   276
by (simp add: CLIM_NSCLIM_iff NSCLIM_add)
paulson@14405
   277
paulson@14405
   278
(*** NSLIM_mult hence CLIM_mult *)
paulson@14405
   279
paulson@14405
   280
lemma NSCLIM_mult:
paulson@14405
   281
     "[| f -- x --NSC> l; g -- x --NSC> m |]
paulson@14405
   282
      ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"
paulson@14405
   283
by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite)
paulson@14405
   284
paulson@14405
   285
lemma CLIM_mult:
paulson@14405
   286
     "[| f -- x --C> l; g -- x --C> m |]
paulson@14405
   287
      ==> (%x. f(x) * g(x)) -- x --C> (l * m)"
paulson@14405
   288
by (simp add: CLIM_NSCLIM_iff NSCLIM_mult)
paulson@14405
   289
paulson@14405
   290
(*** NSCLIM_const and CLIM_const ***)
paulson@14405
   291
paulson@14405
   292
lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k"
paulson@14405
   293
by (simp add: NSCLIM_def)
paulson@14405
   294
paulson@14405
   295
lemma CLIM_const [simp]: "(%x. k) -- x --C> k"
paulson@14405
   296
by (simp add: CLIM_def)
paulson@14405
   297
paulson@14405
   298
(*** NSCLIM_minus and CLIM_minus ***)
paulson@14405
   299
paulson@14405
   300
lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"
paulson@14405
   301
by (simp add: NSCLIM_def)
paulson@14405
   302
paulson@14405
   303
lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"
paulson@14405
   304
by (simp add: CLIM_NSCLIM_iff NSCLIM_minus)
paulson@14405
   305
paulson@14405
   306
(*** NSCLIM_diff hence CLIM_diff ***)
paulson@14405
   307
paulson@14405
   308
lemma NSCLIM_diff:
paulson@14405
   309
     "[| f -- x --NSC> l; g -- x --NSC> m |]
paulson@14405
   310
      ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"
paulson@14469
   311
by (simp add: diff_minus NSCLIM_add NSCLIM_minus)
paulson@14405
   312
paulson@14405
   313
lemma CLIM_diff:
paulson@14405
   314
     "[| f -- x --C> l; g -- x --C> m |]
paulson@14405
   315
      ==> (%x. f(x) - g(x)) -- x --C> (l - m)"
paulson@14405
   316
by (simp add: CLIM_NSCLIM_iff NSCLIM_diff)
paulson@14405
   317
paulson@14405
   318
(*** NSCLIM_inverse and hence CLIM_inverse *)
paulson@14405
   319
paulson@14405
   320
lemma NSCLIM_inverse:
paulson@14405
   321
     "[| f -- a --NSC> L;  L \<noteq> 0 |]
paulson@14405
   322
      ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
paulson@14469
   323
apply (simp add: NSCLIM_def, clarify)
paulson@14405
   324
apply (drule spec)
paulson@14469
   325
apply (force simp add: hcomplex_of_complex_capprox_inverse)
paulson@14405
   326
done
paulson@14405
   327
paulson@14405
   328
lemma CLIM_inverse:
paulson@14405
   329
     "[| f -- a --C> L;  L \<noteq> 0 |]
paulson@14405
   330
      ==> (%x. inverse(f(x))) -- a --C> (inverse L)"
paulson@14405
   331
by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse)
paulson@14405
   332
paulson@14405
   333
(*** NSCLIM_zero, CLIM_zero, etc. ***)
paulson@14405
   334
paulson@14405
   335
lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"
paulson@14469
   336
apply (simp add: diff_minus)
paulson@14405
   337
apply (rule_tac a1 = l in right_minus [THEN subst])
paulson@14469
   338
apply (rule NSCLIM_add, auto) 
paulson@14405
   339
done
paulson@14405
   340
paulson@14405
   341
lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"
paulson@14405
   342
by (simp add: CLIM_NSCLIM_iff NSCLIM_zero)
paulson@14405
   343
paulson@14405
   344
lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"
paulson@14405
   345
by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto)
paulson@14405
   346
paulson@14405
   347
lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"
paulson@14405
   348
by (drule_tac g = "%x. l" and m = l in CLIM_add, auto)
paulson@14405
   349
paulson@14405
   350
(*** NSCLIM_not zero and hence CLIM_not_zero ***)
paulson@13957
   351
paulson@14405
   352
lemma NSCLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --NSC> 0)"
paulson@14405
   353
apply (auto simp del: hcomplex_of_complex_zero simp add: NSCLIM_def)
paulson@14405
   354
apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI)
paulson@14405
   355
apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym]
paulson@14405
   356
            simp del: hcomplex_of_complex_zero)
paulson@14405
   357
done
paulson@14405
   358
paulson@14405
   359
(* [| k \<noteq> 0; (%x. k) -- x --NSC> 0 |] ==> R *)
paulson@14405
   360
lemmas NSCLIM_not_zeroE = NSCLIM_not_zero [THEN notE, standard]
paulson@14405
   361
paulson@14405
   362
lemma CLIM_not_zero: "k \<noteq> 0 ==> ~ ((%x. k) -- x --C> 0)"
paulson@14405
   363
by (simp add: CLIM_NSCLIM_iff NSCLIM_not_zero)
paulson@14405
   364
paulson@14405
   365
(*** NSCLIM_const hence CLIM_const ***)
paulson@14405
   366
paulson@14405
   367
lemma NSCLIM_const_eq: "(%x. k) -- x --NSC> L ==> k = L"
paulson@14405
   368
apply (rule ccontr)
paulson@14405
   369
apply (drule NSCLIM_zero)
paulson@14405
   370
apply (rule NSCLIM_not_zeroE [of "k-L"], auto)
paulson@14405
   371
done
paulson@14405
   372
paulson@14405
   373
lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L"
paulson@14405
   374
by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq)
paulson@14405
   375
paulson@14405
   376
(*** NSCLIM and hence CLIM are unique ***)
paulson@14405
   377
paulson@14405
   378
lemma NSCLIM_unique: "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M"
paulson@14405
   379
apply (drule NSCLIM_minus)
paulson@14405
   380
apply (drule NSCLIM_add, assumption)
paulson@14405
   381
apply (auto dest!: NSCLIM_const_eq [symmetric])
paulson@14405
   382
done
paulson@14405
   383
paulson@14405
   384
lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M"
paulson@14405
   385
by (simp add: CLIM_NSCLIM_iff NSCLIM_unique)
paulson@14405
   386
paulson@14405
   387
(***  NSCLIM_mult_zero and CLIM_mult_zero ***)
paulson@14405
   388
paulson@14405
   389
lemma NSCLIM_mult_zero:
paulson@14405
   390
     "[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0"
paulson@14405
   391
by (drule NSCLIM_mult, auto)
paulson@14405
   392
paulson@14405
   393
lemma CLIM_mult_zero:
paulson@14405
   394
     "[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0"
paulson@14405
   395
by (drule CLIM_mult, auto)
paulson@14405
   396
paulson@14405
   397
(*** NSCLIM_self hence CLIM_self ***)
paulson@14405
   398
paulson@14405
   399
lemma NSCLIM_self: "(%x. x) -- a --NSC> a"
paulson@14405
   400
by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox)
paulson@14405
   401
paulson@14405
   402
lemma CLIM_self: "(%x. x) -- a --C> a"
paulson@14405
   403
by (simp add: CLIM_NSCLIM_iff NSCLIM_self)
paulson@14405
   404
paulson@14405
   405
(** another equivalence result **)
paulson@14405
   406
lemma NSCLIM_NSCRLIM_iff:
paulson@14405
   407
   "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
paulson@14405
   408
apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff)
paulson@14405
   409
apply (auto dest!: spec) 
paulson@14405
   410
apply (rule_tac [!] z = xa in eq_Abs_hcomplex)
paulson@14405
   411
apply (auto simp add: hcomplex_diff starfunC starfunCR hcomplex_of_complex_def hcmod mem_infmal_iff)
paulson@14405
   412
done
paulson@14405
   413
paulson@14405
   414
(** much, much easier standard proof **)
paulson@14405
   415
lemma CLIM_CRLIM_iff: "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)"
paulson@14405
   416
by (simp add: CLIM_def CRLIM_def)
paulson@14405
   417
paulson@14405
   418
(* so this is nicer nonstandard proof *)
paulson@14405
   419
lemma NSCLIM_NSCRLIM_iff2:
paulson@14405
   420
     "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
paulson@14469
   421
by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])
paulson@14405
   422
paulson@14405
   423
lemma NSCLIM_NSCRLIM_Re_Im_iff:
paulson@14405
   424
     "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) &
paulson@14405
   425
                            (%x. Im(f x)) -- a --NSCR> Im(L))"
paulson@14405
   426
apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im)
paulson@14405
   427
apply (auto simp add: NSCLIM_def NSCRLIM_def)
paulson@14405
   428
apply (auto dest!: spec) 
paulson@14405
   429
apply (rule_tac z = x in eq_Abs_hcomplex)
paulson@14469
   430
apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def)
paulson@14405
   431
done
paulson@14405
   432
paulson@14405
   433
lemma CLIM_CRLIM_Re_Im_iff:
paulson@14405
   434
     "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) &
paulson@14405
   435
                         (%x. Im(f x)) -- a --CR> Im(L))"
paulson@14405
   436
by (simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff NSCLIM_NSCRLIM_Re_Im_iff)
paulson@14405
   437
paulson@14405
   438
paulson@14405
   439
subsection{*Continuity*}
paulson@14405
   440
paulson@14405
   441
lemma isNSContcD:
paulson@14405
   442
      "[| isNSContc f a; y @c= hcomplex_of_complex a |]
paulson@14405
   443
       ==> ( *fc* f) y @c= hcomplex_of_complex (f a)"
paulson@14405
   444
by (simp add: isNSContc_def)
paulson@14405
   445
paulson@14405
   446
lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) "
paulson@14405
   447
by (simp add: isNSContc_def NSCLIM_def)
paulson@14405
   448
paulson@14405
   449
lemma NSCLIM_isNSContc:
paulson@14405
   450
      "f -- a --NSC> (f a) ==> isNSContc f a"
paulson@14405
   451
apply (simp add: isNSContc_def NSCLIM_def, auto)
paulson@14405
   452
apply (case_tac "y = hcomplex_of_complex a", auto)
paulson@14405
   453
done
paulson@14405
   454
paulson@14405
   455
text{*Nonstandard continuity can be defined using NS Limit in 
paulson@14405
   456
similar fashion to standard definition of continuity*}
paulson@14405
   457
paulson@14405
   458
lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))"
paulson@14405
   459
by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc)
paulson@14405
   460
paulson@14405
   461
lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))"
paulson@14405
   462
by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff)
paulson@14405
   463
paulson@14405
   464
(*** key result for continuity ***)
paulson@14405
   465
lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)"
paulson@14405
   466
by (simp add: isContc_def isNSContc_CLIM_iff)
paulson@14405
   467
paulson@14405
   468
lemma isContc_isNSContc: "isContc f a ==> isNSContc f a"
paulson@14405
   469
by (erule isNSContc_isContc_iff [THEN iffD2])
paulson@14405
   470
paulson@14405
   471
lemma isNSContc_isContc: "isNSContc f a ==> isContc f a"
paulson@14405
   472
by (erule isNSContc_isContc_iff [THEN iffD1])
paulson@14405
   473
paulson@14405
   474
paulson@14405
   475
text{*Alternative definition of continuity*}
paulson@14405
   476
lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"
paulson@14405
   477
apply (simp add: NSCLIM_def, auto)
paulson@14405
   478
apply (drule_tac x = "hcomplex_of_complex a + x" in spec)
paulson@14405
   479
apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp)
paulson@14405
   480
apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]])
paulson@14405
   481
apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1])
paulson@14405
   482
 prefer 3 apply (simp add: compare_rls hcomplex_add_commute)
paulson@14405
   483
apply (rule_tac [2] z = x in eq_Abs_hcomplex)
paulson@14405
   484
apply (rule_tac [4] z = x in eq_Abs_hcomplex)
paulson@14405
   485
apply (auto simp add: starfunC hcomplex_of_complex_def hcomplex_minus hcomplex_add)
paulson@14405
   486
done
paulson@14405
   487
paulson@14405
   488
lemma NSCLIM_isContc_iff:
paulson@14405
   489
     "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"
paulson@14405
   490
by (rule NSCLIM_h_iff)
paulson@14405
   491
paulson@14405
   492
lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"
paulson@14405
   493
by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff)
paulson@14405
   494
paulson@14405
   495
lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"
paulson@14405
   496
by (simp add: isContc_def CLIM_isContc_iff)
paulson@14405
   497
paulson@14405
   498
lemma isContc_add:
paulson@14405
   499
     "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"
paulson@14405
   500
by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
paulson@14405
   501
paulson@14405
   502
lemma isContc_mult:
paulson@14405
   503
     "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"
paulson@14405
   504
by (auto intro!: starfunC_mult_CFinite_capprox 
paulson@14405
   505
            simp del: starfunC_mult [symmetric]
paulson@14405
   506
            simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)
paulson@14405
   507
paulson@14405
   508
paulson@14405
   509
lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
paulson@14469
   510
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_o [symmetric])
paulson@14405
   511
paulson@14405
   512
lemma isContc_o2:
paulson@14405
   513
     "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
paulson@14405
   514
by (auto dest: isContc_o simp add: o_def)
paulson@14405
   515
paulson@14405
   516
lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a"
paulson@14405
   517
by (simp add: isNSContc_def)
paulson@14405
   518
paulson@14405
   519
lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a"
paulson@14405
   520
by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus)
paulson@14405
   521
paulson@14405
   522
lemma isContc_inverse:
paulson@14405
   523
      "[| isContc f x; f x \<noteq> 0 |] ==> isContc (%x. inverse (f x)) x"
paulson@14405
   524
by (simp add: isContc_def CLIM_inverse)
paulson@14405
   525
paulson@14405
   526
lemma isNSContc_inverse:
paulson@14405
   527
     "[| isNSContc f x; f x \<noteq> 0 |] ==> isNSContc (%x. inverse (f x)) x"
paulson@14405
   528
by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff)
paulson@14405
   529
paulson@14405
   530
lemma isContc_diff:
paulson@14405
   531
      "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
paulson@14469
   532
apply (simp add: diff_minus)
paulson@14405
   533
apply (auto intro: isContc_add isContc_minus)
paulson@14405
   534
done
paulson@14405
   535
paulson@14405
   536
lemma isContc_const [simp]: "isContc (%x. k) a"
paulson@14405
   537
by (simp add: isContc_def)
paulson@14405
   538
paulson@14405
   539
lemma isNSContc_const [simp]: "isNSContc (%x. k) a"
paulson@14405
   540
by (simp add: isNSContc_def)
paulson@14405
   541
paulson@14405
   542
paulson@14405
   543
subsection{*Functions from Complex to Reals*}
paulson@14405
   544
paulson@14405
   545
lemma isNSContCRD:
paulson@14405
   546
      "[| isNSContCR f a; y @c= hcomplex_of_complex a |]
paulson@14405
   547
       ==> ( *fcR* f) y @= hypreal_of_real (f a)"
paulson@14405
   548
by (simp add: isNSContCR_def)
paulson@14405
   549
paulson@14405
   550
lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) "
paulson@14405
   551
by (simp add: isNSContCR_def NSCRLIM_def)
paulson@14405
   552
paulson@14405
   553
lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a"
paulson@14405
   554
apply (auto simp add: isNSContCR_def NSCRLIM_def)
paulson@14405
   555
apply (case_tac "y = hcomplex_of_complex a", auto)
paulson@14405
   556
done
paulson@14405
   557
paulson@14405
   558
lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))"
paulson@14405
   559
by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR)
paulson@14405
   560
paulson@14405
   561
lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))"
paulson@14405
   562
by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff)
paulson@14405
   563
paulson@14405
   564
(*** another key result for continuity ***)
paulson@14405
   565
lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)"
paulson@14405
   566
by (simp add: isContCR_def isNSContCR_CRLIM_iff)
paulson@14405
   567
paulson@14405
   568
lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a"
paulson@14405
   569
by (erule isNSContCR_isContCR_iff [THEN iffD2])
paulson@14405
   570
paulson@14405
   571
lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a"
paulson@14405
   572
by (erule isNSContCR_isContCR_iff [THEN iffD1])
paulson@14405
   573
paulson@14405
   574
lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)"
paulson@14405
   575
by (auto intro: capprox_hcmod_approx 
paulson@14405
   576
         simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] 
paulson@14405
   577
                    isNSContCR_def) 
paulson@14405
   578
paulson@14405
   579
lemma isContCR_cmod [simp]: "isContCR cmod (a)"
paulson@14469
   580
by (simp add: isNSContCR_isContCR_iff [symmetric])
paulson@14405
   581
paulson@14405
   582
lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a"
paulson@14405
   583
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re)
paulson@14405
   584
paulson@14405
   585
lemma isContc_isContCR_Im: "isContc f a ==> isContCR (%x. Im (f x)) a"
paulson@14405
   586
by (simp add: isContc_def isContCR_def CLIM_CRLIM_Im)
paulson@14405
   587
paulson@14405
   588
paulson@14405
   589
subsection{*Derivatives*}
paulson@14405
   590
paulson@14405
   591
lemma CDERIV_iff: "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
paulson@14405
   592
by (simp add: cderiv_def)
paulson@14405
   593
paulson@14405
   594
lemma CDERIV_NSC_iff:
paulson@14405
   595
      "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
paulson@14405
   596
by (simp add: cderiv_def CLIM_NSCLIM_iff)
paulson@14405
   597
paulson@14405
   598
lemma CDERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D"
paulson@14405
   599
by (simp add: cderiv_def)
paulson@14405
   600
paulson@14405
   601
lemma NSC_DERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D"
paulson@14405
   602
by (simp add: cderiv_def CLIM_NSCLIM_iff)
paulson@14405
   603
paulson@14405
   604
text{*Uniqueness*}
paulson@14405
   605
lemma CDERIV_unique: "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E"
paulson@14405
   606
by (simp add: cderiv_def CLIM_unique)
paulson@14405
   607
paulson@14405
   608
(*** uniqueness: a nonstandard proof ***)
paulson@14405
   609
lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E"
paulson@14405
   610
apply (simp add: nscderiv_def)
paulson@14405
   611
apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"]
paulson@14405
   612
            intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3)
paulson@14405
   613
done
paulson@13957
   614
paulson@13957
   615
paulson@14405
   616
subsection{* Differentiability*}
paulson@14405
   617
paulson@14405
   618
lemma CDERIV_CLIM_iff:
paulson@14405
   619
     "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) =
paulson@14405
   620
      ((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)"
paulson@14405
   621
apply (simp add: CLIM_def)
paulson@14405
   622
apply (rule_tac f=All in arg_cong) 
paulson@14405
   623
apply (rule ext) 
paulson@14405
   624
apply (rule imp_cong) 
paulson@14405
   625
apply (rule refl) 
paulson@14405
   626
apply (rule_tac f=Ex in arg_cong) 
paulson@14405
   627
apply (rule ext) 
paulson@14405
   628
apply (rule conj_cong) 
paulson@14405
   629
apply (rule refl) 
paulson@14405
   630
apply (rule trans) 
paulson@14405
   631
apply (rule all_shift [where a=a], simp) 
paulson@14405
   632
done
paulson@14405
   633
paulson@14405
   634
lemma CDERIV_iff2:
paulson@14405
   635
     "(CDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)"
paulson@14405
   636
by (simp add: cderiv_def CDERIV_CLIM_iff)
paulson@14405
   637
paulson@14405
   638
paulson@14405
   639
subsection{* Equivalence of NS and Standard Differentiation*}
paulson@14405
   640
paulson@14405
   641
(*** first equivalence ***)
paulson@14405
   642
lemma NSCDERIV_NSCLIM_iff:
paulson@14405
   643
      "(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
paulson@14405
   644
apply (simp add: nscderiv_def NSCLIM_def, auto)
paulson@14405
   645
apply (drule_tac x = xa in bspec)
paulson@14405
   646
apply (rule_tac [3] ccontr)
paulson@14405
   647
apply (drule_tac [3] x = h in spec)
paulson@14405
   648
apply (auto simp add: mem_cinfmal_iff starfunC_lambda_cancel)
paulson@14405
   649
done
paulson@14405
   650
paulson@14405
   651
(*** 2nd equivalence ***)
paulson@14405
   652
lemma NSCDERIV_NSCLIM_iff2:
paulson@14405
   653
     "(NSCDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)"
paulson@14405
   654
by (simp add: NSCDERIV_NSCLIM_iff CDERIV_CLIM_iff CLIM_NSCLIM_iff [symmetric])
paulson@14405
   655
paulson@14405
   656
lemma NSCDERIV_iff2:
paulson@14405
   657
     "(NSCDERIV f x :> D) =
paulson@14405
   658
      (\<forall>xa. xa \<noteq> hcomplex_of_complex x & xa @c= hcomplex_of_complex x -->
paulson@14405
   659
        ( *fc* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"
paulson@14405
   660
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
paulson@14405
   661
paulson@14405
   662
lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)"
paulson@14405
   663
by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff)
paulson@14405
   664
paulson@14405
   665
lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x"
paulson@14405
   666
apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus)
paulson@14405
   667
apply (drule capprox_minus_iff [THEN iffD1])
paulson@14405
   668
apply (subgoal_tac "xa + - (hcomplex_of_complex x) \<noteq> 0")
paulson@14405
   669
 prefer 2 apply (simp add: compare_rls) 
paulson@14405
   670
apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
paulson@15013
   671
 prefer 2 apply (simp add: add_assoc [symmetric]) 
paulson@15013
   672
apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute)
paulson@14405
   673
apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
paulson@14405
   674
apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
paulson@14405
   675
            simp add: mult_assoc)
paulson@14405
   676
apply (drule_tac x3 = D in 
paulson@14405
   677
       CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult,
paulson@14405
   678
                                    THEN mem_cinfmal_iff [THEN iffD1]])
paulson@14405
   679
apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2])
paulson@14405
   680
done
paulson@14405
   681
paulson@14405
   682
lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x"
paulson@14405
   683
by (simp add: NSCDERIV_CDERIV_iff [symmetric] isNSContc_isContc_iff [symmetric] NSCDERIV_isNSContc)
paulson@14405
   684
paulson@14405
   685
text{* Differentiation rules for combinations of functions follow by clear, 
paulson@14405
   686
straightforard algebraic manipulations*}
paulson@14405
   687
paulson@14405
   688
(* use simple constant nslimit theorem *)
paulson@14405
   689
lemma NSCDERIV_const [simp]: "(NSCDERIV (%x. k) x :> 0)"
paulson@14405
   690
by (simp add: NSCDERIV_NSCLIM_iff)
paulson@14405
   691
paulson@14405
   692
lemma CDERIV_const [simp]: "(CDERIV (%x. k) x :> 0)"
paulson@14405
   693
by (simp add: NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   694
paulson@14405
   695
lemma NSCDERIV_add:
paulson@14405
   696
     "[| NSCDERIV f x :> Da;  NSCDERIV g x :> Db |]
paulson@14405
   697
      ==> NSCDERIV (%x. f x + g x) x :> Da + Db"
paulson@14405
   698
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify)
paulson@14405
   699
apply (auto dest!: spec simp add: add_divide_distrib diff_minus)
paulson@14405
   700
apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add)
paulson@14405
   701
apply (auto simp add: add_ac)
paulson@14405
   702
done
paulson@14405
   703
paulson@14405
   704
lemma CDERIV_add:
paulson@14405
   705
     "[| CDERIV f x :> Da; CDERIV g x :> Db |]
paulson@14405
   706
      ==> CDERIV (%x. f x + g x) x :> Da + Db"
paulson@14405
   707
by (simp add: NSCDERIV_add NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   708
paulson@14405
   709
paulson@14405
   710
subsection{*Lemmas for Multiplication*}
paulson@14405
   711
paulson@14405
   712
lemma lemma_nscderiv1: "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
paulson@14405
   713
by (simp add: right_diff_distrib)
paulson@14405
   714
paulson@14405
   715
lemma lemma_nscderiv2:
paulson@14405
   716
     "[| (x + y) / z = hcomplex_of_complex D + yb; z \<noteq> 0;
paulson@14405
   717
         z : CInfinitesimal; yb : CInfinitesimal |]
paulson@14405
   718
      ==> x + y @c= 0"
paulson@14405
   719
apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption)
paulson@14405
   720
apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl)
paulson@14405
   721
apply (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add 
paulson@14405
   722
            simp add: mem_cinfmal_iff [symmetric])
paulson@14405
   723
apply (erule CInfinitesimal_subset_CFinite [THEN subsetD])
paulson@14405
   724
done
paulson@14405
   725
paulson@14405
   726
lemma NSCDERIV_mult:
paulson@14405
   727
     "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
paulson@14405
   728
      ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
paulson@14405
   729
apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify) 
paulson@14405
   730
apply (auto dest!: spec
paulson@14405
   731
            simp add: starfunC_lambda_cancel lemma_nscderiv1)
paulson@14405
   732
apply (simp (no_asm) add: add_divide_distrib)
paulson@14405
   733
apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+
paulson@14405
   734
apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
paulson@14405
   735
apply (simp add: diff_minus)
paulson@14405
   736
apply (drule_tac D = Db in lemma_nscderiv2)
paulson@14405
   737
apply (drule_tac [4]
paulson@14405
   738
        capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]])
paulson@14405
   739
apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc)
paulson@14405
   740
apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst])
paulson@14405
   741
apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym] 
paulson@14405
   742
		    CInfinitesimal_add CInfinitesimal_mult
paulson@14405
   743
		    CInfinitesimal_hcomplex_of_complex_mult
paulson@14405
   744
		    CInfinitesimal_hcomplex_of_complex_mult2
paulson@15013
   745
            simp add: add_assoc [symmetric])
paulson@14405
   746
done
paulson@14405
   747
paulson@14405
   748
lemma CDERIV_mult:
paulson@14405
   749
     "[| CDERIV f x :> Da; CDERIV g x :> Db |]
paulson@14405
   750
      ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
paulson@14405
   751
by (simp add: NSCDERIV_mult NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   752
paulson@14405
   753
lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"
paulson@14405
   754
apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff 
paulson@14469
   755
                 minus_mult_right right_distrib [symmetric] diff_minus
paulson@14405
   756
            del: times_divide_eq_right minus_mult_right [symmetric])
paulson@14405
   757
apply (erule NSCLIM_const [THEN NSCLIM_mult])
paulson@14405
   758
done
paulson@14405
   759
paulson@14405
   760
lemma CDERIV_cmult: "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"
paulson@14405
   761
by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   762
paulson@14405
   763
lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"
paulson@14469
   764
apply (simp add: NSCDERIV_NSCLIM_iff diff_minus)
paulson@14405
   765
apply (rule_tac t = "f x" in minus_minus [THEN subst])
paulson@14405
   766
apply (simp (no_asm_simp) add: minus_add_distrib [symmetric]
paulson@14405
   767
            del: minus_add_distrib minus_minus)
paulson@14405
   768
apply (erule NSCLIM_minus)
paulson@14405
   769
done
paulson@14405
   770
paulson@14405
   771
lemma CDERIV_minus: "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D"
paulson@14405
   772
by (simp add: NSCDERIV_minus NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   773
paulson@14405
   774
lemma NSCDERIV_add_minus:
paulson@14405
   775
     "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
paulson@14405
   776
      ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db"
paulson@14405
   777
by (blast dest: NSCDERIV_add NSCDERIV_minus)
paulson@14405
   778
paulson@14405
   779
lemma CDERIV_add_minus:
paulson@14405
   780
     "[| CDERIV f x :> Da; CDERIV g x :> Db |]
paulson@14405
   781
      ==> CDERIV (%x. f x + -g x) x :> Da + -Db"
paulson@14405
   782
by (blast dest: CDERIV_add CDERIV_minus)
paulson@14405
   783
paulson@14405
   784
lemma NSCDERIV_diff:
paulson@14405
   785
     "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
paulson@14405
   786
      ==> NSCDERIV (%x. f x - g x) x :> Da - Db"
paulson@14469
   787
by (simp add: diff_minus NSCDERIV_add_minus)
paulson@14405
   788
paulson@14405
   789
lemma CDERIV_diff:
paulson@14405
   790
     "[| CDERIV f x :> Da; CDERIV g x :> Db |]
paulson@14405
   791
       ==> CDERIV (%x. f x - g x) x :> Da - Db"
paulson@14469
   792
by (simp add: diff_minus CDERIV_add_minus)
paulson@14405
   793
paulson@14405
   794
paulson@14405
   795
subsection{*Chain Rule*}
paulson@14405
   796
paulson@14405
   797
(* lemmas *)
paulson@14405
   798
lemma NSCDERIV_zero:
paulson@14405
   799
      "[| NSCDERIV g x :> D;
paulson@14405
   800
          ( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);
paulson@14405
   801
          xa : CInfinitesimal; xa \<noteq> 0
paulson@14405
   802
       |] ==> D = 0"
paulson@14405
   803
apply (simp add: nscderiv_def)
paulson@14405
   804
apply (drule bspec, auto)
paulson@14405
   805
done
paulson@14405
   806
paulson@14405
   807
lemma NSCDERIV_capprox:
paulson@14405
   808
  "[| NSCDERIV f x :> D;  h: CInfinitesimal;  h \<noteq> 0 |]
paulson@14405
   809
   ==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0"
paulson@14405
   810
apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric])
paulson@14405
   811
apply (rule CInfinitesimal_ratio)
paulson@14405
   812
apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto)
paulson@14405
   813
done
paulson@14405
   814
paulson@14405
   815
paulson@14405
   816
(*--------------------------------------------------*)
paulson@14405
   817
(* from one version of differentiability            *)
paulson@14405
   818
(*                                                  *)
paulson@14405
   819
(*   f(x) - f(a)                                    *)
paulson@14405
   820
(* --------------- @= Db                            *)
paulson@14405
   821
(*     x - a                                        *)
paulson@14405
   822
(* -------------------------------------------------*)
paulson@14405
   823
paulson@14405
   824
lemma NSCDERIVD1:
paulson@14405
   825
   "[| NSCDERIV f (g x) :> Da;
paulson@14405
   826
       ( *fc* g) (hcomplex_of_complex(x) + xa) \<noteq> hcomplex_of_complex (g x);
paulson@14405
   827
       ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|]
paulson@14405
   828
    ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa))
paulson@14405
   829
	 - hcomplex_of_complex (f (g x))) /
paulson@14405
   830
	(( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x))
paulson@14405
   831
	   @c= hcomplex_of_complex (Da)"
paulson@14469
   832
by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)
paulson@14405
   833
paulson@14405
   834
(*--------------------------------------------------*)
paulson@14405
   835
(* from other version of differentiability          *)
paulson@14405
   836
(*                                                  *)
paulson@14405
   837
(*  f(x + h) - f(x)                                 *)
paulson@14405
   838
(* ----------------- @= Db                          *)
paulson@14405
   839
(*         h                                        *)
paulson@14405
   840
(*--------------------------------------------------*)
paulson@14405
   841
paulson@14405
   842
lemma NSCDERIVD2:
paulson@14405
   843
  "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa \<noteq> 0 |]
paulson@14405
   844
   ==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa
paulson@14405
   845
       @c= hcomplex_of_complex (Db)"
paulson@14469
   846
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_lambda_cancel)
paulson@14405
   847
paulson@14405
   848
lemma lemma_complex_chain: "(z::hcomplex) \<noteq> 0 ==> x*y = (x*inverse(z))*(z*y)"
paulson@14405
   849
by auto
paulson@14405
   850
paulson@14405
   851
paulson@14405
   852
text{*Chain rule*}
paulson@14405
   853
theorem NSCDERIV_chain:
paulson@14405
   854
     "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |]
paulson@14405
   855
      ==> NSCDERIV (f o g) x :> Da * Db"
paulson@14405
   856
apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric])
paulson@14405
   857
apply safe
paulson@14405
   858
apply (frule_tac f = g in NSCDERIV_capprox)
paulson@14405
   859
apply (auto simp add: starfunC_lambda_cancel2 starfunC_o [symmetric])
paulson@14405
   860
apply (case_tac "( *fc* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ")
paulson@14405
   861
apply (drule_tac g = g in NSCDERIV_zero)
paulson@14405
   862
apply (auto simp add: hcomplex_divide_def)
paulson@14405
   863
apply (rule_tac z1 = "( *fc* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst])
paulson@14405
   864
apply (simp (no_asm_simp))
paulson@14405
   865
apply (rule capprox_mult_hcomplex_of_complex)
paulson@14405
   866
apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2] 
paulson@14430
   867
            simp add: diff_minus [symmetric] divide_inverse [symmetric])
paulson@14405
   868
apply (blast intro: NSCDERIVD2)
paulson@14405
   869
done
paulson@14405
   870
paulson@14405
   871
text{*standard version*}
paulson@14405
   872
lemma CDERIV_chain:
paulson@14405
   873
     "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
paulson@14405
   874
      ==> CDERIV (f o g) x :> Da * Db"
paulson@14405
   875
by (simp add: NSCDERIV_CDERIV_iff [symmetric] NSCDERIV_chain)
paulson@14405
   876
paulson@14405
   877
lemma CDERIV_chain2:
paulson@14405
   878
     "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
paulson@14405
   879
      ==> CDERIV (%x. f (g x)) x :> Da * Db"
paulson@14405
   880
by (auto dest: CDERIV_chain simp add: o_def)
paulson@14405
   881
paulson@14405
   882
paulson@14405
   883
subsection{* Differentiation of Natural Number Powers*}
paulson@14405
   884
paulson@14405
   885
lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1"
paulson@14405
   886
by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def)
paulson@14405
   887
paulson@14405
   888
lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1"
paulson@14405
   889
by (simp add: NSCDERIV_CDERIV_iff [symmetric])
paulson@14405
   890
paulson@14405
   891
lemmas isContc_Id = CDERIV_Id [THEN CDERIV_isContc, standard]
paulson@13957
   892
paulson@14405
   893
text{*derivative of linear multiplication*}
paulson@14405
   894
lemma CDERIV_cmult_Id [simp]: "CDERIV (op * c) x :> c"
paulson@14405
   895
by (cut_tac c = c and x = x in CDERIV_Id [THEN CDERIV_cmult], simp)
paulson@14405
   896
paulson@14405
   897
lemma NSCDERIV_cmult_Id [simp]: "NSCDERIV (op * c) x :> c"
paulson@14405
   898
by (simp add: NSCDERIV_CDERIV_iff)
paulson@14405
   899
paulson@14405
   900
lemma CDERIV_pow [simp]:
paulson@14405
   901
     "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
paulson@14405
   902
apply (induct_tac "n")
paulson@14405
   903
apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
paulson@15013
   904
apply (auto simp add: left_distrib real_of_nat_Suc)
paulson@14405
   905
apply (case_tac "n")
paulson@14405
   906
apply (auto simp add: mult_ac add_commute)
paulson@14405
   907
done
paulson@14405
   908
paulson@14405
   909
text{*Nonstandard version*}
paulson@14405
   910
lemma NSCDERIV_pow:
paulson@14405
   911
     "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
paulson@14405
   912
by (simp add: NSCDERIV_CDERIV_iff)
paulson@14405
   913
paulson@14405
   914
lemma lemma_CDERIV_subst:
paulson@14405
   915
     "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E"
paulson@14405
   916
by auto
paulson@14405
   917
paulson@14405
   918
(*used once, in NSCDERIV_inverse*)
paulson@14405
   919
lemma CInfinitesimal_add_not_zero:
paulson@14405
   920
     "[| h: CInfinitesimal; x \<noteq> 0 |] ==> hcomplex_of_complex x + h \<noteq> 0"
paulson@14405
   921
apply clarify
paulson@14405
   922
apply (drule equals_zero_I, auto)
paulson@14405
   923
done
paulson@14405
   924
paulson@14405
   925
text{*Can't relax the premise @{term "x \<noteq> 0"}: it isn't continuous at zero*}
paulson@14405
   926
lemma NSCDERIV_inverse:
paulson@14405
   927
     "x \<noteq> 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
paulson@14405
   928
apply (simp add: nscderiv_def Ball_def, clarify) 
paulson@14405
   929
apply (frule CInfinitesimal_add_not_zero [where x=x])
paulson@14469
   930
apply (auto simp add: starfunC_inverse_inverse diff_minus 
paulson@14405
   931
           simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
paulson@14405
   932
apply (simp add: hcomplex_add_commute numeral_2_eq_2 inverse_add
paulson@14405
   933
                 inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
paulson@14405
   934
                 add_ac mult_ac 
paulson@15013
   935
            del: inverse_minus_eq inverse_mult_distrib
paulson@15013
   936
                 minus_mult_right [symmetric] minus_mult_left [symmetric])
paulson@14405
   937
apply (simp only: mult_assoc [symmetric] right_distrib)
paulson@14405
   938
apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
paulson@14405
   939
apply (rule inverse_add_CInfinitesimal_capprox2)
paulson@14405
   940
apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal 
paulson@14405
   941
            intro: CFinite_mult 
paulson@14405
   942
            simp add: inverse_minus_eq [symmetric])
paulson@14405
   943
apply (rule CInfinitesimal_CFinite_mult2, auto)
paulson@14405
   944
done
paulson@14405
   945
paulson@14405
   946
lemma CDERIV_inverse:
paulson@14405
   947
     "x \<noteq> 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
paulson@14405
   948
by (simp add: NSCDERIV_inverse NSCDERIV_CDERIV_iff [symmetric] 
paulson@14405
   949
         del: complexpow_Suc)
paulson@14405
   950
paulson@14405
   951
paulson@14405
   952
subsection{*Derivative of Reciprocals (Function @{term inverse})*}
paulson@14405
   953
paulson@14405
   954
lemma CDERIV_inverse_fun:
paulson@14405
   955
     "[| CDERIV f x :> d; f(x) \<noteq> 0 |]
paulson@14405
   956
      ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
paulson@14405
   957
apply (rule mult_commute [THEN subst])
paulson@15013
   958
apply (simp add: minus_mult_left power_inverse
paulson@15013
   959
            del: complexpow_Suc minus_mult_left [symmetric])
paulson@14405
   960
apply (fold o_def)
paulson@14405
   961
apply (blast intro!: CDERIV_chain CDERIV_inverse)
paulson@14405
   962
done
paulson@14405
   963
paulson@14405
   964
lemma NSCDERIV_inverse_fun:
paulson@14405
   965
     "[| NSCDERIV f x :> d; f(x) \<noteq> 0 |]
paulson@14405
   966
      ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
paulson@14405
   967
by (simp add: NSCDERIV_CDERIV_iff CDERIV_inverse_fun del: complexpow_Suc)
paulson@14405
   968
paulson@14405
   969
paulson@14405
   970
subsection{* Derivative of Quotient*}
paulson@14405
   971
paulson@14405
   972
lemma CDERIV_quotient:
paulson@14405
   973
     "[| CDERIV f x :> d; CDERIV g x :> e; g(x) \<noteq> 0 |]
paulson@14405
   974
       ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
paulson@14469
   975
apply (simp add: diff_minus)
paulson@14405
   976
apply (drule_tac f = g in CDERIV_inverse_fun)
paulson@14405
   977
apply (drule_tac [2] CDERIV_mult, assumption+)
paulson@14430
   978
apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left 
paulson@14430
   979
                 mult_ac 
paulson@14430
   980
            del: minus_mult_right [symmetric] minus_mult_left [symmetric]
paulson@14430
   981
                 complexpow_Suc)
paulson@14405
   982
done
paulson@14405
   983
paulson@14405
   984
lemma NSCDERIV_quotient:
paulson@14405
   985
     "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) \<noteq> 0 |]
paulson@14405
   986
       ==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
paulson@14405
   987
by (simp add: NSCDERIV_CDERIV_iff CDERIV_quotient del: complexpow_Suc)
paulson@14405
   988
paulson@14405
   989
paulson@14405
   990
subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}
paulson@14405
   991
paulson@14405
   992
lemma CLIM_equal:
paulson@14405
   993
      "[| \<forall>x. x \<noteq> a --> (f x = g x) |] ==> (f -- a --C> l) = (g -- a --C> l)"
paulson@14405
   994
by (simp add: CLIM_def complex_add_minus_iff)
paulson@14405
   995
paulson@14405
   996
lemma CLIM_trans:
paulson@14405
   997
     "[| (%x. f(x) + -g(x)) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l"
paulson@14405
   998
apply (drule CLIM_add, assumption)
paulson@14405
   999
apply (simp add: complex_add_assoc)
paulson@14405
  1000
done
paulson@14405
  1001
paulson@14405
  1002
lemma CARAT_CDERIV:
paulson@14405
  1003
     "(CDERIV f x :> l) =
paulson@14405
  1004
      (\<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isContc g x & g x = l)"
paulson@14405
  1005
apply safe
paulson@14405
  1006
apply (rule_tac x = "%z. if z=x then l else (f (z) - f (x)) / (z-x)" in exI)
paulson@14405
  1007
apply (auto simp add: mult_assoc isContc_iff CDERIV_iff)
paulson@14405
  1008
apply (rule_tac [!] CLIM_equal [THEN iffD1], auto)
paulson@14405
  1009
done
paulson@14405
  1010
paulson@14405
  1011
paulson@14405
  1012
lemma CARAT_NSCDERIV:
paulson@14405
  1013
     "NSCDERIV f x :> l ==>
paulson@14405
  1014
      \<exists>g. (\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
paulson@14469
  1015
by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)
paulson@14405
  1016
paulson@14405
  1017
(* FIXME tidy! How about a NS proof? *)
paulson@14405
  1018
lemma CARAT_CDERIVD:
paulson@14405
  1019
     "(\<forall>z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
paulson@14405
  1020
      ==> NSCDERIV f x :> l"
paulson@14405
  1021
apply (simp only: NSCDERIV_iff2) 
paulson@14405
  1022
apply (tactic {*(auto_tac (claset(), 
paulson@14405
  1023
              simpset() delsimprocs field_cancel_factor
paulson@14405
  1024
                        addsimps [thm"NSCDERIV_iff2"])) *})
paulson@14405
  1025
apply (simp add: isNSContc_def)
paulson@14405
  1026
done
paulson@13957
  1027
paulson@14405
  1028
ML
paulson@14405
  1029
{*
paulson@14405
  1030
val complex_add_minus_iff = thm "complex_add_minus_iff";
paulson@14405
  1031
val complex_add_eq_0_iff = thm "complex_add_eq_0_iff";
paulson@14405
  1032
val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re";
paulson@14405
  1033
val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im";
paulson@14405
  1034
val CLIM_NSCLIM = thm "CLIM_NSCLIM";
paulson@14405
  1035
val eq_Abs_hcomplex_ALL = thm "eq_Abs_hcomplex_ALL";
paulson@14405
  1036
val lemma_CLIM = thm "lemma_CLIM";
paulson@14405
  1037
val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2";
paulson@14405
  1038
val lemma_csimp = thm "lemma_csimp";
paulson@14405
  1039
val NSCLIM_CLIM = thm "NSCLIM_CLIM";
paulson@14405
  1040
val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff";
paulson@14405
  1041
val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM";
paulson@14405
  1042
val lemma_CRLIM = thm "lemma_CRLIM";
paulson@14405
  1043
val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2";
paulson@14405
  1044
val lemma_crsimp = thm "lemma_crsimp";
paulson@14405
  1045
val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM";
paulson@14405
  1046
val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff";
paulson@14405
  1047
val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re";
paulson@14405
  1048
val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im";
paulson@14405
  1049
val CLIM_cnj = thm "CLIM_cnj";
paulson@14405
  1050
val CLIM_cnj_iff = thm "CLIM_cnj_iff";
paulson@14405
  1051
val NSCLIM_add = thm "NSCLIM_add";
paulson@14405
  1052
val CLIM_add = thm "CLIM_add";
paulson@14405
  1053
val NSCLIM_mult = thm "NSCLIM_mult";
paulson@14405
  1054
val CLIM_mult = thm "CLIM_mult";
paulson@14405
  1055
val NSCLIM_const = thm "NSCLIM_const";
paulson@14405
  1056
val CLIM_const = thm "CLIM_const";
paulson@14405
  1057
val NSCLIM_minus = thm "NSCLIM_minus";
paulson@14405
  1058
val CLIM_minus = thm "CLIM_minus";
paulson@14405
  1059
val NSCLIM_diff = thm "NSCLIM_diff";
paulson@14405
  1060
val CLIM_diff = thm "CLIM_diff";
paulson@14405
  1061
val NSCLIM_inverse = thm "NSCLIM_inverse";
paulson@14405
  1062
val CLIM_inverse = thm "CLIM_inverse";
paulson@14405
  1063
val NSCLIM_zero = thm "NSCLIM_zero";
paulson@14405
  1064
val CLIM_zero = thm "CLIM_zero";
paulson@14405
  1065
val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel";
paulson@14405
  1066
val CLIM_zero_cancel = thm "CLIM_zero_cancel";
paulson@14405
  1067
val NSCLIM_not_zero = thm "NSCLIM_not_zero";
paulson@14405
  1068
val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE";
paulson@14405
  1069
val CLIM_not_zero = thm "CLIM_not_zero";
paulson@14405
  1070
val NSCLIM_const_eq = thm "NSCLIM_const_eq";
paulson@14405
  1071
val CLIM_const_eq = thm "CLIM_const_eq";
paulson@14405
  1072
val NSCLIM_unique = thm "NSCLIM_unique";
paulson@14405
  1073
val CLIM_unique = thm "CLIM_unique";
paulson@14405
  1074
val NSCLIM_mult_zero = thm "NSCLIM_mult_zero";
paulson@14405
  1075
val CLIM_mult_zero = thm "CLIM_mult_zero";
paulson@14405
  1076
val NSCLIM_self = thm "NSCLIM_self";
paulson@14405
  1077
val CLIM_self = thm "CLIM_self";
paulson@14405
  1078
val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff";
paulson@14405
  1079
val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff";
paulson@14405
  1080
val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2";
paulson@14405
  1081
val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff";
paulson@14405
  1082
val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff";
paulson@14405
  1083
val isNSContcD = thm "isNSContcD";
paulson@14405
  1084
val isNSContc_NSCLIM = thm "isNSContc_NSCLIM";
paulson@14405
  1085
val NSCLIM_isNSContc = thm "NSCLIM_isNSContc";
paulson@14405
  1086
val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff";
paulson@14405
  1087
val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff";
paulson@14405
  1088
val isNSContc_isContc_iff = thm "isNSContc_isContc_iff";
paulson@14405
  1089
val isContc_isNSContc = thm "isContc_isNSContc";
paulson@14405
  1090
val isNSContc_isContc = thm "isNSContc_isContc";
paulson@14405
  1091
val NSCLIM_h_iff = thm "NSCLIM_h_iff";
paulson@14405
  1092
val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff";
paulson@14405
  1093
val CLIM_isContc_iff = thm "CLIM_isContc_iff";
paulson@14405
  1094
val isContc_iff = thm "isContc_iff";
paulson@14405
  1095
val isContc_add = thm "isContc_add";
paulson@14405
  1096
val isContc_mult = thm "isContc_mult";
paulson@14405
  1097
val isContc_o = thm "isContc_o";
paulson@14405
  1098
val isContc_o2 = thm "isContc_o2";
paulson@14405
  1099
val isNSContc_minus = thm "isNSContc_minus";
paulson@14405
  1100
val isContc_minus = thm "isContc_minus";
paulson@14405
  1101
val isContc_inverse = thm "isContc_inverse";
paulson@14405
  1102
val isNSContc_inverse = thm "isNSContc_inverse";
paulson@14405
  1103
val isContc_diff = thm "isContc_diff";
paulson@14405
  1104
val isContc_const = thm "isContc_const";
paulson@14405
  1105
val isNSContc_const = thm "isNSContc_const";
paulson@14405
  1106
val isNSContCRD = thm "isNSContCRD";
paulson@14405
  1107
val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM";
paulson@14405
  1108
val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR";
paulson@14405
  1109
val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff";
paulson@14405
  1110
val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff";
paulson@14405
  1111
val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff";
paulson@14405
  1112
val isContCR_isNSContCR = thm "isContCR_isNSContCR";
paulson@14405
  1113
val isNSContCR_isContCR = thm "isNSContCR_isContCR";
paulson@14405
  1114
val isNSContCR_cmod = thm "isNSContCR_cmod";
paulson@14405
  1115
val isContCR_cmod = thm "isContCR_cmod";
paulson@14405
  1116
val isContc_isContCR_Re = thm "isContc_isContCR_Re";
paulson@14405
  1117
val isContc_isContCR_Im = thm "isContc_isContCR_Im";
paulson@14405
  1118
val CDERIV_iff = thm "CDERIV_iff";
paulson@14405
  1119
val CDERIV_NSC_iff = thm "CDERIV_NSC_iff";
paulson@14405
  1120
val CDERIVD = thm "CDERIVD";
paulson@14405
  1121
val NSC_DERIVD = thm "NSC_DERIVD";
paulson@14405
  1122
val CDERIV_unique = thm "CDERIV_unique";
paulson@14405
  1123
val NSCDeriv_unique = thm "NSCDeriv_unique";
paulson@14405
  1124
val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff";
paulson@14405
  1125
val CDERIV_iff2 = thm "CDERIV_iff2";
paulson@14405
  1126
val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff";
paulson@14405
  1127
val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2";
paulson@14405
  1128
val NSCDERIV_iff2 = thm "NSCDERIV_iff2";
paulson@14405
  1129
val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff";
paulson@14405
  1130
val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc";
paulson@14405
  1131
val CDERIV_isContc = thm "CDERIV_isContc";
paulson@14405
  1132
val NSCDERIV_const = thm "NSCDERIV_const";
paulson@14405
  1133
val CDERIV_const = thm "CDERIV_const";
paulson@14405
  1134
val NSCDERIV_add = thm "NSCDERIV_add";
paulson@14405
  1135
val CDERIV_add = thm "CDERIV_add";
paulson@14405
  1136
val lemma_nscderiv1 = thm "lemma_nscderiv1";
paulson@14405
  1137
val lemma_nscderiv2 = thm "lemma_nscderiv2";
paulson@14405
  1138
val NSCDERIV_mult = thm "NSCDERIV_mult";
paulson@14405
  1139
val CDERIV_mult = thm "CDERIV_mult";
paulson@14405
  1140
val NSCDERIV_cmult = thm "NSCDERIV_cmult";
paulson@14405
  1141
val CDERIV_cmult = thm "CDERIV_cmult";
paulson@14405
  1142
val NSCDERIV_minus = thm "NSCDERIV_minus";
paulson@14405
  1143
val CDERIV_minus = thm "CDERIV_minus";
paulson@14405
  1144
val NSCDERIV_add_minus = thm "NSCDERIV_add_minus";
paulson@14405
  1145
val CDERIV_add_minus = thm "CDERIV_add_minus";
paulson@14405
  1146
val NSCDERIV_diff = thm "NSCDERIV_diff";
paulson@14405
  1147
val CDERIV_diff = thm "CDERIV_diff";
paulson@14405
  1148
val NSCDERIV_zero = thm "NSCDERIV_zero";
paulson@14405
  1149
val NSCDERIV_capprox = thm "NSCDERIV_capprox";
paulson@14405
  1150
val NSCDERIVD1 = thm "NSCDERIVD1";
paulson@14405
  1151
val NSCDERIVD2 = thm "NSCDERIVD2";
paulson@14405
  1152
val lemma_complex_chain = thm "lemma_complex_chain";
paulson@14405
  1153
val NSCDERIV_chain = thm "NSCDERIV_chain";
paulson@14405
  1154
val CDERIV_chain = thm "CDERIV_chain";
paulson@14405
  1155
val CDERIV_chain2 = thm "CDERIV_chain2";
paulson@14405
  1156
val NSCDERIV_Id = thm "NSCDERIV_Id";
paulson@14405
  1157
val CDERIV_Id = thm "CDERIV_Id";
paulson@14405
  1158
val isContc_Id = thms "isContc_Id";
paulson@14405
  1159
val CDERIV_cmult_Id = thm "CDERIV_cmult_Id";
paulson@14405
  1160
val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id";
paulson@14405
  1161
val CDERIV_pow = thm "CDERIV_pow";
paulson@14405
  1162
val NSCDERIV_pow = thm "NSCDERIV_pow";
paulson@14405
  1163
val lemma_CDERIV_subst = thm "lemma_CDERIV_subst";
paulson@14405
  1164
val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero";
paulson@14405
  1165
val NSCDERIV_inverse = thm "NSCDERIV_inverse";
paulson@14405
  1166
val CDERIV_inverse = thm "CDERIV_inverse";
paulson@14405
  1167
val CDERIV_inverse_fun = thm "CDERIV_inverse_fun";
paulson@14405
  1168
val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun";
paulson@14405
  1169
val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared";
paulson@14405
  1170
val CDERIV_quotient = thm "CDERIV_quotient";
paulson@14405
  1171
val NSCDERIV_quotient = thm "NSCDERIV_quotient";
paulson@14405
  1172
val CLIM_equal = thm "CLIM_equal";
paulson@14405
  1173
val CLIM_trans = thm "CLIM_trans";
paulson@14405
  1174
val CARAT_CDERIV = thm "CARAT_CDERIV";
paulson@14405
  1175
val CARAT_NSCDERIV = thm "CARAT_NSCDERIV";
paulson@14405
  1176
val CARAT_CDERIVD = thm "CARAT_CDERIVD";
paulson@14405
  1177
*}
paulson@14405
  1178
paulson@14405
  1179
end