# HG changeset patch
# User huffman
# Date 1179174771 -7200
# Node ID 08b0fa905ea0896fcbfbf4096278abf589b44bef
# Parent  64d300e16370bbf31c22c2552a47bf8fe3fe1c25
tuned proofs

diff -r 64d300e16370 -r 08b0fa905ea0 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Mon May 14 20:48:32 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon May 14 22:32:51 2007 +0200
@@ -559,27 +559,23 @@
 
 text{*An unbounded sequence's inverse tends to 0*}
 
-text{* standard proof seems easier *}
 lemma LIMSEQ_inverse_zero:
-      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
-apply (simp add: LIMSEQ_def, safe)
-apply (drule_tac x = "inverse r" in spec, safe)
-apply (rule_tac x = N in exI, safe)
-apply (drule spec, auto)
+  "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
+apply (rule LIMSEQ_I)
+apply (drule_tac x="inverse r" in spec, safe)
+apply (rule_tac x="N" in exI, safe)
+apply (drule_tac x="n" in spec, safe)
 apply (frule positive_imp_inverse_positive)
-apply (frule order_less_trans, assumption)
-apply (frule_tac a = "f n" in positive_imp_inverse_positive)
-apply (simp add: abs_if) 
-apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
-apply (auto intro: inverse_less_iff_less [THEN iffD2]
-            simp del: inverse_inverse_eq)
+apply (frule (1) less_imp_inverse_less)
+apply (subgoal_tac "0 < X n", simp)
+apply (erule (1) order_less_trans)
 done
 
 text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
 
 lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
 apply (rule LIMSEQ_inverse_zero, safe)
-apply (cut_tac x = y in reals_Archimedean2)
+apply (cut_tac x = r in reals_Archimedean2)
 apply (safe, rule_tac x = n in exI)
 apply (auto simp add: real_of_nat_Suc)
 done
@@ -1045,7 +1041,7 @@
 apply (simp add: Bseq_def)
 apply (rule_tac x = 1 in exI)
 apply (simp add: power_abs)
-apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
+apply (auto dest: power_mono)
 done
 
 lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
@@ -1115,10 +1111,11 @@
 qed
 
 lemma LIMSEQ_power_zero:
-  fixes x :: "'a::{real_normed_div_algebra,recpower}"
+  fixes x :: "'a::{real_normed_algebra_1,recpower}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
-apply (simp add: norm_power [symmetric] LIMSEQ_norm_zero)
+apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
+apply (simp add: power_abs norm_power_ineq)
 done
 
 lemma LIMSEQ_divide_realpow_zero: