src/HOL/SEQ.thy
changeset 35748 5f35613d9a65
parent 35292 e4a431b6d9b7
child 36625 2ba6525f9905
     1.1 --- a/src/HOL/SEQ.thy	Fri Mar 12 12:02:22 2010 +0100
     1.2 +++ b/src/HOL/SEQ.thy	Fri Mar 12 15:35:41 2010 +0100
     1.3 @@ -981,6 +981,24 @@
     1.4      by (blast intro: eq_refl X)
     1.5  qed
     1.6  
     1.7 +lemma incseq_SucI:
     1.8 +  assumes "\<And>n. X n \<le> X (Suc n)"
     1.9 +  shows "incseq X" unfolding incseq_def
    1.10 +proof safe
    1.11 +  fix m n :: nat
    1.12 +  { fix d m :: nat
    1.13 +    have "X m \<le> X (m + d)"
    1.14 +    proof (induct d)
    1.15 +      case (Suc d)
    1.16 +      also have "X (m + d) \<le> X (m + Suc d)"
    1.17 +        using assms by simp
    1.18 +      finally show ?case .
    1.19 +    qed simp }
    1.20 +  note this[of m "n - m"]
    1.21 +  moreover assume "m \<le> n"
    1.22 +  ultimately show "X m \<le> X n" by simp
    1.23 +qed
    1.24 +
    1.25  lemma decseq_imp_monoseq:  "decseq X \<Longrightarrow> monoseq X"
    1.26    by (simp add: decseq_def monoseq_def)
    1.27