# HG changeset patch # User paulson # Date 1077360219 -3600 # Node ID 534de3572a65aa06a36059a3b554ccc033b749f6 # Parent 4952c5a92e04eb99f8810892552cfa11c31d814d conversion of Complex/CLim to Isar script diff -r 4952c5a92e04 -r 534de3572a65 src/HOL/Complex/CLim.ML --- a/src/HOL/Complex/CLim.ML Sat Feb 21 08:43:08 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,1196 +0,0 @@ -(* Title : CLim.ML - Author : Jacques D. Fleuriot - Copyright : 2001 University of Edinburgh - Description : A first theory of limits, continuity and - differentiation for complex functions -*) - -(*FIXME: MOVE these two to Complex.thy*) -Goal "(x + - a = (0::complex)) = (x=a)"; -by (simp_tac (simpset() addsimps [diff_eq_eq,symmetric complex_diff_def]) 1); -qed "complex_add_minus_iff"; -Addsimps [complex_add_minus_iff]; - -Goal "(x+y = (0::complex)) = (y = -x)"; -by Auto_tac; -by (dtac (sym RS (diff_eq_eq RS iffD2)) 1); -by Auto_tac; -qed "complex_add_eq_0_iff"; -AddIffs [complex_add_eq_0_iff]; - - -(*-----------------------------------------------------------------------*) -(* Limit of complex to complex function *) -(*-----------------------------------------------------------------------*) - -Goalw [NSCLIM_def,NSCRLIM_def] - "f -- a --NSC> L ==> (%x. Re(f x)) -- a --NSCR> Re(L)"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC_approx_Re_Im_iff, - hRe_hcomplex_of_complex])); -qed "NSCLIM_NSCRLIM_Re"; - -Goalw [NSCLIM_def,NSCRLIM_def] - "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC_approx_Re_Im_iff, - hIm_hcomplex_of_complex])); -qed "NSCLIM_NSCRLIM_Im"; - -Goalw [CLIM_def,NSCLIM_def,capprox_def] - "f -- x --C> L ==> f -- x --NSC> L"; -by Auto_tac; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_def, - starfunC,hcomplex_diff,CInfinitesimal_hcmod_iff,hcmod, - Infinitesimal_FreeUltrafilterNat_iff])); -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); -by (Step_tac 1); -by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac); -by (dres_inst_tac [("x","s")] spec 1 THEN Auto_tac); -by (Ultra_tac 1); -by (dtac sym 1 THEN Auto_tac); -qed "CLIM_NSCLIM"; - -Goal "(ALL t. P t) = (ALL X. P (Abs_hcomplex(hcomplexrel `` {X})))"; -by Auto_tac; -by (res_inst_tac [("z","t")] eq_Abs_hcomplex 1); -by Auto_tac; -qed "eq_Abs_hcomplex_ALL"; - -Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ -\ cmod (xa - x) < s & r <= cmod (f xa - L)) \ -\ ==> ALL (n::nat). EX xa. xa ~= x & \ -\ cmod(xa - x) < inverse(real(Suc n)) & r <= cmod(f xa - L)"; -by (Clarify_tac 1); -by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); -by Auto_tac; -val lemma_CLIM = result(); - -(* not needed? *) -Goal "ALL x z. EX y. Q x z y ==> EX f. ALL x z. Q x z (f x z)"; -by (rtac choice 1 THEN Step_tac 1); -by (blast_tac (claset() addIs [choice]) 1); -qed "choice2"; - -Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ -\ cmod (xa - x) < s & r <= cmod (f xa - L)) \ -\ ==> EX X. ALL (n::nat). X n ~= x & \ -\ cmod(X n - x) < inverse(real(Suc n)) & r <= cmod(f (X n) - L)"; -by (dtac lemma_CLIM 1); -by (dtac choice 1); -by (Blast_tac 1); -val lemma_skolemize_CLIM2 = result(); - -Goal "ALL n. X n ~= x & \ -\ cmod (X n - x) < inverse (real(Suc n)) & \ -\ r <= cmod (f (X n) - L) ==> \ -\ ALL n. cmod (X n - x) < inverse (real(Suc n))"; -by (Auto_tac ); -val lemma_csimp = result(); - -Goalw [CLIM_def,NSCLIM_def] - "f -- x --NSC> L ==> f -- x --C> L"; -by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL, - starfunC,CInfinitesimal_capprox_minus RS sym,hcomplex_diff, - CInfinitesimal_hcmod_iff,hcomplex_of_complex_def, - Infinitesimal_FreeUltrafilterNat_iff,hcmod])); -by (EVERY1[rtac ccontr, Asm_full_simp_tac]); -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); -by (dtac lemma_skolemize_CLIM2 1); -by (Step_tac 1); -by (dres_inst_tac [("x","X")] spec 1); -by Auto_tac; -by (dtac (lemma_csimp RS complex_seq_to_hcomplex_CInfinitesimal) 1); -by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff, - hcomplex_of_complex_def,Infinitesimal_FreeUltrafilterNat_iff, - hcomplex_diff,hcmod]) 1); -by (Blast_tac 1); -by (dres_inst_tac [("x","r")] spec 1); -by (Clarify_tac 1); -by (dtac FreeUltrafilterNat_all 1); -by (Ultra_tac 1); -by (arith_tac 1); -qed "NSCLIM_CLIM"; - -(**** First key result ****) - -Goal "(f -- x --C> L) = (f -- x --NSC> L)"; -by (blast_tac (claset() addIs [CLIM_NSCLIM,NSCLIM_CLIM]) 1); -qed "CLIM_NSCLIM_iff"; - -(*-----------------------------------------------------------------------*) -(* Limit of complex to real function *) -(*-----------------------------------------------------------------------*) - -Goalw [CRLIM_def,NSCRLIM_def,capprox_def] - "f -- x --CR> L ==> f -- x --NSCR> L"; -by Auto_tac; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [hcomplex_of_complex_def, - starfunCR,hcomplex_diff,CInfinitesimal_hcmod_iff,hcmod,hypreal_diff, - Infinitesimal_FreeUltrafilterNat_iff,Infinitesimal_approx_minus RS sym, - hypreal_of_real_def])); -by (rtac bexI 1 THEN rtac lemma_hyprel_refl 2); -by (Step_tac 1); -by (dres_inst_tac [("x","u")] spec 1 THEN Auto_tac); -by (dres_inst_tac [("x","s")] spec 1 THEN Auto_tac); -by (Ultra_tac 1); -by (dtac sym 1 THEN Auto_tac); -qed "CRLIM_NSCRLIM"; - -Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ -\ cmod (xa - x) < s & r <= abs (f xa - L)) \ -\ ==> ALL (n::nat). EX xa. xa ~= x & \ -\ cmod(xa - x) < inverse(real(Suc n)) & r <= abs (f xa - L)"; -by (Clarify_tac 1); -by (cut_inst_tac [("n1","n")] - (real_of_nat_Suc_gt_zero RS positive_imp_inverse_positive) 1); -by Auto_tac; -val lemma_CRLIM = result(); - -Goal "ALL s. 0 < s --> (EX xa. xa ~= x & \ -\ cmod (xa - x) < s & r <= abs (f xa - L)) \ -\ ==> EX X. ALL (n::nat). X n ~= x & \ -\ cmod(X n - x) < inverse(real(Suc n)) & r <= abs (f (X n) - L)"; -by (dtac lemma_CRLIM 1); -by (dtac choice 1); -by (Blast_tac 1); -val lemma_skolemize_CRLIM2 = result(); - -Goal "ALL n. X n ~= x & \ -\ cmod (X n - x) < inverse (real(Suc n)) & \ -\ r <= abs (f (X n) - L) ==> \ -\ ALL n. cmod (X n - x) < inverse (real(Suc n))"; -by (Auto_tac ); -val lemma_crsimp = result(); - -Goalw [CRLIM_def,NSCRLIM_def,capprox_def] - "f -- x --NSCR> L ==> f -- x --CR> L"; -by (auto_tac (claset(),simpset() addsimps [eq_Abs_hcomplex_ALL, - starfunCR,hcomplex_diff,hcomplex_of_complex_def,hypreal_diff, - CInfinitesimal_hcmod_iff,hcmod,Infinitesimal_approx_minus RS sym, - Infinitesimal_FreeUltrafilterNat_iff])); -by (EVERY1[rtac ccontr, Asm_full_simp_tac]); -by (asm_full_simp_tac (simpset() addsimps [linorder_not_less]) 1); -by (dtac lemma_skolemize_CRLIM2 1); -by (Step_tac 1); -by (dres_inst_tac [("x","X")] spec 1); -by Auto_tac; -by (dtac (lemma_crsimp RS complex_seq_to_hcomplex_CInfinitesimal) 1); -by (asm_full_simp_tac (simpset() addsimps [CInfinitesimal_hcmod_iff, - hcomplex_of_complex_def,Infinitesimal_FreeUltrafilterNat_iff, - hcomplex_diff,hcmod]) 1); -by (Blast_tac 1); -by (auto_tac (claset(),simpset() addsimps [hypreal_of_real_def, - hypreal_diff])); -by (dres_inst_tac [("x","r")] spec 1); -by (Clarify_tac 1); -by (dtac FreeUltrafilterNat_all 1); -by (Ultra_tac 1); -qed "NSCRLIM_CRLIM"; - -(** second key result **) -Goal "(f -- x --CR> L) = (f -- x --NSCR> L)"; -by (blast_tac (claset() addIs [CRLIM_NSCRLIM,NSCRLIM_CRLIM]) 1); -qed "CRLIM_NSCRLIM_iff"; - -(** get this result easily now **) -Goal "f -- a --C> L ==> (%x. Re(f x)) -- a --CR> Re(L)"; -by (auto_tac (claset() addDs [NSCLIM_NSCRLIM_Re],simpset() - addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff RS sym])); -qed "CLIM_CRLIM_Re"; - -Goal "f -- a --C> L ==> (%x. Im(f x)) -- a --CR> Im(L)"; -by (auto_tac (claset() addDs [NSCLIM_NSCRLIM_Im],simpset() - addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff RS sym])); -qed "CLIM_CRLIM_Im"; - -Goal "f -- a --C> L ==> (%x. cnj (f x)) -- a --C> cnj L"; -by (auto_tac (claset(),simpset() addsimps [CLIM_def, - complex_cnj_diff RS sym])); -qed "CLIM_cnj"; - -Goal "((%x. cnj (f x)) -- a --C> cnj L) = (f -- a --C> L)"; -by (auto_tac (claset(),simpset() addsimps [CLIM_def, - complex_cnj_diff RS sym])); -qed "CLIM_cnj_iff"; - -(*** NSLIM_add hence CLIM_add *) - -Goalw [NSCLIM_def] - "[| f -- x --NSC> l; g -- x --NSC> m |] \ -\ ==> (%x. f(x) + g(x)) -- x --NSC> (l + m)"; -by (auto_tac (claset() addSIs [capprox_add], simpset())); -qed "NSCLIM_add"; - -Goal "[| f -- x --C> l; g -- x --C> m |] \ -\ ==> (%x. f(x) + g(x)) -- x --C> (l + m)"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_add]) 1); -qed "CLIM_add"; - -(*** NSLIM_mult hence CLIM_mult *) - -Goalw [NSCLIM_def] - "[| f -- x --NSC> l; g -- x --NSC> m |] \ -\ ==> (%x. f(x) * g(x)) -- x --NSC> (l * m)"; -by (auto_tac (claset() addSIs [capprox_mult_CFinite], simpset())); -qed "NSCLIM_mult"; - -Goal "[| f -- x --C> l; g -- x --C> m |] \ -\ ==> (%x. f(x) * g(x)) -- x --C> (l * m)"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_mult]) 1); -qed "CLIM_mult"; - -(*** NSCLIM_const and CLIM_const ***) - -Goalw [NSCLIM_def] "(%x. k) -- x --NSC> k"; -by Auto_tac; -qed "NSCLIM_const"; -Addsimps [NSCLIM_const]; - -Goalw [CLIM_def] "(%x. k) -- x --C> k"; -by Auto_tac; -qed "CLIM_const"; -Addsimps [CLIM_const]; - -(*** NSCLIM_minus and CLIM_minus ***) - -Goalw [NSCLIM_def] - "f -- a --NSC> L ==> (%x. -f(x)) -- a --NSC> -L"; -by Auto_tac; -qed "NSCLIM_minus"; - -Goal "f -- a --C> L ==> (%x. -f(x)) -- a --C> -L"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_minus]) 1); -qed "CLIM_minus"; - -(*** NSCLIM_diff hence CLIM_diff ***) - -Goalw [complex_diff_def] - "[| f -- x --NSC> l; g -- x --NSC> m |] \ -\ ==> (%x. f(x) - g(x)) -- x --NSC> (l - m)"; -by (auto_tac (claset(), simpset() addsimps [NSCLIM_add,NSCLIM_minus])); -qed "NSCLIM_diff"; - -Goal "[| f -- x --C> l; g -- x --C> m |] \ -\ ==> (%x. f(x) - g(x)) -- x --C> (l - m)"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_diff]) 1); -qed "CLIM_diff"; - -(*** NSCLIM_inverse and hence CLIM_inverse *) - -Goalw [NSCLIM_def] - "[| f -- a --NSC> L; L ~= 0 |] \ -\ ==> (%x. inverse(f(x))) -- a --NSC> (inverse L)"; -by (Clarify_tac 1); -by (dtac spec 1); -by (auto_tac (claset(), - simpset() addsimps [hcomplex_of_complex_capprox_inverse])); -qed "NSCLIM_inverse"; - -Goal "[| f -- a --C> L; L ~= 0 |] \ -\ ==> (%x. inverse(f(x))) -- a --C> (inverse L)"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_inverse]) 1); -qed "CLIM_inverse"; - -(*** NSCLIM_zero, CLIM_zero, etc. ***) - -Goal "f -- a --NSC> l ==> (%x. f(x) - l) -- a --NSC> 0"; -by (res_inst_tac [("a1","l")] (right_minus RS subst) 1); -by (rewtac complex_diff_def); -by (rtac NSCLIM_add 1 THEN Auto_tac); -qed "NSCLIM_zero"; - -Goal "f -- a --C> l ==> (%x. f(x) - l) -- a --C> 0"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_zero]) 1); -qed "CLIM_zero"; - -Goal "(%x. f(x) - l) -- x --NSC> 0 ==> f -- x --NSC> l"; -by (dres_inst_tac [("g","%x. l"),("m","l")] NSCLIM_add 1); -by Auto_tac; -qed "NSCLIM_zero_cancel"; - -Goal "(%x. f(x) - l) -- x --C> 0 ==> f -- x --C> l"; -by (dres_inst_tac [("g","%x. l"),("m","l")] CLIM_add 1); -by Auto_tac; -qed "CLIM_zero_cancel"; - -(*** NSCLIM_not zero and hence CLIM_not_zero ***) - -(*not in simpset?*) -Addsimps [hypreal_epsilon_not_zero]; - -Goalw [NSCLIM_def] "k ~= 0 ==> ~ ((%x. k) -- x --NSC> 0)"; -by (auto_tac (claset(),simpset() delsimps [hcomplex_of_complex_zero])); -by (res_inst_tac [("x","hcomplex_of_complex x + hcomplex_of_hypreal epsilon")] exI 1); -by (auto_tac (claset() addIs [CInfinitesimal_add_capprox_self RS capprox_sym],simpset() - delsimps [hcomplex_of_complex_zero])); -qed "NSCLIM_not_zero"; - -(* [| k ~= 0; (%x. k) -- x --NSC> 0 |] ==> R *) -bind_thm("NSCLIM_not_zeroE", NSCLIM_not_zero RS notE); - -Goal "k ~= 0 ==> ~ ((%x. k) -- x --C> 0)"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_not_zero]) 1); -qed "CLIM_not_zero"; - -(*** NSCLIM_const hence CLIM_const ***) - -Goal "(%x. k) -- x --NSC> L ==> k = L"; -by (rtac ccontr 1); -by (dtac NSCLIM_zero 1); -by (rtac NSCLIM_not_zeroE 1 THEN assume_tac 2); -by Auto_tac; -qed "NSCLIM_const_eq"; - -Goal "(%x. k) -- x --C> L ==> k = L"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff,NSCLIM_const_eq]) 1); -qed "CLIM_const_eq"; - -(*** NSCLIM and hence CLIM are unique ***) - -Goal "[| f -- x --NSC> L; f -- x --NSC> M |] ==> L = M"; -by (dtac NSCLIM_minus 1); -by (dtac NSCLIM_add 1 THEN assume_tac 1); -by (auto_tac (claset() addSDs [NSCLIM_const_eq RS sym], simpset())); -qed "NSCLIM_unique"; - -Goal "[| f -- x --C> L; f -- x --C> M |] ==> L = M"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_unique]) 1); -qed "CLIM_unique"; - -(*** NSCLIM_mult_zero and CLIM_mult_zero ***) - -Goal "[| f -- x --NSC> 0; g -- x --NSC> 0 |] \ -\ ==> (%x. f(x)*g(x)) -- x --NSC> 0"; -by (dtac NSCLIM_mult 1 THEN Auto_tac); -qed "NSCLIM_mult_zero"; - -Goal "[| f -- x --C> 0; g -- x --C> 0 |] \ -\ ==> (%x. f(x)*g(x)) -- x --C> 0"; -by (dtac CLIM_mult 1 THEN Auto_tac); -qed "CLIM_mult_zero"; - -(*** NSCLIM_self hence CLIM_self ***) - -Goalw [NSCLIM_def] "(%x. x) -- a --NSC> a"; -by (auto_tac (claset() addIs [starfunC_Idfun_capprox],simpset())); -qed "NSCLIM_self"; - -Goal "(%x. x) -- a --C> a"; -by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff,NSCLIM_self]) 1); -qed "CLIM_self"; - -(** another equivalence result **) -Goalw [NSCLIM_def,NSCRLIM_def] - "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"; -by (auto_tac (claset(),simpset() addsimps [CInfinitesimal_capprox_minus - RS sym,CInfinitesimal_hcmod_iff])); -by (ALLGOALS(dtac spec) THEN Auto_tac); -by (ALLGOALS(res_inst_tac [("z","xa")] eq_Abs_hcomplex)); -by (auto_tac (claset(),simpset() addsimps [hcomplex_diff, - starfunC,starfunCR,hcomplex_of_complex_def,hcmod,mem_infmal_iff])); -qed "NSCLIM_NSCRLIM_iff"; - -(** much, much easier standard proof **) -Goalw [CLIM_def,CRLIM_def] - "(f -- x --C> L) = ((%y. cmod(f y - L)) -- x --CR> 0)"; -by Auto_tac; -qed "CLIM_CRLIM_iff"; - -(* so this is nicer nonstandard proof *) -Goal "(f -- x --NSC> L) = ((%y. cmod(f y - L)) -- x --NSCR> 0)"; -by (auto_tac (claset(),simpset() addsimps [CRLIM_NSCRLIM_iff RS sym, - CLIM_CRLIM_iff,CLIM_NSCLIM_iff RS sym])); -qed "NSCLIM_NSCRLIM_iff2"; - -Goal "(f -- a --NSC> L) = ((%x. Re(f x)) -- a --NSCR> Re(L) & \ -\ (%x. Im(f x)) -- a --NSCR> Im(L))"; -by (auto_tac (claset() addIs [NSCLIM_NSCRLIM_Re,NSCLIM_NSCRLIM_Im],simpset())); -by (auto_tac (claset(),simpset() addsimps [NSCLIM_def,NSCRLIM_def])); -by (REPEAT(dtac spec 1) THEN Auto_tac); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [capprox_approx_iff,starfunC, - hcomplex_of_complex_def,starfunCR,hypreal_of_real_def])); -qed "NSCLIM_NSCRLIM_Re_Im_iff"; - -Goal "(f -- a --C> L) = ((%x. Re(f x)) -- a --CR> Re(L) & \ -\ (%x. Im(f x)) -- a --CR> Im(L))"; -by (auto_tac (claset(),simpset() addsimps [CLIM_NSCLIM_iff,CRLIM_NSCRLIM_iff, - NSCLIM_NSCRLIM_Re_Im_iff])); -qed "CLIM_CRLIM_Re_Im_iff"; - - -(*-----------------------------------------------------------------------*) -(* Continuity *) -(*-----------------------------------------------------------------------*) - -Goalw [isNSContc_def] - "[| isNSContc f a; y @c= hcomplex_of_complex a |] \ -\ ==> ( *fc* f) y @c= hcomplex_of_complex (f a)"; -by (Blast_tac 1); -qed "isNSContcD"; - -Goalw [isNSContc_def,NSCLIM_def] - "isNSContc f a ==> f -- a --NSC> (f a) "; -by (Blast_tac 1); -qed "isNSContc_NSCLIM"; - -Goalw [isNSContc_def,NSCLIM_def] - "f -- a --NSC> (f a) ==> isNSContc f a"; -by Auto_tac; -by (res_inst_tac [("Q","y = hcomplex_of_complex a")] - (excluded_middle RS disjE) 1); -by Auto_tac; -qed "NSCLIM_isNSContc"; - -(*--------------------------------------------------*) -(* NS continuity can be defined using NS Limit in *) -(* similar fashion to standard def of continuity *) -(* -------------------------------------------------*) - -Goal "(isNSContc f a) = (f -- a --NSC> (f a))"; -by (blast_tac (claset() addIs [isNSContc_NSCLIM,NSCLIM_isNSContc]) 1); -qed "isNSContc_NSCLIM_iff"; - -Goal "(isNSContc f a) = (f -- a --C> (f a))"; -by (asm_full_simp_tac (simpset() addsimps - [CLIM_NSCLIM_iff,isNSContc_NSCLIM_iff]) 1); -qed "isNSContc_CLIM_iff"; - -(*** key result for continuity ***) -Goalw [isContc_def] "(isNSContc f a) = (isContc f a)"; -by (rtac isNSContc_CLIM_iff 1); -qed "isNSContc_isContc_iff"; - -Goal "isContc f a ==> isNSContc f a"; -by (etac (isNSContc_isContc_iff RS iffD2) 1); -qed "isContc_isNSContc"; - -Goal "isNSContc f a ==> isContc f a"; -by (etac (isNSContc_isContc_iff RS iffD1) 1); -qed "isNSContc_isContc"; - -(*--------------------------------------------------*) -(* Alternative definition of continuity *) -(* -------------------------------------------------*) - -Goalw [NSCLIM_def] - "(f -- a --NSC> L) = ((%h. f(a + h)) -- 0 --NSC> L)"; -by Auto_tac; -by (dres_inst_tac [("x","hcomplex_of_complex a + x")] spec 1); -by (dres_inst_tac [("x","- hcomplex_of_complex a + x")] spec 2); -by Safe_tac; -by (Asm_full_simp_tac 1); -by (rtac ((mem_cinfmal_iff RS iffD2) RS - (CInfinitesimal_add_capprox_self RS capprox_sym)) 1); -by (rtac (capprox_minus_iff2 RS iffD1) 4); -by (asm_full_simp_tac (simpset() addsimps compare_rls@[hcomplex_add_commute]) 3); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 4); -by (auto_tac (claset(), - simpset() addsimps [starfunC, hcomplex_of_complex_def, - hcomplex_minus, hcomplex_add])); -qed "NSCLIM_h_iff"; - -Goal "(f -- a --NSC> f a) = ((%h. f(a + h)) -- 0 --NSC> f a)"; -by (rtac NSCLIM_h_iff 1); -qed "NSCLIM_isContc_iff"; - -Goal "(f -- a --C> f a) = ((%h. f(a + h)) -- 0 --C> f(a))"; -by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff, NSCLIM_isContc_iff]) 1); -qed "CLIM_isContc_iff"; - -Goalw [isContc_def] "(isContc f x) = ((%h. f(x + h)) -- 0 --C> f(x))"; -by (simp_tac (simpset() addsimps [CLIM_isContc_iff]) 1); -qed "isContc_iff"; - -Goal "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) + g(x)) a"; -by (auto_tac (claset() addIs [capprox_add], - simpset() addsimps [isNSContc_isContc_iff RS sym, isNSContc_def])); -qed "isContc_add"; - -Goal "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) * g(x)) a"; -by (auto_tac (claset() addSIs [starfunC_mult_CFinite_capprox], - simpset() delsimps [starfunC_mult RS sym] - addsimps [isNSContc_isContc_iff RS sym, isNSContc_def])); -qed "isContc_mult"; - -(*** more theorems: note simple proofs ***) - -Goal "[| isContc f a; isContc g (f a) |] \ -\ ==> isContc (g o f) a"; -by (auto_tac (claset(),simpset() addsimps [isNSContc_isContc_iff RS sym, - isNSContc_def,starfunC_o RS sym])); -qed "isContc_o"; - -Goal "[| isContc f a; isContc g (f a) |] \ -\ ==> isContc (%x. g (f x)) a"; -by (auto_tac (claset() addDs [isContc_o],simpset() addsimps [o_def])); -qed "isContc_o2"; - -Goalw [isNSContc_def] "isNSContc f a ==> isNSContc (%x. - f x) a"; -by Auto_tac; -qed "isNSContc_minus"; - -Goal "isContc f a ==> isContc (%x. - f x) a"; -by (auto_tac (claset(),simpset() addsimps [isNSContc_isContc_iff RS sym, - isNSContc_minus])); -qed "isContc_minus"; - -Goalw [isContc_def] - "[| isContc f x; f x ~= 0 |] ==> isContc (%x. inverse (f x)) x"; -by (blast_tac (claset() addIs [CLIM_inverse]) 1); -qed "isContc_inverse"; - -Goal "[| isNSContc f x; f x ~= 0 |] ==> isNSContc (%x. inverse (f x)) x"; -by (auto_tac (claset() addIs [isContc_inverse],simpset() addsimps - [isNSContc_isContc_iff])); -qed "isNSContc_inverse"; - -Goalw [complex_diff_def] - "[| isContc f a; isContc g a |] ==> isContc (%x. f(x) - g(x)) a"; -by (auto_tac (claset() addIs [isContc_add,isContc_minus],simpset())); -qed "isContc_diff"; - -Goalw [isContc_def] "isContc (%x. k) a"; -by (Simp_tac 1); -qed "isContc_const"; -Addsimps [isContc_const]; - -Goalw [isNSContc_def] "isNSContc (%x. k) a"; -by (Simp_tac 1); -qed "isNSContc_const"; -Addsimps [isNSContc_const]; - - -(*-----------------------------------------------------------------------*) -(* functions from complex to reals *) -(* ----------------------------------------------------------------------*) - -Goalw [isNSContCR_def] - "[| isNSContCR f a; y @c= hcomplex_of_complex a |] \ -\ ==> ( *fcR* f) y @= hypreal_of_real (f a)"; -by (Blast_tac 1); -qed "isNSContCRD"; - -Goalw [isNSContCR_def,NSCRLIM_def] - "isNSContCR f a ==> f -- a --NSCR> (f a) "; -by (Blast_tac 1); -qed "isNSContCR_NSCRLIM"; - -Goalw [isNSContCR_def,NSCRLIM_def] - "f -- a --NSCR> (f a) ==> isNSContCR f a"; -by Auto_tac; -by (res_inst_tac [("Q","y = hcomplex_of_complex a")] - (excluded_middle RS disjE) 1); -by Auto_tac; -qed "NSCRLIM_isNSContCR"; - -Goal "(isNSContCR f a) = (f -- a --NSCR> (f a))"; -by (blast_tac (claset() addIs [isNSContCR_NSCRLIM,NSCRLIM_isNSContCR]) 1); -qed "isNSContCR_NSCRLIM_iff"; - -Goal "(isNSContCR f a) = (f -- a --CR> (f a))"; -by (asm_full_simp_tac (simpset() addsimps - [CRLIM_NSCRLIM_iff,isNSContCR_NSCRLIM_iff]) 1); -qed "isNSContCR_CRLIM_iff"; - -(*** another key result for continuity ***) -Goalw [isContCR_def] "(isNSContCR f a) = (isContCR f a)"; -by (rtac isNSContCR_CRLIM_iff 1); -qed "isNSContCR_isContCR_iff"; - -Goal "isContCR f a ==> isNSContCR f a"; -by (etac (isNSContCR_isContCR_iff RS iffD2) 1); -qed "isContCR_isNSContCR"; - -Goal "isNSContCR f a ==> isContCR f a"; -by (etac (isNSContCR_isContCR_iff RS iffD1) 1); -qed "isNSContCR_isContCR"; - -Goalw [isNSContCR_def] "isNSContCR cmod (a)"; -by (auto_tac (claset() addIs [capprox_hcmod_approx], - simpset() addsimps [starfunCR_cmod,hcmod_hcomplex_of_complex - RS sym])); -qed "isNSContCR_cmod"; -Addsimps [isNSContCR_cmod]; - -Goal "isContCR cmod (a)"; -by (auto_tac (claset(),simpset() addsimps [isNSContCR_isContCR_iff RS sym])); -qed "isContCR_cmod"; -Addsimps [isContCR_cmod]; - -Goalw [isContc_def,isContCR_def] - "isContc f a ==> isContCR (%x. Re (f x)) a"; -by (etac CLIM_CRLIM_Re 1); -qed "isContc_isContCR_Re"; - -Goalw [isContc_def,isContCR_def] - "isContc f a ==> isContCR (%x. Im (f x)) a"; -by (etac CLIM_CRLIM_Im 1); -qed "isContc_isContCR_Im"; - -(*-----------------------------------------------------------------------*) -(* Derivatives *) -(*-----------------------------------------------------------------------*) - -Goalw [cderiv_def] - "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"; -by (Blast_tac 1); -qed "CDERIV_iff"; - -Goalw [cderiv_def] - "(CDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"; -by (simp_tac (simpset() addsimps [CLIM_NSCLIM_iff]) 1); -qed "CDERIV_NSC_iff"; - -Goalw [cderiv_def] - "CDERIV f x :> D \ -\ ==> (%h. (f(x + h) - f(x))/h) -- 0 --C> D"; -by (Blast_tac 1); -qed "CDERIVD"; - -Goalw [cderiv_def] - "CDERIV f x :> D ==> (%h. (f(x + h) - f(x))/h) -- 0 --NSC> D"; -by (asm_full_simp_tac (simpset() addsimps [CLIM_NSCLIM_iff]) 1); -qed "NSC_DERIVD"; - -(*** Uniqueness ***) - -Goalw [cderiv_def] - "[| CDERIV f x :> D; CDERIV f x :> E |] ==> D = E"; -by (blast_tac (claset() addIs [CLIM_unique]) 1); -qed "CDERIV_unique"; - -(*** uniqueness: a nonstandard proof ***) -Goalw [nscderiv_def] - "[| NSCDERIV f x :> D; NSCDERIV f x :> E |] ==> D = E"; -by (auto_tac (claset() addSDs [inst "x" "hcomplex_of_hypreal epsilon" bspec] - addSIs [inj_hcomplex_of_complex RS injD] - addDs [capprox_trans3], - simpset())); -qed "NSCDeriv_unique"; - - -(*-----------------------------------------------------------------------*) -(* Differentiability *) -(*-----------------------------------------------------------------------*) - -Goalw [cdifferentiable_def] - "f cdifferentiable x ==> EX D. CDERIV f x :> D"; -by (assume_tac 1); -qed "cdifferentiableD"; - -Goalw [cdifferentiable_def] - "CDERIV f x :> D ==> f cdifferentiable x"; -by (Blast_tac 1); -qed "cdifferentiableI"; - -Goalw [NSCdifferentiable_def] - "f NSCdifferentiable x ==> EX D. NSCDERIV f x :> D"; -by (assume_tac 1); -qed "NSCdifferentiableD"; - -Goalw [NSCdifferentiable_def] - "NSCDERIV f x :> D ==> f NSCdifferentiable x"; -by (Blast_tac 1); -qed "NSCdifferentiableI"; - - -(*-----------------------------------------------------------------------*) -(* Alternative definition for differentiability *) -(*-----------------------------------------------------------------------*) - -Goalw [CLIM_def] - "((%h. (f(a + h) - f(a))/h) -- 0 --C> D) = \ -\ ((%x. (f(x) - f(a)) / (x - a)) -- a --C> D)"; -by (Step_tac 1); -by (ALLGOALS(dtac spec)); -by (Step_tac 1); -by (Blast_tac 1 THEN Blast_tac 2); -by (ALLGOALS(res_inst_tac [("x","s")] exI)); -by (Step_tac 1); -by (dres_inst_tac [("x","x - a")] spec 1); -by (dres_inst_tac [("x","x + a")] spec 2); -by (auto_tac (claset(), simpset() addsimps add_ac)); -qed "CDERIV_CLIM_iff"; - -Goalw [cderiv_def] "(CDERIV f x :> D) = \ -\ ((%z. (f(z) - f(x)) / (z - x)) -- x --C> D)"; -by (simp_tac (simpset() addsimps [CDERIV_CLIM_iff]) 1); -qed "CDERIV_iff2"; - - -(*-----------------------------------------------------------------------*) -(* Equivalence of NS and standard defs of differentiation *) -(*-----------------------------------------------------------------------*) - -(*** first equivalence ***) -Goalw [nscderiv_def,NSCLIM_def] - "(NSCDERIV f x :> D) = ((%h. (f(x + h) - f(x))/h) -- 0 --NSC> D)"; -by Auto_tac; -by (dres_inst_tac [("x","xa")] bspec 1); -by (rtac ccontr 3); -by (dres_inst_tac [("x","h")] spec 3); -by (auto_tac (claset(), - simpset() addsimps [mem_cinfmal_iff, starfunC_lambda_cancel])); -qed "NSCDERIV_NSCLIM_iff"; - -(*** 2nd equivalence ***) -Goal "(NSCDERIV f x :> D) = \ -\ ((%z. (f(z) - f(x)) / (z - x)) -- x --NSC> D)"; -by (full_simp_tac (simpset() addsimps - [NSCDERIV_NSCLIM_iff, CDERIV_CLIM_iff, CLIM_NSCLIM_iff RS sym]) 1); -qed "NSCDERIV_NSCLIM_iff2"; - -Goal "(NSCDERIV f x :> D) = \ -\ (ALL xa. xa ~= hcomplex_of_complex x & xa @c= hcomplex_of_complex x --> \ -\ ( *fc* (%z. (f z - f x) / (z - x))) xa @c= hcomplex_of_complex D)"; -by (auto_tac (claset(), simpset() addsimps [NSCDERIV_NSCLIM_iff2, NSCLIM_def])); -qed "NSCDERIV_iff2"; - -Goalw [cderiv_def] "(NSCDERIV f x :> D) = (CDERIV f x :> D)"; -by (simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,CLIM_NSCLIM_iff]) 1); -qed "NSCDERIV_CDERIV_iff"; - -Goalw [nscderiv_def] - "NSCDERIV f x :> D ==> isNSContc f x"; -by (auto_tac (claset(),simpset() addsimps [isNSContc_NSCLIM_iff, - NSCLIM_def,hcomplex_diff_def])); -by (dtac (capprox_minus_iff RS iffD1) 1); -by (subgoal_tac "xa + - (hcomplex_of_complex x) ~= 0" 1); - by (asm_full_simp_tac (simpset() addsimps compare_rls) 2); -by (dres_inst_tac [("x","- hcomplex_of_complex x + xa")] bspec 1); -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_assoc RS sym]) 2); -by (auto_tac (claset(),simpset() addsimps - [mem_cinfmal_iff RS sym,hcomplex_add_commute])); -by (dres_inst_tac [("c","xa + - hcomplex_of_complex x")] capprox_mult1 1); -by (auto_tac (claset() addIs [CInfinitesimal_subset_CFinite - RS subsetD],simpset() addsimps [mult_assoc])); -by (dres_inst_tac [("x3","D")] (CFinite_hcomplex_of_complex RSN - (2,CInfinitesimal_CFinite_mult) RS (mem_cinfmal_iff RS iffD1)) 1); -by (blast_tac (claset() addIs [capprox_trans,mult_commute RS subst, - (capprox_minus_iff RS iffD2)]) 1); -qed "NSCDERIV_isNSContc"; - -Goal "CDERIV f x :> D ==> isContc f x"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym, - isNSContc_isContc_iff RS sym,NSCDERIV_isNSContc]) 1); -qed "CDERIV_isContc"; - -(*-----------------------------------------------------------------------*) -(* Differentiation rules for combinations of functions follow from clear, *) -(* straightforard, algebraic manipulations *) -(*-----------------------------------------------------------------------*) - -(* use simple constant nslimit theorem *) -Goal "(NSCDERIV (%x. k) x :> 0)"; -by (simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff]) 1); -qed "NSCDERIV_const"; -Addsimps [NSCDERIV_const]; - -Goal "(CDERIV (%x. k) x :> 0)"; -by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1); -qed "CDERIV_const"; -Addsimps [CDERIV_const]; - -Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ -\ ==> NSCDERIV (%x. f x + g x) x :> Da + Db"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, - NSCLIM_def]) 1 THEN REPEAT(Step_tac 1)); -by (auto_tac (claset(), - simpset() addsimps [hcomplex_add_divide_distrib,hcomplex_diff_def])); -by (dres_inst_tac [("b","hcomplex_of_complex Da"), - ("d","hcomplex_of_complex Db")] capprox_add 1); -by (auto_tac (claset(), simpset() addsimps add_ac)); -qed "NSCDERIV_add"; - -Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (%x. f x + g x) x :> Da + Db"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_add, - NSCDERIV_CDERIV_iff RS sym]) 1); -qed "CDERIV_add"; - -(*** lemmas for multiplication ***) - -Goal "((a::hcomplex)*b) - (c*d) = (b*(a - c)) + (c*(b - d))"; -by (simp_tac (simpset() addsimps [right_diff_distrib]) 1); -val lemma_nscderiv1 = result(); - -Goal "[| (x + y) / z = hcomplex_of_complex D + yb; z ~= 0; \ -\ z : CInfinitesimal; yb : CInfinitesimal |] \ -\ ==> x + y @c= 0"; -by (forw_inst_tac [("c1","z")] (hcomplex_mult_right_cancel RS iffD2) 1 - THEN assume_tac 1); -by (thin_tac "(x + y) / z = hcomplex_of_complex D + yb" 1); -by (auto_tac (claset() addSIs [CInfinitesimal_CFinite_mult2, CFinite_add], - simpset() addsimps [mem_cinfmal_iff RS sym])); -by (etac (CInfinitesimal_subset_CFinite RS subsetD) 1); -val lemma_nscderiv2 = result(); - -Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ -\ ==> NSCDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def]) 1 - THEN REPEAT(Step_tac 1)); -by (auto_tac (claset(), - simpset() addsimps [starfunC_lambda_cancel, lemma_nscderiv1, - hcomplex_of_complex_zero])); -by (simp_tac (simpset() addsimps [hcomplex_add_divide_distrib]) 1); -by (REPEAT(dtac (bex_CInfinitesimal_iff2 RS iffD2) 1)); -by (auto_tac (claset(), - simpset() delsimps [times_divide_eq_right] - addsimps [times_divide_eq_right RS sym])); -by (rewtac hcomplex_diff_def); -by (dres_inst_tac [("D","Db")] lemma_nscderiv2 1); -by (dtac (capprox_minus_iff RS iffD2 RS (bex_CInfinitesimal_iff2 RS iffD2)) 4); -by (auto_tac (claset() addSIs [capprox_add_mono1], - simpset() addsimps [left_distrib, right_distrib, mult_commute, add_assoc])); -by (res_inst_tac [("b1","hcomplex_of_complex Db * hcomplex_of_complex (f x)")] - (add_commute RS subst) 1); -by (auto_tac (claset() addSIs [CInfinitesimal_add_capprox_self2 RS capprox_sym, - CInfinitesimal_add, CInfinitesimal_mult, - CInfinitesimal_hcomplex_of_complex_mult, - CInfinitesimal_hcomplex_of_complex_mult2], - simpset() addsimps [hcomplex_add_assoc RS sym])); -qed "NSCDERIV_mult"; - -Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (%x. f x * g x) x :> (Da * g(x)) + (Db * f(x))"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_mult, - NSCDERIV_CDERIV_iff RS sym]) 1); -qed "CDERIV_mult"; - -Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. c * f x) x :> c*D"; -by (asm_full_simp_tac - (simpset() addsimps [times_divide_eq_right RS sym, NSCDERIV_NSCLIM_iff, - minus_mult_right, right_distrib RS sym, - complex_diff_def] - delsimps [times_divide_eq_right, minus_mult_right RS sym]) 1); -by (etac (NSCLIM_const RS NSCLIM_mult) 1); -qed "NSCDERIV_cmult"; - -Goal "CDERIV f x :> D ==> CDERIV (%x. c * f x) x :> c*D"; -by (auto_tac (claset(),simpset() addsimps [NSCDERIV_cmult,NSCDERIV_CDERIV_iff - RS sym])); -qed "CDERIV_cmult"; - -Goal "NSCDERIV f x :> D ==> NSCDERIV (%x. -(f x)) x :> -D"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff,complex_diff_def]) 1); -by (res_inst_tac [("t","f x")] (minus_minus RS subst) 1); -by (asm_simp_tac (simpset() addsimps [minus_add_distrib RS sym] - delsimps [minus_add_distrib, minus_minus] - -) 1); -by (etac NSCLIM_minus 1); -qed "NSCDERIV_minus"; - -Goal "CDERIV f x :> D ==> CDERIV (%x. -(f x)) x :> -D"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_minus,NSCDERIV_CDERIV_iff RS sym]) 1); -qed "CDERIV_minus"; - -Goal "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ -\ ==> NSCDERIV (%x. f x + -g x) x :> Da + -Db"; -by (blast_tac (claset() addDs [NSCDERIV_add,NSCDERIV_minus]) 1); -qed "NSCDERIV_add_minus"; - -Goal "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (%x. f x + -g x) x :> Da + -Db"; -by (blast_tac (claset() addDs [CDERIV_add,CDERIV_minus]) 1); -qed "CDERIV_add_minus"; - -Goalw [complex_diff_def] - "[| NSCDERIV f x :> Da; NSCDERIV g x :> Db |] \ -\ ==> NSCDERIV (%x. f x - g x) x :> Da - Db"; -by (blast_tac (claset() addIs [NSCDERIV_add_minus]) 1); -qed "NSCDERIV_diff"; - -Goalw [complex_diff_def] - "[| CDERIV f x :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (%x. f x - g x) x :> Da - Db"; -by (blast_tac (claset() addIs [CDERIV_add_minus]) 1); -qed "CDERIV_diff"; - - -(*--------------------------------------------------*) -(* Chain rule *) -(*--------------------------------------------------*) - -(* lemmas *) -Goalw [nscderiv_def] - "[| NSCDERIV g x :> D; \ -\ ( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex(g x);\ -\ xa : CInfinitesimal; xa ~= 0 \ -\ |] ==> D = 0"; -by (dtac bspec 1); -by Auto_tac; -qed "NSCDERIV_zero"; - -Goalw [nscderiv_def] - "[| NSCDERIV f x :> D; h: CInfinitesimal; h ~= 0 |] \ -\ ==> ( *fc* f) (hcomplex_of_complex(x) + h) - hcomplex_of_complex(f x) @c= 0"; -by (asm_full_simp_tac (simpset() addsimps [mem_cinfmal_iff RS sym]) 1); -by (rtac CInfinitesimal_ratio 1); -by (rtac capprox_hcomplex_of_complex_CFinite 3); -by Auto_tac; -qed "NSCDERIV_capprox"; - - -(*--------------------------------------------------*) -(* from one version of differentiability *) -(* *) -(* f(x) - f(a) *) -(* --------------- @= Db *) -(* x - a *) -(* -------------------------------------------------*) - -Goal "[| NSCDERIV f (g x) :> Da; \ -\ ( *fc* g) (hcomplex_of_complex(x) + xa) ~= hcomplex_of_complex (g x); \ -\ ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x) \ -\ |] ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa)) \ -\ - hcomplex_of_complex (f (g x))) \ -\ / (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) \ -\ @c= hcomplex_of_complex (Da)"; -by (auto_tac (claset(),simpset() addsimps [NSCDERIV_NSCLIM_iff2, NSCLIM_def])); -qed "NSCDERIVD1"; - -(*--------------------------------------------------*) -(* from other version of differentiability *) -(* *) -(* f(x + h) - f(x) *) -(* ----------------- @= Db *) -(* h *) -(*--------------------------------------------------*) - -Goal "[| NSCDERIV g x :> Db; xa: CInfinitesimal; xa ~= 0 |] \ -\ ==> (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex(g x)) / xa \ -\ @c= hcomplex_of_complex (Db)"; -by (auto_tac (claset(), - simpset() addsimps [NSCDERIV_NSCLIM_iff, NSCLIM_def, - mem_cinfmal_iff, starfunC_lambda_cancel])); -qed "NSCDERIVD2"; - -Goal "(z::hcomplex) ~= 0 ==> x*y = (x*inverse(z))*(z*y)"; -by Auto_tac; -qed "lemma_complex_chain"; - -(*** chain rule ***) - -Goal "[| NSCDERIV f (g x) :> Da; NSCDERIV g x :> Db |] \ -\ ==> NSCDERIV (f o g) x :> Da * Db"; -by (asm_simp_tac (simpset() addsimps [NSCDERIV_NSCLIM_iff, - NSCLIM_def,mem_cinfmal_iff RS sym]) 1 THEN Step_tac 1); -by (forw_inst_tac [("f","g")] NSCDERIV_capprox 1); -by (auto_tac (claset(), - simpset() addsimps [starfunC_lambda_cancel2, starfunC_o RS sym])); -by (case_tac "( *fc* g) (hcomplex_of_complex(x) + xa) = hcomplex_of_complex (g x)" 1); -by (dres_inst_tac [("g","g")] NSCDERIV_zero 1); -by (auto_tac (claset(),simpset() addsimps [hcomplex_divide_def])); -by (res_inst_tac [("z1","( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)"), - ("y1","inverse xa")] (lemma_complex_chain RS ssubst) 1); -by (Asm_simp_tac 1); -by (rtac capprox_mult_hcomplex_of_complex 1); -by (fold_tac [hcomplex_divide_def]); -by (blast_tac (claset() addIs [NSCDERIVD2]) 2); -by (auto_tac (claset() addSIs [NSCDERIVD1] addIs [capprox_minus_iff RS iffD2], - simpset() addsimps [symmetric hcomplex_diff_def])); -qed "NSCDERIV_chain"; - -(* standard version *) -Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (f o g) x :> Da * Db"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym, - NSCDERIV_chain]) 1); -qed "CDERIV_chain"; - -Goal "[| CDERIV f (g x) :> Da; CDERIV g x :> Db |] \ -\ ==> CDERIV (%x. f (g x)) x :> Da * Db"; -by (auto_tac (claset() addDs [CDERIV_chain], simpset() addsimps [o_def])); -qed "CDERIV_chain2"; - -(*-----------------------------------------------------------------------*) -(* Differentiation of natural number powers *) -(*-----------------------------------------------------------------------*) - -Goal "NSCDERIV (%x. x) x :> 1"; -by (auto_tac (claset(), - simpset() addsimps [NSCDERIV_NSCLIM_iff,NSCLIM_def])); -qed "NSCDERIV_Id"; -Addsimps [NSCDERIV_Id]; - -Goal "CDERIV (%x. x) x :> 1"; -by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff RS sym]) 1); -qed "CDERIV_Id"; -Addsimps [CDERIV_Id]; - -bind_thm ("isContc_Id", CDERIV_Id RS CDERIV_isContc); - -(*derivative of linear multiplication*) -Goal "CDERIV (op * c) x :> c"; -by (cut_inst_tac [("c","c"),("x","x")] (CDERIV_Id RS CDERIV_cmult) 1); -by (Asm_full_simp_tac 1); -qed "CDERIV_cmult_Id"; -Addsimps [CDERIV_cmult_Id]; - -Goal "NSCDERIV (op * c) x :> c"; -by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1); -qed "NSCDERIV_cmult_Id"; -Addsimps [NSCDERIV_cmult_Id]; - -Goal "CDERIV (%x. x ^ n) x :> (complex_of_real (real n)) * (x ^ (n - 1))"; -by (induct_tac "n" 1); -by (dtac (CDERIV_Id RS CDERIV_mult) 2); -by (auto_tac (claset(), - simpset() addsimps [complex_of_real_add RS sym, - left_distrib,real_of_nat_Suc] - delsimps [complex_of_real_add])); -by (case_tac "n" 1); -by (auto_tac (claset(), - simpset() addsimps [mult_assoc, add_commute])); -by (auto_tac (claset(),simpset() addsimps [mult_commute])); -qed "CDERIV_pow"; -Addsimps [CDERIV_pow,simplify (simpset()) CDERIV_pow]; - -(* NS version *) -Goal "NSCDERIV (%x. x ^ n) x :> complex_of_real (real n) * (x ^ (n - 1))"; -by (simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff]) 1); -qed "NSCDERIV_pow"; - -Goal "[|CDERIV f x :> D; D = E|] ==> CDERIV f x :> E"; -by Auto_tac; -qed "lemma_CDERIV_subst"; - -(*used once, in NSCDERIV_inverse*) -Goal "[| h: CInfinitesimal; x ~= 0 |] ==> hcomplex_of_complex x + h ~= 0"; -by (Clarify_tac 1); -by (dtac (thm"equals_zero_I") 1); -by Auto_tac; -qed "CInfinitesimal_add_not_zero"; - -(*Can't get rid of x ~= 0 because it isn't continuous at zero*) - -Goalw [nscderiv_def] - "x ~= 0 ==> NSCDERIV (%x. inverse(x)) x :> (- (inverse x ^ 2))"; -by (rtac ballI 1 THEN Asm_full_simp_tac 1 THEN Step_tac 1); -by (forward_tac [CInfinitesimal_add_not_zero] 1); -by (asm_full_simp_tac (simpset() addsimps [hcomplex_add_commute,numeral_2_eq_2]) 2); -by (auto_tac (claset(), - simpset() addsimps [starfunC_inverse_inverse,hcomplex_diff_def] - delsimps [minus_mult_left RS sym, minus_mult_right RS sym])); -by (asm_simp_tac - (simpset() addsimps [inverse_add, - inverse_mult_distrib RS sym, inverse_minus_eq RS sym] - @ add_ac @ mult_ac - delsimps [inverse_minus_eq, - inverse_mult_distrib, minus_mult_right RS sym, minus_mult_left RS sym] ) 1); -by (asm_simp_tac (HOL_ss addsimps [mult_assoc RS sym, right_distrib]) 1); -by (res_inst_tac [("y"," inverse(- hcomplex_of_complex x * hcomplex_of_complex x)")] - capprox_trans 1); -by (rtac inverse_add_CInfinitesimal_capprox2 1); -by (auto_tac (claset() addSDs [hcomplex_of_complex_CFinite_diff_CInfinitesimal] addIs [CFinite_mult], - simpset() addsimps [inverse_minus_eq RS sym])); -by (rtac CInfinitesimal_CFinite_mult2 1); -by Auto_tac; -qed "NSCDERIV_inverse"; - -Goal "x ~= 0 ==> CDERIV (%x. inverse(x)) x :> (-(inverse x ^ 2))"; -by (asm_simp_tac (simpset() addsimps [NSCDERIV_inverse, - NSCDERIV_CDERIV_iff RS sym] delsimps [complexpow_Suc]) 1); -qed "CDERIV_inverse"; - - -(*-----------------------------------------------------------------------*) -(* Derivative of inverse *) -(*-----------------------------------------------------------------------*) - -Goal "[| CDERIV f x :> d; f(x) ~= 0 |] \ -\ ==> CDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"; -by (rtac (mult_commute RS subst) 1); -by (asm_simp_tac (simpset() addsimps [minus_mult_left, - power_inverse] delsimps [complexpow_Suc, minus_mult_left RS sym]) 1); -by (fold_goals_tac [o_def]); -by (blast_tac (claset() addSIs [CDERIV_chain,CDERIV_inverse]) 1); -qed "CDERIV_inverse_fun"; - -Goal "[| NSCDERIV f x :> d; f(x) ~= 0 |] \ -\ ==> NSCDERIV (%x. inverse(f x)) x :> (- (d * inverse(f(x) ^ 2)))"; -by (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff, - CDERIV_inverse_fun] delsimps [complexpow_Suc]) 1); -qed "NSCDERIV_inverse_fun"; - -(*-----------------------------------------------------------------------*) -(* Derivative of quotient *) -(*-----------------------------------------------------------------------*) - - -Goal "x ~= (0::complex) \\ (x * inverse(x) ^ 2) = inverse x"; -by (auto_tac (claset(),simpset() addsimps [numeral_2_eq_2])); -qed "lemma_complex_mult_inverse_squared"; -Addsimps [lemma_complex_mult_inverse_squared]; - -Goalw [complex_diff_def] - "[| 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)"; -by (dres_inst_tac [("f","g")] CDERIV_inverse_fun 1); -by (dtac CDERIV_mult 2); -by (REPEAT(assume_tac 1)); -by (asm_full_simp_tac - (simpset() addsimps [complex_divide_def, right_distrib, - power_inverse,minus_mult_left] @ mult_ac - delsimps [complexpow_Suc, minus_mult_right RS sym, minus_mult_left RS sym]) 1); -qed "CDERIV_quotient"; - -Goal "[| 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 (asm_full_simp_tac (simpset() addsimps [NSCDERIV_CDERIV_iff, - CDERIV_quotient] delsimps [complexpow_Suc]) 1); -qed "NSCDERIV_quotient"; - - -(*-----------------------------------------------------------------------*) -(* Caratheodory formulation of derivative at a point: standard proof *) -(*-----------------------------------------------------------------------*) - - -Goalw [CLIM_def] - "[| ALL x. x ~= a --> (f x = g x) |] \ -\ ==> (f -- a --C> l) = (g -- a --C> l)"; -by (auto_tac (claset(), simpset() addsimps [complex_add_minus_iff])); -qed "CLIM_equal"; - -Goal "[| (%x. f(x) + -g(x)) -- a --C> 0; \ -\ g -- a --C> l |] \ -\ ==> f -- a --C> l"; -by (dtac CLIM_add 1 THEN assume_tac 1); -by (auto_tac (claset(), simpset() addsimps [complex_add_assoc])); -qed "CLIM_trans"; - -Goal "(CDERIV f x :> l) = \ -\ (EX g. (ALL z. f z - f x = g z * (z - x)) & isContc g x & g x = l)"; -by (Step_tac 1); -by (res_inst_tac - [("x","%z. if z = x then l else (f(z) - f(x)) / (z - x)")] exI 1); -by (auto_tac (claset(),simpset() addsimps [mult_assoc, - CLAIM "z ~= x ==> z - x ~= (0::complex)"])); -by (auto_tac (claset(),simpset() addsimps [isContc_iff,CDERIV_iff])); -by (ALLGOALS(rtac (CLIM_equal RS iffD1))); -by Auto_tac; -qed "CARAT_CDERIV"; - -Goal "NSCDERIV f x :> l ==> \ -\ EX g. (ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l"; -by (auto_tac (claset(),simpset() addsimps [NSCDERIV_CDERIV_iff, - isNSContc_isContc_iff,CARAT_CDERIV])); -qed "CARAT_NSCDERIV"; - -(* How about a NS proof? *) -Goal "(ALL z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l \ -\ ==> NSCDERIV f x :> l"; -by (auto_tac (claset(), - simpset() delsimprocs field_cancel_factor - addsimps [NSCDERIV_iff2])); -by (asm_full_simp_tac (simpset() addsimps [isNSContc_def]) 1); -qed "CARAT_CDERIVD"; - diff -r 4952c5a92e04 -r 534de3572a65 src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Sat Feb 21 08:43:08 2004 +0100 +++ b/src/HOL/Complex/CLim.thy Sat Feb 21 11:43:39 2004 +0100 @@ -1,82 +1,1170 @@ (* Title : CLim.thy Author : Jacques D. Fleuriot Copyright : 2001 University of Edinburgh - Description : A first theory of limits, continuity and + Description : A first theory of limits, continuity and differentiation for complex functions *) -CLim = CSeries + +theory CLim = CSeries: + +(*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 (auto simp add: numeral_2_eq_2) + +text{*Changing the quantified variable. Install earlier?*} +lemma all_shift: "(\x::'a::ring. 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 + CLIM :: "[complex=>complex,complex,complex] => bool" ("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60) "f -- a --C> L == - ALL r. 0 < r --> - (EX s. 0 < s & (ALL x. (x ~= a & (cmod(x - a) < s) + \r. 0 < r --> + (\s. 0 < s & (\x. (x \ a & (cmod(x - a) < s) --> cmod(f x - L) < r)))" - NSCLIM :: [complex=>complex,complex,complex] => bool + NSCLIM :: "[complex=>complex,complex,complex] => bool" ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60) - "f -- a --NSC> L == (ALL x. (x ~= hcomplex_of_complex a & - x @c= hcomplex_of_complex a - --> ( *fc* f) x @c= hcomplex_of_complex L))" + "f -- a --NSC> L == (\x. (x \ hcomplex_of_complex a & + x @c= hcomplex_of_complex a + --> ( *fc* f) x @c= hcomplex_of_complex L))" (* f: C --> R *) - CRLIM :: [complex=>real,complex,real] => bool + CRLIM :: "[complex=>real,complex,real] => bool" ("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60) "f -- a --CR> L == - ALL r. 0 < r --> - (EX s. 0 < s & (ALL x. (x ~= a & (cmod(x - a) < s) + \r. 0 < r --> + (\s. 0 < s & (\x. (x \ a & (cmod(x - a) < s) --> abs(f x - L) < r)))" - NSCRLIM :: [complex=>real,complex,real] => bool + NSCRLIM :: "[complex=>real,complex,real] => bool" ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60) - "f -- a --NSCR> L == (ALL x. (x ~= hcomplex_of_complex a & - x @c= hcomplex_of_complex a - --> ( *fcR* f) x @= hypreal_of_real L))" + "f -- a --NSCR> L == (\x. (x \ hcomplex_of_complex a & + x @c= hcomplex_of_complex a + --> ( *fcR* f) x @= hypreal_of_real L))" - isContc :: [complex=>complex,complex] => bool - "isContc f a == (f -- a --C> (f a))" + 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 == (ALL y. y @c= hcomplex_of_complex a --> + isNSContc :: "[complex=>complex,complex] => bool" + "isNSContc f a == (\y. y @c= hcomplex_of_complex a --> ( *fc* f) y @c= hcomplex_of_complex (f a))" - isContCR :: [complex=>real,complex] => bool - "isContCR f a == (f -- a --CR> (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 == (ALL y. y @c= hcomplex_of_complex a --> + isNSContCR :: "[complex=>real,complex] => bool" + "isNSContCR f a == (\y. y @c= hcomplex_of_complex a --> ( *fcR* f) y @= hypreal_of_real (f a))" (* differentiation: D is derivative of function f at x *) - cderiv:: [complex=>complex,complex,complex] => bool + 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 :: "[complex=>complex,complex,complex] => bool" ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60) - "NSCDERIV f x :> D == (ALL h: CInfinitesimal - {0}. + "NSCDERIV f x :> D == (\h \ CInfinitesimal - {0}. (( *fc* f)(hcomplex_of_complex x + h) - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)" - cdifferentiable :: [complex=>complex,complex] => bool (infixl 60) - "f cdifferentiable x == (EX D. CDERIV f x :> 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 --> ( *fc* f) x @c= ( *fc* 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)" +apply (unfold NSCLIM_def NSCRLIM_def) +apply (rule eq_Abs_hcomplex [of x]) +apply (auto simp add: starfunC_approx_Re_Im_iff hRe_hcomplex_of_complex) +done + +lemma NSCLIM_NSCRLIM_Im: + "f -- a --NSC> L ==> (%x. Im(f x)) -- a --NSCR> Im(L)" +apply (unfold NSCLIM_def NSCRLIM_def) +apply (rule eq_Abs_hcomplex [of x]) +apply (auto simp add: starfunC_approx_Re_Im_iff hIm_hcomplex_of_complex) +done + +lemma CLIM_NSCLIM: + "f -- x --C> L ==> f -- x --NSC> L" +apply (unfold CLIM_def NSCLIM_def capprox_def, auto) +apply (rule_tac z = xa in eq_Abs_hcomplex) +apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff + CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, 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_hcomplex_ALL: + "(\t. P t) = (\X. P (Abs_hcomplex(hcomplexrel `` {X})))" +apply auto +apply (rule_tac z = t in eq_Abs_hcomplex, 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 (unfold CLIM_def NSCLIM_def) +apply (rule ccontr) +apply (auto simp add: eq_Abs_hcomplex_ALL starfunC CInfinitesimal_capprox_minus [symmetric] hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def 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 hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcomplex_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 (unfold CRLIM_def NSCRLIM_def capprox_def, auto) +apply (rule_tac z = xa in eq_Abs_hcomplex) +apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff CInfinitesimal_hcmod_iff hcmod hypreal_diff Infinitesimal_FreeUltrafilterNat_iff Infinitesimal_approx_minus [symmetric] hypreal_of_real_def) +apply (rule bexI, rule_tac [2] lemma_hyprel_refl, 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 (unfold CRLIM_def NSCRLIM_def capprox_def) +apply (rule ccontr) +apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff + hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff + hcmod Infinitesimal_approx_minus [symmetric] + 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 hcomplex_of_complex_def + Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod) +apply (auto simp add: hypreal_of_real_def hypreal_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 (auto 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 (auto 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: complex_diff_def 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 (unfold NSCLIM_def, clarify) +apply (drule spec) +apply (auto 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 (rule_tac a1 = l in right_minus [THEN subst]) +apply (unfold complex_diff_def) +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 ***) - NSCdifferentiable :: [complex=>complex,complex] => bool (infixl 60) - "f NSCdifferentiable x == (EX D. NSCDERIV f x :> D)" +lemma NSCLIM_not_zero: "k \ 0 ==> ~ ((%x. k) -- x --NSC> 0)" +apply (auto simp del: hcomplex_of_complex_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: hcomplex_of_complex_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 [!] z = xa in eq_Abs_hcomplex) +apply (auto simp add: hcomplex_diff starfunC starfunCR hcomplex_of_complex_def hcmod mem_infmal_iff) +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 (auto 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 z = x in eq_Abs_hcomplex) +apply (auto simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_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 |] + ==> ( *fc* 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 hcomplex_add_commute) +apply (rule_tac [2] z = x in eq_Abs_hcomplex) +apply (rule_tac [4] z = x in eq_Abs_hcomplex) +apply (auto simp add: starfunC hcomplex_of_complex_def hcomplex_minus hcomplex_add) +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!: starfunC_mult_CFinite_capprox + simp del: starfunC_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 (auto simp add: isNSContc_isContc_iff [symmetric] isNSContc_def starfunC_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: complex_diff_def) +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 |] + ==> ( *fcR* 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 (auto 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 - isUContc :: (complex=>complex) => bool - "isUContc f == (ALL r. 0 < r --> - (EX s. 0 < s & (ALL x y. cmod(x - y) < s - --> cmod(f x - f y) < r)))" +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 starfunC_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 --> + ( *fc* (%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: hcomplex_add_assoc [symmetric]) +apply (auto simp add: mem_cinfmal_iff [symmetric] hcomplex_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: starfunC_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: hcomplex_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] complex_diff_def + 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 complex_diff_def) +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: complex_diff_def 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: complex_diff_def CDERIV_add_minus) + + +subsection{*Chain Rule*} + +(* lemmas *) +lemma NSCDERIV_zero: + "[| NSCDERIV g x :> D; + ( *fc* 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 |] + ==> ( *fc* 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; + ( *fc* g) (hcomplex_of_complex(x) + xa) \ hcomplex_of_complex (g x); + ( *fc* g) (hcomplex_of_complex(x) + xa) @c= hcomplex_of_complex (g x)|] + ==> (( *fc* f) (( *fc* g) (hcomplex_of_complex(x) + xa)) + - hcomplex_of_complex (f (g x))) / + (( *fc* g) (hcomplex_of_complex(x) + xa) - hcomplex_of_complex (g x)) + @c= hcomplex_of_complex (Da)" +by (auto 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 |] + ==> (( *fc* g) (hcomplex_of_complex x + xa) - hcomplex_of_complex(g x)) / xa + @c= hcomplex_of_complex (Db)" +by (auto simp add: NSCDERIV_NSCLIM_iff NSCLIM_def mem_cinfmal_iff starfunC_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: starfunC_lambda_cancel2 starfunC_o [symmetric]) +apply (case_tac "( *fc* g) (hcomplex_of_complex (x) + xa) = hcomplex_of_complex (g x) ") +apply (drule_tac g = g in NSCDERIV_zero) +apply (auto simp add: hcomplex_divide_def) +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]) +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_zero [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) + +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] - isNSUContc :: (complex=>complex) => bool - "isNSUContc f == (ALL x y. x @c= y --> ( *fc* f) x @c= ( *fc* f) y)" +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: complex_of_real_add [symmetric] 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: starfunC_inverse_inverse hcomplex_diff_def + simp del: minus_mult_left [symmetric] minus_mult_right [symmetric]) +apply (simp add: hcomplex_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 (no_asm_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: complex_diff_def) +apply (drule_tac f = g in CDERIV_inverse_fun) +apply (drule_tac [2] CDERIV_mult, assumption+) +apply (simp add: divide_inverse_zero right_distrib power_inverse minus_mult_left mult_ac + del: complexpow_Suc minus_mult_right [symmetric] minus_mult_left [symmetric]) +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 (auto simp add: NSCDERIV_CDERIV_iff isNSContc_isContc_iff CARAT_CDERIV) + +(* FIXME tidy! How about a NS proof? *) +lemma CARAT_CDERIVD: + "(\z. f z - f x = g z * (z - x)) & isNSContc g x & g x = l + ==> NSCDERIV f x :> l" +apply (simp only: NSCDERIV_iff2) +apply (tactic {*(auto_tac (claset(), + simpset() delsimprocs field_cancel_factor + addsimps [thm"NSCDERIV_iff2"])) *}) +apply (simp add: isNSContc_def) +done -end +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_hcomplex_ALL = thm "eq_Abs_hcomplex_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 diff -r 4952c5a92e04 -r 534de3572a65 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Feb 21 08:43:08 2004 +0100 +++ b/src/HOL/IsaMakefile Sat Feb 21 11:43:39 2004 +0100 @@ -158,8 +158,7 @@ Hyperreal/SEQ.ML Hyperreal/SEQ.thy Hyperreal/Series.ML Hyperreal/Series.thy\ Hyperreal/Star.thy Hyperreal/Transcendental.ML\ Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ - Complex/Complex_Main.thy\ - Complex/CLim.ML Complex/CLim.thy\ + Complex/Complex_Main.thy Complex/CLim.thy\ Complex/CSeries.ML Complex/CSeries.thy\ Complex/CStar.ML Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\ Complex/NSCA.ML Complex/NSCA.thy\