--- a/Matcher.thy	Mon Feb 14 11:12:01 2011 +0000
+++ b/Matcher.thy	Mon Feb 14 23:10:44 2011 +0000
@@ -6,9 +6,9 @@
 section {* Sequential Composition of Sets *}
 
 fun
-  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ; _" [100,100] 100)
+  lang_seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100)
 where 
-  "L1 ; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
+  "L1 ;; L2 = {s1 @ s2 | s1 s2. s1 \<in> L1 \<and> s2 \<in> L2}"
 
 
 section {* Kleene Star for Sets *}
@@ -24,7 +24,7 @@
 text {* A standard property of Star *}
 
 lemma lang_star_cases:
-  shows "L\<star> =  {[]} \<union> L ; L\<star>"
+  shows "L\<star> =  {[]} \<union> L ;; L\<star>"
 by (auto) (metis Star.simps)
 
 section {* Regular Expressions *}
@@ -37,14 +37,39 @@
 | ALT rexp rexp
 | STAR rexp
 
+types lang = "string set" 
 
 definition
+  DERIV :: "string \<Rightarrow> lang \<Rightarrow> lang"
+where
   "DERIV s A \<equiv> {s'. s @ s' \<in> A}"
 
 definition
+  delta :: "lang \<Rightarrow> lang"
+where
   "delta A = (if [] \<in> A then {[]} else {})"
 
+lemma
+  "DERIV s (P ; Q) = \<Union>{(delta (DERIV s1 P)) ; (DERIV s2 Q) | s1 s2. s = s1 @ s2}"
+apply(auto)
 
+fun
+  D1 :: "string \<Rightarrow> lang \<Rightarrow> lang"
+where
+  "D1 [] A = A"
+| "D1 (c # s) A = DERIV [c] (D1 s A)"
+
+fun
+  D2 :: "string \<Rightarrow> lang \<Rightarrow> lang"
+where
+  "D2 [] A = A"
+| "D2 (c # s) A = DERIV [c] (D1 s A)"
+
+function
+  D
+where
+  "D s P Q = P ;; Q"
+| "D (c#s) = 
 
 section {* Semantics of Regular Expressions *}