# HG changeset patch
# User huffman
# Date 1267982476 28800
# Node ID 90fffd5ff996beb3c013f1875678728afef18687
# Parent  6fdfe37b84d68e821af557c7d935dd462fe4f714
add simp rules about Ints, Nats

diff -r 6fdfe37b84d6 -r 90fffd5ff996 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Sun Mar 07 08:40:38 2010 -0800
+++ b/src/HOL/RealDef.thy	Sun Mar 07 09:21:16 2010 -0800
@@ -701,6 +701,9 @@
 lemma real_of_int_div4: "real (n div x) <= real (n::int) / real x" 
 by (insert real_of_int_div2 [of n x], simp)
 
+lemma Ints_real_of_int [simp]: "real (x::int) \<in> Ints"
+unfolding real_of_int_def by (rule Ints_of_int)
+
 
 subsection{*Embedding the Naturals into the Reals*}
 
@@ -852,6 +855,12 @@
   apply (simp only: real_of_int_real_of_nat)
 done
 
+lemma Nats_real_of_nat [simp]: "real (n::nat) \<in> Nats"
+unfolding real_of_nat_def by (rule of_nat_in_Nats)
+
+lemma Ints_real_of_nat [simp]: "real (n::nat) \<in> Ints"
+unfolding real_of_nat_def by (rule Ints_of_nat)
+
 
 subsection{* Rationals *}