diff -r f824e1331fc6 -r bd5a8a6b3871 progs/Matcher.thy
--- a/progs/Matcher.thy	Wed Nov 27 08:49:51 2013 +0000
+++ b/progs/Matcher.thy	Wed Nov 27 21:36:30 2013 +0000
@@ -2,6 +2,7 @@
   imports "Main" 
 begin
 
+
 section {* Regular Expressions *}
 
 datatype rexp =
@@ -82,6 +83,34 @@
 | "nullable (STAR r) = True"
 
 fun
+ noccurs :: "rexp \<Rightarrow> bool"
+where
+  "noccurs (NULL) = True"
+| "noccurs (EMPTY) = False"
+| "noccurs (CHAR c) = False"
+| "noccurs (ALT r1 r2) = (noccurs r1 \<or> noccurs r2)"
+| "noccurs (SEQ r1 r2) = (noccurs r1 \<or> noccurs r2)"
+| "noccurs (STAR r) = (noccurs r)"
+
+lemma
+  "\<not> noccurs r \<Longrightarrow> L r \<noteq> {}"
+apply(induct r)
+apply(auto simp add: Seq_def)
+done
+
+lemma
+  "L r = {} \<Longrightarrow> noccurs r"
+apply(induct r)
+apply(auto simp add: Seq_def)
+done
+
+lemma does_not_hold:
+  "noccurs r \<Longrightarrow> L r = {}"
+apply(induct r)
+apply(auto simp add: Seq_def)
+oops
+
+fun
  der :: "char \<Rightarrow> rexp \<Rightarrow> rexp"
 where
   "der c (NULL) = NULL"
@@ -110,6 +139,25 @@
 by (induct r) (auto simp add: Seq_def) 
 section {* Left-Quotient of a Set *}
 
+fun
+ zeroable :: "rexp \<Rightarrow> bool"
+where
+  "zeroable (NULL) = True"
+| "zeroable (EMPTY) = False"
+| "zeroable (CHAR c) = False"
+| "zeroable (ALT r1 r2) = (zeroable r1 \<and> zeroable r2)"
+| "zeroable (SEQ r1 r2) = (zeroable r1 \<or> zeroable r2)"
+| "zeroable (STAR r) = False"
+
+
+lemma zeroable_correctness:
+  shows "zeroable r  \<longleftrightarrow>  (L r = {})"
+apply(induct r)
+apply(auto simp add: Seq_def)[6]
+done
+
+section {* Left-Quotient of a Set *}
+
 definition
   Der :: "char \<Rightarrow> string set \<Rightarrow> string set"
 where