theory Derivsimports Myhill_2beginsection {* 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_defby autolemma Der_null [simp]: shows "Der c {} = {}"unfolding Der_defby autolemma Der_empty [simp]: shows "Der c {[]} = {}"unfolding Der_defby autolemma Der_char [simp]: shows "Der c {[d]} = (if c = d then {[]} else {})"unfolding Der_defby autolemma Der_union [simp]: shows "Der c (A \<union> B) = Der c A \<union> Der c B"unfolding Der_defby autolemma 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_defunfolding Seq_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 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>" . qedlemma Ders_singleton: shows "Ders [c] A = Der c A"unfolding Der_def Ders_defby simplemma 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_defby autosubsection {* 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_defby (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)donesubsection {* 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)donelemma pders_singleton: "pders [c] r = pder c r"apply(subst append_Nil[symmetric])apply(simp only: pders.simps)apply(simp)donelemma 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 autolemma 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 autolemma 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_defby (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)donelemma 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 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. 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 blastqed (simp)abbreviation "UNIV1 \<equiv> UNIV - {[]}"lemma pders_set_NULL: shows "pders_set UNIV1 NULL = {NULL}"by autolemma 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 autolemma 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)donelemma 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)donelemma 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)donelemma 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)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)qedlemma 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)qedsection {* 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 simplemma shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)"unfolding Ders_ders[symmetric] Ders_pders by simpend