# 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) \ 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) \ Nats" +unfolding real_of_nat_def by (rule of_nat_in_Nats) + +lemma Ints_real_of_nat [simp]: "real (n::nat) \ Ints" +unfolding real_of_nat_def by (rule Ints_of_nat) + subsection{* Rationals *}