src/HOL/Library/Omega_Words_Fun.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 64593 50c715579715 child 67443 3abf6a722518 permissions -rw-r--r--
executable domain membership checks
     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>)" )

    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 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

   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 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

   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> "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

   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> "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"

   629       by (simp add: mod_add_left_eq [symmetric])

   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

   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> "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

   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