header "Derivatives of regular expressions"+
−
+
−
(* Author: Christian Urban *)+
−
+
−
theory Derivatives+
−
imports Regular_Exp+
−
begin+
−
+
−
text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}+
−
+
−
subsection {* Left-Quotients of languages *}+
−
+
−
definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"+
−
where "Deriv x A = { xs. x#xs \<in> A }"+
−
+
−
definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"+
−
where "Derivs xs A = { ys. xs @ ys \<in> A }"+
−
+
−
abbreviation +
−
  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 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 "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 Deriv_star [simp]:+
−
  shows "Deriv c (star A) = (Deriv c A) @@ star A"+
−
proof -+
−
  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 "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"+
−
    by (simp only: star_unfold_left[symmetric])+
−
  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 "... =  (Deriv c A) @@ star A"+
−
    using incl by auto+
−
  finally show "Deriv c (star A) = (Deriv c A) @@ star A" . +
−
qed+
−
+
−
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+
−
+
−
+
−
subsection {* Brozowski's derivatives of regular expressions *}+
−
+
−
fun+
−
  nullable :: "'a rexp \<Rightarrow> bool"+
−
where+
−
  "nullable (Zero) = False"+
−
| "nullable (One) = True"+
−
| "nullable (Atom c) = False"+
−
| "nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)"+
−
| "nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)"+
−
| "nullable (Star r) = True"+
−
+
−
fun+
−
  deriv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"+
−
where+
−
  "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 +
−
  derivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"+
−
where+
−
  "derivs [] r = r"+
−
| "derivs (c # s) r = derivs s (deriv c r)"+
−
+
−
+
−
lemma nullable_iff:+
−
  shows "nullable r \<longleftrightarrow> [] \<in> lang r"+
−
by (induct r) (auto simp add: conc_def split: if_splits)+
−
+
−
lemma Deriv_deriv:+
−
  shows "Deriv c (lang r) = lang (deriv c r)"+
−
by (induct r) (simp_all add: nullable_iff)+
−
+
−
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 *}+
−
+
−
abbreviation+
−
  "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"+
−
+
−
fun+
−
  pderiv :: "'a \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp set"+
−
where+
−
  "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+
−
  pderivs :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"+
−
where+
−
  "pderivs [] r = {r}"+
−
| "pderivs (c # s) r = \<Union> (pderivs s) ` (pderiv c r)"+
−
+
−
abbreviation+
−
 pderiv_set :: "'a \<Rightarrow> 'a rexp set \<Rightarrow> 'a rexp set"+
−
where+
−
  "pderiv_set c rs \<equiv> \<Union> pderiv c ` rs"+
−
+
−
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 pderivs_snoc:+
−
  shows "pderivs (s @ [c]) r = pderiv_set c (pderivs s r)"+
−
by (simp add: pderivs_append)+
−
+
−
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 pderivs_Atom:+
−
  shows "pderivs s (Atom c) \<subseteq> {Atom c, One}"+
−
by (induct s) (simp_all)+
−
+
−
subsection {* Relating left-quotients and partial derivatives *}+
−
+
−
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 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. 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 ` (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 *}+
−
+
−
lemma deriv_pderiv:+
−
  shows "(\<Union> lang ` (pderiv c r)) = lang (deriv c r)"+
−
unfolding Deriv_deriv[symmetric] Deriv_pderiv by simp+
−
+
−
lemma derivs_pderivs:+
−
  shows "(\<Union> lang ` (pderivs s r)) = lang (derivs s r)"+
−
unfolding Derivs_derivs[symmetric] Derivs_pderivs by simp+
−
+
−
+
−
subsection {* Finiteness property of partial derivatives *}+
−
+
−
definition+
−
  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 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 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 pderivs_lang_Zero [simp]:+
−
  shows "pderivs_lang UNIV1 Zero = {}"+
