src/HOL/SEQ.thy
changeset 29803 c56a5571f60a
parent 29667 53103fc8ffa3
child 30082 43c5b7bfc791
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/SEQ.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/SEQ.thy	Thu Feb 05 11:34:42 2009 +0100
     1.3 @@ -346,6 +346,11 @@
     1.4  lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) ----> l = f ----> l"
     1.5  by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
     1.6  
     1.7 +lemma LIMSEQ_linear: "\<lbrakk> X ----> x ; l > 0 \<rbrakk> \<Longrightarrow> (\<lambda> n. X (n * l)) ----> x"
     1.8 +  unfolding LIMSEQ_def
     1.9 +  by (metis div_le_dividend div_mult_self1_is_m le_trans nat_mult_commute)
    1.10 +
    1.11 +
    1.12  lemma add_diff_add:
    1.13    fixes a b c d :: "'a::ab_group_add"
    1.14    shows "(a + c) - (b + d) = (a - b) + (c - d)"
    1.15 @@ -678,6 +683,69 @@
    1.16  lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
    1.17  by (simp add: monoseq_Suc)
    1.18  
    1.19 +lemma monoseq_minus: assumes "monoseq a"
    1.20 +  shows "monoseq (\<lambda> n. - a n)"
    1.21 +proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
    1.22 +  case True
    1.23 +  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
    1.24 +  thus ?thesis by (rule monoI2)
    1.25 +next
    1.26 +  case False
    1.27 +  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
    1.28 +  thus ?thesis by (rule monoI1)
    1.29 +qed
    1.30 +
    1.31 +lemma monoseq_le: assumes "monoseq a" and "a ----> x"
    1.32 +  shows "((\<forall> n. a n \<le> x) \<and> (\<forall>m. \<forall>n\<ge>m. a m \<le> a n)) \<or> 
    1.33 +         ((\<forall> n. x \<le> a n) \<and> (\<forall>m. \<forall>n\<ge>m. a n \<le> a m))"
    1.34 +proof -
    1.35 +  { fix x n fix a :: "nat \<Rightarrow> real"
    1.36 +    assume "a ----> x" and "\<forall> m. \<forall> n \<ge> m. a m \<le> a n"
    1.37 +    hence monotone: "\<And> m n. m \<le> n \<Longrightarrow> a m \<le> a n" by auto
    1.38 +    have "a n \<le> x"
    1.39 +    proof (rule ccontr)
    1.40 +      assume "\<not> a n \<le> x" hence "x < a n" by auto
    1.41 +      hence "0 < a n - x" by auto
    1.42 +      from `a ----> x`[THEN LIMSEQ_D, OF this]
    1.43 +      obtain no where "\<And>n'. no \<le> n' \<Longrightarrow> norm (a n' - x) < a n - x" by blast
    1.44 +      hence "norm (a (max no n) - x) < a n - x" by auto
    1.45 +      moreover
    1.46 +      { fix n' have "n \<le> n' \<Longrightarrow> x < a n'" using monotone[where m=n and n=n'] and `x < a n` by auto }
    1.47 +      hence "x < a (max no n)" by auto
    1.48 +      ultimately
    1.49 +      have "a (max no n) < a n" by auto
    1.50 +      with monotone[where m=n and n="max no n"]
    1.51 +      show False by auto
    1.52 +    qed
    1.53 +  } note top_down = this
    1.54 +  { fix x n m fix a :: "nat \<Rightarrow> real"
    1.55 +    assume "a ----> x" and "monoseq a" and "a m < x"
    1.56 +    have "a n \<le> x \<and> (\<forall> m. \<forall> n \<ge> m. a m \<le> a n)"
    1.57 +    proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
    1.58 +      case True with top_down and `a ----> x` show ?thesis by auto
    1.59 +    next
    1.60 +      case False with `monoseq a`[unfolded monoseq_def] have "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" by auto
    1.61 +      hence "- a m \<le> - x" using top_down[OF LIMSEQ_minus[OF `a ----> x`]] by blast
    1.62 +      hence False using `a m < x` by auto
    1.63 +      thus ?thesis ..
    1.64 +    qed
    1.65 +  } note when_decided = this
    1.66 +
    1.67 +  show ?thesis
    1.68 +  proof (cases "\<exists> m. a m \<noteq> x")
    1.69 +    case True then obtain m where "a m \<noteq> x" by auto
    1.70 +    show ?thesis
    1.71 +    proof (cases "a m < x")
    1.72 +      case True with when_decided[OF `a ----> x` `monoseq a`, where m2=m]
    1.73 +      show ?thesis by blast
    1.74 +    next
    1.75 +      case False hence "- a m < - x" using `a m \<noteq> x` by auto
    1.76 +      with when_decided[OF LIMSEQ_minus[OF `a ----> x`] monoseq_minus[OF `monoseq a`], where m2=m]
    1.77 +      show ?thesis by auto
    1.78 +    qed
    1.79 +  qed auto
    1.80 +qed
    1.81 +
    1.82  text{*Bounded Sequence*}
    1.83  
    1.84  lemma BseqD: "Bseq X ==> \<exists>K. 0 < K & (\<forall>n. norm (X n) \<le> K)"