# Theory Abstract-Rewriting.Seq

(*  Title:       Infinite Sequences
Author:      Christian Sternagel <c-sterna@jaist.ac.jp>
René Thiemann       <rene.thiemann@uibk.ac.at>
Maintainer:  Christian Sternagel and René Thiemann
*)

(*
Copyright 2012 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)
section ‹Infinite Sequences›
theory Seq
imports
Main
"HOL-Library.Infinite_Set"
begin

text ‹Infinite sequences are represented by functions of type @{typ "nat ⇒ 'a"}.›
type_synonym 'a seq = "nat ⇒ 'a"

subsection ‹Operations on Infinite Sequences›

text ‹An infinite sequence is \emph{linked} by a binary predicate @{term P} if every two
consecutive elements satisfy it. Such a sequence is called a \emph{@{term P}-chain}.›
abbreviation (input) chainp :: "('a ⇒ 'a ⇒ bool) ⇒'a seq ⇒ bool" where
"chainp P S ≡ ∀i. P (S i) (S (Suc i))"

text ‹Special version for relations.›
abbreviation (input) chain :: "'a rel ⇒ 'a seq ⇒ bool" where
"chain r S ≡ chainp (λx y. (x, y) ∈ r) S"

text ‹Extending a chain at the front.›
lemma cons_chainp:
assumes "P x (S 0)" and "chainp P S"
shows "chainp P (case_nat x S)" (is "chainp P ?S")
proof
fix i show "P (?S i) (?S (Suc i))" using assms by (cases i) simp_all
qed

text ‹Special version for relations.›
lemma cons_chain:
assumes "(x, S 0) ∈ r" and "chain r S" shows "chain r (case_nat x S)"
using cons_chainp[of "λx y. (x, y) ∈ r", OF assms] .

text ‹A chain admits arbitrary transitive steps.›
lemma chainp_imp_relpowp:
assumes "chainp P S" shows "(P^^j) (S i) (S (i + j))"
proof (induct "i + j" arbitrary: j)
case (Suc n) thus ?case using assms by (cases j) auto
qed simp

lemma chain_imp_relpow:
assumes "chain r S" shows "(S i, S (i + j)) ∈ r^^j"
proof (induct "i + j" arbitrary: j)
case (Suc n) thus ?case using assms by (cases j) auto
qed simp

lemma chainp_imp_tranclp:
assumes "chainp P S" and "i < j" shows "P^++ (S i) (S j)"
proof -
from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto
with chainp_imp_relpowp[of P S "Suc n" i, OF assms(1)]
show ?thesis
unfolding trancl_power[of "(S i, S j)", to_pred]
by force
qed

lemma chain_imp_trancl:
assumes "chain r S" and "i < j" shows "(S i, S j) ∈ r^+"
proof -
from less_imp_Suc_add[OF assms(2)] obtain n where "j = i + Suc n" by auto
with chain_imp_relpow[OF assms(1), of i "Suc n"]
show ?thesis unfolding trancl_power by force
qed

text ‹A chain admits arbitrary reflexive and transitive steps.›
lemma chainp_imp_rtranclp:
assumes "chainp P S" and "i ≤ j" shows "P^** (S i) (S j)"
proof -
from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+
with chainp_imp_relpowp[of P S, OF assms(1), of n i] show ?thesis
by (simp add: relpow_imp_rtrancl[of "(S i, S (i + n))", to_pred])
qed

lemma chain_imp_rtrancl:
assumes "chain r S" and "i ≤ j" shows "(S i, S j) ∈ r^*"
proof -
from assms(2) obtain n where "j = i + n" by (induct "j - i" arbitrary: j) force+
with chain_imp_relpow[OF assms(1), of i n] show ?thesis by (simp add: relpow_imp_rtrancl)
qed

text ‹If for every @{term i} there is a later index @{term "f i"} such that the
corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.›
lemma stepfun_imp_chainp':
assumes "∀i≥n::nat. f i ≥ i ∧ P (S i) (S (f i))"
shows "chainp P (λi. S ((f ^^ i) n))" (is "chainp P ?T")
proof
fix i
from assms have "(f ^^ i) n ≥ n" by (induct i) auto
with assms[THEN spec[of _ "(f ^^ i) n"]]
show "P (?T i) (?T (Suc i))" by simp
qed

