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