Theory Seq_More
subsection ‹Results on Infinite Sequences›
theory Seq_More
imports
"Abstract-Rewriting.Seq"
Transitive_Closure_More
begin
lemma down_chain_imp_eq:
fixes f :: "nat seq"
assumes "∀i. f i ≥ f (Suc i)"
shows "∃N. ∀i > N. f i = f (Suc i)"
proof -
let ?F = "{f i | i. True}"
from wf_less [unfolded wf_eq_minimal, THEN spec, of ?F]
obtain x where "x ∈ ?F" and *: "∀y. y < x ⟶ y ∉ ?F" by auto
obtain N where "f N = x" using ‹x ∈ ?F› by auto
moreover have "∀i > N. f i ∈ ?F" by auto
ultimately have "∀i > N. ¬ f i < x" using * by auto
moreover have "∀i > N. f N ≥ f i"
using chainp_imp_rtranclp [of "(≥)" f, OF assms] by simp
ultimately have "∀i > N. f i = f (Suc i)"
using ‹f N = x› by (auto) (metis less_SucI order.not_eq_order_implies_strict)
then show ?thesis ..
qed
lemma inc_seq_greater:
fixes f :: "nat seq"
assumes "∀i. f i < f (Suc i)"
shows "∃i. f i > N"
using assms
apply (induct N)
apply (auto)
apply (metis neq0_conv)
by (metis Suc_lessI)
end