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.32    by (simp add: complex_norm_def)
    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