lemma stepfun_imp_chainp:
assumes "∀i≥n::nat. f i > i ∧ P (S i) (S (f i))"
shows "chainp P (λi. S ((f ^^ i) n))" (is "chainp P ?T")
using stepfun_imp_chainp'[of n f P S] and assms by force

lemma subchain:
assumes "∀i::nat>n. ∃j>i. P (f i) (f j)"
shows "∃φ. (∀i j. i < j ⟶ φ i < φ j) ∧ (∀i. P (f (φ i)) (f (φ (Suc i))))"
proof -
from assms have "∀i∈{i. i > n}. ∃j>i. P (f i) (f j)" by simp
from bchoice [OF this] obtain g
where *: "∀i>n. g i > i"
and **: "∀i>n. P (f i) (f (g i))" by auto
define φ where [simp]: "φ i = (g ^^ i) (Suc n)" for i
from * have ***: "⋀i. φ i > n" by (induct_tac i) auto
then have "⋀i. φ i < φ (Suc i)" using * by (induct_tac i) auto
then have "⋀i j. i < j ⟹ φ i < φ j" by (rule lift_Suc_mono_less)
moreover have "⋀i. P (f (φ i)) (f (φ (Suc i)))" using ** and *** by simp
ultimately show ?thesis by blast
qed

text ‹If for every @{term i} there is a later index @{term j} such that the
corresponding elements satisfy the predicate @{term P}, then there is a @{term P}-chain.›
lemma steps_imp_chainp':
assumes "∀i≥n::nat. ∃j≥i. P (S i) (S j)" shows "∃T. chainp P T"
proof -
from assms have "∀i∈{i. i ≥ n}. ∃j≥i. P (S i) (S j)" by auto
from bchoice [OF this] (*choice could be replaced by an application of Least_Enum.infinitely_many2*)
obtain f where "∀i≥n. f i ≥ i ∧ P (S i) (S (f i))" by auto
from stepfun_imp_chainp'[of n f P S, OF this] show ?thesis by fast
qed

lemma steps_imp_chainp:
assumes "∀i≥n::nat. ∃j>i. P (S i) (S j)" shows "∃T. chainp P T"
using steps_imp_chainp' [of n P S] and assms by force

subsection ‹Predicates on Natural Numbers›

text ‹If some property holds for infinitely many natural numbers, obtain
an index function that points to these numbers in increasing order.›

locale infinitely_many =
fixes p :: "nat ⇒ bool"
assumes infinite: "INFM j. p j"
begin

lemma inf: "∃j≥i. p j" using infinite[unfolded INFM_nat_le] by auto

fun index :: "nat seq" where
"index 0 = (LEAST n. p n)"
| "index (Suc n) = (LEAST k. p k ∧ k > index n)"

lemma index_p: "p (index n)"
proof (induct n)
case 0
from inf obtain j where "p j" by auto
with LeastI[of p j] show ?case by auto
next
case (Suc n)
from inf obtain k where "k ≥ Suc (index n) ∧ p k" by auto
with LeastI[of "λ k. p k ∧ k > index n" k] show ?case by auto
qed

lemma index_ordered: "index n < index (Suc n)"
proof -
from inf obtain k where "k ≥ Suc (index n) ∧ p k" by auto
with LeastI[of "λ k. p k ∧ k > index n" k] show ?thesis by auto
qed

lemma index_not_p_between:
assumes i1: "index n < i"
and i2: "i < index (Suc n)"
shows "¬ p i"
proof -
from not_less_Least[OF i2[simplified]] i1 show ?thesis by auto
qed

lemma index_ordered_le:
assumes "i ≤ j" shows "index i ≤ index j"
proof -
from assms have "j = i + (j - i)" by auto
then obtain k where j: "j = i + k" by auto
have "index i ≤ index (i + k)"
proof (induct k)
case (Suc k)
with index_ordered[of "i + k"]
show ?case by auto
qed simp
thus ?thesis unfolding j .
qed

