src/HOL/Complex.thy
changeset 31292 d24b2692562f
parent 31021 53642251a04f
child 31413 729d90a531e4
--- a/src/HOL/Complex.thy	Thu May 28 17:24:18 2009 -0700
+++ b/src/HOL/Complex.thy	Thu May 28 22:53:23 2009 -0700
@@ -278,6 +278,9 @@
 definition
   complex_sgn_def: "sgn x = x /\<^sub>R cmod x"
 
+definition
+  dist_complex_def: "dist x y = cmod (x - y)"
+
 lemmas cmod_def = complex_norm_def
 
 lemma complex_norm [simp]: "cmod (Complex x y) = sqrt (x\<twosuperior> + y\<twosuperior>)"
@@ -299,7 +302,10 @@
   show "norm (x * y) = norm x * norm y"
     by (induct x, induct y)
        (simp add: real_sqrt_mult [symmetric] power2_eq_square algebra_simps)
-  show "sgn x = x /\<^sub>R cmod x" by(simp add: complex_sgn_def)
+  show "sgn x = x /\<^sub>R cmod x"
+    by (rule complex_sgn_def)
+  show "dist x y = cmod (x - y)"
+    by (rule dist_complex_def)
 qed
 
 end