src/HOL/Library/Omega_Words_Fun.thy
changeset 67443 3abf6a722518
parent 64593 50c715579715
child 68977 c73ca43087c0
     1.1 --- a/src/HOL/Library/Omega_Words_Fun.thy	Tue Jan 16 09:12:16 2018 +0100
     1.2 +++ b/src/HOL/Library/Omega_Words_Fun.thy	Tue Jan 16 09:30:00 2018 +0100
     1.3 @@ -529,20 +529,20 @@
     1.4  proof -
     1.5    have "\<exists>k. range (suffix k x) \<subseteq> limit x"
     1.6    proof -
     1.7 -    \<comment> "The set of letters that are not in the limit is certainly finite."
     1.8 +    \<comment> \<open>The set of letters that are not in the limit is certainly finite.\<close>
     1.9      from fin have "finite (range x - limit x)"
    1.10        by simp
    1.11 -    \<comment> "Moreover, any such letter occurs only finitely often"
    1.12 +    \<comment> \<open>Moreover, any such letter occurs only finitely often\<close>
    1.13      moreover
    1.14      have "\<forall>a \<in> range x - limit x. finite (x -` {a})"
    1.15        by (auto simp add: limit_vimage)
    1.16 -    \<comment> "Thus, there are only finitely many occurrences of such letters."
    1.17 +    \<comment> \<open>Thus, there are only finitely many occurrences of such letters.\<close>
    1.18      ultimately have "finite (UN a : range x - limit x. x -` {a})"
    1.19        by (blast intro: finite_UN_I)
    1.20 -    \<comment> "Therefore these occurrences are within some initial interval."
    1.21 +    \<comment> \<open>Therefore these occurrences are within some initial interval.\<close>
    1.22      then obtain k where "(UN a : range x - limit x. x -` {a}) \<subseteq> {..<k}"
    1.23        by (blast dest: finite_nat_bounded)
    1.24 -    \<comment> "This is just the bound we are looking for."
    1.25 +    \<comment> \<open>This is just the bound we are looking for.\<close>
    1.26      hence "\<forall>m. k \<le> m \<longrightarrow> x m \<in> limit x"
    1.27        by (auto simp add: limit_vimage)
    1.28      hence "range (suffix k x) \<subseteq> limit x"
    1.29 @@ -624,11 +624,11 @@
    1.30      fix a assume a: "a \<in> set w"
    1.31      then obtain k where k: "k < length w \<and> w!k = a"
    1.32        by (auto simp add: set_conv_nth)
    1.33 -    \<comment> "the following bound is terrible, but it simplifies the proof"
    1.34 +    \<comment> \<open>the following bound is terrible, but it simplifies the proof\<close>
    1.35      from nempty k have "\<forall>m. w\<^sup>\<omega> ((Suc m)*(length w) + k) = a"
    1.36        by (simp add: mod_add_left_eq [symmetric])
    1.37      moreover
    1.38 -    \<comment> "why is the following so hard to prove??"
    1.39 +    \<comment> \<open>why is the following so hard to prove??\<close>
    1.40      have "\<forall>m. m < (Suc m)*(length w) + k"
    1.41      proof
    1.42        fix m
    1.43 @@ -672,10 +672,10 @@
    1.44    shows "\<exists>a \<in> (f -` {x}). a \<in> limit w"
    1.45  proof (rule ccontr)
    1.46    assume contra: "\<not> ?thesis"
    1.47 -  \<comment> "hence, every element in the pre-image occurs only finitely often"
    1.48 +  \<comment> \<open>hence, every element in the pre-image occurs only finitely often\<close>
    1.49    then have "\<forall>a \<in> (f -` {x}). finite {n. w n = a}"
    1.50      by (simp add: limit_def Inf_many_def)
    1.51 -  \<comment> "so there are only finitely many occurrences of any such element"
    1.52 +  \<comment> \<open>so there are only finitely many occurrences of any such element\<close>
    1.53    with fin have "finite (\<Union> a \<in> (f -` {x}). {n. w n = a})"
    1.54      by auto
    1.55    \<comment> \<open>these are precisely those positions where $x$ occurs in $f \circ w$\<close>
    1.56 @@ -683,7 +683,7 @@
    1.57    have "(\<Union> a \<in> (f -` {x}). {n. w n = a}) = {n. f(w n) = x}"
    1.58      by auto
    1.59    ultimately
    1.60 -  \<comment> "so $x$ can occur only finitely often in the translated word"
    1.61 +  \<comment> \<open>so $x$ can occur only finitely often in the translated word\<close>
    1.62    have "finite {n. f(w n) = x}"
    1.63      by simp
    1.64    \<comment> \<open>\ldots\ which yields a contradiction\<close>