# HG changeset patch
# User huffman
# Date 1159328369 -7200
# Node ID 8d21108bc6dd9a35da9ac8a0fe2bb2308f2e5a77
# Parent  3ca92a58ebd7d8c3868cbb45d3f3c8a00a12f96a
move star_of_norm from SEQ.thy to NSA.thy

diff -r 3ca92a58ebd7 -r 8d21108bc6dd src/HOL/Hyperreal/NSA.thy
--- 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
 
diff -r 3ca92a58ebd7 -r 8d21108bc6dd src/HOL/Hyperreal/SEQ.thy
--- 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)