--- a/Closures.thy	Mon Sep 05 15:42:29 2011 +0000
+++ b/Closures.thy	Mon Sep 05 20:59:50 2011 +0000
@@ -209,7 +209,7 @@
 qed
 
 
-subsection {* Non-regularity for languages *}
+subsection {* Continuation lemma for showing non-regularity of languages *}
 
 lemma continuation_lemma:
   fixes A B::"'a::finite lang"
@@ -243,7 +243,7 @@
 qed
 
 
-subsubsection {* The language @{text "a ^ n b ^ n"} is not regular *}
+subsection {* The language @{text "a\<^sup>n b\<^sup>n"} is not regular *}
 
 abbreviation
   replicate_rev ("_ ^^^ _" [100, 100] 100)

--- a/Derivatives.thy	Mon Sep 05 15:42:29 2011 +0000
+++ b/Derivatives.thy	Mon Sep 05 20:59:50 2011 +0000
@@ -1,9 +1,11 @@
+header "Derivatives of regular expressions"
+
+(* Author: Christian Urban *)
+
 theory Derivatives
 imports Regular_Exp
 begin
 
-section {* Leftquotients, Derivatives and Partial Derivatives *}
-
 text{* This theory is based on work by Brozowski \cite{Brzozowski64} and Antimirov \cite{Antimirov95}. *}
 
 subsection {* Left-Quotients of languages *}
@@ -69,15 +71,8 @@
   and   "Derivs (s1 @ s2) A = Derivs s2 (Derivs s1 A)"
 unfolding Derivs_def Deriv_def by auto
 
-(*
-lemma Deriv_insert_eps[simp]: 
-"Deriv a (insert [] A) = Deriv a A"
-by (auto simp: Deriv_def)
-*)
 
-
-
-subsection {* Brozowsky's derivatives of regular expressions *}
+subsection {* Brozowski's derivatives of regular expressions *}
 
 fun
   nullable :: "'a rexp \<Rightarrow> bool"
@@ -383,4 +378,17 @@
 by (metis finite_pderivs_lang_UNIV pderivs_lang_subset rev_finite_subset subset_UNIV)
 
 
+subsection {* A regular expression matcher based on Brozowski's derivatives *}
+
+fun
+  matcher :: "'a rexp \<Rightarrow> 'a list \<Rightarrow> bool"
+where
+  "matcher r s = nullable (derivs s r)"
+
+lemma matcher_correctness:
+  shows "matcher r s \<longleftrightarrow> s \<in> lang r"
+by (induct s arbitrary: r)
+   (simp_all add: nullable_iff Deriv_deriv[symmetric] Deriv_def)
+
+
 end
\ No newline at end of file