(* 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/>. *) 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))" 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: "∃ 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))" 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 ⇒ 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 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 ∧ 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