Theory Well_Quasi_Orders.Infinite_Sequences

(*  Title:      Well-Quasi-Orders
    Author:     Christian Sternagel <c.sternagel@gmail.com>
    Maintainer: Christian Sternagel
    License:    LGPL
*)

section ‹Infinite Sequences›

text ‹Some useful constructions on and facts about infinite sequences.›

theory Infinite_Sequences
imports Main
begin

text ‹The set of all infinite sequences over elements from @{term A}.›
definition "SEQ A = {f::nat ⇒ 'a. ∀i. f i ∈ A}"

lemma SEQ_iff [iff]:
  "f ∈ SEQ A ⟷ (∀i. f i ∈ A)"
by (auto simp: SEQ_def)


text ‹The ‹i›-th "column" of a set ‹B› of infinite sequences.›
definition "ith B i = {f i | f. f ∈ B}"

lemma ithI [intro]:
  "f ∈ B ⟹ f i = x ⟹ x ∈ ith B i"
by (auto simp: ith_def)

lemma ithE [elim]:
  "⟦x ∈ ith B i; ⋀f. ⟦f ∈ B; f i = x⟧ ⟹ Q⟧ ⟹ Q"
by (auto simp: ith_def)

lemma ith_conv:
  "x ∈ ith B i ⟷ (∃f ∈ B. x = f i)"
by auto

text ‹
  The restriction of a set ‹B› of sequences to sequences that are equal to a given sequence
  ‹f› up to position ‹i›.
›
definition eq_upto :: "(nat ⇒ 'a) set ⇒ (nat ⇒ 'a) ⇒ nat ⇒ (nat ⇒ 'a) set"
where
  "eq_upto B f i = {g ∈ B. ∀j < i. f j = g j}"

lemma eq_uptoI [intro]:
  "⟦g ∈ B; ⋀j. j < i ⟹ f j = g j⟧ ⟹ g ∈ eq_upto B f i"
by (auto simp: eq_upto_def)

lemma eq_uptoE [elim]:
  "⟦g ∈ eq_upto B f i; ⟦g ∈ B; ⋀j. j < i ⟹ f j = g j⟧ ⟹ Q⟧ ⟹ Q"
by (auto simp: eq_upto_def)

lemma eq_upto_Suc:
  "⟦g ∈ eq_upto B f i; g i = f i⟧ ⟹ g ∈ eq_upto B f (Suc i)"
by (auto simp: eq_upto_def less_Suc_eq)

lemma eq_upto_0 [simp]:
  "eq_upto B f 0 = B"
by (auto simp: eq_upto_def)

lemma eq_upto_cong [fundef_cong]:
  assumes "⋀j. j < i ⟹ f j = g j" and "B = C"
  shows "eq_upto B f i = eq_upto C g i"
using assms by (auto simp: eq_upto_def)


subsection ‹Lexicographic Order on Infinite Sequences›

definition "LEX P f g ⟷ (∃i::nat. P (f i) (g i) ∧ (∀j<i. f j = g j))"
abbreviation "LEXEQ P ≡ (LEX P)⇧=⇧="

lemma LEX_imp_not_LEX:
  assumes "LEX P f g"
    and [dest]: "⋀x y z. P x y ⟹ P y z ⟹ P x z"
    and [simp]: "⋀x. ¬ P x x"
  shows "¬ LEX P g f"
proof -
  { fix i j :: nat
    assume "P (f i) (g i)" and "∀k<i. f k = g k"
      and "P (g j) (f j)" and "∀k<j. g k = f k"
    then have False by (cases "i < j") (auto simp: not_less dest!: le_imp_less_or_eq) }
  then show "¬ LEX P g f" using ‹LEX P f g› unfolding LEX_def by blast
qed

lemma LEX_cases:
  assumes "LEX P f g"
  obtains (eq) "f = g" | (neq) k where "∀i<k. f i = g i" and "P (f k) (g k)"
using assms by (auto simp: LEX_def)

lemma LEX_imp_less:
  assumes "∀x∈A. ¬ P x x" and "f ∈ SEQ A ∨ g ∈ SEQ A"
    and "LEX P f g" and "∀i<k. f i = g i" and "f k ≠ g k"
  shows "P (f k) (g k)"
using assms by (auto elim!: LEX_cases) (metis linorder_neqE_nat)+

end