--- 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)
-----------------------------------
--- 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"
--- 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
--- 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"
--- 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)
--- 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 *}
--- 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)
--- 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)