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