# HG changeset patch
# User hoelzl
# Date 1334752160 -7200
# Node ID 5e7e394f78d467e6c0c7ddda49a67d53b444ad47
# Parent  c031e65c8ddc7aa52c63a86c0cba874915565704
add simp rules to rewrite comparisons of 1 and real

diff -r c031e65c8ddc -r 5e7e394f78d4 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Wed Apr 18 14:29:19 2012 +0200
+++ b/src/HOL/RealDef.thy	Wed Apr 18 14:29:20 2012 +0200
@@ -1159,6 +1159,18 @@
 lemma real_of_int_le_zero_cancel_iff [simp, presburger]: "(real (n::int) <= 0) = (n <= 0)"
 by (simp add: real_of_int_def)
 
+lemma one_less_real_of_int_cancel_iff: "1 < real (i :: int) \<longleftrightarrow> 1 < i"
+  unfolding real_of_one[symmetric] real_of_int_less_iff ..
+
+lemma one_le_real_of_int_cancel_iff: "1 \<le> real (i :: int) \<longleftrightarrow> 1 \<le> i"
+  unfolding real_of_one[symmetric] real_of_int_le_iff ..
+
+lemma real_of_int_less_one_cancel_iff: "real (i :: int) < 1 \<longleftrightarrow> i < 1"
+  unfolding real_of_one[symmetric] real_of_int_less_iff ..
+
+lemma real_of_int_le_one_cancel_iff: "real (i :: int) \<le> 1 \<longleftrightarrow> i \<le> 1"
+  unfolding real_of_one[symmetric] real_of_int_le_iff ..
+
 lemma real_of_int_abs [simp]: "real (abs x) = abs(real (x::int))"
 by (auto simp add: abs_if)