# HG changeset patch # User huffman # Date 1176235363 -7200 # Node ID 0e5ac9503d7e3313911466066494bb0ad0d8db26 # Parent 2b093ba973bc4ea8b63b6997fe5e661dbdc76c1a new standard proof of LIMSEQ_realpow_zero diff -r 2b093ba973bc -r 0e5ac9503d7e src/HOL/Hyperreal/SEQ.thy --- a/src/HOL/Hyperreal/SEQ.thy Tue Apr 10 22:01:19 2007 +0200 +++ b/src/HOL/Hyperreal/SEQ.thy Tue Apr 10 22:02:43 2007 +0200 @@ -1412,10 +1412,62 @@ apply (auto simp del: star_of_mult simp add: star_of_mult [symmetric]) done -text{* standard version *} +lemma LIMSEQ_inverse_realpow_zero_lemma: + fixes x :: real + assumes x: "0 \ x" + shows "real n * x + 1 \ (x + 1) ^ n" +apply (induct n) +apply simp +apply simp +apply (rule order_trans) +prefer 2 +apply (erule mult_left_mono) +apply (rule add_increasing [OF x], simp) +apply (simp add: real_of_nat_Suc) +apply (simp add: ring_distrib) +apply (simp add: mult_nonneg_nonneg x) +done + +lemma LIMSEQ_inverse_realpow_zero: + "1 < (x::real) \ (\n. inverse (x ^ n)) ----> 0" +proof (rule LIMSEQ_inverse_zero [rule_format]) + fix y :: real + assume x: "1 < x" + hence "0 < x - 1" by simp + hence "\y. \N::nat. y < real N * (x - 1)" + by (rule reals_Archimedean3) + hence "\N::nat. y < real N * (x - 1)" .. + then obtain N::nat where "y < real N * (x - 1)" .. + also have "\ \ real N * (x - 1) + 1" by simp + also have "\ \ (x - 1 + 1) ^ N" + by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp) + also have "\ = x ^ N" by simp + finally have "y < x ^ N" . + hence "\n\N. y < x ^ n" + apply clarify + apply (erule order_less_le_trans) + apply (erule power_increasing) + apply (rule order_less_imp_le [OF x]) + done + thus "\N. \n\N. y < x ^ n" .. +qed + lemma LIMSEQ_realpow_zero: - "[| 0 \ (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0" -by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff) + "\0 \ (x::real); x < 1\ \ (\n. x ^ n) ----> 0" +proof (cases) + assume "x = 0" + hence "(\n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const) + thus ?thesis by (rule LIMSEQ_imp_Suc) +next + assume "0 \ x" and "x \ 0" + hence x0: "0 < x" by simp + assume x1: "x < 1" + from x0 x1 have "1 < inverse x" + by (rule real_inverse_gt_one) + hence "(\n. inverse (inverse x ^ n)) ----> 0" + by (rule LIMSEQ_inverse_realpow_zero) + thus ?thesis by (simp add: power_inverse) +qed lemma LIMSEQ_power_zero: fixes x :: "'a::{real_normed_div_algebra,recpower}"