--- a/src/HOL/Hyperreal/NSA.thy Wed Sep 27 05:19:24 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Wed Sep 27 05:39:29 2006 +0200
@@ -62,6 +62,12 @@
declare hnorm_def [transfer_unfold]
+lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
+by (simp add: hnorm_def)
+
+lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
+by transfer (rule refl)
+
lemma hnorm_ge_zero [simp]:
"\<And>x::'a::real_normed_vector star. 0 \<le> hnorm x"
by transfer (rule norm_ge_zero)
@@ -913,7 +919,8 @@
"(star_of x \<in> Infinitesimal) = (x = 0)"
apply (auto simp add: Infinitesimal_def)
apply (drule_tac x="hnorm (star_of x)" in bspec)
-apply (simp add: hnorm_def)
+apply (simp add: SReal_def)
+apply (rule_tac x="norm x" in exI, simp)
apply simp
done
--- a/src/HOL/Hyperreal/SEQ.thy Wed Sep 27 05:19:24 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy Wed Sep 27 05:39:29 2006 +0200
@@ -160,9 +160,6 @@
lemma starfun_hnorm: "\<And>x. hnorm (( *f* f) x) = ( *f* (\<lambda>x. norm (f x))) x"
by transfer simp
-lemma star_of_norm [simp]: "star_of (norm x) = hnorm (star_of x)"
-by transfer simp
-
lemma NSLIMSEQ_norm: "X ----NS> a \<Longrightarrow> (\<lambda>n. norm (X n)) ----NS> norm a"
by (simp add: NSLIMSEQ_def starfun_hnorm [symmetric] approx_hnorm)