# 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)) \ abs (z - of_int m)" + shows "\z - of_int (round z)\ \ \z - of_int m\" proof (cases "of_int m \ z") case True hence "\z - of_int (round z)\ \ \of_int \z\ - z\" 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 \ \ \ cnj z = z" by (auto simp: complex_is_Real_iff complex_eq_iff) -lemma in_Reals_norm: "z \ \ \ norm(z) = abs(Re z)" +lemma in_Reals_norm: "z \ \ \ norm z = \Re z\" by (simp add: complex_is_Real_iff norm_complex_def) lemma series_comparison_complex: @@ -719,7 +719,7 @@ lemma rcis_Ex: "\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) = \r\" 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 \ abs (x div y) = abs x div abs y" +lemma abs_div: "(y::int) dvd x \ \x div y\ = \x\ div \y\" by (unfold dvd_def, cases "y=0", auto simp add: abs_mult) text\Suggested by Matthias Daum\ 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 \ a / abs b) = (0 \ a | b = 0)" +lemma zero_le_divide_abs_iff [simp]: "(0 \ a / \b\) = (0 \ a | b = 0)" by (auto simp: zero_le_divide_iff) -lemma divide_le_0_abs_iff [simp]: "(a / abs b \ 0) = (a \ 0 | b = 0)" +lemma divide_le_0_abs_iff [simp]: "(a / \b\ \ 0) = (a \ 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 \ int \ int" where - "gcd_int x y = int (gcd (nat (abs x)) (nat (abs y)))" + "gcd_int x y = int (gcd (nat \x\) (nat \y\))" definition lcm_int :: "int \ int \ int" where - "lcm_int x y = int (lcm (nat (abs x)) (nat (abs y)))" + "lcm_int x y = int (lcm (nat \x\) (nat \y\))" -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]: "\gcd (x::int) y\ = 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 \x\ \y\" 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 \x\ (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 \y::int\ = gcd x y" by (metis abs_idempotent gcd_abs_int) lemma gcd_cases_int: @@ -695,7 +695,7 @@ and "x <= 0 \ y >= 0 \ P (gcd (-x) y)" and "x <= 0 \ y <= 0 \ 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 \x\ \y\" 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]: "\lcm i j::int\ = 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 \x\ (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 \y::int\ = 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 = \x\" 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) = \x\" 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 = \x\" 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 \ gcd x y = y" by (fact gcd_nat.absorb2) -lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \ gcd (x::int) y = abs x" +lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \ gcd (x::int) y = \x\" 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 \ gcd (x::int) y = abs y" +lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \ gcd (x::int) y = \y\" by (metis gcd_proj1_if_dvd_int gcd_commute_int) text \ @@ -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: "\k::int\ * 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. \d\ <= \i\} = {- \i\ .. \i\}" by(auto simp:abs_if) + hence "finite {d. \d\ <= \i\}" 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\0 \ Max{d::int. d dvd n} = abs n" +lemma Max_divisors_self_int[simp]: "n\0 \ Max{d::int. d dvd n} = \n\" 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 \ x dvd a \ x dvd b \ abs x = 1" + "coprime (a::int) b \ x dvd a \ x dvd b \ \x\ = 1" using gcd_greatest_iff [of x a b] by auto lemma coprime_divisors_nat: @@ -1763,7 +1763,7 @@ subsection \LCM properties\ -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 = \a\ * \b\ 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: "\m::int\ * \n\ = 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 \ lcm x y = abs y" +lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \ lcm x y = \y\" 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 \ 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 \ lcm y x = abs y" +lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \ lcm y x = \y\" by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int) lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \ n dvd m" @@ -1889,10 +1889,10 @@ lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \ 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) \ n dvd m" +lemma lcm_proj1_iff_int[simp]: "lcm m n = \m::int\ \ 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) \ m dvd n" +lemma lcm_proj2_iff_int[simp]: "lcm m n = \n::int\ \ 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 \ nat (abs x) dvd nat (abs y)" +lemma dvd_int_iff: "x dvd y \ nat \x\ dvd nat \y\" by (fact dvd_int_unfold_dvd_nat) lemma dvd_Lcm_int [simp]: @@ -2223,7 +2223,7 @@ "gcd k l = \if l = (0::integer) then k else gcd l (\k\ mod \l\)\" 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 = \a\ * \b\ 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 \ 'a" -begin - -notation (xsymbols) - abs ("\_\") - -end + fixes abs :: "'a \ 'a" ("\_\") class sgn = fixes sgn :: "'a \ 'a" @@ -1375,7 +1369,7 @@ lemma dense_eq0_I: fixes x::"'a::{dense_linorder,ordered_ab_group_add_abs}" shows "(\e. 0 < e \ \x\ \ e) ==> x = 0" - apply (cases "abs x=0", simp) + apply (cases "\x\ = 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) \ setsum (%i. abs(f i)) A" + shows "\setsum f A\ \ setsum (%i. \f i\) 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 \ setsum (%i. abs(f i)) A" + shows "0 \ setsum (%i. \f i\) A" by (simp add: setsum_nonneg) lemma abs_setsum_abs[simp]: fixes f :: "'a => ('b::ordered_ab_group_add_abs)" - shows "abs (\a\A. abs(f a)) = (\a\A. abs(f a))" + shows "\\a\A. \f a\\ = (\a\A. \f a\)" 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 \Rings\. But is it really better than just rewriting with \abs_if\?\ lemma abs_split [arith_split, no_atp]: - "P(abs(a::'a::linordered_idom)) = ((0 \ a --> P a) & (a < 0 --> P(-a)))" + "P \a::'a::linordered_idom\ = ((0 \ 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 \ \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 \w * z\ = nat \w\ * nat \z\" 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\Intermediate value theorems\ lemma int_val_lemma: - "(\i 1) --> + "(\if(i+1) - f i\ \ 1) --> f 0 \ k --> k \ f n --> (\i \ 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: - "[| \i. m \ i & i < n --> abs(f(i + 1::nat) - f i) \ 1; m < n; + "[| \i. m \ i & i < n --> \f(i + 1::nat) - f i\ \ 1; m < n; f m \ k; k \ f n |] ==> ? i. m \ i & i \ 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 "\n\ = 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 \z\)" unfolding zdvd_int by (cases "z \ 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 \z\ dvd m)" unfolding zdvd_int by (cases "z \ 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 : "\m t::real. m < n & abs t \ abs x --> DERIV (diff m) t :> diff (Suc m) t" - shows "\t. abs t \ abs x & + and DERIV : "\m t::real. m < n & \t\ \ \x\ --> DERIV (diff m) t :> diff (Suc m) t" + shows "\t. \t\ \ \x\ & f x = (\mt. _ \ f x = ?f x t") @@ -294,7 +294,7 @@ fixes x::real assumes INIT1: "diff 0 = f" and INIT2: "0 < n" and INIT3: "x \ 0" and DERIV: "\m x. DERIV (diff m) x :> diff(Suc m) x" - shows "\t. 0 < abs t & abs t < abs x & f x = + shows "\t. 0 < \t\ & \t\ < \x\ & f x = (\mt. _ \ _ \ f x = ?f x t") proof (cases rule: linorder_cases) @@ -320,7 +320,7 @@ "diff 0 = f & (\m x. DERIV (diff m) x :> diff(Suc m) x) & x ~= 0 & n > 0 - --> (\t. 0 < abs t & abs t < abs x & + --> (\t. 0 < \t\ & \t\ < \x\ & f x = (\mm x::real. DERIV (diff m) x :> diff (Suc m) x" - shows "\t. abs t \ abs x & f x = + shows "\t. \t\ \ \x\ & f x = (\mt. _ \ f x = ?f x t") proof cases @@ -363,7 +363,7 @@ lemma Maclaurin_all_le_objl: "diff 0 = f & (\m x. DERIV (diff m) x :> diff (Suc m) x) - --> (\t::real. abs t \ abs x & + --> (\t::real. \t\ \ \x\ & f x = (\m 0 |] - ==> (\t. 0 < abs t & - abs t < abs x & + ==> (\t. 0 < \t\ & + \t\ < \x\ & exp x = (\mt::real. abs t \ abs x & + "\t::real. \t\ \ \x\ & exp x = (\mt. abs t \ abs x & + "\t. \t\ \ \x\ & sin x = (\mt::real. abs t \ abs x & + "\t::real. \t\ \ \x\ & cos x = (\m (v::real) |] ==> \(x + u) - y\ \ v" + "[|x = y; \u\ \ (v::real) |] ==> \(x + u) - y\ \ v" by auto lemma Maclaurin_sin_bound: - "abs(sin x - (\m inverse((fact n)) * \x\ ^ n" + "\sin x - (\m \ inverse((fact n)) * \x\ ^ n" proof - have "!! x (y::real). x \ 1 \ 0 \ y \ x * y \ 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 \ nat \ 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 (\(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 \ int \ int" where - "int_gcd x y = int (nat_gcd (nat (abs x)) (nat (abs y)))" + "int_gcd x y = int (nat_gcd (nat \x\) (nat \y\))" definition int_lcm :: "int \ int \ int" where - "int_lcm x y = int (nat_lcm (nat (abs x)) (nat (abs y)))" + "int_lcm x y = int (nat_lcm (nat \x\) (nat \y\))" definition Frac :: "int \ int \ bool" where "Frac \ \(a, b). b > 0 \ 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: "\sgn x :: real\ = (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 @@ "\ 1 < - 1" by (simp_all add: less_le) -lemma abs_numeral [simp]: "abs (numeral n) = numeral n" +lemma abs_numeral [simp]: "\numeral n\ = numeral n" by simp -lemma abs_neg_numeral [simp]: "abs (- numeral n) = numeral n" +lemma abs_neg_numeral [simp]: "\- numeral n\ = numeral n" by (simp only: abs_minus_cancel abs_numeral) -lemma abs_neg_one [simp]: - "abs (- 1) = 1" +lemma abs_neg_one [simp]: "\- 1\ = 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: "\a ^ n\ = \a\ ^ 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]: "\(-a) ^ n\ = \a ^ n\" by (simp add: power_abs) -lemma zero_less_power_abs_iff [simp]: - "0 < abs a ^ n \ a \ 0 \ n = 0" +lemma zero_less_power_abs_iff [simp]: "0 < \a\ ^ n \ a \ 0 \ 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 \ abs a ^ n" +lemma zero_le_power_abs [simp]: "0 \ \a\ ^ n" by (rule zero_le_power [OF abs_ge_zero]) lemma zero_le_power2 [simp]: @@ -658,12 +654,10 @@ "a\<^sup>2 \ 0 \ a = 0" by (simp add: le_less) -lemma abs_power2 [simp]: - "abs (a\<^sup>2) = a\<^sup>2" +lemma abs_power2 [simp]: "\a\<^sup>2\ = 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]: "\a\\<^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 \ 1 \ abs(x) \ 1" +lemma abs_square_le_1:"x\<^sup>2 \ 1 \ \x\ \ 1" using abs_le_square_iff [of x 1] by simp -lemma abs_square_eq_1: "x\<^sup>2 = 1 \ abs(x) = 1" +lemma abs_square_eq_1: "x\<^sup>2 = 1 \ \x\ = 1" by (auto simp add: abs_if power2_eq_1_iff) -lemma abs_square_less_1: "x\<^sup>2 < 1 \ abs(x) < 1" +lemma abs_square_less_1: "x\<^sup>2 < 1 \ \x\ < 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\The \-\\ Version\ -lemma decr_lemma: "0 < (d::int) \ x - (abs(x-z)+1) * d < z" -by(induct rule: int_gr_induct,simp_all add:int_distrib) +lemma decr_lemma: "0 < (d::int) \ x - (\x - z\ + 1) * d < z" + by (induct rule: int_gr_induct) (simp_all add: int_distrib) -lemma incr_lemma: "0 < (d::int) \ z < x + (abs(x-z)+1) * d" -by(induct rule: int_gr_induct, simp_all add:int_distrib) +lemma incr_lemma: "0 < (d::int) \ z < x + (\x - z\ + 1) * d" + by (induct rule: int_gr_induct) (simp_all add: int_distrib) lemma decr_mult_lemma: assumes dpos: "(0::int) < d" and minus: "\x. P x \ 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 \ (P x = P1 x)" .. - let ?w = "x - (abs(x-z)+1) * d" + let ?w = "x - (\x - z\ + 1) * d" from dpos have w: "?w < z" by(rule decr_lemma) have "P1 x = P1 ?w" using P1eqP1 by blast also have "\ = 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: "\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 + (\x - z\ + 1) * d" + let ?w = "x - (- (\x - z\ + 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 \ (y::rat) \ x < y \ x = y" definition - "abs (a::rat) = (if a < 0 then - a else a)" + "\a::rat\ = (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 \ (y::real) \ x < y \ x = y" definition - "abs (a::real) = (if a < 0 then - a else a)" + "\a::real\ = (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 \x\ = (\of_int x\ :: '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 \x \ \\ obtain i::int and n::nat where "n \ 0" and "x = real_of_int i / real n" by(auto simp add: Rats_eq_int_div_nat) - hence "\x\ = real(nat(abs i)) / real n" by (simp add: of_nat_nat) + hence "\x\ = real (nat \i\) / real n" by (simp add: of_nat_nat) then obtain m :: nat where x_rat: "\x\ = real m / real n" by blast let ?gcd = "gcd m n" from \n\0\ have gcd: "?gcd \ 0" by simp @@ -1414,17 +1414,17 @@ subsection\Absolute Value Function for the Reals\ -lemma abs_minus_add_cancel: "abs(x + (-y)) = abs (y + (-(x::real)))" -by (simp add: abs_if) +lemma abs_minus_add_cancel: "\x + (- y)\ = \y + (- (x::real))\" + 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 + \x\" + 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: "~ \x\ + (1::real) < x" + by simp -lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \ abs(x + -l) + abs(y + -m)" -by simp +lemma abs_sum_triangle_ineq: "\(x::real) + y + (-l + -m)\ \ \x + -l\ + \y + -m\" + by simp subsection\Floor and Ceiling Functions from the Reals to the Integers\ 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]: "\ (a * a < 0)" by (simp add: not_less) -proposition abs_eq_iff: "abs x = abs y \ x = y \ x = -y" +proposition abs_eq_iff: "\x\ = \y\ \ x = y \ 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 \ x <= 1 \ abs(ln (1 + x) - x) <= x\<^sup>2" + fixes x::real shows "0 <= x \ x <= 1 \ \ln (1 + x) - x\ <= 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 "\ln(1 + x) - x\ = - (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 \ x <= 0 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" + fixes x::real shows "-(1 / 2) <= x \ x <= 0 \ \ln (1 + x) - x\ <= 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 "\ln (1 + x) - x\ = 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 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" + fixes x::real shows "\x\ <= 1 / 2 \ \ln (1 + x) - x\ <= 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 "(\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 "\x\"] obtain n :: nat where *: "real n > \x\" .. hence "eventually (\n :: nat. 0 < 1 + x / real n) at_top" apply (intro eventually_sequentiallyI [of n]) apply (case_tac "x \ 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) \ 1" + fixes x::real shows "\sin x * sin y + cos x * cos y\ \ 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 \ x ==> x < pi/2 \ 0 \ tan x" using less_eq_real_def tan_gt_zero by auto -lemma cos_tan: "abs(x) < pi/2 \ cos(x) = 1 / sqrt(1 + tan(x) ^ 2)" +lemma cos_tan: "\x\ < pi/2 \ 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 \ sin(x) = tan(x) / sqrt(1 + tan(x) ^ 2)" +lemma sin_tan: "\x\ < pi/2 \ 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 @@ \ (tan(x) \ tan(y) \ x \ y)" by (meson tan_mono_le not_le tan_monotone) -lemma tan_bound_pi2: "abs(x) < pi/4 \ abs(tan x) < 1" +lemma tan_bound_pi2: "\x\ < pi/4 \ \tan x\ < 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 \ x \ x \ 1 \ 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 \ 1 \ abs y \ 1 \ (arcsin x = arcsin y \ x = y)" +lemma arcsin_eq_iff: "\x\ \ 1 \ \y\ \ 1 \ (arcsin x = arcsin y \ x = y)" by (metis abs_le_iff arcsin minus_le_iff) lemma cos_arcsin_nonzero: "-1 < x \ x < 1 \ cos(arcsin x) \ 0" @@ -4820,13 +4820,13 @@ done qed -lemma arcsin_less_mono: "abs x \ 1 \ abs y \ 1 \ arcsin x < arcsin y \ x < y" +lemma arcsin_less_mono: "\x\ \ 1 \ \y\ \ 1 \ arcsin x < arcsin y \ 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 \ 1 \ abs y \ 1 \ arcsin x \ arcsin y \ x \ y" +lemma arcsin_le_mono: "\x\ \ 1 \ \y\ \ 1 \ arcsin x \ arcsin y \ x \ y" using arcsin_less_mono not_le by blast lemma arcsin_less_arcsin: "-1 \ x \ x < y \ y \ 1 \ arcsin x < arcsin y" @@ -4835,13 +4835,13 @@ lemma arcsin_le_arcsin: "-1 \ x \ x \ y \ y \ 1 \ arcsin x \ arcsin y" using arcsin_le_mono by auto -lemma arccos_less_mono: "abs x \ 1 \ abs y \ 1 \ (arccos x < arccos y \ y < x)" +lemma arccos_less_mono: "\x\ \ 1 \ \y\ \ 1 \ (arccos x < arccos y \ 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 \ 1 \ abs y \ 1 \ arccos x \ arccos y \ y \ x" +lemma arccos_le_mono: "\x\ \ 1 \ \y\ \ 1 \ arccos x \ arccos y \ y \ x" using arccos_less_mono [of y x] by (simp add: not_le [symmetric]) @@ -4851,7 +4851,7 @@ lemma arccos_le_arccos: "-1 \ x \ x \ y \ y \ 1 \ arccos y \ arccos x" using arccos_le_mono by auto -lemma arccos_eq_iff: "abs x \ 1 & abs y \ 1 \ (arccos x = arccos y \ x = y)" +lemma arccos_eq_iff: "\x\ \ 1 & \y\ \ 1 \ (arccos x = arccos y \ x = y)" using cos_arccos_abs by fastforce subsection \Machins formula\