remove unnecessary assumption from real_normed_vector
authorhoelzl
Thu Jan 31 17:42:12 2013 +0100 (2013-01-31)
changeset 51002496013a6eb38
parent 51001 461fdbbdb912
child 51003 198cb05fb35b
remove unnecessary assumption from real_normed_vector
NEWS
src/HOL/Complex.thy
src/HOL/Library/FrechetDeriv.thy
src/HOL/Library/Inner_Product.thy
src/HOL/Library/Product_Vector.thy
src/HOL/Library/Product_plus.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/RealVector.thy
     1.1 --- a/NEWS	Thu Jan 31 12:09:07 2013 +0100
     1.2 +++ b/NEWS	Thu Jan 31 17:42:12 2013 +0100
     1.3 @@ -4,6 +4,12 @@
     1.4  New in this Isabelle version
     1.5  ----------------------------
     1.6  
     1.7 +*** HOL ***
     1.8 +
     1.9 +* Theory "RealVector" and "Limits": Introduce type class
    1.10 +(lin)order_topology. Allows to generalize theorems about limits and
    1.11 +order. Instances are reals and extended reals.
    1.12 +
    1.13  
    1.14  New in Isabelle2013 (February 2013)
    1.15  -----------------------------------
     2.1 --- a/src/HOL/Complex.thy	Thu Jan 31 12:09:07 2013 +0100
     2.2 +++ b/src/HOL/Complex.thy	Thu Jan 31 17:42:12 2013 +0100
     2.3 @@ -288,8 +288,6 @@
     2.4  
     2.5  instance proof
     2.6    fix r :: real and x y :: complex and S :: "complex set"
     2.7 -  show "0 \<le> norm x"
     2.8 -    by (induct x) simp
     2.9    show "(norm x = 0) = (x = 0)"
    2.10      by (induct x) simp
    2.11    show "norm (x + y) \<le> norm x + norm y"
     3.1 --- a/src/HOL/Library/FrechetDeriv.thy	Thu Jan 31 12:09:07 2013 +0100
     3.2 +++ b/src/HOL/Library/FrechetDeriv.thy	Thu Jan 31 17:42:12 2013 +0100
     3.3 @@ -5,7 +5,7 @@
     3.4  header {* Frechet Derivative *}
     3.5  
     3.6  theory FrechetDeriv
     3.7 -imports Complex_Main
     3.8 +imports "~~/src/HOL/Complex_Main"
     3.9  begin
    3.10  
    3.11  definition
     4.1 --- a/src/HOL/Library/Inner_Product.thy	Thu Jan 31 12:09:07 2013 +0100
     4.2 +++ b/src/HOL/Library/Inner_Product.thy	Thu Jan 31 17:42:12 2013 +0100
     4.3 @@ -117,8 +117,6 @@
     4.4  subclass real_normed_vector
     4.5  proof
     4.6    fix a :: real and x y :: 'a
     4.7 -  show "0 \<le> norm x"
     4.8 -    unfolding norm_eq_sqrt_inner by simp
     4.9    show "norm x = 0 \<longleftrightarrow> x = 0"
    4.10      unfolding norm_eq_sqrt_inner by simp
    4.11    show "norm (x + y) \<le> norm x + norm y"
     5.1 --- a/src/HOL/Library/Product_Vector.thy	Thu Jan 31 12:09:07 2013 +0100
     5.2 +++ b/src/HOL/Library/Product_Vector.thy	Thu Jan 31 17:42:12 2013 +0100
     5.3 @@ -408,8 +408,6 @@
     5.4  
     5.5  instance proof
     5.6    fix r :: real and x y :: "'a \<times> 'b"
     5.7 -  show "0 \<le> norm x"
     5.8 -    unfolding norm_prod_def by simp
     5.9    show "norm x = 0 \<longleftrightarrow> x = 0"
    5.10      unfolding norm_prod_def
    5.11      by (simp add: prod_eq_iff)
     6.1 --- a/src/HOL/Library/Product_plus.thy	Thu Jan 31 12:09:07 2013 +0100
     6.2 +++ b/src/HOL/Library/Product_plus.thy	Thu Jan 31 17:42:12 2013 +0100
     6.3 @@ -5,7 +5,7 @@
     6.4  header {* Additive group operations on product types *}
     6.5  
     6.6  theory Product_plus
     6.7 -imports Main
     6.8 +imports "~~/src/HOL/Main"
     6.9  begin
    6.10  
    6.11  subsection {* Operations *}
     7.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 31 12:09:07 2013 +0100
     7.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Jan 31 17:42:12 2013 +0100
     7.3 @@ -387,9 +387,6 @@
     7.4  
     7.5  instance proof
     7.6    fix a :: real and x y :: "'a ^ 'b"
     7.7 -  show "0 \<le> norm x"
     7.8 -    unfolding norm_vec_def
     7.9 -    by (rule setL2_nonneg)
    7.10    show "norm x = 0 \<longleftrightarrow> x = 0"
    7.11      unfolding norm_vec_def
    7.12      by (simp add: setL2_eq_0_iff vec_eq_iff)
     8.1 --- a/src/HOL/RealVector.thy	Thu Jan 31 12:09:07 2013 +0100
     8.2 +++ b/src/HOL/RealVector.thy	Thu Jan 31 17:42:12 2013 +0100
     8.3 @@ -725,10 +725,20 @@
     8.4    assumes dist_norm: "dist x y = norm (x - y)"
     8.5  
     8.6  class real_normed_vector = real_vector + sgn_div_norm + dist_norm + open_dist +
     8.7 -  assumes norm_ge_zero [simp]: "0 \<le> norm x"
     8.8 -  and norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
     8.9 +  assumes norm_eq_zero [simp]: "norm x = 0 \<longleftrightarrow> x = 0"
    8.10    and norm_triangle_ineq: "norm (x + y) \<le> norm x + norm y"
    8.11    and norm_scaleR [simp]: "norm (scaleR a x) = \<bar>a\<bar> * norm x"
    8.12 +begin
    8.13 +
    8.14 +lemma norm_ge_zero [simp]: "0 \<le> norm x"
    8.15 +proof -
    8.16 +  have "0 = norm (x + -1 *\<^sub>R x)" 
    8.17 +    using scaleR_add_left[of 1 "-1" x] norm_scaleR[of 0 x] by (simp add: scaleR_one)
    8.18 +  also have "\<dots> \<le> norm x + norm (-1 *\<^sub>R x)" by (rule norm_triangle_ineq)
    8.19 +  finally show ?thesis by simp
    8.20 +qed
    8.21 +
    8.22 +end
    8.23  
    8.24  class real_normed_algebra = real_algebra + real_normed_vector +
    8.25    assumes norm_mult_ineq: "norm (x * y) \<le> norm x * norm y"
    8.26 @@ -954,7 +964,6 @@
    8.27  apply (rule dist_real_def)
    8.28  apply (rule open_real_def)
    8.29  apply (simp add: sgn_real_def)
    8.30 -apply (rule abs_ge_zero)
    8.31  apply (rule abs_eq_0)
    8.32  apply (rule abs_triangle_ineq)
    8.33  apply (rule abs_mult)