lemma index_surj:
assumes "k ≥ index l"
shows "∃i j. k = index i + j ∧ index i + j < index (Suc i)"
proof -
from assms have "k = index l + (k - index l)" by auto
then obtain u where k: "k = index l + u" by auto
show ?thesis unfolding k
proof (induct u)
case 0
show ?case
by (intro exI conjI, rule refl, insert index_ordered[of l], simp)
next
case (Suc u)
then obtain i j
where lu: "index l + u = index i + j" and lt: "index i + j < index (Suc i)" by auto
hence "index l + u < index (Suc i)" by auto
show ?case
proof (cases "index l + (Suc u) = index (Suc i)")
case False
show ?thesis
by (rule exI[of _ i], rule exI[of _ "Suc j"], insert lu lt False, auto)
next
case True
show ?thesis
by (rule exI[of _ "Suc i"], rule exI[of _ 0], insert True index_ordered[of "Suc i"], auto)
qed
qed
qed

lemma index_ordered_less:
assumes "i < j" shows "index i < index j"
proof -
from assms have "Suc i ≤ j" by auto
from index_ordered_le[OF this]
have "index (Suc i) ≤ index j" .
with index_ordered[of i] show ?thesis by auto
qed

lemma index_not_p_start: assumes i: "i < index 0" shows "¬ p i"
proof -
from i[simplified index.simps] have "i < Least p" .
from not_less_Least[OF this] show ?thesis .
qed

end

subsection ‹Assembling Infinite Words from Finite Words›

text ‹Concatenate infinitely many non-empty words to an infinite word.›

fun inf_concat_simple :: "(nat ⇒ nat) ⇒ nat ⇒ (nat × nat)" where
"inf_concat_simple f 0 = (0, 0)"
| "inf_concat_simple f (Suc n) = (
let (i, j) = inf_concat_simple f n in
if Suc j < f i then (i, Suc j)
else (Suc i, 0))"

assumes ck: "inf_concat_simple f k = (i, j)"
and jl: "j + l < f i"
shows "inf_concat_simple f (k + l) = (i,j + l)"
using jl
proof (induct l)
case 0
thus ?case using ck by simp
next
case (Suc l)
hence c: "inf_concat_simple f (k + l) = (i, j+ l)" by auto
show ?case
by (simp add: c, insert Suc(2), auto)
qed

lemma inf_concat_simple_surj_zero: "∃ k. inf_concat_simple f k = (i,0)"
proof (induct i)
case 0
show ?case
by (rule exI[of _ 0], simp)
next
case (Suc i)
then obtain k where ck: "inf_concat_simple f k = (i,0)" by auto
show ?case
proof (cases "f i")
case 0
show ?thesis
by (rule exI[of _ "Suc k"], simp add: ck 0)
next
case (Suc n)
hence "0 + n < f i" by auto
from inf_concat_simple_add[OF ck, OF this] Suc
show ?thesis
by (intro exI[of _ "k + Suc n"], auto)
qed
qed

lemma inf_concat_simple_surj:
assumes "j < f i"
shows "∃ k. inf_concat_simple f k = (i,j)"
proof -
from assms have j: "0 + j < f i" by auto
from inf_concat_simple_surj_zero obtain k where "inf_concat_simple f k = (i,0)" by auto
from inf_concat_simple_add[OF this, OF j] show ?thesis by auto
qed

lemma inf_concat_simple_mono:
assumes "k ≤ k'" shows "fst (inf_concat_simple f k) ≤ fst (inf_concat_simple f k')"
proof -
from assms have "k' = k + (k' - k)" by auto
then obtain l where k': "k' = k + l" by auto
show ?thesis  unfolding k'
proof (induct l)
case (Suc l)
obtain i j where ckl: "inf_concat_simple f (k+l) = (i,j)" by (cases "inf_concat_simple f (k+l)", auto)
with Suc have "fst (inf_concat_simple f k) ≤ i" by auto
also have "... ≤ fst (inf_concat_simple f (k + Suc l))"
finally show ?case .
qed simp
qed

(* inf_concat assembles infinitely many (possibly empty) words to an infinite word *)
fun inf_concat :: "(nat ⇒ nat) ⇒ nat ⇒ nat × nat" where
"inf_concat n 0 = (LEAST j. n j > 0, 0)"
| "inf_concat n (Suc k) = (let (i, j) = inf_concat n k in (if Suc j < n i then (i, Suc j) else (LEAST i'. i' > i ∧ n i' > 0, 0)))"

