diff -r db0ff630bbb7 -r 43e070803c1c thys/Exercises.thy
--- a/thys/Exercises.thy	Thu Apr 11 17:37:00 2019 +0100
+++ b/thys/Exercises.thy	Fri May 10 11:56:37 2019 +0100
@@ -50,9 +50,8 @@
 apply(simp_all add: zeroable_correctness nullable_correctness Sequ_def)
 using Nil_is_append_conv apply blast
 apply blast
-apply(auto)
-using Star_cstring
-  by (metis concat_eq_Nil_conv) 
+  apply(auto)
+  by (metis Star_decomp hd_Cons_tl list.distinct(1))
 
 lemma atmostempty_correctness_aux:
   shows "atmostempty r \<longleftrightarrow> \<not> somechars r"
@@ -110,8 +109,22 @@
 lemma Star_atmostempty:
   assumes "A \<subseteq> {[]}"
   shows "A\<star> \<subseteq> {[]}"
-using assms
-using Star_cstring concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD by fastforce
+  using assms
+  using Star_decomp concat_eq_Nil_conv empty_iff insert_iff subsetI subset_singletonD 
+  apply(auto)
+proof -
+  fix x :: "char list"
+  assume a1: "x \<in> A\<star>"
+  assume "\<And>c x A. c # x \<in> A\<star> \<Longrightarrow> \<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"
+  then have f2: "\<forall>cs C c. \<exists>csa. c # csa \<in> C \<or> c # cs \<notin> C\<star>"
+    by auto
+  obtain cc :: "char list \<Rightarrow> char" and ccs :: "char list \<Rightarrow> char list" where
+    "\<And>cs. cs = [] \<or> cc cs # ccs cs = cs"
+    by (metis (no_types) list.exhaust)
+  then show "x = []"
+    using f2 a1 by (metis assms empty_iff insert_iff list.distinct(1) subset_singletonD)
+qed
+  
 
 lemma Star_empty_string_finite:
   shows "finite ({[]}\<star>)"