# Theory 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