(*
Author: Stefan Merz
Author: Salomon Sickert
Author: Julian Brunner
Author: Peter Lammich
*)
section \$\omega$-words\
theory Omega_Words_Fun
imports Infinite_Set
begin
text \Note: This theory is based on Stefan Merz's work.\
text \
Automata recognize languages, which are sets of words. For the
theory of $\omega$-automata, we are mostly interested in
$\omega$-words, but it is sometimes useful to reason about
finite words, too. We are modeling finite words as lists; this
lets us benefit from the existing library. Other formalizations
could be investigated, such as representing words as functions
whose domains are initial intervals of the natural numbers.
\
subsection \Type declaration and elementary operations\
text \
We represent $\omega$-words as functions from the natural numbers
to the alphabet type. Other possible formalizations include
a coinductive definition or a uniform encoding of finite and
infinite words, as studied by M\"uller et al.
\
type_synonym
'a word = "nat \ 'a"
text \
We can prefix a finite word to an $\omega$-word, and a way
to obtain an $\omega$-word from a finite, non-empty word is by
$\omega$-iteration.
\
definition
conc :: "['a list, 'a word] \ 'a word" (infixr "\" 65)
where "w \ x == \n. if n < length w then w!n else x (n - length w)"
definition
iter :: "'a list \ 'a word" ("(_\<^sup>\)" [1000])
where "iter w == if w = [] then undefined else (\n. w!(n mod (length w)))"
lemma conc_empty[simp]: "[] \ w = w"
unfolding conc_def by auto
lemma conc_fst[simp]: "n < length w \ (w \ x) n = w!n"
by (simp add: conc_def)
lemma conc_snd[simp]: "\(n < length w) \ (w \ x) n = x (n - length w)"
by (simp add: conc_def)
lemma iter_nth [simp]: "0 < length w \ w\<^sup>\ n = w!(n mod (length w))"
by (simp add: iter_def)
lemma conc_conc[simp]: "u \ v \ w = (u @ v) \ w" (is "?lhs = ?rhs")
proof
fix n
have u: "n < length u \ ?lhs n = ?rhs n"
by (simp add: conc_def nth_append)
have v: "\ \(n < length u); n < length u + length v \ \ ?lhs n = ?rhs n"
by (simp add: conc_def nth_append, arith)
have w: "\(n < length u + length v) \ ?lhs n = ?rhs n"
by (simp add: conc_def nth_append, arith)
from u v w show "?lhs n = ?rhs n" by blast
qed
lemma range_conc[simp]: "range (w\<^sub>1 \ w\<^sub>2) = set w\<^sub>1 \ range w\<^sub>2"
proof (intro equalityI subsetI)
fix a
assume "a \ range (w\<^sub>1 \ w\<^sub>2)"
then obtain i where 1: "a = (w\<^sub>1 \ w\<^sub>2) i" by auto
then show "a \ set w\<^sub>1 \ range w\<^sub>2"
unfolding 1 by (cases "i < length w\<^sub>1") simp_all
next
fix a
assume a: "a \ set w\<^sub>1 \ range w\<^sub>2"
then show "a \ range (w\<^sub>1 \ w\<^sub>2)"
proof
assume "a \ set w\<^sub>1"
then obtain i where 1: "i < length w\<^sub>1" "a = w\<^sub>1 ! i"
using in_set_conv_nth by metis
show ?thesis
proof
show "a = (w\<^sub>1 \ w\<^sub>2) i" using 1 by auto
show "i \ UNIV" by rule
qed
next
assume "a \ range w\<^sub>2"
then obtain i where 1: "a = w\<^sub>2 i" by auto
show ?thesis
proof
show "a = (w\<^sub>1 \ w\<^sub>2) (length w\<^sub>1 + i)" using 1 by simp
show "length w\<^sub>1 + i \ UNIV" by rule
qed
qed
qed
lemma iter_unroll: "0 < length w \ w\<^sup>\ = w \ w\<^sup>\"
by (rule ext) (simp add: conc_def mod_geq)
subsection \Subsequence, Prefix, and Suffix\
definition suffix :: "[nat, 'a word] \ 'a word"
where "suffix k x \ \n. x (k+n)"
definition subsequence :: "'a word \ nat \ nat \ 'a list" ("_ [_ \ _]" 900)
where "subsequence w i j \ map w [i.. 'a word \ 'a list"
where "prefix n w \ subsequence w 0 n"
lemma suffix_nth [simp]: "(suffix k x) n = x (k+n)"
by (simp add: suffix_def)
lemma suffix_0 [simp]: "suffix 0 x = x"
by (simp add: suffix_def)
lemma suffix_suffix [simp]: "suffix m (suffix k x) = suffix (k+m) x"
by (rule ext) (simp add: suffix_def add.assoc)
lemma subsequence_append: "prefix (i + j) w = prefix i w @ (w [i \ i + j])"
unfolding map_append[symmetric] upt_add_eq_append[OF le0] subsequence_def ..
lemma subsequence_drop[simp]: "drop i (w [j \ k]) = w [j + i \ k]"
by (simp add: subsequence_def drop_map)
lemma subsequence_empty[simp]: "w [i \ j] = [] \ j \ i"
by (auto simp add: subsequence_def)
lemma subsequence_length[simp]: "length (subsequence w i j) = j - i"
by (simp add: subsequence_def)
lemma subsequence_nth[simp]: "k < j - i \ (w [i \ j]) ! k = w (i + k)"
unfolding subsequence_def
by auto
lemma subseq_to_zero[simp]: "w[i\0] = []"
by simp
lemma subseq_to_smaller[simp]: "i\j \ w[i\j] = []"
by simp
lemma subseq_to_Suc[simp]: "i\j \ w [i \ Suc j] = w [ i \ j ] @ [w j]"
by (auto simp: subsequence_def)
lemma subsequence_singleton[simp]: "w [i \ Suc i] = [w i]"
by (auto simp: subsequence_def)
lemma subsequence_prefix_suffix: "prefix (j - i) (suffix i w) = w [i \ j]"
proof (cases "i \ j")
case True
have "w [i \ j] = map w (map (\n. n + i) [0.. = map (\n. w (n + i)) [0.. (suffix n x)"
by (rule ext) (simp add: subsequence_def conc_def)
declare prefix_suffix[symmetric, simp]
lemma word_split: obtains v\<^sub>1 v\<^sub>2 where "v = v\<^sub>1 \ v\<^sub>2" "length v\<^sub>1 = k"
proof
show "v = prefix k v \ suffix k v"
by (rule prefix_suffix)
show "length (prefix k v) = k"
by simp
qed
lemma set_subsequence[simp]: "set (w[i\j]) = w`{i.. k]) = w [j \ min (j + i) k]"
by (simp add: subsequence_def take_map min_def)
lemma subsequence_shift[simp]: "(suffix i w) [j \ k] = w [i + j \ i + k]"
by (metis add_diff_cancel_left subsequence_prefix_suffix suffix_suffix)
lemma suffix_subseq_join[simp]: "i \ j \ v [i \ j] \ suffix j v = suffix i v"
by (metis (no_types, lifting) Nat.add_0_right le_add_diff_inverse prefix_suffix
subsequence_shift suffix_suffix)
lemma prefix_conc_fst[simp]:
assumes "j \ length w"
shows "prefix j (w \ w') = take j w"
proof -
have "\i < j. (prefix j (w \ w')) ! i = (take j w) ! i"
using assms by (simp add: conc_fst subsequence_def)
thus ?thesis
by (simp add: assms list_eq_iff_nth_eq min.absorb2)
qed
lemma prefix_conc_snd[simp]:
assumes "n \ length u"
shows "prefix n (u \ v) = u @ prefix (n - length u) v"
proof (intro nth_equalityI allI impI)
show "length (prefix n (u \ v)) = length (u @ prefix (n - length u) v)"
using assms by simp
fix i
assume "i < length (prefix n (u \ v))"
then show "prefix n (u \ v) ! i = (u @ prefix (n - length u) v) ! i"
by (cases "i < length u") (auto simp: nth_append)
qed
lemma prefix_conc_length[simp]: "prefix (length w) (w \ w') = w"
by simp
lemma suffix_conc_fst[simp]:
assumes "n \ length u"
shows "suffix n (u \ v) = drop n u \ v"
proof
show "suffix n (u \ v) i = (drop n u \ v) i" for i
using assms by (cases "n + i < length u") (auto simp: algebra_simps)
qed
lemma suffix_conc_snd[simp]:
assumes "n \ length u"
shows "suffix n (u \ v) = suffix (n - length u) v"
proof
show "suffix n (u \ v) i = suffix (n - length u) v i" for i
using assms by simp
qed
lemma suffix_conc_length[simp]: "suffix (length w) (w \ w') = w'"
unfolding conc_def by force
lemma concat_eq[iff]:
assumes "length v\<^sub>1 = length v\<^sub>2"
shows "v\<^sub>1 \ u\<^sub>1 = v\<^sub>2 \ u\<^sub>2 \ v\<^sub>1 = v\<^sub>2 \ u\<^sub>1 = u\<^sub>2"
(is "?lhs \ ?rhs")
proof
assume ?lhs
then have 1: "(v\<^sub>1 \ u\<^sub>1) i = (v\<^sub>2 \ u\<^sub>2) i" for i by auto
show ?rhs
proof (intro conjI ext nth_equalityI allI impI)
show "length v\<^sub>1 = length v\<^sub>2" by (rule assms(1))
next
fix i
assume 2: "i < length v\<^sub>1"
have 3: "i < length v\<^sub>2" using assms(1) 2 by simp
show "v\<^sub>1 ! i = v\<^sub>2 ! i" using 1[of i] 2 3 by simp
next
show "u\<^sub>1 i = u\<^sub>2 i" for i
using 1[of "length v\<^sub>1 + i"] assms(1) by simp
qed
next
assume ?rhs
then show ?lhs by simp
qed
lemma same_concat_eq[iff]: "u \ v = u \ w \ v = w"
by simp
lemma comp_concat[simp]: "f \ u \ v = map f u \ (f \ v)"
proof
fix i
show "(f \ u \ v) i = (map f u \ (f \ v)) i"
by (cases "i < length u") simp_all
qed
subsection \Prepending\
primrec build :: "'a \ 'a word \ 'a word" (infixr "##" 65)
where "(a ## w) 0 = a" | "(a ## w) (Suc i) = w i"
lemma build_eq[iff]: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2 \ a\<^sub>1 = a\<^sub>2 \ w\<^sub>1 = w\<^sub>2"
proof
assume 1: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2"
have 2: "(a\<^sub>1 ## w\<^sub>1) i = (a\<^sub>2 ## w\<^sub>2) i" for i
using 1 by auto
show "a\<^sub>1 = a\<^sub>2 \ w\<^sub>1 = w\<^sub>2"
proof (intro conjI ext)
show "a\<^sub>1 = a\<^sub>2"
using 2[of "0"] by simp
show "w\<^sub>1 i = w\<^sub>2 i" for i
using 2[of "Suc i"] by simp
qed
next
assume 1: "a\<^sub>1 = a\<^sub>2 \ w\<^sub>1 = w\<^sub>2"
show "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2" using 1 by simp
qed
lemma build_cons[simp]: "(a # u) \ v = a ## u \ v"
proof
fix i
show "((a # u) \ v) i = (a ## u \ v) i"
proof (cases i)
case 0
show ?thesis unfolding 0 by simp
next
case (Suc j)
show ?thesis unfolding Suc by (cases "j < length u", simp+)
qed
qed
lemma build_append[simp]: "(w @ a # u) \ v = w \ a ## u \ v"
unfolding conc_conc[symmetric] by simp
lemma build_first[simp]: "w 0 ## suffix (Suc 0) w = w"
proof
show "(w 0 ## suffix (Suc 0) w) i = w i" for i
by (cases i) simp_all
qed
lemma build_split[intro]: "w = w 0 ## suffix 1 w"
by simp
lemma build_range[simp]: "range (a ## w) = insert a (range w)"
proof safe
show "(a ## w) i \ range w \ (a ## w) i = a" for i
by (cases i) auto
show "a \ range (a ## w)"
proof (rule range_eqI)
show "a = (a ## w) 0" by simp
qed
show "w i \ range (a ## w)" for i
proof (rule range_eqI)
show "w i = (a ## w) (Suc i)" by simp
qed
qed
lemma suffix_singleton_suffix[simp]: "w i ## suffix (Suc i) w = suffix i w"
using suffix_subseq_join[of i "Suc i" w]
by simp
text \Find the first occurrence of a letter from a given set\
lemma word_first_split_set:
assumes "A \ range w \ {}"
obtains u a v where "w = u \ [a] \ v" "A \ set u = {}" "a \ A"
proof -
define i where "i = (LEAST i. w i \ A)"
show ?thesis
proof
show "w = prefix i w \ [w i] \ suffix (Suc i) w"
by simp
show "A \ set (prefix i w) = {}"
apply safe
subgoal premises prems for a
proof -
from prems obtain k where 3: "k < i" "w k = a"
by auto
have 4: "w k \ A"
using not_less_Least 3(1) unfolding i_def .
show ?thesis
using prems(1) 3(2) 4 by auto
qed
done
show "w i \ A"
using LeastI assms(1) unfolding i_def by fast
qed
qed
subsection \The limit set of an $\omega$-word\
text \
The limit set (also called infinity set) of an $\omega$-word
is the set of letters that appear infinitely often in the word.
This set plays an important role in defining acceptance conditions
of $\omega$-automata.
\
definition limit :: "'a word \ 'a set"
where "limit x \ {a . \\<^sub>\n . x n = a}"
lemma limit_iff_frequent: "a \ limit x \ (\\<^sub>\n . x n = a)"
by (simp add: limit_def)
text \
The following is a different way to define the limit,
using the reverse image, making the laws about reverse
image applicable to the limit set.
(Might want to change the definition above?)
\
lemma limit_vimage: "(a \ limit x) = infinite (x -` {a})"
by (simp add: limit_def Inf_many_def vimage_def)
lemma two_in_limit_iff:
"({a, b} \ limit x) =
((\n. x n =a ) \ (\n. x n = a \ (\m>n. x m = b)) \ (\m. x m = b \ (\n>m. x n = a)))"
(is "?lhs = (?r1 \ ?r2 \ ?r3)")
proof
assume lhs: "?lhs"
hence 1: "?r1" by (auto simp: limit_def elim: INFM_EX)
from lhs have "\n. \m>n. x m = b" by (auto simp: limit_def INFM_nat)
hence 2: "?r2" by simp
from lhs have "\m. \n>m. x n = a" by (auto simp: limit_def INFM_nat)
hence 3: "?r3" by simp
from 1 2 3 show "?r1 \ ?r2 \ ?r3" by simp
next
assume "?r1 \ ?r2 \ ?r3"
hence 1: "?r1" and 2: "?r2" and 3: "?r3" by simp+
have infa: "\m. \n\m. x n = a"
proof
fix m
show "\n\m. x n = a" (is "?A m")
proof (induct m)
from 1 show "?A 0" by simp
next
fix m
assume ih: "?A m"
then obtain n where n: "n \ m" "x n = a" by auto
with 2 obtain k where k: "k>n" "x k = b" by auto
with 3 obtain l where l: "l>k" "x l = a" by auto
from n k l have "l \ Suc m" by auto
with l show "?A (Suc m)" by auto
qed
qed
hence infa': "\\<^sub>\n. x n = a" by (simp add: INFM_nat_le)
have "\n. \m>n. x m = b"
proof
fix n
from infa obtain k where k1: "k\n" and k2: "x k = a" by auto
from 2 k2 obtain l where l1: "l>k" and l2: "x l = b" by auto
from k1 l1 have "l > n" by auto
with l2 show "\m>n. x m = b" by auto
qed
hence "\\<^sub>\m. x m = b" by (simp add: INFM_nat)
with infa' show "?lhs" by (auto simp: limit_def)
qed
text \
For $\omega$-words over a finite alphabet, the limit set is
non-empty. Moreover, from some position onward, any such word
contains only letters from its limit set.
\
lemma limit_nonempty:
assumes fin: "finite (range x)"
shows "\a. a \ limit x"
proof -
from fin obtain a where "a \ range x \ infinite (x -` {a})"
by (rule inf_img_fin_domE) auto
hence "a \ limit x"
by (auto simp add: limit_vimage)
thus ?thesis ..
qed
lemmas limit_nonemptyE = limit_nonempty[THEN exE]
lemma limit_inter_INF:
assumes hyp: "limit w \ S \ {}"
shows "\\<^sub>\ n. w n \ S"
proof -
from hyp obtain x where "\\<^sub>\ n. w n = x" and "x \ S"
by (auto simp add: limit_def)
thus ?thesis
by (auto elim: INFM_mono)
qed
text \
The reverse implication is true only if $S$ is finite.
\
lemma INF_limit_inter:
assumes hyp: "\\<^sub>\ n. w n \ S"
and fin: "finite (S \ range w)"
shows "\a. a \ limit w \ S"
proof (rule ccontr)
assume contra: "\(\a. a \ limit w \ S)"
hence "\