# HG changeset patch
# User huffman
# Date 1176341850 -7200
# Node ID a5dc96fad632b6ff0ef56a931fa5e21289fecc8c
# Parent  f3a6c9389e7b387915ae94d60e99c54a218a2c50
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy

diff -r f3a6c9389e7b -r a5dc96fad632 src/HOL/Hyperreal/Deriv.thy
--- a/src/HOL/Hyperreal/Deriv.thy	Thu Apr 12 02:59:44 2007 +0200
+++ b/src/HOL/Hyperreal/Deriv.thy	Thu Apr 12 03:37:30 2007 +0200
@@ -9,7 +9,7 @@
 header{* Differentiation *}
 
 theory Deriv
-imports Lim
+imports HLim
 begin
 
 text{*Standard and Nonstandard Definitions*}
diff -r f3a6c9389e7b -r a5dc96fad632 src/HOL/Hyperreal/HLim.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Hyperreal/HLim.thy	Thu Apr 12 03:37:30 2007 +0200
@@ -0,0 +1,385 @@
+(*  Title       : HLim.thy
+    ID          : $Id$
+    Author      : Jacques D. Fleuriot
+    Copyright   : 1998  University of Cambridge
+    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
+*)
+
+header{* Limits and Continuity (Nonstandard) *}
+
+theory HLim
+imports HSEQ Lim
+begin
+
+text{*Nonstandard Definitions*}
+
+definition
+  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
+            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
+  "f -- a --NS> L =
+    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
+
+definition
+  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
+    --{*NS definition dispenses with limit notions*}
+  "isNSCont f a = (\<forall>y. y @= star_of a -->
+         ( *f* f) y @= star_of (f a))"
+
+definition
+  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
+  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+
+
+subsection {* Limits of Functions *}
+
+lemma NSLIM_I:
+  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
+   \<Longrightarrow> f -- a --NS> L"
+by (simp add: NSLIM_def)
+
+lemma NSLIM_D:
+  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
+   \<Longrightarrow> starfun f x \<approx> star_of L"
+by (simp add: NSLIM_def)
+
+text{*Proving properties of limits using nonstandard definition.
+      The properties hold for standard limits as well!*}
+
+lemma NSLIM_mult:
+  fixes l m :: "'a::real_normed_algebra"
+  shows "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
+by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
+
+lemma starfun_scaleR [simp]:
+  "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
+by transfer (rule refl)
+
+lemma NSLIM_scaleR:
+  "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
+by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
+
+lemma NSLIM_add:
+     "[| f -- x --NS> l; g -- x --NS> m |]
+      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
+by (auto simp add: NSLIM_def intro!: approx_add)
+
+lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
+by (simp add: NSLIM_def)
+
+lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
+by (simp add: NSLIM_def)
+
+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)"
+by (simp only: NSLIM_add NSLIM_minus)
+
+lemma NSLIM_inverse:
+  fixes L :: "'a::real_normed_div_algebra"
+  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
+      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
+apply (simp add: NSLIM_def, clarify)
+apply (drule spec)
+apply (auto simp add: star_of_approx_inverse)
+done
+
+lemma NSLIM_zero:
+  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_diff [OF f NSLIM_const])
+  thus ?thesis by simp
+qed
+
+lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
+apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
+apply (auto simp add: diff_minus add_assoc)
+done
+
+lemma NSLIM_const_not_eq:
+  fixes a :: real (*TODO: generalize to real_normed_div_algebra*)
+  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
+apply (simp add: NSLIM_def)
+apply (rule_tac x="star_of a + epsilon" in exI)
+apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
+            simp add: hypreal_epsilon_not_zero)
+done
+
+lemma NSLIM_not_zero:
+  fixes a :: real
+  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
+by (rule NSLIM_const_not_eq)
+
+lemma NSLIM_const_eq:
+  fixes a :: real
+  shows "(%x. k) -- a --NS> L ==> k = L"
+apply (rule ccontr)
+apply (blast dest: NSLIM_const_not_eq)
+done
+
+text{* can actually be proved more easily by unfolding the definition!*}
+lemma NSLIM_unique:
+  fixes a :: real
+  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
+apply (drule NSLIM_minus)
+apply (drule NSLIM_add, assumption)
+apply (auto dest!: NSLIM_const_eq [symmetric])
+apply (simp add: diff_def [symmetric])
+done
+
+lemma NSLIM_mult_zero:
+  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
+  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
+by (drule NSLIM_mult, auto)
+
+lemma NSLIM_self: "(%x. x) -- a --NS> a"
+by (simp add: NSLIM_def)
+
+subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
+
+lemma LIM_NSLIM:
+  assumes f: "f -- a --> L" shows "f -- a --NS> L"
+proof (rule NSLIM_I)
+  fix x
+  assume neq: "x \<noteq> star_of a"
+  assume approx: "x \<approx> star_of a"
+  have "starfun f x - star_of L \<in> Infinitesimal"
+  proof (rule InfinitesimalI2)
+    fix r::real assume r: "0 < r"
+    from LIM_D [OF f r]
+    obtain s where s: "0 < s" and
+      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
+      by fast
+    from less_r have less_r':
+       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
+        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
+      by transfer
+    from approx have "x - star_of a \<in> Infinitesimal"
+      by (unfold approx_def)
+    hence "hnorm (x - star_of a) < star_of s"
+      using s by (rule InfinitesimalD2)
+    with neq show "hnorm (starfun f x - star_of L) < star_of r"
+      by (rule less_r')
+  qed
+  thus "starfun f x \<approx> star_of L"
+    by (unfold approx_def)
+qed
+
+lemma NSLIM_LIM:
+  assumes f: "f -- a --NS> L" shows "f -- a --> L"
+proof (rule LIM_I)
+  fix r::real assume r: "0 < r"
+  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
+        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
+  proof (rule exI, safe)
+    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
+  next
+    fix x assume neq: "x \<noteq> star_of a"
+    assume "hnorm (x - star_of a) < epsilon"
+    with Infinitesimal_epsilon
+    have "x - star_of a \<in> Infinitesimal"
+      by (rule hnorm_less_Infinitesimal)
+    hence "x \<approx> star_of a"
+      by (unfold approx_def)
+    with f neq have "starfun f x \<approx> star_of L"
+      by (rule NSLIM_D)
+    hence "starfun f x - star_of L \<in> Infinitesimal"
+      by (unfold approx_def)
+    thus "hnorm (starfun f x - star_of L) < star_of r"
+      using r by (rule InfinitesimalD2)
+  qed
+  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
+    by transfer
+qed
+
+theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
+by (blast intro: LIM_NSLIM NSLIM_LIM)
+
+
+subsection {* Continuity *}
+
+lemma isNSContD:
+  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
+by (simp add: isNSCont_def)
+
+lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
+by (simp add: isNSCont_def NSLIM_def)
+
+lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
+apply (simp add: isNSCont_def NSLIM_def, auto)
+apply (case_tac "y = star_of a", auto)
+done
+
+text{*NS continuity can be defined using NS Limit in
+    similar fashion to standard def of continuity*}
+lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
+by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
+
+text{*Hence, NS continuity can be given
+  in terms of standard limit*}
+lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
+by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
+
+text{*Moreover, it's trivial now that NS continuity
+  is equivalent to standard continuity*}
+lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
+apply (simp add: isCont_def)
+apply (rule isNSCont_LIM_iff)
+done
+
+text{*Standard continuity ==> NS continuity*}
+lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
+by (erule isNSCont_isCont_iff [THEN iffD2])
+
+text{*NS continuity ==> Standard continuity*}
+lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
+by (erule isNSCont_isCont_iff [THEN iffD1])
+
+text{*Alternative definition of continuity*}
+
+(* Prove equivalence between NS limits - *)
+(* seems easier than using standard def  *)
+lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
+apply (simp add: NSLIM_def, auto)
+apply (drule_tac x = "star_of a + x" in spec)
+apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
+apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
+apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
+ prefer 2 apply (simp add: add_commute diff_def [symmetric])
+apply (rule_tac x = x in star_cases)
+apply (rule_tac [2] x = x in star_cases)
+apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
+done
+
+lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
+by (rule NSLIM_h_iff)
+
+lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
+by (simp add: isNSCont_def)
+
+lemma isNSCont_inverse:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
+  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
+by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
+
+lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
+by (simp add: isNSCont_def)
+
+lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
+apply (simp add: isNSCont_def)
+apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
+done
+
+(****************************************************************
+(%* Leave as commented until I add topology theory or remove? *%)
+(%*------------------------------------------------------------
+  Elementary topology proof for a characterisation of
+  continuity now: a function f is continuous if and only
+  if the inverse image, {x. f(x) \<in> A}, of any open set A
+  is always an open set
+ ------------------------------------------------------------*%)
+Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
+               ==> isNSopen {x. f x \<in> A}"
+by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
+by (dtac (mem_monad_approx RS approx_sym);
+by (dres_inst_tac [("x","a")] spec 1);
+by (dtac isNSContD 1 THEN assume_tac 1)
+by (dtac bspec 1 THEN assume_tac 1)
+by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
+by (blast_tac (claset() addIs [starfun_mem_starset]);
+qed "isNSCont_isNSopen";
+
+Goalw [isNSCont_def]
+          "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
+\              ==> isNSCont f x";
+by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
+     (approx_minus_iff RS iffD2)],simpset() addsimps
+      [Infinitesimal_def,SReal_iff]));
+by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
+by (etac (isNSopen_open_interval RSN (2,impE));
+by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
+by (dres_inst_tac [("x","x")] spec 1);
+by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
+    simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
+qed "isNSopen_isNSCont";
+
+Goal "(\<forall>x. isNSCont f x) = \
+\     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
+by (blast_tac (claset() addIs [isNSCont_isNSopen,
+    isNSopen_isNSCont]);
+qed "isNSCont_isNSopen_iff";
+
+(%*------- Standard version of same theorem --------*%)
+Goal "(\<forall>x. isCont f x) = \
+\         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
+by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
+              simpset() addsimps [isNSopen_isopen_iff RS sym,
+              isNSCont_isCont_iff RS sym]));
+qed "isCont_isopen_iff";
+*******************************************************************)
+
+subsection {* Uniform Continuity *}
+
+lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
+by (simp add: isNSUCont_def)
+
+lemma isUCont_isNSUCont:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes f: "isUCont f" shows "isNSUCont f"
+proof (unfold isNSUCont_def, safe)
+  fix x y :: "'a star"
+  assume approx: "x \<approx> y"
+  have "starfun f x - starfun f y \<in> Infinitesimal"
+  proof (rule InfinitesimalI2)
+    fix r::real assume r: "0 < r"
+    with f obtain s where s: "0 < s" and
+      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
+      by (auto simp add: isUCont_def)
+    from less_r have less_r':
+       "\<And>x y. hnorm (x - y) < star_of s
+        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
+      by transfer
+    from approx have "x - y \<in> Infinitesimal"
+      by (unfold approx_def)
+    hence "hnorm (x - y) < star_of s"
+      using s by (rule InfinitesimalD2)
+    thus "hnorm (starfun f x - starfun f y) < star_of r"
+      by (rule less_r')
+  qed
+  thus "starfun f x \<approx> starfun f y"
+    by (unfold approx_def)
+qed
+
+lemma isNSUCont_isUCont:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
+  assumes f: "isNSUCont f" shows "isUCont f"
+proof (unfold isUCont_def, safe)
+  fix r::real assume r: "0 < r"
+  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
+        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
+  proof (rule exI, safe)
+    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
+  next
+    fix x y :: "'a star"
+    assume "hnorm (x - y) < epsilon"
+    with Infinitesimal_epsilon
+    have "x - y \<in> Infinitesimal"
+      by (rule hnorm_less_Infinitesimal)
+    hence "x \<approx> y"
+      by (unfold approx_def)
+    with f have "starfun f x \<approx> starfun f y"
+      by (simp add: isNSUCont_def)
+    hence "starfun f x - starfun f y \<in> Infinitesimal"
+      by (unfold approx_def)
+    thus "hnorm (starfun f x - starfun f y) < star_of r"
+      using r by (rule InfinitesimalD2)
+  qed
+  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
+    by transfer
+qed
+
+end
diff -r f3a6c9389e7b -r a5dc96fad632 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Thu Apr 12 02:59:44 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Thu Apr 12 03:37:30 2007 +0200
@@ -8,10 +8,10 @@
 header{* Limits and Continuity *}
 
 theory Lim
-imports HSEQ
+imports SEQ
 begin
 
-text{*Standard and Nonstandard Definitions*}
+text{*Standard Definitions*}
 
 definition
   LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
@@ -21,29 +21,13 @@
         --> norm (f x - L) < r)"
 
 definition
