4 Description : Convergence of sequences and series |
4 Description : Convergence of sequences and series |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
6 *) |
6 *) |
7 |
7 |
8 theory SEQ |
8 theory SEQ |
9 imports NatStar HyperPow |
9 imports NatStar |
10 begin |
10 begin |
11 |
11 |
12 constdefs |
12 constdefs |
13 |
13 |
14 LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60) |
14 LIMSEQ :: "[nat=>real,real] => bool" ("((_)/ ----> (_))" [60, 60] 60) |
737 text{* FIXME: Long. Maximal element in subsequence *} |
737 text{* FIXME: Long. Maximal element in subsequence *} |
738 lemma SUP_rabs_subseq: |
738 lemma SUP_rabs_subseq: |
739 "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)" |
739 "\<exists>m. m \<le> M & (\<forall>n. n \<le> M --> \<bar>(X::nat=> real) n\<bar> \<le> \<bar>X m\<bar>)" |
740 apply (induct M) |
740 apply (induct M) |
741 apply (rule_tac x = 0 in exI, simp, safe) |
741 apply (rule_tac x = 0 in exI, simp, safe) |
742 apply (cut_tac x = "\<bar>X (Suc n)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear) |
742 apply (cut_tac x = "\<bar>X (Suc M)\<bar>" and y = "\<bar>X m\<bar> " in linorder_less_linear) |
743 apply safe |
743 apply safe |
744 apply (rule_tac x = m in exI) |
744 apply (rule_tac x = m in exI) |
745 apply (rule_tac [2] x = m in exI) |
745 apply (rule_tac [2] x = m in exI) |
746 apply (rule_tac [3] x = "Suc n" in exI, simp_all, safe) |
746 apply (rule_tac [3] x = "Suc M" in exI, simp_all, safe) |
747 apply (erule_tac [!] m1 = na in le_imp_less_or_eq [THEN disjE]) |
747 apply (erule_tac [!] m1 = n in le_imp_less_or_eq [THEN disjE]) |
748 apply (simp_all add: less_Suc_cancel_iff) |
748 apply (simp_all add: less_Suc_cancel_iff) |
749 apply (blast intro: order_le_less_trans [THEN order_less_imp_le]) |
749 apply (blast intro: order_le_less_trans [THEN order_less_imp_le]) |
750 done |
750 done |
751 |
751 |
752 lemma lemma_Nat_covered: |
752 lemma lemma_Nat_covered: |