--- a/Derivatives.thy Fri Aug 19 20:39:07 2011 +0000
+++ b/Derivatives.thy Mon Aug 22 12:49:27 2011 +0000
@@ -1,67 +1,81 @@
theory Derivatives
-imports Myhill_2
+imports Regular_Exp
begin
-section {* Left-Quotients and Derivatives *}
-
-subsection {* Left-Quotients *}
+section {* Leftquotients, Derivatives and Partial Derivatives *}
-definition
- Delta :: "'a lang \<Rightarrow> 'a lang"
-where
- "Delta A = (if [] \<in> A then {[]} else {})"
+text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}
+
+subsection {* Left-Quotients of languages *}
-definition
- Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
- "Der c A \<equiv> {s'. [c] @ s' \<in> A}"
+definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Deriv x A = { xs. x#xs \<in> A }"
-definition
- Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
-where
- "Ders s A \<equiv> {s'. s @ s' \<in> A}"
+definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Derivs xs A = { ys. xs @ ys \<in> A }"
abbreviation
- "Derss s A \<equiv> \<Union> (Ders s) ` A"
+ Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
+where
+ "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
+
+
+lemma Deriv_empty[simp]: "Deriv a {} = {}"
+ and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
+ and Deriv_char[simp]: "Deriv a {[b]} = (if a = b then {[]} else {})"
+ and Deriv_union[simp]: "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
+by (auto simp: Deriv_def)
-lemma Der_simps [simp]:
- shows "Der c {} = {}"
- and "Der c {[]} = {}"
- and "Der c {[d]} = (if c = d then {[]} else {})"
- and "Der c (A \<union> B) = Der c A \<union> Der c B"
-unfolding Der_def by auto
+lemma Deriv_conc_subset:
+"Deriv a A @@ B \<subseteq> Deriv a (A @@ B)" (is "?L \<subseteq> ?R")
+proof
+ fix w assume "w \<in> ?L"
+ then obtain u v where "w = u @ v" "a # u \<in> A" "v \<in> B"
+ by (auto simp: Deriv_def)
+ then have "a # w \<in> A @@ B"
+ by (auto intro: concI[of "a # u", simplified])
+ thus "w \<in> ?R" by (auto simp: Deriv_def)
+qed
lemma Der_conc [simp]:
- shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"
-unfolding Der_def Delta_def conc_def
+ shows "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
+unfolding Deriv_def conc_def
by (auto simp add: Cons_eq_append_conv)
-lemma Der_star [simp]:
- shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
+lemma Deriv_star [simp]:
+ shows "Deriv c (star A) = (Deriv c A) @@ star A"
proof -
- have incl: "Delta A \<cdot> Der c (A\<star>) \<subseteq> (Der c A) \<cdot> A\<star>"
- unfolding Der_def Delta_def conc_def
- apply(auto)
+ have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
+ unfolding Deriv_def conc_def
+ apply(auto simp add: Cons_eq_append_conv)
apply(drule star_decom)
apply(auto simp add: Cons_eq_append_conv)
done
-
- have "Der c (A\<star>) = Der c (A \<cdot> A\<star> \<union> {[]})"
+
+ have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
by (simp only: star_unfold_left[symmetric])
- also have "... = Der c (A \<cdot> A\<star>)"
- by (simp only: Der_simps) (simp)
- also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
+ also have "... = Deriv c (A @@ star A)"
+ by (simp only: Deriv_union) (simp)
+ also have "... = (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
by simp
- also have "... = (Der c A) \<cdot> A\<star>"
+ also have "... = (Deriv c A) @@ star A"
using incl by auto
- finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
+ finally show "Deriv c (star A) = (Deriv c A) @@ star A" .
qed
-lemma Ders_simps [simp]:
- shows "Ders [] A = A"
- and "Ders (c # s) A = Ders s (Der c A)"
- and "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"
-unfolding Ders_def Der_def by auto
+lemma Derivs_simps [simp]:
+ shows "Derivs [] A = A"
+ and "Derivs (c # s) A = Derivs s (Deriv c A)"
+ and "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
+unfolding Derivs_def Deriv_def by auto
+
+(*
+lemma Deriv_insert_eps[simp]:
+"Deriv a (insert [] A) = Deriv a A"
+by (auto simp: Deriv_def)
+*)
+
+
subsection {* Brozowsky's derivatives of regular expressions *}
@@ -76,247 +90,254 @@
| "nullable (Star r) = True"
fun
- der :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+ deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
- "der c (Zero) = Zero"
-| "der c (One) = Zero"
-| "der c (Atom c') = (if c = c' then One else Zero)"
-| "der c (Plus r1 r2) = Plus (der c r1) (der c r2)"
-| "der c (Times r1 r2) =
- (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)"
+ "deriv c (Zero) = Zero"
+| "deriv c (One) = Zero"
+| "deriv c (Atom c') = (if c = c' then One else Zero)"
+| "deriv c (Plus r1 r2) = Plus (deriv c r1) (deriv c r2)"
+| "deriv c (Times r1 r2) =
+ (if nullable r1 then Plus (Times (deriv c r1) r2) (deriv c r2) else Times (deriv c r1) r2)"
+| "deriv c (Star r) = Times (deriv c r) (Star r)"
fun
- ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
+ derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"
where
- "ders [] r = r"
-| "ders (c # s) r = ders s (der c r)"
+ "derivs [] r = r"
+| "derivs (c # s) r = derivs s (deriv c r)"
-lemma Delta_nullable:
- shows "Delta (lang r) = (if nullable r then {[]} else {})"
-unfolding Delta_def
+lemma nullable_iff:
+ shows "nullable r \<longleftrightarrow> [] \<in> lang r"
by (induct r) (auto simp add: conc_def split: if_splits)
-lemma Der_der:
- shows "Der c (lang r) = lang (der c r)"
-by (induct r) (simp_all add: Delta_nullable)
+lemma Deriv_deriv:
+ shows "Deriv c (lang r) = lang (deriv c r)"
+by (induct r) (simp_all add: nullable_iff)
-lemma Ders_ders:
- shows "Ders s (lang r) = lang (ders s r)"
-by (induct s arbitrary: r) (simp_all add: Der_der)
+lemma Derivs_derivs:
+ shows "Derivs s (lang r) = lang (derivs s r)"
+by (induct s arbitrary: r) (simp_all add: Deriv_deriv)
-subsection {* Antimirov's Partial Derivatives *}
+subsection {* Antimirov's partial derivivatives *}
abbreviation
"Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"
fun
- pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+ pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
where
- "pder c Zero = {}"
-| "pder c One = {}"
-| "pder c (Atom c') = (if c = c' then {One} else {})"
-| "pder c (Plus r1 r2) = (pder c r1) \<union> (pder c r2)"
-| "pder c (Times r1 r2) =
- (if nullable r1 then Timess (pder c r1) r2 \<union> pder c r2 else Timess (pder c r1) r2)"
-| "pder c (Star r) = Timess (pder c r) (Star r)"
-
-abbreviation
- "pder_set c rs \<equiv> \<Union> pder c ` rs"
+ "pderiv c Zero = {}"
+| "pderiv c One = {}"
+| "pderiv c (Atom c') = (if c = c' then {One} else {})"
+| "pderiv c (Plus r1 r2) = (pderiv c r1) \<union> (pderiv c r2)"
+| "pderiv c (Times r1 r2) =
+ (if nullable r1 then Timess (pderiv c r1) r2 \<union> pderiv c r2 else Timess (pderiv c r1) r2)"
+| "pderiv c (Star r) = Timess (pderiv c r) (Star r)"
fun
- pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
+ pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"
where
- "pders [] r = {r}"
-| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"
+ "pderivs [] r = {r}"
+| "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)"
abbreviation
- "pderss s A \<equiv> \<Union> (pders s) ` A"
+ pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
+where
+ "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs"
-lemma pders_append:
- "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders s1 r)"
+abbreviation
+ pderivs_set :: "'a list \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"
+where
+ "pderivs_set s rs \<equiv> \<Union> (pderivs s) ` rs"
+
+lemma pderivs_append:
+ "pderivs (s1 @ s2) r = \<Union> (pderivs s2) ` (pderivs s1 r)"
by (induct s1 arbitrary: r) (simp_all)
-lemma pders_snoc:
- shows "pders (s @ [c]) r = pder_set c (pders s r)"
-by (simp add: pders_append)
+lemma pderivs_snoc:
+ shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"
+by (simp add: pderivs_append)
-lemma pders_simps [simp]:
- shows "pders s Zero = (if s= [] then {Zero} else {})"
- and "pders s One = (if s = [] then {One} else {})"
- and "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
+lemma pderivs_simps [simp]:
+ shows "pderivs s Zero = (if s = [] then {Zero} else {})"
+ and "pderivs s One = (if s = [] then {One} else {})"
+ and "pderivs s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pderivs s r1) \<union> (pderivs s r2))"
by (induct s) (simp_all)
-lemma pders_Atom [intro]:
- shows "pders s (Atom c) \<subseteq> {Atom c, One}"
+lemma pderivs_Atom:
+ shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"
by (induct s) (simp_all)
-subsection {* Relating left-quotients and partial derivatives *}
+subsection {* Relating left-quotients and partial derivivatives *}
-lemma Der_pder:
- shows "Der c (lang r) = \<Union> lang ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable conc_UNION_distrib)
+lemma Deriv_pderiv:
+ shows "Deriv c (lang r) = \<Union> lang ` (pderiv c r)"
+by (induct r) (auto simp add: nullable_iff conc_UNION_distrib)
-lemma Ders_pders:
- shows "Ders s (lang r) = \<Union> lang ` (pders s r)"
+lemma Derivs_pderivs:
+ shows "Derivs s (lang r) = \<Union> lang ` (pderivs s r)"
proof (induct s arbitrary: r)
case (Cons c s)
- have ih: "\<And>r. Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
- have "Ders (c # s) (lang r) = Ders s (Der c (lang r))" by simp
- also have "\<dots> = Ders s (\<Union> lang ` (pder c r))" by (simp add: Der_pder)
- also have "\<dots> = Derss s (lang ` (pder c r))"
- by (auto simp add: Ders_def)
- also have "\<dots> = \<Union> lang ` (pderss s (pder c r))"
+ have ih: "\<And>r. Derivs s (lang r) = \<Union> lang ` (pderivs s r)" by fact
+ have "Derivs (c # s) (lang r) = Derivs s (Deriv c (lang r))" by simp
+ also have "\<dots> = Derivs s (\<Union> lang ` (pderiv c r))" by (simp add: Deriv_pderiv)
+ also have "\<dots> = Derivss s (lang ` (pderiv c r))"
+ by (auto simp add: Derivs_def)
+ also have "\<dots> = \<Union> lang ` (pderivs_set s (pderiv c r))"
using ih by auto
- also have "\<dots> = \<Union> lang ` (pders (c # s) r)" by simp
- finally show "Ders (c # s) (lang r) = \<Union> lang ` pders (c # s) r" .
-qed (simp add: Ders_def)
+ also have "\<dots> = \<Union> lang ` (pderivs (c # s) r)" by simp
+ finally show "Derivs (c # s) (lang r) = \<Union> lang ` pderivs (c # s) r" .
+qed (simp add: Derivs_def)
-subsection {* Relating derivatives and partial derivatives *}
+subsection {* Relating derivivatives and partial derivivatives *}
-lemma der_pder:
- shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
+lemma deriv_pderiv:
+ shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)"
+unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp
-lemma ders_pders:
- shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
+lemma derivs_pderivs:
+ shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)"
+unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp
-subsection {* There are only finitely many partial derivatives for a language *}
+subsection {* Finiteness property of partial derivivatives *}
definition
- "pders_lang A r \<equiv> \<Union>x \<in> A. pders x r"
-
-lemma pders_lang_subsetI [intro]:
- assumes "\<And>s. s \<in> A \<Longrightarrow> pders s r \<subseteq> C"
- shows "pders_lang A r \<subseteq> C"
-using assms unfolding pders_lang_def by (rule UN_least)
+ pderivs_lang :: "'a lang \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"
+where
+ "pderivs_lang A r \<equiv> \<Union>x \<in> A. pderivs x r"
-lemma pders_lang_union:
- shows "pders_lang (A \<union> B) r = (pders_lang A r \<union> pders_lang B r)"
-by (simp add: pders_lang_def)
+lemma pderivs_lang_subsetI:
+ assumes "\<And>s. s \<in> A \<Longrightarrow> pderivs s r \<subseteq> C"
+ shows "pderivs_lang A r \<subseteq> C"
+using assms unfolding pderivs_lang_def by (rule UN_least)
-lemma pders_lang_subset:
- shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r"
-by (auto simp add: pders_lang_def)
+lemma pderivs_lang_union:
+ shows "pderivs_lang (A \<union> B) r = (pderivs_lang A r \<union> pderivs_lang B r)"
+by (simp add: pderivs_lang_def)
+
+lemma pderivs_lang_subset:
+ shows "A \<subseteq> B \<Longrightarrow> pderivs_lang A r \<subseteq> pderivs_lang B r"
+by (auto simp add: pderivs_lang_def)
definition
"UNIV1 \<equiv> UNIV - {[]}"
-lemma pders_lang_Zero [simp]:
- shows "pders_lang UNIV1 Zero = {}"
-unfolding UNIV1_def pders_lang_def by auto
+lemma pderivs_lang_Zero [simp]:
+ shows "pderivs_lang UNIV1 Zero = {}"
+unfolding UNIV1_def pderivs_lang_def by auto
-lemma pders_lang_One [simp]:
- shows "pders_lang UNIV1 One = {}"
-unfolding UNIV1_def pders_lang_def by (auto split: if_splits)
+lemma pderivs_lang_One [simp]:
+ shows "pderivs_lang UNIV1 One = {}"
+unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)
-lemma pders_lang_Atom [simp]:
- shows "pders_lang UNIV1 (Atom c) = {One}"
-unfolding UNIV1_def pders_lang_def
+lemma pderivs_lang_Atom [simp]:
+ shows "pderivs_lang UNIV1 (Atom c) = {One}"
+unfolding UNIV1_def pderivs_lang_def
apply(auto)
apply(frule rev_subsetD)
-apply(rule pders_Atom)
+apply(rule pderivs_Atom)
apply(simp)
apply(case_tac xa)
apply(auto split: if_splits)
done
-lemma pders_lang_Plus [simp]:
- shows "pders_lang UNIV1 (Plus r1 r2) = pders_lang UNIV1 r1 \<union> pders_lang UNIV1 r2"
-unfolding UNIV1_def pders_lang_def by auto
+lemma pderivs_lang_Plus [simp]:
+ shows "pderivs_lang UNIV1 (Plus r1 r2) = pderivs_lang UNIV1 r1 \<union> pderivs_lang UNIV1 r2"
+unfolding UNIV1_def pderivs_lang_def by auto
text {* Non-empty suffixes of a string (needed for teh cases of @{const Times} and @{const Star} *}
definition
- "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
+ "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
-lemma Suf_snoc:
- shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"
-unfolding Suf_def conc_def
+lemma PSuf_snoc:
+ shows "PSuf (s @ [c]) = (PSuf s) @@ {[c]} \<union> {[c]}"
+unfolding PSuf_def conc_def
by (auto simp add: append_eq_append_conv2 append_eq_Cons_conv)
-lemma Suf_Union:
- shows "(\<Union>v \<in> Suf s \<cdot> {[c]}. f v) = (\<Union>v \<in> Suf s. f (v @ [c]))"
+lemma PSuf_Union:
+ shows "(\<Union>v \<in> PSuf s @@ {[c]}. f v) = (\<Union>v \<in> PSuf s. f (v @ [c]))"
by (auto simp add: conc_def)
-lemma pders_lang_snoc:
- shows "pders_lang (Suf s \<cdot> {[c]}) r = (pder_set c (pders_lang (Suf s) r))"
-unfolding pders_lang_def
-by (simp add: Suf_Union pders_snoc)
+lemma pderivs_lang_snoc:
+ shows "pderivs_lang (PSuf s @@ {[c]}) r = (pderiv_set c (pderivs_lang (PSuf s) r))"
+unfolding pderivs_lang_def
+by (simp add: PSuf_Union pderivs_snoc)
-lemma pders_Times:
- shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
+lemma pderivs_Times:
+ shows "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2)"
+ have ih: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)"
by fact
- 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 (Timess (pders s r1) r2 \<union> (pders_lang (Suf s) r2))"
+ have "pderivs (s @ [c]) (Times r1 r2) = pderiv_set c (pderivs s (Times r1 r2))"
+ by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2))"
using ih by (auto) (blast)
- also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_lang (Suf s) r2)"
+ also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"
by (simp)
- also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
- by (simp add: pders_lang_snoc)
- also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+ also have "\<dots> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
+ by (simp add: pderivs_lang_snoc)
+ also
+ have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
by auto
- also have "\<dots> \<subseteq> Timess (pder_set c (pders s r1)) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
+ also
+ have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs s r1)) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
by (auto simp add: if_splits) (blast)
- also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_lang (Suf s \<cdot> {[c]}) r2"
- by (simp add: pders_snoc)
- also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"
- unfolding pders_lang_def by (auto simp add: Suf_snoc)
+ also have "\<dots> = Timess (pderivs (s @ [c]) r1) r2 \<union> pderiv c r2 \<union> pderivs_lang (PSuf s @@ {[c]}) r2"
+ by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> Timess (pderivs (s @ [c]) r1) r2 \<union> pderivs_lang (PSuf (s @ [c])) r2"
+ unfolding pderivs_lang_def by (auto simp add: PSuf_snoc)
finally show ?case .
qed (simp)
-lemma pders_lang_Times_aux1:
+lemma pderivs_lang_Times_aux1:
assumes a: "s \<in> UNIV1"
- shows "pders_lang (Suf s) r \<subseteq> pders_lang UNIV1 r"
-using a unfolding UNIV1_def Suf_def pders_lang_def by auto
+ shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"
+using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto
-lemma pders_lang_Times_aux2:
+lemma pderivs_lang_Times_aux2:
assumes a: "s \<in> UNIV1"
- shows "Timess (pders s r1) r2 \<subseteq> Timess (pders_lang UNIV1 r1) r2"
-using a unfolding pders_lang_def by auto
+ shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"
+using a unfolding pderivs_lang_def by auto
-lemma pders_lang_Times [intro]:
- shows "pders_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pders_lang UNIV1 r1) r2 \<union> pders_lang UNIV1 r2"
-apply(rule pders_lang_subsetI)
+lemma pderivs_lang_Times:
+ shows "pderivs_lang UNIV1 (Times r1 r2) \<subseteq> Timess (pderivs_lang UNIV1 r1) r2 \<union> pderivs_lang UNIV1 r2"
+apply(rule pderivs_lang_subsetI)
apply(rule subset_trans)
-apply(rule pders_Times)
-using pders_lang_Times_aux1 pders_lang_Times_aux2
+apply(rule pderivs_Times)
+using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2
apply(blast)
done
-lemma pders_Star:
+lemma pderivs_Star:
assumes a: "s \<noteq> []"
- shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)"
+ shows "pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)"
using a
proof (induct s rule: rev_induct)
case (snoc c s)
- have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> Timess (pders_lang (Suf s) r) (Star r)" by fact
+ have ih: "s \<noteq> [] \<Longrightarrow> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact
{ assume asm: "s \<noteq> []"
- 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 (Timess (pders_lang (Suf s) r) (Star r))"
+ have "pderivs (s @ [c]) (Star r) = pderiv_set c (pderivs s (Star r))" by (simp add: pderivs_snoc)
+ also have "\<dots> \<subseteq> pderiv_set c (Timess (pderivs_lang (PSuf s) r) (Star r))"
using ih[OF asm] by (auto) (blast)
- also have "\<dots> \<subseteq> Timess (pder_set c (pders_lang (Suf s) r)) (Star r) \<union> pder c (Star r)"
+ also have "\<dots> \<subseteq> Timess (pderiv_set c (pderivs_lang (PSuf s) r)) (Star r) \<union> pderiv c (Star r)"
by (auto split: if_splits) (blast)+
- also have "\<dots> \<subseteq> Timess (pders_lang (Suf (s @ [c])) r) (Star r) \<union> (Timess (pder c r) (Star r))"
- by (simp only: Suf_snoc pders_lang_snoc pders_lang_union)
- (auto simp add: pders_lang_def)
- also have "\<dots> = Timess (pders_lang (Suf (s @ [c])) r) (Star r)"
- by (auto simp add: Suf_snoc Suf_Union pders_snoc pders_lang_def)
+ also have "\<dots> \<subseteq> Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r) \<union> (Timess (pderiv c r) (Star r))"
+ by (simp only: PSuf_snoc pderivs_lang_snoc pderivs_lang_union)
+ (auto simp add: pderivs_lang_def)
+ also have "\<dots> = Timess (pderivs_lang (PSuf (s @ [c])) r) (Star r)"
+ by (auto simp add: PSuf_snoc PSuf_Union pderivs_snoc pderivs_lang_def)
finally have ?case .
}
moreover
{ assume asm: "s = []"
then have ?case
- apply (auto simp add: pders_lang_def pders_snoc Suf_def)
+ apply (auto simp add: pderivs_lang_def pderivs_snoc PSuf_def)
apply(rule_tac x = "[c]" in exI)
apply(auto)
done
@@ -324,14 +345,14 @@
ultimately show ?case by blast
qed (simp)
-lemma pders_lang_Star [intro]:
- shows "pders_lang UNIV1 (Star r) \<subseteq> Timess (pders_lang UNIV1 r) (Star r)"
-apply(rule pders_lang_subsetI)
+lemma pderivs_lang_Star:
+ shows "pderivs_lang UNIV1 (Star r) \<subseteq> Timess (pderivs_lang UNIV1 r) (Star r)"
+apply(rule pderivs_lang_subsetI)
apply(rule subset_trans)
-apply(rule pders_Star)
+apply(rule pderivs_Star)
apply(simp add: UNIV1_def)
-apply(simp add: UNIV1_def Suf_def)
-apply(auto simp add: pders_lang_def)
+apply(simp add: UNIV1_def PSuf_def)
+apply(auto simp add: pderivs_lang_def)
done
lemma finite_Timess [simp]:
@@ -339,72 +360,27 @@
shows "finite (Timess A r)"
using a by auto
-lemma finite_pders_lang_UNIV1:
- shows "finite (pders_lang UNIV1 r)"
+lemma finite_pderivs_lang_UNIV1:
+ shows "finite (pderivs_lang UNIV1 r)"
apply(induct r)
apply(simp_all add:
- finite_subset[OF pders_lang_Times]
- finite_subset[OF pders_lang_Star])
+ finite_subset[OF pderivs_lang_Times]
+ finite_subset[OF pderivs_lang_Star])
done
-lemma pders_lang_UNIV:
- shows "pders_lang UNIV r = pders [] r \<union> pders_lang UNIV1 r"
-unfolding UNIV1_def pders_lang_def
+lemma pderivs_lang_UNIV:
+ shows "pderivs_lang UNIV r = pderivs [] r \<union> pderivs_lang UNIV1 r"
+unfolding UNIV1_def pderivs_lang_def
by blast
-lemma finite_pders_lang_UNIV:
- shows "finite (pders_lang UNIV r)"
-unfolding pders_lang_UNIV
-by (simp add: finite_pders_lang_UNIV1)
-
-lemma finite_pders_lang:
- shows "finite (pders_lang A r)"
-apply(rule rev_finite_subset[OF finite_pders_lang_UNIV])
-apply(rule pders_lang_subset)
-apply(simp)
-done
-
-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
-by auto
-
-subsection {*
- The second direction of the Myhill-Nerode theorem using
- partial derivatives.
-*}
+lemma finite_pderivs_lang_UNIV:
+ shows "finite (pderivs_lang UNIV r)"
+unfolding pderivs_lang_UNIV
+by (simp add: finite_pderivs_lang_UNIV1)
-lemma Myhill_Nerode3:
- fixes r::"'a rexp"
- shows "finite (UNIV // \<approx>(lang r))"
-proof -
- have "finite (UNIV // =(\<lambda>x. pders x r)=)"
- proof -
- have "range (\<lambda>x. pders x r) \<subseteq> Pow (pders_lang UNIV r)"
- unfolding pders_lang_def by auto
- moreover
- have "finite (Pow (pders_lang UNIV r))" by (simp add: finite_pders_lang)
- ultimately
- have "finite (range (\<lambda>x. pders x r))"
- by (simp add: finite_subset)
- then show "finite (UNIV // =(\<lambda>x. pders x r)=)"
- by (rule finite_eq_tag_rel)
- qed
- moreover
- have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
- unfolding tag_eq_def
- by (auto simp add: MN_Rel_Ders Ders_pders)
- moreover
- have "equiv UNIV =(\<lambda>x. pders x r)="
- and "equiv UNIV (\<approx>(lang r))"
- unfolding equiv_def refl_on_def sym_def trans_def
- unfolding tag_eq_def str_eq_def
- by auto
- ultimately show "finite (UNIV // \<approx>(lang r))"
- by (rule refined_partition_finite)
-qed
+lemma finite_pderivs_lang:
+ shows "finite (pderivs_lang A r)"
+by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
end
\ No newline at end of file