--- a/Derivs.thy Tue May 31 20:32:49 2011 +0000
+++ b/Derivs.thy Thu Jun 02 16:44:35 2011 +0000
@@ -1,8 +1,8 @@
theory Derivs
-imports Closure
+imports Myhill_2
begin
-section {* Experiments with Derivatives -- independent of Myhill-Nerode *}
+section {* Left-Quotients and Derivatives *}
subsection {* Left-Quotients *}
@@ -52,30 +52,30 @@
by auto
lemma Der_seq [simp]:
- shows "Der c (A ;; B) = (Der c A) ;; B \<union> (Delta A ;; Der c B)"
+ shows "Der c (A \<cdot> B) = (Der c A) \<cdot> B \<union> (Delta A \<cdot> 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>"
+ shows "Der c (A\<star>) = (Der c A) \<cdot> A\<star>"
proof -
- have incl: "Delta A ;; Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
+ 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 ;; A\<star>)"
+ have "Der c (A\<star>) = Der c ({[]} \<union> A \<cdot> A\<star>)"
by (simp only: star_cases[symmetric])
- also have "... = Der c (A ;; A\<star>)"
+ also have "... = Der c (A \<cdot> A\<star>)"
by (simp only: Der_union Der_empty) (simp)
- also have "... = (Der c A) ;; A\<star> \<union> (Delta A ;; Der c (A\<star>))"
+ also have "... = (Der c A) \<cdot> A\<star> \<union> (Delta A \<cdot> Der c (A\<star>))"
by simp
- also have "... = (Der c A) ;; A\<star>"
+ also have "... = (Der c A) \<cdot> A\<star>"
using incl by auto
- finally show "Der c (A\<star>) = (Der c A) ;; A\<star>" .
+ finally show "Der c (A\<star>) = (Der c A) \<cdot> A\<star>" .
qed
@@ -126,18 +126,18 @@
by (relation "measure (length o fst)") (auto)
lemma Delta_nullable:
- shows "Delta (L r) = (if nullable r then {[]} else {})"
+ shows "Delta (L_rexp 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)"
+ 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 r) = L (ders s r)"
+ 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)
@@ -195,44 +195,44 @@
done
lemma pder_set_lang:
- shows "(\<Union> (L ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L ` (pder c r)))"
+ shows "(\<Union> (L_rexp ` pder_set c R)) = (\<Union>r \<in> R. (\<Union>L_rexp ` (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)"
+ 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 auto
lemma Der_pder:
fixes r::rexp
- shows "Der c (L r) = \<Union> L ` (pder c r)"
+ 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 r) = \<Union> L ` (pders s r)"
+ 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 r) = \<Union> L ` (pders s r)" by fact
- have "Ders (s @ [c]) (L r) = Ders [c] (Ders s (L r))"
+ 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 ` (pders s r))" using ih
+ 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 r))"
+ 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 ` (pder c r)))"
+ 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 ` (pder_set c (pders s r)))"
+ also have "\<dots> = (\<Union>L_rexp ` (pder_set c (pders s r)))"
by (simp add: pder_set_lang)
- also have "\<dots> = (\<Union>L ` (pders (s @ [c]) r))"
+ also have "\<dots> = (\<Union>L_rexp ` (pders (s @ [c]) r))"
by simp
- finally show "Ders (s @ [c]) (L r) = \<Union>L ` pders (s @ [c]) r" .
+ 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 r) = (\<Union> L ` (pders_set A r))"
+ 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]:
@@ -255,12 +255,12 @@
"Suf s \<equiv> {v. v \<noteq> [] \<and> (\<exists>u. u @ v = s)}"
lemma Suf:
- shows "Suf (s @ [c]) = (Suf s) ;; {[c]} \<union> {[c]}"
+ shows "Suf (s @ [c]) = (Suf s) \<cdot> {[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]))"
+ 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:
@@ -277,7 +277,7 @@
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
+ 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))"
@@ -309,7 +309,7 @@
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
+ 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))"
@@ -444,78 +444,49 @@
lemma Myhill_Nerode3:
fixes r::"rexp"
- shows "finite (UNIV // \<approx>(L r))"
+ shows "finite (UNIV // \<approx>(L_rexp r))"
proof -
have "finite (UNIV // =(\<lambda>x. pders x r)=)"
proof -
- have "range (\<lambda>x. pders x r) \<subseteq> {pders s r | s. s \<in> UNIV}" by auto
+ 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 (rule finite_subset)
+ 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 r)"
+ have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(L_rexp r)"
unfolding tag_eq_rel_def
- by (auto simp add: str_eq_def[symmetric] MN_Rel_Ders Ders_pders)
+ 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 r))"
+ 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 r))"
+ ultimately show "finite (UNIV // \<approx>(L_rexp r))"
by (rule refined_partition_finite)
qed
-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 *}
+section {* Relating derivatives and partial derivatives *}
lemma
- shows "(\<Union> L ` (pder c r)) = L (der c r)"
+ shows "(\<Union> L_rexp ` (pder c r)) = L_rexp (der c r)"
unfolding Der_der[symmetric] Der_pder by simp
lemma
- shows "(\<Union> L ` (pders s r)) = L (ders s r)"
+ shows "(\<Union> L_rexp ` (pders s r)) = L_rexp (ders s r)"
unfolding Ders_ders[symmetric] Ders_pders by simp
-
-
-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