src/HOL/Int.thy
changeset 61944 5d06ecfdb472
parent 61799 4cf66f21b764
child 62128 3201ddb00097
     1.1 --- a/src/HOL/Int.thy	Sun Dec 27 22:07:17 2015 +0100
     1.2 +++ b/src/HOL/Int.thy	Mon Dec 28 01:26:34 2015 +0100
     1.3 @@ -529,7 +529,7 @@
     1.4        in theory \<open>Rings\<close>.
     1.5        But is it really better than just rewriting with \<open>abs_if\<close>?\<close>
     1.6  lemma abs_split [arith_split, no_atp]:
     1.7 -     "P(abs(a::'a::linordered_idom)) = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
     1.8 +     "P \<bar>a::'a::linordered_idom\<bar> = ((0 \<le> a --> P a) & (a < 0 --> P(-a)))"
     1.9  by (force dest: order_less_le_trans simp add: abs_if linorder_not_less)
    1.10  
    1.11  lemma negD: "x < 0 \<Longrightarrow> \<exists>n. x = - (int (Suc n))"
    1.12 @@ -944,7 +944,7 @@
    1.13  apply (rule_tac [2] nat_mult_distrib, auto)
    1.14  done
    1.15  
    1.16 -lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
    1.17 +lemma nat_abs_mult_distrib: "nat \<bar>w * z\<bar> = nat \<bar>w\<bar> * nat \<bar>z\<bar>"
    1.18  apply (cases "z=0 | w=0")
    1.19  apply (auto simp add: abs_if nat_mult_distrib [symmetric]
    1.20                        nat_mult_distrib_neg [symmetric] mult_less_0_iff)
    1.21 @@ -1115,7 +1115,7 @@
    1.22  subsection\<open>Intermediate value theorems\<close>
    1.23  
    1.24  lemma int_val_lemma:
    1.25 -     "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
    1.26 +     "(\<forall>i<n::nat. \<bar>f(i+1) - f i\<bar> \<le> 1) -->
    1.27        f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
    1.28  unfolding One_nat_def
    1.29  apply (induct n)
    1.30 @@ -1133,7 +1133,7 @@
    1.31  lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
    1.32  
    1.33  lemma nat_intermed_int_val:
    1.34 -     "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
    1.35 +     "[| \<forall>i. m \<le> i & i < n --> \<bar>f(i + 1::nat) - f i\<bar> \<le> 1; m < n;
    1.36           f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
    1.37  apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
    1.38         in int_val_lemma)
    1.39 @@ -1432,10 +1432,10 @@
    1.40    from zdvd_mult_cancel[OF H2 mp] show "\<bar>n\<bar> = 1" by (simp only: zdvd1_eq)
    1.41  qed
    1.42  
    1.43 -lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))"
    1.44 +lemma int_dvd_iff: "(int m dvd z) = (m dvd nat \<bar>z\<bar>)"
    1.45    unfolding zdvd_int by (cases "z \<ge> 0") simp_all
    1.46  
    1.47 -lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)"
    1.48 +lemma dvd_int_iff: "(z dvd int m) = (nat \<bar>z\<bar> dvd m)"
    1.49    unfolding zdvd_int by (cases "z \<ge> 0") simp_all
    1.50  
    1.51  lemma dvd_int_unfold_dvd_nat: