--- 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>"
--- 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"
--- 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>
--- 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:
--- 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
--- 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])
--- 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
--- 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:
--- 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)
--- 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"
--- 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)"
--- 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
--- 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)
--- 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
--- 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)"
--- 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>
--- 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
--- 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>