# HG changeset patch
# User wenzelm
# Date 1451262394 -3600
# Node ID 5d06ecfdb472e6a613cf0d66b4bcabd33c1cdb9e
# Parent  7fba644ed827e6bcde19bcd7f3ce4e72c8449ee4
prefer symbols for "abs";

diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Archimedean_Field.thy
--- a/src/HOL/Archimedean_Field.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Archimedean_Field.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -647,7 +647,7 @@
      
 lemma round_diff_minimal: 
   fixes z :: "'a :: floor_ceiling"
-  shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
+  shows "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
 proof (cases "of_int m \<ge> z")
   case True
   hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Complex.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -638,7 +638,7 @@
 lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
   by (auto simp: complex_is_Real_iff complex_eq_iff)
 
-lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
+lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
   by (simp add: complex_is_Real_iff norm_complex_def)
 
 lemma series_comparison_complex:
@@ -719,7 +719,7 @@
 lemma rcis_Ex: "\<exists>r a. z = rcis r a"
   by (simp add: complex_eq_iff polar_Ex)
 
-lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
+lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \<bar>r\<bar>"
   by (simp add: rcis_def norm_mult)
 
 lemma cis_rcis_eq: "cis a = rcis 1 a"
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Divides.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -2436,7 +2436,7 @@
   by (rule mod_int_unique [of a b q r],
     simp add: divmod_int_rel_def)
 
-lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
+lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
 by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
 
 text\<open>Suggested by Matthias Daum\<close>
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Fields.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1146,10 +1146,10 @@
   apply (simp add: order_less_imp_le)
 done
 
-lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)"
+lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a | b = 0)"
 by (auto simp: zero_le_divide_iff)
 
-lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)"
+lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
 by (auto simp: divide_le_0_iff)
 
 lemma field_le_mult_one_interval:
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/GCD.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -605,14 +605,14 @@
 definition
   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
 where
-  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
+  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
 definition
   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
 where
-  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
+  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
-instance proof qed
+instance ..
 
 end
 
@@ -676,16 +676,16 @@
   "gcd x (- numeral n :: int) = gcd x (numeral n)"
   by (fact gcd_neg2_int)
 
-lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
+lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
 by(simp add: gcd_int_def)
 
-lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
+lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
 by (simp add: gcd_int_def)
 
-lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
+lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
 by (metis abs_idempotent gcd_abs_int)
 
-lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
+lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
 by (metis abs_idempotent gcd_abs_int)
 
 lemma gcd_cases_int:
@@ -695,7 +695,7 @@
       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   shows "P (gcd x y)"
-by (insert assms, auto, arith)
+  by (insert assms, auto, arith)
 
 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   by (simp add: gcd_int_def)
@@ -706,17 +706,17 @@
 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   by (simp add: lcm_int_def)
 
-lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
+lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
   by (simp add: lcm_int_def)
 
-lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
-by(simp add:lcm_int_def)
+lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
+  by (simp add:lcm_int_def)
 
-lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
-by (metis abs_idempotent lcm_int_def)
+lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
+  by (metis abs_idempotent lcm_int_def)
 
-lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
-by (metis abs_idempotent lcm_int_def)
+lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
+  by (metis abs_idempotent lcm_int_def)
 
 lemma lcm_cases_int:
   fixes x :: int and y
@@ -735,13 +735,13 @@
   by simp
 
 (* was igcd_0, etc. *)
-lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
+lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   by (unfold gcd_int_def, auto)
 
 lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
   by simp
 
-lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
+lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
   by (unfold gcd_int_def, auto)
 
 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
@@ -764,7 +764,7 @@
 lemma gcd_idem_nat: "gcd (x::nat) x = x"
 by simp
 
-lemma gcd_idem_int: "gcd (x::int) x = abs x"
+lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
 by (auto simp add: gcd_int_def)
 
 declare gcd_nat.simps [simp del]
