# HG changeset patch
# User huffman
# Date 1176087088 -7200
# Node ID d650e51b5970e7ccb3f7b48cb3e9ac41946fff25
# Parent  17644bc9cee41455670842533aaa48a924ea402f
new standard proofs of some LIMSEQ lemmas

diff -r 17644bc9cee4 -r d650e51b5970 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sun Apr 08 18:35:19 2007 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Apr 09 04:51:28 2007 +0200
@@ -349,29 +349,35 @@
 apply (erule order_le_less_trans [OF norm_triangle_ineq3])
 done
 
-lemma LIMSEQ_ignore_initial_segment: "f ----> a 
-  ==> (%n. f(n + k)) ----> a"
-  apply (unfold LIMSEQ_def) 
-  apply (clarify)
-  apply (drule_tac x = r in spec)
-  apply (clarify)
-  apply (rule_tac x = "no + k" in exI)
-  by auto
+lemma LIMSEQ_ignore_initial_segment:
+  "f ----> a \<Longrightarrow> (\<lambda>n. f (n + k)) ----> a"
+apply (rule LIMSEQ_I)
+apply (drule (1) LIMSEQ_D)
+apply (erule exE, rename_tac N)
+apply (rule_tac x=N in exI)
+apply simp
+done
 
-lemma LIMSEQ_offset: "(%x. f (x + k)) ----> a ==>
-    f ----> a"
-  apply (unfold LIMSEQ_def)
-  apply clarsimp
-  apply (drule_tac x = r in spec)
-  apply clarsimp
-  apply (rule_tac x = "no + k" in exI)
-  apply clarsimp
-  apply (drule_tac x = "n - k" in spec)
-  apply (frule mp)
-  apply arith
-  apply simp
+lemma LIMSEQ_offset:
+  "(\<lambda>n. f (n + k)) ----> a \<Longrightarrow> f ----> a"
+apply (rule LIMSEQ_I)
+apply (drule (1) LIMSEQ_D)
+apply (erule exE, rename_tac N)
+apply (rule_tac x="N + k" in exI)
+apply clarify
+apply (drule_tac x="n - k" in spec)
+apply (simp add: le_diff_conv2)
 done
 
+lemma LIMSEQ_Suc: "f ----> l \<Longrightarrow> (\<lambda>n. f (Suc n)) ----> l"
+by (drule_tac k="1" in LIMSEQ_ignore_initial_segment, simp)
+
+lemma LIMSEQ_imp_Suc: "(\<lambda>n. f (Suc n)) ----> l \<Longrightarrow> f ----> l"
+by (rule_tac k="1" in LIMSEQ_offset, simp)
+
+lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
+by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+
 lemma add_diff_add:
   fixes a b c d :: "'a::ab_group_add"
   shows "(a + c) - (b + d) = (a - b) + (c - d)"
@@ -622,6 +628,32 @@
 by (cut_tac b=1 in
         LIMSEQ_mult [OF LIMSEQ_const LIMSEQ_inverse_real_of_nat_add_minus], auto)
 
+lemma LIMSEQ_le_const:
+  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. a \<le> X n\<rbrakk> \<Longrightarrow> a \<le> x"
+apply (rule ccontr, simp only: linorder_not_le)
+apply (drule_tac r="a - x" in LIMSEQ_D, simp)
+apply clarsimp
+apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI1)
+apply (drule_tac x="max N no" in spec, drule mp, rule le_maxI2)
+apply simp
+done
+
+lemma LIMSEQ_le_const2:
+  "\<lbrakk>X ----> (x::real); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
+apply (subgoal_tac "- a \<le> - x", simp)
+apply (rule LIMSEQ_le_const)
+apply (erule LIMSEQ_minus)
+apply simp
+done
+
+lemma LIMSEQ_le:
+  "\<lbrakk>X ----> x; Y ----> y; \<exists>N. \<forall>n\<ge>N. X n \<le> Y n\<rbrakk> \<Longrightarrow> x \<le> (y::real)"
+apply (subgoal_tac "0 \<le> y - x", simp)
+apply (rule LIMSEQ_le_const)
+apply (erule (1) LIMSEQ_diff)
+apply (simp add: le_diff_eq)
+done
+
 subsubsection {* Purely nonstandard proofs *}
 
 lemma NSLIMSEQ_iff:
@@ -791,29 +823,7 @@
      "!!(f::nat=>nat). \<forall>n. n \<le> f n ==> finite {n. f n \<le> u}"
 by (rule_tac B="{..u}" in finite_subset, auto intro: order_trans)
 
-subsubsection {* Derived theorems about @{term LIMSEQ} *}
-
-lemma LIMSEQ_le:
-     "[| f ----> l; g ----> m; \<exists>N. \<forall>n \<ge> N. f(n) \<le> g(n) |]
-      ==> l \<le> (m::real)"
-by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_le)
-
-lemma LIMSEQ_le_const: "[| X ----> (r::real); \<forall>n. a \<le> X n |] ==> a \<le> r"
-by (erule LIMSEQ_le [OF LIMSEQ_const], auto)
-
-lemma LIMSEQ_le_const2: "[| X ----> (r::real); \<forall>n. X n \<le> a |] ==> r \<le> a"
-by (erule LIMSEQ_le [OF _ LIMSEQ_const], auto)
-
-lemma LIMSEQ_Suc: "f ----> l ==> (%n. f(Suc n)) ----> l"
-by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_Suc)
-
-lemma LIMSEQ_imp_Suc: "(%n. f(Suc n)) ----> l ==> f ----> l"
-apply (simp add: LIMSEQ_NSLIMSEQ_iff)
-apply (erule NSLIMSEQ_imp_Suc)
-done
-
-lemma LIMSEQ_Suc_iff: "((%n. f(Suc n)) ----> l) = (f ----> l)"
-by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+subsubsection {* Derived theorems about @{term NSLIMSEQ} *}
 
 text{*We prove the NS version from the standard one, since the NS proof
    seems more complicated than the standard one above!*}