--- a/Theories/Derivs.thy Tue May 31 20:32:49 2011 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,521 +0,0 @@
-theory Derivs
-imports Closure
-begin
-
-section {* Experiments with Derivatives -- independent of Myhill-Nerode *}
-
-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 ;; B) = (Der c A) ;; B \<union> (Delta A ;; 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) ;; A\<star>"
-apply(subst star_cases)
-apply(simp only: Delta_def Der_union Der_seq Der_empty)
-apply(simp add: Der_def Seq_def)
-apply(auto)
-apply(drule star_decom)
-apply(auto simp add: Cons_eq_append_conv)
-done
-
-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 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 r) = L (der c r)"
-by (induct r) (simp_all add: Delta_nullable)
-
-lemma Ders_ders:
- fixes r::rexp
- shows "Ders s (L r) = L (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 ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))"
-unfolding image_def
-by auto
-
-lemma
- shows seq_UNION_left: "B ;; (\<Union>n\<in>C. A n) = (\<Union>n\<in>C. B ;; A n)"
- and seq_UNION_right: "(\<Union>n\<in>C. A n) ;; B = (\<Union>n\<in>C. A n ;; B)"
-unfolding Seq_def by auto
-
-lemma Der_pder:
- fixes r::rexp
- shows "Der c (L r) = \<Union> L ` (pder c r)"
-by (induct r) (auto simp add: Delta_nullable seq_UNION_right)
-
-lemma Ders_pders:
- fixes r::rexp
- shows "Ders s (L r) = \<Union> L ` (pders s r)"
-proof (induct s rule: rev_induct)
- case (snoc c s)
- have ih: "Ders s (L r) = \<Union> L ` (pders s r)" by fact
- have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"
- by (simp add: Ders_append)
- also have "\<dots> = Der c (\<Union> L ` (pders s r))" using ih
- by (simp add: Ders_singleton)
- also have "\<dots> = (\<Union>r\<in>pders s r. Der c (L r))"
- unfolding Der_def image_def by auto
- also have "\<dots> = (\<Union>r\<in>pders s r. (\<Union> L ` (pder c r)))"
- by (simp add: Der_pder)
- also have "\<dots> = (\<Union>L ` (pder_set c (pders s r)))"
- by (simp add: pder_set_lang)
- also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))"
- by simp
- finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" .
-qed (simp add: Ders_def)
-
-lemma Ders_set_pders_set:
- fixes r::rexp
- shows "Ders_set A (L r) = (\<Union> L ` (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) ;; {[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 ;; {[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
- 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 blast
- 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 test:
- shows "pders_set A r = (\<Union> {pders s r | s. s \<in> A})"
-by auto
-
-lemma finite_pow_pders:
- shows "finite (Pow (\<Union> {pders s r | s. s \<in> A}))"
-using finite_pders_set
-by (simp add: test)
-
-lemma test2:
- shows "{pders s r | s. s \<in> A} \<subseteq> Pow (\<Union> {pders s r | s. s \<in> A})"
- by auto
-
-lemma test3:
- shows "finite ({pders s r | s. s \<in> A})"
-apply(rule finite_subset)
-apply(rule test2)
-apply(rule finite_pow_pders)
-done
-
-lemma Myhill_Nerode_aux:
- fixes r::"rexp"
- shows "finite (UNIV // =(\<lambda>x. pders x r)=)"
-apply(rule finite_eq_tag_rel)
-apply(rule rev_finite_subset)
-apply(rule test3)
-apply(auto)
-done
-
-lemma Myhill_Nerode3:
- fixes r::"rexp"
- shows "finite (UNIV // \<approx>(L r))"
-apply(rule refined_partition_finite)
-apply(rule Myhill_Nerode_aux[where r="r"])
-apply(simp add: tag_eq_rel_def)
-apply(auto)[1]
-unfolding str_eq_def[symmetric]
-unfolding MN_Rel_Ders
-apply(simp add: Ders_pders)
-apply(rule equivI)
-apply(auto simp add: tag_eq_rel_def refl_on_def sym_def trans_def)
-apply(rule equivI)
-apply(auto simp add: str_eq_rel_def refl_on_def sym_def trans_def)
-done
-
-
-section {* Closure under Left-Quotients *}
-
-lemma closure_left_quotient:
- assumes "regular A"
- shows "regular (Ders_set B A)"
-proof -
- from assms obtain r::rexp where eq: "L r = A" by auto
- have fin: "finite (pders_set B r)" by (rule finite_pders_set)
-
- have "Ders_set B (L r) = (\<Union> L ` (pders_set B r))"
- by (simp add: Ders_set_pders_set)
- also have "\<dots> = L (\<Uplus>(pders_set B r))" using fin by simp
- finally have "Ders_set B A = L (\<Uplus>(pders_set B r))" using eq
- by simp
- then show "regular (Ders_set B A)" by auto
-qed
-
-
-section {* Relating standard and partial derivations *}
-
-lemma
- shows "(\<Union> L ` (pder c r)) = L (der c r)"
-unfolding Der_der[symmetric] Der_pder by simp
-
-lemma
- shows "(\<Union> L ` (pders s r)) = L (ders s r)"
-unfolding Ders_ders[symmetric] Ders_pders by simp
-
-
-section {* attempt to prove MN *}
-(*
-lemma Myhill_Nerode3:
- fixes r::"rexp"
- shows "finite (UNIV // =(\<lambda>x. pders x r)=)"
-apply(rule finite_eq_tag_rel)
-apply(rule finite_pders_set)
-apply(simp add: Range_def)
-unfolding Quotien_def
-by (induct r) (auto)
-*)
-
-fun
- width :: "rexp \<Rightarrow> nat"
-where
- "width (NULL) = 0"
-| "width (EMPTY) = 0"
-| "width (CHAR c) = 1"
-| "width (ALT r1 r2) = width r1 + width r2"
-| "width (SEQ r1 r2) = width r1 + width r2"
-| "width (STAR r) = width r"
-
-
-
-end
\ No newline at end of file