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 = {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 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 = {Zero}"

  and   "pders s One = (if s = [] then {One} else {Zero})"

  and   "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"

  and   "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"

by (induct s) (auto)

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 *}

  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"

unfolding Der_der[symmetric] Der_pder by simp

  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 *}

abbreviation

text {* Non-empty suffixes of a string *}

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)

by (simp add: Suf_Union pders_snoc)

lemma pders_Times:

proof (induct s rule: rev_induct)

  case (snoc c s)

    by fact

  have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" 

    by (simp add: pders_snoc)

    using ih by (auto) (blast)

    by (simp)

    by auto

    by (auto simp add: Suf_snoc)  

  finally show ?case .

qed (simp) 

lemma pders_Star:

  assumes a: "s \<noteq> []"

using a

proof (induct s rule: rev_induct)

  case (snoc c s)

  { assume asm: "s \<noteq> []"

    have "pders (s @ [c]) (Star r) = pder_set c (pders s (Star r))" by (simp add: pders_snoc)

      using ih[OF asm] by (auto) (blast)

      by (auto simp add: Suf_snoc Suf_Union pders_snoc)

    finally have ?case .

  }

  moreover

  { assume asm: "s = []"

    then have ?case

  }

  ultimately show ?case by blast

qed (simp)

definition

  "UNIV1 \<equiv> UNIV - {[]}"

unfolding UNIV1_def by auto

unfolding UNIV1_def by (auto split: if_splits)

unfolding UNIV1_def by (auto split: if_splits)

unfolding UNIV1_def by auto

  assumes a: "s \<in> UNIV1"

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(auto simp add: UNIV1_def)

done

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_Timess:

  assumes a: "finite A"

  shows "finite (Timess A r)"

apply(induct r)

apply(simp)

apply(simp)

apply(rule finite_subset)

apply(simp)

apply(simp)

apply(rule finite_subset)

apply(simp only: finite_Timess finite_Un)

apply(simp)

apply(rule finite_subset)

apply(simp only: finite_Timess)

done

unfolding UNIV1_def

apply(auto)

apply(rule_tac x="[]" in exI)

apply(simp)

done

apply(rule rev_finite_subset)

apply(auto)

done

lemma finite_pders:

  shows "finite (pders s r)"

by simp

lemma finite_pders2:

  shows "finite {pders s r | s. s \<in> A}"

proof -

  moreover

  ultimately 

  show "finite {pders s r | s. s \<in> A}"

    by(rule finite_subset)

qed

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

    by auto

  ultimately show "finite (UNIV // \<approx>(lang r))" 

    by (rule refined_partition_finite)

qed

end