src/HOL/Library/Omega_Words_Fun.thy
author paulson <lp15@cam.ac.uk>
Wed Sep 12 12:51:43 2018 +0100 (13 months ago)
changeset 68977 c73ca43087c0
parent 67443 3abf6a722518
child 69597 ff784d5a5bfb
permissions -rw-r--r--
tiny cleanup
     1 (*
     2     Author:     Stefan Merz
     3     Author:     Salomon Sickert
     4     Author:     Julian Brunner
     5     Author:     Peter Lammich
     6 *)
     7 
     8 section \<open>$\omega$-words\<close>
     9 
    10 theory Omega_Words_Fun
    11 
    12 imports Infinite_Set
    13 begin
    14 
    15 text \<open>Note: This theory is based on Stefan Merz's work.\<close>
    16 
    17 text \<open>
    18   Automata recognize languages, which are sets of words. For the
    19   theory of $\omega$-automata, we are mostly interested in
    20   $\omega$-words, but it is sometimes useful to reason about
    21   finite words, too. We are modeling finite words as lists; this
    22   lets us benefit from the existing library. Other formalizations
    23   could be investigated, such as representing words as functions
    24   whose domains are initial intervals of the natural numbers.
    25 \<close>
    26 
    27 
    28 subsection \<open>Type declaration and elementary operations\<close>
    29 
    30 text \<open>
    31   We represent $\omega$-words as functions from the natural numbers
    32   to the alphabet type. Other possible formalizations include
    33   a coinductive definition or a uniform encoding of finite and
    34   infinite words, as studied by M\"uller et al.
    35 \<close>
    36 
    37 type_synonym
    38   'a word = "nat \<Rightarrow> 'a"
    39 
    40 text \<open>
    41   We can prefix a finite word to an $\omega$-word, and a way
    42   to obtain an $\omega$-word from a finite, non-empty word is by
    43   $\omega$-iteration.
    44 \<close>
    45 
    46 definition
    47   conc :: "['a list, 'a word] \<Rightarrow> 'a word"  (infixr "\<frown>" 65)
    48   where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
    49 
    50 definition
    51   iter :: "'a list \<Rightarrow> 'a word"  ("(_\<^sup>\<omega>)" [1000])
    52   where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
    53 
    54 lemma conc_empty[simp]: "[] \<frown> w = w"
    55   unfolding conc_def by auto
    56 
    57 lemma conc_fst[simp]: "n < length w \<Longrightarrow> (w \<frown> x) n = w!n"
    58   by (simp add: conc_def)
    59 
    60 lemma conc_snd[simp]: "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n - length w)"
    61   by (simp add: conc_def)
    62 
    63 lemma iter_nth [simp]: "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))"
    64   by (simp add: iter_def)
    65 
    66 lemma conc_conc[simp]: "u \<frown> v \<frown> w = (u @ v) \<frown> w" (is "?lhs = ?rhs")
    67 proof
    68   fix n
    69   have u: "n < length u \<Longrightarrow> ?lhs n = ?rhs n"
    70     by (simp add: conc_def nth_append)
    71   have v: "\<lbrakk> \<not>(n < length u); n < length u + length v \<rbrakk> \<Longrightarrow> ?lhs n = ?rhs n"
    72     by (simp add: conc_def nth_append, arith)
    73   have w: "\<not>(n < length u + length v) \<Longrightarrow> ?lhs n = ?rhs n"
    74     by (simp add: conc_def nth_append, arith)
    75   from u v w show "?lhs n = ?rhs n" by blast
    76 qed
    77 
    78 lemma range_conc[simp]: "range (w\<^sub>1 \<frown> w\<^sub>2) = set w\<^sub>1 \<union> range w\<^sub>2"
    79 proof (intro equalityI subsetI)
    80   fix a
    81   assume "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)"
    82   then obtain i where 1: "a = (w\<^sub>1 \<frown> w\<^sub>2) i" by auto
    83   then show "a \<in> set w\<^sub>1 \<union> range w\<^sub>2"
    84     unfolding 1 by (cases "i < length w\<^sub>1") simp_all
    85 next
    86   fix a
    87   assume a: "a \<in> set w\<^sub>1 \<union> range w\<^sub>2"
    88   then show "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)"
    89   proof
    90     assume "a \<in> set w\<^sub>1"
    91     then obtain i where 1: "i < length w\<^sub>1" "a = w\<^sub>1 ! i"
    92       using in_set_conv_nth by metis
    93     show ?thesis
    94     proof
    95       show "a = (w\<^sub>1 \<frown> w\<^sub>2) i" using 1 by auto
    96       show "i \<in> UNIV" by rule
    97     qed
    98   next
    99     assume "a \<in> range w\<^sub>2"
   100     then obtain i where 1: "a = w\<^sub>2 i" by auto
   101     show ?thesis
   102     proof
   103       show "a = (w\<^sub>1 \<frown> w\<^sub>2) (length w\<^sub>1 + i)" using 1 by simp
   104       show "length w\<^sub>1 + i \<in> UNIV" by rule
   105     qed
   106   qed
   107 qed
   108 
   109 
   110 lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
   111   by (rule ext) (simp add: conc_def mod_geq)
   112 
   113 
   114 subsection \<open>Subsequence, Prefix, and Suffix\<close>
   115 
   116 definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
   117   where "suffix k x \<equiv> \<lambda>n. x (k+n)"
   118 
   119 definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"  ("_ [_ \<rightarrow> _]" 900)
   120   where "subsequence w i j \<equiv> map w [i..<j]"
   121 
   122 abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
   123   where "prefix n w \<equiv> subsequence w 0 n"
   124 
   125 lemma suffix_nth [simp]: "(suffix k x) n = x (k+n)"
   126   by (simp add: suffix_def)
   127 
   128 lemma suffix_0 [simp]: "suffix 0 x = x"
   129   by (simp add: suffix_def)
   130 
   131 lemma suffix_suffix [simp]: "suffix m (suffix k x) = suffix (k+m) x"
   132   by (rule ext) (simp add: suffix_def add.assoc)
   133 
   134 lemma subsequence_append: "prefix (i + j) w = prefix i w @ (w [i \<rightarrow> i + j])"
   135   unfolding map_append[symmetric] upt_add_eq_append[OF le0] subsequence_def ..
   136 
   137 lemma subsequence_drop[simp]: "drop i (w [j \<rightarrow> k]) = w [j + i \<rightarrow> k]"
   138   by (simp add: subsequence_def drop_map)
   139 
   140 lemma subsequence_empty[simp]: "w [i \<rightarrow> j] = [] \<longleftrightarrow> j \<le> i"
   141   by (auto simp add: subsequence_def)
   142 
   143 lemma subsequence_length[simp]: "length (subsequence w i j) = j - i"
   144   by (simp add: subsequence_def)
   145 
   146 lemma subsequence_nth[simp]: "k < j - i \<Longrightarrow> (w [i \<rightarrow> j]) ! k = w (i + k)"
   147   unfolding subsequence_def
   148   by auto
   149 
   150 lemma subseq_to_zero[simp]: "w[i\<rightarrow>0] = []"
   151   by simp
   152 
   153 lemma subseq_to_smaller[simp]: "i\<ge>j \<Longrightarrow> w[i\<rightarrow>j] = []"
   154   by simp
   155 
   156 lemma subseq_to_Suc[simp]: "i\<le>j \<Longrightarrow> w [i \<rightarrow> Suc j] = w [ i \<rightarrow> j ] @ [w j]"
   157   by (auto simp: subsequence_def)
   158 
   159 lemma subsequence_singleton[simp]: "w [i \<rightarrow> Suc i] = [w i]"
   160   by (auto simp: subsequence_def)
   161 
   162 
   163 lemma subsequence_prefix_suffix: "prefix (j - i) (suffix i w) = w [i \<rightarrow> j]"
   164 proof (cases "i \<le> j")
   165   case True
   166   have "w [i \<rightarrow> j] = map w (map (\<lambda>n. n + i) [0..<j - i])"
   167     unfolding map_add_upt subsequence_def
   168     using le_add_diff_inverse2[OF True] by force
   169   also
   170   have "\<dots> = map (\<lambda>n. w (n + i)) [0..<j - i]"
   171     unfolding map_map comp_def by blast
   172   finally
   173   show ?thesis
   174     unfolding subsequence_def suffix_def add.commute[of i] by simp
   175 next
   176   case False
   177   then show ?thesis
   178     by (simp add: subsequence_def)
   179 qed
   180 
   181 lemma prefix_suffix: "x = prefix n x \<frown> (suffix n x)"
   182   by (rule ext) (simp add: subsequence_def conc_def)
   183 
   184 declare prefix_suffix[symmetric, simp]
   185 
   186 
   187 lemma word_split: obtains v\<^sub>1 v\<^sub>2 where "v = v\<^sub>1 \<frown> v\<^sub>2" "length v\<^sub>1 = k"
   188 proof
   189   show "v = prefix k v \<frown> suffix k v"
   190     by (rule prefix_suffix)
   191   show "length (prefix k v) = k"
   192     by simp
   193 qed
   194 
   195 
   196 lemma set_subsequence[simp]: "set (w[i\<rightarrow>j]) = w`{i..<j}"
   197   unfolding subsequence_def by auto
   198 
   199 lemma subsequence_take[simp]: "take i (w [j \<rightarrow> k]) = w [j \<rightarrow> min (j + i) k]"
   200   by (simp add: subsequence_def take_map min_def)
   201 
   202 lemma subsequence_shift[simp]: "(suffix i w) [j \<rightarrow> k] = w [i + j \<rightarrow> i + k]"
   203   by (metis add_diff_cancel_left subsequence_prefix_suffix suffix_suffix)
   204 
   205 lemma suffix_subseq_join[simp]: "i \<le> j \<Longrightarrow> v [i \<rightarrow> j] \<frown> suffix j v = suffix i v"
   206   by (metis (no_types, lifting) Nat.add_0_right le_add_diff_inverse prefix_suffix
   207     subsequence_shift suffix_suffix)
   208 
   209 lemma prefix_conc_fst[simp]:
   210   assumes "j \<le> length w"
   211   shows "prefix j (w \<frown> w') = take j w"
   212 proof -
   213   have "\<forall>i < j. (prefix j (w \<frown> w')) ! i = (take j w) ! i"
   214     using assms by (simp add: conc_fst subsequence_def)
   215   thus ?thesis
   216     by (simp add: assms list_eq_iff_nth_eq min.absorb2)
   217 qed
   218 
   219 lemma prefix_conc_snd[simp]:
   220   assumes "n \<ge> length u"
   221   shows "prefix n (u \<frown> v) = u @ prefix (n - length u) v"
   222 proof (intro nth_equalityI)
   223   show "length (prefix n (u \<frown> v)) = length (u @ prefix (n - length u) v)"
   224     using assms by simp
   225   fix i
   226   assume "i < length (prefix n (u \<frown> v))"
   227   then show "prefix n (u \<frown> v) ! i = (u @ prefix (n - length u) v) ! i"
   228     by (cases "i < length u") (auto simp: nth_append)
   229 qed
   230 
   231 lemma prefix_conc_length[simp]: "prefix (length w) (w \<frown> w') = w"
   232   by simp
   233 
   234 lemma suffix_conc_fst[simp]:
   235   assumes "n \<le> length u"
   236   shows "suffix n (u \<frown> v) = drop n u \<frown> v"
   237 proof
   238   show "suffix n (u \<frown> v) i = (drop n u \<frown> v) i" for i
   239     using assms by (cases "n + i < length u") (auto simp: algebra_simps)
   240 qed
   241 
   242 lemma suffix_conc_snd[simp]:
   243   assumes "n \<ge> length u"
   244   shows "suffix n (u \<frown> v) = suffix (n - length u) v"
   245 proof
   246   show "suffix n (u \<frown> v) i = suffix (n - length u) v i" for i
   247     using assms by simp
   248 qed
   249 
   250 lemma suffix_conc_length[simp]: "suffix (length w) (w \<frown> w') = w'"
   251   unfolding conc_def by force
   252 
   253 lemma concat_eq[iff]:
   254   assumes "length v\<^sub>1 = length v\<^sub>2"
   255   shows "v\<^sub>1 \<frown> u\<^sub>1 = v\<^sub>2 \<frown> u\<^sub>2 \<longleftrightarrow> v\<^sub>1 = v\<^sub>2 \<and> u\<^sub>1 = u\<^sub>2"
   256   (is "?lhs \<longleftrightarrow> ?rhs")
   257 proof
   258   assume ?lhs
   259   then have 1: "(v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" for i by auto
   260   show ?rhs
   261   proof (intro conjI ext nth_equalityI)
   262     show "length v\<^sub>1 = length v\<^sub>2" by (rule assms(1))
   263   next
   264     fix i
   265     assume 2: "i < length v\<^sub>1"
   266     have 3: "i < length v\<^sub>2" using assms(1) 2 by simp
   267     show "v\<^sub>1 ! i = v\<^sub>2 ! i" using 1[of i] 2 3 by simp
   268   next
   269     show "u\<^sub>1 i = u\<^sub>2 i" for i
   270       using 1[of "length v\<^sub>1 + i"] assms(1) by simp
   271   qed
   272 next
   273   assume ?rhs
   274   then show ?lhs by simp
   275 qed
   276 
   277 lemma same_concat_eq[iff]: "u \<frown> v = u \<frown> w \<longleftrightarrow> v = w"
   278   by simp
   279 
   280 lemma comp_concat[simp]: "f \<circ> u \<frown> v = map f u \<frown> (f \<circ> v)"
   281 proof
   282   fix i
   283   show "(f \<circ> u \<frown> v) i = (map f u \<frown> (f \<circ> v)) i"
   284     by (cases "i < length u") simp_all
   285 qed
   286 
   287 
   288 subsection \<open>Prepending\<close>
   289 
   290 primrec build :: "'a \<Rightarrow> 'a word \<Rightarrow> 'a word"  (infixr "##" 65)
   291   where "(a ## w) 0 = a" | "(a ## w) (Suc i) = w i"
   292 
   293 lemma build_eq[iff]: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2 \<longleftrightarrow> a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
   294 proof
   295   assume 1: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2"
   296   have 2: "(a\<^sub>1 ## w\<^sub>1) i = (a\<^sub>2 ## w\<^sub>2) i" for i
   297     using 1 by auto
   298   show "a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
   299   proof (intro conjI ext)
   300     show "a\<^sub>1 = a\<^sub>2"
   301       using 2[of "0"] by simp
   302     show "w\<^sub>1 i = w\<^sub>2 i" for i
   303       using 2[of "Suc i"] by simp
   304   qed
   305 next
   306   assume 1: "a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
   307   show "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2" using 1 by simp
   308 qed
   309 
   310 lemma build_cons[simp]: "(a # u) \<frown> v = a ## u \<frown> v"
   311 proof
   312   fix i
   313   show "((a # u) \<frown> v) i = (a ## u \<frown> v) i"
   314   proof (cases i)
   315     case 0
   316     show ?thesis unfolding 0 by simp
   317   next
   318     case (Suc j)
   319     show ?thesis unfolding Suc by (cases "j < length u", simp+)
   320   qed
   321 qed
   322 
   323 lemma build_append[simp]: "(w @ a # u) \<frown> v = w \<frown> a ## u \<frown> v"
   324   unfolding conc_conc[symmetric] by simp
   325 
   326 lemma build_first[simp]: "w 0 ## suffix (Suc 0) w = w"
   327 proof
   328   show "(w 0 ## suffix (Suc 0) w) i = w i" for i
   329     by (cases i) simp_all
   330 qed
   331 
   332 lemma build_split[intro]: "w = w 0 ## suffix 1 w"
   333   by simp
   334 
   335 lemma build_range[simp]: "range (a ## w) = insert a (range w)"
   336 proof safe
   337   show "(a ## w) i \<notin> range w \<Longrightarrow> (a ## w) i = a" for i
   338     by (cases i) auto
   339   show "a \<in> range (a ## w)"
   340   proof (rule range_eqI)
   341     show "a = (a ## w) 0" by simp
   342   qed
   343   show "w i \<in> range (a ## w)" for i
   344   proof (rule range_eqI)
   345     show "w i = (a ## w) (Suc i)" by simp
   346   qed
   347 qed
   348 
   349 lemma suffix_singleton_suffix[simp]: "w i ## suffix (Suc i) w = suffix i w"
   350   using suffix_subseq_join[of i "Suc i" w]
   351   by simp
   352 
   353 text \<open>Find the first occurrence of a letter from a given set\<close>
   354 lemma word_first_split_set:
   355   assumes "A \<inter> range w \<noteq> {}"
   356   obtains u a v where "w = u \<frown> [a] \<frown> v" "A \<inter> set u = {}" "a \<in> A"
   357 proof -
   358   define i where "i = (LEAST i. w i \<in> A)"
   359   show ?thesis
   360   proof
   361     show "w = prefix i w \<frown> [w i] \<frown> suffix (Suc i) w"
   362       by simp
   363     show "A \<inter> set (prefix i w) = {}"
   364       apply safe
   365       subgoal premises prems for a
   366       proof -
   367         from prems obtain k where 3: "k < i" "w k = a"
   368           by auto
   369         have 4: "w k \<notin> A"
   370           using not_less_Least 3(1) unfolding i_def .
   371         show ?thesis
   372           using prems(1) 3(2) 4 by auto
   373       qed
   374       done
   375     show "w i \<in> A"
   376       using LeastI assms(1) unfolding i_def by fast
   377   qed
   378 qed
   379 
   380 
   381 subsection \<open>The limit set of an $\omega$-word\<close>
   382 
   383 text \<open>
   384   The limit set (also called infinity set) of an $\omega$-word
   385   is the set of letters that appear infinitely often in the word.
   386   This set plays an important role in defining acceptance conditions
   387   of $\omega$-automata.
   388 \<close>
   389 
   390 definition limit :: "'a word \<Rightarrow> 'a set"
   391   where "limit x \<equiv> {a . \<exists>\<^sub>\<infinity>n . x n = a}"
   392 
   393 lemma limit_iff_frequent: "a \<in> limit x \<longleftrightarrow> (\<exists>\<^sub>\<infinity>n . x n = a)"
   394   by (simp add: limit_def)
   395 
   396 text \<open>
   397   The following is a different way to define the limit,
   398   using the reverse image, making the laws about reverse
   399   image applicable to the limit set.
   400   (Might want to change the definition above?)
   401 \<close>
   402 
   403 lemma limit_vimage: "(a \<in> limit x) = infinite (x -` {a})"
   404   by (simp add: limit_def Inf_many_def vimage_def)
   405 
   406 lemma two_in_limit_iff:
   407   "({a, b} \<subseteq> limit x) =
   408     ((\<exists>n. x n =a ) \<and> (\<forall>n. x n = a \<longrightarrow> (\<exists>m>n. x m = b)) \<and> (\<forall>m. x m = b \<longrightarrow> (\<exists>n>m. x n = a)))"
   409   (is "?lhs = (?r1 \<and> ?r2 \<and> ?r3)")
   410 proof
   411   assume lhs: "?lhs"
   412   hence 1: "?r1" by (auto simp: limit_def elim: INFM_EX)
   413   from lhs have "\<forall>n. \<exists>m>n. x m = b" by (auto simp: limit_def INFM_nat)
   414   hence 2: "?r2" by simp
   415   from lhs have "\<forall>m. \<exists>n>m. x n = a" by (auto simp: limit_def INFM_nat)
   416   hence 3: "?r3" by simp
   417   from 1 2 3 show "?r1 \<and> ?r2 \<and> ?r3" by simp
   418 next
   419   assume "?r1 \<and> ?r2 \<and> ?r3"
   420   hence 1: "?r1" and 2: "?r2" and 3: "?r3" by simp+
   421   have infa: "\<forall>m. \<exists>n\<ge>m. x n = a"
   422   proof
   423     fix m
   424     show "\<exists>n\<ge>m. x n = a" (is "?A m")
   425     proof (induct m)
   426       from 1 show "?A 0" by simp
   427     next
   428       fix m
   429       assume ih: "?A m"
   430       then obtain n where n: "n \<ge> m" "x n = a" by auto
   431       with 2 obtain k where k: "k>n" "x k = b" by auto
   432       with 3 obtain l where l: "l>k" "x l = a" by auto
   433       from n k l have "l \<ge> Suc m" by auto
   434       with l show "?A (Suc m)" by auto
   435     qed
   436   qed
   437   hence infa': "\<exists>\<^sub>\<infinity>n. x n = a" by (simp add: INFM_nat_le)
   438   have "\<forall>n. \<exists>m>n. x m = b"
   439   proof
   440     fix n
   441     from infa obtain k where k1: "k\<ge>n" and k2: "x k = a" by auto
   442     from 2 k2 obtain l where l1: "l>k" and l2: "x l = b" by auto
   443     from k1 l1 have "l > n" by auto
   444     with l2 show "\<exists>m>n. x m = b" by auto
   445   qed
   446   hence "\<exists>\<^sub>\<infinity>m. x m = b" by (simp add: INFM_nat)
   447   with infa' show "?lhs" by (auto simp: limit_def)
   448 qed
   449 
   450 text \<open>
   451   For $\omega$-words over a finite alphabet, the limit set is
   452   non-empty. Moreover, from some position onward, any such word
   453   contains only letters from its limit set.
   454 \<close>
   455 
   456 lemma limit_nonempty:
   457   assumes fin: "finite (range x)"
   458   shows "\<exists>a. a \<in> limit x"
   459 proof -
   460   from fin obtain a where "a \<in> range x \<and> infinite (x -` {a})"
   461     by (rule inf_img_fin_domE) auto
   462   hence "a \<in> limit x"
   463     by (auto simp add: limit_vimage)
   464   thus ?thesis ..
   465 qed
   466 
   467 lemmas limit_nonemptyE = limit_nonempty[THEN exE]
   468 
   469 lemma limit_inter_INF:
   470   assumes hyp: "limit w \<inter> S \<noteq> {}"
   471   shows "\<exists>\<^sub>\<infinity> n. w n \<in> S"
   472 proof -
   473   from hyp obtain x where "\<exists>\<^sub>\<infinity> n. w n = x" and "x \<in> S"
   474     by (auto simp add: limit_def)
   475   thus ?thesis
   476     by (auto elim: INFM_mono)
   477 qed
   478 
   479 text \<open>
   480   The reverse implication is true only if $S$ is finite.
   481 \<close>
   482 
   483 lemma INF_limit_inter:
   484   assumes hyp: "\<exists>\<^sub>\<infinity> n. w n \<in>  S"
   485     and fin: "finite (S \<inter> range w)"
   486   shows  "\<exists>a. a \<in> limit w \<inter> S"
   487 proof (rule ccontr)
   488   assume contra: "\<not>(\<exists>a. a \<in> limit w \<inter> S)"
   489   hence "\<forall>a\<in>S. finite {n. w n = a}"
   490     by (auto simp add: limit_def Inf_many_def)
   491   with fin have "finite (UN a:S \<inter> range w. {n. w n = a})"
   492     by auto
   493   moreover
   494   have "(UN a:S \<inter> range w. {n. w n = a}) = {n. w n \<in> S}"
   495     by auto
   496   moreover
   497   note hyp
   498   ultimately show "False"
   499     by (simp add: Inf_many_def)
   500 qed
   501 
   502 lemma fin_ex_inf_eq_limit: "finite A \<Longrightarrow> (\<exists>\<^sub>\<infinity>i. w i \<in> A) \<longleftrightarrow> limit w \<inter> A \<noteq> {}"
   503   by (metis INF_limit_inter equals0D finite_Int limit_inter_INF)
   504 
   505 lemma limit_in_range_suffix: "limit x \<subseteq> range (suffix k x)"
   506 proof
   507   fix a
   508   assume "a \<in> limit x"
   509   then obtain l where
   510     kl: "k < l" and xl: "x l = a"
   511     by (auto simp add: limit_def INFM_nat)
   512   from kl obtain m where "l = k+m"
   513     by (auto simp add:  less_iff_Suc_add)
   514   with xl show "a \<in> range (suffix k x)"
   515     by auto
   516 qed
   517 
   518 lemma limit_in_range: "limit r \<subseteq> range r"
   519   using limit_in_range_suffix[of r 0] by simp
   520 
   521 lemmas limit_in_range_suffixD = limit_in_range_suffix[THEN subsetD]
   522 
   523 lemma limit_subset: "limit f \<subseteq> f ` {n..}"
   524   using limit_in_range_suffix[of f n] unfolding suffix_def by auto
   525 
   526 theorem limit_is_suffix:
   527   assumes fin: "finite (range x)"
   528   shows "\<exists>k. limit x = range (suffix k x)"
   529 proof -
   530   have "\<exists>k. range (suffix k x) \<subseteq> limit x"
   531   proof -
   532     \<comment> \<open>The set of letters that are not in the limit is certainly finite.\<close>
   533     from fin have "finite (range x - limit x)"
   534       by simp
   535     \<comment> \<open>Moreover, any such letter occurs only finitely often\<close>
   536     moreover
   537     have "\<forall>a \<in> range x - limit x. finite (x -` {a})"
   538       by (auto simp add: limit_vimage)
   539     \<comment> \<open>Thus, there are only finitely many occurrences of such letters.\<close>
   540     ultimately have "finite (UN a : range x - limit x. x -` {a})"
   541       by (blast intro: finite_UN_I)
   542     \<comment> \<open>Therefore these occurrences are within some initial interval.\<close>
   543     then obtain k where "(UN a : range x - limit x. x -` {a}) \<subseteq> {..<k}"
   544       by (blast dest: finite_nat_bounded)
   545     \<comment> \<open>This is just the bound we are looking for.\<close>
   546     hence "\<forall>m. k \<le> m \<longrightarrow> x m \<in> limit x"
   547       by (auto simp add: limit_vimage)
   548     hence "range (suffix k x) \<subseteq> limit x"
   549       by auto
   550     thus ?thesis ..
   551   qed
   552   then obtain k where "range (suffix k x) \<subseteq> limit x" ..
   553   with limit_in_range_suffix
   554   have "limit x = range (suffix k x)"
   555     by (rule subset_antisym)
   556   thus ?thesis ..
   557 qed
   558 
   559 lemmas limit_is_suffixE = limit_is_suffix[THEN exE]
   560 
   561 
   562 text \<open>
   563   The limit set enjoys some simple algebraic laws with respect
   564   to concatenation, suffixes, iteration, and renaming.
   565 \<close>
   566 
   567 theorem limit_conc [simp]: "limit (w \<frown> x) = limit x"
   568 proof (auto)
   569   fix a assume a: "a \<in> limit (w \<frown> x)"
   570   have "\<forall>m. \<exists>n. m<n \<and> x n = a"
   571   proof
   572     fix m
   573     from a obtain n where "m + length w < n \<and> (w \<frown> x) n = a"
   574       by (auto simp add: limit_def Inf_many_def infinite_nat_iff_unbounded)
   575     hence "m < n - length w \<and> x (n - length w) = a"
   576       by (auto simp add: conc_def)
   577     thus "\<exists>n. m<n \<and> x n = a" ..
   578   qed
   579   hence "infinite {n . x n = a}"
   580     by (simp add: infinite_nat_iff_unbounded)
   581   thus "a \<in> limit x"
   582     by (simp add: limit_def Inf_many_def)
   583 next
   584   fix a assume a: "a \<in> limit x"
   585   have "\<forall>m. length w < m \<longrightarrow> (\<exists>n. m<n \<and> (w \<frown> x) n = a)"
   586   proof (clarify)
   587     fix m
   588     assume m: "length w < m"
   589     with a obtain n where "m - length w < n \<and> x n = a"
   590       by (auto simp add: limit_def Inf_many_def infinite_nat_iff_unbounded)
   591     with m have "m < n + length w \<and> (w \<frown> x) (n + length w) = a"
   592       by (simp add: conc_def, arith)
   593     thus "\<exists>n. m<n \<and> (w \<frown> x) n = a" ..
   594   qed
   595   hence "infinite {n . (w \<frown> x) n = a}"
   596     by (simp add: unbounded_k_infinite)
   597   thus "a \<in> limit (w \<frown> x)"
   598     by (simp add: limit_def Inf_many_def)
   599 qed
   600 
   601 theorem limit_suffix [simp]: "limit (suffix n x) = limit x"
   602 proof -
   603   have "x = (prefix n x) \<frown> (suffix n x)"
   604     by (simp add: prefix_suffix)
   605   hence "limit x = limit (prefix n x \<frown> suffix n x)"
   606     by simp
   607   also have "\<dots> = limit (suffix n x)"
   608     by (rule limit_conc)
   609   finally show ?thesis
   610     by (rule sym)
   611 qed
   612 
   613 theorem limit_iter [simp]:
   614   assumes nempty: "0 < length w"
   615   shows "limit w\<^sup>\<omega> = set w"
   616 proof
   617   have "limit w\<^sup>\<omega> \<subseteq> range w\<^sup>\<omega>"
   618     by (auto simp add: limit_def dest: INFM_EX)
   619   also from nempty have "\<dots> \<subseteq> set w"
   620     by auto
   621   finally show "limit w\<^sup>\<omega> \<subseteq> set w" .
   622 next
   623   {
   624     fix a assume a: "a \<in> set w"
   625     then obtain k where k: "k < length w \<and> w!k = a"
   626       by (auto simp add: set_conv_nth)
   627     \<comment> \<open>the following bound is terrible, but it simplifies the proof\<close>
   628     from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
   629       by (simp add: mod_add_left_eq [symmetric])
   630     moreover
   631     \<comment> \<open>why is the following so hard to prove??\<close>
   632     have "\<forall>m. m < (Suc m)*(length w) + k"
   633     proof
   634       fix m
   635       from nempty have "1 \<le> length w" by arith
   636       hence "m*1 \<le> m*length w" by simp
   637       hence "m \<le> m*length w" by simp
   638       with nempty have "m < length w + (m*length w) + k" by arith
   639       thus "m < (Suc m)*(length w) + k" by simp
   640     qed
   641     moreover note nempty
   642     ultimately have "a \<in> limit w\<^sup>\<omega>"
   643       by (auto simp add: limit_iff_frequent INFM_nat)
   644   }
   645   then show "set w \<subseteq> limit w\<^sup>\<omega>" by auto
   646 qed
   647 
   648 lemma limit_o [simp]:
   649   assumes a: "a \<in> limit w"
   650   shows "f a \<in> limit (f \<circ> w)"
   651 proof -
   652   from a
   653   have "\<exists>\<^sub>\<infinity>n. w n = a"
   654     by (simp add: limit_iff_frequent)
   655   hence "\<exists>\<^sub>\<infinity>n. f (w n) = f a"
   656     by (rule INFM_mono, simp)
   657   thus "f a \<in> limit (f \<circ> w)"
   658     by (simp add: limit_iff_frequent)
   659 qed
   660 
   661 text \<open>
   662   The converse relation is not true in general: $f(a)$ can be in the
   663   limit of $f \circ w$ even though $a$ is not in the limit of $w$.
   664   However, \<open>limit\<close> commutes with renaming if the function is
   665   injective. More generally, if $f(a)$ is the image of only finitely
   666   many elements, some of these must be in the limit of $w$.
   667 \<close>
   668 
   669 lemma limit_o_inv:
   670   assumes fin: "finite (f -` {x})"
   671     and x: "x \<in> limit (f \<circ> w)"
   672   shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
   673 proof (rule ccontr)
   674   assume contra: "\<not> ?thesis"
   675   \<comment> \<open>hence, every element in the pre-image occurs only finitely often\<close>
   676   then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
   677     by (simp add: limit_def Inf_many_def)
   678   \<comment> \<open>so there are only finitely many occurrences of any such element\<close>
   679   with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
   680     by auto
   681   \<comment> \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
   682   moreover
   683   have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
   684     by auto
   685   ultimately
   686   \<comment> \<open>so $x$ can occur only finitely often in the translated word\<close>
   687   have "finite {n. f(w n) = x}"
   688     by simp
   689   \<comment> \<open>\ldots\ which yields a contradiction\<close>
   690   with x show "False"
   691     by (simp add: limit_def Inf_many_def)
   692 qed
   693 
   694 theorem limit_inj [simp]:
   695   assumes inj: "inj f"
   696   shows "limit (f \<circ> w) = f ` (limit w)"
   697 proof
   698   show "f ` limit w \<subseteq> limit (f \<circ> w)"
   699     by auto
   700   show "limit (f \<circ> w) \<subseteq> f ` limit w"
   701   proof
   702     fix x
   703     assume x: "x \<in> limit (f \<circ> w)"
   704     from inj have "finite (f -` {x})"
   705       by (blast intro: finite_vimageI)
   706     with x obtain a where a: "a \<in> (f -` {x}) \<and> a \<in> limit w"
   707       by (blast dest: limit_o_inv)
   708     thus "x \<in> f ` (limit w)"
   709       by auto
   710   qed
   711 qed
   712 
   713 lemma limit_inter_empty:
   714   assumes fin: "finite (range w)"
   715   assumes hyp: "limit w \<inter> S = {}"
   716   shows "\<forall>\<^sub>\<infinity>n. w n \<notin> S"
   717 proof -
   718   from fin obtain k where k_def: "limit w = range (suffix k w)"
   719     using limit_is_suffix by blast
   720   have "w (k + k') \<notin> S" for k'
   721     using hyp unfolding k_def suffix_def image_def by blast
   722   thus ?thesis
   723     unfolding MOST_nat_le using le_Suc_ex by blast
   724 qed
   725 
   726 text \<open>If the limit is the suffix of the sequence's range,
   727   we may increase the suffix index arbitrarily\<close>
   728 lemma limit_range_suffix_incr:
   729   assumes "limit r = range (suffix i r)"
   730   assumes "j\<ge>i"
   731   shows "limit r = range (suffix j r)"
   732     (is "?lhs = ?rhs")
   733 proof -
   734   have "?lhs = range (suffix i r)"
   735     using assms by simp
   736   moreover
   737   have "\<dots> \<supseteq> ?rhs" using \<open>j\<ge>i\<close>
   738     by (metis (mono_tags, lifting) assms(2)
   739         image_subsetI le_Suc_ex range_eqI suffix_def suffix_suffix)
   740   moreover
   741   have "\<dots> \<supseteq> ?lhs" by (rule limit_in_range_suffix)
   742   ultimately
   743   show "?lhs = ?rhs"
   744     by (metis antisym_conv limit_in_range_suffix)
   745 qed
   746 
   747 text \<open>For two finite sequences, we can find a common suffix index such
   748   that the limits can be represented as these suffixes' ranges.\<close>
   749 lemma common_range_limit:
   750   assumes "finite (range x)"
   751     and "finite (range y)"
   752   obtains i where "limit x = range (suffix i x)"
   753     and "limit y = range (suffix i y)"
   754 proof -
   755   obtain i j where 1: "limit x = range (suffix i x)"
   756     and 2: "limit y = range (suffix j y)"
   757     using assms limit_is_suffix by metis
   758   have "limit x = range (suffix (max i j) x)"
   759     and "limit y = range (suffix (max i j) y)"
   760     using limit_range_suffix_incr[OF 1] limit_range_suffix_incr[OF 2]
   761     by auto
   762   thus ?thesis
   763     using that by metis
   764 qed
   765 
   766 
   767 subsection \<open>Index sequences and piecewise definitions\<close>
   768 
   769 text \<open>
   770   A word can be defined piecewise: given a sequence of words $w_0, w_1, \ldots$
   771   and a strictly increasing sequence of integers $i_0, i_1, \ldots$ where $i_0=0$,
   772   a single word is obtained by concatenating subwords of the $w_n$ as given by
   773   the integers: the resulting word is
   774   \[
   775     (w_0)_{i_0} \ldots (w_0)_{i_1-1} (w_1)_{i_1} \ldots (w_1)_{i_2-1} \ldots
   776   \]
   777   We prepare the field by proving some trivial facts about such sequences of
   778   indexes.
   779 \<close>
   780 
   781 definition idx_sequence :: "nat word \<Rightarrow> bool"
   782   where "idx_sequence idx \<equiv> (idx 0 = 0) \<and> (\<forall>n. idx n < idx (Suc n))"
   783 
   784 lemma idx_sequence_less:
   785   assumes iseq: "idx_sequence idx"
   786   shows "idx n < idx (Suc(n+k))"
   787 proof (induct k)
   788   from iseq show "idx n < idx (Suc (n + 0))"
   789     by (simp add: idx_sequence_def)
   790 next
   791   fix k
   792   assume ih: "idx n < idx (Suc(n+k))"
   793   from iseq have "idx (Suc(n+k)) < idx (Suc(n + Suc k))"
   794     by (simp add: idx_sequence_def)
   795   with ih show "idx n < idx (Suc(n + Suc k))"
   796     by (rule less_trans)
   797 qed
   798 
   799 lemma idx_sequence_inj:
   800   assumes iseq: "idx_sequence idx"
   801     and eq: "idx m = idx n"
   802   shows "m = n"
   803 proof (cases m n rule: linorder_cases)
   804   case greater
   805   then obtain k where "m = Suc(n+k)"
   806     by (auto simp add: less_iff_Suc_add)
   807   with iseq have "idx n < idx m"
   808     by (simp add: idx_sequence_less)
   809   with eq show ?thesis
   810     by simp
   811 next
   812   case less
   813   then obtain k where "n = Suc(m+k)"
   814     by (auto simp add: less_iff_Suc_add)
   815   with iseq have "idx m < idx n"
   816     by (simp add: idx_sequence_less)
   817   with eq show ?thesis
   818     by simp
   819 qed
   820 
   821 lemma idx_sequence_mono:
   822   assumes iseq: "idx_sequence idx"
   823     and m: "m \<le> n"
   824   shows "idx m \<le> idx n"
   825 proof (cases "m=n")
   826   case True
   827   thus ?thesis by simp
   828 next
   829   case False
   830   with m have "m < n" by simp
   831   then obtain k where "n = Suc(m+k)"
   832     by (auto simp add: less_iff_Suc_add)
   833   with iseq have "idx m < idx n"
   834     by (simp add: idx_sequence_less)
   835   thus ?thesis by simp
   836 qed
   837 
   838 text \<open>
   839   Given an index sequence, every natural number is contained in the
   840   interval defined by two adjacent indexes, and in fact this interval
   841   is determined uniquely.
   842 \<close>
   843 
   844 lemma idx_sequence_idx:
   845   assumes "idx_sequence idx"
   846   shows "idx k \<in> {idx k ..< idx (Suc k)}"
   847 using assms by (auto simp add: idx_sequence_def)
   848 
   849 lemma idx_sequence_interval:
   850   assumes iseq: "idx_sequence idx"
   851   shows "\<exists>k. n \<in> {idx k ..< idx (Suc k) }"
   852     (is "?P n" is "\<exists>k. ?in n k")
   853 proof (induct n)
   854   from iseq have "0 = idx 0"
   855     by (simp add: idx_sequence_def)
   856   moreover
   857   from iseq have "idx 0 \<in> {idx 0 ..< idx (Suc 0) }"
   858     by (rule idx_sequence_idx)
   859   ultimately
   860   show "?P 0" by auto
   861 next
   862   fix n
   863   assume "?P n"
   864   then obtain k where k: "?in n k" ..
   865   show "?P (Suc n)"
   866   proof (cases "Suc n < idx (Suc k)")
   867     case True
   868     with k have "?in (Suc n) k"
   869       by simp
   870     thus ?thesis ..
   871   next
   872     case False
   873     with k have "Suc n = idx (Suc k)"
   874       by auto
   875     with iseq have "?in (Suc n) (Suc k)"
   876       by (simp add: idx_sequence_def)
   877     thus ?thesis ..
   878   qed
   879 qed
   880 
   881 lemma idx_sequence_interval_unique:
   882   assumes iseq: "idx_sequence idx"
   883     and k: "n \<in> {idx k ..< idx (Suc k)}"
   884     and m: "n \<in> {idx m ..< idx (Suc m)}"
   885   shows "k = m"
   886 proof (cases k m rule: linorder_cases)
   887   case less
   888   hence "Suc k \<le> m" by simp
   889   with iseq have "idx (Suc k) \<le> idx m"
   890     by (rule idx_sequence_mono)
   891   with m have "idx (Suc k) \<le> n"
   892     by auto
   893   with k have "False"
   894     by simp
   895   thus ?thesis ..
   896 next
   897   case greater
   898   hence "Suc m \<le> k" by simp
   899   with iseq have "idx (Suc m) \<le> idx k"
   900     by (rule idx_sequence_mono)
   901   with k have "idx (Suc m) \<le> n"
   902     by auto
   903   with m have "False"
   904     by simp
   905   thus ?thesis ..
   906 qed
   907 
   908 lemma idx_sequence_unique_interval:
   909   assumes iseq: "idx_sequence idx"
   910   shows "\<exists>! k. n \<in> {idx k ..< idx (Suc k) }"
   911 proof (rule ex_ex1I)
   912   from iseq show "\<exists>k. n \<in> {idx k ..< idx (Suc k)}"
   913     by (rule idx_sequence_interval)
   914 next
   915   fix k y
   916   assume "n \<in> {idx k..<idx (Suc k)}" and "n \<in> {idx y..<idx (Suc y)}"
   917   with iseq show "k = y" by (auto elim: idx_sequence_interval_unique)
   918 qed
   919 
   920 text \<open>
   921   Now we can define the piecewise construction of a word using
   922   an index sequence.
   923 \<close>
   924 
   925 definition merge :: "'a word word \<Rightarrow> nat word \<Rightarrow> 'a word"
   926   where "merge ws idx \<equiv> \<lambda>n. let i = THE i. n \<in> {idx i ..< idx (Suc i) } in ws i n"
   927 
   928 lemma merge:
   929   assumes idx: "idx_sequence idx"
   930     and n: "n \<in> {idx i ..< idx (Suc i)}"
   931   shows "merge ws idx n = ws i n"
   932 proof -
   933   from n have "(THE k. n \<in> {idx k ..< idx (Suc k) }) = i"
   934     by (rule the_equality[OF _ sym[OF idx_sequence_interval_unique[OF idx n]]]) simp
   935   thus ?thesis
   936     by (simp add: merge_def Let_def)
   937 qed
   938 
   939 lemma merge0:
   940   assumes idx: "idx_sequence idx"
   941   shows "merge ws idx 0 = ws 0 0"
   942 proof (rule merge[OF idx])
   943   from idx have "idx 0 < idx (Suc 0)"
   944     unfolding idx_sequence_def by blast
   945   with idx show "0 \<in> {idx 0 ..< idx (Suc 0)}"
   946     by (simp add: idx_sequence_def)
   947 qed
   948 
   949 lemma merge_Suc:
   950   assumes idx: "idx_sequence idx"
   951     and n: "n \<in> {idx i ..< idx (Suc i)}"
   952   shows "merge ws idx (Suc n) = (if Suc n = idx (Suc i) then ws (Suc i) else ws i) (Suc n)"
   953 proof auto
   954   assume eq: "Suc n = idx (Suc i)"
   955   from idx have "idx (Suc i) < idx (Suc(Suc i))"
   956     unfolding idx_sequence_def by blast
   957   with eq idx show "merge ws idx (idx (Suc i)) = ws (Suc i) (idx (Suc i))"
   958     by (simp add: merge)
   959 next
   960   assume neq: "Suc n \<noteq> idx (Suc i)"
   961   with n have "Suc n \<in> {idx i ..< idx (Suc i) }"
   962     by auto
   963   with idx show "merge ws idx (Suc n) = ws i (Suc n)"
   964     by (rule merge)
   965 qed
   966 
   967 end