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