# HG changeset patch
# User hoelzl
# Date 1300109857 -3600
# Node ID 8885ba6296927d1a947db67792439abe58172a35
# Parent  a54e8e95fe962311c31b22ab26a8d802681562a0
add lemmas for monotone sequences

diff -r a54e8e95fe96 -r 8885ba629692 src/HOL/SEQ.thy
--- a/src/HOL/SEQ.thy	Mon Mar 14 14:37:36 2011 +0100
+++ b/src/HOL/SEQ.thy	Mon Mar 14 14:37:37 2011 +0100
@@ -13,25 +13,7 @@
 imports Limits RComplete
 begin
 
-abbreviation
-  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
-    ("((_)/ ----> (_))" [60, 60] 60) where
-  "X ----> L \<equiv> (X ---> L) sequentially"
-
-definition
-  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
-    --{*Standard definition of limit using choice operator*}
-  "lim X = (THE L. X ----> L)"
-
-definition
-  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
-    --{*Standard definition of convergence*}
-  "convergent X = (\<exists>L. X ----> L)"
-
-definition
-  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
-    --{*Standard definition for bounded sequence*}
-  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+subsection {* Monotone sequences and subsequences *}
 
 definition
   monoseq :: "(nat \<Rightarrow> 'a::order) \<Rightarrow> bool" where
@@ -56,6 +38,171 @@
     --{*Definition of subsequence*}
   "subseq f \<longleftrightarrow> (\<forall>m. \<forall>n>m. f m < f n)"
 
