src/HOL/Int.thy
changeset 62347 2230b7047376
parent 62128 3201ddb00097
child 62348 9a5f43dac883
     1.1 --- a/src/HOL/Int.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/Int.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -190,6 +190,21 @@
     1.4  apply arith
     1.5  done
     1.6  
     1.7 +lemma zabs_less_one_iff [simp]:
     1.8 +  fixes z :: int
     1.9 +  shows "\<bar>z\<bar> < 1 \<longleftrightarrow> z = 0" (is "?P \<longleftrightarrow> ?Q")
    1.10 +proof
    1.11 +  assume ?Q then show ?P by simp
    1.12 +next
    1.13 +  assume ?P
    1.14 +  with zless_imp_add1_zle [of "\<bar>z\<bar>" 1] have "\<bar>z\<bar> + 1 \<le> 1"
    1.15 +    by simp
    1.16 +  then have "\<bar>z\<bar> \<le> 0"
    1.17 +    by simp
    1.18 +  then show ?Q
    1.19 +    by simp
    1.20 +qed
    1.21 +
    1.22  lemmas int_distrib =
    1.23    distrib_right [of z1 z2 w]
    1.24    distrib_left [of w z1 z2]
    1.25 @@ -320,6 +335,45 @@
    1.26  lemma of_int_nonneg: "z \<ge> 0 \<Longrightarrow> of_int z \<ge> 0"
    1.27    by simp
    1.28  
    1.29 +lemma of_int_abs [simp]:
    1.30 +  "of_int \<bar>x\<bar> = \<bar>of_int x\<bar>"
    1.31 +  by (auto simp add: abs_if)
    1.32 +
    1.33 +lemma of_int_lessD:
    1.34 +  assumes "\<bar>of_int n\<bar> < x"
    1.35 +  shows "n = 0 \<or> x > 1"
    1.36 +proof (cases "n = 0")
    1.37 +  case True then show ?thesis by simp
    1.38 +next
    1.39 +  case False
    1.40 +  then have "\<bar>n\<bar> \<noteq> 0" by simp
    1.41 +  then have "\<bar>n\<bar> > 0" by simp
    1.42 +  then have "\<bar>n\<bar> \<ge> 1"
    1.43 +    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
    1.44 +  then have "\<bar>of_int n\<bar> \<ge> 1"
    1.45 +    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
    1.46 +  then have "1 < x" using assms by (rule le_less_trans)
    1.47 +  then show ?thesis ..
    1.48 +qed
    1.49 +
    1.50 +lemma of_int_leD:
    1.51 +  assumes "\<bar>of_int n\<bar> \<le> x"
    1.52 +  shows "n = 0 \<or> 1 \<le> x"
    1.53 +proof (cases "n = 0")
    1.54 +  case True then show ?thesis by simp
    1.55 +next
    1.56 +  case False
    1.57 +  then have "\<bar>n\<bar> \<noteq> 0" by simp
    1.58 +  then have "\<bar>n\<bar> > 0" by simp
    1.59 +  then have "\<bar>n\<bar> \<ge> 1"
    1.60 +    using zless_imp_add1_zle [of 0 "\<bar>n\<bar>"] by simp
    1.61 +  then have "\<bar>of_int n\<bar> \<ge> 1"
    1.62 +    unfolding of_int_1_le_iff [of "\<bar>n\<bar>", symmetric] by simp
    1.63 +  then have "1 \<le> x" using assms by (rule order_trans)
    1.64 +  then show ?thesis ..
    1.65 +qed
    1.66 +
    1.67 +
    1.68  end
    1.69  
    1.70  text \<open>Comparisons involving @{term of_int}.\<close>
    1.71 @@ -1152,9 +1206,6 @@
    1.72  
    1.73  subsection\<open>Products and 1, by T. M. Rasmussen\<close>
    1.74  
    1.75 -lemma zabs_less_one_iff [simp]: "(\<bar>z\<bar> < 1) = (z = (0::int))"
    1.76 -by arith
    1.77 -
    1.78  lemma abs_zmult_eq_1:
    1.79    assumes mn: "\<bar>m * n\<bar> = 1"
    1.80    shows "\<bar>m\<bar> = (1::int)"