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