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