# HG changeset patch # User paulson # Date 1077390316 -3600 # Node ID 043bf0d9e9b528f1232372e9b06986f75332d102 # Parent e447f23bbe2dd873bd7e3af74f6f8b0a820be112 conversion of Complex/CStar to Isar script diff -r e447f23bbe2d -r 043bf0d9e9b5 src/HOL/Complex/CStar.ML --- a/src/HOL/Complex/CStar.ML Sat Feb 21 15:54:32 2004 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,629 +0,0 @@ -(* Title : CStar.ML - Author : Jacques D. Fleuriot - Copyright : 2001 University of Edinburgh - Description : defining *-transforms in NSA which extends sets of complex numbers, - and complex functions -*) - - - -(*-----------------------------------------------------------------------------------*) -(* Properties of the *-transform applied to sets of reals *) -(* ----------------------------------------------------------------------------------*) - -Goalw [starsetC_def] "*sc*(UNIV::complex set) = (UNIV::hcomplex set)"; -by (Auto_tac); -qed "STARC_complex_set"; -Addsimps [STARC_complex_set]; - -Goalw [starsetC_def] "*sc* {} = {}"; -by (Auto_tac); -qed "STARC_empty_set"; -Addsimps [STARC_empty_set]; - -Goalw [starsetC_def] "*sc* (A Un B) = *sc* A Un *sc* B"; -by (Auto_tac); -by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2)); -by (dtac bspec 1 THEN assume_tac 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (Auto_tac); -by (Ultra_tac 1); -qed "STARC_Un"; - -Goalw [starsetC_n_def] - "*scn* (%n. (A n) Un (B n)) = *scn* A Un *scn* B"; -by Auto_tac; -by (dres_inst_tac [("x","Xa")] bspec 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); -by (auto_tac (claset() addSDs [bspec], simpset())); -by (TRYALL(Ultra_tac)); -qed "starsetC_n_Un"; - -Goalw [InternalCSets_def] - "[| X : InternalCSets; Y : InternalCSets |] \ -\ ==> (X Un Y) : InternalCSets"; -by (auto_tac (claset(), - simpset() addsimps [starsetC_n_Un RS sym])); -qed "InternalCSets_Un"; - -Goalw [starsetC_def] "*sc* (A Int B) = *sc* A Int *sc* B"; -by (Auto_tac); -by (blast_tac (claset() addIs [FreeUltrafilterNat_Int, - FreeUltrafilterNat_subset]) 3); -by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); -qed "STARC_Int"; - -Goalw [starsetC_n_def] - "*scn* (%n. (A n) Int (B n)) = *scn* A Int *scn* B"; -by (Auto_tac); -by (auto_tac (claset() addSDs [bspec],simpset())); -by (TRYALL(Ultra_tac)); -qed "starsetC_n_Int"; - -Goalw [InternalCSets_def] - "[| X : InternalCSets; Y : InternalCSets |] \ -\ ==> (X Int Y) : InternalCSets"; -by (auto_tac (claset(), - simpset() addsimps [starsetC_n_Int RS sym])); -qed "InternalCSets_Int"; - -Goalw [starsetC_def] "*sc* -A = -( *sc* A)"; -by (Auto_tac); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); -by (REPEAT(Step_tac 1) THEN Auto_tac); -by (ALLGOALS(Ultra_tac)); -qed "STARC_Compl"; - -Goalw [starsetC_n_def] "*scn* ((%n. - A n)) = -( *scn* A)"; -by (Auto_tac); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); -by (REPEAT(Step_tac 1) THEN Auto_tac); -by (TRYALL(Ultra_tac)); -qed "starsetC_n_Compl"; - -Goalw [InternalCSets_def] - "X :InternalCSets ==> -X : InternalCSets"; -by (auto_tac (claset(), - simpset() addsimps [starsetC_n_Compl RS sym])); -qed "InternalCSets_Compl"; - -Goal "x ~: *sc* F ==> x : *sc* (- F)"; -by (auto_tac (claset(),simpset() addsimps [STARC_Compl])); -qed "STARC_mem_Compl"; - -Goal "*sc* (A - B) = *sc* A - *sc* B"; -by (auto_tac (claset(),simpset() addsimps - [Diff_eq,STARC_Int,STARC_Compl])); -qed "STARC_diff"; - -Goalw [starsetC_n_def] - "*scn* (%n. (A n) - (B n)) = *scn* A - *scn* B"; -by (Auto_tac); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 2); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 3); -by (auto_tac (claset() addSDs [bspec], simpset())); -by (TRYALL(Ultra_tac)); -qed "starsetC_n_diff"; - -Goalw [InternalCSets_def] - "[| X : InternalCSets; Y : InternalCSets |] \ -\ ==> (X - Y) : InternalCSets"; -by (auto_tac (claset(), simpset() addsimps [starsetC_n_diff RS sym])); -qed "InternalCSets_diff"; - -Goalw [starsetC_def] "A <= B ==> *sc* A <= *sc* B"; -by (REPEAT(blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1)); -qed "STARC_subset"; - -Goalw [starsetC_def,hcomplex_of_complex_def] - "a : A ==> hcomplex_of_complex a : *sc* A"; -by (auto_tac (claset() addIs [FreeUltrafilterNat_subset], - simpset())); -qed "STARC_mem"; - -Goalw [starsetC_def] "hcomplex_of_complex ` A <= *sc* A"; -by (auto_tac (claset(), simpset() addsimps [hcomplex_of_complex_def])); -by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 1); -qed "STARC_hcomplex_of_complex_image_subset"; - -Goal "SComplex <= *sc* (UNIV:: complex set)"; -by Auto_tac; -qed "STARC_SComplex_subset"; - -Goalw [starsetC_def] - "*sc* X Int SComplex = hcomplex_of_complex ` X"; -by (auto_tac (claset(), - simpset() addsimps - [hcomplex_of_complex_def,SComplex_def])); -by (fold_tac [hcomplex_of_complex_def]); -by (rtac imageI 1 THEN rtac ccontr 1); -by (dtac bspec 1); -by (rtac lemma_hcomplexrel_refl 1); -by (blast_tac (claset() addIs [FreeUltrafilterNat_subset]) 2); -by (Auto_tac); -qed "STARC_hcomplex_of_complex_Int"; - -Goal "x ~: hcomplex_of_complex ` A ==> ALL y: A. x ~= hcomplex_of_complex y"; -by (Auto_tac); -qed "lemma_not_hcomplexA"; - -Goalw [starsetC_n_def,starsetC_def] "*sc* X = *scn* (%n. X)"; -by Auto_tac; -qed "starsetC_starsetC_n_eq"; - -Goalw [InternalCSets_def] "( *sc* X) : InternalCSets"; -by (auto_tac (claset(), - simpset() addsimps [starsetC_starsetC_n_eq])); -qed "InternalCSets_starsetC_n"; -Addsimps [InternalCSets_starsetC_n]; - -Goal "X : InternalCSets ==> UNIV - X : InternalCSets"; -by (auto_tac (claset() addIs [InternalCSets_Compl], simpset())); -qed "InternalCSets_UNIV_diff"; - -(*-----------------------------------------------------------------------------------*) -(* Nonstandard extension of a set (defined using a constant sequence) as a special *) -(* case of an internal set *) -(*-----------------------------------------------------------------------------------*) - -Goalw [starsetC_n_def,starsetC_def] - "ALL n. (As n = A) ==> *scn* As = *sc* A"; -by (Auto_tac); -qed "starsetC_n_starsetC"; - -(*-----------------------------------------------------------------------------------*) -(* Theorems about nonstandard extensions of functions *) -(*-----------------------------------------------------------------------------------*) - -Goalw [starfunC_n_def,starfunC_def] - "ALL n. (F n = f) ==> *fcn* F = *fc* f"; -by (Auto_tac); -qed "starfunC_n_starfunC"; - -Goalw [starfunRC_n_def,starfunRC_def] - "ALL n. (F n = f) ==> *fRcn* F = *fRc* f"; -by (Auto_tac); -qed "starfunRC_n_starfunRC"; - -Goalw [starfunCR_n_def,starfunCR_def] - "ALL n. (F n = f) ==> *fcRn* F = *fcR* f"; -by (Auto_tac); -qed "starfunCR_n_starfunCR"; - -Goalw [congruent_def] - "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})"; -by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); -by (ALLGOALS(Ultra_tac)); -qed "starfunC_congruent"; - -(* f::complex => complex *) -Goalw [starfunC_def] - "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ -\ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"; -by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); -by (Ultra_tac 1); -qed "starfunC"; - -Goalw [starfunRC_def] - "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) = \ -\ Abs_hcomplex(hcomplexrel `` {%n. f (X n)})"; -by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by Auto_tac; -by (Ultra_tac 1); -qed "starfunRC"; - -Goalw [starfunCR_def] - "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ -\ Abs_hypreal(hyprel `` {%n. f (X n)})"; -by (res_inst_tac [("f","Abs_hypreal")] arg_cong 1); -by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); -by (Ultra_tac 1); -qed "starfunCR"; - -(** multiplication: ( *f ) x ( *g ) = *(f x g) **) - -Goal "( *fc* f) z * ( *fc* g) z = ( *fc* (%x. f x * g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_mult])); -qed "starfunC_mult"; -Addsimps [starfunC_mult RS sym]; - -Goal "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [starfunRC,hcomplex_mult])); -qed "starfunRC_mult"; -Addsimps [starfunRC_mult RS sym]; - -Goal "( *fcR* f) z * ( *fcR* g) z = ( *fcR* (%x. f x * g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunCR,hypreal_mult])); -qed "starfunCR_mult"; -Addsimps [starfunCR_mult RS sym]; - -(** addition: ( *f ) + ( *g ) = *(f + g) **) - -Goal "( *fc* f) z + ( *fc* g) z = ( *fc* (%x. f x + g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_add])); -qed "starfunC_add"; -Addsimps [starfunC_add RS sym]; - -Goal "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [starfunRC,hcomplex_add])); -qed "starfunRC_add"; -Addsimps [starfunRC_add RS sym]; - -Goal "( *fcR* f) z + ( *fcR* g) z = ( *fcR* (%x. f x + g x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunCR,hypreal_add])); -qed "starfunCR_add"; -Addsimps [starfunCR_add RS sym]; - -(** uminus **) -Goal "( *fc* (%x. - f x)) x = - ( *fc* f) x"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC, hcomplex_minus])); -qed "starfunC_minus"; -Addsimps [starfunC_minus]; - -Goal "( *fRc* (%x. - f x)) x = - ( *fRc* f) x"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [starfunRC, hcomplex_minus])); -qed "starfunRC_minus"; -Addsimps [starfunRC_minus]; - -Goal "( *fcR* (%x. - f x)) x = - ( *fcR* f) x"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR, hypreal_minus])); -qed "starfunCR_minus"; -Addsimps [starfunCR_minus]; - -(** addition: ( *f ) - ( *g ) = *(f - g) **) - -Goalw [hcomplex_diff_def,complex_diff_def] - "( *fc* f) xa - ( *fc* g) xa = ( *fc* (%x. f x - g x)) xa"; -by (auto_tac (claset(),simpset() addsimps [starfunC_minus,starfunC_add RS sym])); -qed "starfunC_diff"; -Addsimps [starfunC_diff RS sym]; - -Goalw [hcomplex_diff_def,complex_diff_def] - "( *fRc* f) xa - ( *fRc* g) xa = ( *fRc* (%x. f x - g x)) xa"; -by (auto_tac (claset(),simpset() addsimps [starfunRC_minus,starfunRC_add RS sym])); -qed "starfunRC_diff"; -Addsimps [starfunRC_diff RS sym]; - -Goalw [hypreal_diff_def,real_diff_def] - "( *fcR* f) xa - ( *fcR* g) xa = ( *fcR* (%x. f x - g x)) xa"; -by (auto_tac (claset(),simpset() addsimps [starfunCR_minus,starfunCR_add RS sym])); -qed "starfunCR_diff"; -Addsimps [starfunCR_diff RS sym]; - -(** composition: ( *f ) o ( *g ) = *(f o g) **) - -Goal "(%x. ( *fc* f) (( *fc* g) x)) = *fc* (%x. f (g x))"; -by (rtac ext 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC])); -qed "starfunC_o2"; - -Goalw [o_def] "( *fc* f) o ( *fc* g) = ( *fc* (f o g))"; -by (simp_tac (simpset() addsimps [starfunC_o2]) 1); -qed "starfunC_o"; - -Goal "(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))"; -by (rtac ext 1); -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [starfunRC,starfunC])); -qed "starfunC_starfunRC_o2"; - -Goal "(%x. ( *f* f) (( *fcR* g) x)) = *fcR* (%x. f (g x))"; -by (rtac ext 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR,starfun])); -qed "starfun_starfunCR_o2"; - -Goalw [o_def] "( *fc* f) o ( *fRc* g) = ( *fRc* (f o g))"; -by (simp_tac (simpset() addsimps [starfunC_starfunRC_o2]) 1); -qed "starfunC_starfunRC_o"; - -Goalw [o_def] "( *f* f) o ( *fcR* g) = ( *fcR* (f o g))"; -by (simp_tac (simpset() addsimps [starfun_starfunCR_o2]) 1); -qed "starfun_starfunCR_o"; - -Goal "( *fc* (%x. k)) z = hcomplex_of_complex k"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC, hcomplex_of_complex_def])); -qed "starfunC_const_fun"; -Addsimps [starfunC_const_fun]; - -Goal "( *fRc* (%x. k)) z = hcomplex_of_complex k"; -by (res_inst_tac [("z","z")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [starfunRC, hcomplex_of_complex_def])); -qed "starfunRC_const_fun"; -Addsimps [starfunRC_const_fun]; - -Goal "( *fcR* (%x. k)) z = hypreal_of_real k"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunCR, hypreal_of_real_def])); -qed "starfunCR_const_fun"; -Addsimps [starfunCR_const_fun]; - -Goal "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC, hcomplex_inverse])); -qed "starfunC_inverse"; -Addsimps [starfunC_inverse RS sym]; - -Goal "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x"; -by (res_inst_tac [("z","x")] eq_Abs_hypreal 1); -by (auto_tac (claset(), simpset() addsimps [starfunRC, hcomplex_inverse])); -qed "starfunRC_inverse"; -Addsimps [starfunRC_inverse RS sym]; - -Goal "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunCR, hypreal_inverse])); -qed "starfunCR_inverse"; -Addsimps [starfunCR_inverse RS sym]; - -Goal "( *fc* f) (hcomplex_of_complex a) = hcomplex_of_complex (f a)"; -by (auto_tac (claset(), - simpset() addsimps [starfunC,hcomplex_of_complex_def])); -qed "starfunC_eq"; -Addsimps [starfunC_eq]; - -Goal "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)"; -by (auto_tac (claset(), - simpset() addsimps [starfunRC,hcomplex_of_complex_def,hypreal_of_real_def])); -qed "starfunRC_eq"; -Addsimps [starfunRC_eq]; - -Goal "( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)"; -by (auto_tac (claset(), - simpset() addsimps [starfunCR,hcomplex_of_complex_def,hypreal_of_real_def])); -qed "starfunCR_eq"; -Addsimps [starfunCR_eq]; - -Goal "( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"; -by (Auto_tac); -qed "starfunC_capprox"; - -Goal "( *fRc* f) (hypreal_of_real a) @c= hcomplex_of_complex (f a)"; -by (Auto_tac); -qed "starfunRC_capprox"; - -Goal "( *fcR* f) (hcomplex_of_complex a) @= hypreal_of_real (f a)"; -by (Auto_tac); -qed "starfunCR_approx"; - -(* -Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"; -*) - -Goal "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"; -by (res_inst_tac [("z","Z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [hcpow,starfunC,hypnat_of_nat_eq])); -qed "starfunC_hcpow"; - -Goal "( *fc* (%h. f (x + h))) xa = ( *fc* f) (hcomplex_of_complex x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC, - hcomplex_of_complex_def,hcomplex_add])); -qed "starfunC_lambda_cancel"; - -Goal "( *fcR* (%h. f (x + h))) xa = ( *fcR* f) (hcomplex_of_complex x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR, - hcomplex_of_complex_def,hcomplex_add])); -qed "starfunCR_lambda_cancel"; - -Goal "( *fRc* (%h. f (x + h))) xa = ( *fRc* f) (hypreal_of_real x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [starfunRC, - hypreal_of_real_def,hypreal_add])); -qed "starfunRC_lambda_cancel"; - -Goal "( *fc* (%h. f(g(x + h)))) xa = ( *fc* (f o g)) (hcomplex_of_complex x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC, - hcomplex_of_complex_def,hcomplex_add])); -qed "starfunC_lambda_cancel2"; - -Goal "( *fcR* (%h. f(g(x + h)))) xa = ( *fcR* (f o g)) (hcomplex_of_complex x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR, - hcomplex_of_complex_def,hcomplex_add])); -qed "starfunCR_lambda_cancel2"; - -Goal "( *fRc* (%h. f(g(x + h)))) xa = ( *fRc* (f o g)) (hypreal_of_real x + xa)"; -by (res_inst_tac [("z","xa")] eq_Abs_hypreal 1); -by (auto_tac (claset(),simpset() addsimps [starfunRC, - hypreal_of_real_def,hypreal_add])); -qed "starfunRC_lambda_cancel2"; - -Goal "[| ( *fc* f) xa @c= l; ( *fc* g) xa @c= m; \ -\ l: CFinite; m: CFinite \ -\ |] ==> ( *fc* (%x. f x * g x)) xa @c= l * m"; -by (dtac capprox_mult_CFinite 1); -by (REPEAT(assume_tac 1)); -by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)], - simpset())); -qed "starfunC_mult_CFinite_capprox"; - -Goal "[| ( *fcR* f) xa @= l; ( *fcR* g) xa @= m; \ -\ l: HFinite; m: HFinite \ -\ |] ==> ( *fcR* (%x. f x * g x)) xa @= l * m"; -by (dtac approx_mult_HFinite 1); -by (REPEAT(assume_tac 1)); -by (auto_tac (claset() addIs [approx_sym RSN (2,approx_HFinite)], - simpset())); -qed "starfunCR_mult_HFinite_capprox"; - -Goal "[| ( *fRc* f) xa @c= l; ( *fRc* g) xa @c= m; \ -\ l: CFinite; m: CFinite \ -\ |] ==> ( *fRc* (%x. f x * g x)) xa @c= l * m"; -by (dtac capprox_mult_CFinite 1); -by (REPEAT(assume_tac 1)); -by (auto_tac (claset() addIs [capprox_sym RSN (2,capprox_CFinite)], - simpset())); -qed "starfunRC_mult_CFinite_capprox"; - -Goal "[| ( *fc* f) xa @c= l; ( *fc* g) xa @c= m \ -\ |] ==> ( *fc* (%x. f x + g x)) xa @c= l + m"; -by (auto_tac (claset() addIs [capprox_add], simpset())); -qed "starfunC_add_capprox"; - -Goal "[| ( *fRc* f) xa @c= l; ( *fRc* g) xa @c= m \ -\ |] ==> ( *fRc* (%x. f x + g x)) xa @c= l + m"; -by (auto_tac (claset() addIs [capprox_add], simpset())); -qed "starfunRC_add_capprox"; - -Goal "[| ( *fcR* f) xa @= l; ( *fcR* g) xa @= m \ -\ |] ==> ( *fcR* (%x. f x + g x)) xa @= l + m"; -by (auto_tac (claset() addIs [approx_add], simpset())); -qed "starfunCR_add_approx"; - -Goal "*fcR* cmod = hcmod"; -by (rtac ext 1); -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR,hcmod])); -qed "starfunCR_cmod"; - -Goal "( *fc* inverse) x = inverse(x)"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC,hcomplex_inverse])); -qed "starfunC_inverse_inverse"; - -Goalw [hcomplex_divide_def,complex_divide_def] - "( *fc* f) xa / ( *fc* g) xa = ( *fc* (%x. f x / g x)) xa"; -by Auto_tac; -qed "starfunC_divide"; -Addsimps [starfunC_divide RS sym]; - -Goalw [hypreal_divide_def,real_divide_def] - "( *fcR* f) xa / ( *fcR* g) xa = ( *fcR* (%x. f x / g x)) xa"; -by Auto_tac; -qed "starfunCR_divide"; -Addsimps [starfunCR_divide RS sym]; - -Goalw [hcomplex_divide_def,complex_divide_def] - "( *fRc* f) xa / ( *fRc* g) xa = ( *fRc* (%x. f x / g x)) xa"; -by Auto_tac; -qed "starfunRC_divide"; -Addsimps [starfunRC_divide RS sym]; - -(*-----------------------------------------------------------------------------------*) -(* Internal functions - some redundancy with *fc* now *) -(*-----------------------------------------------------------------------------------*) - -Goalw [congruent_def] - "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})"; -by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); -by (ALLGOALS(Fuf_tac)); -qed "starfunC_n_congruent"; - -Goalw [starfunC_n_def] - "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = \ -\ Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})"; -by (res_inst_tac [("f","Abs_hcomplex")] arg_cong 1); -by (auto_tac (clasimpset() addIffs [hcomplexrel_iff])); -by (Ultra_tac 1); -qed "starfunC_n"; - -(** multiplication: ( *fn ) x ( *gn ) = *(fn x gn) **) - -Goal "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_mult])); -qed "starfunC_n_mult"; - -(** addition: ( *fn ) + ( *gn ) = *(fn + gn) **) - -Goal "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_add])); -qed "starfunC_n_add"; - -(** uminus **) - -Goal "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_minus])); -qed "starfunC_n_minus"; - -(** subtraction: ( *fn ) - ( *gn ) = *(fn - gn) **) - -Goalw [hcomplex_diff_def,complex_diff_def] - "( *fcn* f) z - ( *fcn* g) z = ( *fcn* (%i x. f i x - g i x)) z"; -by (auto_tac (claset(), - simpset() addsimps [starfunC_n_add,starfunC_n_minus])); -qed "starfunNat_n_diff"; - -(** composition: ( *fn ) o ( *gn ) = *(fn o gn) **) - -Goal "( *fcn* (%i x. k)) z = hcomplex_of_complex k"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(), - simpset() addsimps [starfunC_n, hcomplex_of_complex_def])); -qed "starfunC_n_const_fun"; -Addsimps [starfunC_n_const_fun]; - -Goal "( *fcn* f) (hcomplex_of_complex n) = Abs_hcomplex(hcomplexrel `` {%i. f i n})"; -by (auto_tac (claset(), simpset() addsimps [starfunC_n,hcomplex_of_complex_def])); -qed "starfunC_n_eq"; -Addsimps [starfunC_n_eq]; - -Goal "(( *fc* f) = ( *fc* g)) = (f = g)"; -by Auto_tac; -by (rtac ext 1 THEN rtac ccontr 1); -by (dres_inst_tac [("x","hcomplex_of_complex(x)")] fun_cong 1); -by (auto_tac (claset(), simpset() addsimps [starfunC,hcomplex_of_complex_def])); -qed "starfunC_eq_iff"; - -Goal "(( *fRc* f) = ( *fRc* g)) = (f = g)"; -by Auto_tac; -by (rtac ext 1 THEN rtac ccontr 1); -by (dres_inst_tac [("x","hypreal_of_real(x)")] fun_cong 1); -by Auto_tac; -qed "starfunRC_eq_iff"; - -Goal "(( *fcR* f) = ( *fcR* g)) = (f = g)"; -by Auto_tac; -by (rtac ext 1 THEN rtac ccontr 1); -by (dres_inst_tac [("x","hcomplex_of_complex(x)")] fun_cong 1); -by Auto_tac; -qed "starfunCR_eq_iff"; - -(*** more theorems ***) - -Goal "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) & \ -\ (( *fcR* (%x. Im(f x))) x = hIm (z)))"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR,starfunC, - hIm,hRe,complex_Re_Im_cancel_iff])); -by (ALLGOALS(Ultra_tac)); -qed "starfunC_eq_Re_Im_iff"; - -Goal "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) & \ -\ (( *fcR* (%x. Im(f x))) x @= hIm (z)))"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunCR,starfunC, - hIm,hRe,capprox_approx_iff])); -qed "starfunC_approx_Re_Im_iff"; - -Goal "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex a"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC])); -qed "starfunC_Idfun_capprox"; - -Goal "( *fc* (%x. x)) x = x"; -by (res_inst_tac [("z","x")] eq_Abs_hcomplex 1); -by (auto_tac (claset(),simpset() addsimps [starfunC])); -qed "starfunC_Id"; -Addsimps [starfunC_Id]; diff -r e447f23bbe2d -r 043bf0d9e9b5 src/HOL/Complex/CStar.thy --- a/src/HOL/Complex/CStar.thy Sat Feb 21 15:54:32 2004 +0100 +++ b/src/HOL/Complex/CStar.thy Sat Feb 21 20:05:16 2004 +0100 @@ -1,57 +1,709 @@ (* Title : CStar.thy Author : Jacques D. Fleuriot Copyright : 2001 University of Edinburgh - Description : defining *-transforms in NSA which extends sets of complex numbers, - and complex functions *) -CStar = NSCA + +header{*Star-transforms in NSA, Extending Sets of Complex Numbers + and Complex Functions*} + +theory CStar = NSCA: constdefs (* nonstandard extension of sets *) - starsetC :: complex set => hcomplex set ("*sc* _" [80] 80) - "*sc* A == {x. ALL X: Rep_hcomplex(x). {n::nat. X n : A}: FreeUltrafilterNat}" + starsetC :: "complex set => hcomplex set" ("*sc* _" [80] 80) + "*sc* A == {x. \X \ Rep_hcomplex(x). {n. X n \ A} \ FreeUltrafilterNat}" (* internal sets *) - starsetC_n :: (nat => complex set) => hcomplex set ("*scn* _" [80] 80) - "*scn* As == {x. ALL X: Rep_hcomplex(x). {n::nat. X n : (As n)}: FreeUltrafilterNat}" - + starsetC_n :: "(nat => complex set) => hcomplex set" ("*scn* _" [80] 80) + "*scn* As == {x. \X \ Rep_hcomplex(x). + {n. X n \ (As n)} \ FreeUltrafilterNat}" + InternalCSets :: "hcomplex set set" - "InternalCSets == {X. EX As. X = *scn* As}" + "InternalCSets == {X. \As. X = *scn* As}" (* star transform of functions f: Complex --> Complex *) - starfunC :: (complex => complex) => hcomplex => hcomplex ("*fc* _" [80] 80) - "*fc* f == (%x. Abs_hcomplex(UN X: Rep_hcomplex(x). hcomplexrel``{%n. f (X n)}))" + starfunC :: "(complex => complex) => hcomplex => hcomplex" + ("*fc* _" [80] 80) + "*fc* f == + (%x. Abs_hcomplex(\X \ Rep_hcomplex(x). hcomplexrel``{%n. f (X n)}))" - starfunC_n :: (nat => (complex => complex)) => hcomplex => hcomplex ("*fcn* _" [80] 80) - "*fcn* F == (%x. Abs_hcomplex(UN X: Rep_hcomplex(x). hcomplexrel``{%n. (F n)(X n)}))" + starfunC_n :: "(nat => (complex => complex)) => hcomplex => hcomplex" + ("*fcn* _" [80] 80) + "*fcn* F == + (%x. Abs_hcomplex(\X \ Rep_hcomplex(x). hcomplexrel``{%n. (F n)(X n)}))" - InternalCFuns :: (hcomplex => hcomplex) set - "InternalCFuns == {X. EX F. X = *fcn* F}" + InternalCFuns :: "(hcomplex => hcomplex) set" + "InternalCFuns == {X. \F. X = *fcn* F}" (* star transform of functions f: Real --> Complex *) - starfunRC :: (real => complex) => hypreal => hcomplex ("*fRc* _" [80] 80) - "*fRc* f == (%x. Abs_hcomplex(UN X: Rep_hypreal(x). hcomplexrel``{%n. f (X n)}))" + starfunRC :: "(real => complex) => hypreal => hcomplex" + ("*fRc* _" [80] 80) + "*fRc* f == (%x. Abs_hcomplex(\X \ Rep_hypreal(x). hcomplexrel``{%n. f (X n)}))" - starfunRC_n :: (nat => (real => complex)) => hypreal => hcomplex ("*fRcn* _" [80] 80) - "*fRcn* F == (%x. Abs_hcomplex(UN X: Rep_hypreal(x). hcomplexrel``{%n. (F n)(X n)}))" + starfunRC_n :: "(nat => (real => complex)) => hypreal => hcomplex" + ("*fRcn* _" [80] 80) + "*fRcn* F == (%x. Abs_hcomplex(\X \ Rep_hypreal(x). hcomplexrel``{%n. (F n)(X n)}))" - InternalRCFuns :: (hypreal => hcomplex) set - "InternalRCFuns == {X. EX F. X = *fRcn* F}" + InternalRCFuns :: "(hypreal => hcomplex) set" + "InternalRCFuns == {X. \F. X = *fRcn* F}" (* star transform of functions f: Complex --> Real; needed for Re and Im parts *) - starfunCR :: (complex => real) => hcomplex => hypreal ("*fcR* _" [80] 80) - "*fcR* f == (%x. Abs_hypreal(UN X: Rep_hcomplex(x). hyprel``{%n. f (X n)}))" + starfunCR :: "(complex => real) => hcomplex => hypreal" + ("*fcR* _" [80] 80) + "*fcR* f == (%x. Abs_hypreal(\X \ Rep_hcomplex(x). hyprel``{%n. f (X n)}))" + + starfunCR_n :: "(nat => (complex => real)) => hcomplex => hypreal" + ("*fcRn* _" [80] 80) + "*fcRn* F == (%x. Abs_hypreal(\X \ Rep_hcomplex(x). hyprel``{%n. (F n)(X n)}))" + + InternalCRFuns :: "(hcomplex => hypreal) set" + "InternalCRFuns == {X. \F. X = *fcRn* F}" + + +subsection{*Properties of the *-Transform Applied to Sets of Reals*} + +lemma STARC_complex_set [simp]: "*sc*(UNIV::complex set) = (UNIV)" +by (simp add: starsetC_def) +declare STARC_complex_set + +lemma STARC_empty_set: "*sc* {} = {}" +by (simp add: starsetC_def) +declare STARC_empty_set [simp] + +lemma STARC_Un: "*sc* (A Un B) = *sc* A Un *sc* B" +apply (auto simp add: starsetC_def) +apply (drule bspec, assumption) +apply (rule_tac z = x in eq_Abs_hcomplex, simp, ultra) +apply (blast intro: FreeUltrafilterNat_subset)+ +done + +lemma starsetC_n_Un: "*scn* (%n. (A n) Un (B n)) = *scn* A Un *scn* B" +apply (auto simp add: starsetC_n_def) +apply (drule_tac x = Xa in bspec) +apply (rule_tac [2] z = x in eq_Abs_hcomplex) +apply (auto dest!: bspec, ultra+) +done + +lemma InternalCSets_Un: + "[| X \ InternalCSets; Y \ InternalCSets |] ==> (X Un Y) \ InternalCSets" +by (auto simp add: InternalCSets_def starsetC_n_Un [symmetric]) + +lemma STARC_Int: "*sc* (A Int B) = *sc* A Int *sc* B" +apply (auto simp add: starsetC_def) +prefer 3 apply (blast intro: FreeUltrafilterNat_Int FreeUltrafilterNat_subset) +apply (blast intro: FreeUltrafilterNat_subset)+ +done + +lemma starsetC_n_Int: "*scn* (%n. (A n) Int (B n)) = *scn* A Int *scn* B" +apply (auto simp add: starsetC_n_def) +apply (auto dest!: bspec, ultra+) +done + +lemma InternalCSets_Int: + "[| X \ InternalCSets; Y \ InternalCSets |] ==> (X Int Y) \ InternalCSets" +by (auto simp add: InternalCSets_def starsetC_n_Int [symmetric]) + +lemma STARC_Compl: "*sc* -A = -( *sc* A)" +apply (auto simp add: starsetC_def) +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (rule_tac [2] z = x in eq_Abs_hcomplex) +apply (auto dest!: bspec, ultra+) +done + +lemma starsetC_n_Compl: "*scn* ((%n. - A n)) = -( *scn* A)" +apply (auto simp add: starsetC_n_def) +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (rule_tac [2] z = x in eq_Abs_hcomplex) +apply (auto dest!: bspec, ultra+) +done + +lemma InternalCSets_Compl: "X :InternalCSets ==> -X \ InternalCSets" +by (auto simp add: InternalCSets_def starsetC_n_Compl [symmetric]) + +lemma STARC_mem_Compl: "x \ *sc* F ==> x \ *sc* (- F)" +by (simp add: STARC_Compl) + +lemma STARC_diff: "*sc* (A - B) = *sc* A - *sc* B" +by (simp add: Diff_eq STARC_Int STARC_Compl) + +lemma starsetC_n_diff: + "*scn* (%n. (A n) - (B n)) = *scn* A - *scn* B" +apply (auto simp add: starsetC_n_def) +apply (rule_tac [2] z = x in eq_Abs_hcomplex) +apply (rule_tac [3] z = x in eq_Abs_hcomplex) +apply (auto dest!: bspec, ultra+) +done + +lemma InternalCSets_diff: + "[| X \ InternalCSets; Y \ InternalCSets |] ==> (X - Y) \ InternalCSets" +by (auto simp add: InternalCSets_def starsetC_n_diff [symmetric]) + +lemma STARC_subset: "A \ B ==> *sc* A \ *sc* B" +apply (simp add: starsetC_def) +apply (blast intro: FreeUltrafilterNat_subset)+ +done + +lemma STARC_mem: "a \ A ==> hcomplex_of_complex a \ *sc* A" +apply (simp add: starsetC_def hcomplex_of_complex_def) +apply (auto intro: FreeUltrafilterNat_subset) +done + +lemma STARC_hcomplex_of_complex_image_subset: + "hcomplex_of_complex ` A \ *sc* A" +apply (auto simp add: starsetC_def hcomplex_of_complex_def) +apply (blast intro: FreeUltrafilterNat_subset) +done + +lemma STARC_SComplex_subset: "SComplex \ *sc* (UNIV:: complex set)" +by auto + +lemma STARC_hcomplex_of_complex_Int: + "*sc* X Int SComplex = hcomplex_of_complex ` X" +apply (auto simp add: starsetC_def hcomplex_of_complex_def SComplex_def) +apply (fold hcomplex_of_complex_def) +apply (rule imageI, rule ccontr) +apply (drule bspec) +apply (rule lemma_hcomplexrel_refl) +prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto) +done + +lemma lemma_not_hcomplexA: + "x \ hcomplex_of_complex ` A ==> \y \ A. x \ hcomplex_of_complex y" +by auto + +lemma starsetC_starsetC_n_eq: "*sc* X = *scn* (%n. X)" +by (simp add: starsetC_n_def starsetC_def) + +lemma InternalCSets_starsetC_n [simp]: "( *sc* X) \ InternalCSets" +by (auto simp add: InternalCSets_def starsetC_starsetC_n_eq) + +lemma InternalCSets_UNIV_diff: + "X \ InternalCSets ==> UNIV - X \ InternalCSets" +by (auto intro: InternalCSets_Compl) + +text{*Nonstandard extension of a set (defined using a constant sequence) as a special case of an internal set*} + +lemma starsetC_n_starsetC: "\n. (As n = A) ==> *scn* As = *sc* A" +by (simp add:starsetC_n_def starsetC_def) + + +subsection{*Theorems about Nonstandard Extensions of Functions*} + +lemma starfunC_n_starfunC: "\n. (F n = f) ==> *fcn* F = *fc* f" +by (simp add: starfunC_n_def starfunC_def) + +lemma starfunRC_n_starfunRC: "\n. (F n = f) ==> *fRcn* F = *fRc* f" +by (simp add: starfunRC_n_def starfunRC_def) + +lemma starfunCR_n_starfunCR: "\n. (F n = f) ==> *fcRn* F = *fcR* f" +by (simp add: starfunCR_n_def starfunCR_def) + +lemma starfunC_congruent: + "congruent hcomplexrel (%X. hcomplexrel``{%n. f (X n)})" +apply (auto simp add: hcomplexrel_iff congruent_def, ultra) +done + +(* f::complex => complex *) +lemma starfunC: + "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = + Abs_hcomplex(hcomplexrel `` {%n. f (X n)})" +apply (simp add: starfunC_def) +apply (rule arg_cong [where f = Abs_hcomplex]) +apply (auto iff add: hcomplexrel_iff, ultra) +done + +lemma starfunRC: + "( *fRc* f) (Abs_hypreal(hyprel``{%n. X n})) = + Abs_hcomplex(hcomplexrel `` {%n. f (X n)})" +apply (simp add: starfunRC_def) +apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra) +done + +lemma starfunCR: + "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = + Abs_hypreal(hyprel `` {%n. f (X n)})" +apply (simp add: starfunCR_def) +apply (rule arg_cong [where f = Abs_hypreal]) +apply (auto iff add: hcomplexrel_iff, ultra) +done + +(** multiplication: ( *f) x ( *g) = *(f x g) **) + +lemma starfunC_mult: "( *fc* f) z * ( *fc* g) z = ( *fc* (%x. f x * g x)) z" +apply (rule_tac z = z in eq_Abs_hcomplex) +apply (auto simp add: starfunC hcomplex_mult) +done +declare starfunC_mult [symmetric, simp] + +lemma starfunRC_mult: + "( *fRc* f) z * ( *fRc* g) z = ( *fRc* (%x. f x * g x)) z" +apply (rule eq_Abs_hypreal [of z]) +apply (simp add: starfunRC hcomplex_mult) +done +declare starfunRC_mult [symmetric, simp] + +lemma starfunCR_mult: + "( *fcR* f) z * ( *fcR* g) z = ( *fcR* (%x. f x * g x)) z" +apply (rule_tac z = z in eq_Abs_hcomplex) +apply (simp add: starfunCR hypreal_mult) +done +declare starfunCR_mult [symmetric, simp] + +(** addition: ( *f) + ( *g) = *(f + g) **) + +lemma starfunC_add: "( *fc* f) z + ( *fc* g) z = ( *fc* (%x. f x + g x)) z" +apply (rule_tac z = z in eq_Abs_hcomplex) +apply (simp add: starfunC hcomplex_add) +done +declare starfunC_add [symmetric, simp] + +lemma starfunRC_add: "( *fRc* f) z + ( *fRc* g) z = ( *fRc* (%x. f x + g x)) z" +apply (rule eq_Abs_hypreal [of z]) +apply (simp add: starfunRC hcomplex_add) +done +declare starfunRC_add [symmetric, simp] + +lemma starfunCR_add: "( *fcR* f) z + ( *fcR* g) z = ( *fcR* (%x. f x + g x)) z" +apply (rule_tac z = z in eq_Abs_hcomplex) +apply (simp add: starfunCR hypreal_add) +done +declare starfunCR_add [symmetric, simp] + +(** uminus **) +lemma starfunC_minus [simp]: "( *fc* (%x. - f x)) x = - ( *fc* f) x" +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (simp add: starfunC hcomplex_minus) +done + +lemma starfunRC_minus [simp]: "( *fRc* (%x. - f x)) x = - ( *fRc* f) x" +apply (rule eq_Abs_hypreal [of x]) +apply (simp add: starfunRC hcomplex_minus) +done + +lemma starfunCR_minus [simp]: "( *fcR* (%x. - f x)) x = - ( *fcR* f) x" +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (simp add: starfunCR hypreal_minus) +done + +(** addition: ( *f) - ( *g) = *(f - g) **) + +lemma starfunC_diff: "( *fc* f) y - ( *fc* g) y = ( *fc* (%x. f x - g x)) y" +by (simp add: diff_minus) +declare starfunC_diff [symmetric, simp] + +lemma starfunRC_diff: + "( *fRc* f) y - ( *fRc* g) y = ( *fRc* (%x. f x - g x)) y" +by (simp add: diff_minus) +declare starfunRC_diff [symmetric, simp] + +lemma starfunCR_diff: + "( *fcR* f) y - ( *fcR* g) y = ( *fcR* (%x. f x - g x)) y" +by (simp add: diff_minus) +declare starfunCR_diff [symmetric, simp] + +(** composition: ( *f) o ( *g) = *(f o g) **) + +lemma starfunC_o2: "(%x. ( *fc* f) (( *fc* g) x)) = *fc* (%x. f (g x))" +apply (rule ext) +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (simp add: starfunC) +done + +lemma starfunC_o: "( *fc* f) o ( *fc* g) = ( *fc* (f o g))" +by (simp add: o_def starfunC_o2) + +lemma starfunC_starfunRC_o2: + "(%x. ( *fc* f) (( *fRc* g) x)) = *fRc* (%x. f (g x))" +apply (rule ext) +apply (rule_tac z = x in eq_Abs_hypreal) +apply (simp add: starfunRC starfunC) +done + +lemma starfun_starfunCR_o2: + "(%x. ( *f* f) (( *fcR* g) x)) = *fcR* (%x. f (g x))" +apply (rule ext) +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (simp add: starfunCR starfun) +done + +lemma starfunC_starfunRC_o: "( *fc* f) o ( *fRc* g) = ( *fRc* (f o g))" +by (simp add: o_def starfunC_starfunRC_o2) + +lemma starfun_starfunCR_o: "( *f* f) o ( *fcR* g) = ( *fcR* (f o g))" +by (simp add: o_def starfun_starfunCR_o2) + +lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunC hcomplex_of_complex_def) +done + +lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k" +apply (rule eq_Abs_hypreal [of z]) +apply (simp add: starfunRC hcomplex_of_complex_def) +done + +lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunCR hypreal_of_real_def) +done + +lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: starfunC hcomplex_inverse) +done +declare starfunC_inverse [symmetric, simp] + +lemma starfunRC_inverse: + "inverse (( *fRc* f) x) = ( *fRc* (%x. inverse (f x))) x" +apply (rule eq_Abs_hypreal [of x]) +apply (simp add: starfunRC hcomplex_inverse) +done +declare starfunRC_inverse [symmetric, simp] + +lemma starfunCR_inverse: + "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: starfunCR hypreal_inverse) +done +declare starfunCR_inverse [symmetric, simp] + +lemma starfunC_eq [simp]: + "( *fc* f) (hcomplex_of_complex a) = hcomplex_of_complex (f a)" +by (simp add: starfunC hcomplex_of_complex_def) + +lemma starfunRC_eq [simp]: + "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)" +by (simp add: starfunRC hcomplex_of_complex_def hypreal_of_real_def) - starfunCR_n :: (nat => (complex => real)) => hcomplex => hypreal ("*fcRn* _" [80] 80) - "*fcRn* F == (%x. Abs_hypreal(UN X: Rep_hcomplex(x). hyprel``{%n. (F n)(X n)}))" +lemma starfunCR_eq [simp]: + "( *fcR* f) (hcomplex_of_complex a) = hypreal_of_real (f a)" +by (simp add: starfunCR hcomplex_of_complex_def hypreal_of_real_def) + +lemma starfunC_capprox: + "( *fc* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)" +by auto + +lemma starfunRC_capprox: + "( *fRc* f) (hypreal_of_real a) @c= hcomplex_of_complex (f a)" +by auto + +lemma starfunCR_approx: + "( *fcR* f) (hcomplex_of_complex a) @= hypreal_of_real (f a)" +by auto + +(* +Goal "( *fcNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N" +*) + +lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" +apply (rule eq_Abs_hcomplex [of Z]) +apply (simp add: hcpow starfunC hypnat_of_nat_eq) +done + +lemma starfunC_lambda_cancel: + "( *fc* (%h. f (x + h))) y = ( *fc* f) (hcomplex_of_complex x + y)" +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) +done + +lemma starfunCR_lambda_cancel: + "( *fcR* (%h. f (x + h))) y = ( *fcR* f) (hcomplex_of_complex x + y)" +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) +done + +lemma starfunRC_lambda_cancel: + "( *fRc* (%h. f (x + h))) y = ( *fRc* f) (hypreal_of_real x + y)" +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: starfunRC hypreal_of_real_def hypreal_add) +done + +lemma starfunC_lambda_cancel2: + "( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)" +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) +done + +lemma starfunCR_lambda_cancel2: + "( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)" +apply (rule eq_Abs_hcomplex [of y]) +apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) +done + +lemma starfunRC_lambda_cancel2: + "( *fRc* (%h. f(g(x + h)))) y = ( *fRc* (f o g)) (hypreal_of_real x + y)" +apply (rule eq_Abs_hypreal [of y]) +apply (simp add: starfunRC hypreal_of_real_def hypreal_add) +done + +lemma starfunC_mult_CFinite_capprox: + "[| ( *fc* f) y @c= l; ( *fc* g) y @c= m; l: CFinite; m: CFinite |] + ==> ( *fc* (%x. f x * g x)) y @c= l * m" +apply (drule capprox_mult_CFinite, assumption+) +apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) +done + +lemma starfunCR_mult_HFinite_capprox: + "[| ( *fcR* f) y @= l; ( *fcR* g) y @= m; l: HFinite; m: HFinite |] + ==> ( *fcR* (%x. f x * g x)) y @= l * m" +apply (drule approx_mult_HFinite, assumption+) +apply (auto intro: approx_sym [THEN [2] approx_HFinite]) +done + +lemma starfunRC_mult_CFinite_capprox: + "[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m; l: CFinite; m: CFinite |] + ==> ( *fRc* (%x. f x * g x)) y @c= l * m" +apply (drule capprox_mult_CFinite, assumption+) +apply (auto intro: capprox_sym [THEN [2] capprox_CFinite]) +done + +lemma starfunC_add_capprox: + "[| ( *fc* f) y @c= l; ( *fc* g) y @c= m |] + ==> ( *fc* (%x. f x + g x)) y @c= l + m" +by (auto intro: capprox_add) + +lemma starfunRC_add_capprox: + "[| ( *fRc* f) y @c= l; ( *fRc* g) y @c= m |] + ==> ( *fRc* (%x. f x + g x)) y @c= l + m" +by (auto intro: capprox_add) + +lemma starfunCR_add_approx: + "[| ( *fcR* f) y @= l; ( *fcR* g) y @= m + |] ==> ( *fcR* (%x. f x + g x)) y @= l + m" +by (auto intro: approx_add) + +lemma starfunCR_cmod: "*fcR* cmod = hcmod" +apply (rule ext) +apply (rule_tac z = x in eq_Abs_hcomplex) +apply (simp add: starfunCR hcmod) +done + +lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: starfunC hcomplex_inverse) +done + +lemma starfunC_divide: "( *fc* f) y / ( *fc* g) y = ( *fc* (%x. f x / g x)) y" +by (simp add: divide_inverse_zero) +declare starfunC_divide [symmetric, simp] + +lemma starfunCR_divide: + "( *fcR* f) y / ( *fcR* g) y = ( *fcR* (%x. f x / g x)) y" +by (simp add: divide_inverse_zero) +declare starfunCR_divide [symmetric, simp] + +lemma starfunRC_divide: + "( *fRc* f) y / ( *fRc* g) y = ( *fRc* (%x. f x / g x)) y" +apply (simp add: divide_inverse_zero) +done +declare starfunRC_divide [symmetric, simp] + + +subsection{*Internal Functions - Some Redundancy With *Fc* Now*} + +lemma starfunC_n_congruent: + "congruent hcomplexrel (%X. hcomplexrel``{%n. f n (X n)})" +by (auto simp add: congruent_def hcomplexrel_iff, ultra) + +lemma starfunC_n: + "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = + Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})" +apply (simp add: starfunC_n_def) +apply (rule arg_cong [where f = Abs_hcomplex]) +apply (auto iff add: hcomplexrel_iff, ultra) +done + +(** multiplication: ( *fn) x ( *gn) = *(fn x gn) **) + +lemma starfunC_n_mult: + "( *fcn* f) z * ( *fcn* g) z = ( *fcn* (% i x. f i x * g i x)) z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunC_n hcomplex_mult) +done + +(** addition: ( *fn) + ( *gn) = *(fn + gn) **) + +lemma starfunC_n_add: + "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunC_n hcomplex_add) +done + +(** uminus **) + +lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunC_n hcomplex_minus) +done + +(** subtraction: ( *fn) - ( *gn) = *(fn - gn) **) - InternalCRFuns :: (hcomplex => hypreal) set - "InternalCRFuns == {X. EX F. X = *fcRn* F}" +lemma starfunNat_n_diff: + "( *fcn* f) z - ( *fcn* g) z = ( *fcn* (%i x. f i x - g i x)) z" +by (simp add: diff_minus starfunC_n_add starfunC_n_minus) + +(** composition: ( *fn) o ( *gn) = *(fn o gn) **) + +lemma starfunC_n_const_fun [simp]: + "( *fcn* (%i x. k)) z = hcomplex_of_complex k" +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunC_n hcomplex_of_complex_def) +done + +lemma starfunC_n_eq [simp]: + "( *fcn* f) (hcomplex_of_complex n) = Abs_hcomplex(hcomplexrel `` {%i. f i n})" +by (simp add: starfunC_n hcomplex_of_complex_def) + +lemma starfunC_eq_iff: "(( *fc* f) = ( *fc* g)) = (f = g)" +apply auto +apply (rule ext, rule ccontr) +apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong) +apply (simp add: starfunC hcomplex_of_complex_def) +done + +lemma starfunRC_eq_iff: "(( *fRc* f) = ( *fRc* g)) = (f = g)" +apply auto +apply (rule ext, rule ccontr) +apply (drule_tac x = "hypreal_of_real (x) " in fun_cong) +apply auto +done + +lemma starfunCR_eq_iff: "(( *fcR* f) = ( *fcR* g)) = (f = g)" +apply auto +apply (rule ext, rule ccontr) +apply (drule_tac x = "hcomplex_of_complex (x) " in fun_cong) +apply auto +done + +lemma starfunC_eq_Re_Im_iff: + "(( *fc* f) x = z) = ((( *fcR* (%x. Re(f x))) x = hRe (z)) & + (( *fcR* (%x. Im(f x))) x = hIm (z)))" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of z]) +apply (auto simp add: starfunCR starfunC hIm hRe complex_Re_Im_cancel_iff, ultra+) +done + +lemma starfunC_approx_Re_Im_iff: + "(( *fc* f) x @c= z) = ((( *fcR* (%x. Re(f x))) x @= hRe (z)) & + (( *fcR* (%x. Im(f x))) x @= hIm (z)))" +apply (rule eq_Abs_hcomplex [of x]) +apply (rule eq_Abs_hcomplex [of z]) +apply (simp add: starfunCR starfunC hIm hRe capprox_approx_iff) +done + +lemma starfunC_Idfun_capprox: + "x @c= hcomplex_of_complex a ==> ( *fc* (%x. x)) x @c= hcomplex_of_complex a" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: starfunC) +done + +lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x" +apply (rule eq_Abs_hcomplex [of x]) +apply (simp add: starfunC) +done -end \ No newline at end of file +ML +{* +val STARC_complex_set = thm "STARC_complex_set"; +val STARC_empty_set = thm "STARC_empty_set"; +val STARC_Un = thm "STARC_Un"; +val starsetC_n_Un = thm "starsetC_n_Un"; +val InternalCSets_Un = thm "InternalCSets_Un"; +val STARC_Int = thm "STARC_Int"; +val starsetC_n_Int = thm "starsetC_n_Int"; +val InternalCSets_Int = thm "InternalCSets_Int"; +val STARC_Compl = thm "STARC_Compl"; +val starsetC_n_Compl = thm "starsetC_n_Compl"; +val InternalCSets_Compl = thm "InternalCSets_Compl"; +val STARC_mem_Compl = thm "STARC_mem_Compl"; +val STARC_diff = thm "STARC_diff"; +val starsetC_n_diff = thm "starsetC_n_diff"; +val InternalCSets_diff = thm "InternalCSets_diff"; +val STARC_subset = thm "STARC_subset"; +val STARC_mem = thm "STARC_mem"; +val STARC_hcomplex_of_complex_image_subset = thm "STARC_hcomplex_of_complex_image_subset"; +val STARC_SComplex_subset = thm "STARC_SComplex_subset"; +val STARC_hcomplex_of_complex_Int = thm "STARC_hcomplex_of_complex_Int"; +val lemma_not_hcomplexA = thm "lemma_not_hcomplexA"; +val starsetC_starsetC_n_eq = thm "starsetC_starsetC_n_eq"; +val InternalCSets_starsetC_n = thm "InternalCSets_starsetC_n"; +val InternalCSets_UNIV_diff = thm "InternalCSets_UNIV_diff"; +val starsetC_n_starsetC = thm "starsetC_n_starsetC"; +val starfunC_n_starfunC = thm "starfunC_n_starfunC"; +val starfunRC_n_starfunRC = thm "starfunRC_n_starfunRC"; +val starfunCR_n_starfunCR = thm "starfunCR_n_starfunCR"; +val starfunC_congruent = thm "starfunC_congruent"; +val starfunC = thm "starfunC"; +val starfunRC = thm "starfunRC"; +val starfunCR = thm "starfunCR"; +val starfunC_mult = thm "starfunC_mult"; +val starfunRC_mult = thm "starfunRC_mult"; +val starfunCR_mult = thm "starfunCR_mult"; +val starfunC_add = thm "starfunC_add"; +val starfunRC_add = thm "starfunRC_add"; +val starfunCR_add = thm "starfunCR_add"; +val starfunC_minus = thm "starfunC_minus"; +val starfunRC_minus = thm "starfunRC_minus"; +val starfunCR_minus = thm "starfunCR_minus"; +val starfunC_diff = thm "starfunC_diff"; +val starfunRC_diff = thm "starfunRC_diff"; +val starfunCR_diff = thm "starfunCR_diff"; +val starfunC_o2 = thm "starfunC_o2"; +val starfunC_o = thm "starfunC_o"; +val starfunC_starfunRC_o2 = thm "starfunC_starfunRC_o2"; +val starfun_starfunCR_o2 = thm "starfun_starfunCR_o2"; +val starfunC_starfunRC_o = thm "starfunC_starfunRC_o"; +val starfun_starfunCR_o = thm "starfun_starfunCR_o"; +val starfunC_const_fun = thm "starfunC_const_fun"; +val starfunRC_const_fun = thm "starfunRC_const_fun"; +val starfunCR_const_fun = thm "starfunCR_const_fun"; +val starfunC_inverse = thm "starfunC_inverse"; +val starfunRC_inverse = thm "starfunRC_inverse"; +val starfunCR_inverse = thm "starfunCR_inverse"; +val starfunC_eq = thm "starfunC_eq"; +val starfunRC_eq = thm "starfunRC_eq"; +val starfunCR_eq = thm "starfunCR_eq"; +val starfunC_capprox = thm "starfunC_capprox"; +val starfunRC_capprox = thm "starfunRC_capprox"; +val starfunCR_approx = thm "starfunCR_approx"; +val starfunC_hcpow = thm "starfunC_hcpow"; +val starfunC_lambda_cancel = thm "starfunC_lambda_cancel"; +val starfunCR_lambda_cancel = thm "starfunCR_lambda_cancel"; +val starfunRC_lambda_cancel = thm "starfunRC_lambda_cancel"; +val starfunC_lambda_cancel2 = thm "starfunC_lambda_cancel2"; +val starfunCR_lambda_cancel2 = thm "starfunCR_lambda_cancel2"; +val starfunRC_lambda_cancel2 = thm "starfunRC_lambda_cancel2"; +val starfunC_mult_CFinite_capprox = thm "starfunC_mult_CFinite_capprox"; +val starfunCR_mult_HFinite_capprox = thm "starfunCR_mult_HFinite_capprox"; +val starfunRC_mult_CFinite_capprox = thm "starfunRC_mult_CFinite_capprox"; +val starfunC_add_capprox = thm "starfunC_add_capprox"; +val starfunRC_add_capprox = thm "starfunRC_add_capprox"; +val starfunCR_add_approx = thm "starfunCR_add_approx"; +val starfunCR_cmod = thm "starfunCR_cmod"; +val starfunC_inverse_inverse = thm "starfunC_inverse_inverse"; +val starfunC_divide = thm "starfunC_divide"; +val starfunCR_divide = thm "starfunCR_divide"; +val starfunRC_divide = thm "starfunRC_divide"; +val starfunC_n_congruent = thm "starfunC_n_congruent"; +val starfunC_n = thm "starfunC_n"; +val starfunC_n_mult = thm "starfunC_n_mult"; +val starfunC_n_add = thm "starfunC_n_add"; +val starfunC_n_minus = thm "starfunC_n_minus"; +val starfunNat_n_diff = thm "starfunNat_n_diff"; +val starfunC_n_const_fun = thm "starfunC_n_const_fun"; +val starfunC_n_eq = thm "starfunC_n_eq"; +val starfunC_eq_iff = thm "starfunC_eq_iff"; +val starfunRC_eq_iff = thm "starfunRC_eq_iff"; +val starfunCR_eq_iff = thm "starfunCR_eq_iff"; +val starfunC_eq_Re_Im_iff = thm "starfunC_eq_Re_Im_iff"; +val starfunC_approx_Re_Im_iff = thm "starfunC_approx_Re_Im_iff"; +val starfunC_Idfun_capprox = thm "starfunC_Idfun_capprox"; +val starfunC_Id = thm "starfunC_Id"; +*} + +end diff -r e447f23bbe2d -r 043bf0d9e9b5 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sat Feb 21 15:54:32 2004 +0100 +++ b/src/HOL/IsaMakefile Sat Feb 21 20:05:16 2004 +0100 @@ -159,7 +159,7 @@ Hyperreal/Star.thy Hyperreal/Transcendental.ML\ Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \ Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy\ - Complex/CStar.ML Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\ + Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy\ Complex/NSCA.ML Complex/NSCA.thy\ Complex/NSComplex.thy @cd Complex; $(ISATOOL) usedir -b $(OUT)/HOL HOL-Complex