src/HOL/Complex.thy
 changeset 31413 729d90a531e4 parent 31292 d24b2692562f child 31417 c12b25b7f015
```     1.1 --- a/src/HOL/Complex.thy	Wed Jun 03 07:12:57 2009 -0700
1.2 +++ b/src/HOL/Complex.thy	Wed Jun 03 07:44:56 2009 -0700
1.3 @@ -268,27 +268,29 @@
1.4  instantiation complex :: real_normed_field
1.5  begin
1.6
1.7 -definition
1.8 -  complex_norm_def: "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
1.9 +definition complex_norm_def:
1.10 +  "norm z = sqrt ((Re z)\<twosuperior> + (Im z)\<twosuperior>)"
1.11
1.12  abbreviation
1.13    cmod :: "complex \<Rightarrow> real" where
1.14    "cmod \<equiv> norm"
1.15
1.16 -definition
1.17 -  complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
1.18 +definition complex_sgn_def:
1.19 +  "sgn x = x /\<^sub>R cmod x"
1.20
1.21 -definition
1.22 -  dist_complex_def: "dist x y = cmod (x - y)"
1.23 +definition dist_complex_def:
1.24 +  "dist x y = cmod (x - y)"
1.25 +
1.26 +definition open_complex_def:
1.27 +  "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y::complex. dist y x < e \<longrightarrow> y \<in> S)"
1.28
1.29  lemmas cmod_def = complex_norm_def
1.30
1.31  lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
1.33
1.34 -instance
1.35 -proof
1.36 -  fix r :: real and x y :: complex
1.37 +instance proof
1.38 +  fix r :: real and x y :: complex and S :: "complex set"
1.39    show "0 \<le> norm x"
1.40      by (induct x) simp
1.41    show "(norm x = 0) = (x = 0)"
1.42 @@ -306,6 +308,8 @@
1.43      by (rule complex_sgn_def)
1.44    show "dist x y = cmod (x - y)"
1.45      by (rule dist_complex_def)
1.46 +  show "open S = (\<forall>x\<in>S. \<exists>e>0. \<forall>y. dist y x < e \<longrightarrow> y \<in> S)"
1.47 +    by (rule open_complex_def)
1.48  qed
1.49
1.50  end
```