src/HOL/Real/HahnBanach/FunctionNorm.thy

 *}
 
 constdefs
   B :: "'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> ('a::{plus, minus, zero} \<Rightarrow> real) \<Rightarrow> real set"
   "B V norm f \<equiv>
-  {Numeral0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
+  {0} \<union> {\<bar>f x\<bar> * inverse (norm x) | x. x \<noteq> 0 \<and> x \<in> V}"
 
 text {*
   @{text n} is the function norm of @{text f}, iff @{text n} is the
   supremum of @{text B}.
 *}

   "function_norm f V norm \<equiv> Sup UNIV (B V norm f)"
 
 syntax
   function_norm :: "('a \<Rightarrow> real) \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> real) \<Rightarrow> real"  ("\<parallel>_\<parallel>_,_")
 
-lemma B_not_empty: "Numeral0 \<in> B V norm f"
+lemma B_not_empty: "0 \<in> B V norm f"
   by (unfold B_def) blast
 
 text {*
   The following lemma states that every continuous linear form on a
   normed space @{text "(V, \<parallel>\<cdot>\<parallel>)"} has a function norm.

 
     txt {* First we have to show that @{text B} is non-empty: *}
 
     show "\<exists>X. X \<in> B V norm f"
     proof
-      show "Numeral0 \<in> (B V norm f)" by (unfold B_def) blast
+      show "0 \<in> (B V norm f)" by (unfold B_def) blast
     qed
 
     txt {* Then we have to show that @{text B} is bounded: *}
 
     from e show "\<exists>Y. isUb UNIV (B V norm f) Y"
     proof
 
       txt {* We know that @{text f} is bounded by some value @{text c}. *}
 
       fix c assume a: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-      def b \<equiv> "max c Numeral0"
+      def b \<equiv> "max c 0"
 
       show "?thesis"
       proof (intro exI isUbI setleI ballI, unfold B_def,
         elim UnE CollectE exE conjE singletonE)
 

         constant @{text b}, such that @{text "y \<le> b"} for all
         @{text "y \<in> B"}. Due to the definition of @{text B} there are
         two cases for @{text "y \<in> B"}.  If @{text "y = 0"} then
         @{text "y \<le> max c 0"}: *}
 
-        fix y assume "y = (Numeral0::real)"
+        fix y assume "y = (0::real)"
         show "y \<le> b" by (simp! add: le_maxI2)
 
         txt {* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
         @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 

         fact that @{text f} is bounded. *}
 
         assume "y = \<bar>f x\<bar> * inverse (norm x)"
         also have "... \<le> c * norm x * inverse (norm x)"
         proof (rule real_mult_le_le_mono2)
-          show "Numeral0 \<le> inverse (norm x)"
-            by (rule order_less_imp_le, rule real_inverse_gt_zero1,
+          show "0 \<le> inverse (norm x)"
+            by (rule order_less_imp_le, rule real_inverse_gt_0,
                 rule normed_vs_norm_gt_zero)
           from a show "\<bar>f x\<bar> \<le> c * norm x" ..
         qed
         also have "... = c * (norm x * inverse (norm x))"
           by (rule real_mult_assoc)
-        also have "(norm x * inverse (norm x)) = (Numeral1::real)"
+        also have "(norm x * inverse (norm x)) = (1::real)"
         proof (rule real_mult_inv_right1)
-          show nz: "norm x \<noteq> Numeral0"
+          show nz: "norm x \<noteq> 0"
             by (rule not_sym, rule lt_imp_not_eq,
               rule normed_vs_norm_gt_zero)
         qed
         also have "c * ... \<le> b " by (simp! add: le_maxI1)
         finally show "y \<le> b" .

 
 text {* The norm of a continuous function is always @{text "\<ge> 0"}. *}
 
 lemma fnorm_ge_zero [intro?]:
   "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm
-   \<Longrightarrow> Numeral0 \<le> \<parallel>f\<parallel>V,norm"
+   \<Longrightarrow> 0 \<le> \<parallel>f\<parallel>V,norm"
 proof -
   assume c: "is_continuous V norm f"
      and n: "is_normed_vectorspace V norm"
 
   txt {* The function norm is defined as the supremum of @{text B}.

   @{text "\<ge> 0"}, provided the supremum exists and @{text B} is not
   empty. *}
 
   show ?thesis
   proof (unfold function_norm_def, rule sup_ub1)
-    show "\<forall>x \<in> (B V norm f). Numeral0 \<le> x"
+    show "\<forall>x \<in> (B V norm f). 0 \<le> x"
     proof (intro ballI, unfold B_def,
            elim UnE singletonE CollectE exE conjE)
       fix x r
       assume "x \<in> V"  "x \<noteq> 0"
         and r: "r = \<bar>f x\<bar> * inverse (norm x)"
 
-      have ge: "Numeral0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
-      have "Numeral0 \<le> inverse (norm x)"
-        by (rule order_less_imp_le, rule real_inverse_gt_zero1, rule)(***
+      have ge: "0 \<le> \<bar>f x\<bar>" by (simp! only: abs_ge_zero)
+      have "0 \<le> inverse (norm x)"
+        by (rule order_less_imp_le, rule real_inverse_gt_0, rule)(***
         proof (rule order_less_imp_le);
-          show "Numeral0 < inverse (norm x)";
+          show "0 < inverse (norm x)";
           proof (rule real_inverse_gt_zero);
-            show "Numeral0 < norm x"; ..;
+            show "0 < norm x"; ..;
           qed;
         qed; ***)
-      with ge show "Numeral0 \<le> r"
+      with ge show "0 \<le> r"
        by (simp only: r, rule real_le_mult_order1a)
     qed (simp!)
 
     txt {* Since @{text f} is continuous the function norm exists: *}
 

     thus "is_Sup UNIV (B V norm f) (Sup UNIV (B V norm f))"
       by (unfold is_function_norm_def function_norm_def)
 
     txt {* @{text B} is non-empty by construction: *}
 
-    show "Numeral0 \<in> B V norm f" by (rule B_not_empty)
+    show "0 \<in> B V norm f" by (rule B_not_empty)
   qed
 qed
 
 text {*
   \medskip The fundamental property of function norms is:

     linearity of @{text f}: for every linear function holds
     @{text "f 0 = 0"}. *}
 
     assume "x = 0"
     have "\<bar>f x\<bar> = \<bar>f 0\<bar>" by (simp!)
-    also from v continuous_linearform have "f 0 = Numeral0" ..
+    also from v continuous_linearform have "f 0 = 0" ..
     also note abs_zero
-    also have "Numeral0 \<le> \<parallel>f\<parallel>V,norm * norm x"
+    also have "0 \<le> \<parallel>f\<parallel>V,norm * norm x"
     proof (rule real_le_mult_order1a)
-      show "Numeral0 \<le> \<parallel>f\<parallel>V,norm" ..
-      show "Numeral0 \<le> norm x" ..
+      show "0 \<le> \<parallel>f\<parallel>V,norm" ..
+      show "0 \<le> norm x" ..
     qed
     finally
     show "\<bar>f x\<bar> \<le> \<parallel>f\<parallel>V,norm * norm x" .
 
   next
     assume "x \<noteq> 0"
-    have n: "Numeral0 < norm x" ..
-    hence nz: "norm x \<noteq> Numeral0"
+    have n: "0 < norm x" ..
+    hence nz: "norm x \<noteq> 0"
       by (simp only: lt_imp_not_eq)
 
     txt {* For the case @{text "x \<noteq> 0"} we derive the following fact
     from the definition of the function norm:*}
 

             conjI, simp)
     qed
 
     txt {* The thesis now follows by a short calculation: *}
 
-    have "\<bar>f x\<bar> = \<bar>f x\<bar> * Numeral1" by (simp!)
-    also from nz have "Numeral1 = inverse (norm x) * norm x"
+    have "\<bar>f x\<bar> = \<bar>f x\<bar> * 1" by (simp!)
+    also from nz have "1 = inverse (norm x) * norm x"
       by (simp add: real_mult_inv_left1)
     also have "\<bar>f x\<bar> * ... = \<bar>f x\<bar> * inverse (norm x) * norm x"
       by (simp! add: real_mult_assoc)
     also from n l have "... \<le> \<parallel>f\<parallel>V,norm * norm x"
       by (simp add: real_mult_le_le_mono2)

   \end{center}
 *}
 
 lemma fnorm_le_ub:
   "is_continuous V norm f \<Longrightarrow> is_normed_vectorspace V norm \<Longrightarrow>
-     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> Numeral0 \<le> c
+     \<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x \<Longrightarrow> 0 \<le> c
   \<Longrightarrow> \<parallel>f\<parallel>V,norm \<le> c"
 proof (unfold function_norm_def)
   assume "is_normed_vectorspace V norm"
   assume c: "is_continuous V norm f"
   assume fb: "\<forall>x \<in> V. \<bar>f x\<bar> \<le> c * norm x"
-    and "Numeral0 \<le> c"
+    and "0 \<le> c"
 
   txt {* Suppose the inequation holds for some @{text "c \<ge> 0"}.  If
   @{text c} is an upper bound of @{text B}, then @{text c} is greater
   than the function norm since the function norm is the least upper
   bound.  *}

       thus le: "y \<le> c"
       proof (unfold B_def, elim UnE CollectE exE conjE singletonE)
 
        txt {* The first case for @{text "y \<in> B"} is @{text "y = 0"}. *}
 
-        assume "y = Numeral0"
+        assume "y = 0"
         show "y \<le> c" by (blast!)
 
         txt{* The second case is @{text "y = \<bar>f x\<bar> / \<parallel>x\<parallel>"} for some
         @{text "x \<in> V"} with @{text "x \<noteq> 0"}. *}
 
       next
         fix x
         assume "x \<in> V"  "x \<noteq> 0"
 
-        have lz: "Numeral0 < norm x"
+        have lz: "0 < norm x"
           by (simp! add: normed_vs_norm_gt_zero)
 
-        have nz: "norm x \<noteq> Numeral0"
+        have nz: "norm x \<noteq> 0"
         proof (rule not_sym)
-          from lz show "Numeral0 \<noteq> norm x"
+          from lz show "0 \<noteq> norm x"
             by (simp! add: order_less_imp_not_eq)
         qed
 
-        from lz have "Numeral0 < inverse (norm x)"
-          by (simp! add: real_inverse_gt_zero1)
-        hence inverse_gez: "Numeral0 \<le> inverse (norm x)"
+        from lz have "0 < inverse (norm x)"
+          by (simp! add: real_inverse_gt_0)
+        hence inverse_gez: "0 \<le> inverse (norm x)"
           by (rule order_less_imp_le)
 
         assume "y = \<bar>f x\<bar> * inverse (norm x)"
         also from inverse_gez have "... \<le> c * norm x * inverse (norm x)"
           proof (rule real_mult_le_le_mono2)