author huffman Wed, 23 Aug 2006 21:57:43 +0200 changeset 20407 93a34d5d1dc5 parent 20406 f0a5421efb0b child 20408 f6ccfc09694a
speed up some proofs
 src/HOL/Hyperreal/NSA.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Hyperreal/NSA.thy	Wed Aug 23 17:05:08 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Aug 23 21:57:43 2006 +0200
@@ -285,6 +285,10 @@

subsection{* Set of Infinitesimals is a Subring of the Hyperreals*}

+lemma InfinitesimalI:
+  "(\<And>r. \<lbrakk>r \<in> \<real>; 0 < r\<rbrakk> \<Longrightarrow> \<bar>x\<bar> < r) \<Longrightarrow> x \<in> Infinitesimal"
+
lemma InfinitesimalD:
"x \<in> Infinitesimal ==> \<forall>r \<in> Reals. 0 < r --> abs x < r"
@@ -297,10 +301,10 @@

"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x+y) \<in> Infinitesimal"
+apply (rule InfinitesimalI)
apply (rule hypreal_sum_of_halves [THEN subst])
apply (drule half_gt_zero)
+apply (blast intro: hrabs_add_less SReal_divide_number_of dest: InfinitesimalD)
done

lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
@@ -312,20 +316,25 @@

lemma Infinitesimal_mult:
"[| x \<in> Infinitesimal; y \<in> Infinitesimal |] ==> (x * y) \<in> Infinitesimal"
-apply (auto simp add: Infinitesimal_def abs_mult)
-apply (case_tac "y=0", simp)
-apply (cut_tac a = "abs x" and b = 1 and c = "abs y" and d = r
-       in mult_strict_mono, auto)
+apply (rule InfinitesimalI)
+apply (simp only: abs_mult)
+apply (case_tac "y = 0", simp)
+apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < 1 * r", simp only: mult_1)
+apply (rule mult_strict_mono)
done

lemma Infinitesimal_HFinite_mult:
"[| x \<in> Infinitesimal; y \<in> HFinite |] ==> (x * y) \<in> Infinitesimal"
-apply (auto dest!: HFiniteD simp add: Infinitesimal_def abs_mult)
-apply (frule hrabs_less_gt_zero)
-apply (drule_tac x = "r/t" in bspec)
-apply (blast intro: SReal_divide)
-apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
+apply (rule InfinitesimalI)
+apply (drule HFiniteD, clarify)
+apply (simp only: abs_mult)
+apply (subgoal_tac "\<bar>x\<bar> * \<bar>y\<bar> < (r / t) * t", simp)
+apply (subgoal_tac "0 < r / t")
+apply (rule mult_strict_mono)
+apply (assumption, assumption, simp)
+apply (simp only: divide_pos_pos hrabs_less_gt_zero)
done

lemma Infinitesimal_HFinite_mult2:
@@ -343,13 +352,18 @@
done

+lemma HInfiniteI: "(\<And>r. r \<in> \<real> \<Longrightarrow> r < \<bar>x\<bar>) \<Longrightarrow> x \<in> HInfinite"
+
+lemma HInfiniteD: "\<lbrakk>x \<in> HInfinite; r \<in> \<real>\<rbrakk> \<Longrightarrow> r < \<bar>x\<bar>"
+
lemma HInfinite_mult: "[|x \<in> HInfinite;y \<in> HInfinite|] ==> (x*y) \<in> HInfinite"
-apply (auto simp add: HInfinite_def  abs_mult)
-apply (erule_tac x = 1 in ballE)
-apply (erule_tac x = r in ballE)
-apply (case_tac "y=0", simp)
-apply (cut_tac c = 1 and d = "abs x" and a = r and b = "abs y" in mult_strict_mono)
+apply (rule HInfiniteI, simp only: abs_mult)
+apply (subgoal_tac "r * 1 < \<bar>x\<bar> * \<bar>y\<bar>", simp only: mult_1)
+apply (case_tac "x = 0", simp add: HInfinite_def)
+apply (rule mult_strict_mono)
done

lemma hypreal_add_zero_less_le_mono: "[|r < x; (0::hypreal) \<le> y|] ==> r < x+y"
@@ -421,12 +435,13 @@

lemma not_Infinitesimal_mult:
"[| x \<notin> Infinitesimal;  y \<notin> Infinitesimal|] ==> (x*y) \<notin>Infinitesimal"
-apply (unfold Infinitesimal_def, clarify)
-apply (erule_tac x = "r*ra" in ballE)
-prefer 2 apply (fast intro: SReal_mult)