# HG changeset patch
# User huffman
# Date 1158801410 -7200
# Node ID 6e9b7617c89a537fa25943651fef11a22a8f9fba
# Parent  41a63aabea8382744ef5a0bb7a8cb4acc313dd08
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas

diff -r 41a63aabea83 -r 6e9b7617c89a src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Wed Sep 20 23:30:40 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Sep 21 03:16:50 2006 +0200
@@ -74,6 +74,10 @@
   "\<And>x y::'a::real_normed_vector star. hnorm (x + y) \<le> hnorm x + hnorm y"
 by transfer (rule norm_triangle_ineq)
 
+lemma hnorm_triangle_ineq3:
+  "\<And>x y::'a::real_normed_vector star. \<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)"
+by transfer (rule norm_triangle_ineq3)
+
 lemma hnorm_scaleR:
   "\<And>a (x::'a::real_normed_vector star).
    hnorm (( *f2* scaleR) a x) = \<bar>a\<bar> * hnorm x"
@@ -414,6 +418,10 @@
 lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
 by (simp add: Infinitesimal_def)
 
+lemma Infinitesimal_hnorm_iff:
+  "(hnorm x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+by (simp add: Infinitesimal_def)
+
 lemma Infinitesimal_diff:
      "[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
 by (simp add: diff_def Infinitesimal_add)
@@ -889,6 +897,25 @@
 apply (rule_tac [2] Infinitesimal_zero, auto)
 done
 
+lemma approx_hnorm:
+  fixes x y :: "'a::real_normed_vector star"
+  shows "x \<approx> y \<Longrightarrow> hnorm x \<approx> hnorm y"
+proof (unfold approx_def)
+  assume "x - y \<in> Infinitesimal"
+  hence 1: "hnorm (x - y) \<in> Infinitesimal"
+    by (simp only: Infinitesimal_hnorm_iff)
+  moreover have 2: "(0::real star) \<in> Infinitesimal"
+    by (rule Infinitesimal_zero)
+  moreover have 3: "0 \<le> \<bar>hnorm x - hnorm y\<bar>"
+    by (rule abs_ge_zero)
+  moreover have 4: "\<bar>hnorm x - hnorm y\<bar> \<le> hnorm (x - y)"
+    by (rule hnorm_triangle_ineq3)
+  ultimately have "\<bar>hnorm x - hnorm y\<bar> \<in> Infinitesimal"
+    by (rule Infinitesimal_interval2)
+  thus "hnorm x - hnorm y \<in> Infinitesimal"
+    by (simp only: Infinitesimal_hrabs_iff)
+qed
+
 
 subsection{* Zero is the Only Infinitesimal that is also a Real*}
 
@@ -1274,27 +1301,29 @@
 by (fast intro: not_HFinite_HInfinite)
 
 lemma HFinite_inverse:
-  fixes x :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x :: "'a::real_normed_div_algebra star"
   shows "[| x \<in> HFinite; x \<notin> Infinitesimal |] ==> inverse x \<in> HFinite"
+apply (subgoal_tac "x \<noteq> 0")
 apply (cut_tac x = "inverse x" in HInfinite_HFinite_disj)
-apply (auto dest!: HInfinite_inverse_Infinitesimal)
+apply (auto dest!: HInfinite_inverse_Infinitesimal
+            simp add: nonzero_inverse_inverse_eq)
 done
 
 lemma HFinite_inverse2:
-  fixes x :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x :: "'a::real_normed_div_algebra star"
   shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite"
 by (blast intro: HFinite_inverse)
 
 (* stronger statement possible in fact *)
 lemma Infinitesimal_inverse_HFinite:
-  fixes x :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x :: "'a::real_normed_div_algebra star"
   shows "x \<notin> Infinitesimal ==> inverse(x) \<in> HFinite"
 apply (drule HInfinite_diff_HFinite_Infinitesimal_disj)
 apply (blast intro: HFinite_inverse HInfinite_inverse_Infinitesimal Infinitesimal_subset_HFinite [THEN subsetD])
 done
 
 lemma HFinite_not_Infinitesimal_inverse:
