author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 64593  50c715579715 
child 67443  3abf6a722518 
permissions  rwrr 
61189  1 
(* 
2 
Author: Stefan Merz 

3 
Author: Salomon Sickert 

4 
Author: Julian Brunner 

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  7 

8 
section \<open>$\omega$words\<close> 

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  11 

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  15 
text \<open>Note: This theory is based on Stefan Merz's work.\<close> 
16 

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  25 
\<close> 
26 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

27 

61189  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  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  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  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, nonempty 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  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  47 
conc :: "['a list, 'a word] \<Rightarrow> 'a word" (infixr "\<frown>" 65) 
48 
where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n  length w)" 

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  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  57 
lemma conc_fst[simp]: "n < length w \<Longrightarrow> (w \<frown> x) n = w!n" 
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  60 
lemma conc_snd[simp]: "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n  length w)" 
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  63 
lemma iter_nth [simp]: "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))" 
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  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  80 
fix a 
81 
assume "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)" 

82 
then obtain i where 1: "a = (w\<^sub>1 \<frown> w\<^sub>2) i" by auto 

83 
then show "a \<in> set w\<^sub>1 \<union> range w\<^sub>2" 

84 
unfolding 1 by (cases "i < length w\<^sub>1") simp_all 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

85 
next 
61189  86 
fix a 
87 
assume a: "a \<in> set w\<^sub>1 \<union> range w\<^sub>2" 

88 
then show "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)" 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

89 
proof 
61189  90 
assume "a \<in> set w\<^sub>1" 
91 
then obtain i where 1: "i < length w\<^sub>1" "a = w\<^sub>1 ! i" 

92 
using in_set_conv_nth by metis 

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  99 
assume "a \<in> range w\<^sub>2" 
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  110 
lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>" 
111 
by (rule ext) (simp add: conc_def mod_geq) 

112 

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  115 

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  119 
definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" ("_ [_ \<rightarrow> _]" 900) 
120 
where "subsequence w i j \<equiv> map w [i..<j]" 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

121 

61189  122 
abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list" 
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  125 
lemma suffix_nth [simp]: "(suffix k x) n = x (k+n)" 
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  128 
lemma suffix_0 [simp]: "suffix 0 x = x" 
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  131 
lemma suffix_suffix [simp]: "suffix m (suffix k x) = suffix (k+m) x" 
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  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  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  140 
lemma subsequence_empty[simp]: "w [i \<rightarrow> j] = [] \<longleftrightarrow> j \<le> i" 
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  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  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  150 
lemma subseq_to_zero[simp]: "w[i\<rightarrow>0] = []" 
151 
by simp 

152 

153 
lemma subseq_to_smaller[simp]: "i\<ge>j \<Longrightarrow> w[i\<rightarrow>j] = []" 

154 
by simp 

155 

156 
lemma subseq_to_Suc[simp]: "i\<le>j \<Longrightarrow> w [i \<rightarrow> Suc j] = w [ i \<rightarrow> j ] @ [w j]" 

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  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  166 
have "w [i \<rightarrow> j] = map w (map (\<lambda>n. n + i) [0..<j  i])" 
167 
unfolding map_add_upt subsequence_def 

168 
using le_add_diff_inverse2[OF True] by force 

169 
also 

170 
have "\<dots> = map (\<lambda>n. w (n + i)) [0..<j  i]" 

171 
unfolding map_map comp_def by blast 

172 
finally 

173 
show ?thesis 

174 
unfolding subsequence_def suffix_def add.commute[of i] by simp 

175 
next 

176 
case False 

177 
then show ?thesis 

178 
by (simp add: subsequence_def) 

179 
qed 

61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

180 

61189  181 
lemma prefix_suffix: "x = prefix n x \<frown> (suffix n x)" 
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  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  189 
show "v = prefix k v \<frown> suffix k v" 
190 
by (rule prefix_suffix) 

191 
show "length (prefix k v) = k" 

192 
by simp 

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  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  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  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  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  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  223 
show "length (prefix n (u \<frown> v)) = length (u @ prefix (n  length u) v)" 
224 
using assms by simp 

225 
fix i 

226 
assume "i < length (prefix n (u \<frown> v))" 

227 
then show "prefix n (u \<frown> v) ! i = (u @ prefix (n  length u) v) ! i" 

228 
by (cases "i < length u") (auto simp: nth_append) 

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  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  238 
show "suffix n (u \<frown> v) i = (drop n u \<frown> v) i" for i 
239 
using assms by (cases "n + i < length u") (auto simp: algebra_simps) 

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  246 
show "suffix n (u \<frown> v) i = suffix (n  length u) v i" for i 
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  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  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  258 
assume ?lhs 
259 
then have 1: "(v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" for i by auto 

