tuned proofs
authorhuffman
Mon May 14 22:32:51 2007 +0200 (2007-05-14)
changeset 2297408b0fa905ea0
parent 22973 64d300e16370
child 22975 03085c441c14
tuned proofs
src/HOL/Hyperreal/SEQ.thy
     1.1 --- a/src/HOL/Hyperreal/SEQ.thy	Mon May 14 20:48:32 2007 +0200
     1.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Mon May 14 22:32:51 2007 +0200
     1.3 @@ -559,27 +559,23 @@
     1.4  
     1.5  text{*An unbounded sequence's inverse tends to 0*}
     1.6  
     1.7 -text{* standard proof seems easier *}
     1.8  lemma LIMSEQ_inverse_zero:
     1.9 -      "\<forall>y::real. \<exists>N. \<forall>n \<ge> N. y < f(n) ==> (%n. inverse(f n)) ----> 0"
    1.10 -apply (simp add: LIMSEQ_def, safe)
    1.11 -apply (drule_tac x = "inverse r" in spec, safe)
    1.12 -apply (rule_tac x = N in exI, safe)
    1.13 -apply (drule spec, auto)
    1.14 +  "\<forall>r::real. \<exists>N. \<forall>n\<ge>N. r < X n \<Longrightarrow> (\<lambda>n. inverse (X n)) ----> 0"
    1.15 +apply (rule LIMSEQ_I)
    1.16 +apply (drule_tac x="inverse r" in spec, safe)
    1.17 +apply (rule_tac x="N" in exI, safe)
    1.18 +apply (drule_tac x="n" in spec, safe)
    1.19  apply (frule positive_imp_inverse_positive)
    1.20 -apply (frule order_less_trans, assumption)
    1.21 -apply (frule_tac a = "f n" in positive_imp_inverse_positive)
    1.22 -apply (simp add: abs_if) 
    1.23 -apply (rule_tac t = r in inverse_inverse_eq [THEN subst])
    1.24 -apply (auto intro: inverse_less_iff_less [THEN iffD2]
    1.25 -            simp del: inverse_inverse_eq)
    1.26 +apply (frule (1) less_imp_inverse_less)
    1.27 +apply (subgoal_tac "0 < X n", simp)
    1.28 +apply (erule (1) order_less_trans)
    1.29  done
    1.30  
    1.31  text{*The sequence @{term "1/n"} tends to 0 as @{term n} tends to infinity*}
    1.32  
    1.33  lemma LIMSEQ_inverse_real_of_nat: "(%n. inverse(real(Suc n))) ----> 0"
    1.34  apply (rule LIMSEQ_inverse_zero, safe)
    1.35 -apply (cut_tac x = y in reals_Archimedean2)
    1.36 +apply (cut_tac x = r in reals_Archimedean2)
    1.37  apply (safe, rule_tac x = n in exI)
    1.38  apply (auto simp add: real_of_nat_Suc)
    1.39  done
    1.40 @@ -1045,7 +1041,7 @@
    1.41  apply (simp add: Bseq_def)
    1.42  apply (rule_tac x = 1 in exI)
    1.43  apply (simp add: power_abs)
    1.44 -apply (auto dest: power_mono intro: order_less_imp_le simp add: abs_if)
    1.45 +apply (auto dest: power_mono)
    1.46  done
    1.47  
    1.48  lemma monoseq_realpow: "[| 0 \<le> x; x \<le> 1 |] ==> monoseq (%n. x ^ n)"
    1.49 @@ -1115,10 +1111,11 @@
    1.50  qed
    1.51  
    1.52  lemma LIMSEQ_power_zero:
    1.53 -  fixes x :: "'a::{real_normed_div_algebra,recpower}"
    1.54 +  fixes x :: "'a::{real_normed_algebra_1,recpower}"
    1.55    shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
    1.56  apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
    1.57 -apply (simp add: norm_power [symmetric] LIMSEQ_norm_zero)
    1.58 +apply (simp only: LIMSEQ_Zseq_iff, erule Zseq_le)
    1.59 +apply (simp add: power_abs norm_power_ineq)
    1.60  done
    1.61  
    1.62  lemma LIMSEQ_divide_realpow_zero: