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

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>s \<in> A. pders s 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)

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

lemma pders_lang_Zero [simp]:
  shows "pders_lang UNIV1 Zero = {Zero}"
unfolding UNIV1_def pders_lang_def by auto

lemma pders_lang_One [simp]:
  shows "pders_lang UNIV1 One = {Zero}"
unfolding UNIV1_def pders_lang_def by (auto split: if_splits)

lemma pders_lang_Atom:
  shows "pders_lang UNIV1 (Atom c) \<subseteq> {One, Zero}"
unfolding UNIV1_def pders_lang_def by (auto split: if_splits)

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)
apply(simp)
apply(rule finite_subset[OF pders_lang_Atom])
apply(simp)
apply(simp)
apply(rule finite_subset[OF pders_lang_Times])
apply(simp)
apply(rule finite_subset[OF pders_lang_Star])
apply(simp)
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)
apply(rule_tac r="r" in finite_pders_lang_UNIV)
apply(auto simp add: pders_lang_def)
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