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