add lemmas norm_not_less_zero, norm_le_zero_iff
authorhuffman
Mon, 02 Oct 2006 18:30:10 +0200
changeset 20828 68ed2e514ca0
parent 20827 e3a503048f9b
child 20829 863b187780bb
add lemmas norm_not_less_zero, norm_le_zero_iff
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"