theory Derivativesimports Myhill_2beginsection {* 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 autolemma 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_defby (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>" . qedlemma 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 autosubsection {* 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_defby (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 shows "(\<Union> lang ` (pder c r)) = lang (der c r)"unfolding Der_der[symmetric] Der_pder by simplemma shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"unfolding Ders_ders[symmetric] Ders_pders by simpsubsection {* There are only finitely many partial derivatives for a language *}abbreviation "pders_set A r \<equiv> \<Union>s \<in> A. pders s r"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_defby (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_set_snoc: shows "pders_set (Suf s \<cdot> {[c]}) r = (pder_set c (pders_set (Suf s) r))"by (simp add: Suf_Union pders_snoc)lemma pders_Times: shows "pders s (Times r1 r2) \<subseteq> Timess (pders s r1) r2 \<union> (pders_set (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_set (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_set (Suf s) r2))" using ih by (auto) (blast) also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pder_set c (pders_set (Suf s) r2)" by (simp) also have "\<dots> = pder_set c (Timess (pders s r1) r2) \<union> pders_set (Suf s \<cdot> {[c]}) r2" by (simp add: pders_set_snoc) also have "\<dots> \<subseteq> pder_set c (Timess (pders s r1) r2) \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2" by auto also have "\<dots> \<subseteq> Timess (pders (s @ [c]) r1) r2 \<union> pder c r2 \<union> pders_set (Suf s \<cdot> {[c]}) r2" by (auto simp add: if_splits pders_snoc) (blast) also have "\<dots> = Timess (pders (s @ [c]) r1) r2 \<union> pders_set (Suf (s @ [c])) r2" by (auto simp add: Suf_snoc) finally show ?case .qed (simp) lemma pders_Star: assumes a: "s \<noteq> []" shows "pders s (Star r) \<subseteq> (\<Union>v \<in> Suf s. Timess (pders v r) (Star r))"using aproof (induct s rule: rev_induct) case (snoc c s) have ih: "s \<noteq> [] \<Longrightarrow> pders s (Star r) \<subseteq> (\<Union>v\<in>Suf s. Timess (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. Timess (pders v r) (Star r)))" using ih[OF asm] by (auto) (blast) also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Timess (pders v r) (Star r)))" by simp also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Timess (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. (Timess (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. (Timess (pders (v @ [c]) r) (Star r))) \<union> (Timess (pder c r) (Star r))" by (simp add: pders_snoc) also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Timess (pders v r) (Star r)))" by (auto simp add: Suf_snoc 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 blastqed (simp)definition "UNIV1 \<equiv> UNIV - {[]}"lemma pders_set_Zero: shows "pders_set UNIV1 Zero = {Zero}"unfolding UNIV1_def by autolemma 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 autolemma 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> Timess (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"unfolding UNIV1_defapply(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)donelemma pders_set_Star: shows "pders_set UNIV1 (Star r) \<subseteq> Timess (pders_set UNIV1 r) (Star r)"unfolding UNIV1_defapply(rule UN_least)apply(rule subset_trans)apply(rule pders_Star)apply(simp)apply(simp add: Suf_def)apply(auto)donelemma finite_Timess: assumes a: "finite A" shows "finite (Timess 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_Timess finite_Un)apply(simp)apply(rule finite_subset)apply(rule pders_set_Star)apply(simp only: finite_Timess)donelemma pders_set_UNIV_UNIV1: shows "pders_set UNIV r = pders [] r \<union> pders_set UNIV1 r"unfolding UNIV1_defapply(auto)apply(rule_tac x="[]" in exI)apply(simp)donelemma finite_pders_set_UNIV: shows "finite (pders_set UNIV r)"unfolding pders_set_UNIV_UNIV1by (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)donelemma finite_pders: shows "finite (pders s r)"using finite_pders_set[where A="{s}" and r="r"]by simplemma 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)qedtext {* 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_defby autosubsection {* 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)qedend