--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Seq.thy Wed Aug 29 13:09:36 2012 +0000
@@ -0,0 +1,541 @@
+(* 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
+ 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
\ No newline at end of file