--- a/thys/Exercises.thy	Fri Jan 12 02:33:35 2018 +0000
+++ b/thys/Exercises.thy	Tue May 15 10:24:25 2018 +0100
@@ -30,6 +30,8 @@
      zeroable r1 \<or> zeroable r2 \<or> (atmostempty r1 \<and> atmostempty r2)"
 | "atmostempty (STAR r) = atmostempty r"
 
+
+
 fun
  somechars :: "rexp \<Rightarrow> bool"
 where
@@ -50,8 +52,7 @@
 apply blast
 apply(auto)
 using Star_cstring
-by (metis concat_eq_Nil_conv) 
-
+  by (metis concat_eq_Nil_conv) 
 
 lemma atmostempty_correctness_aux:
   shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
@@ -65,6 +66,33 @@
 by(auto simp add: atmostempty_correctness_aux somechars_correctness)
 
 fun
+ leastsinglechar :: "rexp \<Rightarrow> bool"
+where
+  "leastsinglechar (ZERO) \<longleftrightarrow> False"
+| "leastsinglechar (ONE) \<longleftrightarrow> False"
+| "leastsinglechar (CHAR c) \<longleftrightarrow> True"
+| "leastsinglechar (ALT r1 r2) \<longleftrightarrow> leastsinglechar r1 \<or> leastsinglechar r2"
+| "leastsinglechar (SEQ r1 r2) \<longleftrightarrow> 
+      (if (zeroable r1 \<or> zeroable r2) then False
+       else ((nullable r1 \<and> leastsinglechar r2) \<or> (nullable r2 \<and> leastsinglechar r1)))"
+| "leastsinglechar (STAR r) \<longleftrightarrow> leastsinglechar r"
+
+lemma leastsinglechar_correctness:
+  "leastsinglechar r \<longleftrightarrow> (\<exists>c. [c] \<in> L r)"
+  apply(induct r)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  prefer 2
+  apply(simp)
+  apply(blast)
+  prefer 2
+  apply(simp)
+  using Star.step Star_decomp apply fastforce
+  apply(simp add: Sequ_def zeroable_correctness nullable_correctness)
+  by (metis append_Nil append_is_Nil_conv butlast_append butlast_snoc)
+
+fun
  infinitestrings :: "rexp \<Rightarrow> bool"
 where
   "infinitestrings (ZERO) = False"