−
unfolding UNIV1_def pderivs_lang_def by auto+
−
+
−
lemma pderivs_lang_One [simp]:+
−
  shows "pderivs_lang UNIV1 One = {}"+
−
unfolding UNIV1_def pderivs_lang_def by (auto split: if_splits)+
−
+
−
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 pderivs_Atom)+
−
apply(simp)+
−
apply(case_tac xa)+
−
apply(auto split: if_splits)+
−
done+
−
+
−
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 the cases of @{const Times} and @{const Star} below) *}+
−
+
−
definition+
−
  "PSuf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"+
−
+
−
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 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 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 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: "pderivs s (Times r1 r2) \<subseteq> Timess (pderivs s r1) r2 \<union> (pderivs_lang (PSuf s) r2)" +
−
    by fact+
−
  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> = pderiv_set c (Timess (pderivs s r1) r2) \<union> pderiv_set c (pderivs_lang (PSuf s) r2)"+
−
    by (simp)+
−
  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 (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 (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 pderivs_lang_Times_aux1:+
−
  assumes a: "s \<in> UNIV1"+
−
  shows "pderivs_lang (PSuf s) r \<subseteq> pderivs_lang UNIV1 r"+
−
using a unfolding UNIV1_def PSuf_def pderivs_lang_def by auto+
−
+
−
lemma pderivs_lang_Times_aux2:+
−
  assumes a: "s \<in> UNIV1"+
−
  shows "Timess (pderivs s r1) r2 \<subseteq> Timess (pderivs_lang UNIV1 r1) r2"+
−
using a unfolding pderivs_lang_def by auto+
−
+
−
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 pderivs_Times)+
−
using pderivs_lang_Times_aux1 pderivs_lang_Times_aux2+
−
apply(blast)+
−
done+
−
+
−
lemma pderivs_Star:+
−
  assumes a: "s \<noteq> []"+
−
  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> pderivs s (Star r) \<subseteq> Timess (pderivs_lang (PSuf s) r) (Star r)" by fact+
−
  { assume asm: "s \<noteq> []"+
−
    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 (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 (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: pderivs_lang_def pderivs_snoc PSuf_def)+
−
      apply(rule_tac x = "[c]" in exI)+
−
      apply(auto)+
−
      done+
−
  }+
−
  ultimately show ?case by blast+
−
qed (simp)+
−
+
−
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 pderivs_Star)+
−
apply(simp add: UNIV1_def)+
−
apply(simp add: UNIV1_def PSuf_def)+
−
apply(auto simp add: pderivs_lang_def)+
−
done+
−
+
−
lemma finite_Timess [simp]:+
−
  assumes a: "finite A"+
−
  shows "finite (Timess A r)"+
−
using a by auto+
−
+
−
lemma finite_pderivs_lang_UNIV1:+
−
  shows "finite (pderivs_lang UNIV1 r)"+
−
apply(induct r)+
−
apply(simp_all add: +
−
  finite_subset[OF pderivs_lang_Times]+
−
  finite_subset[OF pderivs_lang_Star])+
−
done+
−
    +
−
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_pderivs_lang_UNIV:+
−
  shows "finite (pderivs_lang UNIV r)"+
−
unfolding pderivs_lang_UNIV+
−
by (simp add: finite_pderivs_lang_UNIV1)+
−
+
−
lemma finite_pderivs_lang:+
−
  shows "finite (pderivs_lang A r)"+
−
by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)+
−
+
−
+
−
subsection {* A regular expression matcher based on Brozowski's derivatives *}+
−
+
−
fun+
−
  matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool"+
−
where+
−
  "matcher r s = nullable (derivs s r)"+
−
+
−
lemma matcher_correctness:+
−
  shows "matcher r s \<longleftrightarrow> s \<in> lang r"+
−
by (induct s arbitrary: r)+
−
   (simp_all add: nullable_iff Deriv_deriv[symmetric] Deriv_def)+
−
+
−
+
−
end+
−