--- a/thys/Lexer.thy	Thu Jul 06 16:05:33 2017 +0100
+++ b/thys/Lexer.thy	Tue Jul 18 18:39:20 2017 +0100
@@ -79,17 +79,20 @@
 by (auto) (metis Star.simps)
 
 lemma Star_decomp: 
-  assumes a: "c # x \<in> A\<star>" 
-  shows "\<exists>a b. x = a @ b \<and> c # a \<in> A \<and> b \<in> A\<star>"
-using a
+  assumes "c # x \<in> A\<star>" 
+  shows "\<exists>s1 s2. x = s1 @ s2 \<and> c # s1 \<in> A \<and> s2 \<in> A\<star>"
+using assms
 by (induct x\<equiv>"c # x" rule: Star.induct) 
    (auto simp add: append_eq_Cons_conv)
 
 lemma Star_Der_Sequ: 
   shows "Der c (A\<star>) \<subseteq> (Der c A) ;; A\<star>"
 unfolding Der_def
-by(auto simp add: Der_def Sequ_def Star_decomp)
-
+apply(rule subsetI)
+apply(simp)
+unfolding Sequ_def
+apply(simp)
+by(auto simp add: Sequ_def Star_decomp)
 
 
 lemma Der_star [simp]:
@@ -245,8 +248,7 @@
 | "\<turnstile> v2 : r2 \<Longrightarrow> \<turnstile> Right v2 : ALT r1 r2"
 | "\<turnstile> Void : ONE"
 | "\<turnstile> Char c : CHAR c"
-| "\<turnstile> Stars [] : STAR r"
-| "\<lbrakk>\<turnstile> v : r; \<turnstile> Stars vs : STAR r\<rbrakk> \<Longrightarrow> \<turnstile> Stars (v # vs) : STAR r"
+| "\<forall>v \<in> set vs. \<turnstile> v : r \<Longrightarrow> \<turnstile> Stars vs : STAR r"
 
 inductive_cases Prf_elims:
   "\<turnstile> v : ZERO"
@@ -254,31 +256,25 @@
   "\<turnstile> v : ALT r1 r2"
   "\<turnstile> v : ONE"
   "\<turnstile> v : CHAR c"
-(*  "\<turnstile> vs : STAR r"*)
+  "\<turnstile> vs : STAR r"
+
+lemma Star_concat:
+  assumes "\<forall>s \<in> set ss. s \<in> A"  
+  shows "concat ss \<in> A\<star>"
+using assms by (induct ss) (auto)
+
 
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-by(induct v r rule: Prf.induct)
-  (auto simp add: Sequ_def)
-
-lemma Prf_Stars:
-  assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
-  shows "\<turnstile> Stars vs : STAR r"
-using assms
-by(induct vs) (auto intro: Prf.intros)
+by (induct v r rule: Prf.induct)
+   (auto simp add: Sequ_def Star_concat)
 
 lemma Prf_Stars_append:
   assumes "\<turnstile> Stars vs1 : STAR r" "\<turnstile> Stars vs2 : STAR r"
   shows "\<turnstile> Stars (vs1 @ vs2) : STAR r"
 using assms
-apply(induct vs1 arbitrary: vs2)
-apply(auto intro: Prf.intros)
-apply(erule Prf.cases)
-apply(simp_all)
-apply(auto intro: Prf.intros)
-done
-
+by (auto intro!: Prf.intros elim!: Prf_elims)
 
 lemma Star_string:
   assumes "s \<in> A\<star>"
@@ -306,40 +302,45 @@
   assumes "\<turnstile> v : r" 
   shows "flat v \<in> L r"
 using assms
-by (induct)(auto simp add: Sequ_def)
+by (induct) (auto simp add: Sequ_def Star_concat)
 
 lemma L_flat_Prf2:
   assumes "s \<in> L r" 
   shows "\<exists>v. \<turnstile> v : r \<and> flat v = s"
 using assms
-apply(induct r arbitrary: s)
-apply(auto simp add: Sequ_def intro: Prf.intros)
-using Prf.intros(1) flat.simps(5) apply blast
-using Prf.intros(2) flat.simps(3) apply blast
-using Prf.intros(3) flat.simps(4) apply blast
-apply(subgoal_tac "\<exists>vs::val list. concat (map flat vs) = s \<and> (\<forall>v \<in> set vs. \<turnstile> v : r)")
-apply(auto)[1]
-apply(rule_tac x="Stars vs" in exI)
-apply(simp)
-apply (simp add: Prf_Stars)
-apply(drule Star_string)
-apply(auto)
-apply(rule Star_val)
-apply(auto)
-done
+proof(induct r arbitrary: s)
+  case (STAR r s)
+  have IH: "\<And>s. s \<in> L r \<Longrightarrow> \<exists>v. \<turnstile> v : r \<and> flat v = s" by fact
+  have "s \<in> L (STAR r)" by fact
+  then obtain ss where "concat ss = s" "\<forall>s \<in> set ss. s \<in> L r"
+  using Star_string by auto
+  then obtain vs where "concat (map flat vs) = s" "\<forall>v\<in>set vs. \<turnstile> v : r"
+  using IH Star_val by blast
+  then show "\<exists>v. \<turnstile> v : STAR r \<and> flat v = s"
+  using Prf.intros(6) flat_Stars by blast
+next 
+  case (SEQ r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : SEQ r1 r2 \<and> flat v = s"
+  unfolding Sequ_def L.simps by (fastforce intro: Prf.intros)
+next
+  case (ALT r1 r2 s)
+  then show "\<exists>v. \<turnstile> v : ALT r1 r2 \<and> flat v = s"
+  unfolding L.simps by (fastforce intro: Prf.intros)
+qed (auto intro: Prf.intros)
 
 lemma L_flat_Prf:
   "L(r) = {flat v | v. \<turnstile> v : r}"
 using L_flat_Prf1 L_flat_Prf2 by blast
 
+(*
 lemma Star_values_exists:
   assumes "s \<in> (L r)\<star>"
   shows "\<exists>vs. concat (map flat vs) = s \<and> \<turnstile> Stars vs : STAR r"
 using assms
 apply(drule_tac Star_string)
 apply(auto)
-by (metis L_flat_Prf2 Prf_Stars Star_val)
-
+by (metis L_flat_Prf2 Prf.intros(6) Star_val)
+*)
 
 
 section {* Sulzmann and Lu functions *}
@@ -385,24 +386,14 @@
 using assms
 apply(induct r arbitrary: c v rule: rexp.induct)
 apply(auto intro!: Prf.intros mkeps_nullable elim!: Prf_elims split: if_splits)
-(* STAR *)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)[7]
-apply(auto)
-apply (metis Prf.intros(6) Prf.intros(7))
-by (metis Prf.intros(7))
+done
 
 lemma Prf_injval_flat:
   assumes "\<turnstile> v : der c r" 
   shows "flat (injval r c v) = c # (flat v)"
 using assms
 apply(induct arbitrary: v rule: der.induct)
-apply(auto elim!: Prf_elims split: if_splits)
-apply(metis mkeps_flat)
-apply(rotate_tac 2)
-apply(erule Prf.cases)
-apply(simp_all)[7]
+apply(auto elim!: Prf_elims intro: mkeps_flat split: if_splits)
 done
 
 
@@ -444,7 +435,9 @@
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
 using assms
-by (induct s r v rule: Posix.induct)(auto intro: Prf.intros)
+apply(induct s r v rule: Posix.induct)
+apply(auto intro!: Prf.intros elim!: Prf_elims)
+done
 
 
 lemma Posix_mkeps: