diff r 97f2ed240431 r 2230b7047376 src/HOL/Int.thy
 a/src/HOL/Int.thy Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/Int.thy Wed Feb 17 21:51:57 2016 +0100
@@ 190,6 +190,21 @@
apply arith
done
+lemma zabs_less_one_iff [simp]:
+ fixes z :: int
+ shows "\z\ < 1 \ z = 0" (is "?P \ ?Q")
+proof
+ assume ?Q then show ?P by simp
+next
+ assume ?P
+ with zless_imp_add1_zle [of "\z\" 1] have "\z\ + 1 \ 1"
+ by simp
+ then have "\z\ \ 0"
+ by simp
+ then show ?Q
+ by simp
+qed
+
lemmas int_distrib =
distrib_right [of z1 z2 w]
distrib_left [of w z1 z2]
@@ 320,6 +335,45 @@
lemma of_int_nonneg: "z \ 0 \ of_int z \ 0"
by simp
+lemma of_int_abs [simp]:
+ "of_int \x\ = \of_int x\"
+ by (auto simp add: abs_if)
+
+lemma of_int_lessD:
+ assumes "\of_int n\ < x"
+ shows "n = 0 \ x > 1"
+proof (cases "n = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "\n\ \ 0" by simp
+ then have "\n\ > 0" by simp
+ then have "\n\ \ 1"
+ using zless_imp_add1_zle [of 0 "\n\"] by simp
+ then have "\of_int n\ \ 1"
+ unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
+ then have "1 < x" using assms by (rule le_less_trans)
+ then show ?thesis ..
+qed
+
+lemma of_int_leD:
+ assumes "\of_int n\ \ x"
+ shows "n = 0 \ 1 \ x"
+proof (cases "n = 0")
+ case True then show ?thesis by simp
+next
+ case False
+ then have "\n\ \ 0" by simp
+ then have "\n\ > 0" by simp
+ then have "\n\ \ 1"
+ using zless_imp_add1_zle [of 0 "\n\"] by simp
+ then have "\of_int n\ \ 1"
+ unfolding of_int_1_le_iff [of "\n\", symmetric] by simp
+ then have "1 \ x" using assms by (rule order_trans)
+ then show ?thesis ..
+qed
+
+
end
text \Comparisons involving @{term of_int}.\
@@ 1152,9 +1206,6 @@
subsection\Products and 1, by T. M. Rasmussen\
lemma zabs_less_one_iff [simp]: "(\z\ < 1) = (z = (0::int))"
by arith

lemma abs_zmult_eq_1:
assumes mn: "\m * n\ = 1"
shows "\m\ = (1::int)"