--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Regular_Exp.thy	Mon Jul 25 13:33:38 2011 +0000
@@ -0,0 +1,36 @@
+(*  Author:     Tobias Nipkow
+    Copyright   1998 TUM
+*)
+
+header "Regular expressions"
+
+theory Regular_Exp
+imports Regular_Set
+begin
+
+datatype 'a rexp =
+  Zero |
+  One |
+  Atom 'a |
+  Plus "('a rexp)" "('a rexp)" |
+  Times "('a rexp)" "('a rexp)" |
+  Star "('a rexp)"
+
+primrec lang :: "'a rexp => 'a list set" where
+"lang Zero = {}" |
+"lang One = {[]}" |
+"lang (Atom a) = {[a]}" |
+"lang (Plus r s) = (lang r) Un (lang s)" |
+"lang (Times r s) = conc (lang r) (lang s)" |
+"lang (Star r) = star(lang r)"
+
+primrec atoms :: "'a rexp \<Rightarrow> 'a set"
+where
+"atoms Zero = {}" |
+"atoms One = {}" |
+"atoms (Atom a) = {a}" |
+"atoms (Plus r s) = atoms r \<union> atoms s" |
+"atoms (Times r s) = atoms r \<union> atoms s" |
+"atoms (Star r) = atoms r"
+
+end