-  NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
-            ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
-  "f -- a --NS> L =
-    (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
-
-definition
   isCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
   "isCont f a = (f -- a --> (f a))"
 
 definition
-  isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
-    --{*NS definition dispenses with limit notions*}
-  "isNSCont f a = (\<forall>y. y @= star_of a -->
-         ( *f* f) y @= star_of (f a))"
-
-definition
   isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
   "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
 
-definition
-  isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
-  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
-
 
 subsection {* Limits of Functions *}
 
@@ -374,6 +358,8 @@
   shows "(\<lambda>x. f x ^ n) -- a --> l ^ n"
 by (induct n, simp, simp add: power_Suc LIM_mult f)
 
+subsubsection {* Derived theorems about @{term LIM} *}
+
 lemma LIM_inverse_lemma:
   fixes x :: "'a::real_normed_div_algebra"
   assumes r: "0 < r"
@@ -436,175 +422,6 @@
   shows "\<lbrakk>f -- a --> L; L \<noteq> 0\<rbrakk> \<Longrightarrow> (\<lambda>x. inverse (f x)) -- a --> inverse L"
 by (rule LIM_inverse_fun [THEN LIM_compose])
 
-subsubsection {* Purely nonstandard proofs *}
-
-lemma NSLIM_I:
-  "(\<And>x. \<lbrakk>x \<noteq> star_of a; x \<approx> star_of a\<rbrakk> \<Longrightarrow> starfun f x \<approx> star_of L)
-   \<Longrightarrow> f -- a --NS> L"
-by (simp add: NSLIM_def)
-
-lemma NSLIM_D:
-  "\<lbrakk>f -- a --NS> L; x \<noteq> star_of a; x \<approx> star_of a\<rbrakk>
-   \<Longrightarrow> starfun f x \<approx> star_of L"
-by (simp add: NSLIM_def)
-
-text{*Proving properties of limits using nonstandard definition.
-      The properties hold for standard limits as well!*}
-
-lemma NSLIM_mult:
-  fixes l m :: "'a::real_normed_algebra"
-  shows "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) * g(x)) -- x --NS> (l * m)"
-by (auto simp add: NSLIM_def intro!: approx_mult_HFinite)
-
-lemma starfun_scaleR [simp]:
-  "starfun (\<lambda>x. f x *# g x) = (\<lambda>x. scaleHR (starfun f x) (starfun g x))"
-by transfer (rule refl)
-
-lemma NSLIM_scaleR:
-  "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) *# g(x)) -- x --NS> (l *# m)"
-by (auto simp add: NSLIM_def intro!: approx_scaleR_HFinite)
-
-lemma NSLIM_add:
-     "[| f -- x --NS> l; g -- x --NS> m |]
-      ==> (%x. f(x) + g(x)) -- x --NS> (l + m)"
-by (auto simp add: NSLIM_def intro!: approx_add)
-
-lemma NSLIM_const [simp]: "(%x. k) -- x --NS> k"
-by (simp add: NSLIM_def)
-
-lemma NSLIM_minus: "f -- a --NS> L ==> (%x. -f(x)) -- a --NS> -L"
-by (simp add: NSLIM_def)
-
-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)"
-by (simp only: NSLIM_add NSLIM_minus)
-
-lemma NSLIM_inverse:
-  fixes L :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --NS> L;  L \<noteq> 0 |]
-      ==> (%x. inverse(f(x))) -- a --NS> (inverse L)"
-apply (simp add: NSLIM_def, clarify)
-apply (drule spec)
-apply (auto simp add: star_of_approx_inverse)
-done
-
-lemma NSLIM_zero:
-  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_diff [OF f NSLIM_const])
-  thus ?thesis by simp
-qed
-
-lemma NSLIM_zero_cancel: "(%x. f(x) - l) -- x --NS> 0 ==> f -- x --NS> l"
-apply (drule_tac g = "%x. l" and m = l in NSLIM_add)
-apply (auto simp add: diff_minus add_assoc)
-done
-
-lemma NSLIM_const_not_eq:
-  fixes a :: real (* TODO: generalize to real_normed_div_algebra *)
-  shows "k \<noteq> L ==> ~ ((%x. k) -- a --NS> L)"
-apply (simp add: NSLIM_def)
-apply (rule_tac x="star_of a + epsilon" in exI)
-apply (auto intro: Infinitesimal_add_approx_self [THEN approx_sym]
-            simp add: hypreal_epsilon_not_zero)
-done
-
-lemma NSLIM_not_zero:
-  fixes a :: real
-  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
-by (rule NSLIM_const_not_eq)
-
-lemma NSLIM_const_eq:
-  fixes a :: real
-  shows "(%x. k) -- a --NS> L ==> k = L"
-apply (rule ccontr)
-apply (blast dest: NSLIM_const_not_eq)
-done
-
-text{* can actually be proved more easily by unfolding the definition!*}
-lemma NSLIM_unique:
-  fixes a :: real
-  shows "[| f -- a --NS> L; f -- a --NS> M |] ==> L = M"
-apply (drule NSLIM_minus)
-apply (drule NSLIM_add, assumption)
-apply (auto dest!: NSLIM_const_eq [symmetric])
-apply (simp add: diff_def [symmetric])
-done
-
-lemma NSLIM_mult_zero:
-  fixes f g :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_algebra"
-  shows "[| f -- x --NS> 0; g -- x --NS> 0 |] ==> (%x. f(x)*g(x)) -- x --NS> 0"
-by (drule NSLIM_mult, auto)
-
-lemma NSLIM_self: "(%x. x) -- a --NS> a"
-by (simp add: NSLIM_def)
-
-subsubsection {* Equivalence of @{term LIM} and @{term NSLIM} *}
-
-lemma LIM_NSLIM:
-  assumes f: "f -- a --> L" shows "f -- a --NS> L"
-proof (rule NSLIM_I)
-  fix x
-  assume neq: "x \<noteq> star_of a"
-  assume approx: "x \<approx> star_of a"
-  have "starfun f x - star_of L \<in> Infinitesimal"
-  proof (rule InfinitesimalI2)
-    fix r::real assume r: "0 < r"
-    from LIM_D [OF f r]
-    obtain s where s: "0 < s" and
-      less_r: "\<And>x. \<lbrakk>x \<noteq> a; norm (x - a) < s\<rbrakk> \<Longrightarrow> norm (f x - L) < r"
-      by fast
-    from less_r have less_r':
-       "\<And>x. \<lbrakk>x \<noteq> star_of a; hnorm (x - star_of a) < star_of s\<rbrakk>
-        \<Longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
-      by transfer
-    from approx have "x - star_of a \<in> Infinitesimal"
-      by (unfold approx_def)
-    hence "hnorm (x - star_of a) < star_of s"
-      using s by (rule InfinitesimalD2)
-    with neq show "hnorm (starfun f x - star_of L) < star_of r"
-      by (rule less_r')
-  qed
-  thus "starfun f x \<approx> star_of L"
-    by (unfold approx_def)
-qed
-
-lemma NSLIM_LIM:
-  assumes f: "f -- a --NS> L" shows "f -- a --> L"
-proof (rule LIM_I)
-  fix r::real assume r: "0 < r"
-  have "\<exists>s>0. \<forall>x. x \<noteq> star_of a \<and> hnorm (x - star_of a) < s
-        \<longrightarrow> hnorm (starfun f x - star_of L) < star_of r"
-  proof (rule exI, safe)
-    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
-  next
-    fix x assume neq: "x \<noteq> star_of a"
-    assume "hnorm (x - star_of a) < epsilon"
-    with Infinitesimal_epsilon
-    have "x - star_of a \<in> Infinitesimal"
-      by (rule hnorm_less_Infinitesimal)
-    hence "x \<approx> star_of a"
-      by (unfold approx_def)
-    with f neq have "starfun f x \<approx> star_of L"
-      by (rule NSLIM_D)
-    hence "starfun f x - star_of L \<in> Infinitesimal"
-      by (unfold approx_def)
-    thus "hnorm (starfun f x - star_of L) < star_of r"
-      using r by (rule InfinitesimalD2)
-  qed
-  thus "\<exists>s>0. \<forall>x. x \<noteq> a \<and> norm (x - a) < s \<longrightarrow> norm (f x - L) < r"
-    by transfer
-qed
-
-theorem LIM_NSLIM_iff: "(f -- x --> L) = (f -- x --NS> L)"
-by (blast intro: LIM_NSLIM NSLIM_LIM)
-
 
 subsection {* Continuity *}
 
@@ -675,193 +492,15 @@
   shows "isCont f a \<Longrightarrow> isCont (\<lambda>x. f x ^ n) a"
   unfolding isCont_def by (rule LIM_power)
 
-subsubsection {* Nonstandard proofs *}
-
-lemma isNSContD:
-  "\<lbrakk>isNSCont f a; y \<approx> star_of a\<rbrakk> \<Longrightarrow> ( *f* f) y \<approx> star_of (f a)"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_NSLIM: "isNSCont f a ==> f -- a --NS> (f a) "
-by (simp add: isNSCont_def NSLIM_def)
-
-lemma NSLIM_isNSCont: "f -- a --NS> (f a) ==> isNSCont f a"
-apply (simp add: isNSCont_def NSLIM_def, auto)
-apply (case_tac "y = star_of a", auto)
-done
-
-text{*NS continuity can be defined using NS Limit in
-    similar fashion to standard def of continuity*}
-lemma isNSCont_NSLIM_iff: "(isNSCont f a) = (f -- a --NS> (f a))"
-by (blast intro: isNSCont_NSLIM NSLIM_isNSCont)
-
-text{*Hence, NS continuity can be given
-  in terms of standard limit*}
-lemma isNSCont_LIM_iff: "(isNSCont f a) = (f -- a --> (f a))"
-by (simp add: LIM_NSLIM_iff isNSCont_NSLIM_iff)
-
-text{*Moreover, it's trivial now that NS continuity
-  is equivalent to standard continuity*}
-lemma isNSCont_isCont_iff: "(isNSCont f a) = (isCont f a)"
-apply (simp add: isCont_def)
-apply (rule isNSCont_LIM_iff)
-done
-
-text{*Standard continuity ==> NS continuity*}
-lemma isCont_isNSCont: "isCont f a ==> isNSCont f a"
-by (erule isNSCont_isCont_iff [THEN iffD2])
-
-text{*NS continuity ==> Standard continuity*}
-lemma isNSCont_isCont: "isNSCont f a ==> isCont f a"
-by (erule isNSCont_isCont_iff [THEN iffD1])
-
-text{*Alternative definition of continuity*}
-(* Prove equivalence between NS limits - *)
-(* seems easier than using standard def  *)
-lemma NSLIM_h_iff: "(f -- a --NS> L) = ((%h. f(a + h)) -- 0 --NS> L)"
-apply (simp add: NSLIM_def, auto)
-apply (drule_tac x = "star_of a + x" in spec)
-apply (drule_tac [2] x = "- star_of a + x" in spec, safe, simp)
-apply (erule mem_infmal_iff [THEN iffD2, THEN Infinitesimal_add_approx_self [THEN approx_sym]])
-apply (erule_tac [3] approx_minus_iff2 [THEN iffD1])
- prefer 2 apply (simp add: add_commute diff_def [symmetric])
-apply (rule_tac x = x in star_cases)
-apply (rule_tac [2] x = x in star_cases)
-apply (auto simp add: starfun star_of_def star_n_minus star_n_add add_assoc approx_refl star_n_zero_num)
-done
-
-lemma NSLIM_isCont_iff: "(f -- a --NS> f a) = ((%h. f(a + h)) -- 0 --NS> f a)"
-by (rule NSLIM_h_iff)
-
-lemma isNSCont_minus: "isNSCont f a ==> isNSCont (%x. - f x) a"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_inverse:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
-  shows "[| isNSCont f x; f x \<noteq> 0 |] ==> isNSCont (%x. inverse (f x)) x"
-by (auto intro: isCont_inverse simp add: isNSCont_isCont_iff)
-
-lemma isNSCont_const [simp]: "isNSCont (%x. k) a"
-by (simp add: isNSCont_def)
-
-lemma isNSCont_abs [simp]: "isNSCont abs (a::real)"
-apply (simp add: isNSCont_def)
-apply (auto intro: approx_hrabs simp add: starfun_rabs_hrabs)
-done
-
 lemma isCont_abs [simp]: "isCont abs (a::real)"
-by (auto simp add: isNSCont_isCont_iff [symmetric])
+by (rule isCont_rabs [OF isCont_Id])
 
 
-(****************************************************************
-(%* Leave as commented until I add topology theory or remove? *%)
-(%*------------------------------------------------------------
-  Elementary topology proof for a characterisation of
-  continuity now: a function f is continuous if and only
-  if the inverse image, {x. f(x) \<in> A}, of any open set A
-  is always an open set
- ------------------------------------------------------------*%)
-Goal "[| isNSopen A; \<forall>x. isNSCont f x |]
-               ==> isNSopen {x. f x \<in> A}"
-by (auto_tac (claset(),simpset() addsimps [isNSopen_iff1]));
-by (dtac (mem_monad_approx RS approx_sym);
-by (dres_inst_tac [("x","a")] spec 1);
-by (dtac isNSContD 1 THEN assume_tac 1)
-by (dtac bspec 1 THEN assume_tac 1)
-by (dres_inst_tac [("x","( *f* f) x")] approx_mem_monad2 1);
-by (blast_tac (claset() addIs [starfun_mem_starset]);
-qed "isNSCont_isNSopen";
-
-Goalw [isNSCont_def]
-          "\<forall>A. isNSopen A --> isNSopen {x. f x \<in> A} \
-\              ==> isNSCont f x";
-by (auto_tac (claset() addSIs [(mem_infmal_iff RS iffD1) RS
-     (approx_minus_iff RS iffD2)],simpset() addsimps
-      [Infinitesimal_def,SReal_iff]));
-by (dres_inst_tac [("x","{z. abs(z + -f(x)) < ya}")] spec 1);
-by (etac (isNSopen_open_interval RSN (2,impE));
-by (auto_tac (claset(),simpset() addsimps [isNSopen_def,isNSnbhd_def]));
-by (dres_inst_tac [("x","x")] spec 1);
-by (auto_tac (claset() addDs [approx_sym RS approx_mem_monad],
-    simpset() addsimps [hypreal_of_real_zero RS sym,STAR_starfun_rabs_add_minus]));
-qed "isNSopen_isNSCont";
-
-Goal "(\<forall>x. isNSCont f x) = \
-\     (\<forall>A. isNSopen A --> isNSopen {x. f(x) \<in> A})";
-by (blast_tac (claset() addIs [isNSCont_isNSopen,
-    isNSopen_isNSCont]);
-qed "isNSCont_isNSopen_iff";
-
-(%*------- Standard version of same theorem --------*%)
-Goal "(\<forall>x. isCont f x) = \
-\         (\<forall>A. isopen A --> isopen {x. f(x) \<in> A})";
-by (auto_tac (claset() addSIs [isNSCont_isNSopen_iff],
-              simpset() addsimps [isNSopen_isopen_iff RS sym,
-              isNSCont_isCont_iff RS sym]));
-qed "isCont_isopen_iff";
-*******************************************************************)
-
 subsection {* Uniform Continuity *}
 
-lemma isNSUContD: "[| isNSUCont f; x \<approx> y|] ==> ( *f* f) x \<approx> ( *f* f) y"
-by (simp add: isNSUCont_def)
-
 lemma isUCont_isCont: "isUCont f ==> isCont f x"
 by (simp add: isUCont_def isCont_def LIM_def, meson)
 
-lemma isUCont_isNSUCont:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes f: "isUCont f" shows "isNSUCont f"
-proof (unfold isNSUCont_def, safe)
-  fix x y :: "'a star"
-  assume approx: "x \<approx> y"
-  have "starfun f x - starfun f y \<in> Infinitesimal"
-  proof (rule InfinitesimalI2)
-    fix r::real assume r: "0 < r"
-    with f obtain s where s: "0 < s" and
-      less_r: "\<And>x y. norm (x - y) < s \<Longrightarrow> norm (f x - f y) < r"
-      by (auto simp add: isUCont_def)
-    from less_r have less_r':
-       "\<And>x y. hnorm (x - y) < star_of s
-        \<Longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
-      by transfer
-    from approx have "x - y \<in> Infinitesimal"
-      by (unfold approx_def)
-    hence "hnorm (x - y) < star_of s"
-      using s by (rule InfinitesimalD2)
-    thus "hnorm (starfun f x - starfun f y) < star_of r"
-      by (rule less_r')
-  qed
-  thus "starfun f x \<approx> starfun f y"
-    by (unfold approx_def)
-qed
-
-lemma isNSUCont_isUCont:
-  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
-  assumes f: "isNSUCont f" shows "isUCont f"
-proof (unfold isUCont_def, safe)
-  fix r::real assume r: "0 < r"
-  have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s
-        \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
-  proof (rule exI, safe)
-    show "0 < epsilon" by (rule hypreal_epsilon_gt_zero)
-  next
-    fix x y :: "'a star"
-    assume "hnorm (x - y) < epsilon"
-    with Infinitesimal_epsilon
-    have "x - y \<in> Infinitesimal"
-      by (rule hnorm_less_Infinitesimal)
-    hence "x \<approx> y"
-      by (unfold approx_def)
-    with f have "starfun f x \<approx> starfun f y"
-      by (simp add: isNSUCont_def)
-    hence "starfun f x - starfun f y \<in> Infinitesimal"
-      by (unfold approx_def)
-    thus "hnorm (starfun f x - starfun f y) < star_of r"
-      using r by (rule InfinitesimalD2)
-  qed
-  thus "\<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r"
-    by transfer
-qed
 
 subsection {* Relation of LIM and LIMSEQ *}
 
diff -r f3a6c9389e7b -r a5dc96fad632 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Apr 12 02:59:44 2007 +0200
+++ b/src/HOL/IsaMakefile	Thu Apr 12 03:37:30 2007 +0200
@@ -161,7 +161,7 @@
   Hyperreal/StarDef.thy Hyperreal/StarClasses.thy				\
   Hyperreal/EvenOdd.thy Hyperreal/Fact.thy Hyperreal/HLog.thy			\
   Hyperreal/Filter.thy Hyperreal/HSeries.thy Hyperreal/transfer.ML		\
-  Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy				\
+  Hyperreal/HLim.thy Hyperreal/HSEQ.thy Hyperreal/HTranscendental.thy		\
   Hyperreal/HyperDef.thy Hyperreal/HyperNat.thy					\
   Hyperreal/Hyperreal.thy							\
   Hyperreal/Integration.thy Hyperreal/Lim.thy Hyperreal/Log.thy			\