--- a/src/HOL/Hyperreal/Lim.thy Sat Sep 30 17:36:55 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy Sat Sep 30 18:04:28 2006 +0200
@@ -240,6 +240,15 @@
==> (%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)"
@@ -383,6 +392,11 @@
==> (%x. f(x) * g(x)) -- x --> (l * m)"
by (simp add: LIM_NSLIM_iff NSLIM_mult)
+lemma LIM_scaleR:
+ "[| f -- x --> l; g -- x --> m |]
+ ==> (%x. f(x) *# g(x)) -- x --> (l *# m)"
+by (simp add: LIM_NSLIM_iff NSLIM_scaleR)
+
lemma LIM_add2:
"[| f -- x --> l; g -- x --> m |] ==> (%x. f(x) + g(x)) -- x --> (l + m)"
by (simp add: LIM_NSLIM_iff NSLIM_add)