--- a/Journal/Paper.thy Thu Jul 28 17:52:36 2011 +0000
+++ b/Journal/Paper.thy Sun Jul 31 10:27:41 2011 +0000
@@ -39,8 +39,8 @@
notation (latex output)
- str_eq_rel ("\<approx>\<^bsub>_\<^esub>") and
- str_eq ("_ \<approx>\<^bsub>_\<^esub> _") and
+ str_eq ("\<approx>\<^bsub>_\<^esub>") and
+ str_eq_applied ("_ \<approx>\<^bsub>_\<^esub> _") and
conc (infixr "\<cdot>" 100) and
star ("_\<^bsup>\<star>\<^esup>") and
pow ("_\<^bsup>_\<^esup>" [100, 100] 100) and
@@ -59,13 +59,13 @@
Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
- tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
- tag_str_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
- tag_str_Times ("tag\<^isub>S\<^isub>E\<^isub>Q _ _" [100, 100] 100) and
- tag_str_Times ("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) and
- tag_eq_rel ("\<^raw:$\threesim$>\<^bsub>_\<^esub>") and
+ tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _" [100, 100] 100) and
+ tag_Plus ("tag\<^bsub>PLUS\<^esub> _ _ _" [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
Delta ("\<Delta>'(_')") and
nullable ("\<delta>'(_')") and
Cons ("_ :: _" [100, 100] 100)
@@ -74,6 +74,10 @@
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
by auto
+lemma str_eq_def':
+ shows "x \<approx>A y \<equiv> (\<forall>z. x @ z \<in> A \<longleftrightarrow> y @ z \<in> A)"
+unfolding str_eq_def by simp
+
lemma conc_def':
"A \<cdot> B = {s\<^isub>1 @ s\<^isub>2 | s\<^isub>1 s\<^isub>2. s\<^isub>1 \<in> A \<and> s\<^isub>2 \<in> B}"
unfolding conc_def by simp
@@ -174,7 +178,7 @@
\begin{center}
\begin{tabular}{ccc}
- \begin{tikzpicture}[scale=0.9]
+ \begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
@@ -190,8 +194,8 @@
\node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
\node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
- \draw (-0.6,0.0) node {\footnotesize$A_1$};
- \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \draw (-0.6,0.0) node {\small$A_1$};
+ \draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}
&
@@ -200,7 +204,7 @@
&
- \begin{tikzpicture}[scale=0.9]
+ \begin{tikzpicture}[scale=1]
%\draw[step=2mm] (-1,-1) grid (1,1);
\draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
@@ -219,8 +223,8 @@
\draw (C) to [very thick, bend left=45] (B);
\draw (D) to [very thick, bend right=45] (B);
- \draw (-0.6,0.0) node {\footnotesize$A_1$};
- \draw ( 0.6,0.0) node {\footnotesize$A_2$};
+ \draw (-0.6,0.0) node {\small$A_1$};
+ \draw ( 0.6,0.0) node {\small$A_2$};
\end{tikzpicture}
\end{tabular}
@@ -300,7 +304,7 @@
everything is crystal clear. However, paper proofs about automata often
involve subtle side-conditions which are easily overlooked, but which make
formal reasoning rather painful. For example Kozen's proof of the
- Myhill-Nerode theorem requires that the automata do not have inaccessible
+ Myhill-Nerode theorem requires that automata do not have inaccessible
states \cite{Kozen97}. Another subtle side-condition is completeness of
automata, that is automata need to have total transition functions and at most one
`sink' state from which there is no connection to a final state (Brozowski
@@ -346,7 +350,7 @@
To our best knowledge, our proof of the Myhill-Nerode theorem is the first
that is based on regular expressions, only. The part of this theorem stating
that finitely many partitions imply regularity of the language is proved by
- an argument about solving equational sytems. This argument appears to be
+ an argument about solving equational systems. This argument appears to be
folklore. For the other part, we give two proofs: one direct proof using
certain tagging-functions, and another indirect proof using Antimirov's
partial derivatives \cite{Antimirov95}. Again to our best knowledge, the
@@ -403,10 +407,11 @@
the proofs for these properties, but invite the reader to consult our
formalisation.\footnote{Available at \url{http://www4.in.tum.de/~urbanc/regexp.html}}
- The notation in Isabelle/HOL for the quotient of a language @{text A} according to an
- equivalence relation @{term REL} is @{term "A // REL"}. We will write
- @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined
- as \mbox{@{text "{y | y \<approx> x}"}}.
+ The notation in Isabelle/HOL for the quotient of a language @{text A}
+ according to an equivalence relation @{term REL} is @{term "A // REL"}. We
+ will write @{text "\<lbrakk>x\<rbrakk>\<^isub>\<approx>"} for the equivalence class defined as
+ \mbox{@{text "{y | y \<approx> x}"}}, and have @{text "x \<approx> y"} if and only if @{text
+ "\<lbrakk>x\<rbrakk>\<^isub>\<approx> = \<lbrakk>y\<rbrakk>\<^isub>\<approx>"}.
Central to our proof will be the solution of equational systems
@@ -426,9 +431,9 @@
\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 \<cdot> A\<star>"},
- which is equal to @{term "A\<star> = {[]} \<union> A\<star> \<cdot> A"}. Adding @{text B} to both
- sides gives @{term "B \<cdot> A\<star> = B \<cdot> ({[]} \<union> A\<star> \<cdot> A)"}, whose right-hand side
+ we have @{term "A\<star> = A \<cdot> A\<star> \<union> {[]}"},
+ which is equal to @{term "A\<star> = A\<star> \<cdot> A \<union> {[]}"}. Adding @{text B} to both
+ sides gives @{term "B \<cdot> A\<star> = B \<cdot> (A\<star> \<cdot> A \<union> {[]})"}, whose right-hand side
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
@@ -515,7 +520,7 @@
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]}
+ @{thm str_eq_def'}
\end{center}
\end{dfntn}
@@ -641,7 +646,7 @@
\noindent
where @{text "d\<^isub>1\<dots>d\<^isub>n"} is the sequence of all characters
- except @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
+ but not containing @{text c}, and @{text "c\<^isub>1\<dots>c\<^isub>m"} is the sequence of all
characters.
Overloading the function @{text \<calL>} for the two kinds of terms in the
@@ -1067,7 +1072,7 @@
text {*
\noindent
- In this section and the next we will give two proofs for establishing the second
+ In this section we will give a proof for establishing the second
part of the Myhill-Nerode theorem. It can be formulated in our setting as follows:
\begin{thrm}
@@ -1075,7 +1080,7 @@
\end{thrm}
\noindent
- The first proof will be by induction on the structure of @{text r}. It turns out
+ The proof will be by induction on the structure of @{text r}. It turns out
the base cases are straightforward.
@@ -1099,11 +1104,11 @@
Much more interesting, however, are the inductive cases. They seem hard to solve
directly. The reader is invited to try.
- In order how to see how our first proof proceeds we use the following suggestive picture
- from Constable et al \cite{Constable00}:
+ In order to see how our proof proceeds consider the following suggestive picture
+ taken from Constable et al \cite{Constable00}:
- \begin{center}
- \begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
+ \begin{equation}\label{pics}
+ \mbox{\begin{tabular}{c@ {\hspace{10mm}}c@ {\hspace{10mm}}c}
\begin{tikzpicture}[scale=1]
%Circle
\draw[thick] (0,0) circle (1.1);
@@ -1129,10 +1134,17 @@
\draw (\a: 0.77) node {$a_{\l}$};
\end{tikzpicture}\\
@{term UNIV} & @{term "UNIV // (\<approx>(lang r))"} & @{term "UNIV // R"}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
- Our first proof will rely on some
+ \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
+ them, it suffices to show in each induction step the existence of another
+ relation, say @{text R}, for which we can show that there are finitely many
+ equivalence classes and which refines @{term "\<approx>(lang r)"}. A relation @{text
+ "R\<^isub>1"} is said to \emph{refine} @{text "R\<^isub>2"} provided @{text
+ "R\<^isub>1 \<subseteq> R\<^isub>2"}. For constructing @{text R} will rely on some
\emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will
be easy to prove that the \emph{range} of these tagging-functions is finite.
The range of a function @{text f} is defined as
@@ -1142,13 +1154,14 @@
\end{center}
\noindent
- that means we take the image of @{text f} w.r.t.~all elements in the domain.
- With this we will be able to infer that the tagging-functions, seen as relations,
- give rise to finitely many equivalence classes of @{const UNIV}. Finally we
- will show that the tagging-relations are more refined than @{term "\<approx>(lang r)"}, which
- implies that @{term "UNIV // \<approx>(lang 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.
+ that means we take the image of @{text f} w.r.t.~all elements in the
+ domain. With this we will be able to infer that the tagging-functions, seen
+ as relations, give rise to finitely many equivalence classes of @{const
+ UNIV}. Finally we will show that the tagging-relations are more refined than
+ @{term "\<approx>(lang r)"}, which implies that @{term "UNIV // \<approx>(lang r)"} must
+ also be finite. We formally define the notion of a \emph{tagging-relation}
+ as follows.
+
\begin{dfntn}[Tagging-Relation] Given a tagging-function @{text tag}, then two strings @{text x}
and @{text y} are \emph{tag-related} provided
@@ -1212,7 +1225,7 @@
\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 find a tagging-function whose
+ 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.
@@ -1220,14 +1233,14 @@
We take as tagging-function
%
\begin{center}
- @{thm tag_str_Plus_def[where A="A" and B="B", THEN meta_eq_app]}
+ @{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.
We can show in general, if @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
then @{term "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"} holds. The range of
- @{term "tag_str_Plus A B"} is a subset of this product set---so finite. It remains to be shown
+ @{term "tag_Plus A B"} is a subset of this product set---so finite. It remains to be shown
that @{text "=tag\<^isub>A\<^isub>L\<^isub>T A B="} refines @{term "\<approx>(A \<union> B)"}. This amounts to
showing
%
@@ -1269,17 +1282,21 @@
notions of \emph{string prefixes}
%
\begin{center}
- @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\hspace{10mm}
+ \begin{tabular}{l}
+ @{text "x \<le> y \<equiv> \<exists>z. y = x @ z"}\\
@{text "x < y \<equiv> x \<le> y \<and> x \<noteq> y"}
+ \end{tabular}
\end{center}
%
\noindent
and \emph{string subtraction}:
%
\begin{center}
- @{text "[] - y \<equiv> []"}\hspace{10mm}
- @{text "x - [] \<equiv> x"}\hspace{10mm}
- @{text "cx - dy \<equiv> if c = d then x - y else cx"}
+ \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+ @{text "[] - y"} & @{text "\<equiv>"} & @{text "[]"}\\
+ @{text "x - []"} & @{text "\<equiv>"} & @{text "x"}\\
+ @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}
+ \end{tabular}
\end{center}
%
\noindent
@@ -1289,8 +1306,8 @@
this string to be in @{term "A \<cdot> B"}:
%
\begin{center}
- \begin{tabular}{@ {}c@ {\hspace{10mm}}c@ {}}
- \scalebox{0.7}{
+ \begin{tabular}{c}
+ \scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (xa) { $\hspace{3em}@{text "x'"}\hspace{3em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of xa] (xxa) { $\hspace{0.2em}@{text "x - x'"}\hspace{0.2em}$ };
@@ -1316,8 +1333,8 @@
($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
node[midway, below=0.5em]{@{term "x' \<in> A"}};
\end{tikzpicture}}
- &
- \scalebox{0.7}{
+ \\
+ \scalebox{0.9}{
\begin{tikzpicture}
\node[draw,minimum height=3.8ex] (x) { $\hspace{4.8em}@{text x}\hspace{4.8em}$ };
\node[draw,minimum height=3.8ex, right=-0.03em of x] (za) { $\hspace{0.6em}@{text "z'"}\hspace{0.6em}$ };
@@ -1353,7 +1370,7 @@
following tagging-function
%
\begin{center}
- @{thm tag_str_Times_def[where ?L1.0="A" and ?L2.0="B", THEN meta_eq_app]}
+ @{thm tag_Times_def[where ?A="A" and ?B="B", THEN meta_eq_app]}
\end{center}
\noindent
@@ -1363,11 +1380,11 @@
\begin{proof}[@{const TIMES}-Case]
If @{term "finite (UNIV // \<approx>A)"} and @{term "finite (UNIV // \<approx>B)"}
then @{term "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"} holds. The range of
- @{term "tag_str_TIMES A B"} is a subset of this product set, and therefore finite.
+ @{term "tag_Times 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_TIMES A B x = tag_str_TIMES A B y \<and> x @ z \<in> A \<cdot> B \<longrightarrow> y @ z \<in> A \<cdot> B"}
+ @{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"}
\end{center}
%
\noindent
@@ -1380,7 +1397,7 @@
\end{center}
%
\noindent
- and by the assumption about @{term "tag_str_TIMES A B"} also
+ and by the assumption about @{term "tag_Times A B"} also
%
\begin{center}
@{term "(\<approx>B `` {x - x'}) \<in> ({\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A})"}
@@ -1395,7 +1412,7 @@
@{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_TIMES A B"} we have
+ By the assumption about @{term "tag_Times 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 \<cdot> B"}. We again can complete the @{const TIMES}-case
@@ -1467,17 +1484,17 @@
the following tagging-function:
%
\begin{center}
- @{thm tag_str_Star_def[where ?L1.0="A", THEN meta_eq_app]}\smallskip
+ @{thm tag_Star_def[where ?A="A", THEN meta_eq_app]}\smallskip
\end{center}
\begin{proof}[@{const Star}-Case]
If @{term "finite (UNIV // \<approx>A)"}
then @{term "finite (Pow (UNIV // \<approx>A))"} holds. The range of
- @{term "tag_str_Star A"} is a subset of this set, and therefore finite.
+ @{term "tag_Star A"} is a subset of this set, and therefore finite.
Again we have to show injectivity of this tagging-function as
%
\begin{center}
- @{term "\<forall>z. tag_str_Star A x = tag_str_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
+ @{term "\<forall>z. tag_Star A x = tag_Star A y \<and> x @ z \<in> A\<star> \<longrightarrow> y @ z \<in> A\<star>"}
\end{center}
%
\noindent
--- a/Myhill_2.thy Thu Jul 28 17:52:36 2011 +0000
+++ b/Myhill_2.thy Sun Jul 31 10:27:41 2011 +0000
@@ -5,21 +5,30 @@
section {* Direction @{text "regular language \<Rightarrow> finite partition"} *}
-definition
- str_eq :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> bool" ("_ \<approx>_ _")
-where
- "x \<approx>A y \<equiv> (x, y) \<in> (\<approx>A)"
-
-lemma str_eq_def2:
- shows "\<approx>A = {(x, y) | x y. x \<approx>A y}"
-unfolding str_eq_def
-by simp
-
definition
- tag_eq_rel :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
+ tag_eq :: "('a list \<Rightarrow> 'b) \<Rightarrow> ('a list \<times> 'a list) set" ("=_=")
where
"=tag= \<equiv> {(x, y). tag x = tag y}"
+abbreviation
+ tag_eq_applied :: "'a list \<Rightarrow> ('a list \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> bool" ("_ =_= _")
+where
+ "x =tag= y \<equiv> (x, y) \<in> =tag="
+
+lemma test:
+ shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
+unfolding str_eq_def
+by auto
+
+lemma test_refined_intro:
+ assumes "\<And>x y z. \<lbrakk>x =tag= y; x @ z \<in> A\<rbrakk> \<Longrightarrow> y @ z \<in> A"
+ shows "=tag= \<subseteq> \<approx>A"
+using assms
+unfolding str_eq_def tag_eq_def
+apply(clarify, simp (no_asm_use))
+by metis
+
+
lemma finite_eq_tag_rel:
assumes rng_fnt: "finite (range tag)"
shows "finite (UNIV // =tag=)"
@@ -45,11 +54,11 @@
and tag_eq: "?f X = ?f Y"
then obtain x y
where "x \<in> X" "y \<in> Y" "tag x = tag y"
- unfolding quotient_def Image_def image_def tag_eq_rel_def
+ unfolding quotient_def Image_def image_def tag_eq_def
by (simp) (blast)
with X_in Y_in
have "X = Y"
- unfolding quotient_def tag_eq_rel_def by auto
+ unfolding quotient_def tag_eq_def by auto
}
then show "inj_on ?f ?A" unfolding inj_on_def by auto
qed
@@ -101,15 +110,15 @@
show "finite (UNIV // =tag=)" by (rule finite_eq_tag_rel[OF rng_fnt])
next
from same_tag_eqvt
- show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_rel_def str_eq_def
- by auto
+ show "=tag= \<subseteq> \<approx>A" unfolding tag_eq_def str_eq_def
+ by blast
next
show "equiv UNIV =tag="
- unfolding equiv_def tag_eq_rel_def refl_on_def sym_def trans_def
+ unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
by auto
next
show "equiv UNIV (\<approx>A)"
- unfolding equiv_def str_eq_rel_def sym_def refl_on_def trans_def
+ unfolding equiv_def str_eq_def sym_def refl_on_def trans_def
by blast
qed
@@ -120,7 +129,7 @@
lemma quot_zero_eq:
shows "UNIV // \<approx>{} = {UNIV}"
-unfolding quotient_def Image_def str_eq_rel_def by auto
+unfolding quotient_def Image_def str_eq_def by auto
lemma quot_zero_finiteI [intro]:
shows "finite (UNIV // \<approx>{})"
@@ -139,11 +148,11 @@
show "x \<in> {{[]}, UNIV - {[]}}"
proof (cases "y = []")
case True with h
- have "x = {[]}" by (auto simp: str_eq_rel_def)
+ have "x = {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
next
case False with h
- have "x = UNIV - {[]}" by (auto simp: str_eq_rel_def)
+ have "x = UNIV - {[]}" by (auto simp: str_eq_def)
thus ?thesis by simp
qed
qed
@@ -165,17 +174,17 @@
show "x \<in> {{[]},{[c]}, UNIV - {[], [c]}}"
proof -
{ assume "y = []" hence "x = {[]}" using h
- by (auto simp:str_eq_rel_def) }
+ by (auto simp: str_eq_def) }
moreover
{ assume "y = [c]" hence "x = {[c]}" using h
- by (auto dest!:spec[where x = "[]"] simp:str_eq_rel_def) }
+ by (auto dest!: spec[where x = "[]"] simp: str_eq_def) }
moreover
{ assume "y \<noteq> []" and "y \<noteq> [c]"
hence "\<forall> z. (y @ z) \<noteq> [c]" by (case_tac y, auto)
moreover have "\<And> p. (p \<noteq> [] \<and> p \<noteq> [c]) = (\<forall> q. p @ q \<noteq> [c])"
by (case_tac p, auto)
ultimately have "x = UNIV - {[],[c]}" using h
- by (auto simp add:str_eq_rel_def)
+ by (auto simp add: str_eq_def)
}
ultimately show ?thesis by blast
qed
@@ -189,38 +198,126 @@
subsubsection {* The inductive case for @{const Plus} *}
definition
- tag_str_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
+ tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
where
- "tag_str_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
+ "tag_Plus A B \<equiv> (\<lambda>x. (\<approx>A `` {x}, \<approx>B `` {x}))"
-lemma quot_union_finiteI [intro]:
+lemma quot_plus_finiteI [intro]:
assumes finite1: "finite (UNIV // \<approx>A)"
and finite2: "finite (UNIV // \<approx>B)"
shows "finite (UNIV // \<approx>(A \<union> B))"
-proof (rule_tac tag = "tag_str_Plus A B" in tag_finite_imageD)
+proof (rule_tac tag = "tag_Plus A B" in tag_finite_imageD)
have "finite ((UNIV // \<approx>A) \<times> (UNIV // \<approx>B))"
using finite1 finite2 by auto
- then show "finite (range (tag_str_Plus A B))"
- unfolding tag_str_Plus_def quotient_def
+ then show "finite (range (tag_Plus A B))"
+ unfolding tag_Plus_def quotient_def
by (rule rev_finite_subset) (auto)
next
- show "\<And>x y. tag_str_Plus A B x = tag_str_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
- unfolding tag_str_Plus_def
+ show "\<And>x y. tag_Plus A B x = tag_Plus A B y \<Longrightarrow> x \<approx>(A \<union> B) y"
+ unfolding tag_Plus_def
unfolding str_eq_def
- unfolding str_eq_rel_def
by auto
qed
subsubsection {* The inductive case for @{text "Times"}*}
+definition
+ "Partitions s \<equiv> {(u, v). u @ v = s}"
+
+lemma conc_elim:
+ assumes "x \<in> A \<cdot> B"
+ shows "\<exists>(u, v) \<in> Partitions x. u \<in> A \<and> v \<in> B"
+using assms
+unfolding conc_def Partitions_def
+by auto
+
+lemma conc_intro:
+ assumes "(u, v) \<in> Partitions x \<and> u \<in> A \<and> v \<in> B"
+ shows "x \<in> A \<cdot> B"
+using assms
+unfolding conc_def Partitions_def
+by auto
+
+
+lemma y:
+ "\<lbrakk>x \<in> A; x \<approx>A y\<rbrakk> \<Longrightarrow> y \<in> A"
+apply(simp add: str_eq_def)
+apply(drule_tac x="[]" in spec)
+apply(simp)
+done
+
definition
- tag_str_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
+ tag_Times3a :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang"
+where
+ "tag_Times3a A B \<equiv> (\<lambda>x. \<approx>A `` {x})"
+
+definition
+ tag_Times3b :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang) set"
+where
+ "tag_Times3b A B \<equiv>
+ (\<lambda>x. ({(\<approx>A `` {u}, \<approx>B `` {v}) | u v. (u, v) \<in> Partitions x}))"
+
+definition
+ tag_Times3 :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> 'a lang \<times> ('a lang \<times> 'a lang) set"
where
- "tag_str_Times L1 L2 \<equiv>
- (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa. xa \<le> x \<and> xa \<in> L1}))"
+ "tag_Times3 A B \<equiv>
+ (\<lambda>x. (tag_Times3a A B x, tag_Times3b A B x))"
-lemma Seq_in_cases:
+lemma
+ assumes a: "tag_Times3a A B x = tag_Times3a A B y"
+ and b: "tag_Times3b A B x = tag_Times3b A B y"
+ and c: "x @ z \<in> A \<cdot> B"
+ shows "y @ z \<in> A \<cdot> B"
+proof -
+ from c obtain u v where
+ h1: "(u, v) \<in> Partitions (x @ z)" and
+ h2: "u \<in> A" and
+ h3: "v \<in> B" by (auto dest: conc_elim)
+ from h1 have "x @ z = u @ v" unfolding Partitions_def by simp
+ then obtain us
+ where "(x = u @ us \<and> us @ z = v) \<or> (x @ us = u \<and> z = us @ v)"
+ by (auto simp add: append_eq_append_conv2)
+ moreover
+ { assume eq: "x = u @ us" "us @ z = v"
+ have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B x"
+ unfolding tag_Times3b_def Partitions_def using eq by auto
+ then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times3b A B y"
+ using b by simp
+ then obtain u' us' where
+ q1: "\<approx>A `` {u} = \<approx>A `` {u'}" and
+ q2: "\<approx>B `` {us} = \<approx>B `` {us'}" and
+ q3: "(u', us') \<in> Partitions y"
+ by (auto simp add: tag_Times3b_def)
+ from q1 h2 have "u' \<in> A"
+ using y unfolding Image_def str_eq_def by blast
+ moreover from q2 h3 eq
+ have "us' @ z \<in> B"
+ unfolding Image_def str_eq_def by auto
+ ultimately have "y @ z \<in> A \<cdot> B" using q3
+ unfolding Partitions_def by auto
+ }
+ moreover
+ { assume eq: "x @ us = u" "z = us @ v"
+ have "(\<approx>A `` {x}) = tag_Times3a A B x"
+ unfolding tag_Times3a_def by simp
+ then have "(\<approx>A `` {x}) = tag_Times3a A B y"
+ using a by simp
+ then have "\<approx>A `` {x} = \<approx>A `` {y}"
+ unfolding tag_Times3a_def by simp
+ moreover
+ have "x @ us \<in> A" using h2 eq by simp
+ ultimately
+ have "y @ us \<in> A" using y
+ unfolding Image_def str_eq_def by blast
+ then have "(y @ us) @ v \<in> A \<cdot> B"
+ using h3 unfolding conc_def by blast
+ then have "y @ z \<in> A \<cdot> B" using eq by simp
+ }
+ ultimately show "y @ z \<in> A \<cdot> B" by blast
+qed
+
+lemma conc_in_cases2:
assumes "x @ z \<in> A \<cdot> B"
shows "(\<exists> x' \<le> x. x' \<in> A \<and> (x - x') @ z \<in> B) \<or>
(\<exists> z' \<le> z. (x @ z') \<in> A \<and> (z - z') \<in> B)"
@@ -228,13 +325,19 @@
unfolding conc_def prefix_def
by (auto simp add: append_eq_append_conv2)
-lemma tag_str_Times_injI:
- assumes eq_tag: "tag_str_Times A B x = tag_str_Times A B y"
+definition
+ tag_Times :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang set)"
+where
+ "tag_Times A B \<equiv>
+ (\<lambda>x. (\<approx>A `` {x}, {(\<approx>B `` {x - x'}) | x'. x' \<le> x \<and> x' \<in> A}))"
+
+lemma tag_Times_injI:
+ assumes eq_tag: "tag_Times A B x = tag_Times A B y"
shows "x \<approx>(A \<cdot> B) y"
proof -
{ fix x y z
assume xz_in_seq: "x @ z \<in> A \<cdot> B"
- and tag_xy: "tag_str_Times A B x = tag_str_Times A B y"
+ and tag_xy: "tag_Times A B x = tag_Times A B y"
have"y @ z \<in> A \<cdot> B"
proof -
{ (* first case with x' in A and (x - x') @ z in B *)
@@ -247,7 +350,7 @@
proof -
have "{\<approx>B `` {x - x'} |x'. x' \<le> x \<and> x' \<in> A} =
{\<approx>B `` {y - y'} |y'. y' \<le> y \<and> y' \<in> A}" (is "?Left = ?Right")
- using tag_xy unfolding tag_str_Times_def by simp
+ using tag_xy unfolding tag_Times_def by simp
moreover
have "\<approx>B `` {x - x'} \<in> ?Left" using h1 h2 by auto
ultimately
@@ -256,49 +359,49 @@
where eq_xy': "\<approx>B `` {x - x'} = \<approx>B `` {y - y'}"
and pref_y': "y' \<le> y" and y'_in: "y' \<in> A"
by simp blast
-
have "(x - x') \<approx>B (y - y')" using eq_xy'
- unfolding Image_def str_eq_rel_def str_eq_def by auto
+ unfolding Image_def str_eq_def by auto
with h3 have "(y - y') @ z \<in> B"
- unfolding str_eq_rel_def str_eq_def by simp
+ unfolding str_eq_def by simp
with pref_y' y'_in
show ?thesis using that by blast
qed
- then have "y @ z \<in> A \<cdot> B" by (erule_tac prefixE) (auto simp: Seq_def)
+ then have "y @ z \<in> A \<cdot> B"
+ unfolding prefix_def by auto
}
moreover
{ (* second case with x @ z' in A and z - z' in B *)
fix z'
assume h1: "z' \<le> z" and h2: "(x @ z') \<in> A" and h3: "z - z' \<in> B"
have "\<approx>A `` {x} = \<approx>A `` {y}"
- using tag_xy unfolding tag_str_Times_def by simp
+ using tag_xy unfolding tag_Times_def by simp
with h2 have "y @ z' \<in> A"
- unfolding Image_def str_eq_rel_def str_eq_def by auto
+ unfolding Image_def str_eq_def by auto
with h1 h3 have "y @ z \<in> A \<cdot> B"
unfolding prefix_def conc_def
by (auto) (metis append_assoc)
}
ultimately show "y @ z \<in> A \<cdot> B"
- using Seq_in_cases [OF xz_in_seq] by blast
+ using conc_in_cases2 [OF xz_in_seq] by blast
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def str_eq_rel_def by blast
+ show "x \<approx>(A \<cdot> B) y" unfolding str_eq_def by blast
qed
-lemma quot_seq_finiteI [intro]:
- fixes L1 L2::"'a lang"
- assumes fin1: "finite (UNIV // \<approx>L1)"
- and fin2: "finite (UNIV // \<approx>L2)"
- shows "finite (UNIV // \<approx>(L1 \<cdot> L2))"
-proof (rule_tac tag = "tag_str_Times L1 L2" in tag_finite_imageD)
- show "\<And>x y. tag_str_Times L1 L2 x = tag_str_Times L1 L2 y \<Longrightarrow> x \<approx>(L1 \<cdot> L2) y"
- by (rule tag_str_Times_injI)
+lemma quot_conc_finiteI [intro]:
+ fixes A B::"'a lang"
+ assumes fin1: "finite (UNIV // \<approx>A)"
+ and fin2: "finite (UNIV // \<approx>B)"
+ shows "finite (UNIV // \<approx>(A \<cdot> B))"
+proof (rule_tac tag = "tag_Times A B" in tag_finite_imageD)
+ show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
+ by (rule tag_Times_injI)
next
- have *: "finite ((UNIV // \<approx>L1) \<times> (Pow (UNIV // \<approx>L2)))"
+ have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>B)))"
using fin1 fin2 by auto
- show "finite (range (tag_str_Times L1 L2))"
- unfolding tag_str_Times_def
+ show "finite (range (tag_Times A B))"
+ unfolding tag_Times_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto
@@ -307,10 +410,60 @@
subsubsection {* The inductive case for @{const "Star"} *}
+definition
+ "SPartitions s \<equiv> {(u, v). u @ v = s \<and> u < s}"
+
+lemma
+ assumes "x \<in> A\<star>" "x \<noteq> []"
+ shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v \<in> A\<star>"
+using assms
+apply(subst (asm) star_unfold_left)
+apply(simp)
+apply(simp add: conc_def)
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x="([], xs @ ys)" in bexI)
+apply(simp)
+apply(simp add: SPartitions_def)
+apply(auto)
+apply (metis append_Cons list.exhaust strict_prefix_simps(2))
+by (metis Nil_is_append_conv Nil_prefix xt1(11))
+
+lemma
+ assumes "x @ z \<in> A\<star>" "x \<noteq> []"
+ shows "\<exists>(u, v) \<in> SPartitions x. u \<in> A\<star> \<and> v @ z \<in> A\<star>"
+using assms
+apply(subst (asm) star_unfold_left)
+apply(simp)
+apply(simp add: conc_def)
+apply(erule exE)+
+apply(erule conjE)+
+apply(rule_tac x="([], x)" in bexI)
+apply(simp)
+apply(simp add: SPartitions_def)
+by (metis Nil_prefix xt1(11))
+
+lemma finite_set_has_max:
+ "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<exists> max \<in> A. \<forall> a \<in> A. length a \<le> length max"
+apply (induct rule:finite.induct)
+apply(simp)
+by (metis (full_types) all_not_in_conv insertI1 insert_iff linorder_linear order_eq_iff order_trans prefix_length_le)
+
+
+
definition
- tag_str_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
+ tag_Star3 :: "'a lang \<Rightarrow> 'a list \<Rightarrow> (bool \<times> 'a lang) set"
where
- "tag_str_Star L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+ "tag_Star3 A \<equiv>
+ (\<lambda>x. ({(u \<in> A\<star>, \<approx>A `` {v}) | u v. (u, v) \<in> Partitions x}))"
+
+
+
+
+definition
+ tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
+where
+ "tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {x - xa} | xa. xa < x \<and> xa \<in> A\<star>})"
text {* A technical lemma. *}
lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>
@@ -349,19 +502,19 @@
by (auto simp:strict_prefix_def)
-lemma tag_str_Star_injI:
+lemma tag_Star_injI:
fixes L\<^isub>1::"('a::finite) lang"
- assumes eq_tag: "tag_str_Star L\<^isub>1 v = tag_str_Star L\<^isub>1 w"
+ assumes eq_tag: "tag_Star L\<^isub>1 v = tag_Star L\<^isub>1 w"
shows "v \<approx>(L\<^isub>1\<star>) w"
proof-
{ fix x y z
assume xz_in_star: "x @ z \<in> L\<^isub>1\<star>"
- and tag_xy: "tag_str_Star L\<^isub>1 x = tag_str_Star L\<^isub>1 y"
+ and tag_xy: "tag_Star L\<^isub>1 x = tag_Star L\<^isub>1 y"
have "y @ z \<in> L\<^isub>1\<star>"
proof(cases "x = []")
case True
with tag_xy have "y = []"
- by (auto simp add: tag_str_Star_def strict_prefix_def)
+ by (auto simp add: tag_Star_def strict_prefix_def)
thus ?thesis using xz_in_star True by simp
next
case False
@@ -386,19 +539,19 @@
proof-
from tag_xy have "{\<approx>L\<^isub>1 `` {x - xa} |xa. xa < x \<and> xa \<in> L\<^isub>1\<star>} =
{\<approx>L\<^isub>1 `` {y - xa} |xa. xa < y \<and> xa \<in> L\<^isub>1\<star>}" (is "?left = ?right")
- by (auto simp:tag_str_Star_def)
+ by (auto simp:tag_Star_def)
moreover have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?left" using h1 h2 by auto
ultimately have "\<approx>L\<^isub>1 `` {x - xa_max} \<in> ?right" by simp
thus ?thesis using that
- apply (simp add:Image_def str_eq_rel_def str_eq_def) by blast
+ apply (simp add: Image_def str_eq_def) by blast
qed
have "(y - ya) @ z \<in> L\<^isub>1\<star>"
proof-
obtain za zb where eq_zab: "z = za @ zb"
and l_za: "(y - ya)@za \<in> L\<^isub>1" and ls_zb: "zb \<in> L\<^isub>1\<star>"
proof -
- from h1 have "(x - xa_max) @ z \<noteq> []"
- by (auto simp:strict_prefix_def elim:prefixE)
+ from h1 have "(x - xa_max) @ z \<noteq> []"
+ unfolding strict_prefix_def prefix_def by auto
from star_decom [OF h3 this]
obtain a b where a_in: "a \<in> L\<^isub>1"
and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>"
@@ -428,9 +581,9 @@
qed }
ultimately show ?P1 and ?P2 by auto
qed
- hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in by (auto elim:prefixE)
+ hence "(x - xa_max)@?za \<in> L\<^isub>1" using a_in unfolding prefix_def by auto
with eq_xya have "(y - ya) @ ?za \<in> L\<^isub>1"
- by (auto simp:str_eq_def str_eq_rel_def)
+ by (auto simp: str_eq_def)
with eq_z and b_in
show ?thesis using that by blast
qed
@@ -439,25 +592,25 @@
with eq_zab show ?thesis by simp
qed
with h5 h6 show ?thesis
- by (auto simp:strict_prefix_def elim: prefixE)
+ unfolding strict_prefix_def prefix_def by auto
qed
}
from this [OF _ eq_tag] and this [OF _ eq_tag [THEN sym]]
- show ?thesis unfolding str_eq_def str_eq_rel_def by blast
+ show ?thesis unfolding str_eq_def by blast
qed
lemma quot_star_finiteI [intro]:
fixes A::"('a::finite) lang"
assumes finite1: "finite (UNIV // \<approx>A)"
shows "finite (UNIV // \<approx>(A\<star>))"
-proof (rule_tac tag = "tag_str_Star A" in tag_finite_imageD)
- show "\<And>x y. tag_str_Star A x = tag_str_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
- by (rule tag_str_Star_injI)
+proof (rule_tac tag = "tag_Star A" in tag_finite_imageD)
+ show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
+ by (rule tag_Star_injI)
next
have *: "finite (Pow (UNIV // \<approx>A))"
using finite1 by auto
- show "finite (range (tag_str_Star A))"
- unfolding tag_str_Star_def
+ show "finite (range (tag_Star A))"
+ unfolding tag_Star_def
apply(rule finite_subset[OF _ *])
unfolding quotient_def
by auto