--- a/Regular_Set.thy	Mon Oct 15 13:23:52 2012 +0000
+++ b/Regular_Set.thy	Mon Dec 03 08:16:58 2012 +0000
@@ -11,6 +11,9 @@
 definition conc :: "'a lang \<Rightarrow> 'a lang \<Rightarrow> 'a lang" (infixr "@@" 75) where
 "A @@ B = {xs@ys | xs ys. xs:A & ys:B}"
 
+text {* checks the code preprocessor for set comprehensions *}
+export_code conc checking SML
+
 overloading lang_pow == "compow :: nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
 begin
   primrec lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
@@ -18,6 +21,18 @@
   "lang_pow (Suc n) A = A @@ (lang_pow n A)"
 end
 
+text {* for code generation *}
+
+definition lang_pow :: "nat \<Rightarrow> 'a lang \<Rightarrow> 'a lang" where
+  lang_pow_code_def [code_abbrev]: "lang_pow = compow"
+
+lemma [code]:
+  "lang_pow (Suc n) A = A @@ (lang_pow n A)"
+  "lang_pow 0 A = {[]}"
+  by (simp_all add: lang_pow_code_def)
+
+hide_const (open) lang_pow
+
 definition star :: "'a lang \<Rightarrow> 'a lang" where
 "star A = (\<Union>n. A ^^ n)"
 
@@ -54,6 +69,9 @@
 and   "UNION I M @@ A = UNION I (%i. M i @@ A)"
 by auto
 
+lemma conc_subset_lists: "A \<subseteq> lists S \<Longrightarrow> B \<subseteq> lists S \<Longrightarrow> A @@ B \<subseteq> lists S"
+by(fastforce simp: conc_def in_lists_conv_set)
+
 
 subsection{* @{term "A ^^ n"} *}
 
@@ -72,15 +90,21 @@
 
 lemma length_lang_pow_ub:
   "ALL w : A. length w \<le> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<le> k*n"
-by(induct n arbitrary: w) (fastsimp simp: conc_def)+
+by(induct n arbitrary: w) (fastforce simp: conc_def)+
 
 lemma length_lang_pow_lb:
   "ALL w : A. length w \<ge> k \<Longrightarrow> w : A^^n \<Longrightarrow> length w \<ge> k*n"
-by(induct n arbitrary: w) (fastsimp simp: conc_def)+
+by(induct n arbitrary: w) (fastforce simp: conc_def)+
+
+lemma lang_pow_subset_lists: "A \<subseteq> lists S \<Longrightarrow> A ^^ n \<subseteq> lists S"
+by(induction n)(auto simp: conc_subset_lists[OF assms])
 
 
 subsection{* @{const star} *}
 
+lemma star_subset_lists: "A \<subseteq> lists S \<Longrightarrow> star A \<subseteq> lists S"
+unfolding star_def by(blast dest: lang_pow_subset_lists)
+
 lemma star_if_lang_pow[simp]: "w : A ^^ n \<Longrightarrow> w : star A"
 by (auto simp: star_def)
 
@@ -161,7 +185,7 @@
 qed
 
 lemma star_conv_concat: "star A = {concat ws|ws. set ws \<subseteq> A}"
-by (fastsimp simp: in_star_iff_concat)
+by (fastforce simp: in_star_iff_concat)
 
 lemma star_insert_eps[simp]: "star (insert [] A) = star(A)"
 proof-
@@ -180,6 +204,68 @@
   shows "\<exists>a b. x = a @ b \<and> a \<noteq> [] \<and> a \<in> A \<and> b \<in> star A"
 using a by (induct rule: star_induct) (blast)+
 
+
+subsection {* Left-Quotients of languages *}
+
+definition Deriv :: "'a \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Deriv x A = { xs. x#xs \<in> A }"
+
+definition Derivs :: "'a list \<Rightarrow> 'a lang \<Rightarrow> 'a lang"
+where "Derivs xs A = { ys. xs @ ys \<in> A }"
+
+abbreviation 
+  Derivss :: "'a list \<Rightarrow> 'a lang set \<Rightarrow> 'a lang"
+where
+  "Derivss s As \<equiv> \<Union> (Derivs s) ` As"
+
+
+lemma Deriv_empty[simp]:   "Deriv a {} = {}"
+  and Deriv_epsilon[simp]: "Deriv a {[]} = {}"
+  and Deriv_char[simp]:    "Deriv a {[b]} = (if a = b then {[]} else {})"
+  and Deriv_union[simp]:   "Deriv a (A \<union> B) = Deriv a A \<union> Deriv a B"
+  and Deriv_inter[simp]:   "Deriv a (A \<inter> B) = Deriv a A \<inter> Deriv a B"
+  and Deriv_compl[simp]:   "Deriv a (-A) = - Deriv a A"
+  and Deriv_Union[simp]:   "Deriv a (Union M) = Union(Deriv a ` M)"
+  and Deriv_UN[simp]:      "Deriv a (UN x:I. S x) = (UN x:I. Deriv a (S x))"
+by (auto simp: Deriv_def)
+
+lemma Der_conc [simp]: "Deriv c (A @@ B) = (Deriv c A) @@ B \<union> (if [] \<in> A then Deriv c B else {})"
+unfolding Deriv_def conc_def
+by (auto simp add: Cons_eq_append_conv)
+
+lemma Deriv_star [simp]: "Deriv c (star A) = (Deriv c A) @@ star A"
+proof -
+  have incl: "[] \<in> A \<Longrightarrow> Deriv c (star A) \<subseteq> (Deriv c A) @@ star A"
+    unfolding Deriv_def conc_def 
+    apply(auto simp add: Cons_eq_append_conv)
+    apply(drule star_decom)
+    apply(auto simp add: Cons_eq_append_conv)
+    done
+
+  have "Deriv c (star A) = Deriv c (A @@ star A \<union> {[]})"
+    by (simp only: star_unfold_left[symmetric])
+  also have "... = Deriv c (A @@ star A)"
+    by (simp only: Deriv_union) (simp)
+  also have "... =  (Deriv c A) @@ (star A) \<union> (if [] \<in> A then Deriv c (star A) else {})"
+    by simp
+   also have "... =  (Deriv c A) @@ star A"
+    using incl by auto
+  finally show "Deriv c (star A) = (Deriv c A) @@ star A" . 
+qed
+
+lemma Deriv_diff[simp]: "Deriv c (A - B) = Deriv c A - Deriv c B"
+by(auto simp add: Deriv_def)
+
+lemma Deriv_lists[simp]: "c : S \<Longrightarrow> Deriv c (lists S) = lists S"
+by(auto simp add: Deriv_def)
+
+lemma Derivs_simps [simp]:
+  shows "Derivs [] A = A"
+  and   "Derivs (c # s) A = Derivs s (Deriv c A)"
+  and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
+unfolding Derivs_def Deriv_def by auto
+
+
 subsection {* Arden's Lemma *}
 
 lemma arden_helper:
@@ -290,5 +376,4 @@
     using eq by blast 
 qed
 
-
 end