theory Derivs

imports Myhill_2

begin

section {* Left-Quotients and Derivatives *}

subsection {* Left-Quotients *}

definition

  Delta :: "lang \<Rightarrow> lang"

where

  "Delta A = (if [] \<in> A then {[]} else {})"

definition

  Der :: "char \<Rightarrow> lang \<Rightarrow> lang"

where

  "Der c A \<equiv> {s. [c] @ s \<in> A}"

definition

  Ders :: "string \<Rightarrow> lang \<Rightarrow> lang"

where

  "Ders s A \<equiv> {s'. s @ s' \<in> A}"

definition

  Ders_set :: "lang \<Rightarrow> lang \<Rightarrow> 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_null [simp]:

  shows "Der c {} = {}"

unfolding Der_def

by auto

lemma Der_empty [simp]:

  shows "Der c {[]} = {}"

unfolding Der_def

by auto

lemma Der_char [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_seq [simp]:

  shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> Der c B)"

unfolding Der_def Delta_def

unfolding Seq_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 Seq_def

    apply(auto)

    apply(drule star_decom)

    apply(auto simp add: Cons_eq_append_conv)

    done

  have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"

    by (simp only: star_cases[symmetric])

  also have "... = Der c (A \<cdot> A\<star>)"

    by (simp only: Der_union Der_empty) (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_singleton:

  shows "Ders [c] A = Der c A"

unfolding Der_def Ders_def

by simp

lemma Ders_append:

  shows "Ders (s1 @ s2) A = Ders s2 (Ders s1 A)"

unfolding Ders_def by simp 

lemma MN_Rel_Ders:

  shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"

unfolding Ders_def str_eq_def str_eq_rel_def

by auto

subsection {* Brozowsky's derivatives of regular expressions *}

fun

  nullable :: "rexp \<Rightarrow> bool"

where

  "nullable (NULL) = False"

| "nullable (EMPTY) = True"

| "nullable (CHAR c) = False"

| "nullable (ALT r1 r2) = (nullable r1 \<or> nullable r2)"

| "nullable (SEQ r1 r2) = (nullable r1 \<and> nullable r2)"

| "nullable (STAR r) = True"

fun

  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"

where

  "der c (NULL) = NULL"

| "der c (EMPTY) = NULL"

| "der c (CHAR c') = (if c = c' then EMPTY else NULL)"

| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

| "der c (SEQ r1 r2) = ALT (SEQ (der c r1) r2) (if nullable r1 then der c r2 else NULL)"

| "der c (STAR r) = SEQ (der c r) (STAR r)"

function 

  ders :: "string \<Rightarrow> rexp \<Rightarrow> rexp"

where

  "ders [] r = r"

| "ders (s @ [c]) r = der c (ders s r)"

by (auto) (metis rev_cases)

termination

  by (relation "measure (length o fst)") (auto)

lemma Delta_nullable:

  shows "Delta (L_rexp r) = (if nullable r then {[]} else {})"

unfolding Delta_def

by (induct r) (auto simp add: Seq_def split: if_splits)

lemma Der_der:

  fixes r::rexp

  shows "Der c (L_rexp r) = L_rexp (der c r)"

by (induct r) (simp_all add: Delta_nullable)

lemma Ders_ders:

  fixes r::rexp

  shows "Ders s (L_rexp r) = L_rexp (ders s r)"

apply(induct s rule: rev_induct)

apply(simp add: Ders_def)

apply(simp only: ders.simps)

apply(simp only: Ders_append)

apply(simp only: Ders_singleton)

apply(simp only: Der_der)

done

subsection {* Antimirov's Partial Derivatives *}

abbreviation

  "SEQS R r \<equiv> {SEQ r' r | r'. r' \<in> R}"

fun

  pder :: "char \<Rightarrow> rexp \<Rightarrow> rexp set"

where

  "pder c NULL = {NULL}"

| "pder c EMPTY = {NULL}"

| "pder c (CHAR c') = (if c = c' then {EMPTY} else {NULL})"

| "pder c (ALT r1 r2) = (pder c r1) \<union> (pder c r2)"

| "pder c (SEQ r1 r2) = SEQS (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"

| "pder c (STAR r) = SEQS (pder c r) (STAR r)"

abbreviation

  "pder_set c R \<equiv> \<Union>r \<in> R. pder c r"

function 

  pders :: "string \<Rightarrow> rexp \<Rightarrow> rexp set"

where

  "pders [] r = {r}"

| "pders (s @ [c]) r = pder_set c (pders s r)"

by (auto) (metis rev_cases)

termination

  by (relation "measure (length o fst)") (auto)

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)"

apply(induct s2 arbitrary: s1 r rule: rev_induct)

apply(simp)

apply(subst append_assoc[symmetric])

apply(simp only: pders.simps)

apply(auto)

done

lemma pders_singleton:

  "pders [c] r = pder c r"

apply(subst append_Nil[symmetric])

apply(simp only: pders.simps)

apply(simp)

done

lemma pder_set_lang:

  shows "(\<Union> (L_rexp ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L_rexp ` (pder c r)))"

unfolding image_def 

by auto

lemma

  shows seq_UNION_left:  "B \<cdot> (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B \<cdot> A n)"

  and   seq_UNION_right: "(\<Union>n\<in>C. A n) \<cdot> B = (\<Union>n\<in>C. A n \<cdot> B)"

unfolding Seq_def by auto

lemma Der_pder:

  fixes r::rexp

  shows "Der c (L_rexp r) = \<Union> L_rexp ` (pder c r)"

by (induct r) (auto simp add: Delta_nullable seq_UNION_right)

lemma Ders_pders:

  fixes r::rexp

  shows "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)"

proof (induct s rule: rev_induct)

  case (snoc c s)

  have ih: "Ders s (L_rexp r) = \<Union> L_rexp ` (pders s r)" by fact

  have "Ders (s @ [c]) (L_rexp r) = Ders [c] (Ders s (L_rexp r))"

    by (simp add: Ders_append)

  also have "\<dots> = Der c (\<Union> L_rexp ` (pders s r))" using ih

    by (simp add: Ders_singleton)

  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L_rexp r))" 

    unfolding Der_def image_def by auto

  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L_rexp `  (pder c r)))"

    by (simp add: Der_pder)

  also have "\<dots> = (\<Union>L_rexp ` (pder_set c (pders s r)))"

    by (simp add: pder_set_lang)

  also have "\<dots> = (\<Union>L_rexp ` (pders (s @ [c]) r))"

    by simp

  finally show "Ders (s @ [c]) (L_rexp r) = \<Union> L_rexp ` pders (s @ [c]) r" .

