regexp: comparison Journal/Paper.thy

equal deleted inserted replaced

-:7743d2ad71d1
+:61d0a412a3ae
 (*<*)
 theory Paper
-imports "../Derivs" "~~/src/HOL/Library/LaTeXsugar"
+imports "../Closure"
 begin
 declare [[show_question_marks = false]]
 consts
 pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
 Suc ("_+1" [100] 100) and
 quotient ("_ \<^raw:\ensuremath{\!\sslash\!}> _" [90, 90] 90) and
 REL ("\<approx>") and
 UPLUS ("_ \<^raw:\ensuremath{\uplus}> _" [90, 90] 90) and
-L ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
+L_rexp ("\<^raw:\ensuremath{\cal{L}}>'(_')" [0] 101) and
 Lam ("\<lambda>'(_')" [100] 100) and
 Trn ("'(_, _')" [100, 100] 100) and
 EClass ("\<lbrakk>_\<rbrakk>\<^bsub>_\<^esub>" [100, 100] 100) and
 transition ("_ \<^raw:\ensuremath{\stackrel{\text{>_\<^raw:}}{\Longmapsto}}> _" [100, 100, 100] 100) and
 Setalt ("\<^raw:\ensuremath{\bigplus}>_" [1000] 999) and
 tag_str_ALT ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [100, 100, 100] 100) and
 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
 tag_str_SEQ ("tag\<^isub>S\<^isub>E\<^isub>Q _ _ _" [100, 100, 100] 100) and
 tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _" [100] 100) and
 tag_str_STAR ("tag\<^isub>S\<^isub>T\<^isub>A\<^isub>R _ _" [100, 100] 100)
 lemma meta_eq_app:
 shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
 by auto
+(* THEOREMS *)
+notation (Rule output)
+"==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+syntax (Rule output)
+"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+notation (Axiom output)
+"Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+notation (IfThen output)
+"==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+"_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+notation (IfThenNoBox output)
+"==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+"_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+"_asm" :: "prop \<Rightarrow> asms" ("_")
 (*>*)
 section {* Introduction *}
 text {*
+\noindent
 Regular languages are an important and well-understood subject in Computer
 Science, with many beautiful theorems and many useful algorithms. There is a
 wide range of textbooks on this subject, many of which are aimed at students
 and contain very detailed `pencil-and-paper' proofs
 (e.g.~\cite{Kozen97}). It seems natural to exercise theorem provers by
 In case of graphs and matrices, this means we have to build our own
 reasoning infrastructure for them, as neither Isabelle/HOL nor HOL4 nor
 HOLlight support them with libraries. Even worse, reasoning about graphs and
 matrices can be a real hassle in HOL-based theorem provers.  Consider for
 example the operation of sequencing two automata, say $A_1$ and $A_2$, by
-connecting the accepting states of $A_1$ to the initial state of $A_2$:\\[-5.5mm]
+connecting the accepting states of $A_1$ to the initial state of $A_2$:
 %
 \begin{center}
 \begin{tabular}{ccc}
 \begin{tikzpicture}[scale=0.8]
 %\draw[step=2mm] (-1,-1) grid (1,1);
 Isabelle/HOL, but take a different approach to regular
 languages. Instead of defining a regular language as one where there exists
 an automaton that recognises all strings of the language, we define a
 regular language as:
-\begin{definition}
+\begin{dfntn}
 A language @{text A} is \emph{regular}, provided there is a regular expression that matches all
 strings of @{text "A"}.
-\end{definition}
+\end{dfntn}
 \noindent
 The reason is that regular expressions, unlike graphs, matrices and functions, can
 be easily defined as inductive datatype. Consequently a corresponding reasoning
 infrastructure comes for free. This has recently been exploited in HOL4 with a formalisation
 text {*
 Strings in Isabelle/HOL are lists of characters with the \emph{empty string}
 being represented by the empty list, written @{term "[]"}.  \emph{Languages}
 are sets of strings. The language containing all strings is written in
 Isabelle/HOL as @{term "UNIV::string set"}. The concatenation of two languages
-is written @{term "A ;; B"} and a language raised to the power @{text n} is written
+is written @{term "A \<cdot> B"} and a language raised to the power @{text n} is written
 @{term "A \<up> n"}. They are defined as usual
 \begin{center}
 @{thm Seq_def[THEN eq_reflection, where A1="A" and B1="B"]}
 \hspace{7mm}
 \noindent
 where @{text "@"} is the list-append operation. The Kleene-star of a language @{text A}
 is defined as the union over all powers, namely @{thm Star_def}. In the paper
 we will make use of the following properties of these constructions.
-\begin{proposition}\label{langprops}\mbox{}\\
+\begin{prpstn}\label{langprops}\mbox{}\\
 \begin{tabular}{@ {}ll}
 (i)   & @{thm star_cases}     \\
 (ii)  & @{thm[mode=IfThen] pow_length}\\
 (iii) & @{thm seq_Union_left} \\
 \end{tabular}
-\end{proposition}
+\end{prpstn}
 \noindent
 In @{text "(ii)"} we use the notation @{term "length s"} for the length of a
 string; this property states that if \mbox{@{term "[] \<notin> A"}} then the lengths of
 the strings in @{term "A \<up> (Suc n)"} must be longer than @{text n}.  We omit
 as \mbox{@{text "{y | y \<approx> x}"}}.
 Central to our proof will be the solution of equational systems
 involving equivalence classes of languages. For this we will use Arden's Lemma \cite{Brzozowski64},
-which solves equations of the form @{term "X = A ;; X \<union> B"} provided
+which solves equations of the form @{term "X = A \<cdot> X \<union> B"} provided
 @{term "[] \<notin> A"}. However we will need the following `reverse'
-version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A ;; X"} to
+version of Arden's Lemma (`reverse' in the sense of changing the order of @{term "A \<cdot> X"} to
-\mbox{@{term "X ;; A"}}).
+\mbox{@{term "X \<cdot> A"}}).
-\begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
+\begin{lmm}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
 If @{thm (prem 1) arden} then
 @{thm (lhs) arden} if and only if
 @{thm (rhs) arden}.
