src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy

     "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 0 \<longrightarrow> x \<bullet> i \<le> f x \<bullet> i"
     "\<forall>x. \<forall>i\<in>Basis. x \<in> unit_cube \<and> True \<and> label x i = 1 \<longrightarrow> f x \<bullet> i \<le> x \<bullet> i"
     using kuhn_labelling_lemma[OF *] by blast
   note label = this [rule_format]
   have lem1: "\<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>i\<in>Basis. label x i \<noteq> label y i \<longrightarrow>
-    abs (f x \<bullet> i - x \<bullet> i) \<le> norm (f y - f x) + norm (y - x)"
+    \<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
   proof safe
     fix x y :: 'a
     assume x: "x \<in> unit_cube"
     assume y: "y \<in> unit_cube"
     fix i
     assume i: "label x i \<noteq> label y i" "i \<in> Basis"
     have *: "\<And>x y fx fy :: real. x \<le> fx \<and> fy \<le> y \<or> fx \<le> x \<and> y \<le> fy \<Longrightarrow>
-      abs (fx - x) \<le> abs (fy - fx) + abs (y - x)" by auto
-    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> abs ((f y - f x)\<bullet>i) + abs ((y - x)\<bullet>i)"
+      \<bar>fx - x\<bar> \<le> \<bar>fy - fx\<bar> + \<bar>y - x\<bar>" by auto
+    have "\<bar>(f x - x) \<bullet> i\<bar> \<le> \<bar>(f y - f x)\<bullet>i\<bar> + \<bar>(y - x)\<bullet>i\<bar>"
       unfolding inner_simps
       apply (rule *)
       apply (cases "label x i = 0")
       apply (rule disjI1)
       apply rule

     finally show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y - f x) + norm (y - x)"
       unfolding inner_simps .
   qed
   have "\<exists>e>0. \<forall>x\<in>unit_cube. \<forall>y\<in>unit_cube. \<forall>z\<in>unit_cube. \<forall>i\<in>Basis.
     norm (x - z) < e \<and> norm (y - z) < e \<and> label x i \<noteq> label y i \<longrightarrow>
-      abs ((f(z) - z)\<bullet>i) < d / (real n)"
+      \<bar>(f(z) - z)\<bullet>i\<bar> < d / (real n)"
   proof -
     have d': "d / real n / 8 > 0"
       using d(1) by (simp add: n_def DIM_positive)
     have *: "uniformly_continuous_on unit_cube f"
       by (rule compact_uniformly_continuous[OF assms(1) compact_unit_cube])

         "x \<in> unit_cube" "y \<in> unit_cube" "z \<in> unit_cube"
         "norm (x - z) < min (e / 2) (d / real n / 8)"
         "norm (y - z) < min (e / 2) (d / real n / 8)"
         "label x i \<noteq> label y i"
       assume i: "i \<in> Basis"
-      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. abs(fx - x) \<le> n1 + n2 \<Longrightarrow>
-        abs (fx - fz) \<le> n3 \<Longrightarrow> abs (x - z) \<le> n4 \<Longrightarrow>
+      have *: "\<And>z fz x fx n1 n2 n3 n4 d4 d :: real. \<bar>fx - x\<bar> \<le> n1 + n2 \<Longrightarrow>
+        \<bar>fx - fz\<bar> \<le> n3 \<Longrightarrow> \<bar>x - z\<bar> \<le> n4 \<Longrightarrow>
         n1 < d4 \<Longrightarrow> n2 < 2 * d4 \<Longrightarrow> n3 < d4 \<Longrightarrow> n4 < d4 \<Longrightarrow>
-        (8 * d4 = d) \<Longrightarrow> abs(fz - z) < d"
+        (8 * d4 = d) \<Longrightarrow> \<bar>fz - z\<bar> < d"
         by auto
       show "\<bar>(f z - z) \<bullet> i\<bar> < d / real n"
         unfolding inner_simps
       proof (rule *)
         show "\<bar>f x \<bullet> i - x \<bullet> i\<bar> \<le> norm (f y -f x) + norm (y - x)"

                (\<forall>j<n. q j \<le> s j \<and> s j \<le> q j + 1) \<and>
                (label (\<Sum>i\<in>Basis. (real (r (b' i)) / real p) *\<^sub>R i) \<circ> b) i \<noteq>
                (label (\<Sum>i\<in>Basis. (real (s (b' i)) / real p) *\<^sub>R i) \<circ> b) i"
     by (rule kuhn_lemma[OF q1 q2 q3])
   def z \<equiv> "(\<Sum>i\<in>Basis. (real (q (b' i)) / real p) *\<^sub>R i)::'a"
-  have "\<exists>i\<in>Basis. d / real n \<le> abs ((f z - z)\<bullet>i)"
+  have "\<exists>i\<in>Basis. d / real n \<le> \<bar>(f z - z)\<bullet>i\<bar>"
   proof (rule ccontr)
     have "\<forall>i\<in>Basis. q (b' i) \<in> {0..p}"
       using q(1) b'
       by (auto intro: less_imp_le simp: bij_betw_def)
     then have "z \<in> unit_cube"