define dist for products
authorhuffman
Thu May 28 17:09:51 2009 -0700 (2009-05-28)
changeset 31290f41c023d90bc
parent 31289 847f00f435d4
child 31291 a2f737a72655
define dist for products
src/HOL/Library/Product_Vector.thy
     1.1 --- a/src/HOL/Library/Product_Vector.thy	Thu May 28 17:00:02 2009 -0700
     1.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu May 28 17:09:51 2009 -0700
     1.3 @@ -51,6 +51,9 @@
     1.4  definition sgn_prod_def:
     1.5    "sgn (x::'a \<times> 'b) = scaleR (inverse (norm x)) x"
     1.6  
     1.7 +definition dist_prod_def:
     1.8 +  "dist (x::'a \<times> 'b) y = norm (x - y)"
     1.9 +
    1.10  lemma norm_Pair: "norm (a, b) = sqrt ((norm a)\<twosuperior> + (norm b)\<twosuperior>)"
    1.11    unfolding norm_prod_def by simp
    1.12  
    1.13 @@ -74,6 +77,8 @@
    1.14      done
    1.15    show "sgn x = scaleR (inverse (norm x)) x"
    1.16      by (rule sgn_prod_def)
    1.17 +  show "dist x y = norm (x - y)"
    1.18 +    by (rule dist_prod_def)
    1.19  qed
    1.20  
    1.21  end