--- a/Paper/Paper.thy Mon Feb 20 11:02:50 2012 +0000
+++ b/Paper/Paper.thy Wed Feb 22 13:25:49 2012 +0000
@@ -1,12 +1,12 @@
(*<*)
theory Paper
-imports "../Myhill_2"
+imports "../Closures2" "../Attic/Prefix_subtract"
begin
declare [[show_question_marks = false]]
consts
- REL :: "(string \<times> string) \<Rightarrow> bool"
+ REL :: "(string \<times> string) set"
UPLUS :: "'a set \<Rightarrow> 'a set \<Rightarrow> (nat \<times> 'a) set"
abbreviation
@@ -32,8 +32,8 @@
ML {* @{term "op ^^"} *}
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
@@ -51,12 +51,12 @@
Append_rexp_rhs ("_ \<^raw:\ensuremath{\triangleleft}> _" [100, 100] 50) and
uminus ("\<^raw:\ensuremath{\overline{>_\<^raw:}}>" [100] 100) and
- tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
- tag_str_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [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)
+ tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _" [100, 100] 100) and
+ tag_Plus ("tag\<^isub>A\<^isub>L\<^isub>T _ _ _" [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)
lemma meta_eq_app:
shows "f \<equiv> \<lambda>x. g x \<Longrightarrow> f x \<equiv> g x"
@@ -66,6 +66,10 @@
"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
+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
+
(* THEOREMS *)
lemma conc_Union_left:
@@ -103,6 +107,27 @@
"_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
"_asm" :: "prop \<Rightarrow> asms" ("_")
+lemma pow_length:
+ assumes a: "[] \<notin> A"
+ and b: "s \<in> A \<up> Suc n"
+ shows "n < length s"
+using b
+proof (induct n arbitrary: s)
+ case 0
+ have "s \<in> A \<up> Suc 0" by fact
+ with a have "s \<noteq> []" by auto
+ then show "0 < length s" by auto
+next
+ case (Suc n)
+ have ih: "\<And>s. s \<in> A \<up> Suc n \<Longrightarrow> n < length s" by fact
+ have "s \<in> A \<up> Suc (Suc n)" by fact
+ then obtain s1 s2 where eq: "s = s1 @ s2" and *: "s1 \<in> A" and **: "s2 \<in> A \<up> Suc n"
+ by (auto simp add: Seq_def)
+ from ih ** have "n < length s2" by simp
+ moreover have "0 < length s1" using * a by auto
+ ultimately show "Suc n < length s" unfolding eq
+ by (simp only: length_append)
+qed
(*>*)
@@ -316,7 +341,7 @@
\begin{proposition}\label{langprops}\mbox{}\\
\begin{tabular}{@ {}ll}
- (i) & @{thm star_cases} \\
+ (i) & @{thm star_unfold_left} \\
(ii) & @{thm[mode=IfThen] pow_length}\\
(iii) & @{thm conc_Union_left} \\
\end{tabular}
@@ -343,24 +368,24 @@
\mbox{@{term "X \<cdot> A"}}).
\begin{lemma}[Reverse Arden's Lemma]\label{arden}\mbox{}\\
- If @{thm (prem 1) arden} then
- @{thm (lhs) arden} if and only if
- @{thm (rhs) arden}.
+ If @{thm (prem 1) reversed_Arden} then
+ @{thm (lhs) reversed_Arden} if and only if
+ @{thm (rhs) reversed_Arden}.
\end{lemma}
\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)"}
+ For the right-to-left direction we assume @{thm (rhs) reversed_Arden} and show
+ that @{thm (lhs) reversed_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
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
+ For the other direction we assume @{thm (lhs) reversed_Arden}. By a simple induction
on @{text n}, we can establish the property
\begin{center}
- @{text "(*)"}\hspace{5mm} @{thm (concl) arden_helper}
+ @{text "(*)"}\hspace{5mm} @{thm (concl) reversed_arden_helper}
\end{center}
\noindent
@@ -368,7 +393,7 @@
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}
+ with length @{text k} is an element in @{text X}. Since @{thm (prem 1) reversed_Arden}
we know by Prop.~\ref{langprops}@{text "(ii)"} that
@{term "s \<notin> X \<cdot> (A \<up> Suc k)"} since its length is only @{text k}
(the strings in @{term "X \<cdot> (A \<up> Suc k)"} are all longer).
@@ -421,7 +446,7 @@
set @{text rs} with @{const NULL} for the empty set. We can prove that for a finite set @{text rs}
%
\begin{equation}\label{uplus}
- \mbox{@{thm (lhs) folds_alt_simp} @{text "= \<Union> (\<calL> ` rs)"}}
+ \mbox{@{thm (lhs) folds_plus_simp} @{text "= \<Union> (\<calL> ` rs)"}}
\end{equation}
\noindent
@@ -441,7 +466,7 @@
\begin{definition}[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]}
+ @{thm str_eq_def'}
\end{center}
\end{definition}
@@ -662,8 +687,8 @@
\begin{lemma}\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
+ @{thm (prem 2) Arden_preserves_soundness}, and
+ @{thm (prem 3) Arden_preserves_soundness}, then
@{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
\end{lemma}