@@ -882,10 +882,10 @@
 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   by (fact gcd_nat.absorb2)
 
-lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
+lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
 
-lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
+lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   by (metis gcd_proj1_if_dvd_int gcd_commute_int)
 
 text \<open>
@@ -900,7 +900,7 @@
   apply (simp_all add: gcd_non_0_nat)
 done
 
-lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
+lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   apply (subst (1 2) gcd_abs_int)
   apply (subst (1 2) abs_mult)
   apply (rule gcd_mult_distrib_nat [transferred])
@@ -1064,8 +1064,8 @@
 lemma finite_divisors_int[simp]:
   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
 proof-
-  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
-  hence "finite{d. abs d <= abs i}" by simp
+  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
+  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
   from finite_subset[OF _ this] show ?thesis using assms
     by (simp add: dvd_imp_le_int subset_iff)
 qed
@@ -1076,7 +1076,7 @@
 apply simp
 done
 
-lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
+lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
 apply(rule antisym)
  apply(rule Max_le_iff [THEN iffD2])
   apply (auto intro: abs_le_D1 dvd_imp_le_int)
@@ -1507,7 +1507,7 @@
   by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
 
 lemma coprime_common_divisor_int:
-  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
+  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   using gcd_greatest_iff [of x a b] by auto
 
 lemma coprime_divisors_nat:
@@ -1763,7 +1763,7 @@
 
 subsection \<open>LCM properties\<close>
 
-lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
+lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   by (simp add: lcm_int_def lcm_nat_def zdiv_int
     of_nat_mult gcd_int_def)
 
@@ -1771,7 +1771,7 @@
   unfolding lcm_nat_def
   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
 
-lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
+lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   unfolding lcm_int_def gcd_int_def
   apply (subst int_mult [symmetric])
   apply (subst prod_gcd_lcm_nat [symmetric])
@@ -1871,7 +1871,7 @@
   apply auto
 done
 
-lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
+lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
   apply (rule sym)
   apply (subst lcm_unique_int [symmetric])
   apply auto
@@ -1880,7 +1880,7 @@
 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
 
-lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
+lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
 
 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
@@ -1889,10 +1889,10 @@
 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
 
-lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
+lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
 
-lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
+lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
 
 lemma (in semiring_gcd) comp_fun_idem_gcd:
@@ -2162,7 +2162,7 @@
   "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   by (fact Lcm_insert)
 
-lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
+lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   by (fact dvd_int_unfold_dvd_nat)
 
 lemma dvd_Lcm_int [simp]:
@@ -2223,7 +2223,7 @@
   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
 by transfer(fact gcd_code_int)
 
-lemma lcm_code_integer [code]: "lcm (a::integer) b = (abs a) * (abs b) div gcd a b"
+lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
 by transfer(fact lcm_altdef_int)
 
 end
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Groups.thy
--- a/src/HOL/Groups.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Groups.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1203,13 +1203,7 @@
 end
 
 class abs =
-  fixes abs :: "'a \<Rightarrow> 'a"
-begin
-
-notation (xsymbols)
-  abs  ("\<bar>_\<bar>")
-
-end
+  fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
 
 class sgn =
   fixes sgn :: "'a \<Rightarrow> 'a"
@@ -1375,7 +1369,7 @@
 lemma dense_eq0_I:
   fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
   shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
-  apply (cases "abs x=0", simp)
+  apply (cases "\<bar>x\<bar> = 0", simp)
   apply (simp only: zero_less_abs_iff [symmetric])
   apply (drule dense)
   apply (auto simp add: not_less [symmetric])
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -780,7 +780,7 @@
 
 lemma setsum_abs[iff]: 
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
-  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
+  shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
 proof (cases "finite A")
   case True
   thus ?thesis
@@ -796,12 +796,12 @@
 
 lemma setsum_abs_ge_zero[iff]:
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
-  shows "0 \<le> setsum (%i. abs(f i)) A"
+  shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
   by (simp add: setsum_nonneg)
 
 lemma abs_setsum_abs[simp]: 
   fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
