prefer symbols for "abs";
authorwenzelm
Mon Dec 28 01:26:34 2015 +0100 (2015-12-28)
changeset 619445d06ecfdb472
parent 61943 7fba644ed827
child 61945 1135b8de26c3
prefer symbols for "abs";
src/HOL/Archimedean_Field.thy
src/HOL/Complex.thy
src/HOL/Divides.thy
src/HOL/Fields.thy
src/HOL/GCD.thy
src/HOL/Groups.thy
src/HOL/Groups_Big.thy
src/HOL/Int.thy
src/HOL/MacLaurin.thy
src/HOL/Nitpick.thy
src/HOL/NthRoot.thy
src/HOL/Num.thy
src/HOL/Power.thy
src/HOL/Presburger.thy
src/HOL/Rat.thy
src/HOL/Real.thy
src/HOL/Rings.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Archimedean_Field.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Archimedean_Field.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -647,7 +647,7 @@
     1.4       
     1.5  lemma round_diff_minimal: 
     1.6    fixes z :: "'a :: floor_ceiling"
     1.7 -  shows "abs (z - of_int (round z)) \<le> abs (z - of_int m)"
     1.8 +  shows "\<bar>z - of_int (round z)\<bar> \<le> \<bar>z - of_int m\<bar>"
     1.9  proof (cases "of_int m \<ge> z")
    1.10    case True
    1.11    hence "\<bar>z - of_int (round z)\<bar> \<le> \<bar>of_int \<lceil>z\<rceil> - z\<bar>"
     2.1 --- a/src/HOL/Complex.thy	Sun Dec 27 22:07:17 2015 +0100
     2.2 +++ b/src/HOL/Complex.thy	Mon Dec 28 01:26:34 2015 +0100
     2.3 @@ -638,7 +638,7 @@
     2.4  lemma Reals_cnj_iff: "z \<in> \<real> \<longleftrightarrow> cnj z = z"
     2.5    by (auto simp: complex_is_Real_iff complex_eq_iff)
     2.6  
     2.7 -lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm(z) = abs(Re z)"
     2.8 +lemma in_Reals_norm: "z \<in> \<real> \<Longrightarrow> norm z = \<bar>Re z\<bar>"
     2.9    by (simp add: complex_is_Real_iff norm_complex_def)
    2.10  
    2.11  lemma series_comparison_complex:
    2.12 @@ -719,7 +719,7 @@
    2.13  lemma rcis_Ex: "\<exists>r a. z = rcis r a"
    2.14    by (simp add: complex_eq_iff polar_Ex)
    2.15  
    2.16 -lemma complex_mod_rcis [simp]: "cmod(rcis r a) = abs r"
    2.17 +lemma complex_mod_rcis [simp]: "cmod (rcis r a) = \<bar>r\<bar>"
    2.18    by (simp add: rcis_def norm_mult)
    2.19  
    2.20  lemma cis_rcis_eq: "cis a = rcis 1 a"
     3.1 --- a/src/HOL/Divides.thy	Sun Dec 27 22:07:17 2015 +0100
     3.2 +++ b/src/HOL/Divides.thy	Mon Dec 28 01:26:34 2015 +0100
     3.3 @@ -2436,7 +2436,7 @@
     3.4    by (rule mod_int_unique [of a b q r],
     3.5      simp add: divmod_int_rel_def)
     3.6  
     3.7 -lemma abs_div: "(y::int) dvd x \<Longrightarrow> abs (x div y) = abs x div abs y"
     3.8 +lemma abs_div: "(y::int) dvd x \<Longrightarrow> \<bar>x div y\<bar> = \<bar>x\<bar> div \<bar>y\<bar>"
     3.9  by (unfold dvd_def, cases "y=0", auto simp add: abs_mult)
    3.10  
    3.11  text\<open>Suggested by Matthias Daum\<close>
     4.1 --- a/src/HOL/Fields.thy	Sun Dec 27 22:07:17 2015 +0100
     4.2 +++ b/src/HOL/Fields.thy	Mon Dec 28 01:26:34 2015 +0100
     4.3 @@ -1146,10 +1146,10 @@
     4.4    apply (simp add: order_less_imp_le)
     4.5  done
     4.6  
     4.7 -lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / abs b) = (0 \<le> a | b = 0)"
     4.8 +lemma zero_le_divide_abs_iff [simp]: "(0 \<le> a / \<bar>b\<bar>) = (0 \<le> a | b = 0)"
     4.9  by (auto simp: zero_le_divide_iff)
    4.10  
    4.11 -lemma divide_le_0_abs_iff [simp]: "(a / abs b \<le> 0) = (a \<le> 0 | b = 0)"
    4.12 +lemma divide_le_0_abs_iff [simp]: "(a / \<bar>b\<bar> \<le> 0) = (a \<le> 0 | b = 0)"
    4.13  by (auto simp: divide_le_0_iff)
    4.14  
    4.15  lemma field_le_mult_one_interval:
     5.1 --- a/src/HOL/GCD.thy	Sun Dec 27 22:07:17 2015 +0100
     5.2 +++ b/src/HOL/GCD.thy	Mon Dec 28 01:26:34 2015 +0100
     5.3 @@ -605,14 +605,14 @@
     5.4  definition
     5.5    gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
     5.6  where
     5.7 -  "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))"
     5.8 +  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
     5.9  
    5.10  definition
    5.11    lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
    5.12  where
    5.13 -  "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))"
    5.14 +  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
    5.15  
    5.16 -instance proof qed
    5.17 +instance ..
    5.18  
    5.19  end
    5.20  
    5.21 @@ -676,16 +676,16 @@
    5.22    "gcd x (- numeral n :: int) = gcd x (numeral n)"
    5.23    by (fact gcd_neg2_int)
    5.24  
    5.25 -lemma abs_gcd_int[simp]: "abs(gcd (x::int) y) = gcd x y"
    5.26 +lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    5.27  by(simp add: gcd_int_def)
    5.28  
    5.29 -lemma gcd_abs_int: "gcd (x::int) y = gcd (abs x) (abs y)"
    5.30 +lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
    5.31  by (simp add: gcd_int_def)
    5.32  
    5.33 -lemma gcd_abs1_int[simp]: "gcd (abs x) (y::int) = gcd x y"
    5.34 +lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    5.35  by (metis abs_idempotent gcd_abs_int)
    5.36  
    5.37 -lemma gcd_abs2_int[simp]: "gcd x (abs y::int) = gcd x y"
    5.38 +lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    5.39  by (metis abs_idempotent gcd_abs_int)
    5.40  
    5.41  lemma gcd_cases_int:
    5.42 @@ -695,7 +695,7 @@
    5.43        and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
    5.44        and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
    5.45    shows "P (gcd x y)"
    5.46 -by (insert assms, auto, arith)
    5.47 +  by (insert assms, auto, arith)
    5.48  
    5.49  lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
    5.50    by (simp add: gcd_int_def)
    5.51 @@ -706,17 +706,17 @@
    5.52  lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
    5.53    by (simp add: lcm_int_def)
    5.54  
    5.55 -lemma lcm_abs_int: "lcm (x::int) y = lcm (abs x) (abs y)"
    5.56 +lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
    5.57    by (simp add: lcm_int_def)
    5.58  
    5.59 -lemma abs_lcm_int [simp]: "abs (lcm i j::int) = lcm i j"
    5.60 -by(simp add:lcm_int_def)
    5.61 +lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
    5.62 +  by (simp add:lcm_int_def)
    5.63  
    5.64 -lemma lcm_abs1_int[simp]: "lcm (abs x) (y::int) = lcm x y"
    5.65 -by (metis abs_idempotent lcm_int_def)
    5.66 +lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    5.67 +  by (metis abs_idempotent lcm_int_def)
    5.68  
    5.69 -lemma lcm_abs2_int[simp]: "lcm x (abs y::int) = lcm x y"
    5.70 -by (metis abs_idempotent lcm_int_def)
    5.71 +lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    5.72 +  by (metis abs_idempotent lcm_int_def)
    5.73  
    5.74  lemma lcm_cases_int:
    5.75    fixes x :: int and y
    5.76 @@ -735,13 +735,13 @@
    5.77    by simp
    5.78  
    5.79  (* was igcd_0, etc. *)
    5.80 -lemma gcd_0_int [simp]: "gcd (x::int) 0 = abs x"
    5.81 +lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
    5.82    by (unfold gcd_int_def, auto)
    5.83  
    5.84  lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
    5.85    by simp
    5.86  
    5.87 -lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = abs x"
    5.88 +lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
    5.89    by (unfold gcd_int_def, auto)
    5.90  
    5.91  lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
    5.92 @@ -764,7 +764,7 @@
    5.93  lemma gcd_idem_nat: "gcd (x::nat) x = x"
    5.94  by simp
    5.95  
    5.96 -lemma gcd_idem_int: "gcd (x::int) x = abs x"
    5.97 +lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
    5.98  by (auto simp add: gcd_int_def)
    5.99  
   5.100  declare gcd_nat.simps [simp del]
   5.101 @@ -882,10 +882,10 @@
   5.102  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   5.103    by (fact gcd_nat.absorb2)
   5.104  
   5.105 -lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = abs x"
   5.106 +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   5.107    by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   5.108  
   5.109 -lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = abs y"
   5.110 +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   5.111    by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   5.112  
   5.113  text \<open>
   5.114 @@ -900,7 +900,7 @@
   5.115    apply (simp_all add: gcd_non_0_nat)
   5.116  done
   5.117  
   5.118 -lemma gcd_mult_distrib_int: "abs (k::int) * gcd m n = gcd (k * m) (k * n)"
   5.119 +lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   5.120    apply (subst (1 2) gcd_abs_int)
   5.121    apply (subst (1 2) abs_mult)
   5.122    apply (rule gcd_mult_distrib_nat [transferred])
   5.123 @@ -1064,8 +1064,8 @@
   5.124  lemma finite_divisors_int[simp]:
   5.125    assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
   5.126  proof-
   5.127 -  have "{d. abs d <= abs i} = {- abs i .. abs i}" by(auto simp:abs_if)
   5.128 -  hence "finite{d. abs d <= abs i}" by simp
   5.129 +  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
   5.130 +  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
   5.131    from finite_subset[OF _ this] show ?thesis using assms
   5.132      by (simp add: dvd_imp_le_int subset_iff)
   5.133  qed
   5.134 @@ -1076,7 +1076,7 @@
   5.135  apply simp
   5.136  done
   5.137  
   5.138 -lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = abs n"
   5.139 +lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
   5.140  apply(rule antisym)
   5.141   apply(rule Max_le_iff [THEN iffD2])
   5.142    apply (auto intro: abs_le_D1 dvd_imp_le_int)
   5.143 @@ -1507,7 +1507,7 @@
   5.144    by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   5.145  
   5.146  lemma coprime_common_divisor_int:
   5.147 -  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
   5.148 +  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   5.149    using gcd_greatest_iff [of x a b] by auto
   5.150  
   5.151  lemma coprime_divisors_nat:
   5.152 @@ -1763,7 +1763,7 @@
   5.153  
   5.154  subsection \<open>LCM properties\<close>
   5.155  
   5.156 -lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
   5.157 +lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   5.158    by (simp add: lcm_int_def lcm_nat_def zdiv_int
   5.159      of_nat_mult gcd_int_def)
   5.160  
   5.161 @@ -1771,7 +1771,7 @@
   5.162    unfolding lcm_nat_def
   5.163    by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
   5.164  
   5.165 -lemma prod_gcd_lcm_int: "abs(m::int) * abs n = gcd m n * lcm m n"
   5.166 +lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
   5.167    unfolding lcm_int_def gcd_int_def
   5.168    apply (subst int_mult [symmetric])
   5.169    apply (subst prod_gcd_lcm_nat [symmetric])
   5.170 @@ -1871,7 +1871,7 @@
   5.171    apply auto
   5.172  done
   5.173  
   5.174 -lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = abs y"
   5.175 +lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
   5.176    apply (rule sym)
   5.177    apply (subst lcm_unique_int [symmetric])
   5.178    apply auto
   5.179 @@ -1880,7 +1880,7 @@
   5.180  lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   5.181  by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
   5.182  
   5.183 -lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = abs y"
   5.184 +lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   5.185  by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
   5.186  
   5.187  lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   5.188 @@ -1889,10 +1889,10 @@
   5.189  lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   5.190  by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
   5.191  
   5.192 -lemma lcm_proj1_iff_int[simp]: "lcm m n = abs(m::int) \<longleftrightarrow> n dvd m"
   5.193 +lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   5.194  by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
   5.195  
   5.196 -lemma lcm_proj2_iff_int[simp]: "lcm m n = abs(n::int) \<longleftrightarrow> m dvd n"
   5.197 +lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   5.198  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   5.199  
   5.200  lemma (in semiring_gcd) comp_fun_idem_gcd:
   5.201 @@ -2162,7 +2162,7 @@
   5.202    "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   5.203    by (fact Lcm_insert)
   5.204  
   5.205 -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
   5.206 +lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   5.207    by (fact dvd_int_unfold_dvd_nat)
   5.208  
   5.209  lemma dvd_Lcm_int [simp]:
   5.210 @@ -2223,7 +2223,7 @@
   5.211    "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   5.212  by transfer(fact gcd_code_int)
   5.213  
   5.214 -lemma lcm_code_integer [code]: "lcm (a::integer) b = (abs a) * (abs b) div gcd a b"
   5.215 +lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   5.216  by transfer(fact lcm_altdef_int)
   5.217  
   5.218  end
     6.1 --- a/src/HOL/Groups.thy	Sun Dec 27 22:07:17 2015 +0100
     6.2 +++ b/src/HOL/Groups.thy	Mon Dec 28 01:26:34 2015 +0100
     6.3 @@ -1203,13 +1203,7 @@
     6.4  end
     6.5  
     6.6  class abs =
     6.7 -  fixes abs :: "'a \<Rightarrow> 'a"
     6.8 -begin
     6.9 -
    6.10 -notation (xsymbols)
    6.11 -  abs  ("\<bar>_\<bar>")
    6.12 -
    6.13 -end
    6.14 +  fixes abs :: "'a \<Rightarrow> 'a"  ("\<bar>_\<bar>")
    6.15  
    6.16  class sgn =
    6.17    fixes sgn :: "'a \<Rightarrow> 'a"
    6.18 @@ -1375,7 +1369,7 @@
    6.19  lemma dense_eq0_I:
    6.20    fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}"
    6.21    shows "(\<And>e. 0 < e \<Longrightarrow> \<bar>x\<bar> \<le> e) ==> x = 0"
    6.22 -  apply (cases "abs x=0", simp)
    6.23 +  apply (cases "\<bar>x\<bar> = 0", simp)
    6.24    apply (simp only: zero_less_abs_iff [symmetric])
    6.25    apply (drule dense)
    6.26    apply (auto simp add: not_less [symmetric])
     7.1 --- a/src/HOL/Groups_Big.thy	Sun Dec 27 22:07:17 2015 +0100
     7.2 +++ b/src/HOL/Groups_Big.thy	Mon Dec 28 01:26:34 2015 +0100
     7.3 @@ -780,7 +780,7 @@
     7.4  
     7.5  lemma setsum_abs[iff]: 
     7.6    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
     7.7 -  shows "abs (setsum f A) \<le> setsum (%i. abs(f i)) A"
     7.8 +  shows "\<bar>setsum f A\<bar> \<le> setsum (%i. \<bar>f i\<bar>) A"
     7.9  proof (cases "finite A")
    7.10    case True
    7.11    thus ?thesis
    7.12 @@ -796,12 +796,12 @@
    7.13  
    7.14  lemma setsum_abs_ge_zero[iff]:
    7.15    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    7.16 -  shows "0 \<le> setsum (%i. abs(f i)) A"
    7.17 +  shows "0 \<le> setsum (%i. \<bar>f i\<bar>) A"
    7.18    by (simp add: setsum_nonneg)
    7.19  
    7.20  lemma abs_setsum_abs[simp]: 
    7.21    fixes f :: "'a => ('b::ordered_ab_group_add_abs)"
    7.22 -  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
    7.23 +  shows "\<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar> = (\<Sum>a\<in>A. \<bar>f a\<bar>)"
    7.24  proof (cases "finite A")
    7.25    case True
    7.26    thus ?thesis
     8.1 --- a/src/HOL/Int.thy	Sun Dec 27 22:07:17 2015 +0100
     8.2 +++ b/src/HOL/Int.thy	Mon Dec 28 01:26:34 2015 +0100
     8.3 @@ -529,7 +529,7 @@
     8.4        in theory \<open>Rings\<close>.
     8.5        But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
     8.6  lemma abs_split [arith_split, no_atp]:
     8.7 -     "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
     8.8 +     "P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
     8.9  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    8.10  
    8.11  lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
    8.12 @@ -944,7 +944,7 @@
    8.13  apply (rule_tac [2] nat_mult_distrib, auto)
    8.14  done
    8.15  
    8.16 -lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
    8.17 +lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
    8.18  apply (cases "z=0 | w=0")
    8.19  apply (auto simp add: abs_if nat_mult_distrib [symmetric]
    8.20                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
    8.21 @@ -1115,7 +1115,7 @@
    8.22  subsection\<open>Intermediate value theorems\<close>
    8.23  
    8.24  lemma int_val_lemma:
    8.25 -     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
    8.26 +     "(\<forall>i<n::nat. \<bar>f(i+1) - f i\<bar> \<le> 1) -->
    8.27        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
    8.28  unfolding One_nat_def
    8.29  apply (induct n)
    8.30 @@ -1133,7 +1133,7 @@
    8.31  lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
    8.32  
    8.33  lemma nat_intermed_int_val:
    8.34 -     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
    8.35 +     "[| \<forall>i. m \<le> i & i < n --> \<bar>f(i + 1::nat) - f i\<bar> \<le> 1; m < n;
    8.36           f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
    8.37  apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
    8.38         in int_val_lemma)
    8.39 @@ -1432,10 +1432,10 @@
    8.40    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
    8.41  qed
    8.42  
    8.43 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    8.44 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \<bar>z\<bar>)"
    8.45    unfolding zdvd_int by (cases "z \<ge> 0") simp_all
    8.46  
    8.47 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    8.48 +lemma dvd_int_iff: "(z dvd int m) = (nat \<bar>z\<bar> dvd m)"
    8.49    unfolding zdvd_int by (cases "z \<ge> 0") simp_all
    8.50  
    8.51  lemma dvd_int_unfold_dvd_nat:
     9.1 --- a/src/HOL/MacLaurin.thy	Sun Dec 27 22:07:17 2015 +0100
     9.2 +++ b/src/HOL/MacLaurin.thy	Mon Dec 28 01:26:34 2015 +0100
     9.3 @@ -259,8 +259,8 @@
     9.4  
     9.5  lemma Maclaurin_bi_le:
     9.6     assumes "diff 0 = f"
     9.7 -   and DERIV : "\<forall>m t::real. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t"
     9.8 -   shows "\<exists>t. abs t \<le> abs x &
     9.9 +   and DERIV : "\<forall>m t::real. m < n & \<bar>t\<bar> \<le> \<bar>x\<bar> --> DERIV (diff m) t :> diff (Suc m) t"
    9.10 +   shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    9.11                f x =
    9.12                (\<Sum>m<n. diff m 0 / (fact m) * x ^ m) +
    9.13       diff n t / (fact n) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
    9.14 @@ -294,7 +294,7 @@
    9.15    fixes x::real
    9.16    assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \<noteq> 0"
    9.17    and DERIV: "\<forall>m x. DERIV (diff m) x :> diff(Suc m) x"
    9.18 -  shows "\<exists>t. 0 < abs t & abs t < abs x & f x =
    9.19 +  shows "\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> & f x =
    9.20      (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    9.21                  (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> _ \<and> f x = ?f x t")
    9.22  proof (cases rule: linorder_cases)
    9.23 @@ -320,7 +320,7 @@
    9.24       "diff 0 = f &
    9.25        (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
    9.26        x ~= 0 & n > 0
    9.27 -      --> (\<exists>t. 0 < abs t & abs t < abs x &
    9.28 +      --> (\<exists>t. 0 < \<bar>t\<bar> & \<bar>t\<bar> < \<bar>x\<bar> &
    9.29                 f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    9.30                       (diff n t / (fact n)) * x ^ n)"
    9.31  by (blast intro: Maclaurin_all_lt)
    9.32 @@ -336,7 +336,7 @@
    9.33  lemma Maclaurin_all_le:
    9.34    assumes INIT: "diff 0 = f"
    9.35    and DERIV: "\<forall>m x::real. DERIV (diff m) x :> diff (Suc m) x"
    9.36 -  shows "\<exists>t. abs t \<le> abs x & f x =
    9.37 +  shows "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> & f x =
    9.38      (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    9.39      (diff n t / (fact n)) * x ^ n" (is "\<exists>t. _ \<and> f x = ?f x t")
    9.40  proof cases
    9.41 @@ -363,7 +363,7 @@
    9.42  lemma Maclaurin_all_le_objl:
    9.43    "diff 0 = f &
    9.44        (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
    9.45 -      --> (\<exists>t::real. abs t \<le> abs x &
    9.46 +      --> (\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    9.47                f x = (\<Sum>m<n. (diff m 0 / (fact m)) * x ^ m) +
    9.48                      (diff n t / (fact n)) * x ^ n)"
    9.49  by (blast intro: Maclaurin_all_le)
    9.50 @@ -375,15 +375,15 @@
    9.51    fixes x::real
    9.52    shows
    9.53    "[| x ~= 0; n > 0 |]
    9.54 -      ==> (\<exists>t. 0 < abs t &
    9.55 -                abs t < abs x &
    9.56 +      ==> (\<exists>t. 0 < \<bar>t\<bar> &
    9.57 +                \<bar>t\<bar> < \<bar>x\<bar> &
    9.58                  exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
    9.59                          (exp t / (fact n)) * x ^ n)"
    9.60  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
    9.61  
    9.62  
    9.63  lemma Maclaurin_exp_le:
    9.64 -     "\<exists>t::real. abs t \<le> abs x &
    9.65 +     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    9.66              exp x = (\<Sum>m<n. (x ^ m) / (fact m)) +
    9.67                         (exp t / (fact n)) * x ^ n"
    9.68  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
    9.69 @@ -422,7 +422,7 @@
    9.70  by (simp only: cos_add sin_add of_nat_Suc add_divide_distrib distrib_right, auto)
    9.71  
    9.72  lemma Maclaurin_sin_expansion2:
    9.73 -     "\<exists>t. abs t \<le> abs x &
    9.74 +     "\<exists>t. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    9.75         sin x =
    9.76         (\<Sum>m<n. sin_coeff m * x ^ m)
    9.77        + ((sin(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
    9.78 @@ -495,7 +495,7 @@
    9.79  by (simp only: cos_add sin_add of_nat_Suc distrib_right add_divide_distrib, auto)
    9.80  
    9.81  lemma Maclaurin_cos_expansion:
    9.82 -     "\<exists>t::real. abs t \<le> abs x &
    9.83 +     "\<exists>t::real. \<bar>t\<bar> \<le> \<bar>x\<bar> &
    9.84         cos x =
    9.85         (\<Sum>m<n. cos_coeff m * x ^ m)
    9.86        + ((cos(t + 1/2 * real (n) *pi) / (fact n)) * x ^ n)"
    9.87 @@ -550,12 +550,11 @@
    9.88  (* ------------------------------------------------------------------------- *)
    9.89  
    9.90  lemma sin_bound_lemma:
    9.91 -    "[|x = y; abs u \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    9.92 +    "[|x = y; \<bar>u\<bar> \<le> (v::real) |] ==> \<bar>(x + u) - y\<bar> \<le> v"
    9.93  by auto
    9.94  
    9.95  lemma Maclaurin_sin_bound:
    9.96 -  "abs(sin x - (\<Sum>m<n. sin_coeff m * x ^ m))
    9.97 -  \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
    9.98 +  "\<bar>sin x - (\<Sum>m<n. sin_coeff m * x ^ m)\<bar> \<le> inverse((fact n)) * \<bar>x\<bar> ^ n"
    9.99  proof -
   9.100    have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
   9.101      by (rule_tac mult_right_mono,simp_all)
    10.1 --- a/src/HOL/Nitpick.thy	Sun Dec 27 22:07:17 2015 +0100
    10.2 +++ b/src/HOL/Nitpick.thy	Mon Dec 28 01:26:34 2015 +0100
    10.3 @@ -122,11 +122,12 @@
    10.4  function nat_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
    10.5    "nat_gcd x y = (if y = 0 then x else nat_gcd y (x mod y))"
    10.6    by auto
    10.7 -  termination
    10.8 +termination
    10.9    apply (relation "measure (\<lambda>(x, y). x + y + (if y > x then 1 else 0))")
   10.10     apply auto
   10.11     apply (metis mod_less_divisor xt1(9))
   10.12 -  by (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
   10.13 +  apply (metis mod_mod_trivial mod_self nat_neq_iff xt1(10))
   10.14 +  done
   10.15  
   10.16  declare nat_gcd.simps[simp del]
   10.17  
   10.18 @@ -134,10 +135,10 @@
   10.19    "nat_lcm x y = x * y div (nat_gcd x y)"
   10.20  
   10.21  definition int_gcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   10.22 -  "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))"
   10.23 +  "int_gcd x y = int (nat_gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   10.24  
   10.25  definition int_lcm :: "int \<Rightarrow> int \<Rightarrow> int" where
   10.26 -  "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))"
   10.27 +  "int_lcm x y = int (nat_lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   10.28  
   10.29  definition Frac :: "int \<times> int \<Rightarrow> bool" where
   10.30    "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> int_gcd a b = 1"
    11.1 --- a/src/HOL/NthRoot.thy	Sun Dec 27 22:07:17 2015 +0100
    11.2 +++ b/src/HOL/NthRoot.thy	Mon Dec 28 01:26:34 2015 +0100
    11.3 @@ -10,7 +10,7 @@
    11.4  imports Deriv Binomial
    11.5  begin
    11.6  
    11.7 -lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
    11.8 +lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
    11.9    by (simp add: sgn_real_def)
   11.10  
   11.11  lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
    12.1 --- a/src/HOL/Num.thy	Sun Dec 27 22:07:17 2015 +0100
    12.2 +++ b/src/HOL/Num.thy	Mon Dec 28 01:26:34 2015 +0100
    12.3 @@ -954,14 +954,13 @@
    12.4    "\<not> 1 < - 1"
    12.5    by (simp_all add: less_le)
    12.6  
    12.7 -lemma abs_numeral [simp]: "abs (numeral n) = numeral n"
    12.8 +lemma abs_numeral [simp]: "\<bar>numeral n\<bar> = numeral n"
    12.9    by simp
   12.10  
   12.11 -lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n"
   12.12 +lemma abs_neg_numeral [simp]: "\<bar>- numeral n\<bar> = numeral n"
   12.13    by (simp only: abs_minus_cancel abs_numeral)
   12.14  
   12.15 -lemma abs_neg_one [simp]:
   12.16 -  "abs (- 1) = 1"
   12.17 +lemma abs_neg_one [simp]: "\<bar>- 1\<bar> = 1"
   12.18    by simp
   12.19  
   12.20  end
    13.1 --- a/src/HOL/Power.thy	Sun Dec 27 22:07:17 2015 +0100
    13.2 +++ b/src/HOL/Power.thy	Mon Dec 28 01:26:34 2015 +0100
    13.3 @@ -622,24 +622,20 @@
    13.4  context linordered_idom
    13.5  begin
    13.6  
    13.7 -lemma power_abs:
    13.8 -  "abs (a ^ n) = abs a ^ n"
    13.9 +lemma power_abs: "\<bar>a ^ n\<bar> = \<bar>a\<bar> ^ n"
   13.10    by (induct n) (auto simp add: abs_mult)
   13.11  
   13.12 -lemma abs_power_minus [simp]:
   13.13 -  "abs ((-a) ^ n) = abs (a ^ n)"
   13.14 +lemma abs_power_minus [simp]: "\<bar>(-a) ^ n\<bar> = \<bar>a ^ n\<bar>"
   13.15    by (simp add: power_abs)
   13.16  
   13.17 -lemma zero_less_power_abs_iff [simp]:
   13.18 -  "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   13.19 +lemma zero_less_power_abs_iff [simp]: "0 < \<bar>a\<bar> ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
   13.20  proof (induct n)
   13.21    case 0 show ?case by simp
   13.22  next
   13.23    case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff)
   13.24  qed
   13.25  
   13.26 -lemma zero_le_power_abs [simp]:
   13.27 -  "0 \<le> abs a ^ n"
   13.28 +lemma zero_le_power_abs [simp]: "0 \<le> \<bar>a\<bar> ^ n"
   13.29    by (rule zero_le_power [OF abs_ge_zero])
   13.30  
   13.31  lemma zero_le_power2 [simp]:
   13.32 @@ -658,12 +654,10 @@
   13.33    "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
   13.34    by (simp add: le_less)
   13.35  
   13.36 -lemma abs_power2 [simp]:
   13.37 -  "abs (a\<^sup>2) = a\<^sup>2"
   13.38 +lemma abs_power2 [simp]: "\<bar>a\<^sup>2\<bar> = a\<^sup>2"
   13.39    by (simp add: power2_eq_square abs_mult abs_mult_self)
   13.40  
   13.41 -lemma power2_abs [simp]:
   13.42 -  "(abs a)\<^sup>2 = a\<^sup>2"
   13.43 +lemma power2_abs [simp]: "\<bar>a\<bar>\<^sup>2 = a\<^sup>2"
   13.44    by (simp add: power2_eq_square abs_mult_self)
   13.45  
   13.46  lemma odd_power_less_zero:
   13.47 @@ -729,14 +723,14 @@
   13.48      by (auto intro!: power2_le_imp_le [OF _ abs_ge_zero])
   13.49  qed
   13.50  
   13.51 -lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> abs(x) \<le> 1"
   13.52 +lemma abs_square_le_1:"x\<^sup>2 \<le> 1 \<longleftrightarrow> \<bar>x\<bar> \<le> 1"
   13.53    using abs_le_square_iff [of x 1]
   13.54    by simp
   13.55  
   13.56 -lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> abs(x) = 1"
   13.57 +lemma abs_square_eq_1: "x\<^sup>2 = 1 \<longleftrightarrow> \<bar>x\<bar> = 1"
   13.58    by (auto simp add: abs_if power2_eq_1_iff)
   13.59  
   13.60 -lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> abs(x) < 1"
   13.61 +lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
   13.62    using  abs_square_eq_1 [of x] abs_square_le_1 [of x]
   13.63    by (auto simp add: le_less)
   13.64  
    14.1 --- a/src/HOL/Presburger.thy	Sun Dec 27 22:07:17 2015 +0100
    14.2 +++ b/src/HOL/Presburger.thy	Mon Dec 28 01:26:34 2015 +0100
    14.3 @@ -211,11 +211,11 @@
    14.4  
    14.5  subsubsection\<open>The \<open>-\<infinity>\<close> Version\<close>
    14.6  
    14.7 -lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (abs(x-z)+1) * d < z"
    14.8 -by(induct rule: int_gr_induct,simp_all add:int_distrib)
    14.9 +lemma decr_lemma: "0 < (d::int) \<Longrightarrow> x - (\<bar>x - z\<bar> + 1) * d < z"
   14.10 +  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
   14.11  
   14.12 -lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (abs(x-z)+1) * d"
   14.13 -by(induct rule: int_gr_induct, simp_all add:int_distrib)
   14.14 +lemma incr_lemma: "0 < (d::int) \<Longrightarrow> z < x + (\<bar>x - z\<bar> + 1) * d"
   14.15 +  by (induct rule: int_gr_induct) (simp_all add: int_distrib)
   14.16  
   14.17  lemma decr_mult_lemma:
   14.18    assumes dpos: "(0::int) < d" and minus: "\<forall>x. P x \<longrightarrow> P(x - d)" and knneg: "0 <= k"
   14.19 @@ -241,7 +241,7 @@
   14.20    assume eP1: "EX x. P1 x"
   14.21    then obtain x where P1: "P1 x" ..
   14.22    from ePeqP1 obtain z where P1eqP: "ALL x. x < z \<longrightarrow> (P x = P1 x)" ..
   14.23 -  let ?w = "x - (abs(x-z)+1) * d"
   14.24 +  let ?w = "x - (\<bar>x - z\<bar> + 1) * d"
   14.25    from dpos have w: "?w < z" by(rule decr_lemma)
   14.26    have "P1 x = P1 ?w" using P1eqP1 by blast
   14.27    also have "\<dots> = P(?w)" using w P1eqP by blast
   14.28 @@ -287,8 +287,8 @@
   14.29    assume eP1: "EX x. P' x"
   14.30    then obtain x where P1: "P' x" ..
   14.31    from ePeqP1 obtain z where P1eqP: "\<forall>x>z. P x = P' x" ..
   14.32 -  let ?w' = "x + (abs(x-z)+1) * d"
   14.33 -  let ?w = "x - (-(abs(x-z) + 1))*d"
   14.34 +  let ?w' = "x + (\<bar>x - z\<bar> + 1) * d"
   14.35 +  let ?w = "x - (- (\<bar>x - z\<bar> + 1)) * d"
   14.36    have ww'[simp]: "?w = ?w'" by (simp add: algebra_simps)
   14.37    from dpos have w: "?w > z" by(simp only: ww' incr_lemma)
   14.38    hence "P' x = P' ?w" using P1eqP1 by blast
    15.1 --- a/src/HOL/Rat.thy	Sun Dec 27 22:07:17 2015 +0100
    15.2 +++ b/src/HOL/Rat.thy	Mon Dec 28 01:26:34 2015 +0100
    15.3 @@ -451,7 +451,7 @@
    15.4    "x \<le> (y::rat) \<longleftrightarrow> x < y \<or> x = y"
    15.5  
    15.6  definition
    15.7 -  "abs (a::rat) = (if a < 0 then - a else a)"
    15.8 +  "\<bar>a::rat\<bar> = (if a < 0 then - a else a)"
    15.9  
   15.10  definition
   15.11    "sgn (a::rat) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
    16.1 --- a/src/HOL/Real.thy	Sun Dec 27 22:07:17 2015 +0100
    16.2 +++ b/src/HOL/Real.thy	Mon Dec 28 01:26:34 2015 +0100
    16.3 @@ -593,7 +593,7 @@
    16.4    "x \<le> (y::real) \<longleftrightarrow> x < y \<or> x = y"
    16.5  
    16.6  definition
    16.7 -  "abs (a::real) = (if a < 0 then - a else a)"
    16.8 +  "\<bar>a::real\<bar> = (if a < 0 then - a else a)"
    16.9  
   16.10  definition
   16.11    "sgn (a::real) = (if a = 0 then 0 else if 0 < a then 1 else - 1)"
   16.12 @@ -1037,7 +1037,7 @@
   16.13  declare of_int_1_less_iff [algebra, presburger]
   16.14  declare of_int_1_le_iff [algebra, presburger]
   16.15  
   16.16 -lemma of_int_abs [simp]: "of_int (abs x) = (abs(of_int x) :: 'a::linordered_idom)"
   16.17 +lemma of_int_abs [simp]: "of_int \<bar>x\<bar> = (\<bar>of_int x\<bar> :: 'a::linordered_idom)"
   16.18    by (auto simp add: abs_if)
   16.19  
   16.20  lemma int_less_real_le: "(n < m) = (real_of_int n + 1 <= real_of_int m)"
   16.21 @@ -1199,7 +1199,7 @@
   16.22  proof -
   16.23    from \<open>x \<in> \<rat>\<close> obtain i::int and n::nat where "n \<noteq> 0" and "x = real_of_int i / real n"
   16.24      by(auto simp add: Rats_eq_int_div_nat)
   16.25 -  hence "\<bar>x\<bar> = real(nat(abs i)) / real n" by (simp add: of_nat_nat)
   16.26 +  hence "\<bar>x\<bar> = real (nat \<bar>i\<bar>) / real n" by (simp add: of_nat_nat)
   16.27    then obtain m :: nat where x_rat: "\<bar>x\<bar> = real m / real n" by blast
   16.28    let ?gcd = "gcd m n"
   16.29    from \<open>n\<noteq>0\<close> have gcd: "?gcd \<noteq> 0" by simp
   16.30 @@ -1414,17 +1414,17 @@
   16.31  
   16.32  subsection\<open>Absolute Value Function for the Reals\<close>
   16.33  
   16.34 -lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))"
   16.35 -by (simp add: abs_if)
   16.36 +lemma abs_minus_add_cancel: "\<bar>x + (- y)\<bar> = \<bar>y + (- (x::real))\<bar>"
   16.37 +  by (simp add: abs_if)
   16.38  
   16.39 -lemma abs_add_one_gt_zero: "(0::real) < 1 + abs(x)"
   16.40 -by (simp add: abs_if)
   16.41 +lemma abs_add_one_gt_zero: "(0::real) < 1 + \<bar>x\<bar>"
   16.42 +  by (simp add: abs_if)
   16.43  
   16.44 -lemma abs_add_one_not_less_self: "~ abs(x) + (1::real) < x"
   16.45 -by simp
   16.46 +lemma abs_add_one_not_less_self: "~ \<bar>x\<bar> + (1::real) < x"
   16.47 +  by simp
   16.48  
   16.49 -lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
   16.50 -by simp
   16.51 +lemma abs_sum_triangle_ineq: "\<bar>(x::real) + y + (-l + -m)\<bar> \<le> \<bar>x + -l\<bar> + \<bar>y + -m\<bar>"
   16.52 +  by simp
   16.53  
   16.54  
   16.55  subsection\<open>Floor and Ceiling Functions from the Reals to the Integers\<close>
    17.1 --- a/src/HOL/Rings.thy	Sun Dec 27 22:07:17 2015 +0100
    17.2 +++ b/src/HOL/Rings.thy	Mon Dec 28 01:26:34 2015 +0100
    17.3 @@ -1559,7 +1559,7 @@
    17.4  lemma not_square_less_zero [simp]: "\<not> (a * a < 0)"
    17.5    by (simp add: not_less)
    17.6  
    17.7 -proposition abs_eq_iff: "abs x = abs y \<longleftrightarrow> x = y \<or> x = -y"
    17.8 +proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
    17.9    by (auto simp add: abs_if split: split_if_asm)
   17.10  
   17.11  end
    18.1 --- a/src/HOL/Transcendental.thy	Sun Dec 27 22:07:17 2015 +0100
    18.2 +++ b/src/HOL/Transcendental.thy	Mon Dec 28 01:26:34 2015 +0100
    18.3 @@ -1872,7 +1872,7 @@
    18.4    done
    18.5  
    18.6  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
    18.7 -  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
    18.8 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= x\<^sup>2"
    18.9  proof -
   18.10    assume x: "0 <= x"
   18.11    assume x1: "x <= 1"
   18.12 @@ -1880,7 +1880,7 @@
   18.13      by (rule ln_add_one_self_le_self)
   18.14    then have "ln (1 + x) - x <= 0"
   18.15      by simp
   18.16 -  then have "abs(ln(1 + x) - x) = - (ln(1 + x) - x)"
   18.17 +  then have "\<bar>ln(1 + x) - x\<bar> = - (ln(1 + x) - x)"
   18.18      by (rule abs_of_nonpos)
   18.19    also have "... = x - ln (1 + x)"
   18.20      by simp
   18.21 @@ -1895,11 +1895,11 @@
   18.22  qed
   18.23  
   18.24  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
   18.25 -  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
   18.26 +  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
   18.27  proof -
   18.28    assume a: "-(1 / 2) <= x"
   18.29    assume b: "x <= 0"
   18.30 -  have "abs(ln (1 + x) - x) = x - ln(1 - (-x))"
   18.31 +  have "\<bar>ln (1 + x) - x\<bar> = x - ln(1 - (-x))"
   18.32      apply (subst abs_of_nonpos)
   18.33      apply simp
   18.34      apply (rule ln_add_one_self_le_self2)
   18.35 @@ -1915,7 +1915,7 @@
   18.36  qed
   18.37  
   18.38  lemma abs_ln_one_plus_x_minus_x_bound:
   18.39 -  fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
   18.40 +  fixes x::real shows "\<bar>x\<bar> <= 1 / 2 \<Longrightarrow> \<bar>ln (1 + x) - x\<bar> <= 2 * x\<^sup>2"
   18.41    apply (case_tac "0 <= x")
   18.42    apply (rule order_trans)
   18.43    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
   18.44 @@ -2648,7 +2648,7 @@
   18.45    fixes x :: real
   18.46    shows "(\<lambda>n. (1 + x / n) ^ n) ----> exp x"
   18.47  proof (rule filterlim_mono_eventually)
   18.48 -  from reals_Archimedean2 [of "abs x"] obtain n :: nat where *: "real n > abs x" ..
   18.49 +  from reals_Archimedean2 [of "\<bar>x\<bar>"] obtain n :: nat where *: "real n > \<bar>x\<bar>" ..
   18.50    hence "eventually (\<lambda>n :: nat. 0 < 1 + x / real n) at_top"
   18.51      apply (intro eventually_sequentiallyI [of n])
   18.52      apply (case_tac "x \<ge> 0")
   18.53 @@ -3100,7 +3100,7 @@
   18.54    by (simp add: power2_eq_square)
   18.55  
   18.56  lemma sin_cos_le1:
   18.57 -  fixes x::real shows "abs (sin x * sin y + cos x * cos y) \<le> 1"
   18.58 +  fixes x::real shows "\<bar>sin x * sin y + cos x * cos y\<bar> \<le> 1"
   18.59    using cos_diff [of x y]
   18.60    by (metis abs_cos_le_one add.commute)
   18.61  
   18.62 @@ -4225,11 +4225,11 @@
   18.63  lemma tan_pos_pi2_le: "0 \<le> x ==> x < pi/2 \<Longrightarrow> 0 \<le> tan x"
   18.64    using less_eq_real_def tan_gt_zero by auto
   18.65  
   18.66 -lemma cos_tan: "abs(x) < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   18.67 +lemma cos_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> cos(x) = 1 / sqrt(1 + tan(x) ^ 2)"
   18.68    using cos_gt_zero_pi [of x]
   18.69    by (simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   18.70  
   18.71 -lemma sin_tan: "abs(x) < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   18.72 +lemma sin_tan: "\<bar>x\<bar> < pi/2 \<Longrightarrow> sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)"
   18.73    using cos_gt_zero [of "x"] cos_gt_zero [of "-x"]
   18.74    by (force simp add: divide_simps tan_def real_sqrt_divide abs_if split: split_if_asm)
   18.75  
   18.76 @@ -4244,7 +4244,7 @@
   18.77           \<Longrightarrow> (tan(x) \<le> tan(y) \<longleftrightarrow> x \<le> y)"
   18.78    by (meson tan_mono_le not_le tan_monotone)
   18.79  
   18.80 -lemma tan_bound_pi2: "abs(x) < pi/4 \<Longrightarrow> abs(tan x) < 1"
   18.81 +lemma tan_bound_pi2: "\<bar>x\<bar> < pi/4 \<Longrightarrow> \<bar>tan x\<bar> < 1"
   18.82    using tan_45 tan_monotone [of x "pi/4"] tan_monotone [of "-x" "pi/4"]
   18.83    by (auto simp: abs_if split: split_if_asm)
   18.84  
   18.85 @@ -4404,7 +4404,7 @@
   18.86  lemma arcsin_minus: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin(-x) = -arcsin x"
   18.87    by (metis (no_types, hide_lams) arcsin arcsin_sin minus_minus neg_le_iff_le sin_minus)
   18.88  
   18.89 -lemma arcsin_eq_iff: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
   18.90 +lemma arcsin_eq_iff: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arcsin x = arcsin y \<longleftrightarrow> x = y)"
   18.91    by (metis abs_le_iff arcsin minus_le_iff)
   18.92  
   18.93  lemma cos_arcsin_nonzero: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> cos(arcsin x) \<noteq> 0"
   18.94 @@ -4820,13 +4820,13 @@
   18.95      done
   18.96  qed
   18.97  
   18.98 -lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
   18.99 +lemma arcsin_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
  18.100    apply (rule trans [OF sin_mono_less_eq [symmetric]])
  18.101    using arcsin_ubound arcsin_lbound
  18.102    apply auto
  18.103    done
  18.104  
  18.105 -lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
  18.106 +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"
  18.107    using arcsin_less_mono not_le by blast
  18.108  
  18.109  lemma arcsin_less_arcsin: "-1 \<le> x \<Longrightarrow> x < y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x < arcsin y"
  18.110 @@ -4835,13 +4835,13 @@
  18.111  lemma arcsin_le_arcsin: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y"
  18.112    using arcsin_le_mono by auto
  18.113  
  18.114 -lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
  18.115 +lemma arccos_less_mono: "\<bar>x\<bar> \<le> 1 \<Longrightarrow> \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
  18.116    apply (rule trans [OF cos_mono_less_eq [symmetric]])
  18.117    using arccos_ubound arccos_lbound
  18.118    apply auto
  18.119    done
  18.120  
  18.121 -lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
  18.122 +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"
  18.123    using arccos_less_mono [of y x]
  18.124    by (simp add: not_le [symmetric])
  18.125  
  18.126 @@ -4851,7 +4851,7 @@
  18.127  lemma arccos_le_arccos: "-1 \<le> x \<Longrightarrow> x \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> arccos x"
  18.128    using arccos_le_mono by auto
  18.129  
  18.130 -lemma arccos_eq_iff: "abs x \<le> 1 & abs y \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
  18.131 +lemma arccos_eq_iff: "\<bar>x\<bar> \<le> 1 & \<bar>y\<bar> \<le> 1 \<Longrightarrow> (arccos x = arccos y \<longleftrightarrow> x = y)"
  18.132    using cos_arccos_abs by fastforce
  18.133  
  18.134  subsection \<open>Machins formula\<close>