diff -r 98d51a89d5a9 -r 654b542ce8db thys/LexerExt.thy
--- a/thys/LexerExt.thy	Tue Mar 07 00:24:10 2017 +0000
+++ b/thys/LexerExt.thy	Wed Mar 08 10:32:51 2017 +0000
@@ -789,11 +789,10 @@
     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> Stars (v # vs)"
 | Posix_NMTIMES2: "s \<in> UPNTIMES r m \<rightarrow> Stars vs \<Longrightarrow>  s \<in> NMTIMES r 0 m \<rightarrow> Stars vs"
-| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; 
+| Posix_PLUS1: "\<lbrakk>s1 \<in> r \<rightarrow> v; s2 \<in> STAR r \<rightarrow> Stars vs; flat v = [] \<Longrightarrow> flat (Stars vs) = [];
     \<not>(\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (s1 @ s\<^sub>3) \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))\<rbrakk>
     \<Longrightarrow> (s1 @ s2) \<in> PLUS r \<rightarrow> Stars (v # vs)"
 
-
 inductive_cases Posix_elims:
   "s \<in> ZERO \<rightarrow> v"
   "s \<in> ONE \<rightarrow> v"
@@ -822,6 +821,48 @@
 done
 
 
+lemma 
+  "([] @ []) \<in> PLUS (ONE) \<rightarrow> Stars ([Void])"
+apply(rule Posix_PLUS1)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(simp)
+apply(simp)
+done
+
+lemma 
+  assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []" "\<forall>s' \<in> L r. length s' < length s"
+  shows "([] @ (s @ [])) \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left Void, Right v])"
+using assms
+oops
+
+lemma 
+  "([] @ ([] @ [])) \<in> FROMNTIMES (ONE) (Suc (Suc 0)) \<rightarrow> Stars ([Void, Void])"
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(rule Posix.intros)
+apply(auto)
+done
+
+
+lemma 
+  assumes "s \<in> r \<rightarrow> v" "flat v \<noteq> []"
+  "s \<in> PLUS (ALT ONE r) \<rightarrow> Stars ([Left(Void), Right(v)])"
+  shows "False"
+using assms
+apply(rotate_tac 2)
+apply(erule_tac Posix.cases)
+apply(simp_all)
+apply(auto)
+oops
+
+
+
+
+
 lemma Posix1a:
   assumes "s \<in> r \<rightarrow> v"
   shows "\<turnstile> v : r"
@@ -1131,12 +1172,12 @@
 next
   case (Posix_PLUS1 s1 r v s2 vs v2)
   have "(s1 @ s2) \<in> PLUS r \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs"
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (STAR r) \<rightarrow> Stars vs" (*"flat v = [] \<Longrightarrow> flat (Stars vs) = []"*)
        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (STAR r) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
-  by (metis Posix1(1) Posix_PLUS1.hyps(5) append_Nil2 self_append_conv2)
+  by (metis Posix1(1) Posix_PLUS1.hyps(6) append_self_conv append_self_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> STAR r \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1533,36 +1574,32 @@
   case (PLUS r)
   have IH: "\<And>s v. s \<in> der c r \<rightarrow> v \<Longrightarrow> (c # s) \<in> r \<rightarrow> injval r c v" by fact
   have "s \<in> der c (PLUS r) \<rightarrow> v" by fact
-  then consider
-      (cons) v1 vs s1 s2 where 
-        "v = Seq v1 (Stars vs)" "s = s1 @ s2" 
-        "s1 \<in> der c r \<rightarrow> v1" "s2 \<in> (STAR r) \<rightarrow> (Stars vs)"
-        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" 
-        apply(simp)
-        apply(auto elim!: Posix_elims(1-5) simp add: der_correctness Der_def intro: Posix.intros)
-        defer     
-        apply(rotate_tac 3)
-        apply(erule_tac Posix_elims(6))
-        apply (simp add: Posix.intros(6))
-        using Posix.intros(7) by blast
-    then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" 
-    proof (cases)
-      case cons
-          have "s1 \<in> der c r \<rightarrow> v1" by fact
-          then have "(c # s1) \<in> r \<rightarrow> injval r c v1" using IH by simp
-        moreover
-          have "s2 \<in> STAR r \<rightarrow> Stars vs" by fact
-        moreover 
-          have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L (der c r) \<and> s\<^sub>4 \<in> L (STAR r))" by fact
-          then have "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> (c # s1) @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (STAR r))" 
-            by (simp add: der_correctness Der_def)
-        ultimately 
-        have "((c # s1) @ s2) \<in> (PLUS r) \<rightarrow> Stars (injval r c v1 # vs)" 
-          apply(rule_tac Posix.intros)
-          apply(simp_all)
-          done
-        then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v" using cons by(simp)
-    qed
+  then show "(c # s) \<in> PLUS r \<rightarrow> injval (PLUS r) c v"
+  apply -
+  apply(erule Posix.cases)
+  apply(simp_all)
+  apply(auto)
+  apply(rotate_tac 3)
+  apply(erule Posix.cases)
+  apply(simp_all)
+  apply(subst append_Cons[symmetric])
+  apply(rule Posix.intros)
+  using PLUS.hyps apply auto[1]
+  apply(rule Posix.intros)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  apply(simp)
+  using Posix1a Prf_injval_flat apply auto[1]
+  apply(simp add: der_correctness Der_def)
+  apply(subst append_Nil2[symmetric])
+  apply(rule Posix.intros)
+  using PLUS.hyps apply auto[1]
+  apply(rule Posix.intros)
+  apply(simp)
+  apply(simp)
+  done  
 qed
 
 
@@ -1602,5 +1639,8 @@
 using Posix1(1) Posix_determ lexer_correct_None lexer_correct_Some apply fastforce
 using Posix1(1) lexer_correct_None lexer_correct_Some by blast
 
+value "lexer (PLUS (ALT ONE (SEQ (CHAR (CHR ''a'')) (CHAR (CHR ''b''))))) [CHR ''a'', CHR ''b'']"
+
+
 unused_thms
 end
\ No newline at end of file