# Theory CLim

Up to index of Isabelle/HOL/HOL-Complex

theory CLim
imports CSeries
begin

    (*  Title       : CLim.thy
        Author      : Jacques D. Fleuriot
        Copyright   : 2001 University of Edinburgh
        Conversion to Isar and new proofs by Lawrence C Paulson, 2004
    *)

    header{*Limits, Continuity and Differentiation for Complex Functions*}

    theory CLim
    imports CSeries
    begin

    (*not in simpset?*)
    declare hypreal_epsilon_not_zero [simp]

    (*??generalize*)
    lemma lemma_complex_mult_inverse_squared [simp]:
         "x ≠ (0::complex) ==> (x * inverse(x) ^ 2) = inverse x"
    by (simp add: numeral_2_eq_2)

    text{*Changing the quantified variable. Install earlier?*}
    lemma all_shift: "(∀x::'a::comm_ring_1. P x) = (∀x. P (x-a))";
    apply auto
    apply (drule_tac x="x+a" in spec)
    apply (simp add: diff_minus add_assoc)
    done

    lemma complex_add_minus_iff [simp]: "(x + - a = (0::complex)) = (x=a)"
    by (simp add: diff_eq_eq diff_minus [symmetric])

    lemma complex_add_eq_0_iff [iff]: "(x+y = (0::complex)) = (y = -x)"
    apply auto
    apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
    done

    constdefs

      CLIM :: "[complex=>complex,complex,complex] => bool"
                                    ("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
      "f -- a --C> L ==
         ∀r. 0 < r -->
                 (∃s. 0 < s & (∀x. (x ≠ a & (cmod(x - a) < s)
                              --> cmod(f x - L) < r)))"

      NSCLIM :: "[complex=>complex,complex,complex] => bool"
                                  ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
      "f -- a --NSC> L == (∀x. (x ≠ hcomplex_of_complex a &
                                     x @c= hcomplex_of_complex a
                                       --> ( *f* f) x @c= hcomplex_of_complex L))"

      (* f: C --> R *)
      CRLIM :: "[complex=>real,complex,real] => bool"
                                    ("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
      "f -- a --CR> L ==
         ∀r. 0 < r -->
                 (∃s. 0 < s & (∀x. (x ≠ a & (cmod(x - a) < s)
                              --> abs(f x - L) < r)))"

      NSCRLIM :: "[complex=>real,complex,real] => bool"
                                  ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
      "f -- a --NSCR> L == (∀x. (x ≠ hcomplex_of_complex a &
                                     x @c= hcomplex_of_complex a
                                       --> ( *f* f) x @= hypreal_of_real L))"

      isContc :: "[complex=>complex,complex] => bool"
      "isContc f a == (f -- a --C> (f a))"

      (* NS definition dispenses with limit notions *)
      isNSContc :: "[complex=>complex,complex] => bool"
      "isNSContc f a == (∀y. y @c= hcomplex_of_complex a -->
                               ( *f* f) y @c= hcomplex_of_complex (f a))"

      isContCR :: "[complex=>real,complex] => bool"
      "isContCR f a == (f -- a --CR> (f a))"

      (* NS definition dispenses with limit notions *)
      isNSContCR :: "[complex=>real,complex] => bool"
      "isNSContCR f a == (∀y. y @c= hcomplex_of_complex a -->
                               ( *f* f) y @= hypreal_of_real (f a))"

      (* differentiation: D is derivative of function f at x *)
      cderiv:: "[complex=>complex,complex,complex] => bool"
                                ("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
      "CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"

      nscderiv :: "[complex=>complex,complex,complex] => bool"
                                ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
      "NSCDERIV f x :> D == (∀h ∈ CInfinitesimal - {0}.
                                  (( *f* f)(hcomplex_of_complex x + h)
                                     - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)"

      cdifferentiable :: "[complex=>complex,complex] => bool"
                         (infixl "cdifferentiable" 60)
      "f cdifferentiable x == (∃D. CDERIV f x :> D)"

      NSCdifferentiable :: "[complex=>complex,complex] => bool"
                            (infixl "NSCdifferentiable" 60)
      "f NSCdifferentiable x == (∃D. NSCDERIV f x :> D)"

      isUContc :: "(complex=>complex) => bool"
      "isUContc f ==  (∀r. 0 < r -->
                          (∃s. 0 < s & (∀x y. cmod(x - y) < s
                                --> cmod(f x - f y) < r)))"

      isNSUContc :: "(complex=>complex) => bool"
      "isNSUContc f == (∀x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"

    subsection{*Limit of Complex to Complex Function*}

    lemma NSCLIM_NSCRLIM_Re: "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"
    by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff
                  hRe_hcomplex_of_complex)

    lemma NSCLIM_NSCRLIM_Im: "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"
    by (simp add: NSCLIM_def NSCRLIM_def starfunC_approx_Re_Im_iff
                  hIm_hcomplex_of_complex)

    lemma CLIM_NSCLIM:
          "f -- x --C> L ==> f -- x --NSC> L"
    apply (simp add: CLIM_def NSCLIM_def capprox_def, auto)
    apply (rule_tac x = xa in star_cases)
    apply (auto simp add: starfun star_n_diff star_of_def star_n_eq_iff
             CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff)
    apply (rule bexI [OF _ Rep_star_star_n], safe)
    apply (drule_tac x = u in spec, auto)
    apply (drule_tac x = s in spec, auto, ultra)
    apply (drule sym, auto)
    done

    lemma eq_Abs_star_ALL: "(∀t. P t) = (∀X. P (star_n X))"
    apply auto
    apply (rule_tac x = t in star_cases, auto)
    done

    lemma lemma_CLIM:
         "∀s. 0 < s --> (∃xa.  xa ≠ x &
             cmod (xa - x) < s  & r ≤ cmod (f xa - L))
          ==> ∀(n::nat). ∃xa.  xa ≠ x &
                  cmod(xa - x) < inverse(real(Suc n)) & r ≤ cmod(f xa - L)"
    apply clarify
    apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
    done

    lemma lemma_skolemize_CLIM2:
         "∀s. 0 < s --> (∃xa.  xa ≠ x &
             cmod (xa - x) < s  & r ≤ cmod (f xa - L))
          ==> ∃X. ∀(n::nat). X n ≠ x &
                    cmod(X n - x) < inverse(real(Suc n)) & r ≤ cmod(f (X n) - L)"
    apply (drule lemma_CLIM)
    apply (drule choice, blast)
    done

    lemma lemma_csimp:
         "∀n. X n ≠ x &
              cmod (X n - x) < inverse (real(Suc n)) &
              r ≤ cmod (f (X n) - L) ==>
              ∀n. cmod (X n - x) < inverse (real(Suc n))"
    by auto

    lemma NSCLIM_CLIM:
         "f -- x --NSC> L ==> f -- x --C> L"
    apply (simp add: CLIM_def NSCLIM_def)
    apply (rule ccontr)
    apply (auto simp add: eq_Abs_star_ALL starfun
                CInfinitesimal_capprox_minus [symmetric] star_n_diff
                CInfinitesimal_hcmod_iff star_of_def star_n_eq_iff
                Infinitesimal_FreeUltrafilterNat_iff hcmod)
    apply (simp add: linorder_not_less)
    apply (drule lemma_skolemize_CLIM2, safe)
    apply (drule_tac x = X in spec, auto)
    apply (drule lemma_csimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
    apply (simp add: CInfinitesimal_hcmod_iff star_of_def
                Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod,  blast)
    apply (drule_tac x = r in spec, clarify)
    apply (drule FreeUltrafilterNat_all, ultra, arith)
    done

    text{*First key result*}
    theorem CLIM_NSCLIM_iff: "(f -- x --C> L) = (f -- x --NSC> L)"
    by (blast intro: CLIM_NSCLIM NSCLIM_CLIM)

    subsection{*Limit of Complex to Real Function*}

    lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L"
    apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto)
    apply (rule_tac x = xa in star_cases)
    apply (auto simp add: starfun star_n_diff
                  CInfinitesimal_hcmod_iff hcmod
                  Infinitesimal_FreeUltrafilterNat_iff
                  star_of_def star_n_eq_iff
                  Infinitesimal_approx_minus [symmetric])
    apply (rule bexI [OF _ Rep_star_star_n], safe)
    apply (drule_tac x = u in spec, auto)
    apply (drule_tac x = s in spec, auto, ultra)
    apply (drule sym, auto)
    done

    lemma lemma_CRLIM:
         "∀s. 0 < s --> (∃xa.  xa ≠ x &
             cmod (xa - x) < s  & r ≤ abs (f xa - L))
          ==> ∀(n::nat). ∃xa.  xa ≠ x &
                  cmod(xa - x) < inverse(real(Suc n)) & r ≤ abs (f xa - L)"
    apply clarify
    apply (cut_tac n1 = n in real_of_nat_Suc_gt_zero [THEN positive_imp_inverse_positive], auto)
    done

    lemma lemma_skolemize_CRLIM2:
         "∀s. 0 < s --> (∃xa.  xa ≠ x &
             cmod (xa - x) < s  & r ≤ abs (f xa - L))
          ==> ∃X. ∀(n::nat). X n ≠ x &
                    cmod(X n - x) < inverse(real(Suc n)) & r ≤ abs (f (X n) - L)"
    apply (drule lemma_CRLIM)
    apply (drule choice, blast)
    done

    lemma lemma_crsimp:
         "∀n. X n ≠ x &
              cmod (X n - x) < inverse (real(Suc n)) &
              r ≤ abs (f (X n) - L) ==>
          ∀n. cmod (X n - x) < inverse (real(Suc n))"
    by auto

    lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L"
    apply (simp add: CRLIM_def NSCRLIM_def capprox_def)
    apply (rule ccontr)
    apply (auto simp add: eq_Abs_star_ALL starfun star_n_diff
                 CInfinitesimal_hcmod_iff
                 hcmod Infinitesimal_approx_minus [symmetric]
                 star_of_def star_n_eq_iff
                 Infinitesimal_FreeUltrafilterNat_iff)
    apply (simp add: linorder_not_less)
    apply (drule lemma_skolemize_CRLIM2, safe)
    apply (drule_tac x = X in spec, auto)
    apply (drule lemma_crsimp [THEN complex_seq_to_hcomplex_CInfinitesimal])
    apply (simp add: CInfinitesimal_hcmod_iff star_of_def
                 Infinitesimal_FreeUltrafilterNat_iff star_n_diff hcmod)
    apply (auto simp add: star_of_def star_n_diff)
    apply (drule_tac x = r in spec, clarify)
    apply (drule FreeUltrafilterNat_all, ultra)
    done

    text{*Second key result*}
    theorem CRLIM_NSCRLIM_iff: "(f -- x --CR> L) = (f -- x --NSCR> L)"
    by (blast intro: CRLIM_NSCRLIM NSCRLIM_CRLIM)

    (** get this result easily now **)
    lemma CLIM_CRLIM_Re: "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"
    by (auto dest: NSCLIM_NSCRLIM_Re simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])

    lemma CLIM_CRLIM_Im: "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)"
    by (auto dest: NSCLIM_NSCRLIM_Im simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff [symmetric])

    lemma CLIM_cnj: "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"
    by (simp add: CLIM_def complex_cnj_diff [symmetric])

    lemma CLIM_cnj_iff: "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"
    by (simp add: CLIM_def complex_cnj_diff [symmetric])

    (*** NSLIM_add hence CLIM_add *)

    lemma NSCLIM_add:
         "[| f -- x --NSC> l; g -- x --NSC> m |]
          ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"
    by (auto simp: NSCLIM_def intro!: capprox_add)

    lemma CLIM_add:
         "[| f -- x --C> l; g -- x --C> m |]
          ==> (%x. f(x) + g(x)) -- x --C> (l + m)"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_add)

    (*** NSLIM_mult hence CLIM_mult *)

    lemma NSCLIM_mult:
         "[| f -- x --NSC> l; g -- x --NSC> m |]
          ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"
    by (auto simp add: NSCLIM_def intro!: capprox_mult_CFinite)

    lemma CLIM_mult:
         "[| f -- x --C> l; g -- x --C> m |]
          ==> (%x. f(x) * g(x)) -- x --C> (l * m)"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_mult)

    (*** NSCLIM_const and CLIM_const ***)

    lemma NSCLIM_const [simp]: "(%x. k) -- x --NSC> k"
    by (simp add: NSCLIM_def)

    lemma CLIM_const [simp]: "(%x. k) -- x --C> k"
    by (simp add: CLIM_def)

    (*** NSCLIM_minus and CLIM_minus ***)

    lemma NSCLIM_minus: "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"
    by (simp add: NSCLIM_def)

    lemma CLIM_minus: "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_minus)

    (*** NSCLIM_diff hence CLIM_diff ***)

    lemma NSCLIM_diff:
         "[| f -- x --NSC> l; g -- x --NSC> m |]
          ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"
    by (simp add: diff_minus NSCLIM_add NSCLIM_minus)

    lemma CLIM_diff:
         "[| f -- x --C> l; g -- x --C> m |]
          ==> (%x. f(x) - g(x)) -- x --C> (l - m)"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_diff)

    (*** NSCLIM_inverse and hence CLIM_inverse *)

    lemma NSCLIM_inverse:
         "[| f -- a --NSC> L;  L ≠ 0 |]
          ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"
    apply (simp add: NSCLIM_def, clarify)
    apply (drule spec)
    apply (force simp add: hcomplex_of_complex_capprox_inverse)
    done

    lemma CLIM_inverse:
         "[| f -- a --C> L;  L ≠ 0 |]
          ==> (%x. inverse(f(x))) -- a --C> (inverse L)"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_inverse)

    (*** NSCLIM_zero, CLIM_zero, etc. ***)

    lemma NSCLIM_zero: "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"
    apply (simp add: diff_minus)
    apply (rule_tac a1 = l in right_minus [THEN subst])
    apply (rule NSCLIM_add, auto)
    done

    lemma CLIM_zero: "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_zero)

    lemma NSCLIM_zero_cancel: "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"
    by (drule_tac g = "%x. l" and m = l in NSCLIM_add, auto)

    lemma CLIM_zero_cancel: "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"
    by (drule_tac g = "%x. l" and m = l in CLIM_add, auto)

    (*** NSCLIM_not zero and hence CLIM_not_zero ***)

    lemma NSCLIM_not_zero: "k ≠ 0 ==> ~ ((%x. k) -- x --NSC> 0)"
    apply (auto simp del: star_of_zero simp add: NSCLIM_def)
    apply (rule_tac x = "hcomplex_of_complex x + hcomplex_of_hypreal epsilon" in exI)
    apply (auto intro: CInfinitesimal_add_capprox_self [THEN capprox_sym]
                simp del: star_of_zero)
    done

    (* [| k ≠ 0; (%x. k) -- x --NSC> 0 |] ==> R *)
    lemmas NSCLIM_not_zeroE = NSCLIM_not_zero [THEN notE, standard]

    lemma CLIM_not_zero: "k ≠ 0 ==> ~ ((%x. k) -- x --C> 0)"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_not_zero)

    (*** NSCLIM_const hence CLIM_const ***)

    lemma NSCLIM_const_eq: "(%x. k) -- x --NSC> L ==> k = L"
    apply (rule ccontr)
    apply (drule NSCLIM_zero)
    apply (rule NSCLIM_not_zeroE [of "k-L"], auto)
    done

    lemma CLIM_const_eq: "(%x. k) -- x --C> L ==> k = L"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_const_eq)

    (*** NSCLIM and hence CLIM are unique ***)

    lemma NSCLIM_unique: "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M"
    apply (drule NSCLIM_minus)
    apply (drule NSCLIM_add, assumption)
    apply (auto dest!: NSCLIM_const_eq [symmetric])
    done

    lemma CLIM_unique: "[| f -- x --C> L; f -- x --C> M |] ==> L = M"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_unique)

    (***  NSCLIM_mult_zero and CLIM_mult_zero ***)

    lemma NSCLIM_mult_zero:
         "[| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f(x)*g(x)) -- x --NSC> 0"
    by (drule NSCLIM_mult, auto)

    lemma CLIM_mult_zero:
         "[| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f(x)*g(x)) -- x --C> 0"
    by (drule CLIM_mult, auto)

    (*** NSCLIM_self hence CLIM_self ***)

    lemma NSCLIM_self: "(%x. x) -- a --NSC> a"
    by (auto simp add: NSCLIM_def intro: starfunC_Idfun_capprox)

    lemma CLIM_self: "(%x. x) -- a --C> a"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_self)

    (** another equivalence result **)
    lemma NSCLIM_NSCRLIM_iff:
       "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
    apply (auto simp add: NSCLIM_def NSCRLIM_def CInfinitesimal_capprox_minus [symmetric] CInfinitesimal_hcmod_iff)
    apply (auto dest!: spec)
    apply (rule_tac [!] x = xa in star_cases)
    apply (auto simp add: star_n_diff starfun hcmod mem_infmal_iff star_of_def)
    done

    (** much, much easier standard proof **)
    lemma CLIM_CRLIM_iff: "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)"
    by (simp add: CLIM_def CRLIM_def)

    (* so this is nicer nonstandard proof *)
    lemma NSCLIM_NSCRLIM_iff2:
         "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"
    by (simp add: CRLIM_NSCRLIM_iff [symmetric] CLIM_CRLIM_iff CLIM_NSCLIM_iff [symmetric])

    lemma NSCLIM_NSCRLIM_Re_Im_iff:
         "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) &
                                (%x. Im(f x)) -- a --NSCR> Im(L))"
    apply (auto intro: NSCLIM_NSCRLIM_Re NSCLIM_NSCRLIM_Im)
    apply (auto simp add: NSCLIM_def NSCRLIM_def)
    apply (auto dest!: spec)
    apply (rule_tac x = x in star_cases)
    apply (simp add: capprox_approx_iff starfun star_of_def)
    done

    lemma CLIM_CRLIM_Re_Im_iff:
         "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) &
                             (%x. Im(f x)) -- a --CR> Im(L))"
    by (simp add: CLIM_NSCLIM_iff CRLIM_NSCRLIM_iff NSCLIM_NSCRLIM_Re_Im_iff)

    subsection{*Continuity*}

    lemma isNSContcD:
          "[| isNSContc f a; y @c= hcomplex_of_complex a |]
           ==> ( *f* f) y @c= hcomplex_of_complex (f a)"
    by (simp add: isNSContc_def)

    lemma isNSContc_NSCLIM: "isNSContc f a ==> f -- a --NSC> (f a) "
    by (simp add: isNSContc_def NSCLIM_def)

    lemma NSCLIM_isNSContc:
          "f -- a --NSC> (f a) ==> isNSContc f a"
    apply (simp add: isNSContc_def NSCLIM_def, auto)
    apply (case_tac "y = hcomplex_of_complex a", auto)
    done

    text{*Nonstandard continuity can be defined using NS Limit in
    similar fashion to standard definition of continuity*}

    lemma isNSContc_NSCLIM_iff: "(isNSContc f a) = (f -- a --NSC> (f a))"
    by (blast intro: isNSContc_NSCLIM NSCLIM_isNSContc)

    lemma isNSContc_CLIM_iff: "(isNSContc f a) = (f -- a --C> (f a))"
    by (simp add: CLIM_NSCLIM_iff isNSContc_NSCLIM_iff)

    (*** key result for continuity ***)
    lemma isNSContc_isContc_iff: "(isNSContc f a) = (isContc f a)"
    by (simp add: isContc_def isNSContc_CLIM_iff)

    lemma isContc_isNSContc: "isContc f a ==> isNSContc f a"
    by (erule isNSContc_isContc_iff [THEN iffD2])

    lemma isNSContc_isContc: "isNSContc f a ==> isContc f a"
    by (erule isNSContc_isContc_iff [THEN iffD1])

    text{*Alternative definition of continuity*}
    lemma NSCLIM_h_iff: "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"
    apply (simp add: NSCLIM_def, auto)
    apply (drule_tac x = "hcomplex_of_complex a + x" in spec)
    apply (drule_tac [2] x = "- hcomplex_of_complex a + x" in spec, safe, simp)
    apply (rule mem_cinfmal_iff [THEN iffD2, THEN CInfinitesimal_add_capprox_self [THEN capprox_sym]])
    apply (rule_tac [4] capprox_minus_iff2 [THEN iffD1])
     prefer 3 apply (simp add: compare_rls add_commute)
    apply (rule_tac [2] x = x in star_cases)
    apply (rule_tac [4] x = x in star_cases)
    apply (auto simp add: starfun star_n_minus star_n_add star_of_def)
    done

    lemma NSCLIM_isContc_iff:
         "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"
    by (rule NSCLIM_h_iff)

    lemma CLIM_isContc_iff: "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"
    by (simp add: CLIM_NSCLIM_iff NSCLIM_isContc_iff)

    lemma isContc_iff: "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"
    by (simp add: isContc_def CLIM_isContc_iff)

    lemma isContc_add:
         "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"
    by (auto intro: capprox_add simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)

    lemma isContc_mult:
         "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"
    by (auto intro!: starfun_mult_CFinite_capprox
                [simplified starfun_mult [symmetric]]
                simp add: isNSContc_isContc_iff [symmetric] isNSContc_def)

    lemma isContc_o: "[| isContc f a; isContc g (f a) |] ==> isContc (g o f) a"
    by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfun_o [symmetric])

    lemma isContc_o2:
         "[| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a"
    by (auto dest: isContc_o simp add: o_def)

    lemma isNSContc_minus: "isNSContc f a ==> isNSContc (%x. - f x) a"
    by (simp add: isNSContc_def)

    lemma isContc_minus: "isContc f a ==> isContc (%x. - f x) a"
    by (simp add: isNSContc_isContc_iff [symmetric] isNSContc_minus)

    lemma isContc_inverse:
          "[| isContc f x; f x ≠ 0 |] ==> isContc (%x. inverse (f x)) x"
    by (simp add: isContc_def CLIM_inverse)

    lemma isNSContc_inverse:
         "[| isNSContc f x; f x ≠ 0 |] ==> isNSContc (%x. inverse (f x)) x"
    by (auto intro: isContc_inverse simp add: isNSContc_isContc_iff)

    lemma isContc_diff:
          "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"
    apply (simp add: diff_minus)
    apply (auto intro: isContc_add isContc_minus)
    done

    lemma isContc_const [simp]: "isContc (%x. k) a"
    by (simp add: isContc_def)

    lemma isNSContc_const [simp]: "isNSContc (%x. k) a"
    by (simp add: isNSContc_def)

    subsection{*Functions from Complex to Reals*}

    lemma isNSContCRD:
          "[| isNSContCR f a; y @c= hcomplex_of_complex a |]
           ==> ( *f* f) y @= hypreal_of_real (f a)"
    by (simp add: isNSContCR_def)

    lemma isNSContCR_NSCRLIM: "isNSContCR f a ==> f -- a --NSCR> (f a) "
    by (simp add: isNSContCR_def NSCRLIM_def)

    lemma NSCRLIM_isNSContCR: "f -- a --NSCR> (f a) ==> isNSContCR f a"
    apply (auto simp add: isNSContCR_def NSCRLIM_def)
    apply (case_tac "y = hcomplex_of_complex a", auto)
    done

    lemma isNSContCR_NSCRLIM_iff: "(isNSContCR f a) = (f -- a --NSCR> (f a))"
    by (blast intro: isNSContCR_NSCRLIM NSCRLIM_isNSContCR)

    lemma isNSContCR_CRLIM_iff: "(isNSContCR f a) = (f -- a --CR> (f a))"
    by (simp add: CRLIM_NSCRLIM_iff isNSContCR_NSCRLIM_iff)

    (*** another key result for continuity ***)
    lemma isNSContCR_isContCR_iff: "(isNSContCR f a) = (isContCR f a)"
    by (simp add: isContCR_def isNSContCR_CRLIM_iff)

    lemma isContCR_isNSContCR: "isContCR f a ==> isNSContCR f a"
    by (erule isNSContCR_isContCR_iff [THEN iffD2])

    lemma isNSContCR_isContCR: "isNSContCR f a ==> isContCR f a"
    by (erule isNSContCR_isContCR_iff [THEN iffD1])

    lemma isNSContCR_cmod [simp]: "isNSContCR cmod (a)"
    by (auto intro: capprox_hcmod_approx
             simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric]
                        isNSContCR_def)

    lemma isContCR_cmod [simp]: "isContCR cmod (a)"
    by (simp add: isNSContCR_isContCR_iff [symmetric])

    lemma isContc_isContCR_Re: "isContc f a ==> isContCR (%x. Re (f x)) a"
    by (simp add: isContc_def isContCR_def CLIM_CRLIM_Re)

    lemma isContc_isContCR_Im: "isContc f a ==> isContCR (%x. Im (f x)) a"
    by (simp add: isContc_def isContCR_def CLIM_CRLIM_Im)

    subsection{*Derivatives*}

    lemma CDERIV_iff: "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
    by (simp add: cderiv_def)

    lemma CDERIV_NSC_iff:
          "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
    by (simp add: cderiv_def CLIM_NSCLIM_iff)

    lemma CDERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D"
    by (simp add: cderiv_def)

    lemma NSC_DERIVD: "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D"
    by (simp add: cderiv_def CLIM_NSCLIM_iff)

    text{*Uniqueness*}
    lemma CDERIV_unique: "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E"
    by (simp add: cderiv_def CLIM_unique)

    (*** uniqueness: a nonstandard proof ***)
    lemma NSCDeriv_unique: "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E"
    apply (simp add: nscderiv_def)
    apply (auto dest!: bspec [where x = "hcomplex_of_hypreal epsilon"]
                intro!: inj_hcomplex_of_complex [THEN injD] dest: capprox_trans3)
    done

    subsection{* Differentiability*}

    lemma CDERIV_CLIM_iff:
         "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) =
          ((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)"
    apply (simp add: CLIM_def)
    apply (rule_tac f=All in arg_cong)
    apply (rule ext)
    apply (rule imp_cong)
    apply (rule refl)
    apply (rule_tac f=Ex in arg_cong)
    apply (rule ext)
    apply (rule conj_cong)
    apply (rule refl)
    apply (rule trans)
    apply (rule all_shift [where a=a], simp)
    done

    lemma CDERIV_iff2:
         "(CDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)"
    by (simp add: cderiv_def CDERIV_CLIM_iff)

    subsection{* Equivalence of NS and Standard Differentiation*}

    (*** first equivalence ***)
    lemma NSCDERIV_NSCLIM_iff:
          "(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"
    apply (simp add: nscderiv_def NSCLIM_def, auto)
    apply (drule_tac x = xa in bspec)
    apply (rule_tac [3] ccontr)
    apply (drule_tac [3] x = h in spec)
    apply (auto simp add: mem_cinfmal_iff starfun_lambda_cancel)
    done

    (*** 2nd equivalence ***)
    lemma NSCDERIV_NSCLIM_iff2:
         "(NSCDERIV f x :> D) = ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)"
    by (simp add: NSCDERIV_NSCLIM_iff CDERIV_CLIM_iff CLIM_NSCLIM_iff [symmetric])

    lemma NSCDERIV_iff2:
         "(NSCDERIV f x :> D) =
          (∀xa. xa ≠ hcomplex_of_complex x & xa @c= hcomplex_of_complex x -->
            ( *f* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"
    by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)

    lemma NSCDERIV_CDERIV_iff: "(NSCDERIV f x :> D) = (CDERIV f x :> D)"
    by (simp add: cderiv_def NSCDERIV_NSCLIM_iff CLIM_NSCLIM_iff)

    lemma NSCDERIV_isNSContc: "NSCDERIV f x :> D ==> isNSContc f x"
    apply (auto simp add: nscderiv_def isNSContc_NSCLIM_iff NSCLIM_def diff_minus)
    apply (drule capprox_minus_iff [THEN iffD1])
    apply (subgoal_tac "xa + - (hcomplex_of_complex x) ≠ 0")
     prefer 2 apply (simp add: compare_rls)
    apply (drule_tac x = "- hcomplex_of_complex x + xa" in bspec)
     prefer 2 apply (simp add: add_assoc [symmetric])
    apply (auto simp add: mem_cinfmal_iff [symmetric] add_commute)
    apply (drule_tac c = "xa + - hcomplex_of_complex x" in capprox_mult1)
    apply (auto intro: CInfinitesimal_subset_CFinite [THEN subsetD]
                simp add: mult_assoc)
    apply (drule_tac x3 = D in
           CFinite_hcomplex_of_complex [THEN [2] CInfinitesimal_CFinite_mult,
                                        THEN mem_cinfmal_iff [THEN iffD1]])
    apply (blast intro: capprox_trans mult_commute [THEN subst] capprox_minus_iff [THEN iffD2])
    done

    lemma CDERIV_isContc: "CDERIV f x :> D ==> isContc f x"
    by (simp add: NSCDERIV_CDERIV_iff [symmetric] isNSContc_isContc_iff [symmetric] NSCDERIV_isNSContc)

    text{* Differentiation rules for combinations of functions follow by clear,
    straightforard algebraic manipulations*}

    (* use simple constant nslimit theorem *)
    lemma NSCDERIV_const [simp]: "(NSCDERIV (%x. k) x :> 0)"
    by (simp add: NSCDERIV_NSCLIM_iff)

    lemma CDERIV_const [simp]: "(CDERIV (%x. k) x :> 0)"
    by (simp add: NSCDERIV_CDERIV_iff [symmetric])

    lemma NSCDERIV_add:
         "[| NSCDERIV f x :> Da;  NSCDERIV g x :> Db |]
          ==> NSCDERIV (%x. f x + g x) x :> Da + Db"
    apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify)
    apply (auto dest!: spec simp add: add_divide_distrib diff_minus)
    apply (drule_tac b = "hcomplex_of_complex Da" and d = "hcomplex_of_complex Db" in capprox_add)
    apply (auto simp add: add_ac)
    done

    lemma CDERIV_add:
         "[| CDERIV f x :> Da; CDERIV g x :> Db |]
          ==> CDERIV (%x. f x + g x) x :> Da + Db"
    by (simp add: NSCDERIV_add NSCDERIV_CDERIV_iff [symmetric])

    subsection{*Lemmas for Multiplication*}

    lemma lemma_nscderiv1: "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"
    by (simp add: right_diff_distrib)

    lemma lemma_nscderiv2:
         "[| (x + y) / z = hcomplex_of_complex D + yb; z ≠ 0;
             z : CInfinitesimal; yb : CInfinitesimal |]
          ==> x + y @c= 0"
    apply (frule_tac c1 = z in hcomplex_mult_right_cancel [THEN iffD2], assumption)
    apply (erule_tac V = " (x + y) / z = hcomplex_of_complex D + yb" in thin_rl)
    apply (auto intro!: CInfinitesimal_CFinite_mult2 CFinite_add
                simp add: mem_cinfmal_iff [symmetric])
    apply (erule CInfinitesimal_subset_CFinite [THEN subsetD])
    done

    lemma NSCDERIV_mult:
         "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
          ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
    apply (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def, clarify)
    apply (auto dest!: spec
                simp add: starfun_lambda_cancel lemma_nscderiv1)
    apply (simp (no_asm) add: add_divide_distrib)
    apply (drule bex_CInfinitesimal_iff2 [THEN iffD2])+
    apply (auto simp del: times_divide_eq_right simp add: times_divide_eq_right [symmetric])
    apply (simp add: diff_minus)
    apply (drule_tac D = Db in lemma_nscderiv2)
    apply (drule_tac [4]
            capprox_minus_iff [THEN iffD2, THEN bex_CInfinitesimal_iff2 [THEN iffD2]])
    apply (auto intro!: capprox_add_mono1 simp add: left_distrib right_distrib mult_commute add_assoc)
    apply (rule_tac b1 = "hcomplex_of_complex Db * hcomplex_of_complex (f x) " in add_commute [THEN subst])
    apply (auto intro!: CInfinitesimal_add_capprox_self2 [THEN capprox_sym]
                        CInfinitesimal_add CInfinitesimal_mult
                        CInfinitesimal_hcomplex_of_complex_mult
                        CInfinitesimal_hcomplex_of_complex_mult2
                simp add: add_assoc [symmetric])
    done

    lemma CDERIV_mult:
         "[| CDERIV f x :> Da; CDERIV g x :> Db |]
          ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"
    by (simp add: NSCDERIV_mult NSCDERIV_CDERIV_iff [symmetric])

    lemma NSCDERIV_cmult: "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"
    apply (simp add: times_divide_eq_right [symmetric] NSCDERIV_NSCLIM_iff
                     minus_mult_right right_distrib [symmetric] diff_minus
                del: times_divide_eq_right minus_mult_right [symmetric])
    apply (erule NSCLIM_const [THEN NSCLIM_mult])
    done

    lemma CDERIV_cmult: "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"
    by (simp add: NSCDERIV_cmult NSCDERIV_CDERIV_iff [symmetric])

    lemma NSCDERIV_minus: "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"
    apply (simp add: NSCDERIV_NSCLIM_iff diff_minus)
    apply (rule_tac t = "f x" in minus_minus [THEN subst])
    apply (simp (no_asm_simp) add: minus_add_distrib [symmetric]
                del: minus_add_distrib minus_minus)
    apply (erule NSCLIM_minus)
    done

    lemma CDERIV_minus: "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D"
    by (simp add: NSCDERIV_minus NSCDERIV_CDERIV_iff [symmetric])

    lemma NSCDERIV_add_minus:
         "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
          ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db"
    by (blast dest: NSCDERIV_add NSCDERIV_minus)

    lemma CDERIV_add_minus:
         "[| CDERIV f x :> Da; CDERIV g x :> Db |]
          ==> CDERIV (%x. f x + -g x) x :> Da + -Db"
    by (blast dest: CDERIV_add CDERIV_minus)

    lemma NSCDERIV_diff:
         "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
          ==> NSCDERIV (%x. f x - g x) x :> Da - Db"
    by (simp add: diff_minus NSCDERIV_add_minus)

    lemma CDERIV_diff:
         "[| CDERIV f x :> Da; CDERIV g x :> Db |]
           ==> CDERIV (%x. f x - g x) x :> Da - Db"
    by (simp add: diff_minus CDERIV_add_minus)

    subsection{*Chain Rule*}

    (* lemmas *)
    lemma NSCDERIV_zero:
          "[| NSCDERIV g x :> D;
              ( *f* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);
              xa : CInfinitesimal; xa ≠ 0
           |] ==> D = 0"
    apply (simp add: nscderiv_def)
    apply (drule bspec, auto)
    done

    lemma NSCDERIV_capprox:
      "[| NSCDERIV f x :> D;  h: CInfinitesimal;  h ≠ 0 |]
       ==> ( *f* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0"
    apply (simp add: nscderiv_def mem_cinfmal_iff [symmetric])
    apply (rule CInfinitesimal_ratio)
    apply (rule_tac [3] capprox_hcomplex_of_complex_CFinite, auto)
    done

    (*--------------------------------------------------*)
    (* from one version of differentiability            *)
    (*                                                  *)
    (*   f(x) - f(a)                                    *)
    (* --------------- @= Db                            *)
    (*     x - a                                        *)
    (* -------------------------------------------------*)

    lemma NSCDERIVD1:
       "[| NSCDERIV f (g x) :> Da;
           ( *f* g) (hcomplex_of_complex(x) + xa) ≠ hcomplex_of_complex (g x);
           ( *f* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|]
        ==> (( *f* f) (( *f* g) (hcomplex_of_complex(x) + xa))
             - hcomplex_of_complex (f (g x))) /
            (( *f* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x))
               @c= hcomplex_of_complex (Da)"
    by (simp add: NSCDERIV_NSCLIM_iff2 NSCLIM_def)

    (*--------------------------------------------------*)
    (* from other version of differentiability          *)
    (*                                                  *)
    (*  f(x + h) - f(x)                                 *)
    (* ----------------- @= Db                          *)
    (*         h                                        *)
    (*--------------------------------------------------*)

    lemma NSCDERIVD2:
      "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa ≠ 0 |]
       ==> (( *f* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa
           @c= hcomplex_of_complex (Db)"
    by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfun_lambda_cancel)

    lemma lemma_complex_chain: "(z::hcomplex) ≠ 0 ==> x*y = (x*inverse(z))*(z*y)"
    by auto

    text{*Chain rule*}
    theorem NSCDERIV_chain:
         "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |]
          ==> NSCDERIV (f o g) x :> Da * Db"
    apply (simp (no_asm_simp) add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff [symmetric])
    apply safe
    apply (frule_tac f = g in NSCDERIV_capprox)
    apply (auto simp add: starfun_lambda_cancel2 starfun_o [symmetric])
    apply (case_tac "( *f* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ")
    apply (drule_tac g = g in NSCDERIV_zero)
    apply (auto simp add: divide_inverse)
    apply (rule_tac z1 = "( *f* g) (hcomplex_of_complex (x) + xa) - hcomplex_of_complex (g x) " and y1 = "inverse xa" in lemma_complex_chain [THEN ssubst])
    apply (simp (no_asm_simp))
    apply (rule capprox_mult_hcomplex_of_complex)
    apply (auto intro!: NSCDERIVD1 intro: capprox_minus_iff [THEN iffD2]
                simp add: diff_minus [symmetric] divide_inverse [symmetric])
    apply (blast intro: NSCDERIVD2)
    done

    text{*standard version*}
    lemma CDERIV_chain:
         "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
          ==> CDERIV (f o g) x :> Da * Db"
    by (simp add: NSCDERIV_CDERIV_iff [symmetric] NSCDERIV_chain)

    lemma CDERIV_chain2:
         "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |]
          ==> CDERIV (%x. f (g x)) x :> Da * Db"
    by (auto dest: CDERIV_chain simp add: o_def)

    subsection{* Differentiation of Natural Number Powers*}

    lemma NSCDERIV_Id [simp]: "NSCDERIV (%x. x) x :> 1"
    by (simp add: NSCDERIV_NSCLIM_iff NSCLIM_def divide_self del: divide_self_if)

    lemma CDERIV_Id [simp]: "CDERIV (%x. x) x :> 1"
    by (simp add: NSCDERIV_CDERIV_iff [symmetric])

    lemmas isContc_Id = CDERIV_Id [THEN CDERIV_isContc, standard]

    text{*derivative of linear multiplication*}
    lemma CDERIV_cmult_Id [simp]: "CDERIV (op * c) x :> c"
    by (cut_tac c = c and x = x in CDERIV_Id [THEN CDERIV_cmult], simp)

    lemma NSCDERIV_cmult_Id [simp]: "NSCDERIV (op * c) x :> c"
    by (simp add: NSCDERIV_CDERIV_iff)

    lemma CDERIV_pow [simp]:
         "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - Suc 0))"
    apply (induct_tac "n")
    apply (drule_tac [2] CDERIV_Id [THEN CDERIV_mult])
    apply (auto simp add: left_distrib real_of_nat_Suc)
    apply (case_tac "n")
    apply (auto simp add: mult_ac add_commute)
    done

    text{*Nonstandard version*}
    lemma NSCDERIV_pow:
         "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"
    by (simp add: NSCDERIV_CDERIV_iff)

    lemma lemma_CDERIV_subst:
         "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E"
    by auto

    (*used once, in NSCDERIV_inverse*)
    lemma CInfinitesimal_add_not_zero:
         "[| h: CInfinitesimal; x ≠ 0 |] ==> hcomplex_of_complex x + h ≠ 0"
    apply clarify
    apply (drule equals_zero_I, auto)
    done

    text{*Can't relax the premise @{term "x ≠ 0"}: it isn't continuous at zero*}
    lemma NSCDERIV_inverse:
         "x ≠ 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"
    apply (simp add: nscderiv_def Ball_def, clarify)
    apply (frule CInfinitesimal_add_not_zero [where x=x])
    apply (auto simp add: starfun_inverse_inverse diff_minus
               simp del: minus_mult_left [symmetric] minus_mult_right [symmetric])
    apply (simp add: add_commute numeral_2_eq_2 inverse_add
                     inverse_mult_distrib [symmetric] inverse_minus_eq [symmetric]
                     add_ac mult_ac
                del: inverse_minus_eq inverse_mult_distrib
                     minus_mult_right [symmetric] minus_mult_left [symmetric])
    apply (simp only: mult_assoc [symmetric] right_distrib)
    apply (rule_tac y = " inverse (- hcomplex_of_complex x * hcomplex_of_complex x) " in capprox_trans)
    apply (rule inverse_add_CInfinitesimal_capprox2)
    apply (auto dest!: hcomplex_of_complex_CFinite_diff_CInfinitesimal
                intro: CFinite_mult
                simp add: inverse_minus_eq [symmetric])
    apply (rule CInfinitesimal_CFinite_mult2, auto)
    done

    lemma CDERIV_inverse:
         "x ≠ 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"
    by (simp add: NSCDERIV_inverse NSCDERIV_CDERIV_iff [symmetric]
             del: complexpow_Suc)

    subsection{*Derivative of Reciprocals (Function @{term inverse})*}

    lemma CDERIV_inverse_fun:
         "[| CDERIV f x :> d; f(x) ≠ 0 |]
          ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
    apply (rule mult_commute [THEN subst])
    apply (simp add: minus_mult_left power_inverse
                del: complexpow_Suc minus_mult_left [symmetric])
    apply (fold o_def)
    apply (blast intro!: CDERIV_chain CDERIV_inverse)
    done

    lemma NSCDERIV_inverse_fun:
         "[| NSCDERIV f x :> d; f(x) ≠ 0 |]
          ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"
    by (simp add: NSCDERIV_CDERIV_iff CDERIV_inverse_fun del: complexpow_Suc)

    subsection{* Derivative of Quotient*}

    lemma CDERIV_quotient:
         "[| CDERIV f x :> d; CDERIV g x :> e; g(x) ≠ 0 |]
           ==> CDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
    apply (simp add: diff_minus)
    apply (drule_tac f = g in CDERIV_inverse_fun)
    apply (drule_tac [2] CDERIV_mult, assumption+)
    apply (simp add: divide_inverse right_distrib power_inverse minus_mult_left
                     mult_ac
                del: minus_mult_right [symmetric] minus_mult_left [symmetric]
                     complexpow_Suc)
    done

    lemma NSCDERIV_quotient:
         "[| NSCDERIV f x :> d; NSCDERIV g x :> e; g(x) ≠ 0 |]
           ==> NSCDERIV (%y. f(y) / (g y)) x :> (d*g(x) - (e*f(x))) / (g(x) ^ 2)"
    by (simp add: NSCDERIV_CDERIV_iff CDERIV_quotient del: complexpow_Suc)

    subsection{*Caratheodory Formulation of Derivative at a Point: Standard Proof*}

    lemma CLIM_equal:
          "[| ∀x. x ≠ a --> (f x = g x) |] ==> (f -- a --C> l) = (g -- a --C> l)"
    by (simp add: CLIM_def complex_add_minus_iff)

    lemma CLIM_trans:
         "[| (%x. f(x) + -g(x)) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l"
    apply (drule CLIM_add, assumption)
    apply (simp add: complex_add_assoc)
    done

    lemma CARAT_CDERIV:
         "(CDERIV f x :> l) =
          (∃g. (∀z. f z - f x = g z * (z - x)) & isContc g x & g x = l)"
    apply safe
    apply (rule_tac x = "%z. if z=x then l else (f (z) - f (x)) / (z-x)" in exI)
    apply (auto simp add: mult_assoc isContc_iff CDERIV_iff)
    apply (rule_tac [!] CLIM_equal [THEN iffD1], auto)
    done

    lemma CARAT_NSCDERIV:
         "NSCDERIV f x :> l ==>
          ∃g. (∀z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"
    by (simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV)

    lemma CARAT_CDERIVD:
         "(∀z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l
          ==> NSCDERIV f x :> l"
    by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq);

    ML
    {*
    val complex_add_minus_iff = thm "complex_add_minus_iff";
    val complex_add_eq_0_iff = thm "complex_add_eq_0_iff";
    val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re";
    val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im";
    val CLIM_NSCLIM = thm "CLIM_NSCLIM";
    val eq_Abs_star_ALL = thm "eq_Abs_star_ALL";
    val lemma_CLIM = thm "lemma_CLIM";
    val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2";
    val lemma_csimp = thm "lemma_csimp";
    val NSCLIM_CLIM = thm "NSCLIM_CLIM";
    val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff";
    val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM";
    val lemma_CRLIM = thm "lemma_CRLIM";
    val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2";
    val lemma_crsimp = thm "lemma_crsimp";
    val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM";
    val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff";
    val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re";
    val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im";
    val CLIM_cnj = thm "CLIM_cnj";
    val CLIM_cnj_iff = thm "CLIM_cnj_iff";
    val NSCLIM_add = thm "NSCLIM_add";
    val CLIM_add = thm "CLIM_add";
    val NSCLIM_mult = thm "NSCLIM_mult";
    val CLIM_mult = thm "CLIM_mult";
    val NSCLIM_const = thm "NSCLIM_const";
    val CLIM_const = thm "CLIM_const";
    val NSCLIM_minus = thm "NSCLIM_minus";
    val CLIM_minus = thm "CLIM_minus";
    val NSCLIM_diff = thm "NSCLIM_diff";
    val CLIM_diff = thm "CLIM_diff";
    val NSCLIM_inverse = thm "NSCLIM_inverse";
    val CLIM_inverse = thm "CLIM_inverse";
    val NSCLIM_zero = thm "NSCLIM_zero";
    val CLIM_zero = thm "CLIM_zero";
    val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel";
    val CLIM_zero_cancel = thm "CLIM_zero_cancel";
    val NSCLIM_not_zero = thm "NSCLIM_not_zero";
    val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE";
    val CLIM_not_zero = thm "CLIM_not_zero";
    val NSCLIM_const_eq = thm "NSCLIM_const_eq";
    val CLIM_const_eq = thm "CLIM_const_eq";
    val NSCLIM_unique = thm "NSCLIM_unique";
    val CLIM_unique = thm "CLIM_unique";
    val NSCLIM_mult_zero = thm "NSCLIM_mult_zero";
    val CLIM_mult_zero = thm "CLIM_mult_zero";
    val NSCLIM_self = thm "NSCLIM_self";
    val CLIM_self = thm "CLIM_self";
    val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff";
    val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff";
    val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2";
    val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff";
    val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff";
    val isNSContcD = thm "isNSContcD";
    val isNSContc_NSCLIM = thm "isNSContc_NSCLIM";
    val NSCLIM_isNSContc = thm "NSCLIM_isNSContc";
    val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff";
    val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff";
    val isNSContc_isContc_iff = thm "isNSContc_isContc_iff";
    val isContc_isNSContc = thm "isContc_isNSContc";
    val isNSContc_isContc = thm "isNSContc_isContc";
    val NSCLIM_h_iff = thm "NSCLIM_h_iff";
    val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff";
    val CLIM_isContc_iff = thm "CLIM_isContc_iff";
    val isContc_iff = thm "isContc_iff";
    val isContc_add = thm "isContc_add";
    val isContc_mult = thm "isContc_mult";
    val isContc_o = thm "isContc_o";
    val isContc_o2 = thm "isContc_o2";
    val isNSContc_minus = thm "isNSContc_minus";
    val isContc_minus = thm "isContc_minus";
    val isContc_inverse = thm "isContc_inverse";
    val isNSContc_inverse = thm "isNSContc_inverse";
    val isContc_diff = thm "isContc_diff";
    val isContc_const = thm "isContc_const";
    val isNSContc_const = thm "isNSContc_const";
    val isNSContCRD = thm "isNSContCRD";
    val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM";
    val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR";
    val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff";
    val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff";
    val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff";
    val isContCR_isNSContCR = thm "isContCR_isNSContCR";
    val isNSContCR_isContCR = thm "isNSContCR_isContCR";
    val isNSContCR_cmod = thm "isNSContCR_cmod";
    val isContCR_cmod = thm "isContCR_cmod";
    val isContc_isContCR_Re = thm "isContc_isContCR_Re";
    val isContc_isContCR_Im = thm "isContc_isContCR_Im";
    val CDERIV_iff = thm "CDERIV_iff";
    val CDERIV_NSC_iff = thm "CDERIV_NSC_iff";
    val CDERIVD = thm "CDERIVD";
    val NSC_DERIVD = thm "NSC_DERIVD";
    val CDERIV_unique = thm "CDERIV_unique";
    val NSCDeriv_unique = thm "NSCDeriv_unique";
    val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff";
    val CDERIV_iff2 = thm "CDERIV_iff2";
    val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff";
    val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2";
    val NSCDERIV_iff2 = thm "NSCDERIV_iff2";
    val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff";
    val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc";
    val CDERIV_isContc = thm "CDERIV_isContc";
    val NSCDERIV_const = thm "NSCDERIV_const";
    val CDERIV_const = thm "CDERIV_const";
    val NSCDERIV_add = thm "NSCDERIV_add";
    val CDERIV_add = thm "CDERIV_add";
    val lemma_nscderiv1 = thm "lemma_nscderiv1";
    val lemma_nscderiv2 = thm "lemma_nscderiv2";
    val NSCDERIV_mult = thm "NSCDERIV_mult";
    val CDERIV_mult = thm "CDERIV_mult";
    val NSCDERIV_cmult = thm "NSCDERIV_cmult";
    val CDERIV_cmult = thm "CDERIV_cmult";
    val NSCDERIV_minus = thm "NSCDERIV_minus";
    val CDERIV_minus = thm "CDERIV_minus";
    val NSCDERIV_add_minus = thm "NSCDERIV_add_minus";
    val CDERIV_add_minus = thm "CDERIV_add_minus";
    val NSCDERIV_diff = thm "NSCDERIV_diff";
    val CDERIV_diff = thm "CDERIV_diff";
    val NSCDERIV_zero = thm "NSCDERIV_zero";
    val NSCDERIV_capprox = thm "NSCDERIV_capprox";
    val NSCDERIVD1 = thm "NSCDERIVD1";
    val NSCDERIVD2 = thm "NSCDERIVD2";
    val lemma_complex_chain = thm "lemma_complex_chain";
    val NSCDERIV_chain = thm "NSCDERIV_chain";
    val CDERIV_chain = thm "CDERIV_chain";
    val CDERIV_chain2 = thm "CDERIV_chain2";
    val NSCDERIV_Id = thm "NSCDERIV_Id";
    val CDERIV_Id = thm "CDERIV_Id";
    val isContc_Id = thms "isContc_Id";
    val CDERIV_cmult_Id = thm "CDERIV_cmult_Id";
    val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id";
    val CDERIV_pow = thm "CDERIV_pow";
    val NSCDERIV_pow = thm "NSCDERIV_pow";
    val lemma_CDERIV_subst = thm "lemma_CDERIV_subst";
    val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero";
    val NSCDERIV_inverse = thm "NSCDERIV_inverse";
    val CDERIV_inverse = thm "CDERIV_inverse";
    val CDERIV_inverse_fun = thm "CDERIV_inverse_fun";
    val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun";
    val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared";
    val CDERIV_quotient = thm "CDERIV_quotient";
    val NSCDERIV_quotient = thm "NSCDERIV_quotient";
    val CLIM_equal = thm "CLIM_equal";
    val CLIM_trans = thm "CLIM_trans";
    val CARAT_CDERIV = thm "CARAT_CDERIV";
    val CARAT_NSCDERIV = thm "CARAT_NSCDERIV";
    val CARAT_CDERIVD = thm "CARAT_CDERIVD";
    *}

    end

lemma lemma_complex_mult_inverse_squared:

      x ≠ 0 ==> x * (inverse x)² = inverse x

lemma all_shift:

      (∀x. P x) = (∀x. P (x - a))

lemma complex_add_minus_iff:

      (x + - a = 0) = (x = a)

lemma complex_add_eq_0_iff:

      (x + y = 0) = (y = - x)

### Limit of Complex to Complex Function

lemma NSCLIM_NSCRLIM_Re:

      f -- a --NSC> L ==> (%x. Re (f x)) -- a --NSCR> Re L

lemma NSCLIM_NSCRLIM_Im:

      f -- a --NSC> L ==> (%x. Im (f x)) -- a --NSCR> Im L

lemma CLIM_NSCLIM:

      f -- x --C> L ==> f -- x --NSC> L

lemma eq_Abs_star_ALL:

      (∀t. P t) = (∀X. P (star_n X))

lemma lemma_CLIM:

      ∀s>0. ∃xa. xa ≠ x ∧ cmod (xa - x) < s ∧ r ≤ cmod (f xa - L)
      ==> ∀n. ∃xa. xa ≠ x ∧
                   cmod (xa - x) < inverse (real (Suc n)) ∧ r ≤ cmod (f xa - L)

lemma lemma_skolemize_CLIM2:

      ∀s>0. ∃xa. xa ≠ x ∧ cmod (xa - x) < s ∧ r ≤ cmod (f xa - L)
      ==> ∃X. ∀n. X n ≠ x ∧
                  cmod (X n - x) < inverse (real (Suc n)) ∧ r ≤ cmod (f (X n) - L)

lemma lemma_csimp:

      ∀n. X n ≠ x ∧ cmod (X n - x) < inverse (real (Suc n)) ∧ r ≤ cmod (f (X n) - L)
      ==> ∀n. cmod (X n - x) < inverse (real (Suc n))

lemma NSCLIM_CLIM:

      f -- x --NSC> L ==> f -- x --C> L

theorem CLIM_NSCLIM_iff:

      f -- x --C> L = f -- x --NSC> L

### Limit of Complex to Real Function

lemma CRLIM_NSCRLIM:

      f -- x --CR> L ==> f -- x --NSCR> L

lemma lemma_CRLIM:

      ∀s>0. ∃xa. xa ≠ x ∧ cmod (xa - x) < s ∧ r ≤ ¦f xa - L¦
      ==> ∀n. ∃xa. xa ≠ x ∧ cmod (xa - x) < inverse (real (Suc n)) ∧ r ≤ ¦f xa - L¦

lemma lemma_skolemize_CRLIM2:

      ∀s>0. ∃xa. xa ≠ x ∧ cmod (xa - x) < s ∧ r ≤ ¦f xa - L¦
      ==> ∃X. ∀n. X n ≠ x ∧
                  cmod (X n - x) < inverse (real (Suc n)) ∧ r ≤ ¦f (X n) - L¦

lemma lemma_crsimp:

      ∀n. X n ≠ x ∧ cmod (X n - x) < inverse (real (Suc n)) ∧ r ≤ ¦f (X n) - L¦
      ==> ∀n. cmod (X n - x) < inverse (real (Suc n))

lemma NSCRLIM_CRLIM:

      f -- x --NSCR> L ==> f -- x --CR> L

theorem CRLIM_NSCRLIM_iff:

      f -- x --CR> L = f -- x --NSCR> L

lemma CLIM_CRLIM_Re:

      f -- a --C> L ==> (%x. Re (f x)) -- a --CR> Re L

lemma CLIM_CRLIM_Im:

      f -- a --C> L ==> (%x. Im (f x)) -- a --CR> Im L

lemma CLIM_cnj:

      f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L

lemma CLIM_cnj_iff:

      (%x. cnj (f x)) -- a --C> cnj L = f -- a --C> L

lemma NSCLIM_add:

      [| f -- x --NSC> l; g -- x --NSC> m |] ==> (%x. f x + g x) -- x --NSC> l + m

lemma CLIM_add:

      [| f -- x --C> l; g -- x --C> m |] ==> (%x. f x + g x) -- x --C> l + m

lemma NSCLIM_mult:

      [| f -- x --NSC> l; g -- x --NSC> m |] ==> (%x. f x * g x) -- x --NSC> l * m

lemma CLIM_mult:

      [| f -- x --C> l; g -- x --C> m |] ==> (%x. f x * g x) -- x --C> l * m

lemma NSCLIM_const:

      (%x. k) -- x --NSC> k

lemma CLIM_const:

      (%x. k) -- x --C> k

lemma NSCLIM_minus:

      f -- a --NSC> L ==> (%x. - f x) -- a --NSC> - L

lemma CLIM_minus:

      f -- a --C> L ==> (%x. - f x) -- a --C> - L

lemma NSCLIM_diff:

      [| f -- x --NSC> l; g -- x --NSC> m |] ==> (%x. f x - g x) -- x --NSC> l - m

lemma CLIM_diff:

      [| f -- x --C> l; g -- x --C> m |] ==> (%x. f x - g x) -- x --C> l - m

lemma NSCLIM_inverse:

      [| f -- a --NSC> L; L ≠ 0 |] ==> (%x. inverse (f x)) -- a --NSC> inverse L

lemma CLIM_inverse:

      [| f -- a --C> L; L ≠ 0 |] ==> (%x. inverse (f x)) -- a --C> inverse L

lemma NSCLIM_zero:

      f -- a --NSC> l ==> (%x. f x - l) -- a --NSC> 0

lemma CLIM_zero:

      f -- a --C> l ==> (%x. f x - l) -- a --C> 0

lemma NSCLIM_zero_cancel:

      (%x. f x - l) -- x --NSC> 0 ==> f -- x --NSC> l

lemma CLIM_zero_cancel:

      (%x. f x - l) -- x --C> 0 ==> f -- x --C> l

lemma NSCLIM_not_zero:

      k ≠ 0 ==> ¬ (%x. k) -- x --NSC> 0

lemmas NSCLIM_not_zeroE:

      [| k ≠ 0; (%x. k) -- x --NSC> 0 |] ==> R

lemmas NSCLIM_not_zeroE:

      [| k ≠ 0; (%x. k) -- x --NSC> 0 |] ==> R

lemma CLIM_not_zero:

      k ≠ 0 ==> ¬ (%x. k) -- x --C> 0

lemma NSCLIM_const_eq:

      (%x. k) -- x --NSC> L ==> k = L

lemma CLIM_const_eq:

      (%x. k) -- x --C> L ==> k = L

lemma NSCLIM_unique:

      [| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M

lemma CLIM_unique:

      [| f -- x --C> L; f -- x --C> M |] ==> L = M

lemma NSCLIM_mult_zero:

      [| f -- x --NSC> 0; g -- x --NSC> 0 |] ==> (%x. f x * g x) -- x --NSC> 0

lemma CLIM_mult_zero:

      [| f -- x --C> 0; g -- x --C> 0 |] ==> (%x. f x * g x) -- x --C> 0

lemma NSCLIM_self:

      (%x. x) -- a --NSC> a

lemma CLIM_self:

      (%x. x) -- a --C> a

lemma NSCLIM_NSCRLIM_iff:

      f -- x --NSC> L = (%y. cmod (f y - L)) -- x --NSCR> 0

lemma CLIM_CRLIM_iff:

      f -- x --C> L = (%y. cmod (f y - L)) -- x --CR> 0

lemma NSCLIM_NSCRLIM_iff2:

      f -- x --NSC> L = (%y. cmod (f y - L)) -- x --NSCR> 0

lemma NSCLIM_NSCRLIM_Re_Im_iff:

      f -- a --NSC> L =
      ((%x. Re (f x)) -- a --NSCR> Re L ∧ (%x. Im (f x)) -- a --NSCR> Im L)

lemma CLIM_CRLIM_Re_Im_iff:

      f -- a --C> L =
      ((%x. Re (f x)) -- a --CR> Re L ∧ (%x. Im (f x)) -- a --CR> Im L)

### Continuity

lemma isNSContcD:

      [| isNSContc f a; y @c= star_of a |] ==> (*f* f) y @c= star_of (f a)

lemma isNSContc_NSCLIM:

      isNSContc f a ==> f -- a --NSC> f a

lemma NSCLIM_isNSContc:

      f -- a --NSC> f a ==> isNSContc f a

lemma isNSContc_NSCLIM_iff:

      isNSContc f a = f -- a --NSC> f a

lemma isNSContc_CLIM_iff:

      isNSContc f a = f -- a --C> f a

lemma isNSContc_isContc_iff:

      isNSContc f a = isContc f a

lemma isContc_isNSContc:

      isContc f a ==> isNSContc f a

lemma isNSContc_isContc:

      isNSContc f a ==> isContc f a

lemma NSCLIM_h_iff:

      f -- a --NSC> L = (%h. f (a + h)) -- 0 --NSC> L

lemma NSCLIM_isContc_iff:

      f -- a --NSC> f a = (%h. f (a + h)) -- 0 --NSC> f a

lemma CLIM_isContc_iff:

      f -- a --C> f a = (%h. f (a + h)) -- 0 --C> f a

lemma isContc_iff:

      isContc f x = (%h. f (x + h)) -- 0 --C> f x

lemma isContc_add:

      [| isContc f a; isContc g a |] ==> isContc (%x. f x + g x) a

lemma isContc_mult:

      [| isContc f a; isContc g a |] ==> isContc (%x. f x * g x) a

lemma isContc_o:

      [| isContc f a; isContc g (f a) |] ==> isContc (g o f) a

lemma isContc_o2:

      [| isContc f a; isContc g (f a) |] ==> isContc (%x. g (f x)) a

lemma isNSContc_minus:

      isNSContc f a ==> isNSContc (%x. - f x) a

lemma isContc_minus:

      isContc f a ==> isContc (%x. - f x) a

lemma isContc_inverse:

      [| isContc f x; f x ≠ 0 |] ==> isContc (%x. inverse (f x)) x

lemma isNSContc_inverse:

      [| isNSContc f x; f x ≠ 0 |] ==> isNSContc (%x. inverse (f x)) x

lemma isContc_diff:

      [| isContc f a; isContc g a |] ==> isContc (%x. f x - g x) a

lemma isContc_const:

      isContc (%x. k) a

lemma isNSContc_const:

      isNSContc (%x. k) a

### Functions from Complex to Reals

lemma isNSContCRD:

      [| isNSContCR f a; y @c= star_of a |] ==> (*f* f) y ≈ star_of (f a)

lemma isNSContCR_NSCRLIM:

      isNSContCR f a ==> f -- a --NSCR> f a

lemma NSCRLIM_isNSContCR:

      f -- a --NSCR> f a ==> isNSContCR f a

lemma isNSContCR_NSCRLIM_iff:

      isNSContCR f a = f -- a --NSCR> f a

lemma isNSContCR_CRLIM_iff:

      isNSContCR f a = f -- a --CR> f a

lemma isNSContCR_isContCR_iff:

      isNSContCR f a = isContCR f a

lemma isContCR_isNSContCR:

      isContCR f a ==> isNSContCR f a

lemma isNSContCR_isContCR:

      isNSContCR f a ==> isContCR f a

lemma isNSContCR_cmod:

      isNSContCR cmod a

lemma isContCR_cmod:

      isContCR cmod a

lemma isContc_isContCR_Re:

      isContc f a ==> isContCR (%x. Re (f x)) a

lemma isContc_isContCR_Im:

      isContc f a ==> isContCR (%x. Im (f x)) a

### Derivatives

lemma CDERIV_iff:

      CDERIV f x :> D = (%h. (f (x + h) - f x) / h) -- 0 --C> D

lemma CDERIV_NSC_iff:

      CDERIV f x :> D = (%h. (f (x + h) - f x) / h) -- 0 --NSC> D

lemma CDERIVD:

      CDERIV f x :> D ==> (%h. (f (x + h) - f x) / h) -- 0 --C> D

lemma NSC_DERIVD:

      CDERIV f x :> D ==> (%h. (f (x + h) - f x) / h) -- 0 --NSC> D

lemma CDERIV_unique:

      [| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E

lemma NSCDeriv_unique:

      [| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E

### Differentiability

lemma CDERIV_CLIM_iff:

      (%h. (f (a + h) - f a) / h) -- 0 --C> D =
      (%x. (f x - f a) / (x - a)) -- a --C> D

lemma CDERIV_iff2:

      CDERIV f x :> D = (%z. (f z - f x) / (z - x)) -- x --C> D

### Equivalence of NS and Standard Differentiation

lemma NSCDERIV_NSCLIM_iff:

      NSCDERIV f x :> D = (%h. (f (x + h) - f x) / h) -- 0 --NSC> D

lemma NSCDERIV_NSCLIM_iff2:

      NSCDERIV f x :> D = (%z. (f z - f x) / (z - x)) -- x --NSC> D

lemma NSCDERIV_iff2:

      NSCDERIV f x :> D =
      (∀xa. xa ≠ star_of x ∧ xa @c= star_of x -->
            (*f* (%z. (f z - f x) / (z - x))) xa @c= star_of D)

lemma NSCDERIV_CDERIV_iff:

      NSCDERIV f x :> D = CDERIV f x :> D

lemma NSCDERIV_isNSContc:

      NSCDERIV f x :> D ==> isNSContc f x

lemma CDERIV_isContc:

      CDERIV f x :> D ==> isContc f x

lemma NSCDERIV_const:

      NSCDERIV (%x. k) x :> 0

lemma CDERIV_const:

      CDERIV (%x. k) x :> 0

lemma NSCDERIV_add:

      [| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
      ==> NSCDERIV (%x. f x + g x) x :> Da + Db

lemma CDERIV_add:

      [| CDERIV f x :> Da; CDERIV g x :> Db |] ==> CDERIV (%x. f x + g x) x :> Da + Db

### Lemmas for Multiplication

lemma lemma_nscderiv1:

      a * b - c * d = b * (a - c) + c * (b - d)

lemma lemma_nscderiv2:

      [| (x + y) / z = star_of D + yb; z ≠ 0; z ∈ CInfinitesimal;
         yb ∈ CInfinitesimal |]
      ==> x + y @c= 0

lemma NSCDERIV_mult:

      [| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
      ==> NSCDERIV (%x. f x * g x) x :> Da * g x + Db * f x

lemma CDERIV_mult:

      [| CDERIV f x :> Da; CDERIV g x :> Db |]
      ==> CDERIV (%x. f x * g x) x :> Da * g x + Db * f x

lemma NSCDERIV_cmult:

      NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c * D

lemma CDERIV_cmult:

      CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c * D

lemma NSCDERIV_minus:

      NSCDERIV f x :> D ==> NSCDERIV (%x. - f x) x :> - D

lemma CDERIV_minus:

      CDERIV f x :> D ==> CDERIV (%x. - f x) x :> - D

lemma NSCDERIV_add_minus:

      [| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
      ==> NSCDERIV (%x. f x + - g x) x :> Da + - Db

lemma CDERIV_add_minus:

      [| CDERIV f x :> Da; CDERIV g x :> Db |]
      ==> CDERIV (%x. f x + - g x) x :> Da + - Db

lemma NSCDERIV_diff:

      [| NSCDERIV f x :> Da; NSCDERIV g x :> Db |]
      ==> NSCDERIV (%x. f x - g x) x :> Da - Db

lemma CDERIV_diff:

      [| CDERIV f x :> Da; CDERIV g x :> Db |] ==> CDERIV (%x. f x - g x) x :> Da - Db

### Chain Rule

lemma NSCDERIV_zero:

      [| NSCDERIV g x :> D; (*f* g) (star_of x + xa) = star_of (g x);
         xa ∈ CInfinitesimal; xa ≠ 0 |]
      ==> D = 0

lemma NSCDERIV_capprox:

      [| NSCDERIV f x :> D; h ∈ CInfinitesimal; h ≠ 0 |]
      ==> (*f* f) (star_of x + h) - star_of (f x) @c= 0

lemma NSCDERIVD1:

      [| NSCDERIV f g x :> Da; (*f* g) (star_of x + xa) ≠ star_of (g x);
         (*f* g) (star_of x + xa) @c= star_of (g x) |]
      ==> ((*f* f) ((*f* g) (star_of x + xa)) - star_of (f (g x))) /
          ((*f* g) (star_of x + xa) - star_of (g x)) @c=
          star_of Da

lemma NSCDERIVD2:

      [| NSCDERIV g x :> Db; xa ∈ CInfinitesimal; xa ≠ 0 |]
      ==> ((*f* g) (star_of x + xa) - star_of (g x)) / xa @c= star_of Db

lemma lemma_complex_chain:

      z ≠ 0 ==> x * y = x * inverse z * (z * y)

theorem NSCDERIV_chain:

      [| NSCDERIV f g x :> Da; NSCDERIV g x :> Db |] ==> NSCDERIV (f o g) x :> Da * Db

lemma CDERIV_chain:

      [| CDERIV f g x :> Da; CDERIV g x :> Db |] ==> CDERIV (f o g) x :> Da * Db

lemma CDERIV_chain2:

      [| CDERIV f g x :> Da; CDERIV g x :> Db |] ==> CDERIV (%x. f (g x)) x :> Da * Db

### Differentiation of Natural Number Powers

lemma NSCDERIV_Id:

      NSCDERIV (%x. x) x :> 1

lemma CDERIV_Id:

      CDERIV (%x. x) x :> 1

lemmas isContc_Id:

      isContc (%x. x) x

lemmas isContc_Id:

      isContc (%x. x) x

lemma CDERIV_cmult_Id:

      CDERIV op * c x :> c

lemma NSCDERIV_cmult_Id:

      NSCDERIV op * c x :> c

lemma CDERIV_pow:

      CDERIV (%x. x ^ n) x :> complex_of_real (real n) * x ^ (n - Suc 0)

lemma NSCDERIV_pow:

      NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * x ^ (n - 1)

lemma lemma_CDERIV_subst:

      [| CDERIV f x :> D; D = E |] ==> CDERIV f x :> E

lemma CInfinitesimal_add_not_zero:

      [| h ∈ CInfinitesimal; x ≠ 0 |] ==> star_of x + h ≠ 0

lemma NSCDERIV_inverse:

      x ≠ 0 ==> NSCDERIV inverse x :> - (inverse x)²

lemma CDERIV_inverse:

      x ≠ 0 ==> CDERIV inverse x :> - (inverse x)²

### Derivative of Reciprocals (Function @{term inverse})

lemma CDERIV_inverse_fun:

      [| CDERIV f x :> d; f x ≠ 0 |]
      ==> CDERIV (%x. inverse (f x)) x :> - (d * inverse ((f x)²))

lemma NSCDERIV_inverse_fun:

      [| NSCDERIV f x :> d; f x ≠ 0 |]
      ==> NSCDERIV (%x. inverse (f x)) x :> - (d * inverse ((f x)²))

### Derivative of Quotient

lemma CDERIV_quotient:

      [| CDERIV f x :> d; CDERIV g x :> e; g x ≠ 0 |]
      ==> CDERIV (%y. f y / g y) x :> (d * g x - e * f x) / (g x)²

lemma NSCDERIV_quotient:

      [| NSCDERIV f x :> d; NSCDERIV g x :> e; g x ≠ 0 |]
      ==> NSCDERIV (%y. f y / g y) x :> (d * g x - e * f x) / (g x)²

### Caratheodory Formulation of Derivative at a Point: Standard Proof

lemma CLIM_equal:

      ∀x. x ≠ a --> f x = g x ==> f -- a --C> l = g -- a --C> l

lemma CLIM_trans:

      [| (%x. f x + - g x) -- a --C> 0; g -- a --C> l |] ==> f -- a --C> l

lemma CARAT_CDERIV:

      CDERIV f x :> l = (∃g. (∀z. f z - f x = g z * (z - x)) ∧ isContc g x ∧ g x = l)

lemma CARAT_NSCDERIV:

      NSCDERIV f x :> l
      ==> ∃g. (∀z. f z - f x = g z * (z - x)) ∧ isNSContc g x ∧ g x = l

lemma CARAT_CDERIVD:

      (∀z. f z - f x = g z * (z - x)) ∧ isNSContc g x ∧ g x = l ==> NSCDERIV f x :> l