-  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
+  shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
 proof (cases "finite A")
   case True
   thus ?thesis
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Int.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -529,7 +529,7 @@
       in theory \<open>Rings\<close>.
       But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
 lemma abs_split [arith_split, no_atp]:
-     "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
+     "P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
 by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
 
 lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
@@ -944,7 +944,7 @@
 apply (rule_tac [2] nat_mult_distrib, auto)
 done
 
-lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
+lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
 apply (cases "z=0 | w=0")
 apply (auto simp add: abs_if nat_mult_distrib [symmetric]
                       nat_mult_distrib_neg [symmetric] mult_less_0_iff)
@@ -1115,7 +1115,7 @@
 subsection\<open>Intermediate value theorems\<close>
 
 lemma int_val_lemma:
-     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
+     "(\<forall>i<n::nat. \<bar>f(i+1) - f i\<bar> \<le> 1) -->
       f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
 unfolding One_nat_def
 apply (induct n)
@@ -1133,7 +1133,7 @@
 lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
 
 lemma nat_intermed_int_val:
-     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
+     "[| \<forall>i. m \<le> i & i < n --> \<bar>f(i + 1::nat) - f i\<bar> \<le> 1; m < n;
          f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
 apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
        in int_val_lemma)
@@ -1432,10 +1432,10 @@
   from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
 qed
 
-lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
+lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \<bar>z\<bar>)"
   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
 
-lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
+lemma dvd_int_iff: "(z dvd int m) = (nat \<bar>z\<bar> dvd m)"
   unfolding zdvd_int by (cases "z \<ge> 0") simp_all
 
 lemma dvd_int_unfold_dvd_nat:
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/MacLaurin.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -259,8 +259,8 @@
 
 lemma Maclaurin_bi_le:
    assumes "diff 0 = f"
