# HG changeset patch
# User huffman
# Date 1159323561 -7200
# Node ID f43214ff6baf159e673b4ea2e5a0794ef47548e4
# Parent  72e20198f83450d61abadab9779d59210690276e
add lemmas about Standard, real_of, scaleR

diff -r 72e20198f834 -r f43214ff6baf src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 27 03:05:28 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Sep 27 04:19:21 2006 +0200
@@ -41,6 +41,12 @@
 defs (overloaded)
   star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
 
+lemma Standard_scaleR [simp]: "x \<in> Standard \<Longrightarrow> r *# x \<in> Standard"
+by (simp add: star_scaleR_def)
+
+lemma star_of_scaleR [simp]: "star_of (r *# x) = r *# star_of x"
+by transfer (rule refl)
+
 instance star :: (real_vector) real_vector
 proof
   fix a b :: real
@@ -69,8 +75,11 @@
 
 instance star :: (real_field) real_field ..
 
-lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)"
-by (rule eq_reflection, unfold of_real_def, transfer, rule refl)
+lemma star_of_real_def [transfer_unfold]: "of_real r = star_of (of_real r)"
+by (unfold of_real_def, transfer, rule refl)
+
+lemma Standard_of_real [simp]: "of_real r \<in> Standard"
+by (simp add: star_of_real_def)
 
 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r"
 by transfer (rule refl)