--- 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)
--- 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 \<le> 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) \<le> cmod(a + b)"
(* TODO: generalize *)
proof -
--- 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 \<in> SComplex; y \<in> SComplex |] ==> x + y \<in> SComplex"
-by (rule Standard_add)
-
-lemma SComplex_mult: "[| x \<in> SComplex; y \<in> SComplex |] ==> x * y \<in> SComplex"
-by (rule Standard_mult)
-
-lemma SComplex_inverse: "x \<in> SComplex ==> inverse x \<in> SComplex"
-by (rule Standard_inverse)
-
-lemma SComplex_divide: "[| x \<in> SComplex; y \<in> SComplex |] ==> x/y \<in> SComplex"
-by (rule Standard_divide)
-
-lemma SComplex_minus: "x \<in> SComplex ==> -x \<in> SComplex"
-by (rule Standard_minus)
-
lemma SComplex_minus_iff [simp]: "(-x \<in> SComplex) = (x \<in> SComplex)"
-apply auto
-apply (drule SComplex_minus, auto)
-done
-
-lemma SComplex_diff: "[| x \<in> SComplex; y \<in> SComplex |] ==> x - y \<in> SComplex"
-by (rule Standard_diff)
+by (auto, drule Standard_minus, auto)
lemma SComplex_add_cancel:
"[| x + y \<in> SComplex; y \<in> SComplex |] ==> x \<in> 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) \<in> Reals"
by (simp add: Reals_eq_Standard)
lemma SReal_hcmod_number_of [simp]: "hcmod (number_of w ::hcomplex) \<in> 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 \<in> SComplex ==> hcmod x \<in> Reals"
by (simp add: Reals_eq_Standard)
-lemma SComplex_hcomplex_of_complex: "hcomplex_of_complex x \<in> SComplex"
-by (rule Standard_star_of)
-
-lemma SComplex_number_of: "(number_of w ::hcomplex) \<in> SComplex"
-by (rule Standard_number_of)
-
lemma SComplex_divide_number_of:
"r \<in> SComplex ==> r/(number_of w::hcomplex) \<in> SComplex"
by simp
@@ -102,12 +74,6 @@
"z \<in> SComplex ==> hcmod z \<in> Reals"
by (simp add: Reals_eq_Standard)
-lemma SComplex_zero: "0 \<in> SComplex"
-by (rule Standard_zero)
-
-lemma SComplex_one: "1 \<in> SComplex"
-by (rule Standard_one)
-
(*
Goalw [SComplex_def,SReal_def] "hcmod z \<in> Reals ==> z \<in> 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 \<le> HFinite"
-by (auto simp add: Standard_def)
-
lemma HFinite_hcmod_hcomplex_of_complex [simp]:
"hcmod (hcomplex_of_complex r) \<in> HFinite"
by (auto intro!: SReal_subset_HFinite [THEN subsetD])
-lemma HFinite_hcomplex_of_complex: "hcomplex_of_complex x \<in> HFinite"
-by (rule HFinite_star_of)
-
lemma HFinite_hcmod_iff: "(x \<in> HFinite) = (hcmod x \<in> 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 \<in> 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 \<in> SComplex; a \<noteq> 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 \<in> 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 \<in> 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 \<in> SComplex; a \<noteq> 0 |] ==> (a*x @= 0) = (x @= 0)"
@@ -214,19 +160,19 @@
lemma approx_SComplex_mult_cancel:
"[| a \<in> SComplex; a \<noteq> 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 \<in> SComplex; a \<noteq> 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 \<in> SComplex; x \<noteq> 0 |] ==> x \<in> 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 \<noteq> 0
==> hcomplex_of_complex x \<in> HFinite - Infinitesimal"
by (rule SComplex_HFinite_diff_Infinitesimal, auto)
-lemma hcomplex_of_complex_Infinitesimal_iff_0:
- "(hcomplex_of_complex x \<in> Infinitesimal) = (x=0)"
-by (rule star_of_Infinitesimal_iff_0)
-
lemma number_of_not_Infinitesimal [simp]:
"number_of w \<noteq> (0::hcomplex) ==> (number_of w::hcomplex) \<notin> 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 \<in> SComplex; x @= y; y\<noteq> 0 |] ==> x \<noteq> 0"
@@ -296,18 +235,10 @@
"((number_of w :: hcomplex) \<in> 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 \<in> SComplex; s \<in> 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 \<in> HFinite ==> stc x \<in> HFinite"
-by (erule stc_SComplex [THEN SComplex_subset_HFinite [THEN subsetD]])
+by (erule stc_SComplex [THEN Standard_subset_HFinite [THEN subsetD]])
lemma stc_unique: "\<lbrakk>y \<in> SComplex; y \<approx> x\<rbrakk> \<Longrightarrow> 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 \<in> HFinite; y \<in> 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 \<in> HFinite; y \<in> 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 \<in> HFinite; y \<in> 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 \<in> Infinitesimal ==> stc x = 0"
by (simp add: stc_unique mem_infmal_iff)
@@ -557,7 +488,7 @@
"[| x \<in> HFinite; stc x \<noteq> 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 \<in> Reals ==> hcomplex_of_hypreal x \<in> 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 \<in> HFinite ==> stc(hcomplex_of_hypreal z) = hcomplex_of_hypreal (st z)"
--- 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 \<Rightarrow> hcomplex" where
+ "hcomplex_of_hypreal \<equiv> 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 \<in> Standard \<Longrightarrow> hRe x \<in> Standard"
by (simp add: hcomplex_defs)
@@ -120,10 +120,6 @@
"\<lbrakk>r \<in> Standard; s \<in> Standard\<rbrakk> \<Longrightarrow> HComplex r s \<in> Standard"
by (simp add: hcomplex_defs)
-lemma Standard_hcomplex_of_hypreal [simp]:
- "r \<in> Standard \<Longrightarrow> hcomplex_of_hypreal r \<in> 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]:
- "\<And>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 \<noteq> 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) \<le> 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) \<le> hcmod(x) + hcmod(y)"
-by transfer (rule complex_mod_triangle_ineq)
-
lemma hcmod_triangle_ineq2 [simp]:
"!!a b. hcmod(b + a) - hcmod b \<le> 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) \<le> 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)