-   and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
-   shows "\<exists>t. abs t \<le> abs x &
+   and DERIV : "\<forall>m t::real. m < n & \<bar>t\<bar> \<le> \<bar>x\<bar> --> DERIV (diff m) t :> diff (Suc m) t"
+   shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
               f x =
               (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
      diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
@@ -294,7 +294,7 @@
   fixes x::real
   assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
   and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
-  shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
+  shows "\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> & f x =
     (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
                 (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
 proof (cases rule: linorder_cases)
@@ -320,7 +320,7 @@
      "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
       x ~= 0 & n > 0
-      --> (\<exists>t. 0 < abs t & abs t < abs x &
+      --> (\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> &
                f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
                      (diff n t / (fact n)) * x ^ n)"
 by (blast intro: Maclaurin_all_lt)
@@ -336,7 +336,7 @@
 lemma Maclaurin_all_le:
   assumes INIT: "diff 0 = f"
   and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
-  shows "\<exists>t. abs t \<le> abs x & f x =
+  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> & f x =
     (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
     (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
 proof cases
@@ -363,7 +363,7 @@
 lemma Maclaurin_all_le_objl:
   "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
-      --> (\<exists>t::real. abs t \<le> abs x &
+      --> (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
               f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
                     (diff n t / (fact n)) * x ^ n)"
 by (blast intro: Maclaurin_all_le)
@@ -375,15 +375,15 @@
   fixes x::real
   shows
   "[| x ~= 0; n > 0 |]
-      ==> (\<exists>t. 0 < abs t &
-                abs t < abs x &
+      ==> (\<exists>t. 0 < \<bar>t\<bar> &
+                \<bar>t\<bar> < \<bar>x\<bar> &
                 exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
                         (exp t / (fact n)) * x ^ n)"
 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
 
 
 lemma Maclaurin_exp_le:
-     "\<exists>t::real. abs t \<le> abs x &
+     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
             exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
                        (exp t / (fact n)) * x ^ n"
 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
@@ -422,7 +422,7 @@
 by (simp only: cos_add sin_add of_nat_Suc add_divide_distrib distrib_right, auto)
 
 lemma Maclaurin_sin_expansion2:
-     "\<exists>t. abs t \<le> abs x &
+     "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
        sin x =
        (\<Sum>m<n. sin_coeff m * x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
@@ -495,7 +495,7 @@
 by (simp only: cos_add sin_add of_nat_Suc distrib_right add_divide_distrib, auto)
 
 lemma Maclaurin_cos_expansion:
-     "\<exists>t::real. abs t \<le> abs x &
+     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
        cos x =
        (\<Sum>m<n. cos_coeff m * x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
@@ -550,12 +550,11 @@
 (* ------------------------------------------------------------------------- *)
 
 lemma sin_bound_lemma:
-    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
+    "[|x = y; \<bar>u\<bar> \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
 by auto
 
 lemma Maclaurin_sin_bound:
-  "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
-  \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
+  "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
 proof -
   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
     by (rule_tac mult_right_mono,simp_all)
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Nitpick.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -122,11 +122,12 @@
 function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
   "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
   by auto
-  termination
+termination
   apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
    apply auto
    apply (metis mod_less_divisor xt1(9))
-  by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
+  apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
+  done
 
 declare nat_gcd.simps[simp del]
 
@@ -134,10 +135,10 @@
   "nat_lcm x y = x * y div (nat_gcd x y)"
 
 definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"
+  "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
 definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
-  "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"
+  "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
   "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/NthRoot.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -10,7 +10,7 @@
 imports Deriv Binomial
 begin
 
-lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
+lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
   by (simp add: sgn_real_def)
 
 lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Num.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -954,14 +954,13 @@
   "\<not> 1 < - 1"
   by (simp_all add: less_le)
 
-lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
+lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
   by simp
 
-lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
+lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
   by (simp only: abs_minus_cancel abs_numeral)
 
-lemma abs_neg_one [simp]:
-  "abs (- 1) = 1"
+lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
   by simp
 
 end
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Power.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -622,24 +622,20 @@
 context linordered_idom
 begin
 
-lemma power_abs:
-  "abs (a ^ n) = abs a ^ n"
+lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
   by (induct n) (auto simp add: abs_mult)
 
-lemma abs_power_minus [simp]:
-  "abs ((-a) ^ n) = abs (a ^ n)"
+lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   by (simp add: power_abs)
 
-lemma zero_less_power_abs_iff [simp]:
-  "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
+lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
 proof (induct n)
   case 0 show ?case by simp
 next
   case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff)
 qed
 
-lemma zero_le_power_abs [simp]:
-  "0 \<le> abs a ^ n"
+lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   by (rule zero_le_power [OF abs_ge_zero])
 
 lemma zero_le_power2 [simp]:
@@ -658,12 +654,10 @@
   "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   by (simp add: le_less)
 
-lemma abs_power2 [simp]:
-  "abs (a\<^sup>2) = a\<^sup>2"
+lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   by (simp add: power2_eq_square abs_mult abs_mult_self)
 
-lemma power2_abs [simp]:
-  "(abs a)\<^sup>2 = a\<^sup>2"
+lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   by (simp add: power2_eq_square abs_mult_self)
 
 lemma odd_power_less_zero:
@@ -729,14 +723,14 @@
     by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
 qed
 
-lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
+lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   using abs_le_square_iff [of x 1]
   by simp
 
-lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
+lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   by (auto simp add: abs_if power2_eq_1_iff)
 
-lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
+lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
   by (auto simp add: le_less)
 
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Presburger.thy
--- a/src/HOL/Presburger.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Presburger.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -211,11 +211,11 @@
 
 subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
 
-lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
-by(induct rule: int_gr_induct,simp_all add:int_distrib)
+lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (\<bar>x - z\<bar> + 1) * d < z"
+  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
 
-lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
-by(induct rule: int_gr_induct, simp_all add:int_distrib)
+lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (\<bar>x - z\<bar> + 1) * d"
+  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
 
 lemma decr_mult_lemma:
   assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
@@ -241,7 +241,7 @@
   assume eP1: "EX x. P1 x"
   then obtain x where P1: "P1 x" ..
   from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
-  let ?w = "x - (abs(x-z)+1) * d"
+  let ?w = "x - (\<bar>x - z\<bar> + 1) * d"
   from dpos have w: "?w < z" by(rule decr_lemma)
   have "P1 x = P1 ?w" using P1eqP1 by blast
   also have "\<dots> = P(?w)" using w P1eqP by blast
@@ -287,8 +287,8 @@
   assume eP1: "EX x. P' x"
   then obtain x where P1: "P' x" ..
   from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
-  let ?w' = "x + (abs(x-z)+1) * d"
-  let ?w = "x - (-(abs(x-z) + 1))*d"
+  let ?w' = "x + (\<bar>x - z\<bar> + 1) * d"
+  let ?w = "x - (- (\<bar>x - z\<bar> + 1)) * d"
   have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps)
   from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   hence "P' x = P' ?w" using P1eqP1 by blast
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Rat.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -451,7 +451,7 @@
   "x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y"
 
 definition
-  "abs (a::rat) = (if a < 0 then - a else a)"
+  "\<bar>a::rat\<bar> = (if a < 0 then - a else a)"
 
 definition
   "sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Real.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -593,7 +593,7 @@
   "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
 
 definition
-  "abs (a::real) = (if a < 0 then - a else a)"
+  "\<bar>a::real\<bar> = (if a < 0 then - a else a)"
 
 definition
   "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
@@ -1037,7 +1037,7 @@
 declare of_int_1_less_iff [algebra, presburger]
 declare of_int_1_le_iff [algebra, presburger]
 
-lemma of_int_abs [simp]: "of_int (abs x) = (abs(of_int x) :: 'a::linordered_idom)"
+lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = (\<bar>of_int x\<bar> :: 'a::linordered_idom)"
   by (auto simp add: abs_if)
 
 lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
@@ -1199,7 +1199,7 @@
 proof -
   from \<open>x \<in> \<rat>\<close> obtain i::int and n::nat where "n \<noteq> 0" and "x = real_of_int i / real n"
     by(auto simp add: Rats_eq_int_div_nat)
-  hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by (simp add: of_nat_nat)
+  hence "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by (simp add: of_nat_nat)
   then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
   let ?gcd = "gcd m n"
   from \<open>n\<noteq>0\<close> have gcd: "?gcd \<noteq> 0" by simp
@@ -1414,17 +1414,17 @@
 
 subsection\<open>Absolute Value Function for the Reals\<close>
 
-lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
-by (simp add: abs_if)
+lemma abs_minus_add_cancel: "\<bar>x + (- y)\<bar> = \<bar>y + (- (x::real))\<bar>"
+  by (simp add: abs_if)
 
-lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
-by (simp add: abs_if)
+lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>"
+  by (simp add: abs_if)
 
-lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
-by simp
+lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x"
+  by simp
 
-lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
-by simp
+lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (-l + -m)\<bar> \<le> \<bar>x + -l\<bar> + \<bar>y + -m\<bar>"
+  by simp
 
 
 subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Rings.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1559,7 +1559,7 @@
 lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
   by (simp add: not_less)
 
-proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
+proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: split_if_asm)
 
 end
diff -r 7fba644ed827 -r 5d06ecfdb472 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Dec 27 22:07:17 2015 +0100
+++ b/src/HOL/Transcendental.thy	Mon Dec 28 01:26:34 2015 +0100
@@ -1872,7 +1872,7 @@
   done
 
 lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
-  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
+  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= x\<^sup>2"
 proof -
   assume x: "0 <= x"
   assume x1: "x <= 1"
@@ -1880,7 +1880,7 @@
     by (rule ln_add_one_self_le_self)
   then have "ln (1 + x) - x <= 0"
     by simp
-  then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
+  then have "\<bar>ln(1 + x) - x\<bar> = - (ln(1 + x) - x)"
     by (rule abs_of_nonpos)
   also have "... = x - ln (1 + x)"
     by simp
@@ -1895,11 +1895,11 @@
 qed
 
 lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
-  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
+  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
 proof -
   assume a: "-(1 / 2) <= x"
   assume b: "x <= 0"
-  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
+  have "\<bar>ln (1 + x) - x\<bar> = x - ln(1 - (-x))"
     apply (subst abs_of_nonpos)
     apply simp
     apply (rule ln_add_one_self_le_self2)
@@ -1915,7 +1915,7 @@
 qed
 
 lemma abs_ln_one_plus_x_minus_x_bound:
-  fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
+  fixes x::real shows "\<bar>x\<bar> <= 1 / 2 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
   apply (case_tac "0 <= x")
   apply (rule order_trans)
   apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
@@ -2648,7 +2648,7 @@
   fixes x :: real
   shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
 proof (rule filterlim_mono_eventually)
-  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
+  from reals_Archimedean2 [of "\<bar>x\<bar>"] obtain n :: nat where *: "real n > \<bar>x\<bar>" ..
   hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
     apply (intro eventually_sequentiallyI [of n])
     apply (case_tac "x \<ge> 0")
@@ -3100,7 +3100,7 @@
   by (simp add: power2_eq_square)
 
 lemma sin_cos_le1:
-  fixes x::real shows "abs (sin x * sin y + cos x * cos y) \<le> 1"
+  fixes x::real shows "\<bar>sin x * sin y + cos x * cos y\<bar> \<le> 1"
   using cos_diff [of x y]
   by (metis abs_cos_le_one add.commute)
 
@@ -4225,11 +4225,11 @@
 lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
   using less_eq_real_def tan_gt_zero by auto
 
-lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
+lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   using cos_gt_zero_pi [of x]
   by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
 
-lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
+lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
   by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
 
@@ -4244,7 +4244,7 @@
          \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
   by (meson tan_mono_le not_le tan_monotone)
 
-lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
+lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
   using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
   by (auto simp: abs_if split: split_if_asm)
 
@@ -4404,7 +4404,7 @@
 lemma arcsin_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin(-x) = -arcsin x"
   by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
 
-lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
+lemma arcsin_eq_iff: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
   by (metis abs_le_iff arcsin minus_le_iff)
 
 lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
@@ -4820,13 +4820,13 @@
     done
 qed
 
-lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
+lemma arcsin_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
   apply (rule trans [OF sin_mono_less_eq [symmetric]])
   using arcsin_ubound arcsin_lbound
   apply auto
   done
 
-lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
+lemma arcsin_le_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
   using arcsin_less_mono not_le by blast
 
 lemma arcsin_less_arcsin: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x < arcsin y"
@@ -4835,13 +4835,13 @@
 lemma arcsin_le_arcsin: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
   using arcsin_le_mono by auto
 
-lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
+lemma arccos_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
   apply (rule trans [OF cos_mono_less_eq [symmetric]])
   using arccos_ubound arccos_lbound
   apply auto
   done
 
-lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
+lemma arccos_le_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
   using arccos_less_mono [of y x]
   by (simp add: not_le [symmetric])
 
@@ -4851,7 +4851,7 @@
 lemma arccos_le_arccos: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> arccos x"
   using arccos_le_mono by auto
 
-lemma arccos_eq_iff: "abs x \<le> 1 & abs y \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
+lemma arccos_eq_iff: "\<bar>x\<bar> \<le> 1 & \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
   using cos_arccos_abs by fastforce
 
 subsection \<open>Machins formula\<close>