regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:560712a29a36
+:c4893e84c88e
 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
 Append_rexp2 ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 100) and
 Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
 uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
-tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
+tag_Plus ("+tag _ _" [100, 100] 100) and
-tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
+tag_Plus ("+tag _ _ _" [100, 100, 100] 100) and
 tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
 tag_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
 tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
 tag_Star ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100) and
 tag_eq ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
 Functions are much better supported in Isabelle/HOL, but they still lead to similar
 problems as with graphs.  Composing, for example, two non-deterministic automata in parallel
 requires also the formalisation of disjoint unions. Nipkow \cite{Nipkow98}
 dismisses for this the option of using identities, because it leads according to
-him to ``messy proofs''. He
+him to ``messy proofs''. Since he does not need to define what a regular
-opts for a variant of \eqref{disjointunion} using bit lists, but writes
+language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
 \begin{quote}
 \it%
 \begin{tabular}{@ {}l@ {}p{0.88\textwidth}@ {}}
 `` & All lemmas appear obvious given a picture of the composition of automata\ldots
 \noindent
 That means we eliminated the dependency of @{text "X\<^isub>3"} on the
 right-hand side.  Note we used the abbreviation
 @{text "\<^raw:\ensuremath{\bigplus}>{ATOM c\<^isub>1,\<dots>,ATOM c\<^isub>m}"}
 to stand for a regular expression that matches with every character. In
-our algorithm we are only interested in the existence of such a regular expresion
+our algorithm we are only interested in the existence of such a regular expression
-and not specify it any further.
+and do not specify it any further.
 It can be easily seen that the @{text "Arden"}-operation mimics Arden's
 Lemma on the level of equations. To ensure the non-emptiness condition of
 Arden's Lemma we say that a right-hand side is @{text ardenable} provided
 \noindent
 hold, which shows that @{term "UNIV // \<approx>(lang r)"} must be finite.
 \end{proof}
 \noindent
-Much more interesting, however, are the inductive cases. They seem hard to solve
+Much more interesting, however, are the inductive cases. They seem hard to be solved
 directly. The reader is invited to try.
 In order to see how our proof proceeds consider the following suggestive picture
 taken from Constable et al \cite{Constable00}:
 \end{tabular}}
 \end{equation}
 \noindent
 The relation @{term "\<approx>(lang r)"} partitions the set of all strings into some
-equivalence classes. To show that there are only finitely many of
+equivalence classes. To show that there are only finitely many of them, it
-them, it suffices to show in each induction step the existence of another
+suffices to show in each induction step that another relation, say @{text
-relation, say @{text R}, for which we can show that there are finitely many
+R}, has finitely many equivalence classes and refines @{term "\<approx>(lang r)"}. A
-equivalence classes and which refines @{term "\<approx>(lang r)"}. A relation @{text
+relation @{text "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"}
-"R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text
+provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will
-"R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will rely on some
+rely on some \emph{tagging-functions} defined over strings. Given the
-\emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
+inductive hypothesis, it will be easy to prove that the \emph{range} of
-be easy to prove that the \emph{range} of these tagging-functions is finite.
+these tagging-functions is finite. The range of a function @{text f} is
-The range of a function @{text f} is defined as
+defined as
 \begin{center}
 @{text "range f \<equiv> f ` UNIV"}
 \end{center}
 \noindent
 \noindent
 Chaining Lem.~\ref{finone} and \ref{fintwo} together, means in order to show
 that @{term "UNIV // \<approx>(lang r)"} is finite, we have to construct a tagging-function whose
 range can be shown to be finite and whose tagging-relation refines @{term "\<approx>(lang r)"}.
-Let us attempt the @{const PLUS}-case first.
+Let us attempt the @{const PLUS}-case first. We take as tagging-function
-\begin{proof}[@{const "PLUS"}-Case]
-We take as tagging-function
-%
 \begin{center}
 @{thm tag_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
 \end{center}
 \noindent
-where @{text "A"} and @{text "B"} are some arbitrary languages.
+where @{text "A"} and @{text "B"} are some arbitrary languages. The reason for this choice
-We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
+is that we need to that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. This amounts
-then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
+to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
-@{term "tag_Plus A B"} is a subset of this product set---so finite. It remains to be shown
+@{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. The definition will allow to infer this.
-that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
-showing
+\begin{proof}[@{const "PLUS"}-Case]
-%
+We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite
-\begin{center}
+(UNIV // \<approx>B)"} then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"}
-@{term "tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<longrightarrow> x \<approx>(A \<union> B) y"}
+holds. The range of @{term "tag_Plus A B"} is a subset of this product
-\end{center}
+set---so finite. For the refinement proof-obligation, we know that @{term
-%
+"(\<approx>A `` {x}, \<approx>B `` {x}) = (\<approx>A `` {y}, \<approx>B `` {y})"} holds by assumption. Then
-\noindent
+clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"} hold, as we needed to
-which by unfolding the Myhill-Nerode relation is identical to
+show. Finally we can discharge this case by setting @{text A} to @{term
-%
+"lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
-\begin{equation}\label{pattern}
-@{text "\<forall>z. tag\<^isub>A\<^isub>L\<^isub>T A B x = tag\<^isub>A\<^isub>L\<^isub>T A B y \<and> x @ z \<in> A \<union> B \<longrightarrow> y @ z \<in> A \<union> B"}
-\end{equation}
-%
-\noindent
-since both @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} and @{term "\<approx>(A \<union> B)"} are symmetric. To solve
-\eqref{pattern} we just have to unfold the definition of the tagging-function and analyse
-in which set, @{text A} or @{text B}, the string @{term "x @ z"} is.
-The definition of the tagging-function will give us in each case the
-information to infer that @{text "y @ z \<in> A \<union> B"}.
-Finally we
-can discharge this case by setting @{text A} to @{term "lang r\<^isub>1"} and @{text B} to @{term "lang r\<^isub>2"}.
 \end{proof}
 \noindent
 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,

changeset 183	c4893e84c88e
parent 182	560712a29a36
child 184	2455db3b06ac