# HG changeset patch
# User wenzelm
# Date 1442497686 -7200
# Node ID 9583ddfc07b37f3f0cd5d76b5b74b65aa59da6cd
# Parent  b34551d94934adc719c980f57efe8736e0c4df68
isabelle update_cartouches;
tuned proofs;
tuned whitespace;

diff -r b34551d94934 -r 9583ddfc07b3 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Thu Sep 17 15:47:24 2015 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Thu Sep 17 15:48:06 2015 +0200
@@ -1,13 +1,20 @@
-(* Author: Stefan Merz
-  Additions by Salomon Sickert, Julian Brunner, Peter Lammich.
+(*
+    Author:     Stefan Merz
+    Author:     Salomon Sickert
+    Author:     Julian Brunner
+    Author:     Peter Lammich
 *)
-section {* $\omega$-words *}
+
+section \<open>$\omega$-words\<close>
+
 theory Omega_Words_Fun
-imports "~~/src/HOL/Library/Infinite_Set"
+
+imports Infinite_Set
 begin
-text {* Note: This theory is based on Stefan Merz's work. *}
 
-text {*
+text \<open>Note: This theory is based on Stefan Merz's work.\<close>
+
+text \<open>
   Automata recognize languages, which are sets of words. For the
   theory of $\omega$-automata, we are mostly interested in
   $\omega$-words, but it is sometimes useful to reason about
@@ -15,25 +22,26 @@
   lets us benefit from the existing library. Other formalizations
   could be investigated, such as representing words as functions
   whose domains are initial intervals of the natural numbers.
-*}
+\<close>
+
 
-subsection {* Type declaration and elementary operations *}
+subsection \<open>Type declaration and elementary operations\<close>
 
-text {*
+text \<open>
   We represent $\omega$-words as functions from the natural numbers
   to the alphabet type. Other possible formalizations include
   a coinductive definition or a uniform encoding of finite and
   infinite words, as studied by M\"uller et al.
-*}
+\<close>
 
 type_synonym
   'a word = "nat \<Rightarrow> 'a"
 
-text {*
+text \<open>
   We can prefix a finite word to an $\omega$-word, and a way
   to obtain an $\omega$-word from a finite, non-empty word is by
   $\omega$-iteration.
-*}
+\<close>
 
 definition
   conc :: "['a list, 'a word] \<Rightarrow> 'a word"    (infixr "conc" 65)
@@ -50,20 +58,16 @@
 lemma conc_empty[simp]: "[] \<frown> w = w"
   unfolding conc_def by auto
 
-lemma conc_fst[simp]:
-  "n < length w \<Longrightarrow> (w \<frown> x) n = w!n"
-by (simp add: conc_def)
+lemma conc_fst[simp]: "n < length w \<Longrightarrow> (w \<frown> x) n = w!n"
+  by (simp add: conc_def)
 
-lemma conc_snd[simp]:
-  "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n - length w)"
-by (simp add: conc_def)
+lemma conc_snd[simp]: "\<not>(n < length w) \<Longrightarrow> (w \<frown> x) n = x (n - length w)"
+  by (simp add: conc_def)
 
-lemma iter_nth [simp]:
-  "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))"
-by (simp add: iter_def)
+lemma iter_nth [simp]: "0 < length w \<Longrightarrow> w\<^sup>\<omega> n = w!(n mod (length w))"
+  by (simp add: iter_def)
 
-lemma conc_conc[simp]:
-  "u \<frown> v \<frown> w = (u @ v) \<frown> w" (is "?lhs = ?rhs")
+lemma conc_conc[simp]: "u \<frown> v \<frown> w = (u @ v) \<frown> w" (is "?lhs = ?rhs")
 proof
   fix n
   have u: "n < length u \<Longrightarrow> ?lhs n = ?rhs n"
@@ -77,24 +81,27 @@
 
 lemma range_conc[simp]: "range (w\<^sub>1 \<frown> w\<^sub>2) = set w\<^sub>1 \<union> range w\<^sub>2"
 proof (intro equalityI subsetI)
-  case (goal1 a)
-  obtain i where 1: "a = (w\<^sub>1 \<frown> w\<^sub>2) i" using goal1 by auto
-  show ?case unfolding 1 by (cases "i < length w\<^sub>1", simp+)
+  fix a
+  assume "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)"
+  then obtain i where 1: "a = (w\<^sub>1 \<frown> w\<^sub>2) i" by auto
+  then show "a \<in> set w\<^sub>1 \<union> range w\<^sub>2"
+    unfolding 1 by (cases "i < length w\<^sub>1") simp_all
 next
-  case (goal2 a)
-  show ?case
-  using goal2
+  fix a
+  assume a: "a \<in> set w\<^sub>1 \<union> range w\<^sub>2"
+  then show "a \<in> range (w\<^sub>1 \<frown> w\<^sub>2)"
   proof
-    case (goal1)
-    obtain i where 1: "i < length w\<^sub>1" "a = w\<^sub>1 ! i" using goal1 in_set_conv_nth by metis
+    assume "a \<in> set w\<^sub>1"
+    then obtain i where 1: "i < length w\<^sub>1" "a = w\<^sub>1 ! i"
+      using in_set_conv_nth by metis
     show ?thesis
     proof
       show "a = (w\<^sub>1 \<frown> w\<^sub>2) i" using 1 by auto
       show "i \<in> UNIV" by rule
     qed
   next
-    case (goal2)
-    obtain i where 1: "a = w\<^sub>2 i" using goal2 by auto
+    assume "a \<in> range w\<^sub>2"
+    then obtain i where 1: "a = w\<^sub>2 i" by auto
     show ?thesis
     proof
       show "a = (w\<^sub>1 \<frown> w\<^sub>2) (length w\<^sub>1 + i)" using 1 by simp
@@ -104,114 +111,107 @@
 qed
 
 
-lemma iter_unroll:
-  "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
-by (rule ext, simp add: conc_def mod_geq)
+lemma iter_unroll: "0 < length w \<Longrightarrow> w\<^sup>\<omega> = w \<frown> w\<^sup>\<omega>"
+  by (rule ext) (simp add: conc_def mod_geq)
+
 
 subsection \<open>Subsequence, Prefix, and Suffix\<close>
-definition
-  suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
+
+definition suffix :: "[nat, 'a word] \<Rightarrow> 'a word"
   where "suffix k x \<equiv> \<lambda>n. x (k+n)"
 
-definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list" 
-  ("_ [_ \<rightarrow> _]" 900) 
-where
-  "subsequence w i j \<equiv> map w [i..<j]"
+definition subsequence :: "'a word \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a list"  ("_ [_ \<rightarrow> _]" 900)
+  where "subsequence w i j \<equiv> map w [i..<j]"
 
-abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list" 
-where
-  "prefix n w \<equiv> subsequence w 0 n"
+abbreviation prefix :: "nat \<Rightarrow> 'a word \<Rightarrow> 'a list"
+  where "prefix n w \<equiv> subsequence w 0 n"
 
-lemma suffix_nth [simp]:
-  "(suffix k x) n = x (k+n)"
-by (simp add: suffix_def)
+lemma suffix_nth [simp]: "(suffix k x) n = x (k+n)"
+  by (simp add: suffix_def)
 
-lemma suffix_0 [simp]:
-  "suffix 0 x = x"
-by (simp add: suffix_def)
+lemma suffix_0 [simp]: "suffix 0 x = x"
+  by (simp add: suffix_def)
 
-lemma suffix_suffix [simp]:
-  "suffix m (suffix k x) = suffix (k+m) x"
-by (rule ext, simp add: suffix_def add.assoc)
+lemma suffix_suffix [simp]: "suffix m (suffix k x) = suffix (k+m) x"
+  by (rule ext) (simp add: suffix_def add.assoc)
 
-lemma subsequence_append:
-  "prefix (i + j) w = prefix i w @ (w [i \<rightarrow> i + j])"
+lemma subsequence_append: "prefix (i + j) w = prefix i w @ (w [i \<rightarrow> i + j])"
   unfolding map_append[symmetric] upt_add_eq_append[OF le0] subsequence_def ..
 
-lemma subsequence_drop[simp]:
-  "drop i (w [j \<rightarrow> k]) = w [j + i \<rightarrow> k]"
+lemma subsequence_drop[simp]: "drop i (w [j \<rightarrow> k]) = w [j + i \<rightarrow> k]"
   by (simp add: subsequence_def drop_map)
 
-lemma subsequence_empty[simp]:
-  "w [i \<rightarrow> j] = [] \<longleftrightarrow> j \<le> i"
-  by (auto simp add: subsequence_def) 
+lemma subsequence_empty[simp]: "w [i \<rightarrow> j] = [] \<longleftrightarrow> j \<le> i"
+  by (auto simp add: subsequence_def)
 
-lemma subsequence_length[simp]:
-  "length (subsequence w i j) = j - i"
+lemma subsequence_length[simp]: "length (subsequence w i j) = j - i"
   by (simp add: subsequence_def)
 
-lemma subsequence_nth[simp]: 
-  "k < j - i \<Longrightarrow> (w [i \<rightarrow> j]) ! k = w (i + k)"
+lemma subsequence_nth[simp]: "k < j - i \<Longrightarrow> (w [i \<rightarrow> j]) ! k = w (i + k)"
   unfolding subsequence_def
   by auto
 
-lemma subseq_to_zero[simp]: "w[i\<rightarrow>0] = []" by simp
-lemma subseq_to_smaller[simp]: "i\<ge>j \<Longrightarrow> w[i\<rightarrow>j] = []" by simp
-lemma subseq_to_Suc[simp]: "i\<le>j \<Longrightarrow> w [i \<rightarrow> Suc j] = w [ i \<rightarrow> j ] @ [w j]" 
+lemma subseq_to_zero[simp]: "w[i\<rightarrow>0] = []"
+  by simp
+
+lemma subseq_to_smaller[simp]: "i\<ge>j \<Longrightarrow> w[i\<rightarrow>j] = []"
+  by simp
+
+lemma subseq_to_Suc[simp]: "i\<le>j \<Longrightarrow> w [i \<rightarrow> Suc j] = w [ i \<rightarrow> j ] @ [w j]"
   by (auto simp: subsequence_def)
 
 lemma subsequence_singleton[simp]: "w [i \<rightarrow> Suc i] = [w i]"
   by (auto simp: subsequence_def)
 
 
-lemma subsequence_prefix_suffix:
-  "prefix (j - i) (suffix i w) = w [i \<rightarrow> j]"
+lemma subsequence_prefix_suffix: "prefix (j - i) (suffix i w) = w [i \<rightarrow> j]"
 proof (cases "i \<le> j")
   case True
-    have "w [i \<rightarrow> j] = map w (map (\<lambda>n. n + i) [0..<j - i])"
-      unfolding map_add_upt subsequence_def 
-      using le_add_diff_inverse2[OF True] by force
-    also
-    have "\<dots> = map (\<lambda>n. w (n + i)) [0..<j - i]"
-      unfolding map_map comp_def by blast
-    finally
-    show ?thesis 
-      unfolding subsequence_def suffix_def add.commute[of i] by simp
-qed (simp add: subsequence_def)
+  have "w [i \<rightarrow> j] = map w (map (\<lambda>n. n + i) [0..<j - i])"
+    unfolding map_add_upt subsequence_def
+    using le_add_diff_inverse2[OF True] by force
+  also
+  have "\<dots> = map (\<lambda>n. w (n + i)) [0..<j - i]"
+    unfolding map_map comp_def by blast
+  finally
+  show ?thesis
+    unfolding subsequence_def suffix_def add.commute[of i] by simp
+next
+  case False
+  then show ?thesis
+    by (simp add: subsequence_def)
+qed
 
-lemma prefix_suffix: 
-  "x = prefix n x \<frown> (suffix n x)"
-  by (rule ext, simp add: subsequence_def conc_def)
+lemma prefix_suffix: "x = prefix n x \<frown> (suffix n x)"
+  by (rule ext) (simp add: subsequence_def conc_def)
 
 declare prefix_suffix[symmetric, simp]
 
 
-lemma word_split:
-  obtains v\<^sub>1 v\<^sub>2
-  where "v = v\<^sub>1 \<frown> v\<^sub>2" "length v\<^sub>1 = k"
+lemma word_split: obtains v\<^sub>1 v\<^sub>2 where "v = v\<^sub>1 \<frown> v\<^sub>2" "length v\<^sub>1 = k"
 proof
-  show "v = prefix k v \<frown> suffix k v" using prefix_suffix by this
-  show "length (prefix k v) = k" by simp
+  show "v = prefix k v \<frown> suffix k v"
+    by (rule prefix_suffix)
+  show "length (prefix k v) = k"
+    by simp
 qed
 
 
 lemma set_subsequence[simp]: "set (w[i\<rightarrow>j]) = w`{i..<j}"
   unfolding subsequence_def by auto
 
-lemma subsequence_take[simp]:
-  "take i (w [j \<rightarrow> k]) = w [j \<rightarrow> min (j + i) k]"
+lemma subsequence_take[simp]: "take i (w [j \<rightarrow> k]) = w [j \<rightarrow> min (j + i) k]"
   by (simp add: subsequence_def take_map min_def)
 
-lemma subsequence_shift[simp]:
-  "(suffix i w) [j \<rightarrow> k] = w [i + j \<rightarrow> i + k]"
+lemma subsequence_shift[simp]: "(suffix i w) [j \<rightarrow> k] = w [i + j \<rightarrow> i + k]"
   by (metis add_diff_cancel_left subsequence_prefix_suffix suffix_suffix)
 
 lemma suffix_subseq_join[simp]: "i \<le> j \<Longrightarrow> v [i \<rightarrow> j] \<frown> suffix j v = suffix i v"
-  by (metis (no_types, lifting) Nat.add_0_right le_add_diff_inverse prefix_suffix 
+  by (metis (no_types, lifting) Nat.add_0_right le_add_diff_inverse prefix_suffix
     subsequence_shift suffix_suffix)
 
 lemma prefix_conc_fst[simp]:
-  assumes "j \<le> length w" 
+  assumes "j \<le> length w"
   shows "prefix j (w \<frown> w') = take j w"
 proof -
   have "\<forall>i < j. (prefix j (w \<frown> w')) ! i = (take j w) ! i"
@@ -219,95 +219,98 @@
   thus ?thesis
     by (simp add: assms list_eq_iff_nth_eq min.absorb2)
 qed
- 
+
 lemma prefix_conc_snd[simp]:
   assumes "n \<ge> length u"
   shows "prefix n (u \<frown> v) = u @ prefix (n - length u) v"
 proof (intro nth_equalityI allI impI)
-  case (goal1)
-  show ?case using assms by simp
-next
-  case (goal2 i)
-  show ?case using goal2 
-    by (cases "i < length u")
-       (auto simp: nth_append)
-
+  show "length (prefix n (u \<frown> v)) = length (u @ prefix (n - length u) v)"
+    using assms by simp
+  fix i
+  assume "i < length (prefix n (u \<frown> v))"
+  then show "prefix n (u \<frown> v) ! i = (u @ prefix (n - length u) v) ! i"
+    by (cases "i < length u") (auto simp: nth_append)
 qed
 
-lemma prefix_conc_length[simp]:
-  "prefix (length w) (w \<frown> w') = w"
+lemma prefix_conc_length[simp]: "prefix (length w) (w \<frown> w') = w"
   by simp
 
 lemma suffix_conc_fst[simp]:
   assumes "n \<le> length u"
   shows "suffix n (u \<frown> v) = drop n u \<frown> v"
 proof
-  case (goal1 i)
-  show ?case using assms by (cases "n + i < length u", auto simp: algebra_simps)
+  show "suffix n (u \<frown> v) i = (drop n u \<frown> v) i" for i
+    using assms by (cases "n + i < length u") (auto simp: algebra_simps)
 qed
 
 lemma suffix_conc_snd[simp]:
   assumes "n \<ge> length u"
   shows "suffix n (u \<frown> v) = suffix (n - length u) v"
 proof
-  case (goal1 i)
-  show ?case using assms by simp
+  show "suffix n (u \<frown> v) i = suffix (n - length u) v i" for i
+    using assms by simp
 qed
 
-lemma suffix_conc_length[simp]:
-  "suffix (length w) (w \<frown> w') = w'"
+lemma suffix_conc_length[simp]: "suffix (length w) (w \<frown> w') = w'"
   unfolding conc_def by force
 
 lemma concat_eq[iff]:
   assumes "length v\<^sub>1 = length v\<^sub>2"
   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"
+  (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  case (goal1)
-  have 1: "\<And> i. (v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" using goal1 by auto
-  show ?case
+  assume ?lhs
+  then have 1: "(v\<^sub>1 \<frown> u\<^sub>1) i = (v\<^sub>2 \<frown> u\<^sub>2) i" for i by auto
+  show ?rhs
   proof (intro conjI ext nth_equalityI allI impI)
-    show "length v\<^sub>1 = length v\<^sub>2" using assms(1) by this
+    show "length v\<^sub>1 = length v\<^sub>2" by (rule assms(1))
   next
     fix i
     assume 2: "i < length v\<^sub>1"
     have 3: "i < length v\<^sub>2" using assms(1) 2 by simp
     show "v\<^sub>1 ! i = v\<^sub>2 ! i" using 1[of i] 2 3 by simp
   next
-    fix i
-    show "u\<^sub>1 i = u\<^sub>2 i" using 1[of "length v\<^sub>1 + i"] assms(1) by simp
+    show "u\<^sub>1 i = u\<^sub>2 i" for i
+      using 1[of "length v\<^sub>1 + i"] assms(1) by simp
   qed
 next
-  case (goal2)
-  show ?case using goal2 by simp
+  assume ?rhs
+  then show ?lhs by simp
 qed
-lemma same_concat_eq[iff]: "u \<frown> v = u \<frown> w \<longleftrightarrow> v = w" by simp
+
+lemma same_concat_eq[iff]: "u \<frown> v = u \<frown> w \<longleftrightarrow> v = w"
+  by simp
 
 lemma comp_concat[simp]: "f \<circ> u \<frown> v = map f u \<frown> (f \<circ> v)"
 proof
   fix i
-  show "(f \<circ> u \<frown> v) i = (map f u \<frown> (f \<circ> v)) i" by (cases "i < length u", simp+)
+  show "(f \<circ> u \<frown> v) i = (map f u \<frown> (f \<circ> v)) i"
+    by (cases "i < length u") simp_all
 qed
 
+
 subsection \<open>Prepending\<close>
 
-primrec build :: "'a \<Rightarrow> 'a word \<Rightarrow> 'a word" (infixr "##" 65)
+primrec build :: "'a \<Rightarrow> 'a word \<Rightarrow> 'a word"  (infixr "##" 65)
   where "(a ## w) 0 = a" | "(a ## w) (Suc i) = w i"
 
 lemma build_eq[iff]: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2 \<longleftrightarrow> a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
 proof
   assume 1: "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2"
-  have 2: "\<And> i. (a\<^sub>1 ## w\<^sub>1) i = (a\<^sub>2 ## w\<^sub>2) i" using 1 by auto
+  have 2: "(a\<^sub>1 ## w\<^sub>1) i = (a\<^sub>2 ## w\<^sub>2) i" for i
+    using 1 by auto
   show "a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
   proof (intro conjI ext)
-    show "a\<^sub>1 = a\<^sub>2" using 2[of "0"] by simp
-  next
-    fix i
-    show "w\<^sub>1 i = w\<^sub>2 i" using 2[of "Suc i"] by simp
+    show "a\<^sub>1 = a\<^sub>2"
+      using 2[of "0"] by simp
+    show "w\<^sub>1 i = w\<^sub>2 i" for i
+      using 2[of "Suc i"] by simp
   qed
 next
   assume 1: "a\<^sub>1 = a\<^sub>2 \<and> w\<^sub>1 = w\<^sub>2"
   show "a\<^sub>1 ## w\<^sub>1 = a\<^sub>2 ## w\<^sub>2" using 1 by simp
 qed
+
 lemma build_cons[simp]: "(a # u) \<frown> v = a ## u \<frown> v"
 proof
   fix i
@@ -320,89 +323,93 @@
     show ?thesis unfolding Suc by (cases "j < length u", simp+)
   qed
 qed
+
 lemma build_append[simp]: "(w @ a # u) \<frown> v = w \<frown> a ## u \<frown> v"
   unfolding conc_conc[symmetric] by simp
+
 lemma build_first[simp]: "w 0 ## suffix (Suc 0) w = w"
 proof
-  fix i
-  show "(w 0 ## suffix (Suc 0) w) i = w i" by (cases i, simp+)
+  show "(w 0 ## suffix (Suc 0) w) i = w i" for i
+    by (cases i) simp_all
 qed
-lemma build_split[intro]: "w = w 0 ## suffix 1 w" by simp
+
+lemma build_split[intro]: "w = w 0 ## suffix 1 w"
+  by simp
+
 lemma build_range[simp]: "range (a ## w) = insert a (range w)"
 proof safe
-  fix i
-  show "(a ## w) i \<notin> range w \<Longrightarrow> (a ## w) i = a" by (cases i, auto)
-next
+  show "(a ## w) i \<notin> range w \<Longrightarrow> (a ## w) i = a" for i
+    by (cases i) auto
   show "a \<in> range (a ## w)"
   proof (rule range_eqI)
     show "a = (a ## w) 0" by simp
   qed
-next
-  fix i
-  show "w i \<in> range (a ## w)"
+  show "w i \<in> range (a ## w)" for i
   proof (rule range_eqI)
     show "w i = (a ## w) (Suc i)" by simp
   qed
 qed
 
 lemma suffix_singleton_suffix[simp]: "w i ## suffix (Suc i) w = suffix i w"
-  using suffix_subseq_join[of i "Suc i" w] 
+  using suffix_subseq_join[of i "Suc i" w]
   by simp
 
 text \<open>Find the first occurrence of a letter from a given set\<close>
 lemma word_first_split_set:
   assumes "A \<inter> range w \<noteq> {}"
-  obtains u a v
-  where "w = u \<frown> [a] \<frown> v" "A \<inter> set u = {}" "a \<in> A"
+  obtains u a v where "w = u \<frown> [a] \<frown> v" "A \<inter> set u = {}" "a \<in> A"
 proof -
   def i \<equiv> "LEAST i. w i \<in> A"
   show ?thesis
   proof
-    show "w = prefix i w \<frown> [w i] \<frown> suffix (Suc i) w" by simp
+    show "w = prefix i w \<frown> [w i] \<frown> suffix (Suc i) w"
+      by simp
     show "A \<inter> set (prefix i w) = {}"
-    proof safe
-      case (goal1 a)
-      obtain k where 3: "k < i" "w k = a" using goal1(2) by auto
-      have 4: "w k \<notin> A" using not_less_Least 3(1) unfolding i_def by this
-      show ?case using goal1(1) 3(2) 4 by auto
-    qed
-    show "w i \<in> A" using LeastI assms(1) unfolding i_def by fast
+      apply safe
+      subgoal premises prems for a
+      proof -
+        from prems obtain k where 3: "k < i" "w k = a"
+          by auto
+        have 4: "w k \<notin> A"
+          using not_less_Least 3(1) unfolding i_def .
+        show ?thesis
+          using prems(1) 3(2) 4 by auto
+      qed
+      done
+    show "w i \<in> A"
+      using LeastI assms(1) unfolding i_def by fast
   qed
 qed
 
 
+subsection \<open>The limit set of an $\omega$-word\<close>
 
-subsection {* The limit set of an $\omega$-word *}
-
-text {*
+text \<open>
   The limit set (also called infinity set) of an $\omega$-word
   is the set of letters that appear infinitely often in the word.
   This set plays an important role in defining acceptance conditions
   of $\omega$-automata.
-*}
+\<close>
 
-definition
-  limit :: "'a word \<Rightarrow> 'a set"
-  where "limit x \<equiv> { a . \<exists>\<^sub>\<infinity>n . x n = a }"
+definition limit :: "'a word \<Rightarrow> 'a set"
+  where "limit x \<equiv> {a . \<exists>\<^sub>\<infinity>n . x n = a}"
 
-lemma limit_iff_frequent:
-  "(a \<in> limit x) = (\<exists>\<^sub>\<infinity>n . x n = a)"
-by (simp add: limit_def)
+lemma limit_iff_frequent: "a \<in> limit x \<longleftrightarrow> (\<exists>\<^sub>\<infinity>n . x n = a)"
+  by (simp add: limit_def)
 
-text {*
+text \<open>
   The following is a different way to define the limit,
   using the reverse image, making the laws about reverse
-  image applicable to the limit set. 
+  image applicable to the limit set.
   (Might want to change the definition above?)
-*}
+\<close>
 
-lemma limit_vimage:
-  "(a \<in> limit x) = infinite (x -` {a})"
-by (simp add: limit_def Inf_many_def vimage_def)
+lemma limit_vimage: "(a \<in> limit x) = infinite (x -` {a})"
+  by (simp add: limit_def Inf_many_def vimage_def)
 
 lemma two_in_limit_iff:
-  "({a,b} \<subseteq> limit x) = 
-   ((\<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)))"
+  "({a, b} \<subseteq> limit x) =
+    ((\<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)))"
   (is "?lhs = (?r1 \<and> ?r2 \<and> ?r3)")
 proof
   assume lhs: "?lhs"
@@ -444,18 +451,18 @@
   with infa' show "?lhs" by (auto simp: limit_def)
 qed
 
-text {*
+text \<open>
   For $\omega$-words over a finite alphabet, the limit set is
   non-empty. Moreover, from some position onward, any such word
   contains only letters from its limit set.
-*}
+\<close>
 
 lemma limit_nonempty:
   assumes fin: "finite (range x)"
   shows "\<exists>a. a \<in> limit x"
 proof -
   from fin obtain a where "a \<in> range x \<and> infinite (x -` {a})"
-    by (rule inf_img_fin_domE, auto)
+    by (rule inf_img_fin_domE) auto
   hence "a \<in> limit x"
     by (auto simp add: limit_vimage)
   thus ?thesis ..
@@ -473,12 +480,13 @@
     by (auto elim: INFM_mono)
 qed
 
-text {*
+text \<open>
   The reverse implication is true only if $S$ is finite.
-*}
+\<close>
 
 lemma INF_limit_inter:
-  assumes hyp: "\<exists>\<^sub>\<infinity> n. w n \<in>  S" and fin: "finite (S \<inter> range w)"
+  assumes hyp: "\<exists>\<^sub>\<infinity> n. w n \<in>  S"
+    and fin: "finite (S \<inter> range w)"
   shows  "\<exists>a. a \<in> limit w \<inter> S"
 proof (rule ccontr)
   assume contra: "\<not>(\<exists>a. a \<in> limit w \<inter> S)"
@@ -498,8 +506,7 @@
 lemma fin_ex_inf_eq_limit: "finite A \<Longrightarrow> (\<exists>\<^sub>\<infinity>i. w i \<in> A) \<longleftrightarrow> limit w \<inter> A \<noteq> {}"
   by (metis INF_limit_inter equals0D finite_Int limit_inter_INF)
 
-lemma limit_in_range_suffix:
-  "limit x \<subseteq> range (suffix k x)"
+lemma limit_in_range_suffix: "limit x \<subseteq> range (suffix k x)"
 proof
   fix a
   assume "a \<in> limit x"
@@ -517,8 +524,7 @@
 
 lemmas limit_in_range_suffixD = limit_in_range_suffix[THEN subsetD]
 
-lemma limit_subset:
-  "limit f \<subseteq> f ` {n..}"
+lemma limit_subset: "limit f \<subseteq> f ` {n..}"
   using limit_in_range_suffix[of f n] unfolding suffix_def by auto
 
 theorem limit_is_suffix:
@@ -557,13 +563,12 @@
 theorems limit_is_suffixE = limit_is_suffix[THEN exE]
 
 
-text {*
+text \<open>
   The limit set enjoys some simple algebraic laws with respect
   to concatenation, suffixes, iteration, and renaming.
-*}
+\<close>
 
-theorem limit_conc [simp]:
-  "limit (w \<frown> x) = limit x"
+theorem limit_conc [simp]: "limit (w \<frown> x) = limit x"
 proof (auto)
   fix a assume a: "a \<in> limit (w \<frown> x)"
   have "\<forall>m. \<exists>n. m<n \<and> x n = a"
@@ -597,8 +602,7 @@
     by (simp add: limit_def Inf_many_def)
 qed
 
-theorem limit_suffix [simp]: 
-  "limit (suffix n x) = limit x"
+theorem limit_suffix [simp]: "limit (suffix n x) = limit x"
 proof -
   have "x = (prefix n x) \<frown> (suffix n x)"
     by (simp add: prefix_suffix)
@@ -625,8 +629,7 @@
     then obtain k where k: "k < length w \<and> w!k = a"
       by (auto simp add: set_conv_nth)
     -- "the following bound is terrible, but it simplifies the proof"
-    from nempty k
-    have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
+    from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
       by (simp add: mod_add_left_eq)
     moreover
     -- "why is the following so hard to prove??"
@@ -659,26 +662,27 @@
     by (simp add: limit_iff_frequent)
 qed
 
-text {*
+text \<open>
   The converse relation is not true in general: $f(a)$ can be in the
   limit of $f \circ w$ even though $a$ is not in the limit of $w$.
   However, @{text limit} commutes with renaming if the function is
   injective. More generally, if $f(a)$ is the image of only finitely
   many elements, some of these must be in the limit of $w$.
-*}
+\<close>
 
 lemma limit_o_inv:
-  assumes fin: "finite (f -` {x})" and x: "x \<in> limit (f \<circ> w)"
+  assumes fin: "finite (f -` {x})"
+    and x: "x \<in> limit (f \<circ> w)"
   shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
 proof (rule ccontr)
-  assume contra: "\<not>(\<exists>a \<in> (f -` {x}). a \<in> limit w)"
+  assume contra: "\<not> ?thesis"
   -- "hence, every element in the pre-image occurs only finitely often"
   then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
     by (simp add: limit_def Inf_many_def)
   -- "so there are only finitely many occurrences of any such element"
   with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
     by auto
-  -- {* these are precisely those positions where $x$ occurs in $f \circ w$ *}
+  -- \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
   moreover
   have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
     by auto
@@ -686,7 +690,7 @@
   -- "so $x$ can occur only finitely often in the translated word"
   have "finite {n. f(w n) = x}"
     by simp
-  -- {* \ldots\ which yields a contradiction *}
+  -- \<open>\ldots\ which yields a contradiction\<close>
   with x show "False"
     by (simp add: limit_def Inf_many_def)
 qed
@@ -697,7 +701,6 @@
 proof
   show "f ` limit w \<subseteq> limit (f \<circ> w)"
     by auto
-next
   show "limit (f \<circ> w) \<subseteq> f ` limit w"
   proof
     fix x
@@ -718,7 +721,7 @@
 proof -
   from fin obtain k where k_def: "limit w = range (suffix k w)"
     using limit_is_suffix by blast
-  have "\<And>k'. w (k + k') \<notin> S"
+  have "w (k + k') \<notin> S" for k'
     using hyp unfolding k_def suffix_def image_def by blast
   thus ?thesis
     unfolding MOST_nat_le using le_Suc_ex by blast
@@ -730,16 +733,16 @@
   assumes "limit r = range (suffix i r)"
   assumes "j\<ge>i"
   shows "limit r = range (suffix j r)"
-  (is "?lhs = ?rhs")
+    (is "?lhs = ?rhs")
 proof -
   have "?lhs = range (suffix i r)"
     using assms by simp
   moreover
   have "\<dots> \<supseteq> ?rhs" using \<open>j\<ge>i\<close>
-    by (metis (mono_tags, lifting) assms(2) image_subsetI le_Suc_ex range_eqI suffix_def suffix_suffix)
+    by (metis (mono_tags, lifting) assms(2)
+        image_subsetI le_Suc_ex range_eqI suffix_def suffix_suffix)
   moreover
-  have "\<dots> \<supseteq> ?lhs" 
-    using limit_in_range_suffix .
+  have "\<dots> \<supseteq> ?lhs" by (rule limit_in_range_suffix)
   ultimately
   show "?lhs = ?rhs"
     by (metis antisym_conv limit_in_range_suffix)
@@ -748,15 +751,15 @@
 text \<open>For two finite sequences, we can find a common suffix index such
   that the limits can be represented as these suffixes' ranges.\<close>
 lemma common_range_limit:
-  assumes "finite (range x)" and "finite (range y)"
-  obtains i where "limit x = range (suffix i x)"  
+  assumes "finite (range x)"
+    and "finite (range y)"
+  obtains i where "limit x = range (suffix i x)"
     and "limit y = range (suffix i y)"
 proof -
-  obtain i j where 
-        1: "limit x = range (suffix i x)"
+  obtain i j where 1: "limit x = range (suffix i x)"
     and 2: "limit y = range (suffix j y)"
     using assms limit_is_suffix by metis
-  have "limit x = range (suffix (max i j) x)"  
+  have "limit x = range (suffix (max i j) x)"
     and "limit y = range (suffix (max i j) y)"
     using limit_range_suffix_incr[OF 1] limit_range_suffix_incr[OF 2]
     by auto
@@ -765,9 +768,9 @@
 qed
 
 
-subsection {* Index sequences and piecewise definitions *}
+subsection \<open>Index sequences and piecewise definitions\<close>
 
-text {*
+text \<open>
   A word can be defined piecewise: given a sequence of words $w_0, w_1, \ldots$
   and a strictly increasing sequence of integers $i_0, i_1, \ldots$ where $i_0=0$,
   a single word is obtained by concatenating subwords of the $w_n$ as given by
@@ -775,12 +778,11 @@
   \[
     (w_0)_{i_0} \ldots (w_0)_{i_1-1} (w_1)_{i_1} \ldots (w_1)_{i_2-1} \ldots
   \]
-  We prepare the field by proving some trivial facts about such sequences of 
+  We prepare the field by proving some trivial facts about such sequences of
   indexes.
-*}
+\<close>
 
-definition
-  idx_sequence :: "nat word \<Rightarrow> bool"
+definition idx_sequence :: "nat word \<Rightarrow> bool"
   where "idx_sequence idx \<equiv> (idx 0 = 0) \<and> (\<forall>n. idx n < idx (Suc n))"
 
 lemma idx_sequence_less:
@@ -800,7 +802,7 @@
 
 lemma idx_sequence_inj:
   assumes iseq: "idx_sequence idx"
-  and eq: "idx m = idx n"
+    and eq: "idx m = idx n"
   shows "m = n"
 proof (rule nat_less_cases)
   assume "n<m"
@@ -822,7 +824,7 @@
 
 lemma idx_sequence_mono:
   assumes iseq: "idx_sequence idx"
-  and m: "m \<le> n"
+    and m: "m \<le> n"
   shows "idx m \<le> idx n"
 proof (cases "m=n")
   case True
@@ -837,11 +839,11 @@
   thus ?thesis by simp
 qed
 
-text {*
+text \<open>
   Given an index sequence, every natural number is contained in the
   interval defined by two adjacent indexes, and in fact this interval
   is determined uniquely.
-*}
+\<close>
 
 lemma idx_sequence_idx:
   assumes "idx_sequence idx"
@@ -882,8 +884,8 @@
 
 lemma idx_sequence_interval_unique:
   assumes iseq: "idx_sequence idx"
-  and k: "n \<in> {idx k ..< idx (Suc k) }"
-  and m: "n \<in> {idx m ..< idx (Suc m) }"
+    and k: "n \<in> {idx k ..< idx (Suc k)}"
+    and m: "n \<in> {idx m ..< idx (Suc m)}"
   shows "k = m"
 proof (rule nat_less_cases)
   assume "k < m"
@@ -919,19 +921,17 @@
   with iseq show "k = y" by (auto elim: idx_sequence_interval_unique)
 qed
 
-text {*
+text \<open>
   Now we can define the piecewise construction of a word using
   an index sequence.
-*}
+\<close>
 
-definition
-  merge :: "['a word word, nat word] \<Rightarrow> 'a word"
-  where "merge ws idx \<equiv>
-           \<lambda> n. let i = THE i. n \<in> {idx i ..< idx (Suc i) } in ws i n"
+definition merge :: "'a word word \<Rightarrow> nat word \<Rightarrow> 'a word"
+  where "merge ws idx \<equiv> \<lambda>n. let i = THE i. n \<in> {idx i ..< idx (Suc i) } in ws i n"
 
 lemma merge:
   assumes idx: "idx_sequence idx"
-  and n: "n \<in> {idx i ..< idx (Suc i) }"
+    and n: "n \<in> {idx i ..< idx (Suc i)}"
   shows "merge ws idx n = ws i n"
 proof -
   from n have "(THE k. n \<in> {idx k ..< idx (Suc k) }) = i"
@@ -945,20 +945,19 @@
   shows "merge ws idx 0 = ws 0 0"
 proof (rule merge[OF idx])
   from idx have "idx 0 < idx (Suc 0)"
-    by (unfold idx_sequence_def, blast)
+    unfolding idx_sequence_def by blast
   with idx show "0 \<in> {idx 0 ..< idx (Suc 0)}"
     by (simp add: idx_sequence_def)
 qed
 
 lemma merge_Suc:
   assumes idx: "idx_sequence idx"
-  and n: "n \<in> {idx i ..< idx (Suc i) }"
-  shows "merge ws idx (Suc n) = 
-         (if Suc n = idx (Suc i) then ws (Suc i) else ws i) (Suc n)"
-proof (auto)
+    and n: "n \<in> {idx i ..< idx (Suc i)}"
+  shows "merge ws idx (Suc n) = (if Suc n = idx (Suc i) then ws (Suc i) else ws i) (Suc n)"
+proof auto
   assume eq: "Suc n = idx (Suc i)"
   from idx have "idx (Suc i) < idx (Suc(Suc i))"
-    by (unfold idx_sequence_def, blast)
+    unfolding idx_sequence_def by blast
   with eq idx show "merge ws idx (idx (Suc i)) = ws (Suc i) (idx (Suc i))"
     by (simp add: merge)
 next