theory Derivatives+
−
imports Myhill_2+
−
begin+
−
+
−
section {* Left-Quotients and Derivatives *}+
−
+
−
subsection {* Left-Quotients *}+
−
+
−
definition+
−
  Delta :: "'a lang \<Rightarrow> 'a lang"+
−
where+
−
  "Delta A = (if [] \<in> A then {[]} else {})"+
−
+
−
definition+
−
  Der :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"+
−
where+
−
  "Der c A \<equiv> {s'. [c] @ s' \<in> A}"+
−
+
−
definition+
−
  Ders :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"+
−
where+
−
  "Ders s A \<equiv> {s'. s @ s' \<in> A}"+
−
+
−
abbreviation +
−
  "Derss s A \<equiv> \<Union> (Ders s) ` A"+
−
+
−
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 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+
−
by (auto simp add: Cons_eq_append_conv)+
−
+
−
lemma Der_star [simp]:+
−
  shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"+
−
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)+
−
    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> {[]})"+
−
    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>))"+
−
    by simp+
−
  also have "... =  (Der c A) \<cdot> A\<star>"+
−
    using incl by auto+
−
  finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" . +
−
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+
−
+
−
subsection {* Brozowsky'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+
−
  der :: "'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)"+
−
+
−
fun +
−
  ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a rexp"+
−
where+
−
  "ders [] r = r"+
−
| "ders (c # s) r = ders s (der c r)"+
−
+
−
+
−
lemma Delta_nullable:+
−
  shows "Delta (lang r) = (if nullable r then {[]} else {})"+
−
unfolding Delta_def+
−
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 Ders_ders:+
−
  shows "Ders s (lang r) = lang (ders s r)"+
−
by (induct s arbitrary: r) (simp_all add: Der_der)+
−
+
−
+
−
subsection {* Antimirov's Partial Derivatives *}+
−
+
−
abbreviation+
−
  "Timess rs r \<equiv> {Times r' r | r'. r' \<in> rs}"+
−
+
−
fun+
−
  pder :: "'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"+
−
+
−
fun+
−
  pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"+
−
where+
−
  "pders [] r = {r}"+
−
| "pders (c # s) r = \<Union> (pders s) ` (pder c r)"+
−
+
−
abbreviation+
−
  "pderss s A \<equiv> \<Union> (pders s) ` A"+
−
+
−
lemma pders_append:+
−
  "pders (s1 @ s2) r = \<Union> (pders s2) ` (pders 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 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))"+
−
by (induct s) (simp_all)+
−
+
−
lemma pders_Atom [intro]:+
−
  shows "pders s (Atom c) \<subseteq> {Atom c, One}"+
−
by (induct s) (simp_all)+
−
+
−
subsection {* Relating left-quotients and partial derivatives *}+
−
+
−
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 Ders_pders:+
−
  shows "Ders s (lang r) = \<Union> lang ` (pders 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))"+
−
    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)+
−
+
−
subsection {* Relating derivatives and partial derivatives *}+
−
+
−
lemma der_pder:+
−
  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"+
−
unfolding Der_der[symmetric] Der_pder by simp+
−
+
−
lemma ders_pders:+
−
  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"+
−
unfolding Ders_ders[symmetric] Ders_pders by simp+
−
+
−
+
−
subsection {* There are only finitely many partial derivatives for a language *}+
−
+
−
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)+
−
+
−
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 pders_lang_subset:+
−
  shows "A \<subseteq> B \<Longrightarrow> pders_lang A r \<subseteq> pders_lang B r"+
−
by (auto simp add: pders_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 pders_lang_One [simp]:+
−
  shows "pders_lang UNIV1 One = {}"+
−
unfolding UNIV1_def pders_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 +
−
apply(auto)+
−
apply(frule rev_subsetD)+
−
apply(rule pders_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+
−
+
−
+
−
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)}"+
−
+
−
lemma Suf_snoc:+
−
  shows "Suf (s @ [c]) = (Suf s) \<cdot> {[c]} \<union> {[c]}"+
−
unfolding Suf_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]))"+
−
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 pders_Times:+
−
  shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_lang (Suf 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)" +
−
    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))"+
−
    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)"+
−
    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"+
−
    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"+
−
    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> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pders_lang (Suf (s @ [c])) r2"+
−
    unfolding pders_lang_def by (auto simp add: Suf_snoc)  +
−
  finally show ?case .+
−
qed (simp) +
−
+
−
lemma pders_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+
−
+
−
lemma pders_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+
−
+
−
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)+
−
apply(rule subset_trans)+
−
apply(rule pders_Times)+
−
using pders_lang_Times_aux1 pders_lang_Times_aux2+
−
apply(blast)+
−
done+
−
+
−
lemma pders_Star:+
−
  assumes a: "s \<noteq> []"+
−
  shows "pders s (Star r) \<subseteq> Timess (pders_lang (Suf 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+
−
  { 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))"+
−
      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)"+
−
      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)+
−
    finally have ?case .+
−
  }+
−
  moreover+
−
  { assume asm: "s = []"+
−
    then have ?case+
−
      apply (auto simp add: pders_lang_def pders_snoc Suf_def)+
−
      apply(rule_tac x = "[c]" in exI)+
−
      apply(auto)+
−
      done+
−
  }+
−
  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)+
−
apply(rule subset_trans)+
−
apply(rule pders_Star)+
−
apply(simp add: UNIV1_def)+
−
apply(simp add: UNIV1_def Suf_def)+
−
apply(auto simp add: pders_lang_def)+
−
done+
−
+
−
lemma finite_Timess [simp]:+
−
  assumes a: "finite A"+
−
  shows "finite (Timess A r)"+
−
using a by auto+
−
+
−
lemma finite_pders_lang_UNIV1:+
−
  shows "finite (pders_lang UNIV1 r)"+
−
apply(induct r)+
−
apply(simp_all add: +
−
  finite_subset[OF pders_lang_Times]+
−
  finite_subset[OF pders_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+
−
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 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+
−
+
−
+
−
end+
−