author huffman Mon May 14 22:32:51 2007 +0200 (2007-05-14) changeset 22974 08b0fa905ea0 parent 22973 64d300e16370 child 22975 03085c441c14
tuned proofs
```     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.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.42  apply (rule_tac x = 1 in exI)
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:
```