65 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
65 tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and |
66 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and |
66 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and |
67 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and |
67 tag_str_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and |
68 tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and |
68 tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and |
69 Delta ("\<Delta>'(_')") and |
69 Delta ("\<Delta>'(_')") and |
70 nullable ("\<delta>'(_')") |
70 nullable ("\<delta>'(_')") and |
|
71 Cons ("_ :: _" [100, 100] 100) |
71 |
72 |
72 lemma meta_eq_app: |
73 lemma meta_eq_app: |
73 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" |
74 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x" |
74 by auto |
75 by auto |
75 |
76 |
387 is defined as the union over all powers, namely @{thm star_def}. In the paper |
388 is defined as the union over all powers, namely @{thm star_def}. In the paper |
388 we will make use of the following properties of these constructions. |
389 we will make use of the following properties of these constructions. |
389 |
390 |
390 \begin{prpstn}\label{langprops}\mbox{}\\ |
391 \begin{prpstn}\label{langprops}\mbox{}\\ |
391 \begin{tabular}{@ {}ll} |
392 \begin{tabular}{@ {}ll} |
392 (i) & @{thm star_cases} \\ |
393 (i) & @{thm star_unfold_left} \\ |
393 (ii) & @{thm[mode=IfThen] pow_length}\\ |
394 (ii) & @{thm[mode=IfThen] pow_length}\\ |
394 (iii) & @{thm conc_Union_left} \\ |
395 (iii) & @{thm conc_Union_left} \\ |
395 \end{tabular} |
396 \end{tabular} |
396 \end{prpstn} |
397 \end{prpstn} |
397 |
398 |
1096 |
1097 |
1097 \noindent |
1098 \noindent |
1098 Much more interesting, however, are the inductive cases. They seem hard to solve |
1099 Much more interesting, however, are the inductive cases. They seem hard to solve |
1099 directly. The reader is invited to try. |
1100 directly. The reader is invited to try. |
1100 |
1101 |
1101 Constable et al \cite{Constable00} give the following suggestive picture about |
1102 In order how to see how our first proof proceeds we use the following suggestive picture |
1102 equivalence classes: |
1103 from Constable et al \cite{Constable00}: |
|
1104 |
|
1105 \begin{center} |
|
1106 \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c} |
|
1107 \begin{tikzpicture}[scale=1] |
|
1108 %Circle |
|
1109 \draw[thick] (0,0) circle (1.1); |
|
1110 \end{tikzpicture} |
|
1111 & |
|
1112 \begin{tikzpicture}[scale=1] |
|
1113 %Circle |
|
1114 \draw[thick] (0,0) circle (1.1); |
|
1115 %Main rays |
|
1116 \foreach \a in {0, 90,...,359} |
|
1117 \draw[very thick] (0, 0) -- (\a:1.1); |
|
1118 \foreach \a / \l in {45/1, 135/2, 225/3, 315/4} |
|
1119 \draw (\a: 0.65) node {$a_\l$}; |
|
1120 \end{tikzpicture} |
|
1121 & |
|
1122 \begin{tikzpicture}[scale=1] |
|
1123 %Circle |
|
1124 \draw[thick] (0,0) circle (1.1); |
|
1125 %Main rays |
|
1126 \foreach \a in {0, 45,...,359} |
|
1127 \draw[very thick] (0, 0) -- (\a:1.1); |
|
1128 \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2} |
|
1129 \draw (\a: 0.77) node {$a_{\l}$}; |
|
1130 \end{tikzpicture}\\ |
|
1131 @{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"} |
|
1132 \end{tabular} |
|
1133 \end{center} |
1103 |
1134 |
1104 Our first proof will rely on some |
1135 Our first proof will rely on some |
1105 \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will |
1136 \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will |
1106 be easy to prove that the \emph{range} of these tagging-functions is finite. |
1137 be easy to prove that the \emph{range} of these tagging-functions is finite. |
1107 The range of a function @{text f} is defined as |
1138 The range of a function @{text f} is defined as |