--- a/progs/Matcher.thy	Thu Dec 11 12:34:03 2025 +0000
+++ b/progs/Matcher.thy	Mon Dec 15 18:32:26 2025 +0000
@@ -88,48 +88,6 @@
 lemma nullable_correctness:
   shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
 apply(induct r)
-(* ZERO case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-(* ONE case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-(* CHAR case *)
-apply(simp only: nullable.simps)
-apply(simp only: L.simps)
-apply(simp)
-prefer 2
-(* ALT case *)
-apply(simp (no_asm) only: nullable.simps)
-apply(simp only:)
-apply(simp only: L.simps)
-apply(simp)
-(* SEQ case *)
-apply(simp only: L.simps)
-apply(simp)
-oops
-
-lemma nullable_correctness:
-  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
-apply(simp_all)
-(* all easy subgoals are proved except the last 2 *)
-(* where the definition of Seq needs to be unfolded. *)
-oops
-
-lemma nullable_correctness:
-  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
-apply(simp_all add: Seq_def)
-(* except the star case every thing is proved *)
-(* we need to use the rule for Star.start *)
-oops
-
-lemma nullable_correctness:
-  shows "nullable r  \<longleftrightarrow> [] \<in> (L r)"
-apply(induct r)
 apply(simp_all add: Seq_def Star.start)
 done