260 
show ?rhs 

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  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  269 
show "u\<^sub>1 i = u\<^sub>2 i" for i 
270 
using 1[of "length v\<^sub>1 + i"] assms(1) by simp 

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  273 
assume ?rhs 
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  276 

277 
lemma same_concat_eq[iff]: "u \<frown> v = u \<frown> w \<longleftrightarrow> v = w" 

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  283 
show "(f \<circ> u \<frown> v) i = (map f u \<frown> (f \<circ> v)) i" 
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  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  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  296 
have 2: "(a\<^sub>1 ## w\<^sub>1) i = (a\<^sub>2 ## w\<^sub>2) i" for i 
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  300 
show "a\<^sub>1 = a\<^sub>2" 
301 
using 2[of "0"] by simp 

302 
show "w\<^sub>1 i = w\<^sub>2 i" for i 

303 
using 2[of "Suc i"] by simp 

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  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  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  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  328 
show "(w 0 ## suffix (Suc 0) w) i = w i" for i 
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  331 

332 
lemma build_split[intro]: "w = w 0 ## suffix 1 w" 

333 
by simp 

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  337 
show "(a ## w) i \<notin> range w \<Longrightarrow> (a ## w) i = a" for i 
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  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  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  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  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  361 
show "w = prefix i w \<frown> [w i] \<frown> suffix (Suc i) w" 
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  364 
apply safe 
365 
subgoal premises prems for a 

366 
proof  

367 
from prems obtain k where 3: "k < i" "w k = a" 

368 
by auto 

369 
have 4: "w k \<notin> A" 

370 
using not_less_Least 3(1) unfolding i_def . 

371 
show ?thesis 

372 
using prems(1) 3(2) 4 by auto 

373 
qed 

374 
done 

375 
show "w i \<in> A" 

376 
using LeastI assms(1) unfolding i_def by fast 

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  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  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  388 
\<close> 
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

389 

61189  390 
definition limit :: "'a word \<Rightarrow> 'a set" 
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  393 
lemma limit_iff_frequent: "a \<in> limit x \<longleftrightarrow> (\<exists>\<^sub>\<infinity>n . x n = a)" 
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  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  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  401 
\<close> 
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

402 

61189  403 
lemma limit_vimage: "(a \<in> limit x) = infinite (x ` {a})" 
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  407 
"({a, b} \<subseteq> limit x) = 
408 
((\<exists>n. x n =a ) \<and> (\<forall>n. x n = a \<longrightarrow> (\<exists>m>n. x m = b)) \<and> (\<forall>m. x m = b \<longrightarrow> (\<exists>n>m. x n = a)))" 

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  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 
nonempty. 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  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  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  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  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  484 
assumes hyp: "\<exists>\<^sub>\<infinity> n. w n \<in> S" 
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  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  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  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  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  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  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  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  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  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  565 
\<close> 
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

566 

61189  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  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  627 
\<comment> "the following bound is terrible, but it simplifies the proof" 
61189  628 
from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a" 
64593
50c715579715
reoriented congruence rules in nonexplosive 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  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  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  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  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  670 
assumes fin: "finite (f ` {x})" 
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  674 
assume contra: "\<not> ?thesis" 
61585  675 
\<comment> "hence, every element in the preimage 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  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  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  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  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  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  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  738 
by (metis (mono_tags, lifting) assms(2) 
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  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  750 
assumes "finite (range x)" 
751 
and "finite (range y)" 

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  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  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  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  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_11} (w_1)_{i_1} \ldots (w_1)_{i_21} \ldots 
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

776 
\] 
61189  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  779 
\<close> 
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

780 

61189  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  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  803 
proof (cases m n rule: linorder_cases) 
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  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  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  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  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  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  883 
and k: "n \<in> {idx k ..< idx (Suc k)}" 
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  886 
proof (cases k m rule: linorder_cases) 
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  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  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  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  923 
\<close> 
61178
0b071f72f330
Omega_Words_Fun: Infinite words as functions from nat.
lammich <lammich@in.tum.de>
parents:
diff
changeset

924 

61189  925 
definition merge :: "'a word word \<Rightarrow> nat word \<Rightarrow> 'a word" 
926 
where "merge ws idx \<equiv> \<lambda>n. let i = THE i. n \<in> {idx i ..< idx (Suc i) } in ws i n" 

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  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  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  951 
and n: "n \<in> {idx i ..< idx (Suc i)}" 
952 
shows "merge ws idx (Suc n) = (if Suc n = idx (Suc i) then ws (Suc i) else ws i) (Suc n)" 

953 
proof auto 

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