diff -r 79401279ba21 -r 2d6beddb6fa6 Seq.thy
--- /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