# HG changeset patch # User huffman # Date 1178666764 -7200 # Node ID 005be8dafce0761dad9dae5cda0eb30c79ba798a # Parent bc10bb8d08092207d75609f2eefff76fbea3fb2e hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas diff -r bc10bb8d0809 -r 005be8dafce0 src/HOL/Complex/CLim.thy --- a/src/HOL/Complex/CLim.thy Wed May 09 00:57:46 2007 +0200 +++ b/src/HOL/Complex/CLim.thy Wed May 09 01:26:04 2007 +0200 @@ -134,7 +134,7 @@ subsection{*Functions from Complex to Reals*} lemma isNSContCR_cmod [simp]: "isNSCont cmod (a)" -by (auto intro: approx_hcmod_approx +by (auto intro: approx_hnorm simp add: starfunCR_cmod hcmod_hcomplex_of_complex [symmetric] isNSCont_def) diff -r bc10bb8d0809 -r 005be8dafce0 src/HOL/Complex/Complex.thy --- a/src/HOL/Complex/Complex.thy Wed May 09 00:57:46 2007 +0200 +++ b/src/HOL/Complex/Complex.thy Wed May 09 01:26:04 2007 +0200 @@ -455,14 +455,6 @@ lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \ cmod a" by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) -lemma complex_mod_add_less: - "[| cmod x < r; cmod y < s |] ==> cmod (x + y) < r + s" -by (auto intro: order_le_less_trans complex_mod_triangle_ineq) - -lemma complex_mod_mult_less: - "[| cmod x < r; cmod y < s |] ==> cmod (x * y) < r * s" -by (auto intro: real_mult_less_mono' simp add: complex_mod_mult) - lemma complex_mod_diff_ineq [simp]: "cmod(a) - cmod(b) \ cmod(a + b)" (* TODO: generalize *) proof - diff -r bc10bb8d0809 -r 005be8dafce0 src/HOL/Complex/NSCA.thy --- a/src/HOL/Complex/NSCA.thy Wed May 09 00:57:46 2007 +0200 +++ b/src/HOL/Complex/NSCA.thy Wed May 09 01:26:04 2007 +0200 @@ -22,51 +22,23 @@ subsection{*Closure Laws for SComplex, the Standard Complex Numbers*} -lemma SComplex_add: "[| x \ SComplex; y \ SComplex |] ==> x + y \ SComplex" -by (rule Standard_add) - -lemma SComplex_mult: "[| x \ SComplex; y \ SComplex |] ==> x * y \ SComplex" -by (rule Standard_mult) - -lemma SComplex_inverse: "x \ SComplex ==> inverse x \ SComplex" -by (rule Standard_inverse) - -lemma SComplex_divide: "[| x \ SComplex; y \ SComplex |] ==> x/y \ SComplex" -by (rule Standard_divide) - -lemma SComplex_minus: "x \ SComplex ==> -x \ SComplex" -by (rule Standard_minus) - lemma SComplex_minus_iff [simp]: "(-x \ SComplex) = (x \ SComplex)" -apply auto -apply (drule SComplex_minus, auto) -done - -lemma SComplex_diff: "[| x \ SComplex; y \ SComplex |] ==> x - y \ SComplex" -by (rule Standard_diff) +by (auto, drule Standard_minus, auto) lemma SComplex_add_cancel: "[| x + y \ SComplex; y \ SComplex |] ==> x \ SComplex" -by (drule SComplex_diff, assumption, simp) +by (drule (1) Standard_diff, simp) lemma SReal_hcmod_hcomplex_of_complex [simp]: "hcmod (hcomplex_of_complex r) \ Reals" by (simp add: Reals_eq_Standard) lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \ Reals" -apply (subst star_of_number_of [symmetric]) -apply (rule SReal_hcmod_hcomplex_of_complex) -done +by (simp add: Reals_eq_Standard) lemma SReal_hcmod_SComplex: "x \ SComplex ==> hcmod x \ Reals" by (simp add: Reals_eq_Standard) -lemma SComplex_hcomplex_of_complex: "hcomplex_of_complex x \ SComplex" -by (rule Standard_star_of) - -lemma SComplex_number_of: "(number_of w ::hcomplex) \ SComplex" -by (rule Standard_number_of) - lemma SComplex_divide_number_of: "r \ SComplex ==> r/(number_of w::hcomplex) \ SComplex" by simp @@ -102,12 +74,6 @@ "z \ SComplex ==> hcmod z \ Reals" by (simp add: Reals_eq_Standard) -lemma SComplex_zero: "0 \ SComplex" -by (rule Standard_zero) - -lemma SComplex_one: "1 \ SComplex" -by (rule Standard_one) - (* Goalw [SComplex_def,SReal_def] "hcmod z \ Reals ==> z \ SComplex" by (res_inst_tac [("z","z")] eq_Abs_hcomplex 1); @@ -118,16 +84,10 @@ subsection{*The Finite Elements form a Subring*} -lemma SComplex_subset_HFinite [simp]: "SComplex \ HFinite" -by (auto simp add: Standard_def) - lemma HFinite_hcmod_hcomplex_of_complex [simp]: "hcmod (hcomplex_of_complex r) \ HFinite" by (auto intro!: SReal_subset_HFinite [THEN subsetD]) -lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \ HFinite" -by (rule HFinite_star_of) - lemma HFinite_hcmod_iff: "(x \ HFinite) = (hcmod x \ HFinite)" by (simp add: HFinite_def) @@ -182,31 +142,17 @@ by (auto_tac (claset(),simpset() addsimps [Infinitesimal_hcmod_iff])); *) -lemma approx_mult_subst_SComplex: - "[| u @= x*hcomplex_of_complex v; x @= y |] - ==> u @= y*hcomplex_of_complex v" -by (rule approx_mult_subst_star_of) - -lemma approx_hcomplex_of_complex_HFinite: - "x @= hcomplex_of_complex D ==> x \ HFinite" -by (rule approx_star_of_HFinite) - -lemma approx_mult_hcomplex_of_complex: - "[|a @= hcomplex_of_complex b; c @= hcomplex_of_complex d |] - ==> a*c @= hcomplex_of_complex b * hcomplex_of_complex d" -by (rule approx_mult_star_of) - lemma approx_SComplex_mult_cancel_zero: "[| a \ SComplex; a \ 0; a*x @= 0 |] ==> x @= 0" -apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) +apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]]) apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_mult_SComplex1: "[| a \ SComplex; x @= 0 |] ==> x*a @= 0" -by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult1) +by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult1) lemma approx_mult_SComplex2: "[| a \ SComplex; x @= 0 |] ==> a*x @= 0" -by (auto dest: SComplex_subset_HFinite [THEN subsetD] approx_mult2) +by (auto dest: Standard_subset_HFinite [THEN subsetD] approx_mult2) lemma approx_mult_SComplex_zero_cancel_iff [simp]: "[|a \ SComplex; a \ 0 |] ==> (a*x @= 0) = (x @= 0)" @@ -214,19 +160,19 @@ lemma approx_SComplex_mult_cancel: "[| a \ SComplex; a \ 0; a* w @= a*z |] ==> w @= z" -apply (drule SComplex_inverse [THEN SComplex_subset_HFinite [THEN subsetD]]) +apply (drule Standard_inverse [THEN Standard_subset_HFinite [THEN subsetD]]) apply (auto dest: approx_mult2 simp add: mult_assoc [symmetric]) done lemma approx_SComplex_mult_cancel_iff1 [simp]: "[| a \ SComplex; a \ 0|] ==> (a* w @= a*z) = (w @= z)" -by (auto intro!: approx_mult2 SComplex_subset_HFinite [THEN subsetD] +by (auto intro!: approx_mult2 Standard_subset_HFinite [THEN subsetD] intro: approx_SComplex_mult_cancel) (* TODO: generalize following theorems: hcmod -> hnorm *) lemma approx_hcmod_approx_zero: "(x @= y) = (hcmod (y - x) @= 0)" -apply (subst hcmod_diff_commute) +apply (subst hnorm_minus_commute) apply (simp add: approx_def Infinitesimal_hcmod_iff diff_minus) done @@ -250,9 +196,6 @@ apply (auto intro: Infinitesimal_hcmod_add_diff simp add: mem_infmal_iff [symmetric] diff_minus [symmetric]) done -lemma approx_hcmod_approx: "x @= y ==> hcmod x @= hcmod y" -by (rule approx_hnorm) - subsection{*Zero is the Only Infinitesimal Complex Number*} @@ -269,20 +212,16 @@ lemma SComplex_HFinite_diff_Infinitesimal: "[| x \ SComplex; x \ 0 |] ==> x \ HFinite - Infinitesimal" -by (auto dest: SComplex_Infinitesimal_zero SComplex_subset_HFinite [THEN subsetD]) +by (auto dest: SComplex_Infinitesimal_zero Standard_subset_HFinite [THEN subsetD]) lemma hcomplex_of_complex_HFinite_diff_Infinitesimal: "hcomplex_of_complex x \ 0 ==> hcomplex_of_complex x \ HFinite - Infinitesimal" by (rule SComplex_HFinite_diff_Infinitesimal, auto) -lemma hcomplex_of_complex_Infinitesimal_iff_0: - "(hcomplex_of_complex x \ Infinitesimal) = (x=0)" -by (rule star_of_Infinitesimal_iff_0) - lemma number_of_not_Infinitesimal [simp]: "number_of w \ (0::hcomplex) ==> (number_of w::hcomplex) \ Infinitesimal" -by (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) +by (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) lemma approx_SComplex_not_zero: "[| y \ SComplex; x @= y; y\ 0 |] ==> x \ 0" @@ -296,18 +235,10 @@ "((number_of w :: hcomplex) \ Infinitesimal) = (number_of w = (0::hcomplex))" apply (rule iffI) -apply (fast dest: SComplex_number_of [THEN SComplex_Infinitesimal_zero]) +apply (fast dest: Standard_number_of [THEN SComplex_Infinitesimal_zero]) apply (simp (no_asm_simp)) done -lemma hcomplex_of_complex_approx_iff: - "(hcomplex_of_complex k @= hcomplex_of_complex m) = (k = m)" -by (rule star_of_approx_iff) - -lemma hcomplex_of_complex_approx_number_of_iff [simp]: - "(hcomplex_of_complex k @= number_of w) = (k = number_of w)" -by (subst hcomplex_of_complex_approx_iff [symmetric], auto) - lemma approx_unique_complex: "[| r \ SComplex; s \ SComplex; r @= x; s @= x|] ==> r = s" by (blast intro: SComplex_approx_iff [THEN iffD1] approx_trans2) @@ -474,10 +405,10 @@ done lemma stc_HFinite: "x \ HFinite ==> stc x \ HFinite" -by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]]) +by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]]) lemma stc_unique: "\y \ SComplex; y \ x\ \ stc x = y" -apply (frule SComplex_subset_HFinite [THEN subsetD]) +apply (frule Standard_subset_HFinite [THEN subsetD]) apply (drule (1) approx_HFinite) apply (unfold stc_def) apply (rule some_equality) @@ -524,10 +455,10 @@ lemma stc_add: "[| x \ HFinite; y \ HFinite |] ==> stc (x + y) = stc(x) + stc(y)" -by (simp add: stc_unique stc_SComplex stc_approx_self approx_add SComplex_add) +by (simp add: stc_unique stc_SComplex stc_approx_self approx_add) lemma stc_number_of [simp]: "stc (number_of w) = number_of w" -by (rule SComplex_number_of [THEN stc_SComplex_eq]) +by (rule Standard_number_of [THEN stc_SComplex_eq]) lemma stc_zero [simp]: "stc 0 = 0" by simp @@ -540,12 +471,12 @@ lemma stc_diff: "[| x \ HFinite; y \ HFinite |] ==> stc (x-y) = stc(x) - stc(y)" -by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff SComplex_diff) +by (simp add: stc_unique stc_SComplex stc_approx_self approx_diff) lemma stc_mult: "[| x \ HFinite; y \ HFinite |] ==> stc (x * y) = stc(x) * stc(y)" -by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite SComplex_mult) +by (simp add: stc_unique stc_SComplex stc_approx_self approx_mult_HFinite) lemma stc_Infinitesimal: "x \ Infinitesimal ==> stc x = 0" by (simp add: stc_unique mem_infmal_iff) @@ -557,7 +488,7 @@ "[| x \ HFinite; stc x \ 0 |] ==> stc(inverse x) = inverse (stc x)" apply (drule stc_not_Infinitesimal) -apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse SComplex_inverse) +apply (simp add: stc_unique stc_SComplex stc_approx_self approx_inverse) done lemma stc_divide [simp]: @@ -574,8 +505,9 @@ lemma SComplex_SReal_hcomplex_of_hypreal: "x \ Reals ==> hcomplex_of_hypreal x \ SComplex" -by (auto simp add: SReal_def Standard_def hcomplex_of_hypreal_def - simp del: star_of_of_real) +apply (rule Standard_of_hypreal) +apply (simp add: Reals_eq_Standard) +done lemma stc_hcomplex_of_hypreal: "z \ HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)" diff -r bc10bb8d0809 -r 005be8dafce0 src/HOL/Complex/NSComplex.thy --- a/src/HOL/Complex/NSComplex.thy Wed May 09 00:57:46 2007 +0200 +++ b/src/HOL/Complex/NSComplex.thy Wed May 09 01:26:04 2007 +0200 @@ -62,9 +62,9 @@ (*----- injection from hyperreals -----*) -definition - hcomplex_of_hypreal :: "hypreal => hcomplex" where - "hcomplex_of_hypreal = *f* complex_of_real" +abbreviation + hcomplex_of_hypreal :: "hypreal \ hcomplex" where + "hcomplex_of_hypreal \ of_hypreal" definition (* abbreviation for r*(cos a + i sin a) *) @@ -86,7 +86,7 @@ *) lemmas hcomplex_defs [transfer_unfold] = hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def - hcomplex_of_hypreal_def hrcis_def hexpi_def HComplex_def + hrcis_def hexpi_def HComplex_def lemma Standard_hRe [simp]: "x \ Standard \ hRe x \ Standard" by (simp add: hcomplex_defs) @@ -120,10 +120,6 @@ "\r \ Standard; s \ Standard\ \ HComplex r s \ Standard" by (simp add: hcomplex_defs) -lemma Standard_hcomplex_of_hypreal [simp]: - "r \ Standard \ hcomplex_of_hypreal r \ Standard" -by (simp add: hcomplex_defs) - lemma hcmod_def: "hcmod = *f* cmod" by (rule hnorm_def) @@ -203,62 +199,18 @@ subsection{*Subraction and Division*} lemma hcomplex_diff_eq_eq [simp]: "((x::hcomplex) - y = z) = (x = z + y)" +(* TODO: delete *) by (rule OrderedGroup.diff_eq_eq) -lemma hcomplex_add_divide_distrib: "(x+y)/(z::hcomplex) = x/z + y/z" -by (rule Ring_and_Field.add_divide_distrib) - subsection{*Embedding Properties for @{term hcomplex_of_hypreal} Map*} -lemma hcomplex_of_hypreal_cancel_iff [iff]: - "!!x y. (hcomplex_of_hypreal x = hcomplex_of_hypreal y) = (x = y)" -by transfer (rule of_real_eq_iff) - -lemma hcomplex_of_hypreal_one [simp]: "hcomplex_of_hypreal 1 = 1" -by transfer (rule of_real_1) - -lemma hcomplex_of_hypreal_zero [simp]: "hcomplex_of_hypreal 0 = 0" -by transfer (rule of_real_0) - -lemma hcomplex_of_hypreal_minus [simp]: - "!!x. hcomplex_of_hypreal(-x) = - hcomplex_of_hypreal x" -by transfer (rule of_real_minus) - -lemma hcomplex_of_hypreal_inverse [simp]: - "!!x. hcomplex_of_hypreal(inverse x) = inverse(hcomplex_of_hypreal x)" -by transfer (rule of_real_inverse) - -lemma hcomplex_of_hypreal_add [simp]: - "!!x y. hcomplex_of_hypreal (x + y) = - hcomplex_of_hypreal x + hcomplex_of_hypreal y" -by transfer (rule of_real_add) - -lemma hcomplex_of_hypreal_diff [simp]: - "!!x y. hcomplex_of_hypreal (x - y) = - hcomplex_of_hypreal x - hcomplex_of_hypreal y " -by transfer (rule of_real_diff) - -lemma hcomplex_of_hypreal_mult [simp]: - "!!x y. hcomplex_of_hypreal (x * y) = - hcomplex_of_hypreal x * hcomplex_of_hypreal y" -by transfer (rule of_real_mult) - -lemma hcomplex_of_hypreal_divide [simp]: - "!!x y. hcomplex_of_hypreal(x/y) = - hcomplex_of_hypreal x / hcomplex_of_hypreal y" -by transfer (rule of_real_divide) - lemma hRe_hcomplex_of_hypreal [simp]: "!!z. hRe(hcomplex_of_hypreal z) = z" by transfer (rule Re_complex_of_real) lemma hIm_hcomplex_of_hypreal [simp]: "!!z. hIm(hcomplex_of_hypreal z) = 0" by transfer (rule Im_complex_of_real) -lemma hcomplex_of_hypreal_zero_iff [simp]: - "\x. (hcomplex_of_hypreal x = 0) = (x = 0)" -by transfer (rule of_real_eq_0_iff) - lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal epsilon \ 0" by (simp add: hypreal_epsilon_not_zero) @@ -281,16 +233,6 @@ subsection{*Modulus (Absolute Value) of Nonstandard Complex Number*} -lemma hcmod_zero [simp]: "hcmod(0) = 0" -by (rule hnorm_zero) - -lemma hcmod_one [simp]: "hcmod(1) = 1" -by (rule hnorm_one) - -lemma hcmod_hcomplex_of_hypreal [simp]: - "!!x. hcmod(hcomplex_of_hypreal x) = abs x" -by transfer (rule norm_of_real) - lemma hcomplex_of_hypreal_abs: "hcomplex_of_hypreal (abs x) = hcomplex_of_hypreal(hcmod(hcomplex_of_hypreal x))" @@ -395,9 +337,6 @@ subsection{*More Theorems about the Function @{term hcmod}*} -lemma hcomplex_hcmod_eq_zero_cancel [simp]: "!!x. (hcmod x = 0) = (x = 0)" -by transfer (rule norm_eq_zero) - lemma hcmod_hcomplex_of_hypreal_of_nat [simp]: "hcmod (hcomplex_of_hypreal(hypreal_of_nat n)) = hypreal_of_nat n" by simp @@ -406,40 +345,13 @@ "hcmod (hcomplex_of_hypreal(hypreal_of_hypnat n)) = hypreal_of_hypnat n" by simp -lemma hcmod_minus [simp]: "!!x. hcmod (-x) = hcmod(x)" -by transfer (rule norm_minus_cancel) - lemma hcmod_mult_hcnj: "!!z. hcmod(z * hcnj(z)) = hcmod(z) ^ 2" by transfer (rule complex_mod_mult_cnj) -lemma hcmod_ge_zero [simp]: "!!x. (0::hypreal) \ hcmod x" -by transfer (rule norm_ge_zero) - -lemma hrabs_hcmod_cancel [simp]: "abs(hcmod x) = hcmod x" -by (simp add: abs_if linorder_not_less) - -lemma hcmod_mult: "!!x y. hcmod(x*y) = hcmod(x) * hcmod(y)" -by transfer (rule complex_mod_mult) - -lemma hcmod_triangle_ineq [simp]: - "!!x y. hcmod (x + y) \ hcmod(x) + hcmod(y)" -by transfer (rule complex_mod_triangle_ineq) - lemma hcmod_triangle_ineq2 [simp]: "!!a b. hcmod(b + a) - hcmod b \ hcmod a" by transfer (rule complex_mod_triangle_ineq2) -lemma hcmod_diff_commute: "!!x y. hcmod (x - y) = hcmod (y - x)" -by transfer (rule norm_minus_commute) - -lemma hcmod_add_less: - "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x + y) < r + s" -by transfer (rule complex_mod_add_less) - -lemma hcmod_mult_less: - "!!x y r s. [| hcmod x < r; hcmod y < s |] ==> hcmod (x * y) < r * s" -by transfer (rule complex_mod_mult_less) - lemma hcmod_diff_ineq [simp]: "!!a b. hcmod(a) - hcmod(b) \ hcmod(a + b)" by transfer (rule complex_mod_diff_ineq) @@ -453,12 +365,6 @@ lemma hcmod_hcpow: "!!x n. hcmod(x pow n) = hcmod(x) pow n" by transfer (rule complex_mod_complexpow) -lemma hcmod_hcomplex_inverse: "!!x. hcmod(inverse x) = inverse(hcmod x)" -by transfer (rule norm_inverse) - -lemma hcmod_divide: "!!x y. hcmod(x/y) = hcmod(x)/(hcmod y)" -by transfer (rule norm_divide) - subsection{*Exponentiation*} @@ -734,7 +640,8 @@ type @{typ complex} to to @{typ hcomplex}*} lemma inj_hcomplex_of_complex: "inj(hcomplex_of_complex)" -by (rule inj_onI, simp) +(* TODO: delete *) +by (rule inj_star_of) lemma hcomplex_of_complex_i: "iii = hcomplex_of_complex ii" by (rule iii_def)