# HG changeset patch
# User huffman
# Date 1243555791 25200
# Node ID f41c023d90bc5e2c67d89800d4c26c6facbe1ba1
# Parent  847f00f435d43dc2e4e7cff5cd4f732ce66d236e
define dist for products

diff -r 847f00f435d4 -r f41c023d90bc src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu May 28 17:00:02 2009 -0700
+++ b/src/HOL/Library/Product_Vector.thy	Thu May 28 17:09:51 2009 -0700
@@ -51,6 +51,9 @@
 definition sgn_prod_def:
   "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
 
+definition dist_prod_def:
+  "dist (x::'a \<times> 'b) y = norm (x - y)"
+
 lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)"
   unfolding norm_prod_def by simp
 
@@ -74,6 +77,8 @@
     done
   show "sgn x = scaleR (inverse (norm x)) x"
     by (rule sgn_prod_def)
+  show "dist x y = norm (x - y)"
+    by (rule dist_prod_def)
 qed
 
 end