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