--- a/Derivatives.thy Thu Jul 28 11:56:25 2011 +0000
+++ b/Derivatives.thy Thu Jul 28 14:22:10 2011 +0000
@@ -14,7 +14,7 @@
definition
Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
where
- "Der c A \<equiv> {s. [c] @ s \<in> A}"
+ "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
definition
Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
@@ -77,25 +77,19 @@
finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
qed
+lemma Ders_nil [simp]:
+ shows "Ders [] A = A"
+unfolding Ders_def by simp
-lemma Ders_singleton:
- shows "Ders [c] A = Der c A"
-unfolding Der_def Ders_def
-by simp
+lemma Ders_cons [simp]:
+ shows "Ders (c # s) A = Ders s (Der c A)"
+unfolding Ders_def Der_def by auto
-lemma Ders_append:
+lemma Ders_append [simp]:
shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
unfolding Ders_def by simp
-text {* Relating the Myhill-Nerode relation with left-quotients. *}
-
-lemma MN_Rel_Ders:
- shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
-unfolding Ders_def str_eq_def str_eq_rel_def
-by auto
-
-
subsection {* Brozowsky's derivatives of regular expressions *}
fun
@@ -119,15 +113,12 @@
(if nullable r1 then Plus (Times (der c r1) r2) (der c r2) else Times (der c r1) r2)"
| "der c (Star r) = Times (der c r) (Star r)"
-function
+fun
ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
"ders [] r = r"
-| "ders (s @ [c]) r = der c (ders s r)"
-by (auto) (metis rev_cases)
+| "ders (c # s) r = ders s (der c r)"
-termination
- by (relation "measure (length o fst)") (auto)
lemma Delta_nullable:
shows "Delta (lang r) = (if nullable r then {[]} else {})"
@@ -140,13 +131,7 @@
lemma Ders_ders:
shows "Ders s (lang r) = lang (ders s r)"
-apply(induct s rule: rev_induct)
-apply(simp add: Ders_def)
-apply(simp only: ders.simps)
-apply(simp only: Ders_append)
-apply(simp only: Ders_singleton)
-apply(simp only: Der_der)
-done
+by (induct s arbitrary: r) (simp_all add: Der_der)
subsection {* Antimirov's Partial Derivatives *}
@@ -161,40 +146,29 @@
| "pder c One = {Zero}"
| "pder c (Atom c') = (if c = c' then {One} else {Zero})"
| "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
-| "pder c (Times r1 r2) = Times_set (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
+| "pder c (Times r1 r2) =
+ (if nullable r1 then Times_set (pder c r1) r2 \<union> pder c r2 else Times_set (pder c r1) r2)"
| "pder c (Star r) = Times_set (pder c r) (Star r)"
abbreviation
"pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
-function
+fun
pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
where
"pders [] r = {r}"
-| "pders (s @ [c]) r = pder_set c (pders s r)"
-by (auto) (metis rev_cases)
-
-termination
- by (relation "measure (length o fst)") (auto)
+| "pders (c # s) r = (\<Union>r'\<in> (pder c r). (pders s r'))"
abbreviation
"pders_set A r \<equiv> \<Union>s \<in> A. pders s r"
lemma pders_append:
"pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
-apply(induct s2 arbitrary: s1 r rule: rev_induct)
-apply(simp)
-apply(subst append_assoc[symmetric])
-apply(simp only: pders.simps)
-apply(auto)
-done
+by (induct s1 arbitrary: r) (simp_all)
-lemma pders_singleton:
- "pders [c] r = pder c r"
-apply(subst append_Nil[symmetric])
-apply(simp only: pders.simps)
-apply(simp)
-done
+lemma pders_snoc:
+ shows "pders (s @ [c]) r = pder_set c (pders s r)"
+by (simp add: pders_append)
lemma pders_set_lang:
shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
@@ -203,19 +177,19 @@
lemma pders_Zero [simp]:
shows "pders s Zero = {Zero}"
-by (induct s rule: rev_induct) (simp_all)
+by (induct s) (simp_all)
lemma pders_One [simp]:
shows "pders s One = (if s = [] then {One} else {Zero})"
-by (induct s rule: rev_induct) (auto)
+by (induct s) (auto)
lemma pders_Atom [simp]:
shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
-by (induct s rule: rev_induct) (auto)
+by (induct s) (auto)
lemma pders_Plus [simp]:
shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
-by (induct s rule: rev_induct) (auto)
+by (induct s) (auto)
text {* Non-empty suffixes of a string *}
@@ -237,7 +211,8 @@
case (snoc c s)
have ih: "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"
by fact
- have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp
+ have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))"
+ by (simp add: pders_snoc)
also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
using ih by (auto) (blast)
also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
@@ -245,15 +220,11 @@
also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> (\<Union>v \<in> Suf s. pder_set c (pders v r2))"
by (simp)
also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
- by (auto)
+ by (auto simp add: pders_snoc)
also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
by (auto simp add: if_splits) (blast)
also have "\<dots> = Times_set (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"
- apply(subst (2) pders.simps)
- apply(simp only: Suf)
- apply(simp add: Suf_Union pders_singleton)
- apply(auto)
- done
+ by (auto simp add: pders_snoc Suf Suf_Union)
finally show ?case .
qed (simp)
@@ -265,7 +236,7 @@
case (snoc c s)
have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r))" by fact
{ assume asm: "s \<noteq> []"
- have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by simp
+ have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)
also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. Times_set (pders v r) (Star r)))"
using ih[OF asm] by blast
also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
@@ -275,52 +246,46 @@
also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r))) \<union> pder c (Star r)"
using asm by (auto simp add: Suf_def)
also have "\<dots> = (\<Union>v\<in>Suf s. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
- by simp
+ by (simp add: pders_snoc)
also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"
- apply(simp only: Suf)
- apply(simp add: Suf_Union pders_singleton)
- apply(auto)
- done
+ by (auto simp add: Suf Suf_Union pders_snoc)
finally have ?case .
}
moreover
{ assume asm: "s = []"
then have ?case
- apply(simp add: pders_singleton Suf_def)
- apply(auto)
- apply(rule_tac x="[c]" in exI)
- apply(simp add: pders_singleton)
- done
+ by (auto simp add: pders_snoc Suf_def)
}
ultimately show ?case by blast
qed (simp)
-abbreviation
+definition
"UNIV1 \<equiv> UNIV - {[]}"
lemma pders_set_Zero:
shows "pders_set UNIV1 Zero = {Zero}"
-by auto
+unfolding UNIV1_def by auto
lemma pders_set_One:
shows "pders_set UNIV1 One = {Zero}"
-by (auto split: if_splits)
+unfolding UNIV1_def by (auto split: if_splits)
lemma pders_set_Atom:
shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
-by (auto split: if_splits)
+unfolding UNIV1_def by (auto split: if_splits)
lemma pders_set_Plus:
shows "pders_set UNIV1 (Plus r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"
-by auto
+unfolding UNIV1_def by auto
lemma pders_set_Times_aux:
assumes a: "s \<in> UNIV1"
shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"
-using a by (auto simp add: Suf_def)
+using a unfolding UNIV1_def Suf_def by (auto)
lemma pders_set_Times:
shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
apply(rule pders_Times)
@@ -329,11 +294,12 @@
apply(auto)[1]
apply(rule subset_trans)
apply(rule pders_set_Times_aux)
-apply(auto)
+apply(auto simp add: UNIV1_def)
done
lemma pders_set_Star:
shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (pders_set UNIV1 r) (Star r)"
+unfolding UNIV1_def
apply(rule UN_least)
apply(rule subset_trans)
apply(rule pders_Star)
@@ -369,6 +335,7 @@
lemma pders_set_UNIV_UNIV1:
shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"
+unfolding UNIV1_def
apply(auto)
apply(rule_tac x="[]" in exI)
apply(simp)
@@ -418,7 +385,7 @@
have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
by (simp add: Ders_append)
also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
- by (simp add: Ders_singleton)
+ by (simp)
also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))"
unfolding Der_def image_def by auto
also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang ` (pder c r)))"
@@ -426,7 +393,7 @@
also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
by (simp add: pders_set_lang)
also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
- by simp
+ by (simp add: pders_snoc)
finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
qed (simp add: Ders_def)
@@ -446,6 +413,12 @@
unfolding Ders_ders[symmetric] Ders_pders by simp
+text {* Relating the Myhill-Nerode relation with left-quotients. *}
+
+lemma MN_Rel_Ders:
+ shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
+unfolding Ders_def str_eq_def str_eq_rel_def
+by auto
subsection {*
The second direction of the Myhill-Nerode theorem using
@@ -488,4 +461,5 @@
by (rule refined_partition_finite)
qed
+
end
\ No newline at end of file
--- a/Journal/Paper.thy Thu Jul 28 11:56:25 2011 +0000
+++ b/Journal/Paper.thy Thu Jul 28 14:22:10 2011 +0000
@@ -779,8 +779,8 @@
\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
+ @{thm (prem 2) Arden_preserves_soundness}, and
+ @{thm (prem 3) Arden_preserves_soundness}, then
@{text "X = \<Union>\<calL> ` (Arden X rhs)"}.
\end{lmm}
@@ -1098,6 +1098,9 @@
Much more interesting, however, are the inductive cases. They seem hard to solve
directly. The reader is invited to try.
+ Constable et al \cite{Constable00} give the following suggestive picture about
+ equivalence classes:
+
Our first proof 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.
--- a/Myhill_1.thy Thu Jul 28 11:56:25 2011 +0000
+++ b/Myhill_1.thy Thu Jul 28 14:22:10 2011 +0000
@@ -5,7 +5,7 @@
section {* Direction @{text "finite partition \<Rightarrow> regular language"} *}
-lemma Pair_Collect[simp]:
+lemma Pair_Collect [simp]:
shows "(x, y) \<in> {(x, y). P x y} \<longleftrightarrow> P x y"
by simp
@@ -57,7 +57,6 @@
by (auto)
lemma lang_rhs_union_distrib:
- fixes A B::"('a trm) set"
shows "lang_rhs A \<union> lang_rhs B = lang_rhs (A \<union> B)"
by simp
@@ -350,7 +349,7 @@
subsubsection {* Interation step *}
-lemma Arden_keeps_eq:
+lemma Arden_preserves_soundness:
assumes l_eq_r: "X = lang_rhs rhs"
and not_empty: "ardenable rhs"
and finite: "finite rhs"
@@ -379,37 +378,37 @@
finally show "X = lang_rhs (Arden X rhs)" by simp
qed
-lemma Append_keeps_finite:
+lemma Append_preserves_finite:
"finite rhs \<Longrightarrow> finite (Append_rexp_rhs rhs r)"
by (auto simp: Append_rexp_rhs_def)
-lemma Arden_keeps_finite:
+lemma Arden_preserves_finite:
"finite rhs \<Longrightarrow> finite (Arden X rhs)"
-by (auto simp: Arden_def Append_keeps_finite)
+by (auto simp: Arden_def Append_preserves_finite)
-lemma Append_keeps_nonempty:
+lemma Append_preserves_ardenable:
"ardenable rhs \<Longrightarrow> ardenable (Append_rexp_rhs rhs r)"
apply (auto simp: ardenable_def Append_rexp_rhs_def)
by (case_tac x, auto simp: conc_def)
-lemma nonempty_set_sub:
+lemma ardenable_set_sub:
"ardenable rhs \<Longrightarrow> ardenable (rhs - A)"
by (auto simp:ardenable_def)
-lemma nonempty_set_union:
+lemma ardenable_set_union:
"\<lbrakk>ardenable rhs; ardenable rhs'\<rbrakk> \<Longrightarrow> ardenable (rhs \<union> rhs')"
by (auto simp:ardenable_def)
-lemma Arden_keeps_nonempty:
+lemma Arden_preserves_ardenable:
"ardenable rhs \<Longrightarrow> ardenable (Arden X rhs)"
-by (simp only:Arden_def Append_keeps_nonempty nonempty_set_sub)
+by (simp only:Arden_def Append_preserves_ardenable ardenable_set_sub)
-lemma Subst_keeps_nonempty:
+lemma Subst_preserves_ardenable:
"\<lbrakk>ardenable rhs; ardenable xrhs\<rbrakk> \<Longrightarrow> ardenable (Subst rhs X xrhs)"
-by (simp only: Subst_def Append_keeps_nonempty nonempty_set_union nonempty_set_sub)
+by (simp only: Subst_def Append_preserves_ardenable ardenable_set_union ardenable_set_sub)
-lemma Subst_keeps_eq:
+lemma Subst_preserves_soundness:
assumes substor: "X = lang_rhs xrhs"
and finite: "finite rhs"
shows "lang_rhs (Subst rhs X xrhs) = lang_rhs rhs" (is "?Left = ?Right")
@@ -433,11 +432,11 @@
ultimately show ?thesis by simp
qed
-lemma Subst_keeps_finite_rhs:
+lemma Subst_preserves_finite_rhs:
"\<lbrakk>finite rhs; finite yrhs\<rbrakk> \<Longrightarrow> finite (Subst rhs Y yrhs)"
-by (auto simp: Subst_def Append_keeps_finite)
+by (auto simp: Subst_def Append_preserves_finite)
-lemma Subst_all_keeps_finite:
+lemma Subst_all_preserves_finite:
assumes finite: "finite ES"
shows "finite (Subst_all ES Y yrhs)"
proof -
@@ -450,11 +449,11 @@
show "finite (Subst_all ES Y yrhs)" by simp
qed
-lemma Subst_all_keeps_finite_rhs:
+lemma Subst_all_preserves_finite_rhs:
"\<lbrakk>finite_rhs ES; finite yrhs\<rbrakk> \<Longrightarrow> finite_rhs (Subst_all ES Y yrhs)"
-by (auto intro:Subst_keeps_finite_rhs simp add:Subst_all_def finite_rhs_def)
+by (auto intro:Subst_preserves_finite_rhs simp add:Subst_all_def finite_rhs_def)
-lemma append_rhs_keeps_cls:
+lemma append_rhs_preserves_cls:
"rhss (Append_rexp_rhs rhs r) = rhss rhs"
apply (auto simp: rhss_def Append_rexp_rhs_def)
apply (case_tac xa, auto simp: image_def)
@@ -462,20 +461,20 @@
lemma Arden_removes_cl:
"rhss (Arden Y yrhs) = rhss yrhs - {Y}"
-apply (simp add:Arden_def append_rhs_keeps_cls)
+apply (simp add:Arden_def append_rhs_preserves_cls)
by (auto simp: rhss_def)
-lemma lhss_keeps_cls:
+lemma lhss_preserves_cls:
"lhss (Subst_all ES Y yrhs) = lhss ES"
by (auto simp: lhss_def Subst_all_def)
lemma Subst_updates_cls:
"X \<notin> rhss xrhs \<Longrightarrow>
rhss (Subst rhs X xrhs) = rhss rhs \<union> rhss xrhs - {X}"
-apply (simp only:Subst_def append_rhs_keeps_cls rhss_union_distrib)
+apply (simp only:Subst_def append_rhs_preserves_cls rhss_union_distrib)
by (auto simp: rhss_def)
-lemma Subst_all_keeps_validity:
+lemma Subst_all_preserves_validity:
assumes sc: "validity (ES \<union> {(Y, yrhs)})" (is "validity ?A")
shows "validity (Subst_all ES Y (Arden Y yrhs))" (is "validity ?B")
proof -
@@ -516,24 +515,24 @@
using invariant_ES by (simp only:invariant_def soundness_def, blast)
have finite_yrhs: "finite yrhs"
using invariant_ES by (auto simp:invariant_def finite_rhs_def)
- have nonempty_yrhs: "ardenable yrhs"
+ have ardenable_yrhs: "ardenable yrhs"
using invariant_ES by (auto simp:invariant_def ardenable_all_def)
show "soundness (Subst_all ES Y (Arden Y yrhs))"
proof -
have "Y = lang_rhs (Arden Y yrhs)"
using Y_eq_yrhs invariant_ES finite_yrhs
using finite_Trn[OF finite_yrhs]
- apply(rule_tac Arden_keeps_eq)
+ apply(rule_tac Arden_preserves_soundness)
apply(simp_all)
unfolding invariant_def ardenable_all_def ardenable_def
apply(auto)
done
thus ?thesis using invariant_ES
unfolding invariant_def finite_rhs_def2 soundness_def Subst_all_def
- by (auto simp add: Subst_keeps_eq simp del: lang_rhs.simps)
+ by (auto simp add: Subst_preserves_soundness simp del: lang_rhs.simps)
qed
show "finite (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES by (simp add:invariant_def Subst_all_keeps_finite)
+ using invariant_ES by (simp add:invariant_def Subst_all_preserves_finite)
show "distinctness (Subst_all ES Y (Arden Y yrhs))"
using invariant_ES
unfolding distinctness_def Subst_all_def invariant_def by auto
@@ -543,10 +542,10 @@
assume "(X, rhs) \<in> ES"
hence "ardenable rhs" using invariant_ES
by (auto simp add:invariant_def ardenable_all_def)
- with nonempty_yrhs
+ with ardenable_yrhs
have "ardenable (Subst rhs Y (Arden Y yrhs))"
- by (simp add:nonempty_yrhs
- Subst_keeps_nonempty Arden_keeps_nonempty)
+ by (simp add:ardenable_yrhs
+ Subst_preserves_ardenable Arden_preserves_ardenable)
} thus ?thesis by (auto simp add:ardenable_all_def Subst_all_def)
qed
show "finite_rhs (Subst_all ES Y (Arden Y yrhs))"
@@ -557,13 +556,13 @@
proof -
have "finite yrhs" using invariant_ES
by (auto simp:invariant_def finite_rhs_def)
- thus ?thesis using Arden_keeps_finite by auto
+ thus ?thesis using Arden_preserves_finite by auto
qed
ultimately show ?thesis
- by (simp add:Subst_all_keeps_finite_rhs)
+ by (simp add:Subst_all_preserves_finite_rhs)
qed
show "validity (Subst_all ES Y (Arden Y yrhs))"
- using invariant_ES Subst_all_keeps_validity by (auto simp add: invariant_def)
+ using invariant_ES Subst_all_preserves_validity by (auto simp add: invariant_def)
qed
lemma Remove_in_card_measure:
@@ -734,14 +733,14 @@
by (auto, case_tac x, auto)
have "finite A" using Inv_ES unfolding A_def invariant_def finite_rhs_def
- using Arden_keeps_finite by auto
+ using Arden_preserves_finite by auto
then have fin: "finite {r. Lam r \<in> A}" by (rule finite_Lam)
have "X = lang_rhs xrhs" using Inv_ES unfolding invariant_def soundness_def
by simp
then have "X = lang_rhs A" using Inv_ES
unfolding A_def invariant_def ardenable_all_def finite_rhs_def
- by (rule_tac Arden_keeps_eq) (simp_all add: finite_Trn)
+ by (rule_tac Arden_preserves_soundness) (simp_all add: finite_Trn)
then have "X = lang_rhs {Lam r | r. Lam r \<in> A}" using eq by simp
then have "X = lang (\<Uplus>{r. Lam r \<in> A})" using fin by auto
then show "\<exists>r. X = lang r" by blast