summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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>