# HG changeset patch
# User huffman
# Date 1178644535 -7200
# Node ID d53b72246e678e495c1d379f1cfa30de6ad920e1
# Parent  2b4c831ceca7fc998096f0f18cc192833d5deca5
add of_hypreal constant with lemmas

diff -r 2b4c831ceca7 -r d53b72246e67 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 18:23:37 2007 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Tue May 08 19:15:35 2007 +0200
@@ -102,6 +102,58 @@
 by (simp add: Reals_def Standard_def)
 
 
+subsection {* Injection from @{typ hypreal} *}
+
+definition
+  of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
+  "of_hypreal = *f* of_real"
+
+declare of_hypreal_def [transfer_unfold]
+
+lemma Standard_of_hypreal [simp]:
+  "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
+by (simp add: of_hypreal_def)
+
+lemma of_hypreal_0 [simp]: "of_hypreal 0 = 0"
+by transfer (rule of_real_0)
+
+lemma of_hypreal_1 [simp]: "of_hypreal 1 = 1"
+by transfer (rule of_real_1)
+
+lemma of_hypreal_add [simp]:
+  "\<And>x y. of_hypreal (x + y) = of_hypreal x + of_hypreal y"
+by transfer (rule of_real_add)
+
+lemma of_hypreal_minus [simp]: "\<And>x. of_hypreal (- x) = - of_hypreal x"
+by transfer (rule of_real_minus)
+
+lemma of_hypreal_diff [simp]:
+  "\<And>x y. of_hypreal (x - y) = of_hypreal x - of_hypreal y"
+by transfer (rule of_real_diff)
+
+lemma of_hypreal_mult [simp]:
+  "\<And>x y. of_hypreal (x * y) = of_hypreal x * of_hypreal y"
+by transfer (rule of_real_mult)
+
+lemma of_hypreal_inverse [simp]:
+  "\<And>x. of_hypreal (inverse x) =
+   inverse (of_hypreal x :: 'a::{real_div_algebra,division_by_zero} star)"
+by transfer (rule of_real_inverse)
+
+lemma of_hypreal_divide [simp]:
+  "\<And>x y. of_hypreal (x / y) =
+   (of_hypreal x / of_hypreal y :: 'a::{real_field,division_by_zero} star)"
+by transfer (rule of_real_divide)
+
+lemma of_hypreal_eq_iff [simp]:
+  "\<And>x y. (of_hypreal x = of_hypreal y) = (x = y)"
+by transfer (rule of_real_eq_iff)
+
+lemma of_hypreal_eq_0_iff [simp]:
+  "\<And>x. (of_hypreal x = 0) = (x = 0)"
+by transfer (rule of_real_eq_0_iff)
+
+
 subsection{*Properties of @{term starrel}*}
 
 lemma lemma_starrel_refl [simp]: "x \<in> starrel `` {x}"