# 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 \<le> x"
+  shows "real n * x + 1 \<le> (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) \<Longrightarrow> (\<lambda>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 "\<forall>y. \<exists>N::nat. y < real N * (x - 1)"
+    by (rule reals_Archimedean3)
+  hence "\<exists>N::nat. y < real N * (x - 1)" ..
+  then obtain N::nat where "y < real N * (x - 1)" ..
+  also have "\<dots> \<le> real N * (x - 1) + 1" by simp
+  also have "\<dots> \<le> (x - 1 + 1) ^ N"
+    by (rule LIMSEQ_inverse_realpow_zero_lemma, cut_tac x, simp)
+  also have "\<dots> = x ^ N" by simp
+  finally have "y < x ^ N" .
+  hence "\<forall>n\<ge>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 "\<exists>N. \<forall>n\<ge>N. y < x ^ n" ..
+qed
+
 lemma LIMSEQ_realpow_zero:
-  "[| 0 \<le> (x::real); x < 1 |] ==> (%n. x ^ n) ----> 0"
-by (simp add: NSLIMSEQ_realpow_zero LIMSEQ_NSLIMSEQ_iff)
+  "\<lbrakk>0 \<le> (x::real); x < 1\<rbrakk> \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
+proof (cases)
+  assume "x = 0"
+  hence "(\<lambda>n. x ^ Suc n) ----> 0" by (simp add: LIMSEQ_const)
+  thus ?thesis by (rule LIMSEQ_imp_Suc)
+next
+  assume "0 \<le> x" and "x \<noteq> 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 "(\<lambda>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}"