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}"+
−
+
−
definition+
−
  Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang"+
−
where+
−
  "Ders_set A B \<equiv> {s' | s s'. s @ s' \<in> B \<and> s \<in> A}"+
−
+
−
lemma Ders_set_Ders:+
−
  shows "Ders_set A B = (\<Union>s \<in> A. Ders s B)"+
−
unfolding Ders_set_def Ders_def+
−
by auto+
−
+
−
lemma Der_zero [simp]:+
−
  shows "Der c {} = {}"+
−
unfolding Der_def+
−
by auto+
−
+
−
lemma Der_one [simp]:+
−
  shows "Der c {[]} = {}"+
−
unfolding Der_def+
−
by auto+
−
+
−
lemma Der_atom [simp]:+
−
  shows "Der c {[d]} = (if c = d then {[]} else {})"+
−
unfolding Der_def+
−
by auto+
−
+
−
lemma Der_union [simp]:+
−
  shows "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 +
−
    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_union Der_one) (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_nil [simp]:+
−
  shows "Ders [] A = A"+
−
unfolding 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 [simp]:+
−
  shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"+
−
unfolding Ders_def by simp +
−
+
−
+
−
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+
−
  "Times_set rs r \<equiv> {Times r' r | r'. r' \<in> rs}"+
−
+
−
fun+
−
  pder :: "'a \<Rightarrow> 'a rexp \<Rightarrow> ('a rexp) set"+
−
where+
−
  "pder c Zero = {Zero}"+
−
| "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) = +
−
    (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"+
−
+
−
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+
−
  "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)"+
−
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_set_lang:+
−
  shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"+
−
unfolding image_def +
−
by auto+
−
+
−
lemma pders_Zero [simp]:+
−
  shows "pders s Zero = {Zero}"+
−
by (induct s) (simp_all)+
−
+
−
lemma pders_One [simp]:+
−
  shows "pders s One = (if s = [] then {One} else {Zero})"+
−
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) (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) (auto)+
−
+
−
text {* Non-empty suffixes of a string *}+
−
+
−
definition+
−
  "Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"+
−
+
−
lemma Suf:+
−
  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]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"+
−
by (auto simp add: conc_def)+
−
+
−
lemma pders_Times:+
−
  shows "pders s (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)"+
−
proof (induct s rule: rev_induct)+
−
  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 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)"+
−
    by (simp)+
−
  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 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)"+
−
    by (auto simp add: pders_snoc Suf Suf_Union)+
−
  finally show ?case .+
−
qed (simp)+
−
+
−
lemma pders_Star:+
−
  assumes a: "s \<noteq> []"+
−
  shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Times_set (pders v 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> (\<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 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)))"+
−
      by simp+
−
    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (pder_set c (pders v r)) (Star r) \<union> pder c (Star r)))"+
−
      by (auto split: if_splits) +
−
    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 add: pders_snoc)+
−
    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (pders v r) (Star r)))"+
−
      by (auto simp add: Suf Suf_Union pders_snoc)+
−
    finally have ?case .+
−
  }+
−
  moreover+
−
  { assume asm: "s = []"+
−
    then have ?case+
−
      by (auto simp add: pders_snoc Suf_def)+
−
  }+
−
  ultimately show ?case by blast+
−
qed (simp)+
−
+
−
definition+
−
  "UNIV1 \<equiv> UNIV - {[]}"+
−
+
−
lemma pders_set_Zero:+
−
  shows "pders_set UNIV1 Zero = {Zero}"+
−
unfolding UNIV1_def by auto+
−
+
−
lemma pders_set_One:+
−
  shows "pders_set UNIV1 One = {Zero}"+
−
unfolding UNIV1_def by (auto split: if_splits)+
−
+
−
lemma pders_set_Atom:+
−
  shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"+
−
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"+
−
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 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)+
−
apply(simp)+
−
apply(rule conjI) +
−
apply(auto)[1]+
−
apply(rule subset_trans)+
−
apply(rule pders_set_Times_aux)+
−
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)+
−
apply(simp)+
−
apply(simp add: Suf_def)+
−
apply(auto)+
−
done+
−
+
−
lemma finite_Times_set:+
−
  assumes a: "finite A"+
−
  shows "finite (Times_set A r)"+
−
using a by (auto)+
−
+
−
lemma finite_pders_set_UNIV1:+
−
  shows "finite (pders_set UNIV1 r)"+
−
apply(induct r)+
−
apply(simp)+
−
apply(simp only: pders_set_One)+
−
apply(simp)+
−
apply(rule finite_subset)+
−
apply(rule pders_set_Atom)+
−
apply(simp)+
−
apply(simp only: pders_set_Plus)+
−
apply(simp)+
−
apply(rule finite_subset)+
−
apply(rule pders_set_Times)+
−
apply(simp only: finite_Times_set finite_Un)+
−
apply(simp)+
−
apply(rule finite_subset)+
−
apply(rule pders_set_Star)+
−
apply(simp only: finite_Times_set)+
−
done+
−
    +
−
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)+
−
done+
−
+
−
lemma finite_pders_set_UNIV:+
−
  shows "finite (pders_set UNIV r)"+
−
unfolding pders_set_UNIV_UNIV1+
−
by (simp add: finite_pders_set_UNIV1)+
−
+
−
lemma finite_pders_set:+
−
  shows "finite (pders_set A r)"+
−
apply(rule rev_finite_subset)+
−
apply(rule_tac r="r" in finite_pders_set_UNIV)+
−
apply(auto)+
−
done+
−
+
−
lemma finite_pders:+
−
  shows "finite (pders s r)"+
−
using finite_pders_set[where A="{s}" and r="r"]+
−
by simp+
−
+
−
lemma finite_pders2:+
−
  shows "finite {pders s r | s. s \<in> A}"+
−
proof -+
−
  have "{pders s r | s. s \<in> A} \<subseteq> Pow (pders_set A r)" by auto+
−
  moreover+
−
  have "finite (Pow (pders_set A r))"+
−
    using finite_pders_set by simp+
−
  ultimately +
−
  show "finite {pders s r | s. s \<in> A}"+
−
    by(rule finite_subset)+
−
qed+
−
+
−
+
−
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 rule: rev_induct)+
−
  case (snoc c s)+
−
  have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact+
−
  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)+
−
  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)))"+
−
    by (simp add: Der_pder)+
−
  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 add: pders_snoc)+
−
  finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .+
−
qed (simp add: Ders_def)+
−
+
−
lemma Ders_set_pders_set:+
−
  shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"+
−
by (simp add: Ders_set_Ders Ders_pders)+
−
+
−
+
−
subsection {* Relating derivatives and partial derivatives *}+
−
+
−
lemma+
−
  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"+
−
unfolding Der_der[symmetric] Der_pder by simp+
−
+
−
lemma+
−
  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"+
−
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+
−
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) = {pders s r | s. s \<in> UNIV}" by auto+
−
    moreover +
−
    have "finite {pders s r | s. s \<in> UNIV}" by (rule finite_pders2)+
−
    ultimately+
−
    have "finite (range (\<lambda>x. pders x r))"+
−
      by simp+
−
    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)="+
−
    unfolding equiv_def refl_on_def sym_def trans_def+
−
    unfolding tag_eq_def+
−
    by auto+
−
  moreover+
−
  have "equiv UNIV (\<approx>(lang r))"+
−
    unfolding equiv_def refl_on_def sym_def trans_def+
−
    unfolding str_eq_def+
−
    by auto+
−
  ultimately show "finite (UNIV // \<approx>(lang r))" +
−
    by (rule refined_partition_finite)+
−
qed+
−
+
−
+
−
end+
−