# HG changeset patch
# User huffman
# Date 1159806610 -7200
# Node ID 68ed2e514ca052a3aac326727ee972609f76ec5b
# Parent  e3a503048f9bb204d9edc844625a35af7266fc62
add lemmas norm_not_less_zero, norm_le_zero_iff

diff -r e3a503048f9b -r 68ed2e514ca0 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Mon Oct 02 17:33:13 2006 +0200
+++ b/src/HOL/Real/RealVector.thy	Mon Oct 02 18:30:10 2006 +0200
@@ -406,14 +406,18 @@
 apply (rule abs_mult)
 done
 
-lemma norm_zero [simp]: "norm (0::'a::real_normed_vector) = 0"
+lemma norm_zero [simp]: "norm (0::'a::normed) = 0"
 by simp
 
-lemma zero_less_norm_iff [simp]:
-  fixes x :: "'a::real_normed_vector"
-  shows "(0 < norm x) = (x \<noteq> 0)"
+lemma zero_less_norm_iff [simp]: "(0 < norm x) = (x \<noteq> (0::'a::normed))"
 by (simp add: order_less_le)
 
+lemma norm_not_less_zero [simp]: "\<not> norm (x::'a::normed) < 0"
+by (simp add: linorder_not_less)
+
+lemma norm_le_zero_iff [simp]: "(norm x \<le> 0) = (x = (0::'a::normed))"
+by (simp add: order_le_less)
+
 lemma norm_minus_cancel [simp]:
   fixes x :: "'a::real_normed_vector"
   shows "norm (- x) = norm x"