# HG changeset patch
# User huffman
# Date 1159387982 -7200
# Node ID 22b0e2f3fe7e8f6e2f2d22f3d48a33547302af07
# Parent  2233f6afc491aeca5d0cff3c464207959048a71b
add lemmas about hnorm, Infinitesimal

diff -r 2233f6afc491 -r 22b0e2f3fe7e src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 21:53:55 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Sep 27 22:13:02 2006 +0200
@@ -494,13 +494,21 @@
   "(x::hypreal) \<in> HFinite - Infinitesimal ==> abs x \<in> HFinite - Infinitesimal"
 by blast
 
-lemma hrabs_less_Infinitesimal:
-      "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
+lemma hnorm_le_Infinitesimal:
+  "\<lbrakk>e \<in> Infinitesimal; hnorm x \<le> e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
 by (auto simp add: Infinitesimal_def abs_less_iff)
 
+lemma hnorm_less_Infinitesimal:
+  "\<lbrakk>e \<in> Infinitesimal; hnorm x < e\<rbrakk> \<Longrightarrow> x \<in> Infinitesimal"
+by (erule hnorm_le_Infinitesimal, erule order_less_imp_le)
+
 lemma hrabs_le_Infinitesimal:
      "[| e \<in> Infinitesimal; abs (x::hypreal) \<le> e |] ==> x \<in> Infinitesimal"
-by (blast dest: order_le_imp_less_or_eq intro: hrabs_less_Infinitesimal)
+by (erule hnorm_le_Infinitesimal, simp)
+
+lemma hrabs_less_Infinitesimal:
+      "[| e \<in> Infinitesimal; abs (x::hypreal) < e |] ==> x \<in> Infinitesimal"
+by (erule hnorm_less_Infinitesimal, simp)
 
 lemma Infinitesimal_interval:
       "[| e \<in> Infinitesimal; e' \<in> Infinitesimal; e' < x ; x < e |]