# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1447261910 0
# Node ID 6ef461bee3fae5be9a05ceefedcc62503f110850
# Parent  7ffc9c4f1f740f6cad5de078422bbbd37c4713f0
new conversion theorems for int, nat to float

diff -r 7ffc9c4f1f74 -r 6ef461bee3fa src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Wed Nov 11 16:42:30 2015 +0100
+++ b/src/HOL/Library/Float.thy	Wed Nov 11 17:11:50 2015 +0000
@@ -31,7 +31,6 @@
 declare real_of_float_inverse[simp] float_of_inverse [simp]
 declare real_of_float [simp]
 
-
 subsection \<open>Real operations preserving the representation as floating point number\<close>
 
 lemma floatI: fixes m e :: int shows "m * 2 powr e = x \<Longrightarrow> x \<in> float"
@@ -214,6 +213,12 @@
 
 end
 
+lemma real_of_float [simp]: "real_of_float (of_nat n) = of_nat n"
+by (induct n) simp_all
+
+lemma real_of_float_of_int_eq [simp]: "real_of_float (of_int z) = of_int z"
+  by (cases z rule: int_diff_cases) (simp_all add: of_rat_diff)
+
 lemma Float_0_eq_0[simp]: "Float 0 e = 0"
   by transfer simp