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)"
```