lemma inf_concat_bounds:
assumes inf: "INFM i. n i > 0"
and res: "inf_concat n k = (i,j)"
shows "j < n i"
proof (cases k)
case 0
with res have i: "i = (LEAST i. n i > 0)" and j: "j = 0" by auto
from inf[unfolded INFM_nat_le] obtain i' where i': "0 < n i'" by auto
have "0 < n (LEAST i. n i > 0)"
by (rule LeastI, rule i')
with i j show ?thesis by auto
next
case (Suc k')
obtain i' j' where res': "inf_concat n k' = (i',j')" by force
note res = res[unfolded Suc inf_concat.simps res' Let_def split]
show ?thesis
proof (cases "Suc j' < n i'")
case True
with res show ?thesis by auto
next
case False
with res have i: "i = (LEAST f. i' < f ∧ 0 < n f)" and j: "j = 0" by auto
from inf[unfolded INFM_nat] obtain f where f: "i' < f ∧ 0 < n f" by auto
have "0 < n (LEAST f. i' < f ∧ 0 < n f)"
using LeastI[of "λ f. i' < f ∧ 0 < n f", OF f]
by auto
with i j show ?thesis by auto
qed
qed

assumes res: "inf_concat n k = (i,j)"
and j: "j + m < n i"
shows "inf_concat n (k + m) = (i,j+m)"
using j
proof (induct m)
case 0 show ?case using res by auto
next
case (Suc m)
hence "inf_concat n (k + m) = (i, j+m)" by auto
with Suc(2)
show ?case by auto
qed

lemma inf_concat_step:
assumes res: "inf_concat n k = (i,j)"
and j: "Suc (j + m) = n i"
shows "inf_concat n (k + Suc m) = (LEAST i'. i' > i ∧ 0 < n i', 0)"
proof -
from j have "j + m < n i" by auto
note res = inf_concat_add[OF res, OF this]
show ?thesis by (simp add: res j)
qed

lemma inf_concat_surj_zero:
assumes "0 < n i"
shows "∃k. inf_concat n k = (i, 0)"
proof -
{
fix l
have "∀ j. j < l ∧ 0 < n j ⟶ (∃ k. inf_concat n k = (j,0))"
proof (induct l)
case 0
thus ?case by auto
next
case (Suc l)
show ?case
proof (intro allI impI, elim conjE)
fix j
assume j: "j < Suc l" and nj: "0 < n j"
show "∃ k. inf_concat n k = (j, 0)"
proof (cases "j < l")
case True
from Suc[THEN spec[of _ j]] True nj show ?thesis by auto
next
case False
with j have j: "j = l" by auto
show ?thesis
proof (cases "∃ j'. j' < l ∧ 0 < n j'")
case False
have l: "(LEAST i. 0 < n i) = l"
proof (rule Least_equality, rule nj[unfolded j])
fix l'
assume "0 < n l'"
with False have "¬ l' < l" by auto
thus "l ≤ l'" by auto
qed
show ?thesis
by (rule exI[of _ 0], simp add: l j)
next
case True
then obtain lll where lll: "lll < l" and nlll: "0 < n lll" by auto
then obtain ll where l: "l = Suc ll" by (cases l, auto)
from lll l have lll: "lll = ll - (ll - lll)" by auto
let ?l' = "LEAST d. 0 < n (ll - d)"
have nl': "0 < n (ll - ?l')"
proof (rule LeastI)
show "0 < n (ll - (ll - lll))" using lll nlll by auto
qed
with Suc[THEN spec[of _ "ll - ?l'"]] obtain k where k:
"inf_concat n k = (ll - ?l',0)" unfolding l by auto
from nl' obtain off where off: "Suc (0 + off) = n (ll - ?l')" by (cases "n (ll - ?l')", auto)
from inf_concat_step[OF k, OF off]
have id: "inf_concat n (k + Suc off) = (LEAST i'. ll - ?l' < i' ∧ 0 < n i',0)" (is "_ = (?l,0)") .
have ll: "?l = l" unfolding l
proof (rule Least_equality)
show "ll - ?l' < Suc ll ∧ 0 < n (Suc ll)" using nj[unfolded j l] by simp
next
fix l'
assume ass: "ll - ?l' < l' ∧ 0 < n l'"
show "Suc ll ≤ l'"
proof (rule ccontr)
assume not: "¬ ?thesis"
hence "l' ≤ ll" by auto
hence "ll = l' + (ll - l')" by auto
then obtain k where ll: "ll = l' + k" by auto
from ass have "l' + k - ?l' < l'" unfolding ll by auto
hence kl': "k < ?l'" by auto
have "0 < n (ll - k)" using ass unfolding ll by simp
from Least_le[of "λ k. 0 < n (ll - k)", OF this] kl'
show False by auto
qed
qed
show ?thesis unfolding j
by (rule exI[of _ "k + Suc off"], unfold id ll, simp)
qed
qed
qed
qed
}
with assms show ?thesis by auto
qed

lemma inf_concat_surj:
assumes j: "j < n i"
shows "∃k. inf_concat n k = (i, j)"
proof -
from j have "0 < n i" by auto
from inf_concat_surj_zero[of n, OF this]
obtain k where "inf_concat n k = (i,0)" by auto
from inf_concat_add[OF this, of j] j
show ?thesis by auto
qed

lemma inf_concat_mono:
assumes inf: "INFM i. n i > 0"
and resk: "inf_concat n k = (i, j)"
and reskp: "inf_concat n k' = (i', j')"
and lt: "i < i'"
shows "k < k'"
proof -
note bounds = inf_concat_bounds[OF inf]
{
assume "k' ≤ k"
hence "k = k' + (k - k')" by auto
then obtain l where k: "k = k' + l" by auto
have "i' ≤ fst (inf_concat n (k' + l))"
proof (induct l)
case 0
with reskp show ?case by auto
next
case (Suc l)
obtain i'' j'' where l: "inf_concat n (k' + l) = (i'',j'')" by force
with Suc have one: "i' ≤ i''" by auto
from bounds[OF l] have j'': "j'' < n i''" by auto
show ?case
proof (cases "Suc j'' < n i''")
case True
show ?thesis by (simp add: l True one)
next
case False
let ?i = "LEAST i'. i'' < i' ∧ 0 < n i'"
from inf[unfolded INFM_nat] obtain k where "i'' < k ∧ 0 < n k" by auto
from LeastI[of "λ k. i'' < k ∧ 0 < n k", OF this]
have "i'' < ?i" by auto
with one show ?thesis by (simp add: l False)
qed
qed
with resk k lt have False by auto
}
thus ?thesis by arith
qed

lemma inf_concat_Suc:
assumes inf: "INFM i. n i > 0"
and f: "⋀ i. f i (n i) = f (Suc i) 0"
and resk: "inf_concat n k = (i, j)"
and ressk: "inf_concat n (Suc k) = (i', j')"
shows "f i' j' = f i (Suc j)"
proof -
note bounds = inf_concat_bounds[OF inf]
from bounds[OF resk] have j: "j < n i" .
show ?thesis
proof (cases "Suc j < n i")
case True
with ressk resk
show ?thesis by simp
next
case False
let ?p = "λ i'. i < i' ∧ 0 < n i'"
let ?i' = "LEAST i'. ?p i'"
from False j have id: "Suc (j + 0) = n i" by auto
from inf_concat_step[OF resk, OF id] ressk
have i': "i' = ?i'" and j': "j' = 0" by auto
from id have j: "Suc j = n i" by simp
from inf[unfolded INFM_nat] obtain k where "?p k" by auto
from LeastI[of ?p, OF this] have "?p ?i'" .
hence "?i' = Suc i + (?i' - Suc i)" by simp
then obtain d where ii': "?i' = Suc i + d" by auto
from not_less_Least[of _ ?p, unfolded ii'] have d': "⋀ d'. d' < d ⟹ n (Suc i + d') = 0" by auto
have "f (Suc i) 0 = f ?i' 0" unfolding ii' using d'
proof (induct d)
case 0
show ?case by simp
next
case (Suc d)
hence "f (Suc i) 0 = f (Suc i + d) 0" by auto
also have "... = f (Suc (Suc i + d)) 0"
unfolding f[symmetric]
using Suc(2)[of d] by simp
finally show ?case by simp
qed
thus ?thesis unfolding i' j' j f by simp
qed
qed

end