+lemma incseq_mono: "mono f \<longleftrightarrow> incseq f"
+  unfolding mono_def incseq_def by auto
+
+lemma incseq_SucI:
+  "(\<And>n. X n \<le> X (Suc n)) \<Longrightarrow> incseq X"
+  using lift_Suc_mono_le[of X]
+  by (auto simp: incseq_def)
+
+lemma incseqD: "\<And>i j. incseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f i \<le> f j"
+  by (auto simp: incseq_def)
+
+lemma incseq_SucD: "incseq A \<Longrightarrow> A i \<le> A (Suc i)"
+  using incseqD[of A i "Suc i"] by auto
+
+lemma incseq_Suc_iff: "incseq f \<longleftrightarrow> (\<forall>n. f n \<le> f (Suc n))"
+  by (auto intro: incseq_SucI dest: incseq_SucD)
+
+lemma incseq_const[simp, intro]: "incseq (\<lambda>x. k)"
+  unfolding incseq_def by auto
+
+lemma decseq_SucI:
+  "(\<And>n. X (Suc n) \<le> X n) \<Longrightarrow> decseq X"
+  using order.lift_Suc_mono_le[OF dual_order, of X]
+  by (auto simp: decseq_def)
+
+lemma decseqD: "\<And>i j. decseq f \<Longrightarrow> i \<le> j \<Longrightarrow> f j \<le> f i"
+  by (auto simp: decseq_def)
+
+lemma decseq_SucD: "decseq A \<Longrightarrow> A (Suc i) \<le> A i"
+  using decseqD[of A i "Suc i"] by auto
+
+lemma decseq_Suc_iff: "decseq f \<longleftrightarrow> (\<forall>n. f (Suc n) \<le> f n)"
+  by (auto intro: decseq_SucI dest: decseq_SucD)
+
+lemma decseq_const[simp, intro]: "decseq (\<lambda>x. k)"
+  unfolding decseq_def by auto
+
+lemma monoseq_iff: "monoseq X \<longleftrightarrow> incseq X \<or> decseq X"
+  unfolding monoseq_def incseq_def decseq_def ..
+
+lemma monoseq_Suc:
+  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
+  unfolding monoseq_iff incseq_Suc_iff decseq_Suc_iff ..
+
+lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
+by (simp add: monoseq_def)
+
+lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
+by (simp add: monoseq_def)
+
+lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
+by (simp add: monoseq_Suc)
+
+lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
+by (simp add: monoseq_Suc)
+
+lemma monoseq_minus:
+  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
+  assumes "monoseq a"
+  shows "monoseq (\<lambda> n. - a n)"
+proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
+  case True
+  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
+  thus ?thesis by (rule monoI2)
+next
+  case False
+  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
+  thus ?thesis by (rule monoI1)
+qed
+
+text{*Subsequence (alternative definition, (e.g. Hoskins)*}
+
+lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
+apply (simp add: subseq_def)
+apply (auto dest!: less_imp_Suc_add)
+apply (induct_tac k)
+apply (auto intro: less_trans)
+done
+
+text{* for any sequence, there is a monotonic subsequence *}
+lemma seq_monosub:
+  fixes s :: "nat => 'a::linorder"
+  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
+proof cases
+  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
+  assume *: "\<forall>n. \<exists>p. ?P p n"
+  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
+  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
+  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
+  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
+  then have "subseq f" unfolding subseq_Suc_iff by auto
+  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
+  proof (intro disjI2 allI)
+    fix n show "s (f (Suc n)) \<le> s (f n)"
+    proof (cases n)
+      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
+    next
+      case (Suc m)
+      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
+      with P_Suc Suc show ?thesis by simp
+    qed
+  qed
+  ultimately show ?thesis by auto
+next
+  let "?P p m" = "m < p \<and> s m < s p"
+  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
+  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
+  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
+  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
+  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
+  have P_0: "?P (f 0) (Suc N)"
+    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
+  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
+      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
+  note P' = this
+  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
+      by (induct i) (insert P_0 P', auto) }
+  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
+    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
+  then show ?thesis by auto
+qed
+
+lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
+proof(induct n)
+  case 0 thus ?case by simp
+next
+  case (Suc n)
+  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
+  have "n < f (Suc n)" by arith
+  thus ?case by arith
+qed
+
+lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
+  by (simp add: incseq_def monoseq_def)
+
+lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
+  by (simp add: decseq_def monoseq_def)
+
+lemma decseq_eq_incseq:
+  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
+  by (simp add: decseq_def incseq_def)
+
+subsection {* Defintions of limits *}
+
+abbreviation
+  LIMSEQ :: "[nat \<Rightarrow> 'a::topological_space, 'a] \<Rightarrow> bool"
+    ("((_)/ ----> (_))" [60, 60] 60) where
+  "X ----> L \<equiv> (X ---> L) sequentially"
+
+definition
+  lim :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> 'a" where
+    --{*Standard definition of limit using choice operator*}
+  "lim X = (THE L. X ----> L)"
+
+definition
+  convergent :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
+    --{*Standard definition of convergence*}
+  "convergent X = (\<exists>L. X ----> L)"
+
+definition
+  Bseq :: "(nat => 'a::real_normed_vector) => bool" where
+    --{*Standard definition for bounded sequence*}
+  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+
 definition
   Cauchy :: "(nat \<Rightarrow> 'a::metric_space) \<Rightarrow> bool" where
     --{*Standard definition of the Cauchy condition*}
@@ -502,53 +649,6 @@
     qed
 qed
 
-text{*Subsequence (alternative definition, (e.g. Hoskins)*}
-
-lemma subseq_Suc_iff: "subseq f = (\<forall>n. (f n) < (f (Suc n)))"
-apply (simp add: subseq_def)
-apply (auto dest!: less_imp_Suc_add)
-apply (induct_tac k)
-apply (auto intro: less_trans)
-done
-
-lemma monoseq_Suc:
-  "monoseq X \<longleftrightarrow> (\<forall>n. X n \<le> X (Suc n)) \<or> (\<forall>n. X (Suc n) \<le> X n)"
-apply (simp add: monoseq_def)
-apply (auto dest!: le_imp_less_or_eq)
-apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
-apply (induct_tac "ka")
-apply (auto intro: order_trans)
-apply (erule contrapos_np)
-apply (induct_tac "k")
-apply (auto intro: order_trans)
-done
-
-lemma monoI1: "\<forall>m. \<forall> n \<ge> m. X m \<le> X n ==> monoseq X"
-by (simp add: monoseq_def)
-
-lemma monoI2: "\<forall>m. \<forall> n \<ge> m. X n \<le> X m ==> monoseq X"
-by (simp add: monoseq_def)
-
-lemma mono_SucI1: "\<forall>n. X n \<le> X (Suc n) ==> monoseq X"
-by (simp add: monoseq_Suc)
-
-lemma mono_SucI2: "\<forall>n. X (Suc n) \<le> X n ==> monoseq X"
-by (simp add: monoseq_Suc)
-
-lemma monoseq_minus:
-  fixes a :: "nat \<Rightarrow> 'a::ordered_ab_group_add"
-  assumes "monoseq a"
-  shows "monoseq (\<lambda> n. - a n)"
-proof (cases "\<forall> m. \<forall> n \<ge> m. a m \<le> a n")
-  case True
-  hence "\<forall> m. \<forall> n \<ge> m. - a n \<le> - a m" by auto
-  thus ?thesis by (rule monoI2)
-next
-  case False
-  hence "\<forall> m. \<forall> n \<ge> m. - a m \<le> - a n" using `monoseq a`[unfolded monoseq_def] by auto
-  thus ?thesis by (rule monoI1)
-qed
-
 lemma monoseq_le:
   fixes a :: "nat \<Rightarrow> real"
   assumes "monoseq a" and "a ----> x"
@@ -602,60 +702,6 @@
   qed auto
 qed
 
-text{* for any sequence, there is a monotonic subsequence *}
-lemma seq_monosub:
-  fixes s :: "nat => 'a::linorder"
-  shows "\<exists>f. subseq f \<and> monoseq (\<lambda> n. (s (f n)))"
-proof cases
-  let "?P p n" = "p > n \<and> (\<forall>m\<ge>p. s m \<le> s p)"
-  assume *: "\<forall>n. \<exists>p. ?P p n"
-  def f \<equiv> "nat_rec (SOME p. ?P p 0) (\<lambda>_ n. SOME p. ?P p n)"
-  have f_0: "f 0 = (SOME p. ?P p 0)" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
-  have P_0: "?P (f 0) 0" unfolding f_0 using *[rule_format] by (rule someI2_ex) auto
-  have P_Suc: "\<And>i. ?P (f (Suc i)) (f i)" unfolding f_Suc using *[rule_format] by (rule someI2_ex) auto
-  then have "subseq f" unfolding subseq_Suc_iff by auto
-  moreover have "monoseq (\<lambda>n. s (f n))" unfolding monoseq_Suc
-  proof (intro disjI2 allI)
-    fix n show "s (f (Suc n)) \<le> s (f n)"
-    proof (cases n)
-      case 0 with P_Suc[of 0] P_0 show ?thesis by auto
-    next
-      case (Suc m)
-      from P_Suc[of n] Suc have "f (Suc m) \<le> f (Suc (Suc m))" by simp
-      with P_Suc Suc show ?thesis by simp
-    qed
-  qed
-  ultimately show ?thesis by auto
-next
-  let "?P p m" = "m < p \<and> s m < s p"
-  assume "\<not> (\<forall>n. \<exists>p>n. (\<forall>m\<ge>p. s m \<le> s p))"
-  then obtain N where N: "\<And>p. p > N \<Longrightarrow> \<exists>m>p. s p < s m" by (force simp: not_le le_less)
-  def f \<equiv> "nat_rec (SOME p. ?P p (Suc N)) (\<lambda>_ n. SOME p. ?P p n)"
-  have f_0: "f 0 = (SOME p. ?P p (Suc N))" unfolding f_def by simp
-  have f_Suc: "\<And>i. f (Suc i) = (SOME p. ?P p (f i))" unfolding f_def nat_rec_Suc ..
-  have P_0: "?P (f 0) (Suc N)"
-    unfolding f_0 some_eq_ex[of "\<lambda>p. ?P p (Suc N)"] using N[of "Suc N"] by auto
-  { fix i have "N < f i \<Longrightarrow> ?P (f (Suc i)) (f i)"
-      unfolding f_Suc some_eq_ex[of "\<lambda>p. ?P p (f i)"] using N[of "f i"] . }
-  note P' = this
-  { fix i have "N < f i \<and> ?P (f (Suc i)) (f i)"
-      by (induct i) (insert P_0 P', auto) }
-  then have "subseq f" "monoseq (\<lambda>x. s (f x))"
-    unfolding subseq_Suc_iff monoseq_Suc by (auto simp: not_le intro: less_imp_le)
-  then show ?thesis by auto
-qed
-
-lemma seq_suble: assumes sf: "subseq f" shows "n \<le> f n"
-proof(induct n)
-  case 0 thus ?case by simp
-next
-  case (Suc n)
-  from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
-  have "n < f (Suc n)" by arith
-  thus ?case by arith
-qed
-
 lemma LIMSEQ_subseq_LIMSEQ:
   "\<lbrakk> X ----> L; subseq f \<rbrakk> \<Longrightarrow> (X o f) ----> L"
 apply (rule topological_tendstoI)
@@ -810,9 +856,6 @@
 
 subsubsection{*Increasing and Decreasing Series*}
 
-lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
-  by (simp add: incseq_def monoseq_def)
-
 lemma incseq_le:
   fixes X :: "nat \<Rightarrow> real"
   assumes inc: "incseq X" and lim: "X ----> L" shows "X n \<le> L"
@@ -834,32 +877,6 @@
     by (blast intro: eq_refl X)
 qed
 
-lemma incseq_SucI:
-  assumes "\<And>n. X n \<le> X (Suc n)"
-  shows "incseq X" unfolding incseq_def
-proof safe
-  fix m n :: nat
-  { fix d m :: nat
-    have "X m \<le> X (m + d)"
-    proof (induct d)
-      case (Suc d)
-      also have "X (m + d) \<le> X (m + Suc d)"
-        using assms by simp
-      finally show ?case .
-    qed simp }
-  note this[of m "n - m"]
-  moreover assume "m \<le> n"
-  ultimately show "X m \<le> X n" by simp
-qed
-
-lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
-  by (simp add: decseq_def monoseq_def)
-
-lemma decseq_eq_incseq:
-  fixes X :: "nat \<Rightarrow> 'a::ordered_ab_group_add" shows "decseq X = incseq (\<lambda>n. - X n)" 
-  by (simp add: decseq_def incseq_def)
-
-
 lemma decseq_le:
   fixes X :: "nat \<Rightarrow> real" assumes dec: "decseq X" and lim: "X ----> L" shows "L \<le> X n"
 proof -