# HG changeset patch # User huffman # Date 1126050589 -7200 # Node ID 5798fbf42a6ac9bf4ea59c674ece6e87ad1c1eb3 # Parent c6eecde058e48458fc8fa4a970f66ccfce229342 replace type hcomplex with complex star diff -r c6eecde058e4 -r 5798fbf42a6a src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Wed Sep 07 00:48:50 2005 +0200 +++ b/src/HOL/Complex/CLim.thy Wed Sep 07 01:49:49 2005 +0200 @@ -123,8 +123,9 @@ lemma CLIM_NSCLIM: "f -- x --C> L ==> f -- x --NSC> L" apply (simp add: CLIM_def NSCLIM_def capprox_def, auto) -apply (rule_tac z = xa in eq_Abs_hcomplex) +apply (rule_tac z = xa in eq_Abs_star) apply (auto simp add: hcomplex_of_complex_def starfunC hcomplex_diff + star_of_def star_n_def CInfinitesimal_hcmod_iff hcmod Infinitesimal_FreeUltrafilterNat_iff) apply (rule bexI, rule_tac [2] lemma_starrel_refl, safe) apply (drule_tac x = u in spec, auto) @@ -132,10 +133,10 @@ apply (drule sym, auto) done -lemma eq_Abs_hcomplex_ALL: - "(\t. P t) = (\X. P (Abs_hcomplex(hcomplexrel `` {X})))" +lemma eq_Abs_star_ALL: + "(\t. P t) = (\X. P (Abs_star(starrel `` {X})))" apply auto -apply (rule_tac z = t in eq_Abs_hcomplex, auto) +apply (rule_tac z = t in eq_Abs_star, auto) done lemma lemma_CLIM: @@ -168,15 +169,17 @@ "f -- x --NSC> L ==> f -- x --C> L" apply (simp add: CLIM_def NSCLIM_def) apply (rule ccontr) -apply (auto simp add: eq_Abs_hcomplex_ALL starfunC +apply (auto simp add: eq_Abs_star_ALL starfunC CInfinitesimal_capprox_minus [symmetric] hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def + star_of_def star_n_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 + star_of_def star_n_def Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod, blast) apply (drule_tac x = r in spec, clarify) apply (drule FreeUltrafilterNat_all, ultra, arith) @@ -192,7 +195,7 @@ lemma CRLIM_NSCRLIM: "f -- x --CR> L ==> f -- x --NSCR> L" apply (simp add: CRLIM_def NSCRLIM_def capprox_def, auto) -apply (rule_tac z = xa in eq_Abs_hcomplex) +apply (rule_tac z = xa in eq_Abs_star) apply (auto simp add: hcomplex_of_complex_def starfunCR hcomplex_diff CInfinitesimal_hcmod_iff hcmod hypreal_diff Infinitesimal_FreeUltrafilterNat_iff @@ -232,15 +235,17 @@ lemma NSCRLIM_CRLIM: "f -- x --NSCR> L ==> f -- x --CR> L" apply (simp add: CRLIM_def NSCRLIM_def capprox_def) apply (rule ccontr) -apply (auto simp add: eq_Abs_hcomplex_ALL starfunCR hcomplex_diff +apply (auto simp add: eq_Abs_star_ALL starfunCR hcomplex_diff hcomplex_of_complex_def hypreal_diff CInfinitesimal_hcmod_iff - hcmod Infinitesimal_approx_minus [symmetric] + hcmod Infinitesimal_approx_minus [symmetric] + star_of_def star_n_def 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 + star_of_def star_n_def Infinitesimal_FreeUltrafilterNat_iff hcomplex_diff hcmod) apply (auto simp add: hypreal_of_real_def star_of_def star_n_def hypreal_diff) apply (drule_tac x = r in spec, clarify) @@ -408,8 +413,8 @@ "(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) +apply (rule_tac [!] z = xa in eq_Abs_star) +apply (auto simp add: hcomplex_diff starfunC starfunCR hcomplex_of_complex_def hcmod mem_infmal_iff star_of_def star_n_def) done (** much, much easier standard proof **) @@ -427,7 +432,7 @@ 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 (rule_tac z = x in eq_Abs_star) apply (simp add: capprox_approx_iff starfunC hcomplex_of_complex_def starfunCR hypreal_of_real_def star_of_def star_n_def) done @@ -481,9 +486,9 @@ 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) +apply (rule_tac [2] z = x in eq_Abs_star) +apply (rule_tac [4] z = x in eq_Abs_star) +apply (auto simp add: starfunC hcomplex_of_complex_def hcomplex_minus hcomplex_add star_of_def star_n_def) done lemma NSCLIM_isContc_iff: @@ -860,7 +865,7 @@ 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 (auto simp add: divide_inverse) 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) @@ -1028,7 +1033,7 @@ 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 eq_Abs_star_ALL = thm "eq_Abs_star_ALL"; val lemma_CLIM = thm "lemma_CLIM"; val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2"; val lemma_csimp = thm "lemma_csimp"; diff -r c6eecde058e4 -r 5798fbf42a6a src/HOL/Complex/CStar.thy --- a/src/HOL/Complex/CStar.thy Wed Sep 07 00:48:50 2005 +0200 +++ b/src/HOL/Complex/CStar.thy Wed Sep 07 01:49:49 2005 +0200 @@ -14,11 +14,11 @@ (* nonstandard extension of sets *) starsetC :: "complex set => hcomplex set" ("*sc* _" [80] 80) - "*sc* A == {x. \X \ Rep_hcomplex(x). {n. X n \ A} \ FreeUltrafilterNat}" + "*sc* A == {x. \X \ Rep_star(x). {n. X n \ A} \ FreeUltrafilterNat}" (* internal sets *) starsetC_n :: "(nat => complex set) => hcomplex set" ("*scn* _" [80] 80) - "*scn* As == {x. \X \ Rep_hcomplex(x). + "*scn* As == {x. \X \ Rep_star(x). {n. X n \ (As n)} \ FreeUltrafilterNat}" InternalCSets :: "hcomplex set set" @@ -29,12 +29,12 @@ starfunC :: "(complex => complex) => hcomplex => hcomplex" ("*fc* _" [80] 80) "*fc* f == - (%x. Abs_hcomplex(\X \ Rep_hcomplex(x). hcomplexrel``{%n. f (X n)}))" + (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. f (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)}))" + (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. (F n)(X n)}))" InternalCFuns :: "(hcomplex => hcomplex) set" "InternalCFuns == {X. \F. X = *fcn* F}" @@ -44,11 +44,11 @@ starfunRC :: "(real => complex) => hypreal => hcomplex" ("*fRc* _" [80] 80) - "*fRc* f == (%x. Abs_hcomplex(\X \ Rep_star(x). hcomplexrel``{%n. f (X n)}))" + "*fRc* f == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. f (X n)}))" starfunRC_n :: "(nat => (real => complex)) => hypreal => hcomplex" ("*fRcn* _" [80] 80) - "*fRcn* F == (%x. Abs_hcomplex(\X \ Rep_star(x). hcomplexrel``{%n. (F n)(X n)}))" + "*fRcn* F == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. (F n)(X n)}))" InternalRCFuns :: "(hypreal => hcomplex) set" "InternalRCFuns == {X. \F. X = *fRcn* F}" @@ -57,11 +57,11 @@ starfunCR :: "(complex => real) => hcomplex => hypreal" ("*fcR* _" [80] 80) - "*fcR* f == (%x. Abs_star(\X \ Rep_hcomplex(x). starrel``{%n. f (X n)}))" + "*fcR* f == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. f (X n)}))" starfunCR_n :: "(nat => (complex => real)) => hcomplex => hypreal" ("*fcRn* _" [80] 80) - "*fcRn* F == (%x. Abs_star(\X \ Rep_hcomplex(x). starrel``{%n. (F n)(X n)}))" + "*fcRn* F == (%x. Abs_star(\X \ Rep_star(x). starrel``{%n. (F n)(X n)}))" InternalCRFuns :: "(hcomplex => hypreal) set" "InternalCRFuns == {X. \F. X = *fcRn* F}" @@ -80,14 +80,14 @@ 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 (rule_tac z = x in eq_Abs_star, 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 (rule_tac [2] z = x in eq_Abs_star) apply (auto dest!: bspec, ultra+) done @@ -112,15 +112,15 @@ 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 (rule_tac z = x in eq_Abs_star) +apply (rule_tac [2] z = x in eq_Abs_star) 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 (rule_tac z = x in eq_Abs_star) +apply (rule_tac [2] z = x in eq_Abs_star) apply (auto dest!: bspec, ultra+) done @@ -136,8 +136,8 @@ 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 (rule_tac [2] z = x in eq_Abs_star) +apply (rule_tac [3] z = x in eq_Abs_star) apply (auto dest!: bspec, ultra+) done @@ -151,13 +151,13 @@ done lemma STARC_mem: "a \ A ==> hcomplex_of_complex a \ *sc* A" -apply (simp add: starsetC_def hcomplex_of_complex_def) +apply (simp add: starsetC_def hcomplex_of_complex_def star_of_def star_n_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 (auto simp add: starsetC_def hcomplex_of_complex_def star_of_def star_n_def) apply (blast intro: FreeUltrafilterNat_subset) done @@ -166,11 +166,11 @@ 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 (auto simp add: starsetC_def hcomplex_of_complex_def SComplex_def star_of_def star_n_def) +apply (fold star_n_def star_of_def hcomplex_of_complex_def) apply (rule imageI, rule ccontr) apply (drule bspec) -apply (rule lemma_hcomplexrel_refl) +apply (rule lemma_starrel_refl) prefer 2 apply (blast intro: FreeUltrafilterNat_subset, auto) done @@ -207,44 +207,44 @@ by (simp add: starfunCR_n_def starfunCR_def) lemma starfunC_congruent: - "(%X. hcomplexrel``{%n. f (X n)}) respects hcomplexrel" -by (auto simp add: hcomplexrel_iff congruent_def, ultra) + "(%X. starrel``{%n. f (X n)}) respects starrel" +by (auto simp add: starrel_iff congruent_def, ultra) (* f::complex => complex *) lemma starfunC: - "( *fc* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. f (X n)})" + "( *fc* f) (Abs_star(starrel``{%n. X n})) = + Abs_star(starrel `` {%n. f (X n)})" apply (simp add: starfunC_def) -apply (rule arg_cong [where f = Abs_hcomplex]) -apply (auto iff add: hcomplexrel_iff, ultra) +apply (rule arg_cong [where f = Abs_star]) +apply (auto iff add: starrel_iff, ultra) done lemma cstarfun_if_eq: "w \ hcomplex_of_complex x ==> ( *fc* (\z. if z = x then a else g z)) w = ( *fc* g) w" -apply (cases w) -apply (simp add: hcomplex_of_complex_def starfunC, ultra) +apply (rule_tac z=w in eq_Abs_star) +apply (simp add: hcomplex_of_complex_def star_of_def star_n_def starfunC, ultra) done lemma starfunRC: "( *fRc* f) (Abs_star(starrel``{%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. f (X n)})" + Abs_star(starrel `` {%n. f (X n)})" apply (simp add: starfunRC_def) -apply (rule arg_cong [where f = Abs_hcomplex], auto, ultra) +apply (rule arg_cong [where f = Abs_star], auto, ultra) done lemma starfunCR: - "( *fcR* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = + "( *fcR* f) (Abs_star(starrel``{%n. X n})) = Abs_star(starrel `` {%n. f (X n)})" apply (simp add: starfunCR_def) apply (rule arg_cong [where f = Abs_star]) -apply (auto iff add: hcomplexrel_iff, ultra) +apply (auto iff add: starrel_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 (rule_tac z = z in eq_Abs_star) apply (auto simp add: starfunC hcomplex_mult) done declare starfunC_mult [symmetric, simp] @@ -258,7 +258,7 @@ 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 (rule_tac z = z in eq_Abs_star) apply (simp add: starfunCR hypreal_mult) done declare starfunCR_mult [symmetric, simp] @@ -266,7 +266,7 @@ (** 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 (rule_tac z = z in eq_Abs_star) apply (simp add: starfunC hcomplex_add) done declare starfunC_add [symmetric, simp] @@ -278,14 +278,14 @@ 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 (rule_tac z = z in eq_Abs_star) 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 (rule_tac z = x in eq_Abs_star) apply (simp add: starfunC hcomplex_minus) done @@ -295,7 +295,7 @@ done lemma starfunCR_minus [simp]: "( *fcR* (%x. - f x)) x = - ( *fcR* f) x" -apply (rule_tac z = x in eq_Abs_hcomplex) +apply (rule_tac z = x in eq_Abs_star) apply (simp add: starfunCR hypreal_minus) done @@ -319,7 +319,7 @@ 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 (rule_tac z = x in eq_Abs_star) apply (simp add: starfunC) done @@ -336,7 +336,7 @@ 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 (rule_tac z = x in eq_Abs_star) apply (simp add: starfunCR starfun) done @@ -347,22 +347,22 @@ by (simp add: o_def starfun_starfunCR_o2) lemma starfunC_const_fun [simp]: "( *fc* (%x. k)) z = hcomplex_of_complex k" -apply (cases z) -apply (simp add: starfunC hcomplex_of_complex_def) +apply (rule_tac z=z in eq_Abs_star) +apply (simp add: starfunC hcomplex_of_complex_def star_of_def star_n_def) done lemma starfunRC_const_fun [simp]: "( *fRc* (%x. k)) z = hcomplex_of_complex k" apply (rule_tac z=z in eq_Abs_star) -apply (simp add: starfunRC hcomplex_of_complex_def) +apply (simp add: starfunRC hcomplex_of_complex_def star_of_def star_n_def) done lemma starfunCR_const_fun [simp]: "( *fcR* (%x. k)) z = hypreal_of_real k" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: starfunCR hypreal_of_real_def star_of_def star_n_def) done lemma starfunC_inverse: "inverse (( *fc* f) x) = ( *fc* (%x. inverse (f x))) x" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: starfunC hcomplex_inverse) done declare starfunC_inverse [symmetric, simp] @@ -376,14 +376,14 @@ lemma starfunCR_inverse: "inverse (( *fcR* f) x) = ( *fcR* (%x. inverse (f x))) x" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) 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) +by (simp add: starfunC hcomplex_of_complex_def star_of_def star_n_def) lemma starfunRC_eq [simp]: "( *fRc* f) (hypreal_of_real a) = hcomplex_of_complex (f a)" @@ -410,20 +410,20 @@ *) lemma starfunC_hcpow: "( *fc* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n" -apply (cases Z) +apply (rule_tac z=Z in eq_Abs_star) 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 (cases y) -apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) +apply (rule_tac z=y in eq_Abs_star) +apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add star_of_def star_n_def) done lemma starfunCR_lambda_cancel: "( *fcR* (%h. f (x + h))) y = ( *fcR* f) (hcomplex_of_complex x + y)" -apply (cases y) -apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) +apply (rule_tac z=y in eq_Abs_star) +apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add star_of_def star_n_def) done lemma starfunRC_lambda_cancel: @@ -434,14 +434,14 @@ lemma starfunC_lambda_cancel2: "( *fc* (%h. f(g(x + h)))) y = ( *fc* (f o g)) (hcomplex_of_complex x + y)" -apply (cases y) -apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add) +apply (rule_tac z=y in eq_Abs_star) +apply (simp add: starfunC hcomplex_of_complex_def hcomplex_add star_of_def star_n_def) done lemma starfunCR_lambda_cancel2: "( *fcR* (%h. f(g(x + h)))) y = ( *fcR* (f o g)) (hcomplex_of_complex x + y)" -apply (cases y) -apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add) +apply (rule_tac z=y in eq_Abs_star) +apply (simp add: starfunCR hcomplex_of_complex_def hcomplex_add star_of_def star_n_def) done lemma starfunRC_lambda_cancel2: @@ -488,12 +488,12 @@ lemma starfunCR_cmod: "*fcR* cmod = hcmod" apply (rule ext) -apply (rule_tac z = x in eq_Abs_hcomplex) +apply (rule_tac z = x in eq_Abs_star) apply (simp add: starfunCR hcmod) done lemma starfunC_inverse_inverse: "( *fc* inverse) x = inverse(x)" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: starfunC hcomplex_inverse) done @@ -515,22 +515,22 @@ subsection{*Internal Functions - Some Redundancy With *Fc* Now*} lemma starfunC_n_congruent: - "(%X. hcomplexrel``{%n. f n (X n)}) respects hcomplexrel" -by (auto simp add: congruent_def hcomplexrel_iff, ultra) + "(%X. starrel``{%n. f n (X n)}) respects starrel" +by (auto simp add: congruent_def starrel_iff, ultra) lemma starfunC_n: - "( *fcn* f) (Abs_hcomplex(hcomplexrel``{%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. f n (X n)})" + "( *fcn* f) (Abs_star(starrel``{%n. X n})) = + Abs_star(starrel `` {%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) +apply (rule arg_cong [where f = Abs_star]) +apply (auto iff add: starrel_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 (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: starfunC_n hcomplex_mult) done @@ -538,14 +538,14 @@ lemma starfunC_n_add: "( *fcn* f) z + ( *fcn* g) z = ( *fcn* (%i x. f i x + g i x)) z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: starfunC_n hcomplex_add) done (** uminus **) lemma starfunC_n_minus: "- ( *fcn* g) z = ( *fcn* (%i x. - g i x)) z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: starfunC_n hcomplex_minus) done @@ -559,19 +559,19 @@ lemma starfunC_n_const_fun [simp]: "( *fcn* (%i x. k)) z = hcomplex_of_complex k" -apply (cases z) -apply (simp add: starfunC_n hcomplex_of_complex_def) +apply (rule_tac z=z in eq_Abs_star) +apply (simp add: starfunC_n hcomplex_of_complex_def star_of_def star_n_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) + "( *fcn* f) (hcomplex_of_complex n) = Abs_star(starrel `` {%i. f i n})" +by (simp add: starfunC_n hcomplex_of_complex_def star_of_def star_n_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) +apply (simp add: starfunC hcomplex_of_complex_def star_of_def star_n_def) done lemma starfunRC_eq_iff: "(( *fRc* f) = ( *fRc* g)) = (f = g)" @@ -591,25 +591,25 @@ 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 (cases x, cases z) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=z in eq_Abs_star) 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 (cases x, cases z) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=z in eq_Abs_star) 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 (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: starfunC) done lemma starfunC_Id [simp]: "( *fc* (%x. x)) x = x" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: starfunC) done diff -r c6eecde058e4 -r 5798fbf42a6a src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Wed Sep 07 00:48:50 2005 +0200 +++ b/src/HOL/Complex/NSCA.thy Wed Sep 07 01:49:49 2005 +0200 @@ -134,7 +134,7 @@ lemma SComplex_hcmod_SReal: "z \ SComplex ==> hcmod z \ Reals" apply (simp add: SComplex_def SReal_def) -apply (rule_tac z = z in eq_Abs_hcomplex) +apply (rule_tac z = z in eq_Abs_star) apply (auto simp add: hcmod hypreal_of_real_def star_of_def star_n_def hcomplex_of_complex_def cmod_def) apply (rule_tac x = "cmod r" in exI) apply (simp add: cmod_def, ultra) @@ -144,7 +144,7 @@ by (simp add: SComplex_def hcomplex_of_complex_zero_iff) lemma SComplex_one [simp]: "1 \ SComplex" -by (simp add: SComplex_def hcomplex_of_complex_def hcomplex_one_def) +by (simp add: SComplex_def hcomplex_of_complex_def star_of_def star_n_def hypreal_one_def) (* Goalw [SComplex_def,SReal_def] "hcmod z \ Reals ==> z \ SComplex" @@ -659,7 +659,7 @@ by (blast intro: SComplex_capprox_iff [THEN iffD1] capprox_trans2) lemma hcomplex_capproxD1: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) + "Abs_star(starrel ``{%n. X n}) @c= Abs_star(starrel``{%n. Y n}) ==> Abs_star(starrel `` {%n. Re(X n)}) @= Abs_star(starrel `` {%n. Re(Y n)})" apply (auto simp add: approx_FreeUltrafilterNat_iff) @@ -678,7 +678,7 @@ (* same proof *) lemma hcomplex_capproxD2: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n}) + "Abs_star(starrel ``{%n. X n}) @c= Abs_star(starrel``{%n. Y n}) ==> Abs_star(starrel `` {%n. Im(X n)}) @= Abs_star(starrel `` {%n. Im(Y n)})" apply (auto simp add: approx_FreeUltrafilterNat_iff) @@ -699,7 +699,7 @@ Abs_star(starrel `` {%n. Re(Y n)}); Abs_star(starrel `` {%n. Im(X n)}) @= Abs_star(starrel `` {%n. Im(Y n)}) - |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})" + |] ==> Abs_star(starrel ``{%n. X n}) @c= Abs_star(starrel``{%n. Y n})" apply (drule approx_minus_iff [THEN iffD1]) apply (drule approx_minus_iff [THEN iffD1]) apply (rule capprox_minus_iff [THEN iffD2]) @@ -718,7 +718,7 @@ done lemma capprox_approx_iff: - "(Abs_hcomplex(hcomplexrel ``{%n. X n}) @c= Abs_hcomplex(hcomplexrel``{%n. Y n})) = + "(Abs_star(starrel ``{%n. X n}) @c= Abs_star(starrel``{%n. Y n})) = (Abs_star(starrel `` {%n. Re(X n)}) @= Abs_star(starrel `` {%n. Re(Y n)}) & Abs_star(starrel `` {%n. Im(X n)}) @= Abs_star(starrel `` {%n. Im(Y n)}))" apply (blast intro: hcomplex_capproxI hcomplex_capproxD1 hcomplex_capproxD2) @@ -731,7 +731,7 @@ done lemma CFinite_HFinite_Re: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CFinite + "Abs_star(starrel ``{%n. X n}) \ CFinite ==> Abs_star(starrel `` {%n. Re(X n)}) \ HFinite" apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rule bexI, rule_tac [2] lemma_starrel_refl) @@ -745,7 +745,7 @@ done lemma CFinite_HFinite_Im: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CFinite + "Abs_star(starrel ``{%n. X n}) \ CFinite ==> Abs_star(starrel `` {%n. Im(X n)}) \ HFinite" apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rule bexI, rule_tac [2] lemma_starrel_refl) @@ -760,7 +760,7 @@ lemma HFinite_Re_Im_CFinite: "[| Abs_star(starrel `` {%n. Re(X n)}) \ HFinite; Abs_star(starrel `` {%n. Im(X n)}) \ HFinite - |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CFinite" + |] ==> Abs_star(starrel ``{%n. X n}) \ CFinite" apply (auto simp add: CFinite_hcmod_iff hcmod HFinite_FreeUltrafilterNat_iff) apply (rename_tac Y Z u v) apply (rule bexI, rule_tac [2] lemma_starrel_refl) @@ -778,20 +778,20 @@ done lemma CFinite_HFinite_iff: - "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CFinite) = + "(Abs_star(starrel ``{%n. X n}) \ CFinite) = (Abs_star(starrel `` {%n. Re(X n)}) \ HFinite & Abs_star(starrel `` {%n. Im(X n)}) \ HFinite)" by (blast intro: HFinite_Re_Im_CFinite CFinite_HFinite_Im CFinite_HFinite_Re) lemma SComplex_Re_SReal: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) \ SComplex + "Abs_star(starrel ``{%n. X n}) \ SComplex ==> Abs_star(starrel `` {%n. Re(X n)}) \ Reals" apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def) apply (rule_tac x = "Re r" in exI, ultra) done lemma SComplex_Im_SReal: - "Abs_hcomplex(hcomplexrel ``{%n. X n}) \ SComplex + "Abs_star(starrel ``{%n. X n}) \ SComplex ==> Abs_star(starrel `` {%n. Im(X n)}) \ Reals" apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def) apply (rule_tac x = "Im r" in exI, ultra) @@ -800,40 +800,40 @@ lemma Reals_Re_Im_SComplex: "[| Abs_star(starrel `` {%n. Re(X n)}) \ Reals; Abs_star(starrel `` {%n. Im(X n)}) \ Reals - |] ==> Abs_hcomplex(hcomplexrel ``{%n. X n}) \ SComplex" + |] ==> Abs_star(starrel ``{%n. X n}) \ SComplex" apply (auto simp add: SComplex_def hcomplex_of_complex_def SReal_def hypreal_of_real_def star_of_def star_n_def) apply (rule_tac x = "Complex r ra" in exI, ultra) done lemma SComplex_SReal_iff: - "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \ SComplex) = + "(Abs_star(starrel ``{%n. X n}) \ SComplex) = (Abs_star(starrel `` {%n. Re(X n)}) \ Reals & Abs_star(starrel `` {%n. Im(X n)}) \ Reals)" by (blast intro: SComplex_Re_SReal SComplex_Im_SReal Reals_Re_Im_SComplex) lemma CInfinitesimal_Infinitesimal_iff: - "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CInfinitesimal) = + "(Abs_star(starrel ``{%n. X n}) \ CInfinitesimal) = (Abs_star(starrel `` {%n. Re(X n)}) \ Infinitesimal & Abs_star(starrel `` {%n. Im(X n)}) \ Infinitesimal)" by (simp add: mem_cinfmal_iff mem_infmal_iff hcomplex_zero_num hypreal_zero_num capprox_approx_iff) -lemma eq_Abs_hcomplex_EX: - "(\t. P t) = (\X. P (Abs_hcomplex(hcomplexrel `` {X})))" +lemma eq_Abs_star_EX: + "(\t. P t) = (\X. P (Abs_star(starrel `` {X})))" apply auto -apply (rule_tac z = t in eq_Abs_hcomplex, auto) +apply (rule_tac z = t in eq_Abs_star, auto) done -lemma eq_Abs_hcomplex_Bex: - "(\t \ A. P t) = (\X. (Abs_hcomplex(hcomplexrel `` {X})) \ A & - P (Abs_hcomplex(hcomplexrel `` {X})))" +lemma eq_Abs_star_Bex: + "(\t \ A. P t) = (\X. (Abs_star(starrel `` {X})) \ A & + P (Abs_star(starrel `` {X})))" apply auto -apply (rule_tac z = t in eq_Abs_hcomplex, auto) +apply (rule_tac z = t in eq_Abs_star, auto) done (* Here we go - easy proof now!! *) lemma stc_part_Ex: "x:CFinite ==> \t \ SComplex. x @c= t" -apply (rule_tac z = x in eq_Abs_hcomplex) -apply (auto simp add: CFinite_HFinite_iff eq_Abs_hcomplex_Bex SComplex_SReal_iff capprox_approx_iff) +apply (rule_tac z = x in eq_Abs_star) +apply (auto simp add: CFinite_HFinite_iff eq_Abs_star_Bex SComplex_SReal_iff capprox_approx_iff) apply (drule st_part_Ex, safe)+ apply (rule_tac z = t in eq_Abs_star) apply (rule_tac z = ta in eq_Abs_star, auto) @@ -1171,7 +1171,7 @@ by (simp add: CInfinitesimal_hcmod_iff) lemma CInfinite_HInfinite_iff: - "(Abs_hcomplex(hcomplexrel ``{%n. X n}) \ CInfinite) = + "(Abs_star(starrel ``{%n. X n}) \ CInfinite) = (Abs_star(starrel `` {%n. Re(X n)}) \ HInfinite | Abs_star(starrel `` {%n. Im(X n)}) \ HInfinite)" by (simp add: CInfinite_CFinite_iff HInfinite_HFinite_iff CFinite_HFinite_iff) @@ -1216,8 +1216,8 @@ lemma complex_seq_to_hcomplex_CInfinitesimal: "\n. cmod (X n - x) < inverse (real (Suc n)) ==> - Abs_hcomplex(hcomplexrel``{X}) - hcomplex_of_complex x \ CInfinitesimal" -apply (simp add: hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def Infinitesimal_FreeUltrafilterNat_iff hcmod) + Abs_star(starrel``{X}) - hcomplex_of_complex x \ CInfinitesimal" +apply (simp add: hcomplex_diff CInfinitesimal_hcmod_iff hcomplex_of_complex_def star_of_def star_n_def Infinitesimal_FreeUltrafilterNat_iff hcmod) apply (rule bexI, auto) apply (auto dest: FreeUltrafilterNat_inverse_real_of_posnat FreeUltrafilterNat_all FreeUltrafilterNat_Int intro: order_less_trans FreeUltrafilterNat_subset) done @@ -1384,7 +1384,7 @@ val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex"; val SComplex_SReal_iff = thm "SComplex_SReal_iff"; val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff"; -val eq_Abs_hcomplex_Bex = thm "eq_Abs_hcomplex_Bex"; +val eq_Abs_star_Bex = thm "eq_Abs_star_Bex"; val stc_part_Ex = thm "stc_part_Ex"; val stc_part_Ex1 = thm "stc_part_Ex1"; val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty"; diff -r c6eecde058e4 -r 5798fbf42a6a src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Wed Sep 07 00:48:50 2005 +0200 +++ b/src/HOL/Complex/NSComplex.thy Wed Sep 07 01:49:49 2005 +0200 @@ -11,6 +11,8 @@ imports Complex begin +types hcomplex = "complex star" +(* constdefs hcomplexrel :: "((nat=>complex)*(nat=>complex)) set" "hcomplexrel == {p. \X Y. p = ((X::nat=>complex),Y) & @@ -39,54 +41,56 @@ hcinv_def: "inverse(P) == Abs_hcomplex(UN X: Rep_hcomplex(P). hcomplexrel `` {%n. inverse(X n)})" +*) constdefs hcomplex_of_complex :: "complex => hcomplex" - "hcomplex_of_complex z == Abs_hcomplex(hcomplexrel `` {%n. z})" +(* "hcomplex_of_complex z == Abs_star(starrel `` {%n. z})"*) + "hcomplex_of_complex z == star_of z" (*--- real and Imaginary parts ---*) hRe :: "hcomplex => hypreal" - "hRe(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Re (X n)})" + "hRe(z) == Abs_star(UN X:Rep_star(z). starrel `` {%n. Re (X n)})" hIm :: "hcomplex => hypreal" - "hIm(z) == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. Im (X n)})" + "hIm(z) == Abs_star(UN X:Rep_star(z). starrel `` {%n. Im (X n)})" (*----------- modulus ------------*) hcmod :: "hcomplex => hypreal" - "hcmod z == Abs_star(UN X: Rep_hcomplex(z). + "hcmod z == Abs_star(UN X: Rep_star(z). starrel `` {%n. cmod (X n)})" (*------ imaginary unit ----------*) iii :: hcomplex - "iii == Abs_hcomplex(hcomplexrel `` {%n. ii})" + "iii == Abs_star(starrel `` {%n. ii})" (*------- complex conjugate ------*) hcnj :: "hcomplex => hcomplex" - "hcnj z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. cnj (X n)})" + "hcnj z == Abs_star(UN X:Rep_star(z). starrel `` {%n. cnj (X n)})" (*------------ Argand -------------*) hsgn :: "hcomplex => hcomplex" - "hsgn z == Abs_hcomplex(UN X:Rep_hcomplex(z). hcomplexrel `` {%n. sgn(X n)})" + "hsgn z == Abs_star(UN X:Rep_star(z). starrel `` {%n. sgn(X n)})" harg :: "hcomplex => hypreal" - "harg z == Abs_star(UN X:Rep_hcomplex(z). starrel `` {%n. arg(X n)})" + "harg z == Abs_star(UN X:Rep_star(z). starrel `` {%n. arg(X n)})" (* abbreviation for (cos a + i sin a) *) hcis :: "hypreal => hcomplex" - "hcis a == Abs_hcomplex(UN X:Rep_star(a). hcomplexrel `` {%n. cis (X n)})" + "hcis a == Abs_star(UN X:Rep_star(a). starrel `` {%n. cis (X n)})" (*----- injection from hyperreals -----*) hcomplex_of_hypreal :: "hypreal => hcomplex" - "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_star(r). - hcomplexrel `` {%n. complex_of_real (X n)})" + "hcomplex_of_hypreal r == Abs_star(UN X:Rep_star(r). + starrel `` {%n. complex_of_real (X n)})" (* abbreviation for r*(cos a + i sin a) *) hrcis :: "[hypreal, hypreal] => hcomplex" @@ -102,22 +106,22 @@ HComplex :: "[hypreal,hypreal] => hcomplex" "HComplex x y == hcomplex_of_hypreal x + iii * hcomplex_of_hypreal y" - +(* defs (overloaded) - +*) (*----------- division ----------*) - +(* hcomplex_divide_def: "w / (z::hcomplex) == w * inverse z" hcomplex_add_def: - "w + z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z). - hcomplexrel `` {%n. X n + Y n})" + "w + z == Abs_star(UN X:Rep_star(w). UN Y:Rep_star(z). + starrel `` {%n. X n + Y n})" hcomplex_mult_def: - "w * z == Abs_hcomplex(UN X:Rep_hcomplex(w). UN Y:Rep_hcomplex(z). - hcomplexrel `` {%n. X n * Y n})" - + "w * z == Abs_star(UN X:Rep_star(w). UN Y:Rep_star(z). + starrel `` {%n. X n * Y n})" +*) consts @@ -127,83 +131,32 @@ (* hypernatural powers of nonstandard complex numbers *) hcpow_def: "(z::hcomplex) hcpow (n::hypnat) - == Abs_hcomplex(UN X:Rep_hcomplex(z). UN Y: Rep_star(n). - hcomplexrel `` {%n. (X n) ^ (Y n)})" - - -lemma hcomplexrel_refl: "(x,x): hcomplexrel" -by (simp add: hcomplexrel_def) - -lemma hcomplexrel_sym: "(x,y): hcomplexrel ==> (y,x):hcomplexrel" -by (auto simp add: hcomplexrel_def eq_commute) - -lemma hcomplexrel_trans: - "[|(x,y): hcomplexrel; (y,z):hcomplexrel|] ==> (x,z):hcomplexrel" -by (simp add: hcomplexrel_def, ultra) - -lemma equiv_hcomplexrel: "equiv UNIV hcomplexrel" -apply (simp add: equiv_def refl_def sym_def trans_def hcomplexrel_refl) -apply (blast intro: hcomplexrel_sym hcomplexrel_trans) -done - -lemmas equiv_hcomplexrel_iff = - eq_equiv_class_iff [OF equiv_hcomplexrel UNIV_I UNIV_I, simp] - -lemma hcomplexrel_in_hcomplex [simp]: "hcomplexrel``{x} : hcomplex" -by (simp add: hcomplex_def hcomplexrel_def quotient_def, blast) - -declare Abs_hcomplex_inject [simp] Abs_hcomplex_inverse [simp] -declare equiv_hcomplexrel [THEN eq_equiv_class_iff, simp] - -lemma lemma_hcomplexrel_refl [simp]: "x: hcomplexrel `` {x}" -by (simp add: hcomplexrel_def) - -lemma hcomplex_empty_not_mem [simp]: "{} \ hcomplex" -apply (simp add: hcomplex_def hcomplexrel_def) -apply (auto elim!: quotientE) -done - -lemma Rep_hcomplex_nonempty [simp]: "Rep_hcomplex x \ {}" -by (cut_tac x = x in Rep_hcomplex, auto) - -lemma eq_Abs_hcomplex: - "(!!x. z = Abs_hcomplex(hcomplexrel `` {x}) ==> P) ==> P" -apply (rule_tac x1=z in Rep_hcomplex [unfolded hcomplex_def, THEN quotientE]) -apply (drule_tac f = Abs_hcomplex in arg_cong) -apply (force simp add: Rep_hcomplex_inverse hcomplexrel_def) -done - -theorem hcomplex_cases [case_names Abs_hcomplex, cases type: hcomplex]: - "(!!x. z = Abs_hcomplex(hcomplexrel``{x}) ==> P) ==> P" -by (rule eq_Abs_hcomplex [of z], blast) - -lemma hcomplexrel_iff [simp]: - "((X,Y): hcomplexrel) = ({n. X n = Y n}: FreeUltrafilterNat)" -by (simp add: hcomplexrel_def) + == Abs_star(UN X:Rep_star(z). UN Y: Rep_star(n). + starrel `` {%n. (X n) ^ (Y n)})" subsection{*Properties of Nonstandard Real and Imaginary Parts*} lemma hRe: - "hRe(Abs_hcomplex (hcomplexrel `` {X})) = + "hRe(Abs_star (starrel `` {X})) = Abs_star(starrel `` {%n. Re(X n)})" apply (simp add: hRe_def) apply (rule_tac f = Abs_star in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (auto iff: starrel_iff, ultra) done lemma hIm: - "hIm(Abs_hcomplex (hcomplexrel `` {X})) = + "hIm(Abs_star (starrel `` {X})) = Abs_star(starrel `` {%n. Im(X n)})" apply (simp add: hIm_def) apply (rule_tac f = Abs_star in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (auto iff: starrel_iff, ultra) done lemma hcomplex_hRe_hIm_cancel_iff: "(w=z) = (hRe(w) = hRe(z) & hIm(w) = hIm(z))" -apply (cases z, cases w) -apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: hcomplexrel_iff) +apply (rule_tac z=z in eq_Abs_star, rule_tac z=w in eq_Abs_star) +apply (auto simp add: hRe hIm complex_Re_Im_cancel_iff iff: starrel_iff) apply (ultra+) done @@ -211,121 +164,94 @@ by (simp add: hcomplex_hRe_hIm_cancel_iff) lemma hcomplex_hRe_zero [simp]: "hRe 0 = 0" -by (simp add: hcomplex_zero_def hRe hypreal_zero_num) +by (simp add: hRe hypreal_zero_num) lemma hcomplex_hIm_zero [simp]: "hIm 0 = 0" -by (simp add: hcomplex_zero_def hIm hypreal_zero_num) +by (simp add: hIm hypreal_zero_num) lemma hcomplex_hRe_one [simp]: "hRe 1 = 1" -by (simp add: hcomplex_one_def hRe hypreal_one_num) +by (simp add: hRe hypreal_one_num) lemma hcomplex_hIm_one [simp]: "hIm 1 = 0" -by (simp add: hcomplex_one_def hIm hypreal_one_def hypreal_zero_num) +by (simp add: hIm hypreal_one_def hypreal_zero_num) subsection{*Addition for Nonstandard Complex Numbers*} - +(* lemma hcomplex_add_congruent2: - "congruent2 hcomplexrel hcomplexrel (%X Y. hcomplexrel `` {%n. X n + Y n})" -by (auto simp add: congruent2_def iff: hcomplexrel_iff, ultra) - + "congruent2 starrel starrel (%X Y. starrel `` {%n. X n + Y n})" +by (auto simp add: congruent2_def iff: starrel_iff, ultra) +*) lemma hcomplex_add: - "Abs_hcomplex(hcomplexrel``{%n. X n}) + - Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n + Y n})" -apply (simp add: hcomplex_add_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto simp add: iff: hcomplexrel_iff, ultra) -done + "Abs_star(starrel``{%n. X n}) + + Abs_star(starrel``{%n. Y n}) = + Abs_star(starrel``{%n. X n + Y n})" +by (rule hypreal_add) lemma hcomplex_add_commute: "(z::hcomplex) + w = w + z" -apply (cases z, cases w) -apply (simp add: complex_add_commute hcomplex_add) -done +by (rule add_commute) lemma hcomplex_add_assoc: "((z1::hcomplex) + z2) + z3 = z1 + (z2 + z3)" -apply (cases z1, cases z2, cases z3) -apply (simp add: hcomplex_add complex_add_assoc) -done +by (rule add_assoc) lemma hcomplex_add_zero_left: "(0::hcomplex) + z = z" -apply (cases z) -apply (simp add: hcomplex_zero_def hcomplex_add) -done +by simp lemma hcomplex_add_zero_right: "z + (0::hcomplex) = z" -by (simp add: hcomplex_add_zero_left hcomplex_add_commute) +by simp lemma hRe_add: "hRe(x + y) = hRe(x) + hRe(y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hRe hcomplex_add hypreal_add complex_Re_add) done lemma hIm_add: "hIm(x + y) = hIm(x) + hIm(y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hIm hcomplex_add hypreal_add complex_Im_add) done subsection{*Additive Inverse on Nonstandard Complex Numbers*} - +(* lemma hcomplex_minus_congruent: - "(%X. hcomplexrel `` {%n. - (X n)}) respects hcomplexrel" + "(%X. starrel `` {%n. - (X n)}) respects starrel" by (simp add: congruent_def) - +*) lemma hcomplex_minus: - "- (Abs_hcomplex(hcomplexrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. -(X n)})" -apply (simp add: hcomplex_minus_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) -done + "- (Abs_star(starrel `` {%n. X n})) = + Abs_star(starrel `` {%n. -(X n)})" +by (rule hypreal_minus) lemma hcomplex_add_minus_left: "-z + z = (0::hcomplex)" -apply (cases z) -apply (simp add: hcomplex_add hcomplex_minus hcomplex_zero_def) -done +by simp subsection{*Multiplication for Nonstandard Complex Numbers*} lemma hcomplex_mult: - "Abs_hcomplex(hcomplexrel``{%n. X n}) * - Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n * Y n})" -apply (simp add: hcomplex_mult_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) -done + "Abs_star(starrel``{%n. X n}) * + Abs_star(starrel``{%n. Y n}) = + Abs_star(starrel``{%n. X n * Y n})" +by (rule hypreal_mult) lemma hcomplex_mult_commute: "(w::hcomplex) * z = z * w" -apply (cases w, cases z) -apply (simp add: hcomplex_mult complex_mult_commute) -done +by (rule mult_commute) lemma hcomplex_mult_assoc: "((u::hcomplex) * v) * w = u * (v * w)" -apply (cases u, cases v, cases w) -apply (simp add: hcomplex_mult complex_mult_assoc) -done +by (rule mult_assoc) lemma hcomplex_mult_one_left: "(1::hcomplex) * z = z" -apply (cases z) -apply (simp add: hcomplex_one_def hcomplex_mult) -done +by (rule mult_1_left) lemma hcomplex_mult_zero_left: "(0::hcomplex) * z = 0" -apply (cases z) -apply (simp add: hcomplex_zero_def hcomplex_mult) -done +by (rule mult_zero_left) lemma hcomplex_add_mult_distrib: "((z1::hcomplex) + z2) * w = (z1 * w) + (z2 * w)" -apply (cases z1, cases z2, cases w) -apply (simp add: hcomplex_mult hcomplex_add left_distrib) -done +by (rule left_distrib) lemma hcomplex_zero_not_eq_one: "(0::hcomplex) \ (1::hcomplex)" -by (simp add: hcomplex_zero_def hcomplex_one_def) +by (rule zero_neq_one) declare hcomplex_zero_not_eq_one [THEN not_sym, simp] @@ -333,23 +259,22 @@ subsection{*Inverse of Nonstandard Complex Number*} lemma hcomplex_inverse: - "inverse (Abs_hcomplex(hcomplexrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. inverse (X n)})" -apply (simp add: hcinv_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) + "inverse (Abs_star(starrel `` {%n. X n})) = + Abs_star(starrel `` {%n. inverse (X n)})" +apply (fold star_n_def) +apply (simp add: star_inverse_def Ifun_of_def star_of_def Ifun_star_n) done lemma hcomplex_mult_inv_left: "z \ (0::hcomplex) ==> inverse(z) * z = (1::hcomplex)" -apply (cases z) -apply (simp add: hcomplex_zero_def hcomplex_one_def hcomplex_inverse hcomplex_mult, ultra) +apply (rule_tac z=z in eq_Abs_star) +apply (simp add: hypreal_zero_def hypreal_one_def hcomplex_inverse hcomplex_mult, ultra) apply (rule ccontr) apply (drule left_inverse, auto) done subsection {* The Field of Nonstandard Complex Numbers *} - +(* instance hcomplex :: field proof fix z u v w :: hcomplex @@ -385,17 +310,17 @@ show "inverse 0 = (0::hcomplex)" by (simp add: hcomplex_inverse hcomplex_zero_def) qed - +*) subsection{*More Minus Laws*} lemma hRe_minus: "hRe(-z) = - hRe(z)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hRe hcomplex_minus hypreal_minus complex_Re_minus) done lemma hIm_minus: "hIm(-z) = - hIm(z)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hIm hcomplex_minus hypreal_minus complex_Im_minus) done @@ -406,13 +331,13 @@ done lemma hcomplex_i_mult_eq [simp]: "iii * iii = - 1" -by (simp add: iii_def hcomplex_mult hcomplex_one_def hcomplex_minus) +by (simp add: iii_def hcomplex_mult hypreal_one_def hcomplex_minus) lemma hcomplex_i_mult_left [simp]: "iii * (iii * z) = -z" by (simp add: mult_assoc [symmetric]) lemma hcomplex_i_not_zero [simp]: "iii \ 0" -by (simp add: iii_def hcomplex_zero_def) +by (simp add: iii_def hypreal_zero_def) subsection{*More Multiplication Laws*} @@ -438,9 +363,9 @@ subsection{*Subraction and Division*} lemma hcomplex_diff: - "Abs_hcomplex(hcomplexrel``{%n. X n}) - Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n - Y n})" -by (simp add: hcomplex_diff_def hcomplex_minus hcomplex_add complex_diff_def) + "Abs_star(starrel``{%n. X n}) - Abs_star(starrel``{%n. Y n}) = + Abs_star(starrel``{%n. X n - Y n})" +by (rule hypreal_diff) lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" by (rule OrderedGroup.diff_eq_eq) @@ -453,9 +378,9 @@ lemma hcomplex_of_hypreal: "hcomplex_of_hypreal (Abs_star(starrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. complex_of_real (X n)})" + Abs_star(starrel `` {%n. complex_of_real (X n)})" apply (simp add: hcomplex_of_hypreal_def) -apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra) +apply (rule_tac f = Abs_star in arg_cong, auto iff: starrel_iff, ultra) done lemma hcomplex_of_hypreal_cancel_iff [iff]: @@ -465,10 +390,10 @@ done lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" -by (simp add: hcomplex_one_def hcomplex_of_hypreal hypreal_one_num) +by (simp add: hypreal_one_def hcomplex_of_hypreal hypreal_one_num) lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0" -by (simp add: hcomplex_zero_def hypreal_zero_def hcomplex_of_hypreal) +by (simp add: hypreal_zero_def hypreal_zero_def hcomplex_of_hypreal) lemma hcomplex_of_hypreal_minus [simp]: "hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" @@ -491,7 +416,7 @@ lemma hcomplex_of_hypreal_diff [simp]: "hcomplex_of_hypreal (x - y) = hcomplex_of_hypreal x - hcomplex_of_hypreal y " -by (simp add: hcomplex_diff_def hypreal_diff_def) +by (simp add: hypreal_diff_def) lemma hcomplex_of_hypreal_mult [simp]: "hcomplex_of_hypreal (x * y) = hcomplex_of_hypreal x * hcomplex_of_hypreal y" @@ -501,10 +426,7 @@ lemma hcomplex_of_hypreal_divide [simp]: "hcomplex_of_hypreal(x/y) = hcomplex_of_hypreal x / hcomplex_of_hypreal y" -apply (simp add: hcomplex_divide_def) -apply (case_tac "y=0", simp) -apply (simp add: hypreal_divide_def) -done +by (simp add: divide_inverse) lemma hRe_hcomplex_of_hypreal [simp]: "hRe(hcomplex_of_hypreal z) = z" apply (rule_tac z=z in eq_Abs_star) @@ -518,7 +440,7 @@ lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal epsilon \ 0" -by (auto simp add: hcomplex_of_hypreal epsilon_def star_n_def hcomplex_zero_def) +by (auto simp add: hcomplex_of_hypreal epsilon_def star_n_def hypreal_zero_def) subsection{*HComplex theorems*} @@ -534,15 +456,15 @@ done text{*Relates the two nonstandard constructions*} -lemma HComplex_eq_Abs_hcomplex_Complex: +lemma HComplex_eq_Abs_star_Complex: "HComplex (Abs_star (starrel `` {X})) (Abs_star (starrel `` {Y})) = - Abs_hcomplex(hcomplexrel `` {%n::nat. Complex (X n) (Y n)})"; + Abs_star(starrel `` {%n::nat. Complex (X n) (Y n)})"; by (simp add: hcomplex_hRe_hIm_cancel_iff hRe hIm) lemma hcomplex_surj [simp]: "HComplex (hRe z) (hIm z) = z" by (simp add: hcomplex_equality) -lemma hcomplex_induct [case_names rect, induct type: hcomplex]: +lemma hcomplex_induct [case_names rect(*, induct type: hcomplex*)]: "(\x y. P (HComplex x y)) ==> P z" by (rule hcomplex_surj [THEN subst], blast) @@ -550,19 +472,19 @@ subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} lemma hcmod: - "hcmod (Abs_hcomplex(hcomplexrel `` {%n. X n})) = + "hcmod (Abs_star(starrel `` {%n. X n})) = Abs_star(starrel `` {%n. cmod (X n)})" apply (simp add: hcmod_def) apply (rule_tac f = Abs_star in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (auto iff: starrel_iff, ultra) done lemma hcmod_zero [simp]: "hcmod(0) = 0" -by (simp add: hcomplex_zero_def hypreal_zero_def hcmod) +by (simp add: hypreal_zero_def hypreal_zero_def hcmod) lemma hcmod_one [simp]: "hcmod(1) = 1" -by (simp add: hcomplex_one_def hcmod hypreal_one_num) +by (simp add: hypreal_one_def hcmod hypreal_one_num) lemma hcmod_hcomplex_of_hypreal [simp]: "hcmod(hcomplex_of_hypreal x) = abs x" apply (rule_tac z=x in eq_Abs_star) @@ -633,20 +555,20 @@ subsection{*Conjugation*} lemma hcnj: - "hcnj (Abs_hcomplex(hcomplexrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. cnj(X n)})" + "hcnj (Abs_star(starrel `` {%n. X n})) = + Abs_star(starrel `` {%n. cnj(X n)})" apply (simp add: hcnj_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (rule_tac f = Abs_star in arg_cong) +apply (auto iff: starrel_iff, ultra) done lemma hcomplex_hcnj_cancel_iff [iff]: "(hcnj x = hcnj y) = (x = y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcnj) done lemma hcomplex_hcnj_hcnj [simp]: "hcnj (hcnj z) = z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcnj) done @@ -657,52 +579,52 @@ done lemma hcomplex_hmod_hcnj [simp]: "hcmod (hcnj z) = hcmod z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcnj hcmod) done lemma hcomplex_hcnj_minus: "hcnj (-z) = - hcnj z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcnj hcomplex_minus complex_cnj_minus) done lemma hcomplex_hcnj_inverse: "hcnj(inverse z) = inverse(hcnj z)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcnj hcomplex_inverse complex_cnj_inverse) done lemma hcomplex_hcnj_add: "hcnj(w + z) = hcnj(w) + hcnj(z)" -apply (cases z, cases w) +apply (rule_tac z=z in eq_Abs_star, rule_tac z=w in eq_Abs_star) apply (simp add: hcnj hcomplex_add complex_cnj_add) done lemma hcomplex_hcnj_diff: "hcnj(w - z) = hcnj(w) - hcnj(z)" -apply (cases z, cases w) +apply (rule_tac z=z in eq_Abs_star, rule_tac z=w in eq_Abs_star) apply (simp add: hcnj hcomplex_diff complex_cnj_diff) done lemma hcomplex_hcnj_mult: "hcnj(w * z) = hcnj(w) * hcnj(z)" -apply (cases z, cases w) +apply (rule_tac z=z in eq_Abs_star, rule_tac z=w in eq_Abs_star) apply (simp add: hcnj hcomplex_mult complex_cnj_mult) done lemma hcomplex_hcnj_divide: "hcnj(w / z) = (hcnj w)/(hcnj z)" -by (simp add: hcomplex_divide_def hcomplex_hcnj_mult hcomplex_hcnj_inverse) +by (simp add: divide_inverse hcomplex_hcnj_mult hcomplex_hcnj_inverse) lemma hcnj_one [simp]: "hcnj 1 = 1" -by (simp add: hcomplex_one_def hcnj) +by (simp add: hypreal_one_def hcnj) lemma hcomplex_hcnj_zero [simp]: "hcnj 0 = 0" -by (simp add: hcomplex_zero_def hcnj) +by (simp add: hypreal_zero_def hcnj) lemma hcomplex_hcnj_zero_iff [iff]: "(hcnj z = 0) = (z = 0)" -apply (cases z) -apply (simp add: hcomplex_zero_def hcnj) +apply (rule_tac z=z in eq_Abs_star) +apply (simp add: hypreal_zero_def hcnj) done lemma hcomplex_mult_hcnj: "z * hcnj z = hcomplex_of_hypreal (hRe(z) ^ 2 + hIm(z) ^ 2)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcnj hcomplex_mult hcomplex_of_hypreal hRe hIm hypreal_add hypreal_mult complex_mult_cnj numeral_2_eq_2) done @@ -711,8 +633,8 @@ subsection{*More Theorems about the Function @{term hcmod}*} lemma hcomplex_hcmod_eq_zero_cancel [simp]: "(hcmod x = 0) = (x = 0)" -apply (cases x) -apply (simp add: hcmod hcomplex_zero_def hypreal_zero_num) +apply (rule_tac z=x in eq_Abs_star) +apply (simp add: hcmod hypreal_zero_def hypreal_zero_num) done lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: @@ -726,17 +648,17 @@ done lemma hcmod_minus [simp]: "hcmod (-x) = hcmod(x)" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: hcmod hcomplex_minus) done lemma hcmod_mult_hcnj: "hcmod(z * hcnj(z)) = hcmod(z) ^ 2" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hcmod hcomplex_mult hcnj hypreal_mult complex_mod_mult_cnj numeral_2_eq_2) done lemma hcmod_ge_zero [simp]: "(0::hypreal) \ hcmod x" -apply (cases x) +apply (rule_tac z=x in eq_Abs_star) apply (simp add: hcmod hypreal_zero_num hypreal_le) done @@ -744,13 +666,13 @@ by (simp add: abs_if linorder_not_less) lemma hcmod_mult: "hcmod(x*y) = hcmod(x) * hcmod(y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcomplex_mult hypreal_mult complex_mod_mult) done lemma hcmod_add_squared_eq: "hcmod(x + y) ^ 2 = hcmod(x) ^ 2 + hcmod(y) ^ 2 + 2 * hRe(x * hcnj y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcomplex_add hypreal_mult hRe hcnj hcomplex_mult numeral_2_eq_2 realpow_two [symmetric] del: realpow_Suc) @@ -761,7 +683,7 @@ done lemma hcomplex_hRe_mult_hcnj_le_hcmod [simp]: "hRe(x * hcnj y) \ hcmod(x * hcnj y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcnj hcomplex_mult hRe hypreal_le) done @@ -771,7 +693,7 @@ done lemma hcmod_triangle_squared [simp]: "hcmod (x + y) ^ 2 \ (hcmod(x) + hcmod(y)) ^ 2" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcnj hcomplex_add hypreal_mult hypreal_add hypreal_le realpow_two [symmetric] numeral_2_eq_2 del: realpow_Suc) @@ -779,7 +701,7 @@ done lemma hcmod_triangle_ineq [simp]: "hcmod (x + y) \ hcmod(x) + hcmod(y)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcomplex_add hypreal_add hypreal_le) done @@ -789,26 +711,28 @@ done lemma hcmod_diff_commute: "hcmod (x - y) = hcmod (y - x)" -apply (cases x, cases y) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) apply (simp add: hcmod hcomplex_diff complex_mod_diff_commute) done lemma hcmod_add_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" -apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) +apply (rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star) apply (simp add: hcmod hcomplex_add hypreal_add hypreal_less, ultra) apply (auto intro: complex_mod_add_less) done lemma hcmod_mult_less: "[| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" -apply (cases x, cases y, rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) +apply (rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star) apply (simp add: hcmod hypreal_mult hypreal_less hcomplex_mult, ultra) apply (auto intro: complex_mod_mult_less) done lemma hcmod_diff_ineq [simp]: "hcmod(a) - hcmod(b) \ hcmod(a + b)" -apply (cases a, cases b) +apply (rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star) apply (simp add: hcmod hcomplex_add hypreal_diff hypreal_le) done @@ -816,12 +740,12 @@ subsection{*A Few Nonlinear Theorems*} lemma hcpow: - "Abs_hcomplex(hcomplexrel``{%n. X n}) hcpow + "Abs_star(starrel``{%n. X n}) hcpow Abs_star(starrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n ^ Y n})" + Abs_star(starrel``{%n. X n ^ Y n})" apply (simp add: hcpow_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (rule_tac f = Abs_star in arg_cong) +apply (auto iff: starrel_iff, ultra) done lemma hcomplex_of_hypreal_hyperpow: @@ -831,7 +755,7 @@ done lemma hcmod_hcpow: "hcmod(x hcpow n) = hcmod(x) pow n" -apply (cases x, rule_tac z=n in eq_Abs_star) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=n in eq_Abs_star) apply (simp add: hcpow hyperpow hcmod complex_mod_complexpow) done @@ -842,15 +766,18 @@ done lemma hcmod_divide: "hcmod(x/y) = hcmod(x)/(hcmod y)" -by (simp add: hcomplex_divide_def hypreal_divide_def hcmod_mult hcmod_hcomplex_inverse) +by (simp add: divide_inverse hcmod_mult hcmod_hcomplex_inverse) subsection{*Exponentiation*} -primrec - hcomplexpow_0: "z ^ 0 = 1" - hcomplexpow_Suc: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" +lemma hcomplexpow_0 [simp]: "z ^ 0 = (1::hcomplex)" +by (rule power_0) +lemma hcomplexpow_Suc [simp]: "z ^ (Suc n) = (z::hcomplex) * (z ^ n)" +by (rule power_Suc) + +(* instance hcomplex :: recpower proof fix z :: hcomplex @@ -858,7 +785,7 @@ show "z^0 = 1" by simp show "z^(Suc n) = z * (z^n)" by simp qed - +*) lemma hcomplexpow_i_squared [simp]: "iii ^ 2 = - 1" by (simp add: power2_eq_square) @@ -882,18 +809,19 @@ lemma hcpow_minus: "(-x::hcomplex) hcpow n = (if ( *pNat* even) n then (x hcpow n) else -(x hcpow n))" -apply (cases x, rule_tac z=n in eq_Abs_star) +apply (rule_tac z=x in eq_Abs_star, rule_tac z=n in eq_Abs_star) apply (auto simp add: hcpow hyperpow starPNat hcomplex_minus, ultra) apply (auto simp add: neg_power_if, ultra) done lemma hcpow_mult: "((r::hcomplex) * s) hcpow n = (r hcpow n) * (s hcpow n)" -apply (cases r, cases s, rule_tac z=n in eq_Abs_star) +apply (rule_tac z=r in eq_Abs_star, rule_tac z=s in eq_Abs_star) +apply (rule_tac z=n in eq_Abs_star) apply (simp add: hcpow hypreal_mult hcomplex_mult power_mult_distrib) done lemma hcpow_zero [simp]: "0 hcpow (n + 1) = 0" -apply (simp add: hcomplex_zero_def hypnat_one_def, rule_tac z=n in eq_Abs_star) +apply (simp add: hypreal_zero_def hypnat_one_def, rule_tac z=n in eq_Abs_star) apply (simp add: hcpow hypnat_add) done @@ -901,17 +829,17 @@ by (simp add: hSuc_def) lemma hcpow_not_zero [simp,intro]: "r \ 0 ==> r hcpow n \ (0::hcomplex)" -apply (cases r, rule_tac z=n in eq_Abs_star) -apply (auto simp add: hcpow hcomplex_zero_def, ultra) +apply (rule_tac z=r in eq_Abs_star, rule_tac z=n in eq_Abs_star) +apply (auto simp add: hcpow hypreal_zero_def, ultra) done lemma hcpow_zero_zero: "r hcpow n = (0::hcomplex) ==> r = 0" by (blast intro: ccontr dest: hcpow_not_zero) lemma hcomplex_divide: - "Abs_hcomplex(hcomplexrel``{%n. X n}) / Abs_hcomplex(hcomplexrel``{%n. Y n}) = - Abs_hcomplex(hcomplexrel``{%n. X n / Y n})" -by (simp add: hcomplex_divide_def complex_divide_def hcomplex_inverse hcomplex_mult) + "Abs_star(starrel``{%n. X n::complex}) / Abs_star(starrel``{%n. Y n}) = + Abs_star(starrel``{%n. X n / Y n})" +by (simp add: divide_inverse complex_divide_def hcomplex_inverse hcomplex_mult) @@ -919,33 +847,33 @@ subsection{*The Function @{term hsgn}*} lemma hsgn: - "hsgn (Abs_hcomplex(hcomplexrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. sgn (X n)})" + "hsgn (Abs_star(starrel `` {%n. X n})) = + Abs_star(starrel `` {%n. sgn (X n)})" apply (simp add: hsgn_def) -apply (rule_tac f = Abs_hcomplex in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (rule_tac f = Abs_star in arg_cong) +apply (auto iff: starrel_iff, ultra) done lemma hsgn_zero [simp]: "hsgn 0 = 0" -by (simp add: hcomplex_zero_def hsgn) +by (simp add: hypreal_zero_def hsgn) lemma hsgn_one [simp]: "hsgn 1 = 1" -by (simp add: hcomplex_one_def hsgn) +by (simp add: hypreal_one_def hsgn) lemma hsgn_minus: "hsgn (-z) = - hsgn(z)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hsgn hcomplex_minus sgn_minus) done lemma hsgn_eq: "hsgn z = z / hcomplex_of_hypreal (hcmod z)" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hsgn hcomplex_divide hcomplex_of_hypreal hcmod sgn_eq) done lemma hcmod_i: "hcmod (HComplex x y) = ( *f* sqrt) (x ^ 2 + y ^ 2)" apply (rule_tac z=x in eq_Abs_star, rule_tac z=y in eq_Abs_star) -apply (simp add: HComplex_eq_Abs_hcomplex_Complex starfun +apply (simp add: HComplex_eq_Abs_star_Complex starfun hypreal_mult hypreal_add hcmod numeral_2_eq_2) done @@ -970,12 +898,12 @@ by (simp add: i_eq_HComplex_0_1) lemma hRe_hsgn [simp]: "hRe(hsgn z) = hRe(z)/hcmod z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hsgn hcmod hRe hypreal_divide) done lemma hIm_hsgn [simp]: "hIm(hsgn z) = hIm(z)/hcmod z" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: hsgn hcmod hIm hypreal_divide) done @@ -1026,11 +954,11 @@ (*---------------------------------------------------------------------------*) lemma harg: - "harg (Abs_hcomplex(hcomplexrel `` {%n. X n})) = + "harg (Abs_star(starrel `` {%n. X n})) = Abs_star(starrel `` {%n. arg (X n)})" apply (simp add: harg_def) apply (rule_tac f = Abs_star in arg_cong) -apply (auto iff: hcomplexrel_iff, ultra) +apply (auto iff: starrel_iff, ultra) done lemma cos_harg_i_mult_zero_pos: @@ -1055,7 +983,7 @@ lemma hcomplex_of_hypreal_zero_iff [simp]: "(hcomplex_of_hypreal y = 0) = (y = 0)" apply (rule_tac z=y in eq_Abs_star) -apply (simp add: hcomplex_of_hypreal hypreal_zero_num hcomplex_zero_def) +apply (simp add: hcomplex_of_hypreal hypreal_zero_num hypreal_zero_def) done @@ -1075,7 +1003,7 @@ lemma hcomplex_split_polar: "\r a. z = hcomplex_of_hypreal r * (HComplex(( *f* cos) a)(( *f* sin) a))" -apply (cases z) +apply (rule_tac z=z in eq_Abs_star) apply (simp add: lemma_hypreal_P_EX2 hcomplex_of_hypreal iii_def starfun hcomplex_add hcomplex_mult HComplex_def) apply (cut_tac z = x in complex_split_polar2) apply (drule choice, safe)+ @@ -1085,9 +1013,9 @@ lemma hcis: "hcis (Abs_star(starrel `` {%n. X n})) = - Abs_hcomplex(hcomplexrel `` {%n. cis (X n)})" + Abs_star(starrel `` {%n. cis (X n)})" apply (simp add: hcis_def) -apply (rule_tac f = Abs_hcomplex in arg_cong, auto iff: hcomplexrel_iff, ultra) +apply (rule_tac f = Abs_star in arg_cong, auto iff: starrel_iff, ultra) done lemma hcis_eq: @@ -1100,7 +1028,7 @@ lemma hrcis: "hrcis (Abs_star(starrel `` {%n. X n})) (Abs_star(starrel `` {%n. Y n})) = - Abs_hcomplex(hcomplexrel `` {%n. rcis (X n) (Y n)})" + Abs_star(starrel `` {%n. rcis (X n) (Y n)})" by (simp add: hrcis_def hcomplex_of_hypreal hcomplex_mult hcis rcis_def) lemma hrcis_Ex: "\r a. z = hrcis r a" @@ -1162,10 +1090,10 @@ done lemma hcis_zero [simp]: "hcis 0 = 1" -by (simp add: hcomplex_one_def hcis hypreal_zero_num) +by (simp add: hypreal_one_def hcis hypreal_zero_num) lemma hrcis_zero_mod [simp]: "hrcis 0 a = 0" -apply (simp add: hcomplex_zero_def, rule_tac z=a in eq_Abs_star) +apply (simp add: hypreal_zero_def, rule_tac z=a in eq_Abs_star) apply (simp add: hrcis hypreal_zero_num) done @@ -1247,7 +1175,7 @@ by (simp add: NSDeMoivre_ext) lemma hexpi_add: "hexpi(a + b) = hexpi(a) * hexpi(b)" -apply (simp add: hexpi_def, cases a, cases b) +apply (simp add: hexpi_def, rule_tac z=a in eq_Abs_star, rule_tac z=b in eq_Abs_star) apply (simp add: hcis hRe hIm hcomplex_add hcomplex_mult hypreal_mult starfun hcomplex_of_hypreal cis_mult [symmetric] complex_Im_add complex_Re_add exp_add complex_of_real_mult) done @@ -1261,7 +1189,7 @@ done lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" -by (simp add: iii_def hcomplex_of_complex_def) +by (simp add: iii_def hcomplex_of_complex_def star_of_def star_n_def) lemma hcomplex_of_complex_add [simp]: "hcomplex_of_complex (z1 + z2) = hcomplex_of_complex z1 + hcomplex_of_complex z2" @@ -1281,15 +1209,15 @@ by (simp add: hcomplex_of_complex_def hcomplex_minus) lemma hcomplex_of_complex_one [simp]: "hcomplex_of_complex 1 = 1" -by (simp add: hcomplex_of_complex_def hcomplex_one_def) +by (simp add: hcomplex_of_complex_def hypreal_one_def) lemma hcomplex_of_complex_zero [simp]: "hcomplex_of_complex 0 = 0" -by (simp add: hcomplex_of_complex_def hcomplex_zero_def) +by (simp add: hcomplex_of_complex_def hypreal_zero_def) lemma hcomplex_of_complex_zero_iff [simp]: "(hcomplex_of_complex r = 0) = (r = 0)" by (auto intro: FreeUltrafilterNat_P - simp add: hcomplex_of_complex_def hcomplex_zero_def) + simp add: hcomplex_of_complex_def star_of_def star_n_def hypreal_zero_def) lemma hcomplex_of_complex_inverse [simp]: "hcomplex_of_complex (inverse r) = inverse (hcomplex_of_complex r)" @@ -1315,7 +1243,7 @@ lemma hcomplex_of_complex_divide [simp]: "hcomplex_of_complex (z1 / z2) = hcomplex_of_complex z1 / hcomplex_of_complex z2" -by (simp add: hcomplex_divide_def complex_divide_def) +by (simp add: divide_inverse) lemma hRe_hcomplex_of_complex: "hRe (hcomplex_of_complex z) = hypreal_of_real (Re z)" @@ -1332,6 +1260,7 @@ subsection{*Numerals and Arithmetic*} +(* instance hcomplex :: number .. defs (overloaded) @@ -1340,11 +1269,18 @@ instance hcomplex :: number_ring by (intro_classes, simp add: hcomplex_number_of_def) +*) +lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)" +apply (rule eq_reflection) +apply (unfold star_number_def star_of_int_def) +apply (rule star_of_inject [THEN iffD2]) +apply (rule number_of_eq) +done lemma hcomplex_of_complex_of_nat [simp]: "hcomplex_of_complex (of_nat n) = of_nat n" -by (induct n, simp_all) +by (simp add: hcomplex_of_complex_def) lemma hcomplex_of_complex_of_int [simp]: "hcomplex_of_complex (of_int z) = of_int z" @@ -1390,14 +1326,14 @@ (* Goal "z + hcnj z = hcomplex_of_hypreal (2 * hRe(z))" -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); +by (res_inst_tac [("z","z")] eq_Abs_star 1); by (auto_tac (claset(),HOL_ss addsimps [hRe,hcnj,hcomplex_add, hypreal_mult,hcomplex_of_hypreal,complex_add_cnj])); qed "hcomplex_add_hcnj"; Goal "z - hcnj z = \ \ hcomplex_of_hypreal (hypreal_of_real #2 * hIm(z)) * iii"; -by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); +by (res_inst_tac [("z","z")] eq_Abs_star 1); by (auto_tac (claset(),simpset() addsimps [hIm,hcnj,hcomplex_diff, hypreal_of_real_def,hypreal_mult,hcomplex_of_hypreal, complex_diff_cnj,iii_def,hcomplex_mult])); @@ -1410,12 +1346,12 @@ done declare hcomplex_hcnj_num_zero_iff [simp] -lemma hcomplex_zero_num: "0 = Abs_hcomplex (hcomplexrel `` {%n. 0})" -apply (simp add: hcomplex_zero_def) +lemma hcomplex_zero_num: "0 = Abs_star (starrel `` {%n. 0})" +apply (simp add: hypreal_zero_def) done -lemma hcomplex_one_num: "1 = Abs_hcomplex (hcomplexrel `` {%n. 1})" -apply (simp add: hcomplex_one_def) +lemma hcomplex_one_num: "1 = Abs_star (starrel `` {%n. 1})" +apply (simp add: hypreal_one_def) done (*** Real and imaginary stuff ***) @@ -1525,27 +1461,16 @@ ML {* -val hcomplex_zero_def = thm"hcomplex_zero_def"; -val hcomplex_one_def = thm"hcomplex_one_def"; -val hcomplex_minus_def = thm"hcomplex_minus_def"; -val hcomplex_diff_def = thm"hcomplex_diff_def"; -val hcomplex_divide_def = thm"hcomplex_divide_def"; -val hcomplex_mult_def = thm"hcomplex_mult_def"; -val hcomplex_add_def = thm"hcomplex_add_def"; +(* val hcomplex_zero_def = thm"hcomplex_zero_def"; *) +(* val hcomplex_one_def = thm"hcomplex_one_def"; *) +(* val hcomplex_minus_def = thm"hcomplex_minus_def"; *) +(* val hcomplex_diff_def = thm"hcomplex_diff_def"; *) +(* val hcomplex_divide_def = thm"hcomplex_divide_def"; *) +(* val hcomplex_mult_def = thm"hcomplex_mult_def"; *) +(* val hcomplex_add_def = thm"hcomplex_add_def"; *) val hcomplex_of_complex_def = thm"hcomplex_of_complex_def"; val iii_def = thm"iii_def"; -val hcomplexrel_iff = thm"hcomplexrel_iff"; -val hcomplexrel_refl = thm"hcomplexrel_refl"; -val hcomplexrel_sym = thm"hcomplexrel_sym"; -val hcomplexrel_trans = thm"hcomplexrel_trans"; -val equiv_hcomplexrel = thm"equiv_hcomplexrel"; -val equiv_hcomplexrel_iff = thm"equiv_hcomplexrel_iff"; -val hcomplexrel_in_hcomplex = thm"hcomplexrel_in_hcomplex"; -val lemma_hcomplexrel_refl = thm"lemma_hcomplexrel_refl"; -val hcomplex_empty_not_mem = thm"hcomplex_empty_not_mem"; -val Rep_hcomplex_nonempty = thm"Rep_hcomplex_nonempty"; -val eq_Abs_hcomplex = thm"eq_Abs_hcomplex"; val hRe = thm"hRe"; val hIm = thm"hIm"; val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff"; @@ -1562,7 +1487,7 @@ val hcomplex_add_zero_right = thm"hcomplex_add_zero_right"; val hRe_add = thm"hRe_add"; val hIm_add = thm"hIm_add"; -val hcomplex_minus_congruent = thm"hcomplex_minus_congruent"; +(* val hcomplex_minus_congruent = thm"hcomplex_minus_congruent"; *) val hcomplex_minus = thm"hcomplex_minus"; val hcomplex_add_minus_left = thm"hcomplex_add_minus_left"; val hRe_minus = thm"hRe_minus";