src/HOL/Library/Omega_Words_Fun.thy
 author wenzelm Mon Dec 28 01:28:28 2015 +0100 (2015-12-28) changeset 61945 1135b8de26c3 parent 61585 a9599d3d7610 child 63040 eb4ddd18d635 permissions -rw-r--r--
more symbols;
1 (*
2     Author:     Stefan Merz
3     Author:     Salomon Sickert
4     Author:     Julian Brunner
5     Author:     Peter Lammich
6 *)
8 section \<open>$\omega$-words\<close>
10 theory Omega_Words_Fun
12 imports Infinite_Set
13 begin
15 text \<open>Note: This theory is based on Stefan Merz's work.\<close>
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>
28 subsection \<open>Type declaration and elementary operations\<close>
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>
37 type_synonym
38   'a word = "nat \<Rightarrow> 'a"
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>
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)"
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)))"
54 lemma conc_empty[simp]: "[] \<frown> w = w"
55   unfolding conc_def by auto
57 lemma conc_fst[simp]: "n < length w \<Longrightarrow> (w \<frown> x) n = w!n"
60 lemma conc_snd[simp]: "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n - length w)"
63 lemma iter_nth [simp]: "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))"
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
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
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)
114 subsection \<open>Subsequence, Prefix, and Suffix\<close>
116 definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
117   where "suffix k x \<equiv> \<lambda>n. x (k+n)"
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]"
122 abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
123   where "prefix n w \<equiv> subsequence w 0 n"
125 lemma suffix_nth [simp]: "(suffix k x) n = x (k+n)"
128 lemma suffix_0 [simp]: "suffix 0 x = x"
131 lemma suffix_suffix [simp]: "suffix m (suffix k x) = suffix (k+m) x"
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 ..
137 lemma subsequence_drop[simp]: "drop i (w [j \<rightarrow> k]) = w [j + i \<rightarrow> k]"
138   by (simp add: subsequence_def drop_map)
140 lemma subsequence_empty[simp]: "w [i \<rightarrow> j] = [] \<longleftrightarrow> j \<le> i"
141   by (auto simp add: subsequence_def)
143 lemma subsequence_length[simp]: "length (subsequence w i j) = j - i"
146 lemma subsequence_nth[simp]: "k < j - i \<Longrightarrow> (w [i \<rightarrow> j]) ! k = w (i + k)"
147   unfolding subsequence_def
148   by auto
150 lemma subseq_to_zero[simp]: "w[i\<rightarrow>0] = []"
151   by simp
153 lemma subseq_to_smaller[simp]: "i\<ge>j \<Longrightarrow> w[i\<rightarrow>j] = []"
154   by simp
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)
159 lemma subsequence_singleton[simp]: "w [i \<rightarrow> Suc i] = [w i]"
160   by (auto simp: subsequence_def)
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])"
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
179 qed
181 lemma prefix_suffix: "x = prefix n x \<frown> (suffix n x)"
182   by (rule ext) (simp add: subsequence_def conc_def)
184 declare prefix_suffix[symmetric, simp]
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
196 lemma set_subsequence[simp]: "set (w[i\<rightarrow>j]) = w{i..<j}"
197   unfolding subsequence_def by auto
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)
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)
205 lemma suffix_subseq_join[simp]: "i \<le> j \<Longrightarrow> v [i \<rightarrow> j] \<frown> suffix j v = suffix i v"
207     subsequence_shift suffix_suffix)
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
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 allI impI)
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
231 lemma prefix_conc_length[simp]: "prefix (length w) (w \<frown> w') = w"
232   by simp
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
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
250 lemma suffix_conc_length[simp]: "suffix (length w) (w \<frown> w') = w'"
251   unfolding conc_def by force
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 allI impI)
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
277 lemma same_concat_eq[iff]: "u \<frown> v = u \<frown> w \<longleftrightarrow> v = w"
278   by simp
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
288 subsection \<open>Prepending\<close>
290 primrec build :: "'a \<Rightarrow> 'a word \<Rightarrow> 'a word"  (infixr "##" 65)
291   where "(a ## w) 0 = a" | "(a ## w) (Suc i) = w i"
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
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
323 lemma build_append[simp]: "(w @ a # u) \<frown> v = w \<frown> a ## u \<frown> v"
324   unfolding conc_conc[symmetric] by simp
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
332 lemma build_split[intro]: "w = w 0 ## suffix 1 w"
333   by simp
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
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
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   def i \<equiv> "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
381 subsection \<open>The limit set of an $\omega$-word\<close>
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>
390 definition limit :: "'a word \<Rightarrow> 'a set"
391   where "limit x \<equiv> {a . \<exists>\<^sub>\<infinity>n . x n = a}"
393 lemma limit_iff_frequent: "a \<in> limit x \<longleftrightarrow> (\<exists>\<^sub>\<infinity>n . x n = a)"
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>
403 lemma limit_vimage: "(a \<in> limit x) = infinite (x - {a})"
404   by (simp add: limit_def Inf_many_def vimage_def)
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
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>
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
467 lemmas limit_nonemptyE = limit_nonempty[THEN exE]
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
479 text \<open>
480   The reverse implication is true only if $S$ is finite.
481 \<close>
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"
500 qed
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)
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"
514   with xl show "a \<in> range (suffix k x)"
515     by auto
516 qed
518 lemma limit_in_range: "limit r \<subseteq> range r"
519   using limit_in_range_suffix[of r 0] by simp
521 lemmas limit_in_range_suffixD = limit_in_range_suffix[THEN subsetD]
523 lemma limit_subset: "limit f \<subseteq> f  {n..}"
524   using limit_in_range_suffix[of f n] unfolding suffix_def by auto
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> "The set of letters that are not in the limit is certainly finite."
533     from fin have "finite (range x - limit x)"
534       by simp
535     \<comment> "Moreover, any such letter occurs only finitely often"
536     moreover
537     have "\<forall>a \<in> range x - limit x. finite (x - {a})"
538       by (auto simp add: limit_vimage)
539     \<comment> "Thus, there are only finitely many occurrences of such letters."
540     ultimately have "finite (UN a : range x - limit x. x - {a})"
541       by (blast intro: finite_UN_I)
542     \<comment> "Therefore these occurrences are within some initial interval."
543     then obtain k where "(UN a : range x - limit x. x - {a}) \<subseteq> {..<k}"
544       by (blast dest: finite_nat_bounded)
545     \<comment> "This is just the bound we are looking for."
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
559 lemmas limit_is_suffixE = limit_is_suffix[THEN exE]
562 text \<open>
563   The limit set enjoys some simple algebraic laws with respect
564   to concatenation, suffixes, iteration, and renaming.
565 \<close>
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}"
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}"
597   thus "a \<in> limit (w \<frown> x)"
598     by (simp add: limit_def Inf_many_def)
599 qed
601 theorem limit_suffix [simp]: "limit (suffix n x) = limit x"
602 proof -
603   have "x = (prefix n x) \<frown> (suffix n x)"
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
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> "the following bound is terrible, but it simplifies the proof"
628     from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
630     moreover
631     \<comment> "why is the following so hard to prove??"
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
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"
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)"
659 qed
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>
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> "hence, every element in the pre-image occurs only finitely often"
676   then have "\<forall>a \<in> (f - {x}). finite {n. w n = a}"
677     by (simp add: limit_def Inf_many_def)
678   \<comment> "so there are only finitely many occurrences of any such element"
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> "so $x$ can occur only finitely often in the translated word"
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
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
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
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
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
767 subsection \<open>Index sequences and piecewise definitions\<close>
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>
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))"
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))"
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))"
795   with ih show "idx n < idx (Suc(n + Suc k))"
796     by (rule less_trans)
797 qed
799 lemma idx_sequence_inj:
800   assumes iseq: "idx_sequence idx"
801     and eq: "idx m = idx n"
802   shows "m = n"
803 proof (rule nat_less_cases)
804   assume "n<m"
805   then obtain k where "m = Suc(n+k)"
807   with iseq have "idx n < idx m"
809   with eq show ?thesis
810     by simp
811 next
812   assume "m<n"
813   then obtain k where "n = Suc(m+k)"
815   with iseq have "idx m < idx n"
817   with eq show ?thesis
818     by simp
819 qed (simp)
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)"
833   with iseq have "idx m < idx n"
835   thus ?thesis by simp
836 qed
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>
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)
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"
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)"
877     thus ?thesis ..
878   qed
879 qed
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 (rule nat_less_cases)
887   assume "k < m"
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   assume "m < k"
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 (simp)
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
920 text \<open>
921   Now we can define the piecewise construction of a word using
922   an index sequence.
923 \<close>
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"
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
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)}"
947 qed
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))"