64   tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and

    64   tag_Times ("\<times>tag _ _" [100, 100] 100) and

    65   tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and

    65   tag_Times ("\<times>tag _ _ _" [100, 100, 100] 100) and

    66   tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and

    66   tag_Star ("\<star>tag _" [100] 100) and

    67   tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and

    67   tag_Star ("\<star>tag _ _" [100, 100] 100) and

   643                & & \mbox{}\hspace{3mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}

   643                & & \mbox{}\hspace{10mm}@{text "+ (X\<^isub>3, ATOM c\<^isub>1) + \<dots> + (X\<^isub>3, ATOM c\<^isub>m)"}

   759     @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m})) + \<dots> "}\\

   759     @{text "(X\<^isub>1, TIMES (ATOM d\<^isub>1) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m})) + \<dots> "}\\

   761      @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}))"}

   761      @{text "\<dots> + (X\<^isub>1, TIMES (ATOM d\<^isub>n) (STAR \<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}))"}

   769   @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}"} 

   769   @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>, ATOM c\<^isub>m}"} 

  1144   R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. A

  1144   R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. 

  1145   relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}

  1145 

  1146   provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will

  1146   \begin{dfntn}

  1147   A relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}

  1148   provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. 

  1149   \end{dfntn}

  1150 

  1151   \noindent

  1152   For constructing @{text R} will

  1238   is that we need to that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. This amounts

  1244   is that we need to establish that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. 

  1239   to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption

  1245   This amounts to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption

  1240   @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. The definition will allow to infer this.

  1246   @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. As we shall see, this definition will 

  1247   provide us just the right assumptions in order to get the proof through.

  1248   clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"} hold, as we needed to

  1255   clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"}, as we needed to

  1253 

  1260   \noindent

  1254   \noindent

  1261   The @{const TIMES}-case is slightly more complicated. We first prove the

  1255   The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,

  1262   following lemma, which will aid the refinement-proofs.

  1256   they are slightly more complicated. In the @{const TIMES}-case we essentially have

  1263 

  1257   to be able to infer that 

  1264   \begin{lmm}\label{refinement}

  1258   %

  1265   The relation @{text "\<^raw:$\threesim$>\<^bsub>tag\<^esub>"} refines @{term "\<approx>A"}, provided for

  1259   \begin{center}

  1266   all strings @{text x}, @{text y} and @{text z} we have \mbox{@{text "x \<^raw:$\threesim$>\<^bsub>tag\<^esub> y"}}

  1260   @{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}

  1267   and @{term "x @ z \<in> A"} imply @{text "y @ z \<in> A"}.

  1261   \end{center}

  1268   \end{lmm}

  1262   %

  1269 

  1263   \noindent

  1270 

  1264   using the information given by the appropriate tagging-function. The complication 

  1271   \noindent

  1265   is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}

  1272   We therefore can clean information from how the strings @{text "x @ z"} are in @{text A}

  1266   (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the

  1273   and construct appropriate tagging-functions to infer that @{term "y @ z \<in> A"}.

  1267   notions of \emph{string prefixes} 

  1274   For the @{const Times}-case we additionally need the notion of the set of all

  1268   %

  1275   possible partitions of a string

  1269   \begin{center}

  1276 

  1270   \begin{tabular}{l}

  1277   \begin{equation}

  1271   @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\

  1278   @{thm Partitions_def}

  1272   @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}

  1279   \end{equation}

  1273   \end{tabular}

  1280 

  1274   \end{center}

  1275   %

  1276   \noindent

  1277   and \emph{string subtraction}:

  1278 

  1279   \noindent

  1280   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings. 

  1281   

  1287   \scalebox{0.9}{

  1286   \scalebox{1}{

  1289     \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };

  1288     \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };

  1290     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };

  1289     \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z\<^isub>p"}\hspace{0.6em}$ };

  1290     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z\<^isub>s"}\hspace{2.6em}$  };

  1291 

  1292     \draw[decoration={brace,transform={yscale=3}},decorate]

  1293            (x.north west) -- ($(za.north west)+(0em,0em)$)

  1294                node[midway, above=0.5em]{@{text x}};

  1295 

  1296     \draw[decoration={brace,transform={yscale=3}},decorate]

  1297            ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)

  1298                node[midway, above=0.5em]{@{text z}};

  1299 

  1300     \draw[decoration={brace,transform={yscale=3}},decorate]

  1301            ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)

  1302                node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};

  1303 

  1304     \draw[decoration={brace,transform={yscale=3}},decorate]

  1305            ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)

  1306                node[midway, below=0.5em]{@{text "x @ z\<^isub>p \<in> A"}};

  1307 

  1308     \draw[decoration={brace,transform={yscale=3}},decorate]

  1309            ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)

  1310                node[midway, below=0.5em]{@{text "z\<^isub>s \<in> B"}};

  1311   \end{tikzpicture}}

  1312   \\[2mm]

  1313   \scalebox{1}{

  1314   \begin{tikzpicture}

  1315     \node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x\<^isub>p"}\hspace{3em}$ };

  1316     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x\<^isub>s"}\hspace{0.2em}$ };

  1307                node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};

  1333                node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> B"}};

  1311                node[midway, below=0.5em]{@{term "x' \<in> A"}};

  1337                node[midway, below=0.5em]{@{term "x\<^isub>p \<in> A"}};

  1313   \\

  1339   \end{tabular}

  1314   \scalebox{0.9}{

  1340   \end{center}

  1315   \begin{tikzpicture}

  1341   %

  1316     \node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };

  1342   \noindent

  1317     \node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };

  1343   Either @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} 

  1318     \node[draw,minimum height=3.8ex, right=-0.03em of za] (zza) { $\hspace{2.6em}@{text "z - z'"}\hspace{2.6em}$  };

  1344   (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} 

  1319 

  1345   (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case

  1320     \draw[decoration={brace,transform={yscale=3}},decorate]

  1346   we will only go through if we know that  @{term "x \<approx>A y"} holds @{text "(*)"}. Because then 

  1321            (x.north west) -- ($(za.north west)+(0em,0em)$)

  1347   we can infer from @{term "x @ z\<^isub>p \<in> A"} that @{term "y @ z\<^isub>p \<in> A"} holds for all @{text "z\<^isub>p"}.

  1322                node[midway, above=0.5em]{@{text x}};

  1348   In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition

  1323 

  1349   of the string @{text x}. So we have to know that @{text "x\<^isub>p"} is `@{text A}-related' to the

  1324     \draw[decoration={brace,transform={yscale=3}},decorate]

  1350   corresponding partition @{text "y\<^isub>p"}, repsectively that @{text "x\<^isub>s"} is `@{text B}-related' 

  1325            ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)

  1351   to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}.

  1326                node[midway, above=0.5em]{@{text z}};

  1352   Taking the two requirements @{text "(*)"} and @{text "(**)"}, we define the

  1327 

  1353   tagging-function:

  1328     \draw[decoration={brace,transform={yscale=3}},decorate]

  1354 

  1329            ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)

  1355   \begin{center}

  1330                node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};

  1356   @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~

  1331 

  1357   @{text ""}

  1332     \draw[decoration={brace,transform={yscale=3}},decorate]

  1358   \end{center}

  1333            ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)

  1359 

  1334                node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};

  1360   \noindent

  1335 

  1361   With this definition in place, we can discharge the @{const "Times"}-case as follows.

  1336     \draw[decoration={brace,transform={yscale=3}},decorate]

  1362 

  1337            ($(zza.south east)+(0em,0ex)$) -- ($(za.south east)+(0em,0ex)$)

  1338                node[midway, below=0.5em]{@{text "(z - z') \<in> B"}};

  1339   \end{tikzpicture}}

  1340   \end{tabular}

  1341   \end{center}

  1342   %

  1343   \noindent

  1344   Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),

  1345   or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).

  1346   In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the 

  1347   following tagging-function

  1348   %

  1349   \begin{center}

  1350   @{thm tag_Times_def[where ?A="A" and ?B="B", THEN meta_eq_app]}

  1351   \end{center}

  1352 

  1353   \noindent

  1354   with the idea that in the first split we have to make sure that @{text "(x - x') @ z"}

  1355   is in the language @{text B}.

  1361   We have to show injectivity of this tagging-function as

  1368   By Lemma \ref{refinement} we know

  1362   %

  1369 

  1363   \begin{center}

  1370   \begin{center}

  1364   @{term "\<forall>z. tag_Times A B x = tag_Times A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}

  1371    @{term "tag_Times A B x = tag_Times A B y"}

  1365   \end{center}

  1372   \end{center}

  1366   %

  1373 

  1367   \noindent

  1374   \noindent

  1368   There are two cases to be considered (see pictures above). First, there exists 

  1375   and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown

  1369   a @{text "x'"} such that

  1376   above, there are two cases to be considered (see pictures above). First, 

  1370   @{text "x' \<in> A"}, @{text "x' \<le> x"} and @{text "(x - x') @ z \<in> B"} hold. We therefore have

  1377   there exists a @{text "z\<^isub>p"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}.

  1371   %

  1372   \begin{center}

  1373   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A})"}

  1374   \end{center}

  1375   %

  1376   \noindent

  1377   and by the assumption about @{term "tag_Times A B"} also 

  1378   %

  1379   \begin{center}

  1380   @{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}

  1381   \end{center}

  1382   %

  1383   \noindent

  1384   That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and 

  1385   @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that

  1386   @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode

  1387   relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we

  1388   have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore

  1389   @{term "y @ z \<in> A \<cdot> B"}, as needed in this case.

  1390 

  1391   Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.

  1394   relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case

  1380   relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude in this case

  1395   with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const TIMES}-case

  1381   with @{term "y @ z \<in> A \<cdot> B"}.

  1396   by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}. 

  1382 

  1383   Second there exists a @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{term "x\<^isub>p @ x\<^isub>s = x"},

  1384   @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have

  1385   

  1386   \begin{center}

  1387   @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) | x\<^isub>p x\<^isub>s. (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"}

  1388   \end{center}

  1389   

  1390   \noindent

  1391   and by the assumption about @{term "tag_Times A B"} also 

  1392   

  1393   \begin{center}

  1394   @{term "(\<approx>A `` {x\<^isub>p}, \<approx>B `` {x\<^isub>s}) \<in> ({(\<approx>A `` {y\<^isub>p}, \<approx>B `` {y\<^isub>s}) | y\<^isub>p y\<^isub>s. (y\<^isub>p, y\<^isub>s) \<in> Partitions y})"}

  1395   \end{center}

  1396   

  1397   \noindent

  1398   That means there must be a @{text "y\<^isub>p"} and @{text "y\<^isub>s"}

  1399   such that @{text "y\<^isub>p @ y\<^isub>s = y"}. Moreover @{term "\<approx>A ``

  1400   {x\<^isub>p} = \<approx>A `` {y\<^isub>p}"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B ``

  1401   {y\<^isub>s}"}. Unfolding the Myhill-Nerode relation and together with the

  1402   facts that @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}, we

  1403   @{term "y\<^isub>p \<in> A"} and have @{text "y\<^isub>s @ z \<in> B"}, as needed in

  1404   this case.  We again can complete the @{const TIMES}-case by setting @{text

  1405   A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.

  1398   

  1407 

  1399   \noindent

  1408   \noindent

  1400   The case for @{const Star} is similar to @{const TIMES}, but poses a few extra challenges. When

  1409   The case for @{const Star} is similar to @{const TIMES}, but poses a few

  1401   we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 

  1410   extra challenges.  To deal with them we define first the notions of a \emph{string

  1402   empty string, we 

  1411   prefix} and a \emph{strict string prefix}:

  1403   have the following picture:

  1412 

  1404   %

  1413   \begin{center}

  1405   \begin{center}

  1414   \begin{tabular}{l}

  1406   \scalebox{0.7}{

  1415   @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\

  1416   @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}

  1417   \end{tabular}

  1418   \end{center}

  1419 

  1420   \noindent

  1421   When we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"}

  1422   and @{text x} is not the empty string, we have the following picture:

  1423 

  1424   \begin{center}

  1425   \scalebox{1}{

  1408     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{4em}$ };

  1427     \node[draw,minimum height=3.8ex] (xa) { $\hspace{4em}@{text "x\<^bsub>pmax\<^esub>"}\hspace{4em}$ };

  1409     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x - x'\<^isub>m\<^isub>a\<^isub>x"}\hspace{0.5em}$ };

  1428     \node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.5em}@{text "x\<^bsub>s\<^esub>"}\hspace{0.5em}$ };

  1427                node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"}};

  1446                node[midway, below=0.5em]{@{text "x\<^isub>s @ z\<^isub>a \<in> A"}};

  1431                node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};

  1450                node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<star>"}};

  1439                node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};

  1458                node[midway, below=0.5em]{@{term "x\<^isub>s @ z \<in> A\<star>"}};

  1444   We can find a strict prefix @{text "x'"} of @{text x} such that @{term "x' \<in> A\<star>"},

  1463   We can find a strict prefix @{text "x\<^isub>p"} of @{text x} such that @{term "x\<^isub>p \<in> A\<star>"},

  1445   @{text "x' < x"} and the rest @{term "(x - x') @ z \<in> A\<star>"}. For example the empty string 

  1464   @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string 

  1449   @{text "x'\<^isub>m\<^isub>a\<^isub>x"}. Now for the rest of the string @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z"} we

  1468   @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we

  1452   and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x - x'\<^isub>m\<^isub>a\<^isub>x"},

  1471   and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"},

  1453   otherwise @{text "x'\<^isub>m\<^isub>a\<^isub>x"} is not the longest prefix. That means @{text a}

  1472   otherwise @{text "x\<^bsub>pmax\<^esub>"} is not the longest prefix. That means @{text a}

  1455    @{text "z\<^isub>b"}. For this we know that @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a \<in> A"} and

  1474    @{text "z\<^isub>b"}. For this we know that @{text "x\<^isub>s @ z\<^isub>a \<in> A"} and

  1458   `border' of @{text x} and @{text z}. This string is @{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z\<^isub>a"}.

  1477   `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}.

  1478 

  1479   HERE