diff -r b794db0b79db -r b1258b7d2789 Derivatives.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Derivatives.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -0,0 +1,490 @@
+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}"
+
+definition
+  Ders_set :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a 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_zero [simp]:
+  shows "Der c {} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_one [simp]:
+  shows "Der c {[]} = {}"
+unfolding Der_def
+by auto
+
+lemma Der_atom [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_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 
+    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_one) (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 
+
+
+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 str_eq_rel_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) = Plus (Times (der c r1) r2) (if nullable r1 then der c r2 else Zero)"
+| "der c (Star r) = Times (der c r) (Star r)"
+
+function 
+  ders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> 'a 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 (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)"
+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
+  "Times_set 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) = Times_set (pder c r1) r2 \<union> (if nullable r1 then pder c r2 else {})"
+| "pder c (Star r) = Times_set (pder c r) (Star r)"
+
+abbreviation
+  "pder_set c rs \<equiv> \<Union>r \<in> rs. pder c r"
+
+function 
+  pders :: "'a list \<Rightarrow> 'a rexp \<Rightarrow> ('a 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 pders_set_lang:
+  shows "(\<Union> (lang ` pder_set c rs)) = (\<Union>r \<in> rs. (\<Union>lang ` (pder c r)))"
+unfolding image_def 
+by auto
+
+lemma pders_Zero [simp]:
+  shows "pders s Zero = {Zero}"
+by (induct s rule: rev_induct) (simp_all)
+
+lemma pders_One [simp]:
+  shows "pders s One = (if s = [] then {One} else {Zero})"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_Atom [simp]:
+  shows "pders s (Atom c) = (if s = [] then {Atom c} else (if s = [c] then {One} else {Zero}))"
+by (induct s rule: rev_induct) (auto)
+
+lemma pders_Plus [simp]:
+  shows "pders s (Plus r1 r2) = (if s = [] then {Plus r1 r2} else (pders s r1) \<union> (pders s r2))"
+by (induct s rule: rev_induct) (auto)
+
+text {* Non-empty suffixes of a string *}
+
+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 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]}. P v) = (\<Union>v \<in> Suf s. P (v @ [c]))"
+by (auto simp add: conc_def)
+
+lemma pders_Times:
+  shows "pders s (Times r1 r2) \<subseteq> Times_set (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 (Times r1 r2) \<subseteq> Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2)" 
+    by fact
+  have "pders (s @ [c]) (Times r1 r2) = pder_set c (pders s (Times r1 r2))" by simp
+  also have "\<dots> \<subseteq> pder_set c (Times_set (pders s r1) r2 \<union> (\<Union>v \<in> Suf s. pders v r2))"
+    using ih by (auto) (blast)
+  also have "\<dots> = pder_set c (Times_set (pders s r1) r2) \<union> pder_set c (\<Union>v \<in> Suf s. pders v r2)"
+    by (simp)
+  also have "\<dots> = pder_set c (Times_set (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 (Times_set (pders s r1) r2) \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+    by (auto)
+  also have "\<dots> \<subseteq> Times_set (pder_set c (pders s r1)) r2 \<union> (pder c r2) \<union> (\<Union>v \<in> Suf s. pders (v @ [c]) r2)"
+    by (auto simp add: if_splits) (blast)
+  also have "\<dots> = Times_set (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. Times_set (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. Times_set (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. Times_set (pders v r) (Star r)))"
+      using ih[OF asm] by blast
+    also have "\<dots> = (\<Union>v\<in>Suf s. pder_set c (Times_set (pders v r) (Star r)))"
+      by simp
+    also have "\<dots> \<subseteq> (\<Union>v\<in>Suf s. (Times_set (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. (Times_set (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. (Times_set (pders (v @ [c]) r) (Star r))) \<union> (Times_set (pder c r) (Star r))"
+      by simp
+    also have "\<dots> = (\<Union>v\<in>Suf (s @ [c]). (Times_set (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_Zero:
+  shows "pders_set UNIV1 Zero = {Zero}"
+by auto
+
+lemma pders_set_One:
+  shows "pders_set UNIV1 One = {Zero}"
+by (auto split: if_splits)
+
+lemma pders_set_Atom:
+  shows "pders_set UNIV1 (Atom c) \<subseteq> {One, Zero}"
+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"
+by auto
+
+lemma pders_set_Times_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_Times:
+  shows "pders_set UNIV1 (Times r1 r2) \<subseteq> Times_set (pders_set UNIV1 r1) r2 \<union> pders_set UNIV1 r2"
+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(rule pders_set_Times_aux)
+apply(auto)
+done
+
+lemma pders_set_Star:
+  shows "pders_set UNIV1 (Star r) \<subseteq> Times_set (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_Times_set:
+  assumes a: "finite A"
+  shows "finite (Times_set 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_Times_set finite_Un)
+apply(simp)
+apply(rule finite_subset)
+apply(rule pders_set_Star)
+apply(simp only: finite_Times_set)
+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
+
+
+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 rule: rev_induct)
+  case (snoc c s)
+  have ih: "Ders s (lang r) = \<Union> lang ` (pders s r)" by fact
+  have "Ders (s @ [c]) (lang r) = Ders [c] (Ders s (lang r))"
+    by (simp add: Ders_append)
+  also have "\<dots> = Der c (\<Union> lang ` (pders s r))" using ih
+    by (simp add: Ders_singleton)
+  also have "\<dots> = (\<Union>r\<in>pders s r. Der c (lang r))" 
+    unfolding Der_def image_def by auto
+  also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> lang `  (pder c r)))"
+    by (simp add: Der_pder)
+  also have "\<dots> = (\<Union>lang ` (pder_set c (pders s r)))"
+    by (simp add: pders_set_lang)
+  also have "\<dots> = (\<Union>lang ` (pders (s @ [c]) r))"
+    by simp
+  finally show "Ders (s @ [c]) (lang r) = \<Union> lang ` pders (s @ [c]) r" .
+qed (simp add: Ders_def)
+
+lemma Ders_set_pders_set:
+  shows "Ders_set A (lang r) = (\<Union> lang ` (pders_set A r))"
+by (simp add: Ders_set_Ders Ders_pders)
+
+
+subsection {* Relating derivatives and partial derivatives *}
+
+lemma
+  shows "(\<Union> lang ` (pder c r)) = lang (der c r)"
+unfolding Der_der[symmetric] Der_pder by simp
+
+lemma
+  shows "(\<Union> lang ` (pders s r)) = lang (ders s r)"
+unfolding Ders_ders[symmetric] Ders_pders by simp
+
+
+
+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_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>(lang r))"
+    unfolding equiv_def refl_on_def sym_def trans_def
+    unfolding str_eq_rel_def
+    by auto
+  ultimately show "finite (UNIV // \<approx>(lang r))" 
+    by (rule refined_partition_finite)
+qed
+
+end
\ No newline at end of file