author huffman Tue, 12 Dec 2006 07:13:06 +0100 changeset 21786 66da6af2b0c9 parent 21785 885667874dfc child 21787 9edd495b6330
cleaned up; generalized some proofs
 src/HOL/Hyperreal/Lim.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/Lim.thy	Tue Dec 12 07:11:58 2006 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Tue Dec 12 07:13:06 2006 +0100
@@ -171,6 +171,8 @@
apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
done

+lemmas LIM_not_zero = LIM_const_not_eq [where L = 0]
+
lemma LIM_const_eq:
fixes a :: "'a::real_normed_div_algebra"
shows "(%x. k) -- a --> L ==> k = L"
@@ -535,6 +537,10 @@
lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"

+lemma NSLIM_diff:
+  "\<lbrakk>f -- x --NS> l; g -- x --NS> m\<rbrakk> \<Longrightarrow> (\<lambda>x. f x - g x) -- x --NS> (l - m)"
+by (simp only: diff_def NSLIM_add NSLIM_minus)
+
lemma NSLIM_add_minus: "[| f -- x --NS> l; g -- x --NS> m |] ==> (%x. f(x) + -g(x)) -- x --NS> (l + -m)"

@@ -548,10 +554,10 @@
done

lemma NSLIM_zero:
-  assumes f: "f -- a --NS> l" shows "(%x. f(x) + -l) -- a --NS> 0"
+  assumes f: "f -- a --NS> l" shows "(%x. f(x) - l) -- a --NS> 0"
proof -
-  have "(\<lambda>x. f x + - l) -- a --NS> l + -l"
-    by (rule NSLIM_add_minus [OF f NSLIM_const])
+  have "(\<lambda>x. f x - l) -- a --NS> l - l"
+    by (rule NSLIM_diff [OF f NSLIM_const])
thus ?thesis by simp
qed

@@ -691,7 +697,7 @@
==> (%x. inverse(f(x))) -- a --> (inverse L)"

-lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) + -l) -- a --> 0"
+lemma LIM_zero2: "f -- a --> l ==> (%x. f(x) - l) -- a --> 0"

lemma LIM_unique2:
@@ -721,9 +727,12 @@
lemma isCont_Id: "isCont (\<lambda>x. x) a"
unfolding isCont_def by (rule LIM_self)

-lemma isCont_const [simp]: "isCont (%x. k) a"
+lemma isCont_const [simp]: "isCont (\<lambda>x. k) a"
unfolding isCont_def by (rule LIM_const)

+lemma isCont_norm: "isCont f a \<Longrightarrow> isCont (\<lambda>x. norm (f x)) a"
+  unfolding isCont_def by (rule LIM_norm)
+
lemma isCont_add: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x + g x) a"

@@ -735,12 +744,12 @@

lemma isCont_mult:
fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| isCont f a; isCont g a |] ==> isCont (%x. f(x) * g(x)) a"
+  shows "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. f x * g x) a"
unfolding isCont_def by (rule LIM_mult)

lemma isCont_inverse:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
-  shows "[| isCont f x; f x \<noteq> 0 |] ==> isCont (%x. inverse (f x)) x"
+  shows "\<lbrakk>isCont f a; f a \<noteq> 0\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. inverse (f x)) a"
unfolding isCont_def by (rule LIM_inverse)

lemma isCont_LIM_compose:
@@ -764,7 +773,8 @@

subsubsection {* Nonstandard proofs *}

-lemma isNSContD: "[| isNSCont f a; y \<approx> hypreal_of_real a |] ==> ( *f* f) y \<approx> hypreal_of_real (f a)"
+lemma isNSContD:
+  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"