src/HOL/Real/HahnBanach/NormedSpace.thy

 *}
 
 constdefs
   is_seminorm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
   "is_seminorm V norm \<equiv> \<forall>x \<in> V. \<forall>y \<in> V. \<forall>a.
-        #0 \<le> norm x
+        Numeral0 \<le> norm x
       \<and> norm (a \<cdot> x) = \<bar>a\<bar> * norm x
       \<and> norm (x + y) \<le> norm x + norm y"
 
 lemma is_seminormI [intro]:
-  "(\<And>x y a. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> #0 \<le> norm x) \<Longrightarrow>
+  "(\<And>x y a. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> Numeral0 \<le> norm x) \<Longrightarrow>
   (\<And>x a. x \<in> V \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x) \<Longrightarrow>
   (\<And>x y. x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> norm (x + y) \<le> norm x + norm y)
   \<Longrightarrow> is_seminorm V norm"
   by (unfold is_seminorm_def) auto
 
 lemma seminorm_ge_zero [intro?]:
-  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> Numeral0 \<le> norm x"
   by (unfold is_seminorm_def) blast
 
 lemma seminorm_abs_homogenous:
   "is_seminorm V norm \<Longrightarrow> x \<in> V
   \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"

 lemma seminorm_diff_subadditive:
   "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> is_vectorspace V
   \<Longrightarrow> norm (x - y) \<le> 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)"
+  have "norm (x - y) = norm (x + - Numeral1 \<cdot> y)"
     by (simp! add: diff_eq2 negate_eq2a)
-  also have "... \<le> norm x + norm  (- #1 \<cdot> y)"
+  also have "... \<le> norm x + norm  (- Numeral1 \<cdot> y)"
     by (simp! add: seminorm_subadditive)
-  also have "norm (- #1 \<cdot> y) = \<bar>- #1\<bar> * norm y"
+  also have "norm (- Numeral1 \<cdot> y) = \<bar>- Numeral1\<bar> * norm y"
     by (rule seminorm_abs_homogenous)
-  also have "\<bar>- #1\<bar> = (#1::real)" by (rule abs_minus_one)
+  also have "\<bar>- Numeral1\<bar> = (Numeral1::real)" by (rule abs_minus_one)
   finally show "norm (x - y) \<le> norm x + norm y" by simp
 qed
 
 lemma seminorm_minus:
   "is_seminorm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_vectorspace V
   \<Longrightarrow> 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 "... = \<bar>- #1\<bar> * norm x"
+  have "norm (- x) = norm (- Numeral1 \<cdot> x)" by (simp! only: negate_eq1)
+  also have "... = \<bar>- Numeral1\<bar> * norm x"
     by (rule seminorm_abs_homogenous)
-  also have "\<bar>- #1\<bar> = (#1::real)" by (rule abs_minus_one)
+  also have "\<bar>- Numeral1\<bar> = (Numeral1::real)" by (rule abs_minus_one)
   finally show "norm (- x) = norm x" by simp
 qed
 
 
 subsection {* Norms *}

 *}
 
 constdefs
   is_norm :: "'a::{plus, minus, zero} set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> bool"
   "is_norm V norm \<equiv> \<forall>x \<in> V. is_seminorm V norm
-      \<and> (norm x = #0) = (x = 0)"
+      \<and> (norm x = Numeral0) = (x = 0)"
 
 lemma is_normI [intro]:
-  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = #0) = (x = 0)
+  "\<forall>x \<in> V.  is_seminorm V norm  \<and> (norm x = Numeral0) = (x = 0)
   \<Longrightarrow> is_norm V norm" by (simp only: is_norm_def)
 
 lemma norm_is_seminorm [intro?]:
   "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> is_seminorm V norm"
   by (unfold is_norm_def) blast
 
 lemma norm_zero_iff:
-  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> (norm x = #0) = (x = 0)"
+  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> (norm x = Numeral0) = (x = 0)"
   by (unfold is_norm_def) blast
 
 lemma norm_ge_zero [intro?]:
-  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  "is_norm V norm \<Longrightarrow> x \<in> V \<Longrightarrow> Numeral0 \<le> norm x"
   by (unfold is_norm_def is_seminorm_def) blast
 
 
 subsection {* Normed vector spaces *}
 

 lemma normed_vs_norm [intro?]:
   "is_normed_vectorspace V norm \<Longrightarrow> is_norm V norm"
   by (unfold is_normed_vectorspace_def) blast
 
 lemma normed_vs_norm_ge_zero [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> #0 \<le> norm x"
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> Numeral0 \<le> norm x"
   by (unfold is_normed_vectorspace_def) (fast elim: norm_ge_zero)
 
 lemma normed_vs_norm_gt_zero [intro?]:
-  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> #0 < norm x"
+  "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V \<Longrightarrow> x \<noteq> 0 \<Longrightarrow> Numeral0 < 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 \<le> norm x" ..
-  also have "#0 \<noteq> norm x"
+  have "Numeral0 \<le> norm x" ..
+  also have "Numeral0 \<noteq> norm x"
   proof
-    presume "norm x = #0"
+    presume "norm x = Numeral0"
     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" .
+  finally show "Numeral0 < norm x" .
 qed
 
 lemma normed_vs_norm_abs_homogenous [intro?]:
   "is_normed_vectorspace V norm \<Longrightarrow> x \<in> V
   \<Longrightarrow> norm (a \<cdot> x) = \<bar>a\<bar> * norm x"

   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 \<le> norm x" ..
+      show "Numeral0 \<le> norm x" ..
       show "norm (a \<cdot> x) = \<bar>a\<bar> * norm x" ..
       presume "y \<in> E"
       show "norm (x + y) \<le> norm x + norm y" ..
     qed (simp!)+
 
     fix x assume "x \<in> F"
-    show "(norm x = #0) = (x = 0)"
+    show "(norm x = Numeral0) = (x = 0)"
     proof (rule norm_zero_iff)
       show "is_norm E norm" ..
     qed (simp!)
   qed
 qed