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 "xA. ¬ 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