# HG changeset patch
# User huffman
# Date 1243576403 25200
# Node ID d24b2692562f257d2cc731eddeb2ee51d72e5512
# Parent  a2f737a726552ad9342432182f6f503f2db9ada5
definition of dist for complex

diff -r a2f737a72655 -r d24b2692562f src/HOL/Complex.thy
--- 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