-\end{lemma}
+\end{lmm}
 \begin{proof}
 For the right-to-left direction we assume @{thm (rhs) arden} and show
 that @{thm (lhs) arden} holds. From Prop.~\ref{langprops}@{text "(i)"}
-we have @{term "A\<star> = {[]} \<union> A ;; A\<star>"},
+we have @{term "A\<star> = {[]} \<union> A \<cdot> A\<star>"},
-which is equal to @{term "A\<star> = {[]} \<union> A\<star> ;; A"}. Adding @{text B} to both
+which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
-sides gives @{term "B ;; A\<star> = B ;; ({[]} \<union> A\<star> ;; A)"}, whose right-hand side
+sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
-is equal to @{term "(B ;; A\<star>) ;; A \<union> B"}. This completes this direction.
+is equal to @{term "(B \<cdot> A\<star>) \<cdot> A \<union> B"}. This completes this direction.
 For the other direction we assume @{thm (lhs) arden}. By a simple induction
 on @{text n}, we can establish the property
 \begin{center}
 @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
 \end{center}
 \noindent
-Using this property we can show that @{term "B ;; (A \<up> n) \<subseteq> X"} holds for
+Using this property we can show that @{term "B \<cdot> (A \<up> n) \<subseteq> X"} holds for
-all @{text n}. From this we can infer @{term "B ;; A\<star> \<subseteq> X"} using the definition
+all @{text n}. From this we can infer @{term "B \<cdot> A\<star> \<subseteq> X"} using the definition
 of @{text "\<star>"}.
 For the inclusion in the other direction we assume a string @{text s}
 with length @{text k} is an element in @{text X}. Since @{thm (prem 1) arden}
 we know by Prop.~\ref{langprops}@{text "(ii)"} that