qed (simp add: Ders_def)

lemma Ders_set_pders_set:

  fixes r::rexp

  shows "Ders_set A (L_rexp r) = (\<Union> L_rexp ` (pders_set A r))"

by (simp add: Ders_set_Ders Ders_pders)

lemma pders_NULL [simp]:

  shows "pders s NULL = {NULL}"

by (induct s rule: rev_induct) (simp_all)

lemma pders_EMPTY [simp]:

  shows "pders s EMPTY = (if s = [] then {EMPTY} else {NULL})"

by (induct s rule: rev_induct) (auto)

lemma pders_CHAR [simp]:

  shows "pders s (CHAR c) = (if s = [] then {CHAR c} else (if s = [c] then {EMPTY} else {NULL}))"

by (induct s rule: rev_induct) (auto)

lemma pders_ALT [simp]:

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

by (induct s rule: rev_induct) (auto)

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 Seq_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: Seq_def)

lemma inclusion1:

  shows "pder_set c (SEQS R r2) \<subseteq> SEQS (pder_set c R) r2 \<union> (pder c r2)"

apply(auto simp add: if_splits)

apply(blast)

done

lemma pders_SEQ:

  shows "pders s (SEQ r1 r2) \<subseteq> SEQS (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 (SEQ r1 r2) \<subseteq> SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 

    by fact

  have "pders (s @ [c]) (SEQ r1 r2) = pder_set c (pders s (SEQ r1 r2))" by simp

  also have "\<dots> \<subseteq> pder_set c (SEQS (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"

    using ih by (auto) (blast)

  also have "\<dots> = pder_set c (SEQS (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"

    by (simp)

  also have "\<dots> = pder_set c (SEQS (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 (SEQS (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"

    by (auto)

  also have "\<dots> \<subseteq> SEQS (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"

    using inclusion1 by blast

  also have "\<dots> = SEQS (pders (s @ [c]) r1) r2 \<union> (\<Union>v \<in> Suf (s @ [c]). pders v r2)"

    apply(subst (2) pders.simps)

    apply(simp only: Suf)

    apply(simp add: Suf_Union pders_singleton)

    apply(auto)

    done

  finally show ?case .

