# HG changeset patch
# User hoelzl
# Date 1359650532 -3600
# Node ID 496013a6eb38fc236d2539b8a1653fceb6cb13fe
# Parent  461fdbbdb912e54ec148a8f4cc14750168adb463
remove unnecessary assumption from real_normed_vector

diff -r 461fdbbdb912 -r 496013a6eb38 NEWS
--- a/NEWS	Thu Jan 31 12:09:07 2013 +0100
+++ b/NEWS	Thu Jan 31 17:42:12 2013 +0100
@@ -4,6 +4,12 @@
 New in this Isabelle version
 ----------------------------
 
+*** HOL ***
+
+* Theory "RealVector" and "Limits": Introduce type class
+(lin)order_topology. Allows to generalize theorems about limits and
+order. Instances are reals and extended reals.
+
 
 New in Isabelle2013 (February 2013)
 -----------------------------------
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Complex.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -288,8 +288,6 @@
 
 instance proof
   fix r :: real and x y :: complex and S :: "complex set"
-  show "0 \<le> norm x"
-    by (induct x) simp
   show "(norm x = 0) = (x = 0)"
     by (induct x) simp
   show "norm (x + y) \<le> norm x + norm y"
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Library/FrechetDeriv.thy
--- a/src/HOL/Library/FrechetDeriv.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Library/FrechetDeriv.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -5,7 +5,7 @@
 header {* Frechet Derivative *}
 
 theory FrechetDeriv
-imports Complex_Main
+imports "~~/src/HOL/Complex_Main"
 begin
 
 definition
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Library/Inner_Product.thy
--- a/src/HOL/Library/Inner_Product.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Library/Inner_Product.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -117,8 +117,6 @@
 subclass real_normed_vector
 proof
   fix a :: real and x y :: 'a
-  show "0 \<le> norm x"
-    unfolding norm_eq_sqrt_inner by simp
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_eq_sqrt_inner by simp
   show "norm (x + y) \<le> norm x + norm y"
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Library/Product_Vector.thy
--- a/src/HOL/Library/Product_Vector.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Library/Product_Vector.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -408,8 +408,6 @@
 
 instance proof
   fix r :: real and x y :: "'a \<times> 'b"
-  show "0 \<le> norm x"
-    unfolding norm_prod_def by simp
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_prod_def
     by (simp add: prod_eq_iff)
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Library/Product_plus.thy
--- a/src/HOL/Library/Product_plus.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Library/Product_plus.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -5,7 +5,7 @@
 header {* Additive group operations on product types *}
 
 theory Product_plus
-imports Main
+imports "~~/src/HOL/Main"
 begin
 
 subsection {* Operations *}
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -387,9 +387,6 @@
 
 instance proof
   fix a :: real and x y :: "'a ^ 'b"
-  show "0 \<le> norm x"
-    unfolding norm_vec_def
-    by (rule setL2_nonneg)
   show "norm x = 0 \<longleftrightarrow> x = 0"
     unfolding norm_vec_def
     by (simp add: setL2_eq_0_iff vec_eq_iff)
diff -r 461fdbbdb912 -r 496013a6eb38 src/HOL/RealVector.thy
--- a/src/HOL/RealVector.thy	Thu Jan 31 12:09:07 2013 +0100
+++ b/src/HOL/RealVector.thy	Thu Jan 31 17:42:12 2013 +0100
@@ -725,10 +725,20 @@
   assumes dist_norm: "dist x y = norm (x - y)"
 
 class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
-  assumes norm_ge_zero [simp]: "0 \<le> norm x"
-  and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
+  assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
   and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
   and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
+begin
+
+lemma norm_ge_zero [simp]: "0 \<le> norm x"
+proof -
+  have "0 = norm (x + -1 *\<^sub>R x)" 
+    using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
+  also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
+  finally show ?thesis by simp
+qed
+
+end
 
 class real_normed_algebra = real_algebra + real_normed_vector +
   assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
@@ -954,7 +964,6 @@
 apply (rule dist_real_def)
 apply (rule open_real_def)
 apply (simp add: sgn_real_def)
-apply (rule abs_ge_zero)
 apply (rule abs_eq_0)
 apply (rule abs_triangle_ineq)
 apply (rule abs_mult)