author huffman Wed, 23 Aug 2006 22:44:32 +0200 changeset 20409 eba80f91e3fc parent 20408 f6ccfc09694a child 20410 4bd5cd97c547
speed up some proofs
 src/HOL/Hyperreal/Lim.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/Lim.thy	Wed Aug 23 22:12:54 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 23 22:44:32 2006 +0200
@@ -93,9 +93,9 @@
assumes f: "f -- a --> L" and g: "g -- a --> M"
shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (simp add: LIM_eq, clarify)
+proof (unfold LIM_eq, clarify)
fix r :: real
-  assume r: "0<r"
+  assume r: "0 < r"
from LIM_D [OF f half_gt_zero [OF r]]
obtain fs
where fs:    "0 < fs"
@@ -111,8 +111,9 @@
show "0 < min fs gs"  by (simp add: fs gs)
fix x :: real
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
+    hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
with fs_lt gs_lt
-    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by (auto simp add: fs_lt)
+    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by blast+
hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
thus "\<bar>f x + g x - (L + M)\<bar> < r"
by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
@@ -194,8 +195,9 @@
show "0 < min fs gs"  by (simp add: fs gs)
fix x :: real
assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
+    hence  "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
with fs_lt gs_lt
-    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
+    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by blast+
hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
qed```