qed (simp)

lemma pders_STAR:

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

  shows "pders s (STAR r) \<subseteq> (\<Union>v \<in> Suf s. SEQS (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. SEQS (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

    also have "\<dots> \<subseteq> (pder_set c (\<Union>v\<in>Suf s. SEQS (pders v r) (STAR r)))"

      using ih[OF asm] by blast

    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (SEQS (pders v r) (STAR r)))"

      by simp

    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (SEQS (pder_set c (pders v r)) (STAR r) \<union> pder c (STAR r)))"

      using inclusion1 by (auto split: if_splits) 

    also have "\<dots> = (\<Union>v\<in>Suf s. (SEQS (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. (SEQS (pders (v @ [c]) r) (STAR r))) \<union> (SEQS (pder c r) (STAR r))"

      by simp

    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (SEQS (pders v r) (STAR r)))"

      apply(simp only: Suf)

      apply(simp add: Suf_Union pders_singleton)

      apply(auto)

      done

    finally have ?case .

  }

  moreover

  { assume asm: "s = []"

    then have ?case

      apply(simp add: pders_singleton Suf_def)

      apply(auto)

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

      apply(simp add: pders_singleton)

      done

  }

  ultimately show ?case by blast

qed (simp)

abbreviation 

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

lemma pders_set_NULL:

  shows "pders_set UNIV1 NULL = {NULL}"

by auto

lemma pders_set_EMPTY:

  shows "pders_set UNIV1 EMPTY = {NULL}"

by (auto split: if_splits)

lemma pders_set_CHAR:

  shows "pders_set UNIV1 (CHAR c) \<subseteq> {EMPTY, NULL}"

by (auto split: if_splits)

lemma pders_set_ALT:

  shows "pders_set UNIV1 (ALT r1 r2) = pders_set UNIV1 r1 \<union> pders_set UNIV1 r2"

by auto

lemma pders_set_SEQ_aux:

  assumes a: "s \<in> UNIV1"

  shows "pders_set (Suf s) r2 \<subseteq> pders_set UNIV1 r2"

using a by (auto simp add: Suf_def)

lemma pders_set_SEQ:

  shows "pders_set UNIV1 (SEQ r1 r2) \<subseteq> SEQS (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"

apply(rule UN_least)

apply(rule subset_trans)

apply(rule pders_SEQ)

apply(simp)

apply(rule conjI) 

apply(auto)[1]

apply(rule subset_trans)

apply(rule pders_set_SEQ_aux)

apply(auto)

done

lemma pders_set_STAR:

  shows "pders_set UNIV1 (STAR r) \<subseteq> SEQS (pders_set UNIV1 r) (STAR r)"

apply(rule UN_least)

apply(rule subset_trans)

apply(rule pders_STAR)

apply(simp)

apply(simp add: Suf_def)

apply(auto)

done

lemma finite_SEQS:

  assumes a: "finite A"

  shows "finite (SEQS 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_EMPTY)

apply(simp)

apply(rule finite_subset)

apply(rule pders_set_CHAR)

apply(simp)

apply(rule finite_subset)

apply(rule pders_set_SEQ)

apply(simp only: finite_SEQS finite_Un)

apply(simp)

apply(simp only: pders_set_ALT)

apply(simp)

apply(rule finite_subset)

apply(rule pders_set_STAR)

apply(simp only: finite_SEQS)

done

lemma pders_set_UNIV_UNIV1:

  shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"

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

lemma Myhill_Nerode3:

  fixes r::"rexp"

  shows "finite (UNIV // \<approx>(L_rexp 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>(L_rexp r)"

    unfolding tag_eq_rel_def

    unfolding str_eq_def2

    unfolding MN_Rel_Ders

    unfolding Ders_pders

    by auto

  moreover 

  have "equiv UNIV =(\<lambda>x. pders x r)="

    unfolding equiv_def refl_on_def sym_def trans_def

    unfolding tag_eq_rel_def

    by auto

  moreover

  have "equiv UNIV (\<approx>(L_rexp r))"

    unfolding equiv_def refl_on_def sym_def trans_def

    unfolding str_eq_rel_def

    by auto

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

    by (rule refined_partition_finite)

qed

section {* Relating derivatives and partial derivatives *}

lemma

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

unfolding Der_der[symmetric] Der_pder by simp

lemma

  shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)"

unfolding Ders_ders[symmetric] Ders_pders by simp

end