--- a/Regular_Exp.thy	Fri Jul 05 12:07:48 2013 +0100
+++ b/Regular_Exp.thy	Fri Jul 05 17:19:17 2013 +0100
@@ -24,8 +24,7 @@
 "lang (Times r s) = conc (lang r) (lang s)" |
 "lang (Star r) = star(lang r)"
 
-primrec atoms :: "'a rexp \<Rightarrow> 'a set"
-where
+primrec atoms :: "'a rexp \<Rightarrow> 'a set" where
 "atoms Zero = {}" |
 "atoms One = {}" |
 "atoms (Atom a) = {a}" |
@@ -33,4 +32,15 @@
 "atoms (Times r s) = atoms r \<union> atoms s" |
 "atoms (Star r) = atoms r"
 
+primrec nullable :: "'a rexp \<Rightarrow> bool" where
+"nullable (Zero) = False" |
+"nullable (One) = True" |
+"nullable (Atom c) = False" |
+"nullable (Plus r1 r2) = (nullable r1 \<or> nullable r2)" |
+"nullable (Times r1 r2) = (nullable r1 \<and> nullable r2)" |
+"nullable (Star r) = True"
+
+lemma nullable_iff: "nullable r \<longleftrightarrow> [] \<in> lang r"
+by (induct r) (auto simp add: conc_def split: if_splits)
+
 end