author huffman Thu, 21 Sep 2006 03:16:50 +0200 changeset 20652 6e9b7617c89a parent 20651 41a63aabea83 child 20653 24cda2c5fd40
added approx_hnorm theorem; removed division_by_zero class requirements from several lemmas
 src/HOL/Hyperreal/NSA.thy file | annotate | diff | comparison | revisions
```--- 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)"

+lemma Infinitesimal_hnorm_iff:
+  "(hnorm x \<in> Infinitesimal) = (x \<in> Infinitesimal)"
+
lemma Infinitesimal_diff:
"[| x \<in> Infinitesimal;  y \<in> Infinitesimal |] ==> x-y \<in> Infinitesimal"
@@ -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
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]

-  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

-  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

-  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 @@

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 @@