161 | "ders (c # s) r = ders s (der c r)"

   161 | "ders (c # s) r = ders s (der c r)"

   162 

   162 

   163 

   163 

   164 lemma nullable_correctness:

   164 lemma nullable_correctness:

   165   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   165   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"

   166 by (induct r) (auto simp add: Sequ_def) 

   167 by (induct r) (auto simp add: Sequ_def) 

   167 

   168 

   168 lemma der_correctness:

   169 lemma der_correctness:

   169   shows "L (der c r) = Der c (L r)"

   170   shows "L (der c r) = Der c (L r)"

   170 by (induct r) (simp_all add: nullable_correctness)

   171 by (induct r) (simp_all add: nullable_correctness)