(*  Title:       Infinite Sequences

    Author:      Christian Sternagel <c-sterna@jaist.ac.jp>

                 René Thiemann       <rene.thiemann@uibk.ac.at>

    Maintainer:  Christian Sternagel and René Thiemann

    License:     LGPL

*)

(*

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

terms of the GNU Lesser General Public License as published by the Free Software

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/>.

*)

header {* Infinite Sequences *}

theory Seq

imports

  Main

  "~~/src/HOL/Library/Infinite_Set"

begin

text {*Infinite sequences are represented by functions of type @{typ "nat \<Rightarrow> 'a"}.*}

type_synonym 'a seq = "nat \<Rightarrow> 'a"

subsection {*Operations on Infinite Sequences*}

text {*Adding a new element at the front.*}

abbreviation cons :: "'a \<Rightarrow> 'a seq \<Rightarrow> 'a seq" (infixr "#s" 65) where (*FIXME: find better infix symbol*)

  "x #s S \<equiv> (\<lambda>i. case i of 0 \<Rightarrow> x | Suc n \<Rightarrow> S n)"

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 \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow>'a seq \<Rightarrow> bool" where

  "chainp P S \<equiv> \<forall>i. P (S i) (S (Suc i))"

text {*Special version for relations.*}

abbreviation (input) chain :: "'a rel \<Rightarrow> 'a seq \<Rightarrow> bool" where

  "chain r S \<equiv> chainp (\<lambda>x y. (x, y) \<in> r) S"

text {*Extending a chain at the front.*}

lemma cons_chainp:

  assumes "P x (S 0)" and "chainp P S"

  shows "chainp P (x #s 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) \<in> r" and "chain r S" shows "chain r (x #s S)"

  using cons_chainp[of "\<lambda>x y. (x, y) \<in> 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)) \<in> 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) \<in> 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 \<le> 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 \<le> j" shows "(S i, S j) \<in> 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 "\<forall>i\<ge>n::nat. f i > i \<and> P (S i) (S (f i))"

  shows "chainp P (\<lambda>i. S ((f ^^ i) n))" (is "chainp P ?T")

proof

  fix i

  from assms have "(f ^^ i) n \<ge> n" by (induct i) auto

  with assms[THEN spec[of _ "(f ^^ i) n"]]

    show "P (?T i) (?T (Suc i))" by simp

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 "\<forall>i\<ge>n::nat. \<exists>j>i. P (S i) (S j)" shows "\<exists>T. chainp P T"

proof -

  from assms have "\<forall>i\<in>{i. i \<ge> n}. \<exists>j>i. P (S i) (S j)" by auto

  from bchoice[OF this]

    obtain f where seq: "\<forall>i\<ge>n. f i > i \<and> P (S i) (S (f i))" by auto

  from stepfun_imp_chainp[of n f P S, OF this] show ?thesis by fast

qed

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 \<Rightarrow> bool"

  assumes infinite: "INFM j. p j"

begin

lemma inf: "\<exists>j\<ge>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 \<and> 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 \<ge> Suc (index n) \<and> p k" by auto

  with LeastI[of "\<lambda> k. p k \<and> k > index n" k] show ?case by auto

qed

lemma index_ordered: "index n < index (Suc n)"

proof -

  from inf obtain k where "k \<ge> Suc (index n) \<and> p k" by auto

  with LeastI[of "\<lambda> k. p k \<and> 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 "\<not> p i"

proof -

  from not_less_Least[OF i2[simplified]] i1 show ?thesis by auto

qed

lemma index_ordered_le:

  assumes "i \<le> j" shows "index i \<le> 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 \<le> 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 \<ge> index l"

  shows "\<exists>i j. k = index i + j \<and> 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 \<le> j" by auto

  from index_ordered_le[OF this]

  have "index (Suc i) \<le> index j" .

  with index_ordered[of i] show ?thesis by auto

qed

lemma index_not_p_start: assumes i: "i < index 0" shows "\<not> 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 \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> (nat \<times> 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))"

lemma inf_concat_simple_add:

  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: "\<exists> 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 "\<exists> 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 \<le> k'" shows "fst (inf_concat_simple f k) \<le> 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) \<le> i" by auto

    also have "... \<le> fst (inf_concat_simple f (k + Suc l))"

      by (simp add: ckl)

    finally show ?case .

  qed simp

qed

(* inf_concat assembles infinitely many (possibly empty) words to an infinite word *)

fun inf_concat :: "(nat \<Rightarrow> nat) \<Rightarrow> nat \<Rightarrow> nat \<times> 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 \<and> 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 \<and> 0 < n f)" and j: "j = 0" by auto

    from inf[unfolded INFM_nat] obtain f where f: "i' < f \<and> 0 < n f" by auto

    have "0 < n (LEAST f. i' < f \<and> 0 < n f)"

      using LeastI[of "\<lambda> f. i' < f \<and> 0 < n f", OF f]

      by auto

    with i j show ?thesis by auto

  qed

qed

lemma inf_concat_add:

  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 \<and> 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 "\<exists>k. inf_concat n k = (i, 0)"

proof -

  {

    fix l

    have "\<forall> j. j < l \<and> 0 < n j \<longrightarrow> (\<exists> 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 "\<exists> 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 "\<exists> j'. j' < l \<and> 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 "\<not> l' < l" by auto

              thus "l \<le> 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' \<and> 0 < n i',0)" (is "_ = (?l,0)") .

            have ll: "?l = l" unfolding l

            proof (rule Least_equality)

              show "ll - ?l' < Suc ll \<and> 0 < n (Suc ll)" using nj[unfolded j l] by simp

            next

              fix l'

              assume ass: "ll - ?l' < l' \<and> 0 < n l'"

              show "Suc ll \<le> l'" 

              proof (rule ccontr)

                assume not: "\<not> ?thesis"

                hence "l' \<le> 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 "\<lambda> 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 "\<exists>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' \<le> k"

    hence "k = k' + (k - k')" by auto

    then obtain l where k: "k = k' + l" by auto

    have "i' \<le> 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' \<le> 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' \<and> 0 < n i'"

        from inf[unfolded INFM_nat] obtain k where "i'' < k \<and> 0 < n k" by auto

        from LeastI[of "\<lambda> k. i'' < k \<and> 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: "\<And> 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 = "\<lambda> i'. i < i' \<and> 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': "\<And> d'. d' < d \<Longrightarrow> 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