-  fixes x :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x :: "'a::real_normed_div_algebra star"
   shows "x \<in> HFinite - Infinitesimal ==> inverse x \<in> HFinite - Infinitesimal"
 apply (auto intro: Infinitesimal_inverse_HFinite)
 apply (drule Infinitesimal_HFinite_mult2, assumption)
@@ -1302,7 +1331,7 @@
 done
 
 lemma approx_inverse:
-  fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x y :: "'a::real_normed_div_algebra star"
   shows
      "[| x @= y; y \<in>  HFinite - Infinitesimal |]
       ==> inverse x @= inverse y"
@@ -1320,7 +1349,7 @@
 lemmas hypreal_of_real_approx_inverse =  hypreal_of_real_HFinite_diff_Infinitesimal [THEN [2] approx_inverse]
 
 lemma inverse_add_Infinitesimal_approx:
-  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x h :: "'a::real_normed_div_algebra star"
   shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(x + h) @= inverse x"
@@ -1328,7 +1357,7 @@
 done
 
 lemma inverse_add_Infinitesimal_approx2:
-  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x h :: "'a::real_normed_div_algebra star"
   shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(h + x) @= inverse x"
@@ -1337,7 +1366,7 @@
 done
 
 lemma inverse_add_Infinitesimal_approx_Infinitesimal:
-  fixes x h :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x h :: "'a::real_normed_div_algebra star"
   shows
      "[| x \<in> HFinite - Infinitesimal;
          h \<in> Infinitesimal |] ==> inverse(x + h) - inverse x @= h"
@@ -1347,7 +1376,7 @@
 done
 
 lemma Infinitesimal_square_iff:
-  fixes x :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x :: "'a::real_normed_div_algebra star"
   shows "(x \<in> Infinitesimal) = (x*x \<in> Infinitesimal)"
 apply (auto intro: Infinitesimal_mult)
 apply (rule ccontr, frule Infinitesimal_inverse_HFinite)
@@ -1369,7 +1398,7 @@
 by (auto simp add: HInfinite_HFinite_iff)
 
 lemma approx_HFinite_mult_cancel:
-  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes a w z :: "'a::real_normed_div_algebra star"
   shows "[| a: HFinite-Infinitesimal; a* w @= a*z |] ==> w @= z"
 apply safe
 apply (frule HFinite_inverse, assumption)
@@ -1378,7 +1407,7 @@
 done
 
 lemma approx_HFinite_mult_cancel_iff1:
-  fixes a w z :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes a w z :: "'a::real_normed_div_algebra star"
   shows "a: HFinite-Infinitesimal ==> (a * w @= a * z) = (w @= z)"
 by (auto intro: approx_mult2 approx_HFinite_mult_cancel)
 
@@ -1407,7 +1436,7 @@
 done
 
 lemma HInfinite_HFinite_not_Infinitesimal_mult:
-  fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x y :: "'a::real_normed_div_algebra star"
   shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
       ==> x * y \<in> HInfinite"
 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
@@ -1418,7 +1447,7 @@
 done
 
 lemma HInfinite_HFinite_not_Infinitesimal_mult2:
-  fixes x y :: "'a::{real_normed_div_algebra,division_by_zero} star"
+  fixes x y :: "'a::real_normed_div_algebra star"
   shows "[| x \<in> HInfinite; y \<in> HFinite - Infinitesimal |]
       ==> y * x \<in> HInfinite"
 apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
@@ -1537,12 +1566,7 @@
 by (blast dest: Ball_mem_monad_less_zero approx_subset_monad)
 
 theorem approx_hrabs: "(x::hypreal) @= y ==> abs x @= abs y"
-apply (case_tac "x \<in> Infinitesimal") 
-apply (simp add: Infinitesimal_approx_hrabs)
-apply (rule linorder_cases [of 0 x])  
-apply (frule lemma_approx_gt_zero [of x y]) 
-apply (auto simp add: lemma_approx_less_zero [of x y] abs_of_neg)
-done
+by (drule approx_hnorm, simp)
 
 lemma approx_hrabs_zero_cancel: "abs(x::hypreal) @= 0 ==> x @= 0"
 apply (cut_tac x = x in hrabs_disj)