1344 (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} |
1344 (first picture) or there is a prefix of @{text x} in @{text A} and the rest is in @{text B} |
1345 (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case |
1345 (second picture). In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. The first case |
1346 we will only go through if we know that @{term "x \<approx>A y"} holds @{text "(*)"}. Because then |
1346 we will only go through if we know that @{term "x \<approx>A y"} holds @{text "(*)"}. Because then |
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"}. |
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"}. |
1348 In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition |
1348 In the second case we only know that @{text "x\<^isub>p"} and @{text "x\<^isub>s"} is a possible partition |
1349 of the string @{text x}. So we have to know that @{text "x\<^isub>p"} is `@{text A}-related' to the |
1349 of the string @{text x}. So we have to know that both @{text "x\<^isub>p"} and the |
1350 corresponding partition @{text "y\<^isub>p"}, repsectively that @{text "x\<^isub>s"} is `@{text B}-related' |
1350 corresponding partition @{text "y\<^isub>p"} are in @{text "A"}, and that @{text "x\<^isub>s"} is `@{text B}-related' |
1351 to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}. |
1351 to @{text "y\<^isub>s"} @{text "(**)"}. From the latter fact we can infer that @{text "y\<^isub>s @ z \<in> B"}. |
1352 Taking the two requirements @{text "(*)"} and @{text "(**)"}, we define the |
1352 Taking the two requirements, @{text "(*)"} and @{text "(**)"}, together we define the |
1353 tagging-function: |
1353 tagging-function as: |
1354 |
1354 |
1355 \begin{center} |
1355 \begin{center} |
1356 @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~ |
1356 @{thm (lhs) tag_Times_def[where ?A="A" and ?B="B"]}~@{text "\<equiv>"}~ |
1357 @{text ""} |
1357 @{text "(\<lbrakk>x\<rbrakk>\<^bsub>\<approx>A\<^esub>, {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x})"} |
1358 \end{center} |
1358 \end{center} |
1359 |
1359 |
1360 \noindent |
1360 \noindent |
1361 With this definition in place, we can discharge the @{const "Times"}-case as follows. |
1361 With this definition in place, we can discharge the @{const "Times"}-case as follows. |
1362 |
1362 |
1372 \end{center} |
1372 \end{center} |
1373 |
1373 |
1374 \noindent |
1374 \noindent |
1375 and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown |
1375 and @{term "x @ z \<in> A \<cdot> B"}, and have to establish @{term "y @ z \<in> A \<cdot> B"}. As shown |
1376 above, there are two cases to be considered (see pictures above). First, |
1376 above, there are two cases to be considered (see pictures above). First, |
1377 there exists a @{text "z\<^isub>p"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}. |
1377 there exists a @{text "z\<^isub>p"} and @{text "z\<^isub>s"} such that @{term "x @ z\<^isub>p \<in> A"} and @{text "z\<^isub>s \<in> B"}. |
1378 By the assumption about @{term "tag_Times A B"} we have |
1378 By the assumption about @{term "tag_Times A B"} we have |
1379 @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode |
1379 @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode |
1380 relation that @{term "y @ z\<^isub>p \<in> A"} holds. Using @{text "z\<^isub>s \<in> B"}, we can conclude 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 |
1381 with @{term "y @ z \<in> A \<cdot> B"}. |
1381 with @{term "y @ z \<in> A \<cdot> B"}. |
1382 |
1382 |
1383 Second there exists a @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with @{term "x\<^isub>p @ x\<^isub>s = x"}, |
1383 Second there exists a partition @{text "x\<^isub>p"} and @{text "x\<^isub>s"} with |
1384 @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have |
1384 @{text "x\<^isub>p \<in> A"} and @{text "x\<^isub>s @ z \<in> B"}. We therefore have |
1385 |
1385 |
1386 \begin{center} |
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})"} |
1387 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | x\<^isub>p \<in> A \<and> (x\<^isub>p, x\<^isub>s) \<in> Partitions x}"} |
1388 \end{center} |
1388 \end{center} |
1389 |
1389 |
1390 \noindent |
1390 \noindent |
1391 and by the assumption about @{term "tag_Times A B"} also |
1391 and by the assumption about @{term "tag_Times A B"} also |
1392 |
1392 |
1393 \begin{center} |
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})"} |
1394 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>B\<^esub> | y\<^isub>p \<in> A \<and> (y\<^isub>p, y\<^isub>s) \<in> Partitions y}"} |
1395 \end{center} |
1395 \end{center} |
1396 |
1396 |
1397 \noindent |
1397 \noindent |
1398 That means there must be a @{text "y\<^isub>p"} and @{text "y\<^isub>s"} |
1398 This means there must be a partition @{text "y\<^isub>p"} and @{text "y\<^isub>s"} |
1399 such that @{text "y\<^isub>p @ y\<^isub>s = y"}. Moreover @{term "\<approx>A `` |
1399 such that @{term "y\<^isub>p \<in> A"} and @{term "\<approx>B `` {x\<^isub>s} = \<approx>B `` |
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 |
1400 {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 |
1401 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 |
1402 obtain @{term "y\<^isub>p \<in> A"} and @{text "y\<^isub>s @ z \<in> B"}, as needed in |
1404 this case. We again can complete the @{const TIMES}-case by setting @{text |
1403 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"}. |
1404 A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}. |
1406 \end{proof} |
1405 \end{proof} |
1407 |
1406 |
1408 \noindent |
1407 \noindent |
1409 The case for @{const Star} is similar to @{const TIMES}, but poses a few |
1408 The case for @{const Star} is similar to @{const TIMES}, but poses a few |
1410 extra challenges. To deal with them we define first the notions of a \emph{string |
1409 extra challenges. To deal with them we define first the notion of a \emph{string |
1411 prefix} and a \emph{strict string prefix}: |
1410 prefix} and a \emph{strict string prefix}: |
1412 |
1411 |
1413 \begin{center} |
1412 \begin{center} |
1414 \begin{tabular}{l} |
1413 \begin{tabular}{l} |
1415 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\ |
1414 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\ |
1416 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"} |
1415 @{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"} |
1417 \end{tabular} |
1416 \end{tabular} |
1418 \end{center} |
1417 \end{center} |
1419 |
1418 |
1420 \noindent |
1419 \noindent |
1421 When we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} |
1420 When we analyse the case of @{text "x @ z"} being an element in @{term "A\<star>"} |
1422 and @{text x} is not the empty string, we have the following picture: |
1421 and @{text x} is not the empty string, we have the following picture: |
1423 |
1422 |
1424 \begin{center} |
1423 \begin{center} |
1425 \scalebox{1}{ |
1424 \scalebox{1}{ |
1426 \begin{tikzpicture} |
1425 \begin{tikzpicture} |
1441 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$) |
1440 ($(xa.north west)+(0em,3ex)$) -- ($(zb.north east)+(0em,3ex)$) |
1442 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}}; |
1441 node[midway, above=0.8em]{@{term "x @ z \<in> A\<star>"}}; |
1443 |
1442 |
1444 \draw[decoration={brace,transform={yscale=3}},decorate] |
1443 \draw[decoration={brace,transform={yscale=3}},decorate] |
1445 ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$) |
1444 ($(za.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$) |
1446 node[midway, below=0.5em]{@{text "x\<^isub>s @ z\<^isub>a \<in> A"}}; |
1445 node[midway, below=0.5em]{@{term "x\<^isub>s @ z\<^isub>a \<in> A"}}; |
1447 |
1446 |
1448 \draw[decoration={brace,transform={yscale=3}},decorate] |
1447 \draw[decoration={brace,transform={yscale=3}},decorate] |
1449 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) |
1448 ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$) |
1450 node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<star>"}}; |
1449 node[midway, below=0.5em]{@{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"}}; |
1451 |
1450 |
1452 \draw[decoration={brace,transform={yscale=3}},decorate] |
1451 \draw[decoration={brace,transform={yscale=3}},decorate] |
1453 ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$) |
1452 ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$) |
1454 node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}}; |
1453 node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}}; |
1455 |
1454 |
1464 @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string |
1463 @{text "x\<^isub>p < x"} and the rest @{term "x\<^isub>s @ z \<in> A\<star>"}. For example the empty string |
1465 @{text "[]"} would do. |
1464 @{text "[]"} would do. |
1466 There are potentially many such prefixes, but there can only be finitely many of them (the |
1465 There are potentially many such prefixes, but there can only be finitely many of them (the |
1467 string @{text x} is finite). Let us therefore choose the longest one and call it |
1466 string @{text x} is finite). Let us therefore choose the longest one and call it |
1468 @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we |
1467 @{text "x\<^bsub>pmax\<^esub>"}. Now for the rest of the string @{text "x\<^isub>s @ z"} we |
1469 know it is in @{term "A\<star>"}. By definition of @{term "A\<star>"}, we can separate |
1468 know it is in @{term "A\<star>"} and it is not the empty string. By Lemma~\ref{langprops}@{text "(i)"}, |
|
1469 we can separate |
1470 this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"} |
1470 this string into two parts, say @{text "a"} and @{text "b"}, such that @{text "a \<in> A"} |
1471 and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"}, |
1471 and @{term "b \<in> A\<star>"}. Now @{text a} must be strictly longer than @{text "x\<^isub>s"}, |
1472 otherwise @{text "x\<^bsub>pmax\<^esub>"} 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} |
1473 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and |
1473 `overlaps' with @{text z}, splitting it into two components @{text "z\<^isub>a"} and |
1474 @{text "z\<^isub>b"}. For this we know that @{text "x\<^isub>s @ 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 |
1475 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"} |
1475 @{term "z\<^isub>b \<in> A\<star>"}. To cut a story short, we have divided @{term "x @ z \<in> A\<star>"} |
1476 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the |
1476 such that we have a string @{text a} with @{text "a \<in> A"} that lies just on the |
1477 `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}. |
1477 `border' of @{text x} and @{text z}. This string is @{text "x\<^isub>s @ z\<^isub>a"}. |
1478 |
1478 |
1479 HERE |
|
1480 |
|
1481 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use |
1479 In order to show that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}, we use |
1482 the following tagging-function: |
1480 the following tagging-function: |
1483 % |
1481 % |
1484 \begin{center} |
1482 \begin{center} |
1485 @{thm tag_Star_def[where ?A="A", THEN meta_eq_app]}\smallskip |
1483 @{thm (lhs) tag_Star_def[where ?A="A", THEN meta_eq_app]}~@{text "\<equiv>"}~ |
|
1484 @{text "{\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^isub>p < x \<and> x\<^isub>p \<in> A\<^isup>\<star> \<and> (x\<^isub>s, x\<^isub>p) \<in> Partitions x}"} |
1486 \end{center} |
1485 \end{center} |
1487 |
1486 |
1488 \begin{proof}[@{const Star}-Case] |
1487 \begin{proof}[@{const Star}-Case] |
1489 If @{term "finite (UNIV // \<approx>A)"} |
1488 If @{term "finite (UNIV // \<approx>A)"} |
1490 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of |
1489 then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of |
1491 @{term "tag_Star A"} is a subset of this set, and therefore finite. |
1490 @{term "tag_Star A"} is a subset of this set, and therefore finite. |
1492 Again we have to show injectivity of this tagging-function as |
1491 Again we have to show under the assumption @{term "x"}~@{term "=(tag_Star A)="}~@{term y} |
1493 % |
1492 that @{term "x @ z \<in> A\<star>"} implies @{term "y @ z \<in> A\<star>"}. |
1494 \begin{center} |
1493 |
1495 @{term "\<forall>z. tag_Star A x = tag_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"} |
|
1496 \end{center} |
|
1497 % |
|
1498 \noindent |
|
1499 We first need to consider the case that @{text x} is the empty string. |
1494 We first need to consider the case that @{text x} is the empty string. |
1500 From the assumption we can infer @{text y} is the empty string and |
1495 From the assumption we can infer @{text y} is the empty string and |
1501 clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty |
1496 clearly have @{term "y @ z \<in> A\<star>"}. In case @{text x} is not the empty |
1502 string, we can divide the string @{text "x @ z"} as shown in the picture |
1497 string, we can divide the string @{text "x @ z"} as shown in the picture |
1503 above. By the tagging-function we have |
1498 above. By the tagging-function and the facts @{text "x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star>"} and @{text "x\<^bsub>pmax\<^esub> < x"}, |
1504 % |
1499 we have |
1505 \begin{center} |
1500 |
1506 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {x - x'} |x'. x' < x \<and> x' \<in> A\<star>})"} |
1501 \begin{center} |
1507 \end{center} |
1502 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | x\<^bsub>pmax\<^esub> < x \<and> x\<^bsub>pmax\<^esub> \<in> A\<^isup>\<star> \<and> (x\<^bsub>pmax\<^esub>, x\<^isub>s) \<in> Partitions x}"} |
1508 % |
1503 \end{center} |
|
1504 |
1509 \noindent |
1505 \noindent |
1510 which by assumption is equal to |
1506 which by assumption is equal to |
1511 % |
1507 |
1512 \begin{center} |
1508 \begin{center} |
1513 @{term "\<approx>A `` {(x - x'\<^isub>m\<^isub>a\<^isub>x)} \<in> ({\<approx>A `` {y - y'} |y'. y' < y \<and> y' \<in> A\<star>})"} |
1509 @{text "\<lbrakk>x\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> \<in> {\<lbrakk>y\<^isub>s\<rbrakk>\<^bsub>\<approx>A\<^esub> | y\<^bsub>p\<^esub> < y \<and> y\<^bsub>p\<^esub> \<in> A\<^isup>\<star> \<and> (y\<^bsub>p\<^esub>, y\<^isub>s) \<in> Partitions y}"} |
1514 \end{center} |
1510 \end{center} |
1515 % |
1511 |
1516 \noindent |
1512 \noindent |
1517 and we know that we have a @{term "y' \<in> A\<star>"} and @{text "y' < y"} |
1513 and we know there exist partitions @{text "y\<^isub>p"} and @{text |
1518 and also know @{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) \<approx>A (y - y')"}. Unfolding the Myhill-Nerode |
1514 "y\<^isub>s"} with @{term "y\<^isub>p \<in> A\<star>"} and also @{term "x\<^isub>s \<approx>A |
1519 relation we know @{term "(y - y') @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}. |
1515 y\<^isub>s"}. Unfolding the Myhill-Nerode relation we know @{term |
1520 Therefore @{term "y' @ ((y - y') @ z\<^isub>a) @ z\<^isub>b \<in> A\<star>"}, which means |
1516 "y\<^isub>s @ z\<^isub>a \<in> A"}. We also know that @{term "z\<^isub>b \<in> A\<star>"}. |
1521 @{term "y @ z \<in> A\<star>"}. As the last step we have to set @{text "A"} to @{term "lang r"} and |
1517 Therefore @{term "y\<^isub>p @ (y\<^isub>s @ z\<^isub>a) @ z\<^isub>b \<in> |
1522 complete the proof. |
1518 A\<star>"}, which means @{term "y @ z \<in> A\<star>"}. As the last step we have to set |
|
1519 @{text "A"} to @{term "lang r"} and complete the proof. |
1523 \end{proof} |
1520 \end{proof} |
1524 *} |
1521 *} |
1525 |
1522 |
1526 section {* Second Part based on Partial Derivatives *} |
1523 section {* Second Part based on Partial Derivatives *} |
1527 |
1524 |