--- a/src/HOL/Complex.thy Wed Jun 03 07:12:57 2009 -0700
+++ b/src/HOL/Complex.thy Wed Jun 03 07:44:56 2009 -0700
@@ -268,27 +268,29 @@
instantiation complex :: real_normed_field
begin
-definition
- complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
+definition complex_norm_def:
+ "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
abbreviation
cmod :: "complex \<Rightarrow> real" where
"cmod \<equiv> norm"
-definition
- complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
+definition complex_sgn_def:
+ "sgn x = x /\<^sub>R cmod x"
-definition
- dist_complex_def: "dist x y = cmod (x - y)"
+definition dist_complex_def:
+ "dist x y = cmod (x - y)"
+
+definition open_complex_def:
+ "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. dist y x < e \<longrightarrow> y \<in> S)"
lemmas cmod_def = complex_norm_def
lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
by (simp add: complex_norm_def)
-instance
-proof
- fix r :: real and x y :: complex
+instance proof
+ fix r :: real and x y :: complex and S :: "complex set"
show "0 \<le> norm x"
by (induct x) simp
show "(norm x = 0) = (x = 0)"
@@ -306,6 +308,8 @@
by (rule complex_sgn_def)
show "dist x y = cmod (x - y)"
by (rule dist_complex_def)
+ show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
+ by (rule open_complex_def)
qed
end