# HG changeset patch
# User huffman
# Date 1179856075 -7200
# Node ID 1b2acb3ccb2988b51f8f6f0bd43cd9cae55de0d4
# Parent  69e30a7e888018ac7e819d39b6d8f1f269324717
generalize uniqueness of limits to class real_normed_algebra_1

diff -r 69e30a7e8880 -r 1b2acb3ccb29 src/HOL/Hyperreal/HLim.thy
--- a/src/HOL/Hyperreal/HLim.thy	Tue May 22 17:56:06 2007 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Tue May 22 19:47:55 2007 +0200
@@ -101,34 +101,31 @@
 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)"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>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)
+apply (rule_tac x="star_of a + of_hypreal epsilon" in exI)
+apply (simp add: hypreal_epsilon_not_zero approx_def)
+apply (rule Infinitesimal_hnorm_iff [THEN iffD1], simp)
 done
 
 lemma NSLIM_not_zero:
-  fixes a :: real
-  shows "k \<noteq> 0 ==> ~ ((%x. k) -- a --NS> 0)"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "k \<noteq> 0 \<Longrightarrow> \<not> (\<lambda>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"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "(\<lambda>x. k) -- a --NS> L \<Longrightarrow> 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])
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "\<lbrakk>f -- a --NS> L; f -- a --NS> M\<rbrakk> \<Longrightarrow> L = M"
+apply (drule (1) NSLIM_diff)
+apply (auto dest!: NSLIM_const_eq)
 done
 
 lemma NSLIM_mult_zero:
diff -r 69e30a7e8880 -r 1b2acb3ccb29 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue May 22 17:56:06 2007 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Tue May 22 19:47:55 2007 +0200
@@ -160,8 +160,8 @@
 by (fold real_norm_def, rule LIM_norm_zero_iff)
 
 lemma LIM_const_not_eq:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "k \<noteq> L ==> ~ ((%x. k) -- a --> L)"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "k \<noteq> L \<Longrightarrow> \<not> (\<lambda>x. k) -- a --> L"
 apply (simp add: LIM_eq)
 apply (rule_tac x="norm (k - L)" in exI, simp, safe)
 apply (rule_tac x="a + of_real (s/2)" in exI, simp add: norm_of_real)
@@ -170,16 +170,16 @@
 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"
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "(\<lambda>x. k) -- a --> L \<Longrightarrow> k = L"
 apply (rule ccontr)
 apply (blast dest: LIM_const_not_eq)
 done
 
 lemma LIM_unique:
-  fixes a :: "'a::real_normed_div_algebra"
-  shows "[| f -- a --> L; f -- a --> M |] ==> L = M"
-apply (drule LIM_diff, assumption)
+  fixes a :: "'a::real_normed_algebra_1"
+  shows "\<lbrakk>f -- a --> L; f -- a --> M\<rbrakk> \<Longrightarrow> L = M"
+apply (drule (1) LIM_diff)
 apply (auto dest!: LIM_const_eq)
 done