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.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.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)"
```