--- a/Journal/Paper.thy Tue Aug 02 15:27:37 2011 +0000
+++ b/Journal/Paper.thy Wed Aug 03 00:52:41 2011 +0000
@@ -59,8 +59,8 @@
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\<^bsub>PLUS\<^esub> _ _ _" [100, 100, 100] 100) and
+ tag_Plus ("+tag _ _" [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
@@ -261,8 +261,8 @@
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
- opts for a variant of \eqref{disjointunion} using bit lists, but writes
+ him to ``messy proofs''. Since he does not need to define what a regular
+ language is, Nipkow opts for a variant of \eqref{disjointunion} using bit lists, but writes
\begin{quote}
\it%
@@ -768,8 +768,8 @@
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
- and not specify it any further.
+ our algorithm we are only interested in the existence of such a regular expression
+ 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
@@ -1101,7 +1101,7 @@
\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
@@ -1139,16 +1139,16 @@
\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
-
+ equivalence classes. To show that there are only finitely many of them, it
+ suffices to show in each induction step that another relation, say @{text
+ R}, has finitely many equivalence classes and 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
+
\begin{center}
@{text "range f \<equiv> f ` UNIV"}
\end{center}
@@ -1227,42 +1227,27 @@
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.
-
- \begin{proof}[@{const "PLUS"}-Case]
- We take as tagging-function
- %
+ Let us attempt the @{const PLUS}-case first. 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.
- 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_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
- %
- \begin{center}
- @{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"}
- \end{center}
- %
- \noindent
- which by unfolding the Myhill-Nerode relation is identical to
- %
- \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"}.
+ where @{text "A"} and @{text "B"} are some arbitrary languages. The reason for this choice
+ is that we need to that @{term "=(tag_Plus A B)="} refines @{term "\<approx>(A \<union> B)"}. This amounts
+ to showing @{term "x \<approx>A y"} or @{term "x \<approx>B y"} under the assumption
+ @{term "x"}~@{term "=(tag_Plus A B)="}~@{term y}. The definition will allow to infer this.
+
+ \begin{proof}[@{const "PLUS"}-Case]
+ 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_Plus A B"} is a subset of this product
+ 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
+ clearly either @{term "x \<approx>A y"} or @{term "x \<approx>B y"} hold, as we needed 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"}.
\end{proof}
--- a/Journal/ROOT.ML Tue Aug 02 15:27:37 2011 +0000
+++ b/Journal/ROOT.ML Wed Aug 03 00:52:41 2011 +0000
@@ -1,3 +1,4 @@
no_document use_thy "../Closures";
+no_document use_thy "../Attic/Prefix_subtract";
use_thy "Paper"
\ No newline at end of file
--- a/Myhill_2.thy Tue Aug 02 15:27:37 2011 +0000
+++ b/Myhill_2.thy Wed Aug 03 00:52:41 2011 +0000
@@ -15,16 +15,14 @@
where
"x =tag= y \<equiv> (x, y) \<in> =tag="
-lemma test:
+lemma [simp]:
shows "(\<approx>A) `` {x} = (\<approx>A) `` {y} \<longleftrightarrow> x \<approx>A y"
-unfolding str_eq_def
-by auto
+unfolding str_eq_def by auto
-lemma test_refined_intro:
+lemma 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
+using assms unfolding str_eq_def tag_eq_def
apply(clarify, simp (no_asm_use))
by metis
@@ -103,14 +101,13 @@
lemma tag_finite_imageD:
assumes rng_fnt: "finite (range tag)"
- and same_tag_eqvt: "\<And>m n. tag m = tag n \<Longrightarrow> m \<approx>A n"
+ and same_tag_eqvt: "=tag= \<subseteq> \<approx>A"
shows "finite (UNIV // \<approx>A)"
proof (rule_tac refined_partition_finite [of "=tag="])
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_def str_eq_def
- by blast
+ show "=tag= \<subseteq> \<approx>A" .
next
show "equiv UNIV =tag="
unfolding equiv_def tag_eq_def refl_on_def sym_def trans_def
@@ -199,7 +196,7 @@
definition
tag_Plus :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang \<times> 'a lang)"
where
- "tag_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_plus_finiteI [intro]:
assumes finite1: "finite (UNIV // \<approx>A)"
@@ -212,14 +209,12 @@
unfolding tag_Plus_def quotient_def
by (rule rev_finite_subset) (auto)
next
- 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
- by auto
+ show "=tag_Plus A B= \<subseteq> \<approx>(A \<union> B)"
+ unfolding tag_eq_def tag_Plus_def str_eq_def by auto
qed
-subsubsection {* The inductive case for @{text "Times"}*}
+subsubsection {* The inductive case for @{text "Times"} *}
definition
"Partitions s \<equiv> {(u, v). u @ v = s}"
@@ -227,15 +222,13 @@
lemma conc_partitions_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
+using assms unfolding conc_def Partitions_def
by auto
lemma conc_partitions_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
+using assms unfolding conc_def Partitions_def
by auto
lemma equiv_class_member:
@@ -243,7 +236,8 @@
and "\<approx>A `` {x} = \<approx>A `` {y}"
shows "y \<in> A"
using assms
-apply(simp add: Image_def str_eq_def set_eq_iff)
+apply(simp)
+apply(simp add: str_eq_def)
apply(metis append_Nil2)
done
@@ -280,7 +274,7 @@
moreover
{ assume eq: "x = u @ us" "us @ z = v"
have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B x"
- unfolding Partitions_def using eq by auto
+ unfolding Partitions_def using eq by (auto simp add: str_eq_def)
then have "(\<approx>A `` {u}, \<approx>B `` {us}) \<in> tag_Times_2 A B y"
using b by simp
then obtain u' us' where
@@ -314,21 +308,16 @@
qed
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)
- have "=(tag_Times A B)= \<subseteq> \<approx>(A \<cdot> B)"
- apply(rule test_refined_intro)
- apply(rule tag_Times_injI)
- prefer 3
- apply(assumption)
- apply(simp add: tag_Times_def tag_eq_def)
- apply(simp add: tag_eq_def tag_Times_def)
- done
- then show "\<And>x y. tag_Times A B x = tag_Times A B y \<Longrightarrow> x \<approx>(A \<cdot> B) y"
- unfolding tag_eq_def by auto
+ have "\<And>x y z. \<lbrakk>tag_Times A B x = tag_Times A B y; x @ z \<in> A \<cdot> B\<rbrakk> \<Longrightarrow> y @ z \<in> A \<cdot> B"
+ by (rule tag_Times_injI)
+ (auto simp add: tag_Times_def tag_eq_def)
+ then show "=tag_Times A B= \<subseteq> \<approx>(A \<cdot> B)"
+ by (rule refined_intro)
+ (auto simp add: tag_eq_def)
next
have *: "finite ((UNIV // \<approx>A) \<times> (Pow (UNIV // \<approx>A \<times> UNIV // \<approx>B)))"
using fin1 fin2 by auto
@@ -342,14 +331,7 @@
subsubsection {* The inductive case for @{const "Star"} *}
-lemma append_eq_append_conv3:
- assumes "xs @ ys = zs @ ts" "zs < xs"
- shows "\<exists>us. xs = zs @ us \<and> us @ ys = ts"
-using assms
-apply(auto simp add: append_eq_append_conv2 strict_prefix_def)
-done
-
-lemma star_spartitions_elim:
+lemma star_partitions_elim:
assumes "x @ z \<in> A\<star>" "x \<noteq> []"
shows "\<exists>(u, v) \<in> Partitions (x @ z). u < x \<and> u \<in> A\<star> \<and> v \<in> A\<star>"
proof -
@@ -359,7 +341,6 @@
by blast
qed
-
lemma finite_set_has_max2:
"\<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)
@@ -422,9 +403,7 @@
moreover
have "as @ z \<in> A\<star>" using i1' i2 i3 eq by auto
ultimately have "length (u_max @ a) \<le> length u_max" using h4 by blast
- moreover
- have "a \<noteq> []" using i4 .
- ultimately show "False" by auto
+ with i4 show "False" by auto
qed
with i1 obtain za zb
where k1: "v @ za = a"
@@ -433,107 +412,75 @@
unfolding Partitions_def prefix_def
by (auto simp add: append_eq_append_conv2)
show "\<exists> (u, v) \<in> Partitions x. \<exists> (u', v') \<in> Partitions z. u < x \<and> u \<in> A\<star> \<and> v @ u' \<in> A \<and> v' \<in> A\<star>"
- using h0 k2 h1 h2 i2 k1 i3 k4 unfolding Partitions_def by blast
+ using h0 h1 h2 i2 i3 k1 k2 k4 unfolding Partitions_def by blast
qed
-
definition
tag_Star :: "'a lang \<Rightarrow> 'a list \<Rightarrow> ('a lang) set"
where
"tag_Star A \<equiv> (\<lambda>x. {\<approx>A `` {v} | u v. u < x \<and> u \<in> A\<star> \<and> (u, v) \<in> Partitions x})"
-
-lemma tag_Star_injI:
- fixes x::"'a list"
+lemma tag_Star_non_empty_injI:
assumes a: "tag_Star A x = tag_Star A y"
and c: "x @ z \<in> A\<star>"
and d: "x \<noteq> []"
shows "y @ z \<in> A\<star>"
-using c d
-apply(drule_tac star_spartitions_elim2)
-apply(simp)
-apply(simp add: Partitions_def)
-apply(erule exE | erule conjE)+
-apply(subgoal_tac "((\<approx>A) `` {b}) \<in> tag_Star A x")
-apply(simp add: a)
-apply(simp add: tag_Star_def)
-apply(erule exE | erule conjE)+
-apply(simp add: test)
-apply(simp add: Partitions_def)
-apply(subgoal_tac "v @ aa \<in> A\<star>")
-prefer 2
-apply(simp add: str_eq_def)
-apply(subgoal_tac "(u @ v) @ aa @ ba \<in> A\<star>")
-apply(simp)
-apply(simp (no_asm_use))
-apply(rule append_in_starI)
-apply(simp)
-apply(simp (no_asm) only: append_assoc[symmetric])
-apply(rule append_in_starI)
-apply(simp)
-apply(simp)
-apply(simp add: tag_Star_def)
-apply(rule_tac x="a" in exI)
-apply(rule_tac x="b" in exI)
-apply(simp)
-apply(simp add: Partitions_def)
-done
-
-lemma tag_Star_injI2:
- fixes x::"'a list"
+proof -
+ obtain u v u' v'
+ where a1: "(u, v) \<in> Partitions x" "(u', v')\<in> Partitions z"
+ and a2: "u < x"
+ and a3: "u \<in> A\<star>"
+ and a4: "v @ u' \<in> A"
+ and a5: "v' \<in> A\<star>"
+ using c d by (auto dest: star_spartitions_elim2)
+ have "(\<approx>A) `` {v} \<in> tag_Star A x"
+ apply(simp add: tag_Star_def Partitions_def str_eq_def)
+ using a1 a2 a3 by (auto simp add: Partitions_def)
+ then have "(\<approx>A) `` {v} \<in> tag_Star A y" using a by simp
+ then obtain u1 v1
+ where b1: "v \<approx>A v1"
+ and b3: "u1 \<in> A\<star>"
+ and b4: "(u1, v1) \<in> Partitions y"
+ unfolding tag_Star_def by auto
+ have c: "v1 @ u' \<in> A\<star>" using b1 a4 unfolding str_eq_def by simp
+ have "u1 @ (v1 @ u') @ v' \<in> A\<star>"
+ using b3 c a5 by (simp only: append_in_starI)
+ then show "y @ z \<in> A\<star>" using b4 a1
+ unfolding Partitions_def by auto
+qed
+
+lemma tag_Star_empty_injI:
assumes a: "tag_Star A x = tag_Star A y"
and c: "x @ z \<in> A\<star>"
and d: "x = []"
shows "y @ z \<in> A\<star>"
-using c d
+using assms
apply(simp)
-using a
apply(simp add: tag_Star_def strict_prefix_def)
apply(auto simp add: prefix_def Partitions_def)
by (metis Nil_in_star append_self_conv2)
-
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_Star A" in tag_finite_imageD)
- have "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
- apply(rule test_refined_intro)
- apply(case_tac "x=[]")
- apply(rule tag_Star_injI2)
- prefer 3
- apply(assumption)
- prefer 2
- apply(assumption)
- apply(simp add: tag_eq_def)
- apply(rule tag_Star_injI)
- prefer 3
- apply(assumption)
- prefer 2
- apply(assumption)
- unfolding tag_eq_def
- apply(simp)
- done
- then show "\<And>x y. tag_Star A x = tag_Star A y \<Longrightarrow> x \<approx>(A\<star>) y"
- apply(simp add: tag_eq_def)
- apply(auto)
- done
+ have "\<And>x y z. \<lbrakk>tag_Star A x = tag_Star A y; x @ z \<in> A\<star>\<rbrakk> \<Longrightarrow> y @ z \<in> A\<star>"
+ by (case_tac "x = []") (blast intro: tag_Star_empty_injI tag_Star_non_empty_injI)+
+ then show "=(tag_Star A)= \<subseteq> \<approx>(A\<star>)"
+ by (rule refined_intro) (auto simp add: tag_eq_def)
next
have *: "finite (Pow (UNIV // \<approx>A))"
using finite1 by auto
show "finite (range (tag_Star A))"
- unfolding tag_Star_def
- apply(rule finite_subset[OF _ *])
- unfolding quotient_def
- apply(auto)
- done
+ unfolding tag_Star_def
+ by (rule finite_subset[OF _ *])
+ (auto simp add: quotient_def)
qed
subsubsection{* The conclusion *}
lemma Myhill_Nerode2:
- fixes r::"('a::finite) rexp"
+ fixes r::"'a rexp"
shows "finite (UNIV // \<approx>(lang r))"
by (induct r) (auto)
@@ -542,4 +489,4 @@
shows "(\<exists>r. A = lang r) \<longleftrightarrow> finite (UNIV // \<approx>A)"
using Myhill_Nerode1 Myhill_Nerode2 by auto
-end
+end
\ No newline at end of file