(*  Title:      HOL/Real/HahnBanach/NormedSpace.thy

     ID:         $Id$

     Author:     Gertrud Bauer, TU Munich

 *)

 header {* Normed vector spaces *}

 theory NormedSpace =  Subspace:

 syntax 

   abs :: "real \<Rightarrow> real" ("|_|")

 subsection {* Quasinorms *}

 text{* A \emph{seminorm} $\norm{\cdot}$ is a function on a real vector

 space into the reals that has the following properties: It is positive

 definite, absolute homogenous and subadditive.  *}

 constdefs

   is_seminorm :: "['a::{plus, minus, zero} set, 'a => real] => bool"

   "is_seminorm V norm == \<forall>x \<in>  V. \<forall>y \<in> V. \<forall>a. 

         #0 <= norm x 

       \<and> norm (a \<cdot> x) = |a| * norm x

       \<and> norm (x + y) <= norm x + norm y"

 lemma is_seminormI [intro]: 

   "[| !! x y a. [| x \<in> V; y \<in> V|] ==> #0 <= norm x;

   !! x a. x \<in> V ==> norm (a \<cdot> x) = |a| * norm x;

   !! x y. [|x \<in> V; y \<in> V |] ==> norm (x + y) <= norm x + norm y |] 

   ==> is_seminorm V norm"

   by (unfold is_seminorm_def, force)

 lemma seminorm_ge_zero [intro?]:

   "[| is_seminorm V norm; x \<in> V |] ==> #0 <= norm x"

   by (unfold is_seminorm_def, force)

 lemma seminorm_abs_homogenous: 

   "[| is_seminorm V norm; x \<in> V |] 

   ==> norm (a \<cdot> x) = |a| * norm x"

   by (unfold is_seminorm_def, force)

 lemma seminorm_subadditive: 

   "[| is_seminorm V norm; x \<in> V; y \<in> V |] 

   ==> norm (x + y) <= norm x + norm y"

   by (unfold is_seminorm_def, force)

 lemma seminorm_diff_subadditive: 

   "[| is_seminorm V norm; x \<in> V; y \<in> V; is_vectorspace V |] 

   ==> norm (x - y) <= norm x + norm y"

 proof -

   assume "is_seminorm V norm" "x \<in> V" "y \<in> V" "is_vectorspace V"

   have "norm (x - y) = norm (x + - #1 \<cdot> y)"  

     by (simp! add: diff_eq2 negate_eq2a)

   also have "... <= norm x + norm  (- #1 \<cdot> y)" 

     by (simp! add: seminorm_subadditive)

   also have "norm (- #1 \<cdot> y) = |- #1| * norm y" 

     by (rule seminorm_abs_homogenous)

   also have "|- #1| = (#1::real)" by (rule abs_minus_one)

   finally show "norm (x - y) <= norm x + norm y" by simp

 qed

 lemma seminorm_minus: 

   "[| is_seminorm V norm; x \<in> V; is_vectorspace V |] 

   ==> norm (- x) = norm x"

 proof -

   assume "is_seminorm V norm" "x \<in> V" "is_vectorspace V"

   have "norm (- x) = norm (- #1 \<cdot> x)" by (simp! only: negate_eq1)

   also have "... = |- #1| * norm x" 

     by (rule seminorm_abs_homogenous)

   also have "|- #1| = (#1::real)" by (rule abs_minus_one)

   finally show "norm (- x) = norm x" by simp

 qed

 subsection {* Norms *}

 text{* A \emph{norm} $\norm{\cdot}$ is a seminorm that maps only the

 $\zero$ vector to $0$. *}

 constdefs

   is_norm :: "['a::{plus, minus, zero} set, 'a => real] => bool"

   "is_norm V norm == \<forall>x \<in> V.  is_seminorm V norm 

       \<and> (norm x = #0) = (x = 0)"

 lemma is_normI [intro]: 

   "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0) 

   ==> is_norm V norm" by (simp only: is_norm_def)

 lemma norm_is_seminorm [intro?]: 

   "[| is_norm V norm; x \<in> V |] ==> is_seminorm V norm"

   by (unfold is_norm_def, force)

 lemma norm_zero_iff: 

   "[| is_norm V norm; x \<in> V |] ==> (norm x = #0) = (x = 0)"

   by (unfold is_norm_def, force)

 lemma norm_ge_zero [intro?]:

   "[|is_norm V norm; x \<in> V |] ==> #0 <= norm x"

   by (unfold is_norm_def is_seminorm_def, force)

 subsection {* Normed vector spaces *}

 text{* A vector space together with a norm is called

 a \emph{normed space}. *}

 constdefs

   is_normed_vectorspace :: 

   "['a::{plus, minus, zero} set, 'a => real] => bool"

   "is_normed_vectorspace V norm ==

       is_vectorspace V \<and> is_norm V norm"

 lemma normed_vsI [intro]: 

   "[| is_vectorspace V; is_norm V norm |] 

   ==> is_normed_vectorspace V norm"

   by (unfold is_normed_vectorspace_def) blast 

 lemma normed_vs_vs [intro?]: 

   "is_normed_vectorspace V norm ==> is_vectorspace V"

   by (unfold is_normed_vectorspace_def) force

 lemma normed_vs_norm [intro?]: 

   "is_normed_vectorspace V norm ==> is_norm V norm"

   by (unfold is_normed_vectorspace_def, elim conjE)

 lemma normed_vs_norm_ge_zero [intro?]: 

   "[| is_normed_vectorspace V norm; x \<in> V |] ==> #0 <= norm x"

   by (unfold is_normed_vectorspace_def, rule, elim conjE)

 lemma normed_vs_norm_gt_zero [intro?]: 

   "[| is_normed_vectorspace V norm; x \<in> V; x \<noteq> 0 |] ==> #0 < norm x"

 proof (unfold is_normed_vectorspace_def, elim conjE)

   assume "x \<in> V" "x \<noteq> 0" "is_vectorspace V" "is_norm V norm"

   have "#0 <= norm x" ..

   also have "#0 \<noteq> norm x"

   proof

     presume "norm x = #0"

     also have "?this = (x = 0)" by (rule norm_zero_iff)

     finally have "x = 0" .

     thus "False" by contradiction

   qed (rule sym)

   finally show "#0 < norm x" .

 qed

 lemma normed_vs_norm_abs_homogenous [intro?]: 

   "[| is_normed_vectorspace V norm; x \<in> V |] 

   ==> norm (a \<cdot> x) = |a| * norm x"

   by (rule seminorm_abs_homogenous, rule norm_is_seminorm, 

       rule normed_vs_norm)

 lemma normed_vs_norm_subadditive [intro?]: 

   "[| is_normed_vectorspace V norm; x \<in> V; y \<in> V |] 

   ==> norm (x + y) <= norm x + norm y"

   by (rule seminorm_subadditive, rule norm_is_seminorm, 

      rule normed_vs_norm)

 text{* Any subspace of a normed vector space is again a 

 normed vectorspace.*}

 lemma subspace_normed_vs [intro?]: 

   "[| is_vectorspace E; is_subspace F E;

   is_normed_vectorspace E norm |] ==> is_normed_vectorspace F norm"

 proof (rule normed_vsI)

   assume "is_subspace F E" "is_vectorspace E" 

          "is_normed_vectorspace E norm"

   show "is_vectorspace F" ..

   show "is_norm F norm" 

   proof (intro is_normI ballI conjI)

     show "is_seminorm F norm" 

     proof

       fix x y a presume "x \<in> E"

       show "#0 <= norm x" ..

       show "norm (a \<cdot> x) = |a| * norm x" ..

       presume "y \<in> E"

       show "norm (x + y) <= norm x + norm y" ..

     qed (simp!)+

     fix x assume "x \<in> F"

     show "(norm x = #0) = (x = 0)" 

     proof (rule norm_zero_iff)

       show "is_norm E norm" ..

     qed (simp!)

   qed

 qed

 end