equal
deleted
inserted
replaced
71 |
71 |
72 lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
72 lemma BseqI2': assumes K: "\<forall>n\<ge>N. norm (X n) \<le> K" shows "Bseq X" |
73 proof (rule BseqI') |
73 proof (rule BseqI') |
74 let ?A = "norm ` X ` {..N}" |
74 let ?A = "norm ` X ` {..N}" |
75 have 1: "finite ?A" by simp |
75 have 1: "finite ?A" by simp |
76 have 2: "?A \<noteq> {}" by auto |
|
77 fix n::nat |
76 fix n::nat |
78 show "norm (X n) \<le> max K (Max ?A)" |
77 show "norm (X n) \<le> max K (Max ?A)" |
79 proof (cases rule: linorder_le_cases) |
78 proof (cases rule: linorder_le_cases) |
80 assume "n \<ge> N" |
79 assume "n \<ge> N" |
81 hence "norm (X n) \<le> K" using K by simp |
80 hence "norm (X n) \<le> K" using K by simp |
82 thus "norm (X n) \<le> max K (Max ?A)" by simp |
81 thus "norm (X n) \<le> max K (Max ?A)" by simp |
83 next |
82 next |
84 assume "n \<le> N" |
83 assume "n \<le> N" |
85 hence "norm (X n) \<in> ?A" by simp |
84 hence "norm (X n) \<in> ?A" by simp |
86 with 1 2 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
85 with 1 have "norm (X n) \<le> Max ?A" by (rule Max_ge) |
87 thus "norm (X n) \<le> max K (Max ?A)" by simp |
86 thus "norm (X n) \<le> max K (Max ?A)" by simp |
88 qed |
87 qed |
89 qed |
88 qed |
90 |
89 |
91 lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |
90 lemma Bseq_ignore_initial_segment: "Bseq X \<Longrightarrow> Bseq (\<lambda>n. X (n + k))" |