-@{term "s \<notin> X ;; (A \<up> Suc k)"} since its length is only @{text k}
+@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
-(the strings in @{term "X ;; (A \<up> Suc k)"} are all longer).
+(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
 From @{text "(*)"} it follows then that
-@{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B ;; (A \<up> m))"}. This in turn
+@{term s} must be an element in @{term "(\<Union>m\<in>{0..k}. B \<cdot> (A \<up> m))"}. This in turn
-implies that @{term s} is in @{term "(\<Union>n. B ;; (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
+implies that @{term s} is in @{term "(\<Union>n. B \<cdot> (A \<up> n))"}. Using Prop.~\ref{langprops}@{text "(iii)"}
-this is equal to @{term "B ;; A\<star>"}, as we needed to show.\qed
+this is equal to @{term "B \<cdot> A\<star>"}, as we needed to show.\qed
 \end{proof}
 \noindent
 Regular expressions are defined as the inductive datatype
 The key definition in the Myhill-Nerode theorem is the
 \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two
 strings are related, provided there is no distinguishing extension in this
 language. This can be defined as a tertiary relation.
-\begin{definition}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
+\begin{dfntn}[Myhill-Nerode Relation] Given a language @{text A}, two strings @{text x} and
 @{text y} are Myhill-Nerode related provided
 \begin{center}
 @{thm str_eq_def[simplified str_eq_rel_def Pair_Collect]}
 \end{center}
-\end{definition}
+\end{dfntn}
 \noindent
 It is easy to see that @{term "\<approx>A"} is an equivalence relation, which
 partitions the set of all strings, @{text "UNIV"}, into a set of disjoint
 equivalence classes. To illustrate this quotient construction, let us give a simple
 One direction of the Myhill-Nerode theorem establishes
 that if there are finitely many equivalence classes, like in the example above, then
 the language is regular. In our setting we therefore have to show:
-\begin{theorem}\label{myhillnerodeone}
+\begin{thrm}\label{myhillnerodeone}
 @{thm[mode=IfThen] Myhill_Nerode1}
-\end{theorem}
+\end{thrm}
 \noindent
 To prove this theorem, we first define the set @{term "finals A"} as those equivalence
 classes from @{term "UNIV // \<approx>A"} that contain strings of @{text A}, namely
 %
 Overloading the function @{text \<calL>} for the two kinds of terms in the
 equational system, we have
 \begin{center}
 @{text "\<calL>(Y, r) \<equiv>"} %
-@{thm (rhs) L_rhs_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
+@{thm (rhs) L_trm.simps(2)[where X="Y" and r="r", THEN eq_reflection]}\hspace{10mm}
-@{thm L_rhs_trm.simps(1)[where r="r", THEN eq_reflection]}
+@{thm L_trm.simps(1)[where r="r", THEN eq_reflection]}
 \end{center}
 \noindent
 and we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations
 %
 \noindent
 Because we use sets of terms
 for representing the right-hand sides of equations, we can
 prove \eqref{inv1} and \eqref{inv2} more concisely as
 %
-\begin{lemma}\label{inv}
+\begin{lmm}\label{inv}
 If @{thm (prem 1) test} then @{text "X = \<Union> \<calL> ` rhs"}.
-\end{lemma}
+\end{lmm}
 \noindent
 Our proof of Thm.~\ref{myhillnerodeone} will proceed by transforming the
 initial equational system into one in \emph{solved form} maintaining the invariant
 in Lem.~\ref{inv}. From the solved form we will be able to read
 \end{center}
 \noindent
 This allows us to prove a version of Arden's Lemma on the level of equations.
-\begin{lemma}\label{ardenable}
+\begin{lmm}\label{ardenable}
 Given an equation @{text "X = rhs"}.
 If @{text "X = \<Union>\<calL> ` rhs"},
 @{thm (prem 2) Arden_keeps_eq}, and
 @{thm (prem 3) Arden_keeps_eq}, then
 @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
-\end{lemma}
+\end{lmm}
 \noindent
 Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,
 but we can still ensure that it holds troughout our algorithm of transforming equations
 into solved form. The \emph{substitution-operation} takes an equation
 It is straightforward to prove that the initial equational system satisfies the
 invariant.
-\begin{lemma}\label{invzero}
+\begin{lmm}\label{invzero}
 @{thm[mode=IfThen] Init_ES_satisfies_invariant}
-\end{lemma}
+\end{lmm}
 \begin{proof}
 Finiteness is given by the assumption and the way how we set up the
 initial equational system. Soundness is proved in Lem.~\ref{inv}. Distinctness
 follows from the fact that the equivalence classes are disjoint. The @{text ardenable}
 \end{proof}
 \noindent
 Next we show that @{text Iter} preserves the invariant.
-\begin{lemma}\label{iterone}
+\begin{lmm}\label{iterone}
 @{thm[mode=IfThen] iteration_step_invariant[where xrhs="rhs"]}
-\end{lemma}
+\end{lmm}
 \begin{proof}
 The argument boils down to choosing an equation @{text "Y = yrhs"} to be eliminated
 and to show that @{term "Subst_all (ES - {(Y, yrhs)}) Y (Arden Y yrhs)"}
 preserves the invariant.
 \end{proof}
 \noindent
 We also need the fact that @{text Iter} decreases the termination measure.
-\begin{lemma}\label{itertwo}
+\begin{lmm}\label{itertwo}
 @{thm[mode=IfThen] iteration_step_measure[simplified (no_asm), where xrhs="rhs"]}
-\end{lemma}
+\end{lmm}
 \begin{proof}
 By assumption we know that @{text "ES"} is finite and has more than one element.
 Therefore there must be an element @{term "(Y, yrhs) \<in> ES"} with
 @{term "(Y, yrhs) \<noteq> (X, rhs)"}. Using the distinctness property we can infer
 \noindent
 This brings us to our property we want to establish for @{text Solve}.
-\begin{lemma}
+\begin{lmm}
 If @{thm (prem 1) Solve} and @{thm (prem 2) Solve} then there exists
 a @{text rhs} such that  @{term "Solve X (Init (UNIV // \<approx>A)) = {(X, rhs)}"}
 and @{term "invariant {(X, rhs)}"}.
-\end{lemma}
+\end{lmm}
 \begin{proof}
 In order to prove this lemma using \eqref{whileprinciple}, we have to use a slightly
 stronger invariant since Lem.~\ref{iterone} and \ref{itertwo} have the precondition
 that @{term "(X, rhs) \<in> ES"} for some @{text rhs}. This precondition is needed
 \noindent
 With this lemma in place we can show that for every equivalence class in @{term "UNIV // \<approx>A"}
 there exists a regular expression.
-\begin{lemma}\label{every_eqcl_has_reg}
+\begin{lmm}\label{every_eqcl_has_reg}
 @{thm[mode=IfThen] every_eqcl_has_reg}
-\end{lemma}
+\end{lmm}
 \begin{proof}
 By the preceding lemma, we know that there exists a @{text "rhs"} such
 that @{term "Solve X (Init (UNIV // \<approx>A))"} returns the equation @{text "X = rhs"},
 and that the invariant holds for this equation. That means we
 text {*
 We will prove in this section the second part of the Myhill-Nerode
 theorem. It can be formulated in our setting as follows:
-\begin{theorem}
+\begin{thrm}
 Given @{text "r"} is a regular expression, then @{thm Myhill_Nerode2}.
-\end{theorem}
+\end{thrm}
 \noindent
 The proof will be by induction on the structure of @{text r}. It turns out
 the base cases are straightforward.
 will show that the tagging-relations are more refined than @{term "\<approx>(L r)"}, which
 implies that @{term "UNIV // \<approx>(L r)"} must also be finite (a relation @{text "R\<^isub>1"}
 is said to \emph{refine} @{text "R\<^isub>2"} provided @{text "R\<^isub>1 \<subseteq> R\<^isub>2"}).
 We formally define the notion of a \emph{tagging-relation} as follows.
-\begin{definition}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
+\begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
 and @{text y} are \emph{tag-related} provided
 \begin{center}
 @{text "x =tag= y \<equiv> tag x = tag y"}\;.
 \end{center}
-\end{definition}
+\end{dfntn}
 In order to establish finiteness of a set @{text A}, we shall use the following powerful
 principle from Isabelle/HOL's library.
 %
 \noindent
 It states that if an image of a set under an injective function @{text f} (injective over this set)
 is finite, then the set @{text A} itself must be finite. We can use it to establish the following
 two lemmas.
-\begin{lemma}\label{finone}
+\begin{lmm}\label{finone}
 @{thm[mode=IfThen] finite_eq_tag_rel}
-\end{lemma}
+\end{lmm}
 \begin{proof}
 We set in \eqref{finiteimageD}, @{text f} to be @{text "X \<mapsto> tag ` X"}. We have
 @{text "range f"} to be a subset of @{term "Pow (range tag)"}, which we know must be
 finite by assumption. Now @{term "f (UNIV // =tag=)"} is a subset of @{text "range f"},
 @{text "tag x = tag y"}. Since @{text x} and @{text y} are tag-related, this in
 turn means that the equivalence classes @{text X}
 and @{text Y} must be equal.\qed
 \end{proof}
-\begin{lemma}\label{fintwo}
+\begin{lmm}\label{fintwo}
 Given two equivalence relations @{text "R\<^isub>1"} and @{text "R\<^isub>2"}, whereby
 @{text "R\<^isub>1"} refines @{text "R\<^isub>2"}.
 If @{thm (prem 1) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}
 then @{thm (concl) refined_partition_finite[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2"]}.
-\end{lemma}
+\end{lmm}
 \begin{proof}
 We prove this lemma again using \eqref{finiteimageD}. This time we set @{text f} to
 be @{text "X \<mapsto>"}~@{term "{R\<^isub>1 `` {x} | x. x \<in> X}"}. It is easy to see that
 @{term "finite (f ` (UNIV // R\<^isub>2))"} because it is a subset of @{term "Pow (UNIV // R\<^isub>1)"},
 The pattern in \eqref{pattern} is repeated for the other two cases. Unfortunately,
 they are slightly more complicated. In the @{const SEQ}-case we essentially have
 to be able to infer that
 %
 \begin{center}
-@{text "\<dots>"}@{term "x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+@{text "\<dots>"}@{term "x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
 \end{center}
 %
 \noindent
 using the information given by the appropriate tagging-function. The complication
-is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A ;; B"}
+is to find out what the possible splits of @{text "x @ z"} are to be in @{term "A \<cdot> B"}
 (this was easy in case of @{term "A \<union> B"}). To deal with this complication we define the
 notions of \emph{string prefixes}
 %
 \begin{center}
 @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
 \end{center}
 %
 \noindent
 where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.
-Now assuming  @{term "x @ z \<in> A ;; B"} there are only two possible ways of how to `split'
+Now assuming  @{term "x @ z \<in> A \<cdot> B"} there are only two possible ways of how to `split'
-this string to be in @{term "A ;; B"}:
+this string to be in @{term "A \<cdot> B"}:
 %
 \begin{center}
 \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
 \scalebox{0.7}{
 \begin{tikzpicture}
 (z.north west) -- ($(z.north east)+(0em,0em)$)
 node[midway, above=0.5em]{@{text z}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(xa.north west)+(0em,3ex)$) -- ($(z.north east)+(0em,3ex)$)
-node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(z.south east)+(0em,0ex)$) -- ($(xxa.south west)+(0em,0ex)$)
 node[midway, below=0.5em]{@{term "(x - x') @ z \<in> B"}};
 ($(za.north west)+(0em,0ex)$) -- ($(zza.north east)+(0em,0ex)$)
 node[midway, above=0.5em]{@{text z}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(x.north west)+(0em,3ex)$) -- ($(zza.north east)+(0em,3ex)$)
-node[midway, above=0.8em]{@{term "x @ z \<in> A ;; B"}};
+node[midway, above=0.8em]{@{term "x @ z \<in> A \<cdot> B"}};
 \draw[decoration={brace,transform={yscale=3}},decorate]
 ($(za.south east)+(0em,0ex)$) -- ($(x.south west)+(0em,0ex)$)
 node[midway, below=0.5em]{@{text "x @ z' \<in> A"}};
 \end{center}
 %
 \noindent
 Either there is a prefix of @{text x} in @{text A} and the rest is in @{text B} (first picture),
 or @{text x} and a prefix of @{text "z"} is in @{text A} and the rest in @{text B} (second picture).
-In both cases we have to show that @{term "y @ z \<in> A ;; B"}. For this we use the
+In both cases we have to show that @{term "y @ z \<in> A \<cdot> B"}. For this we use the
 following tagging-function
 %
 \begin{center}
 @{thm tag_str_SEQ_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
 \end{center}
 then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
 @{term "tag_str_SEQ A B"} is a subset of this product set, and therefore finite.
 We have to show injectivity of this tagging-function as
 %
 \begin{center}
-@{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A ;; B \<longrightarrow> y @ z \<in> A ;; B"}
+@{term "\<forall>z. tag_str_SEQ A B x = tag_str_SEQ A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
 \end{center}
 %
 \noindent
 There are two cases to be considered (see pictures above). First, there exists
 a @{text "x'"} such that
 That means there must be a @{text "y'"} such that @{text "y' \<in> A"} and
 @{term "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"}. This equality means that
 @{term "(x - x') \<approx>B (y - y')"} holds. Unfolding the Myhill-Nerode
 relation and together with the fact that @{text "(x - x') @ z \<in> B"}, we
 have @{text "(y - y') @ z \<in> B"}. We already know @{text "y' \<in> A"}, therefore
-@{term "y @ z \<in> A ;; B"}, as needed in this case.
+@{term "y @ z \<in> A \<cdot> B"}, as needed in this case.
 Second, there exists a @{text "z'"} such that @{term "x @ z' \<in> A"} and @{text "z - z' \<in> B"}.
 By the assumption about @{term "tag_str_SEQ A B"} we have
 @{term "\<approx>A `` {x} = \<approx>A `` {y}"} and thus @{term "x \<approx>A y"}. Which means by the Myhill-Nerode
 relation that @{term "y @ z' \<in> A"} holds. Using @{text "z - z' \<in> B"}, we can conclude also in this case
-with @{term "y @ z \<in> A ;; B"}. We again can complete the @{const SEQ}-case
+with @{term "y @ z \<in> A \<cdot> B"}. We again can complete the @{const SEQ}-case
 by setting @{text A} to @{term "L r\<^isub>1"} and @{text B} to @{term "L r\<^isub>2"}.\qed
 \end{proof}
 \noindent
 The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
 expressions can conveniently be defined as a datatype in HOL-based theorem
 provers. For us it was therefore interesting to find out how far we can push
 this point of view. We have established in Isabelle/HOL both directions
 of the Myhill-Nerode theorem.
 %
-\begin{theorem}[The Myhill-Nerode Theorem]\mbox{}\\
+\begin{thrm}[The Myhill-Nerode Theorem]\mbox{}\\
 A language @{text A} is regular if and only if @{thm (rhs) Myhill_Nerode}.
-\end{theorem}
+\end{thrm}
 %
 \noindent
 Having formalised this theorem means we
 pushed our point of view quite far. Using this theorem we can obviously prove when a language
 is \emph{not} regular---by establishing that it has infinitely many

changeset 167	61d0a412a3ae
parent 162	e93760534354
child 170	b1258b7d2789