Theory First_Order_Terms.Seq_More

(*
Author:  Christian Sternagel <c.sternagel@gmail.com>
Author:  René Thiemann <rene.thiemann@uibk.ac.at>
License: LGPL
*)
subsection ‹Results on Infinite Sequences›

(* TODO: Move to Abstract-Rewriting.Seq -- maybe this is of very general interest... *)
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